Implement goto labels from GCC extended inline assembly syntax.

[jprotopopov-ut]

Enables inline assembly to specify a list of C labels where the assembler code might jump, turning inline asm into a control flow branching point.

Inline assembly is converted from instruction into a statement; dummy instruction is introduced to replace "empty" instances of inline assembly instruction previously used.

This feature is necessary for Linux kernel module analysis.

[sim642]

I didn't have a deep look at this yet but I want to point out that part of #161 (if not all) was to do the same thing. It needed some changes but the student moved on.

The hope is that this PR can replace it but this should also account for all the unfinished business discussed in #161 which prevented it from being merged.

On another note, #161 seems to have avoided the need for a DummyInstr which seems cleaner. But without having looked into it, I can't tell how avoidable that is.

[jprotopopov-ut]

I didn't have a deep look at this yet but I want to point out that part of #161 (if not all) was to do the same thing. It needed some changes but the student moved on.

The hope is that this PR can replace it but this should also account for all the unfinished business discussed in #161 which prevented it from being merged.

On another note, #161 seems to have avoided the need for a DummyInstr which seems cleaner. But without having looked into it, I can't tell how avoidable that is.

If I understand this comment correctly, #161 does not take goto labels into account in CFG:

We should leave a comment somewhere that for the purpose of computing the successors, we do not consider the gotos that could happen in inline assembly so this is clear to everyone. Probably even in the documentation.

My pull request attempts to faithfully represent potential inline asm goto there. Thus, I needed to upgrade the Asm into statement and introduce DummyInstr as a replacement at instruction level.

[sim642]

My pull request attempts to faithfully represent potential inline asm goto there. Thus, I needed to upgrade the Asm into statement and introduce DummyInstr as a replacement at instruction level.

Things might have been changed after that review comment because currently #161 moves Asm from instr to stmtkind as well, without needing a replacement under instr.

[jprotopopov-ut]

I looked through the code of #161. I presume, the relevant line is:

let dummyStmt =  mkStmt (Asm([], ["dummy statement!!"], [], [], [], [], lu))

I did my changes back in April and do not remember my exact rationale for changing that, but I think I was just baffled with use of inline assembly to express the notion of a dummy instruction, and decided to deal with it in place. Shouldn't appearance of inline assembly in the code pessimize analysis? Even if the respective Asm statement has no input and output parameters, it could in principle do function calls or access globals.

Of course, even if this concern is valid, the pull request needs to be split to address it separately. At the moment, I just created a pull request for whatever I had on my branch.

[sim642]

I think it would be fine to remove dummyInstr and have dummyStmt as that.
It's yet another of CIL's ugly hacks but it should be fine and no worse than it already is. I think dummyStmt might only exist out of laziness in place of a None or sentinel value. It likely could be eliminated to clean things up, but that can be a separate change in the future.
It's not worth introducing DummyInstr and having to handle it everywhere if it shouldn't probably exist at all.

As to how to reach something mergeable, an option would be to also try to clean up #161 based on the unaddressed feedback there (although the history of #161 isn't too pretty), but it might not be worth it.

[jprotopopov-ut]

I have reverted the original definition of dummyStmt and removed DummyInstr. I plan to pull in the test suite from #161, and then will look at what are the remaining meaningful differences between changesets.

[jprotopopov-ut]

Rebased on top of current develop and integrated some changes from #161. At this point, I think, both pull requests have almost converged structurally, but there are still some differences in CFG handling for goto labels. I will leave those as-is and let you consider the pull request on its own merit, because my version of changes has been tested as part Linux module analysis project and seems to work satisfactorily for this purpose.