boogie-org · Dargones · Mar 29, 2023 · Apr 5, 2023 · Apr 5, 2023 · Apr 5, 2023
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -6,6 +6,7 @@ on:
 
 env:
   SOLUTION: source/Corral.sln
+  BOOGIESOLUTION: boogie/Source/Boogie.sln
 
 jobs:
   job0:
@@ -20,6 +21,7 @@ jobs:
         uses: actions/checkout@v2
         with:
           fetch-depth: 0
+          submodules: 'true'
       - name: Build Corral, package Corral
         run: |
           # Find version from tag info
@@ -29,6 +31,8 @@ jobs:
           cd $GITHUB_WORKSPACE
           # Restore dotnet tools
           dotnet tool restore
+          # Build custom Boogie
+          dotnet build ${BOOGIESOLUTION}
           # Build Corral
           dotnet build -p:Version=$VERSION -c Release ${SOLUTION}
           # Create packages

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -5,6 +5,7 @@ on: [push, pull_request, workflow_dispatch]
 env:
   SOLUTION: source/Corral.sln
   AVSOLUTION: source/av.sln
+  BOOGIESOLUTION: boogie/Source/Boogie.sln
   Z3URL: https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip
 
 jobs:
@@ -23,6 +24,7 @@ jobs:
         uses: actions/checkout@v2
         with:
           fetch-depth: 0
+          submodules: 'true'
       - name: Install tools, build Corral, build Angelic Verifier
         run: |
           # Download a Z3 release
@@ -32,6 +34,8 @@ jobs:
           cd $GITHUB_WORKSPACE
           # Restore dotnet tools
           dotnet tool restore
+          # Build custom Boogie
+          dotnet build ${BOOGIESOLUTION}
           # Build Corral
           dotnet build -c ${{ matrix.configuration }} ${SOLUTION}
           # Build Angelic Verifier

diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,4 @@
+[submodule "boogie"]
+	path = boogie
+	url = https://github.com/boogie-org/boogie.git
+	branch = corral
diff --git a/boogie b/boogie
diff --git a/source/AliasAnalysis/AliasAnalysis.csproj b/source/AliasAnalysis/AliasAnalysis.csproj
@@ -9,4 +9,8 @@
     <ProjectReference Include="..\Util\CorralUtil.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/AngelicVerifier/AngelicVerifier.csproj b/source/AngelicVerifier/AngelicVerifier.csproj
@@ -16,4 +16,8 @@
     <ProjectReference Include="..\propinstutils\PropInstUtils.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/AvHarnessInstrumentation/AvHarnessInstrumentation.csproj b/source/AvHarnessInstrumentation/AvHarnessInstrumentation.csproj
@@ -14,4 +14,8 @@
     <ProjectReference Include="..\Corral\Corral.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/AvUtil/AvUtil.csproj b/source/AvUtil/AvUtil.csproj
@@ -5,4 +5,8 @@
     <AssemblyName>AvUtil</AssemblyName>
   </PropertyGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/CoreLib/AbstractHoudini.cs b/source/CoreLib/AbstractHoudini.cs
@@ -48,7 +48,8 @@ public AbstractHoudini(Program program)
             this.impl2Summary = new Dictionary<string, ISummaryElement>();
             this.name2Impl = BoogieUtil.nameImplMapping(program);
 
-            this.vcgen = new VCGen(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List<Checker>());
+            var checkerPool = new CheckerPool(CommandLineOptions.Clo);
+            this.vcgen = new VCGen(program, checkerPool);
             this.prover = ProverInterface.CreateProver(program, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit);
             this.reporter = new AbstractHoudiniErrorReporter();
 
@@ -312,13 +313,13 @@ private void attachEnsures(Implementation impl)
         private void GenVC(Implementation impl)
         {
             ModelViewInfo mvInfo;
-            Dictionary<int, Absy> label2absy;
+            ControlFlowIdMap<Absy> label2absy = new ControlFlowIdMap<Absy>();
 
             vcgen.ConvertCFG2DAG(impl);
             vcgen.PassifyImpl(impl, out mvInfo);
 
             var gen = prover.VCExprGen;
-            var vcexpr = vcgen.GenerateVC(impl, null, out label2absy, prover.Context);
+            var vcexpr = vcgen.GenerateVC(impl, null, label2absy, prover.Context);
 
             // Create a macro so that the VC can sit with the theorem prover
             Macro macro = new Macro(Token.NoToken, impl.Name + "Macro", new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false));

