Sync with Boogie 2.15.7

[Dargones]

This is a draft of the changes necessary to sync Corral with the most recent version of Boogie. I am currently trying to make it work with this custom Boogie version forked from 2.15.7 that still has the static CommandLineOptions.Clo object.

I am publishing this draft despite it not passing any tests (it does compile though) because I would be very grateful for any advice on how to do this correctly and on whether or not there are things one might need to change in Boogie itself to make this work (aside from potentially the changes linked above). I will put the runtime error I get in the thread and here is a select list of modifications I had to make to Corral to compile with Boogie 2.15.7:

• Introduce ImplementationRun objects in several places where an Implementation was used before. I pass TextWriter.Null to the ImplementationRun constructor, not sure if this is correct.

• Replace ProverInterface.BeginCheck + ProverInterface.CheckOutcome sequence of invocations with ProverInterface.Check. This seems to be consistent with how these two methods are replaced in HoudiniSession in this commit.

• Unbox the result of calls that are now marked with async and return Task objects. Should I await on these instead of calling them directly? Whenever the new version of Boogie requires a CancellationToken, I pass CancellationToken.None

• Replace prover.CheckOutcomeCore(reporter) with (prover as SMTLibInteractiveTheoremProver).CheckSat(CancellationToken.None, 1).Result. This change I am least certain about but this commit along with this one seem to indicate that this is the right course of action. I had to similarly introduce a cast to SMTLibInteractiveTheoremProver to access the CalculatePath method.

• Pass various options as arguments instead of using a static CommandLineOptions.Clo object to store them. I re-introduced the static object for now in my custom boogie submodule but am planning to change this back once I get this PR to pass the tests.

• [This is a change to Boogie] Turn the ControlFlowIdMap object used in StratifiedInliningInfo back into an instance field so that it could be accessed externally. This would effectively revert part of this commit but I am not certain if there is any other way of accessing this information that Corral relies on.

I would be very grateful for any advice regarding these changes or the possibility of syncing Corral and Boogie in general.

[Dargones]

Below is the error I am getting on the first regression test. It seems that Corral fails to extract the error trace at some point and I am wondering if the issue might be related to Boogie rather than Corral. I know that /enhancedErrorMessages does not always work now but am not sure if this is in any way related.

Corral program verifier version 1.0.0.0
Warning: Using default recursion bound of 1
Verifying program while tracking: {}
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
   at cba.StormInstrumentationPass.mapBackTrace(ErrorTrace trace) in /Users/fedchina/Desktop/corral/source/CoreLib/CBAPasses.cs:line 287
   at cba.CBADriver.VerifyProgram(PersistentCBAProgram& prog, VarSet trackedVars, Boolean returnTrace, PersistentCBAProgram& pout, InsertionTrans& tinfo, ErrorTrace& cex) in /Users/fedchina/Desktop/corral/source/Corral/CBADriver.cs:line 116
   at cba.CBADriver.checkProgram(PersistentCBAProgram& prog, VarSet trackedVars, Boolean returnTrace, PersistentCBAProgram& pout, InsertionTrans& tinfo, ErrorTrace& cex) in /Users/fedchina/Desktop/corral/source/Corral/CBADriver.cs:line 146
   at cba.Driver.checkAndRefine(PersistentCBAProgram prog, RefinementState refinementState, Action`2 printTrace, ErrorTrace& cexTrace) in /Users/fedchina/Desktop/corral/source/Corral/Driver.cs:line 1566
   at cba.Driver.run(String[] args) in /Users/fedchina/Desktop/corral/source/Corral/Driver.cs:line 387
   at cba.Driver.Main(String[] args) in /Users/fedchina/Desktop/corral/source/Corral/Driver.cs:line 44

[akashlal]

@Dargones Thanks for taking this up. I'd like to help, but it'll take me some time to wrap my head around the changes to Boogie. I'll write back once I understand more.

[akashlal]

Update: I went over the code changes and they look reasonable. It seems that the way a counterexample path is generated in Boogie has changed slightly, which might be causing the crash in corral. I will try to run corral next and debug the issue.

[akashlal]

@Dargones I've pushed some fixes and corral seems to be running on a few examples now. I have not tested corral thoroughly yet. The next step would be to run all the regressions.

My fixes do need one change in boogie, which I was unable to push for some reason. You need to make the following field of class SMTLibProcessTheoremProver be public (at least until we figure out how best to pass it as an argument):

protected volatile ErrorHandler currentErrorHandler;

[Dargones]

Thank you so much for your help, @akashlal, and apologies for belated reply. Have updated my Boogie fork as requested. Will run this on all regressions and report back.