eliminated LazyInliningInfo

1 files changed, 56 insertions, 87 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 758925fa..3bbe92a1 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -67,19 +67,51 @@ namespace VC
             return RECORD_TYPES.INT_BOOL;

         }

 

-        public class LazyInliningInfo {

-          [ContractInvariantMethod]

-          void ObjectInvariant() {

-            Contract.Invariant(impl != null);

-            Contract.Invariant(function != null);

-            Contract.Invariant(controlFlowVariable != null);

-            Contract.Invariant(assertExpr != null);

-            Contract.Invariant(cce.NonNullElements(interfaceVars));

-            Contract.Invariant(incarnationOriginMap == null || cce.NonNullDictionaryAndValues(incarnationOriginMap));

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

+          Variable controlFlowVariable = info.controlFlowVariable;

+          VCExpressionGenerator gen = ch.VCExprGen;

+          ProverContext proverCtxt = ch.TheoremProver.Context;

+          Boogie2VCExprTranslator translator = proverCtxt.BoogieExprTranslator;

+          VCExprVar controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);

+

+          Block exitBlock = null;

+          Dictionary<Block, VCExprVar> reachVars = new Dictionary<Block, VCExprVar>();

+          Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();

+          foreach (Block b in impl.Blocks) {

+            reachVars[b] = gen.Variable(b.Label + "_reachable", Bpl.Type.Bool);

+            reachExprs[b] = VCExpressionGenerator.False;

+            if (b.TransferCmd is ReturnCmd)

+              exitBlock = b;

           }

+          info.reachVars = reachVars;

 

+          foreach (Block b in impl.Blocks) {

+            foreach (Block pb in b.Predecessors) {

+              VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(pb.UniqueId)));

+              VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(b.UniqueId)));

+              reachExprs[b] = gen.Or(reachExprs[b], gen.And(reachVars[pb], controlTransferExpr));

+            }

+          }

+          reachExprs[impl.Blocks[0]] = VCExpressionGenerator.True;

+          List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

+          foreach (Block b in impl.Blocks) {

+            bindings.Add(gen.LetBinding(reachVars[b], reachExprs[b]));

+          }

+          info.reachVarBindings = bindings;

+

+          Debug.Assert(exitBlock != null && exitBlock.Cmds.Length > 0);

+          AssertCmd assertCmd = (AssertCmd)exitBlock.Cmds[exitBlock.Cmds.Length - 1];

+          Debug.Assert(assertCmd != null);

+          VCExpr exitFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(exitBlock.UniqueId)));

+          VCExpr exitTransferExpr = gen.Eq(exitFlowFunctionAppl, gen.Integer(BigNum.FromInt(assertCmd.UniqueId)));

+          VCExpr exitCondition = gen.And(info.reachVars[exitBlock], exitTransferExpr);

+          VCExpr errorExpr = gen.Eq(translator.LookupVariable(info.outputErrorVariable), gen.And(translator.LookupVariable(info.inputErrorVariable), exitCondition));

+          VCExpr reachvcexpr = gen.Let(info.reachVarBindings, errorExpr);

+          return reachvcexpr;

+        }

+

+        public class StratifiedInliningInfo {

           public Implementation impl;

-          public int uniqueId;

           public Function function;

           public Variable controlFlowVariable;

           public List<Variable> interfaceVars;

@@ -98,13 +130,20 @@ namespace VC
           public Variable inputErrorVariable;

           public Variable outputErrorVariable;

 

-          public LazyInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueId, GlobalVariable errorVariable) {

+          public bool initialized;

+          public int inline_cnt;

+          public List<VCExprVar> interfaceExprVars;

+          public VCExpr funcExpr;

+          public VCExpr falseExpr;

+

+          public StratifiedInliningInfo(Implementation impl, Program program, ProverContext ctxt) {

+            Contract.Requires(impl != null);

+            Contract.Requires(program != null);

             Contract.Requires(impl != null);

             Contract.Requires(program != null);

             Procedure proc = cce.NonNull(impl.Proc);

 

             this.impl = impl;

-            this.uniqueId = uniqueId;

             this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

             impl.LocVars.Add(controlFlowVariable);

 

@@ -131,9 +170,6 @@ namespace VC
               Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

               assertExpr = Expr.And(assertExpr, eqExpr);

             }

-            if (errorVariable != null) {

-              proc.Modifies.Add(new IdentifierExpr(Token.NoToken, errorVariable));

-            }

             foreach (IdentifierExpr e in proc.Modifies) {

               Contract.Assert(e != null);

               if (e.Decl == null)

@@ -170,81 +206,14 @@ namespace VC
               foreach (Variable v in interfaceVars) {

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

                 interfaceVarCopies[i].Add(constant);

-                //program.TopLevelDeclarations.Add(constant);

               }

             }

-          }

