Translating Branch Conditions w/ Wrong State

[jennalwise]

This program: https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/bugs/condition_version.c0 fails with error: // ERROR: java.lang.RuntimeException: Error translating! Exiting safely. It fails on line 23 when //@assert box->value > 0; has a run-time check of box->value > 0 created for it. This happens in the catch all case in consume after evalAndAssert is called on box->value > 0. When the run-time check is created, the branch conditions up until that point are translated so they can be added to the run-time check. The problem is that the branch condition !(r’ == 0), where r’ is the symbolic value for r, is being translated with the state at line 23 where r->-1 in the symbolic store instead of r->r’. Instead, translation should happen with the symbolic state where the branch condition was created, in this example that is the symbolic state after line 20. A better solution that Hemant is working on implementing right now is to stop relying on translation for branch conditions and to instead carry around the version of the condition that is not evaluated to a symbolic value. This solution has the same implementation effort as tracking the correct symbolic state for translation.

[jennalwise]

This same issue arises in https://github.com/gradual-verification/gvc0/blob/master/src/test/resources/bugs/translate.c0 for the error Could not translate term into Viper expression! Exiting safely. When the postcondition of append is consumed at the end of the method, a run-time check for list(n) is produced and in doing so the branch condition (! (== n@2@01.Node$next@9@01 Null)) is translated. However, it is translated with the symbolic state at the consume which does not contain a heap chunk for n@2@01.Node$next@9@01. Therefore, the translator is unable to translate n@2@01.Node$next@9@01 into anything and returns None, resulting in the aforementioned error. Instead, if the translation occurs with the symbolic state after evaluating the if condition n->next != NULL and before executing the append method, then translation will succeed successfully using the heap chunk in the OH. Of course, not doing translation is also a solution here.

[hgouni]

This has been fixed by 0deb0b9a, but should be kept open for now, while we bring back translation for branches.

[jennalwise]

Tested & fix looks good!