deleted lazyinlining option 2 and 3

fixed proc copy bounding

1 files changed, 33 insertions, 163 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 576ce080..51bdb033 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -27,7 +27,6 @@ namespace VC {
     [NotDelayed]

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

       : base(program)

-      // throws ProverException

     {

       Contract.Requires(program != null);

       this.appendLogFile = appendLogFile;

@@ -36,10 +35,6 @@ namespace VC {
 

       if (CommandLineOptions.Clo.LazyInlining > 0) {

         this.GenerateVCsForLazyInlining(program);

-        if (CommandLineOptions.Clo.LazyInlining == 3)

-        {

-            CreateCopiesForLazyInlining(CommandLineOptions.Clo.ProcedureCopyBound, program);

-        }

       }

     }

 

@@ -85,9 +80,9 @@ namespace VC {
       public Function function;

       public Variable controlFlowVariable;

       public List<Variable> interfaceVars;

+      public List<List<Variable>> interfaceVarCopies;

       public Expr assertExpr;

       public VCExpr vcexpr;

-      public VCExpr inside_vc; // (without the quantifiers)

       public List<VCExprVar> privateVars;

       public Dictionary<Incarnation, Absy> incarnationOriginMap;

       public Hashtable /*Variable->Expr*/ exitIncarnationMap;

@@ -163,6 +158,16 @@ namespace VC {
         Contract.Assert(returnVar != null);

         this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar);

         ctxt.DeclareFunction(this.function, "");

+

+        interfaceVarCopies = new List<List<Variable>>();

+        int temp = 0;

+        for (int i = 0; i < CommandLineOptions.Clo.ProcedureCopyBound; i++) {

+          interfaceVarCopies.Add(new List<Variable>());

+          foreach (Variable v in interfaceVars) {

+            interfaceVarCopies[i].Add(

+              new Constant(Token.NoToken, new TypedIdent(Token.NoToken, v.Name + temp++, v.TypedIdent.Type)));

+          }

+        }

       }

     }

     [ContractInvariantMethod]

@@ -217,6 +222,25 @@ namespace VC {
           }

           Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);

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

+

+          if (CommandLineOptions.Clo.ProcedureCopyBound > 0) {

+            Expr ret = new LiteralExpr(Token.NoToken, false);

+            for (int k = 0; k < CommandLineOptions.Clo.ProcedureCopyBound; k++) {

+              var iv = info.interfaceVarCopies[k];

+              Contract.Assert(info.function.InParams.Length == iv.Count);

+

+              Expr conj = new LiteralExpr(Token.NoToken, true);

+              for (int i = 0; i < iv.Count; i++) {

+                Expr eqExpr = new NAryExpr(

+                  Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Eq), new ExprSeq(exprs[i], Expr.Ident(iv[i])));

+                conj =

+                  new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.And), new ExprSeq(conj, eqExpr));

+              }

+              ret =

+                new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Or), new ExprSeq(ret, conj));

+            }

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

+          }

         }

       }

 

@@ -226,145 +250,6 @@ namespace VC {
       }

     }

 

-    // proc name -> k -> interface variables

-    public static Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

-    // proc name -> k -> VCExpr

-    Dictionary<string, List<VCExpr>> procVcCopies;

-

-    private void CreateCopiesForLazyInlining(int K, Program program)

-    {

-        interfaceVarCopies = new Dictionary<string, List<List<VCExprVar>>>();

-        procVcCopies = new Dictionary<string, List<VCExpr>>();

-

-        // Duplicate VCs of each procedure K times and remove quantifiers

-        Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);

-        foreach (LazyInliningInfo info in implName2LazyInliningInfo.Values)

-        {

-            Contract.Assert(info != null);

-            CreateCopyForLazyInlining(K, program, info, checker);

-        }

-

-        // Change the procedure calls in each VC

-        // Push all to the theorem prover

-        var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies);

-        foreach (var kvp in procVcCopies)

-        {

-            for (int i = 0; i < kvp.Value.Count; i++)

-            {

-                kvp.Value[i] = bm.Mutate(kvp.Value[i], true);

-                checker.TheoremProver.PushVCExpression(kvp.Value[i]);

-            }

-        }

-    }

-

-    public class BoundingVCMutator : MutatingVCExprVisitor<bool>

-    {

-        // proc name -> k -> interface variables

-        Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

-

-        public BoundingVCMutator(VCExpressionGenerator gen, Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies)

-            : base(gen)

-        {

-            Contract.Requires(gen != null);

-            this.interfaceVarCopies = interfaceVarCopies;

-        }

-

-        protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,

-                                                      List<VCExpr/*!*/>/*!*/ newSubExprs,

-            // has any of the subexpressions changed?

-                                                      bool changed,

-                                                      bool arg)

