Merge pull request boogie-org#7 from atomb/allinone-lib

Add support for using SymDiff as a library

Sources/SymDiff/source/BoogieUtil.cs

@@ -357,11 +357,23 @@ public static bool IsUFName(string name)
       return name.StartsWith("_uf_");
     }
 
-    public static bool InjectUninterpreted(Procedure left, Procedure right, Config cfg, CallGraph cg, List<Declaration> ufDeclarations,bool asserts=false)
+    public static bool InjectUninterpreted(Procedure left,
+                                           Procedure right,
+                                           Config cfg,
+                                           CallGraph cg,
+                                           List<Declaration> ufDeclarations,
+                                           bool hasImplementation,
+                                           bool asserts=false)
     {
       if (left == null || right == null | ufDeclarations == null)
         return true;
 
+      if (!hasImplementation && left.Modifies.Count == 0)
+      {
+        Log.Out(Log.Urgent,
+          $"Compared procedures {left}, {right} do not have bodies and do not have any modifies clauses.");
+      }
+
       int i, j;
 
       var leftNode = cg.NodeOfName(left.Name);

Sources/SymDiff/source/BoogieVerify.cs

@@ -47,6 +47,7 @@ public enum VerificationResult { Error, Verified, Inconclusive, TimeOut, OutOfMe
     public class VerificationTask : Triple<Implementation, Implementation, Implementation>, IEmittable
     {
         public VerificationResult Result;
+        public SDiffCounterexamples Counterexamples;
         public List<Variable> DesiredOutputVars;
         public VerificationTask(Implementation eq, Implementation left, Implementation right)
             : base(eq, left, right)
@@ -198,12 +199,18 @@ public static VerificationResult VerifyImplementation(VC.ConditionGeneration vcg
                 if (!imperativeBlocks.ContainsKey(b.Label))
                     imperativeBlocks.Add(b.Label, duper.VisitBlock(b));
 
+            var inlineOptPrev = BoogieUtils.BoogieOptions.ProcedureInlining;
+            if (Options.UnsoundRecursion)
+            {
+                BoogieUtils.BoogieOptions.ProcedureInlining = CoreOptions.Inlining.Spec;
+            }
             var engine = new ExecutionEngine(BoogieUtils.BoogieOptions, new VerificationResultCache(),
                 CustomStackSizePoolTaskScheduler.Create(16 * 1024 * 1024, 1));
             engine.EliminateDeadVariables(prog);
             engine.CoalesceBlocks(prog);
             engine.Inline(prog);
             engine.Dispose();
+            BoogieUtils.BoogieOptions.ProcedureInlining = inlineOptPrev;
 
             var assumeFlags = new QKeyValue(Token.NoToken, "captureState", new List<object>{ "final_state" }, null);
             AssumeCmd ac = new AssumeCmd(Token.NoToken, new LiteralExpr(Token.NoToken, true), assumeFlags);
@@ -904,6 +911,7 @@ public static int RunVerificationTask(VerificationTask vt, Program prog, out boo
                 newEq = (Implementation)newDict.Get(vt.Eq.Name + "$IMPL");
 
                 vt.Result = VerifyImplementation(vcgen, newEq, newProg, out SErrors);
+                vt.Counterexamples = SErrors;
 
                 switch (vt.Result)
                 {

Sources/SymDiff/source/Driver.cs

@@ -432,10 +432,6 @@ public static int GuessConfig(string[] args)
             var proc = d as Procedure;
             if (proc != null)
             {
-
-                if (Util.IsInlinedProc(proc))
-                    continue;
-
                 var pmap = new ParamMap();
                 foreach (Variable v in proc.InParams)
                     pmap.Add(new HDuple<string>(v.Name, v.Name));

Sources/SymDiff/source/MutualSummary.cs

@@ -125,7 +125,7 @@ public static void PerformHoudiniInferece()
 
 
             var mpsPi = "mergedProgSingle_preInferred.bpl";
-            BoogieUtils.PrintProgram(program, mpsPi);
+            Util.DumpBplAST(program, mpsPi);
             program = BoogieUtils.ParseProgram(mpsPi);
             BoogieUtils.ResolveAndTypeCheckThrow(program, mpsPi, BoogieUtils.BoogieOptions); 
 
@@ -152,7 +152,7 @@ public static void PerformHoudiniInferece()
             var trueConstants = extractVariableAssigned(true, outcome);
             var falseConstants = extractVariableAssigned(false, outcome);
             persistHoudiniInferredFacts(trueConstants, falseConstants, program, houdini);
-            BoogieUtils.PrintProgram(program, "mergedProgSingle_inferred.bpl");
+            Util.DumpBplAST(program, "mergedProgSingle_inferred.bpl");
             Console.WriteLine("Houdini finished and inferred {0}/{1} contracts", trueConstants.Count, outcome.assignment.Count());
             Console.WriteLine("Houdini finished with {0} verified, {1} errors, {2} inconclusives, {3} timeouts",
                     outcome.Verified, outcome.ErrorCount, outcome.Inconclusives, outcome.TimeOuts);

Sources/SymDiff/source/Options.cs

@@ -38,6 +38,11 @@ public enum DAC_ENCODING_OPT { DAC_LINEAR, DAC_NORMAL };
         public static bool EnumerateAllPaths = false; //setting to true means we check assert(F) in EQ
         public static bool RVTOption = false; //RVT option
         public static string LoopStringIdentifier = "_loop_"; // if a function name contains this string we assume it was a loop converted into a recursive function.
+
+        // global variables with these strings in their name will be assumed to be modified in procedures with no
+        // implementations and no modifies clauses
+        public static List<string> HeapStringIdentifiers = ["heap", "Heap"];
+
         //mode where a procedure is inlined when not equal (non-recursive only) [For evaluation of diff inlining]
         public const bool InlineWhenFail = false; //make sure DifferentialInline is turned off
         #endregion

Sources/SymDiff/source/RVTCheck.cs

@@ -138,7 +138,7 @@ public static void RVTMain(SDiff.CallGraph cg1, SDiff.CallGraph cg2, SDiff.CallG
                 //Add the same uninterpreted function by default
                 Procedure leftP = cg.NodeOfName(fnPair.Key).Proc;
                 Procedure rightP = cg.NodeOfName(fnPair.Value).Proc;
-                InjectUIFsOnBothProcs(leftP, rightP);               
+                InjectUIFsOnBothProcs(leftP, rightP, cg.NodeOfName(fnPair.Key).Impl != null);               
                 if (RVTCreateEQProcs(left, ref synEq, ref empty1, ref empty2))
                 {
                     //add the mapping if the eq generation succeeded
@@ -179,13 +179,13 @@ private static string RemoveVersionPrefix(string fnName)
 
         }
 
-        private static void InjectUIFsOnBothProcs(Procedure leftP, Procedure rightP)
+        private static void InjectUIFsOnBothProcs(Procedure leftP, Procedure rightP, bool hasImplementation)
         {
             ////create uifs, grabs the readset from callgraph
             ////same uif for both versions   
             ////injects them as postcondition
             var newDecls = new List<Declaration>();
-            if (SDiff.Boogie.Process.InjectUninterpreted(leftP, rightP, cfg, cg, newDecls))
+            if (SDiff.Boogie.Process.InjectUninterpreted(leftP, rightP, cfg, cg, newDecls, hasImplementation))
                 Log.Out(Log.Error, "Failed to add postconditions to " + leftP.Name + " and " + rightP.Name);
             mergedProgram.AddTopLevelDeclarations(newDecls);
         }
@@ -265,7 +265,7 @@ private static bool RVTCreateEQProcs(int f, ref List<int> synEq, ref List<int> e
             string eqpName = Transform.mkEqProcName(n1.Name, n2.Name);
 
             Duple<Procedure, Implementation> eqp;
-            eqp = Transform.EqualityReduction(n1.Impl, n2.Impl, cfg.FindProcedure(n1.Name, n2.Name), ignores, out outputVars);
+            eqp = Transform.EqualityReduction(n1.Impl, n2.Impl, cfg.FindProcedure(n1.Name, n2.Name), ignores, out outputVars, out _);
 
             // if any visible output
             //VerificationTask vt;

Sources/SymDiff/source/Transform.cs

@@ -61,7 +61,12 @@ public static void MergeVariableSequencesByMap(List<Variable> v1, List<Variable>
           inter.Add(v);
     }
 
-    public static Duple<Procedure, Implementation> EqualityReduction(Implementation i1, Implementation i2, ParamMap argMap, HashSet<Variable> ignoreSet, out List<Variable> outputVarsForVFTask)
+    public static Duple<Procedure, Implementation> EqualityReduction(Implementation i1,
+                                                                     Implementation i2,
+                                                                     ParamMap argMap,
+                                                                     HashSet<Variable> ignoreSet,
+                                                                     out List<Variable> outputVarsForVFTask,
+                                                                     out EqualityProcedureParameterInfo eqParamInfo)
     {
       //map ins1
       //map outs1
@@ -130,14 +135,19 @@ public static Duple<Procedure, Implementation> EqualityReduction(Implementation
       SaveBlock savedInitialGlobals = new SaveBlock(globals.Count);
       SaveBlock savedc1Globals = new SaveBlock(globals.Count);
       SaveBlock savedOutputs = new SaveBlock(interOuts.Count);
+      SaveBlock savedIns1 = new SaveBlock(ins1.Count);
+      SaveBlock savedIns2 = new SaveBlock(ins2.Count);
 
       var globalsArr = B.U.VariablesOfVariableSeq(globals);
 
       Cmd[]
         prec1Copy = savedInitialGlobals.EmitSave(globalsArr),
         postc1Copy = savedc1Globals.EmitSave(globalsArr),
         postc1Restore = savedInitialGlobals.EmitRestore(globalsArr),
-        prec2Copy = savedOutputs.EmitSave(B.U.VariablesOfVariableSeq(interOuts));
+        prec2Copy = savedOutputs.EmitSave(B.U.VariablesOfVariableSeq(interOuts)),
+        ins1Copy = savedIns1.EmitSave(ins1.ToArray()),
+        ins2Copy = savedIns2.EmitSave(ins2.ToArray());
+
 
 
       /***** Emit function calls *****/
@@ -160,6 +170,7 @@ public static Duple<Procedure, Implementation> EqualityReduction(Implementation
       {
         Log.Out(Log.Verifier, "No outputs: skipping (" + d1n + ", " + d2n +")");
         outputVarsForVFTask = null;
+        eqParamInfo = null;
         return null;
       }
 
@@ -189,9 +200,18 @@ public static Duple<Procedure, Implementation> EqualityReduction(Implementation
         comparisonOutIds = B.U.IdentifierExprSeqOfVariableSeq(outs2),
         comparisonGlobals = B.U.IdentifierExprSeqOfVariableSeq(globals);
 
+      eqParamInfo = new EqualityProcedureParameterInfo(
+        savedIns1.Idents.Select(v => v.Name).ToList(),
+        savedOutputs.Idents.Select(v => v.Name).ToList(),
+        savedIns2.Idents.Select(v => v.Name).ToList(),
+        outs2.Select(v => v.Name).ToList(),
+        globals.Select(v => v.Name).ToList(),
+        savedInitialGlobals.Idents.Select(v => v.Name).ToList(),
+        savedc1Globals.Idents.Select(v => v.Name).ToList());
+
       for (int i = 0; i < savedOutputs.Count; i++)
-      {
-          outputEqualityExprs[i] = Tuple.Create(EmitEq(comparisonPrec2Vars[i], comparisonOutIds[i], ignoreSet), comparisonOutIds[i].Decl);
+      { 
+        outputEqualityExprs[i] = Tuple.Create(EmitEq(comparisonPrec2Vars[i], comparisonOutIds[i], ignoreSet), comparisonOutIds[i].Decl);
         outputVars.Add(new Duple<string, Variable>("Output_of_" + d1.Name + "_" + outs1[i].Name, savedOutputs.Decls[i]));
         outputVars.Add(new Duple<string, Variable>("Output_of_" + d2.Name + "_" + outs2[i].Name, outs2[i]));
       }
@@ -221,19 +241,15 @@ public static Duple<Procedure, Implementation> EqualityReduction(Implementation
 
       /***** Compile procedure body ****/
 
-      List<Cmd> body = new List<Cmd>();
-      foreach (Cmd c in prec1Copy)
-        body.Add(c);
+      var body = Enumerable.ToList(ins1Copy);
+      body.AddRange(ins2Copy);
+      body.AddRange(prec1Copy);
       body.Add(c1);
-      foreach (Cmd c in postc1Copy)
-        body.Add(c);
-      foreach (Cmd c in postc1Restore)
-        body.Add(c);
-      foreach (Cmd c in prec2Copy)
-        body.Add(c);
+      body.AddRange(postc1Copy);
+      body.AddRange(postc1Restore);
+      body.AddRange(prec2Copy);
       body.Add(c2);
-      foreach (Cmd c in saveOutputsIntoGlobals)
-        body.Add(c);
+      body.AddRange(saveOutputsIntoGlobals);
       body.Add(hcmd);
       body.Add(assgnCmd);
 
@@ -284,31 +300,28 @@ public static Duple<Procedure, Implementation> EqualityReduction(Implementation
       //var procName = "EQ_" + d1.Name + "__xx__" + d2.Name;
       var procName = mkEqProcName(d1.Name, d2.Name);
 
-      Procedure eqProc =
+      var eqProc =
         new Procedure(Token.NoToken, procName, B.C.empTypeVariableSeq, unionIns,
           new List<Variable>(outputEqualityState.Decls), isPure:false,
           B.C.empRequiresSeq, eqModifies, new List<Ensures>(outputPostConditions));
 
-      BigBlock bl =
+      var bl =
         new BigBlock(Token.NoToken, "AA_INSTR_EQ_BODY", body, null, B.C.dmyTransferCmd);
-      List<BigBlock> bll = new List<BigBlock>();
-      bll.Add(bl);
-
-      List<Variable> locals = new List<Variable>();
-      foreach (Variable v in savedOutputs.Decls)
-        locals.Add(v);
-      foreach (Variable v in savedc1Globals.Decls)
-        locals.Add(v);
-      foreach (Variable v in savedInitialGlobals.Decls)
-        locals.Add(v);
+      var bll = new List<BigBlock> { bl };
+
+      var locals = Enumerable.ToList(savedOutputs.Decls);
+      locals.AddRange(savedIns1.Decls);
+      locals.AddRange(savedIns2.Decls);
+      locals.AddRange(savedc1Globals.Decls);
+      locals.AddRange(savedInitialGlobals.Decls);
       locals.AddRange(unionOuts);
 
-      Implementation eqImp =
+      var eqImp =
         new Implementation(Token.NoToken, procName, B.C.empTypeVariableSeq, unionIns,
           new List<Variable>(outputEqualityState.Decls),
           locals, new StmtList(bll, Token.NoToken));
 
-      List<Declaration> l = new List<Declaration>();
+      var l = new List<Declaration>();
 
       return new Duple<Procedure, Implementation>(eqProc, eqImp);
     }