diff --git a/source/CoreLib/CoreLib.csproj b/source/CoreLib/CoreLib.csproj
@@ -10,4 +10,8 @@
     <ProjectReference Include="..\Util\CorralUtil.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/CoreLib/StratifiedInlining.cs b/source/CoreLib/StratifiedInlining.cs
@@ -255,7 +255,7 @@ public void RunInitialAnalyses(Program prog)
         }
 
         public StratifiedInlining(Program program, string logFilePath, bool appendLogFile, Action<Implementation> PassiveImplInstrumentation) :
-            base(program, logFilePath, appendLogFile, new List<Checker>(), PassiveImplInstrumentation)
+            base(program, logFilePath, appendLogFile, new CheckerPool(CommandLineOptions.Clo), PassiveImplInstrumentation)
         {
             stats = new Stats();
 
@@ -1304,7 +1304,7 @@ public List<Tuple<StratifiedVC, Block>> AssertMustReach(StratifiedVC svc, HashSe
             var ret = new List<Tuple<StratifiedVC, Block>>();
 
             // This is most likely redundant
-            prover.Assert(svc.MustReach(svc.info.impl.Blocks[0]), true);
+            prover.Assert(svc.MustReach(svc.info.impl.Blocks[0], svc.info.absyIds), true);
 
             if (!attachedVCInv.ContainsKey(svc))
                 return ret;
@@ -1318,12 +1318,12 @@ public List<Tuple<StratifiedVC, Block>> AssertMustReach(StratifiedVC svc, HashSe
                 var key = Tuple.Create(vc, callblock);
                 if (prevAsserted != null && !prevAsserted.Contains(key))
                 {
-                    prover.Assert(vc.MustReach(callblock), true);
+                    prover.Assert(vc.MustReach(callblock, svc.info.absyIds), true);
                     ret.Add(key);
                 }
                 iter = parent[iter];
             }
-            prover.Assert(mainVC.MustReach(mainVC.callSites.First(tup => tup.Value.Contains(iter)).Key), true);
+            prover.Assert(mainVC.MustReach(mainVC.callSites.First(tup => tup.Value.Contains(iter)).Key, svc.info.absyIds), true);
             return ret;
         }
 
@@ -1867,7 +1867,7 @@ private Outcome CheckVC(ProverInterface.ErrorHandler reporter)
             var stopwatch = Stopwatch.StartNew();
             prover.Check();
             stats.time += stopwatch.ElapsedTicks;
-            ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);
+            ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter, 1);
             return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
         }
 
@@ -4110,8 +4110,7 @@ public override int StartingProcId()
         private Absy Label2Absy(string procName, string label)
         {
             int id = int.Parse(label);
-            var l2a = si.implName2StratifiedInliningInfo[procName].label2absy;
-            return (Absy)l2a[id];
+            return si.implName2StratifiedInliningInfo[procName].absyIds.GetValue(id);
         }
 
         public override void OnProverError(string message)

diff --git a/source/Corral/Corral.csproj b/source/Corral/Corral.csproj
@@ -24,4 +24,8 @@
     <PackageReference Include="System.Resources.Extensions" Version="4.6.0" />
   </ItemGroup>
 
+  <ItemGroup>
+    <ProjectReference Include="../../boogie/Source/ExecutionEngine/ExecutionEngine.csproj" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/Directory.Build.props b/source/Directory.Build.props
@@ -16,7 +16,7 @@
 
   <!-- Boogie dependency -->
   <ItemGroup>
-    <PackageReference Include="Boogie.ExecutionEngine" Version="2.9.1" />
+    <ProjectReference Include="../../boogie/Source/ExecutionEngine/ExecutionEngine.csproj" />
   </ItemGroup>
 
 </Project>
diff --git a/source/ExplainError/ExplainError.csproj b/source/ExplainError/ExplainError.csproj
@@ -10,4 +10,8 @@
     <ProjectReference Include="..\Util\CorralUtil.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/ExplainError/program.cs b/source/ExplainError/program.cs