-        {

-            //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);

-            Contract.Ensures(Contract.Result<VCExpr>() != null);

-            

-            VCExpr node;

-            if (changed)

-                node = Gen.Function(originalNode.Op,

-                                   newSubExprs, originalNode.TypeArguments);

-            else

-                node = originalNode;

-

-            var expr = node as VCExprNAry;

-            if (expr == null) return node;

-            var op = expr.Op as VCExprBoogieFunctionOp;

-            if (op == null) return node;

-            if (!interfaceVarCopies.ContainsKey(op.Func.Name)) return node;

-

-            // substitute

-            var K = interfaceVarCopies[op.Func.Name].Count;

-            

-

-            VCExpr ret = VCExpressionGenerator.False;

-            for (int k = 0; k < K; k++)

-            {

-                var iv = interfaceVarCopies[op.Func.Name][k];

-                Contract.Assert(op.Arity == iv.Count);

-

-                VCExpr conj = VCExpressionGenerator.True;

-                for (int i = 0; i < iv.Count; i++)

-                {

-                    var c = Gen.Eq(expr[i], iv[i]);

-                    conj = Gen.And(conj, c);

-                }

-                ret = Gen.Or(conj, ret);

-            }

-

-            return ret;

-        }

-

-    } // end BoundingVCMutator

-

-    private static int newVarCnt = 0;

-

-    private void CreateCopyForLazyInlining(int K, Program program, LazyInliningInfo info, Checker checker) 

-    {

-        var translator = checker.TheoremProver.Context.BoogieExprTranslator;

-        interfaceVarCopies.Add(info.impl.Name, new List<List<VCExprVar>>());

-        procVcCopies.Add(info.impl.Name, new List<VCExpr>());

-

-        for (int k = 0; k < K; k++)

-        {

-            var expr = info.inside_vc;

-            // Instantiate the "forall" variables

-            Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();

-            var ls = new List<VCExprVar>();

-            for (int i = 0; i < info.interfaceVars.Count; i++)

-            {

-                var v = translator.LookupVariable(info.interfaceVars[i]);

-                string newName = v.Name + "_fa_" + k.ToString() + "_" + newVarCnt.ToString();

-                newVarCnt++;

-                //checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);

-                var vp = checker.VCExprGen.Variable(newName, v.Type);

-                substForallDict.Add(v, vp);

-                ls.Add(vp);

-            }

-            interfaceVarCopies[info.impl.Name].Add(ls);

-            VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

-

-            SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

-            Contract.Assert(subst != null);

-            expr = subst.Mutate(expr, substForall);

-

-            // Instantiate and declare the "exists" variables

-            Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();

-            foreach (VCExprVar v in info.privateVars)

-            {

-                Contract.Assert(v != null);

-                string newName = v.Name + "_te_" + k.ToString() + "_" + newVarCnt.ToString();

-                newVarCnt++;

-                checker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);

-                substExistsDict.Add(v, checker.VCExprGen.Variable(newName, v.Type));

-            }

-            VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

-

-            subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

-            expr = subst.Mutate(expr, substExists);

-

-            procVcCopies[info.impl.Name].Add(expr);

-        }

-    }

-

     private void GenerateVCForLazyInlining(Program program, LazyInliningInfo info, Checker checker) {

       Contract.Requires(program != null);

       Contract.Requires(info != null);

@@ -389,7 +274,7 @@ namespace VC {
       ResetPredecessors(impl.Blocks);

       VCExpr reachvcexpr = GenerateReachVC(impl, info, checker);

       vcexpr = gen.And(vcexpr, reachvcexpr);

-      

+

       List<VCExprVar> privateVars = new List<VCExprVar>();

       foreach (Variable v in impl.LocVars) {

         Contract.Assert(v != null);

@@ -401,7 +286,6 @@ namespace VC {
       }

 

       info.privateVars = privateVars;

-      info.inside_vc = vcexpr;

 

       if (privateVars.Count > 0) {

         vcexpr = gen.Exists(new List<TypeVariable>(), privateVars, new List<VCTrigger>(),

@@ -421,12 +305,7 @@ namespace VC {
       Function function = cce.NonNull(info.function);

       VCExpr expr = gen.Function(function, interfaceExprs);

       Contract.Assert(expr != null);

-      if (CommandLineOptions.Clo.LazyInlining == 1) {

-        vcexpr = gen.Implies(expr, vcexpr);

-      } else {

-        //Contract.Assert(CommandLineOptions.Clo.LazyInlining == 2);

-        vcexpr = gen.Eq(expr, vcexpr);

-      }

+      vcexpr = gen.Implies(expr, vcexpr);

 

       List<VCTrigger> triggers = new List<VCTrigger>();

       List<VCExpr> exprs = new List<VCExpr>();

@@ -442,10 +321,7 @@ namespace VC {
                           new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);

 

       info.vcexpr = vcexpr;

-      if (CommandLineOptions.Clo.LazyInlining != 3)

-      {

-          checker.TheoremProver.PushVCExpression(vcexpr);

-      }

+      checker.TheoremProver.PushVCExpression(vcexpr);

     }

 

     protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) {

@@ -1662,12 +1538,6 @@ namespace VC {
         VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);

         Contract.Assert(vc != null);

 

-        if (CommandLineOptions.Clo.LazyInlining == 3)

-        {

-            var bm = new BoundingVCMutator(checker.VCExprGen, interfaceVarCopies);

-            vc = bm.Mutate(vc, true);

-        }

-

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

           reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, parent.implName2LazyInliningInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);

         } else {