Add new IcfgBuilder

[Heizmann]

Commits for switching from RCFGBuilder to IcfgBuilder are missing in this branch. But Frank convinced me to already start a pull request.

[schuessf]

Thanks for your work! I did not have a detailed look yet, but here are already some more general comments.

[schuessf]

I just synced the CfgBuilder classes from RCFGBuilder and the new IcfgBuilder. To inspect the differences, you can take a look a the diff.

[schuessf]

In the RCFGBuilder firstStatement is always set to body.getBlock()[0], why is this different here?

[NiklasKult]

For the RCFGBuilder body.getBlock() could never be empty, because the BoogiePreprocessor would insert a return statement in that case. With the setting that disables the UnstructureCode class from the BoogiePreprocessor body.getBlock() can now be empty.

[schuessf]

But does this belong to the CfgBuilder? Wouldn't it be better to move it into its own Preprocessor that always runs independant of UnstructureCode?

[schuessf]

Or do we even need this statement here? Is it possible to create a location without a statement?

[schuessf]

I just looked into the open backtranslation issues, the created CFG for loops (especially when translated from C) looks slightly different.
Consider the following C program

while (x > 0) x--

This is roughly translated to the following Boogie program

while (true) {
  label: if (!(x > 0)) {
    break;
  }
  x := x - 1;
}

In the old CFG, we only had only two states and three edges (with SequenceOfStatements):

• a loop in the initial location with the body and the negated if-condition (x > 0)
• an edge from the initial location to the exit location with the if-condition (!(x > 0))
• an edge from the initial location to the exit location with the negated while-condition (false)
  

With the same settings, the new CFG has 5 locations and the following 6 edges:

• one with the while condition (true)
• an edge from the initial location to the exit location with the negated while-condition (false)
• another edge with true after the label
• an edge with the negated if-condition (x > 0)
• an edge to the exit location with the if-condition (!(x > 0))
• an edge with the body back to the initial location
  

This means that in the old CFG we had a stronger block encoding for SequenceOfStatements. With other settings the CFG should be more similar. I am not sure if this behaviour is desired.

[Heizmann]

Some info (not enough time to think about your post): The new IcfgBuilder alredy makes sure that labels get their own IcfgLocation.

[bahnwaerter]

The changes look good so far. The branch has already been correctly adapted to our Java 21 and Eclipse migration and can therefore be merged without any issues.

However, there are still a few small things that need to be improved. For example, in the comments and the license agreement in the headers of ICFG source code files, the word RCFGBuilder should be replaced consistently with ICFGBuilder.

[maul-esel]

Thanks @NiklasKult, @Heizmann and @schuessf for working on this!

I had a look at the changes and did not find any major issues. Due to the time constraints, I was not able to review in-depth, but since others have done so, and our latest evaluations have shown no major issues (only a slight increase in the number of locations) I have no objection to merging 👍

[maul-esel]

Nitpick: add an error message

[maul-esel]

Is it necessary to make this public?

[schuessf]

I think so, as this is also used by the IcfgBuilder plugin. Of course, it would be more optimal to move it to some library, but we can do this, if we remove RCFGBuilder in the future.

[maul-esel]

I also had a quick look at the RCFGBuilder/ICFGBuilder diff by @schuessf and did not find any issues there either.

[schuessf]

I will try to address these minor issues and merge this later.