-        }

 

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

-          Variable controlFlowVariable = info.controlFlowVariable;

-          VCExpressionGenerator gen = ch.VCExprGen;

-          ProverContext proverCtxt = ch.TheoremProver.Context;

-          Boogie2VCExprTranslator translator = proverCtxt.BoogieExprTranslator;

-          VCExprVar controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);

-

-          Block exitBlock = null;

-          Dictionary<Block, VCExprVar> reachVars = new Dictionary<Block, VCExprVar>();

-          Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();

-          foreach (Block b in impl.Blocks) {

-            reachVars[b] = gen.Variable(b.Label + "_reachable", Bpl.Type.Bool);

-            reachExprs[b] = VCExpressionGenerator.False;

-            if (b.TransferCmd is ReturnCmd)

-              exitBlock = b;

-          }

-          info.reachVars = reachVars;

-

-          foreach (Block b in impl.Blocks) {

-            foreach (Block pb in b.Predecessors) {

-              VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(pb.UniqueId)));

-              VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(b.UniqueId)));

-              reachExprs[b] = gen.Or(reachExprs[b], gen.And(reachVars[pb], controlTransferExpr));

-            }

-          }

-          reachExprs[impl.Blocks[0]] = VCExpressionGenerator.True;

-          List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-          foreach (Block b in impl.Blocks) {

-            bindings.Add(gen.LetBinding(reachVars[b], reachExprs[b]));

+            inline_cnt = 0;

+            privateVars = new List<VCExprVar>();

+            interfaceExprVars = new List<VCExprVar>();

+            initialized = false;

           }

-          info.reachVarBindings = bindings;

-

-          Debug.Assert(exitBlock != null && exitBlock.Cmds.Length > 0);

-          AssertCmd assertCmd = (AssertCmd)exitBlock.Cmds[exitBlock.Cmds.Length - 1];

-          Debug.Assert(assertCmd != null);

-          VCExpr exitFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(exitBlock.UniqueId)));

-          VCExpr exitTransferExpr = gen.Eq(exitFlowFunctionAppl, gen.Integer(BigNum.FromInt(assertCmd.UniqueId)));

-          VCExpr exitCondition = gen.And(info.reachVars[exitBlock], exitTransferExpr);

-          VCExpr errorExpr = gen.Eq(translator.LookupVariable(info.outputErrorVariable), gen.And(translator.LookupVariable(info.inputErrorVariable), exitCondition));

-          VCExpr reachvcexpr = gen.Let(info.reachVarBindings, errorExpr);

-          return reachvcexpr;

-        }

-

-        public class StratifiedInliningInfo : LazyInliningInfo

-        {

-            [ContractInvariantMethod]

-            void ObjectInvariant()

-            {

-                Contract.Invariant(cce.NonNullElements(privateVars));

-                Contract.Invariant(cce.NonNullElements(interfaceExprVars));

-            }

-

-            public bool initialized;

-            public int inline_cnt;

-            public List<VCExprVar> interfaceExprVars;

-            public VCExpr funcExpr;

-            public VCExpr falseExpr;

-

-            public StratifiedInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueid)

-                : base(impl, program, ctxt, uniqueid, null)

-            {

-                Contract.Requires(impl != null);

-                Contract.Requires(program != null);

-                inline_cnt = 0;

-                privateVars = new List<VCExprVar>();

-                interfaceExprVars = new List<VCExprVar>();

-                initialized = false;

-            }

-

         }

 

         public void GenerateVCsForStratifiedInlining(Program program)

@@ -263,7 +232,7 @@ namespace VC
                 Procedure proc = cce.NonNull(impl.Proc);

                 if (proc.FindExprAttribute("inline") != null)

                 {

-                    StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, checker.TheoremProver.Context, QuantifierExpr.GetNextSkolemId());

+                    StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, checker.TheoremProver.Context);

                     implName2StratifiedInliningInfo[impl.Name] = info;

 

                     ExprSeq exprs = new ExprSeq();