@@ -1305,7 +1305,7 @@ private static bool CheckSanity(Implementation impl)
         private static void CreateProver()
         {
             //create vcgen/proverInterface
-            vcgen = new VCGen(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, new List<Checker>());
+            vcgen = new VCGen(prog, new CheckerPool(CommandLineOptions.Clo));
             proverInterface = ProverInterface.CreateProver(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, CommandLineOptions.Clo.TimeLimit);
             translator = proverInterface.Context.BoogieExprTranslator;
             exprGen = proverInterface.Context.ExprGen;
@@ -1352,8 +1352,8 @@ public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementati
                 ref List<Counterexample> cexList)
             {
                 //this creates a z3 process per vcgen
-                var checkers = new List<Checker>();
-                VC.VCGen vcgen = new VC.VCGen(prog, CommandLineOptions.Clo.ProverLogFilePath, CommandLineOptions.Clo.ProverLogFileAppend, checkers);
+                var checkers = new CheckerPool(CommandLineOptions.Clo);
+                VC.VCGen vcgen = new VC.VCGen(prog, checkers);
                 //make deep copy of the blocks
                 var tmpBlocks = new List<Block>();
                 foreach (Block b in i.Blocks)
@@ -1372,11 +1372,7 @@ public static VC.ConditionGeneration.Outcome MyVerifyImplementation(Implementati
                 var outcome = vcgen.VerifyImplementation((Implementation)i, out cexList);
                 var reset = new ResetVerificationState();
                 reset.Visit(i);
-                foreach (Checker checker in checkers)
-                {
-                    //Contract.Assert(checker != null);
-                    checker.Close();
-                }
+                checkers.Dispose();
                 vcgen.Close();
                 i.Blocks = tmpBlocks;
                 i.LocVars = tmpLocVars;

diff --git a/source/FastAvn/FastAvn.csproj b/source/FastAvn/FastAvn.csproj
@@ -16,4 +16,8 @@
     <ProjectReference Include="..\Corral\Corral.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/ProgTransformation/ProgTransformation.csproj b/source/ProgTransformation/ProgTransformation.csproj
@@ -9,4 +9,8 @@
     <ProjectReference Include="..\Util\CorralUtil.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/PropInst/PropInst.csproj b/source/PropInst/PropInst.csproj
@@ -10,4 +10,8 @@
     <ProjectReference Include="..\propinstutils\PropInstUtils.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/Util/CorralUtil.csproj b/source/Util/CorralUtil.csproj
@@ -5,4 +5,8 @@
     <AssemblyName>CorralUtil</AssemblyName>
   </PropertyGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/source/Util/Duplicator.cs b/source/Util/Duplicator.cs
@@ -453,8 +453,7 @@ public override Variable VisitVariable(Variable node)
         public override Function VisitFunction(Function node)
         {
             node = (Function)node.Clone();
-            node.Attributes = CopyAttr(node.Attributes);
-            node.doingExpansion = false;
+            node.Attributes = CopyAttr(node.Attributes);        
             return base.VisitFunction(node);
         }
 

diff --git a/source/propinstutils/PropInstUtils.csproj b/source/propinstutils/PropInstUtils.csproj
@@ -9,4 +9,8 @@
     <ProjectReference Include="..\Util\CorralUtil.csproj" />
   </ItemGroup>
 
+  <ItemGroup>
+    <PackageReference Update="Boogie.ExecutionEngine" Version="2.9.5" />
+  </ItemGroup>
+
 </Project>
diff --git a/test/fwdbck/Files b/test/fwdbck/Files
@@ -12,7 +12,6 @@
 12/simp12.bpl b
 13/simp13.bpl b
 14/simp14.bpl b
-15/simp15.bpl c
 16/simp16.bpl b
 17/simp17.bpl c
 18/simp18.bpl b

diff --git a/test/regression/Files b/test/regression/Files
@@ -35,7 +35,6 @@
 024\f.bpl b
 loop\seq.bpl b
 loop\conc.bpl b
-loop\assert.bpl b
 smack\a.bpl b
 stackdepth\f1.bpl c
 cex\twoasserts.bpl b