added support for recordProcCallSites to new SI

1 files changed, 65 insertions, 32 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fbb8f878..cb507cfc 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -21,6 +21,7 @@ namespace VC {
     public int id;

     public List<VCExprVar> interfaceExprVars;

     public Dictionary<Block, List<StratifiedCallSite>> callSites;

+    public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;

     public VCExpr vcexpr;

     public Dictionary<Block, VCExprVar> reachVars;

 

@@ -81,6 +82,14 @@ namespace VC {
           callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

         }

       }

+

+      recordProcCallSites = new Dictionary<Block, List<StratifiedCallSite>>();

+      foreach (Block b in info.recordProcCallSites.Keys) {

+        recordProcCallSites[b] = new List<StratifiedCallSite>();

+        foreach (CallSite cs in info.recordProcCallSites[b]) {

+          recordProcCallSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

+        }

+      }

     }

 

     public List<StratifiedCallSite> CallSites {

@@ -147,6 +156,7 @@ namespace VC {
     public Hashtable/*<int, Absy!>*/ label2absy;

     public ModelViewInfo mvInfo;

     public Dictionary<Block, List<CallSite>> callSites;

+    public Dictionary<Block, List<CallSite>> recordProcCallSites;

     public bool initialized { get; private set; }

 

     public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {

@@ -256,6 +266,7 @@ namespace VC {
       }

 

       callSites = vcgen.CollectCallSites(impl);

+      recordProcCallSites = vcgen.CollectRecordProcedureCallSites(impl);

       initialized = true;

     }

   }

@@ -300,6 +311,7 @@ namespace VC {
   }

 

   public class StratifiedVCGenBase : VCGen {

+    public readonly static string recordProcName = "boogie_si_record";

     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

 

@@ -312,6 +324,37 @@ namespace VC {
         if (impl == null) continue;

         implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

       }

+      GenerateRecordFunctions();

+    }

+

+    private void GenerateRecordFunctions() {

+      foreach (var decl in program.TopLevelDeclarations) {

+        var proc = decl as Procedure;

+        if (proc == null) continue;

+        if (!proc.Name.StartsWith(recordProcName)) continue;

+        Contract.Assert(proc.InParams.Length == 1);

+

+        // Make a new function

+        TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);

+        Contract.Assert(ti != null);

+        Formal returnVar = new Formal(Token.NoToken, ti, false);

+        Contract.Assert(returnVar != null);

+

+        // Get record type

+        var argtype = proc.InParams[0].TypedIdent.Type;

+

+        var ins = new VariableSeq();

+        ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

+

+        var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

+        prover.Context.DeclareFunction(recordFunc, "");

+

+        var exprs = new ExprSeq();

+        exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

+

+        Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);

+        proc.Ensures.Add(new Ensures(true, freePostExpr));

+      }

     }

 

     public override void Close() {

@@ -341,6 +384,28 @@ namespace VC {
       return callSites;

     }

 

+    public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {

+      var callSites = new Dictionary<Block, List<CallSite>>();

+      foreach (Block block in implementation.Blocks) {

+        for (int i = 0; i < block.Cmds.Length; i++) {

+          AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;

+          if (assumeCmd == null) continue;

+          NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

+          if (naryExpr == null) continue;

+          if (!naryExpr.Fun.FunctionName.StartsWith(recordProcName)) continue;

+          List<VCExpr> interfaceExprs = new List<VCExpr>();

+          foreach (Expr e in naryExpr.Args) {

+            interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));

+          }

+          CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, block, i);

+          if (!callSites.ContainsKey(block))

+            callSites[block] = new List<CallSite>();

+          callSites[block].Add(cs);

+        }

+      }

+      return callSites;

+    }

+

     private int newVarCountForStratifiedInlining = 0;

     public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

       string newName = "StratifiedInlining@" + newVarCountForStratifiedInlining.ToString();

@@ -368,7 +433,6 @@ namespace VC {
     public bool PersistCallTree;

     public static Dictionary<string, int> callTree = null;

     public int numInlined = 0;

-    public readonly static string recordProcName = "boogie_si_record";

     private bool useSummary;

     private SummaryComputation summaryComputation;

     private HashSet<string> procsThatReachedRecBound;

@@ -394,7 +458,6 @@ namespace VC {
 

     public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

       : base(program, logFilePath, appendLogFile) {

-      this.GenerateRecordFunctions();

       PersistCallTree = false;

       useSummary = false;

       procsThatReachedRecBound = new HashSet<string>();

@@ -417,36 +480,6 @@ namespace VC {
       else return extraRecBound[procName];

     }

 

-    public void GenerateRecordFunctions() {

-      foreach (var decl in program.TopLevelDeclarations) {

-        var proc = decl as Procedure;

-        if (proc == null) continue;

-        if (!proc.Name.StartsWith(recordProcName)) continue;

-        Contract.Assert(proc.InParams.Length == 1);

-

-        // Make a new function

-        TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);

-        Contract.Assert(ti != null);

-        Formal returnVar = new Formal(Token.NoToken, ti, false);

-        Contract.Assert(returnVar != null);

-

-        // Get record type

-        var argtype = proc.InParams[0].TypedIdent.Type;

-

-        var ins = new VariableSeq();

-        ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

-

-        var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

-        prover.Context.DeclareFunction(recordFunc, "");

-

-        var exprs = new ExprSeq();

-        exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

-

-        Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);

-        proc.Ensures.Add(new Ensures(true, freePostExpr));

-      }

-    }

-

     public class SummaryComputation {

       // The verification state

       VerificationState vState;