added reachability information to the VC and used that to support arbitrary asserts in lazy inlining

8 files changed, 237 insertions, 63 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 4cf371a5..557f7d41 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -91,7 +91,7 @@ namespace VC
             public VCExpr falseExpr;

 

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

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

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

             {

                 Contract.Requires(impl != null);

                 Contract.Requires(program != null);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index f508fb3d..f3d08edb 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -88,20 +88,29 @@ namespace VC {
       public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins;

       public Hashtable/*<int, Absy!>*/ label2absy;

 

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

+      public Dictionary<Block, VCExprVar> reachVars;

+      public List<VCExprLetBinding> reachVarBindings;

+      public Variable inputErrorVariable;

+      public Variable outputErrorVariable;

+

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

         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);

 

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

         List<Variable> interfaceVars = new List<Variable>();

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

         Contract.Assert(assertExpr != null);

         foreach (Variable v in program.GlobalVariables()) {

           Contract.Assert(v != null);

           interfaceVars.Add(v);

+          if (v.Name == "error")

+            inputErrorVariable = v;

         }

         // InParams must be obtained from impl and not proc

         foreach (Variable v in impl.InParams) {

@@ -117,17 +126,24 @@ 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)

             continue;

           Variable v = e.Decl;

-          Constant c = new Constant(Token.NoToken,

-                                    new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

+          Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));

           interfaceVars.Add(c);

+          if (v.Name == "error") {

+            outputErrorVariable = c;

+            continue;

+          }

           Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

           assertExpr = Expr.And(assertExpr, eqExpr);

         }

+

         this.interfaceVars = interfaceVars;

         this.assertExpr = Expr.Not(assertExpr);

         VariableSeq functionInterfaceVars = new VariableSeq();

@@ -149,6 +165,7 @@ namespace VC {
     }

 

     private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

+    private GlobalVariable errorVariable;

 

     public void GenerateVCsForLazyInlining(Program program) {

       Contract.Requires(program != null);

@@ -161,6 +178,9 @@ namespace VC {
       VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)c.Op;

       checker.TheoremProver.Context.DeclareFunction(op.Func, "");

 

+      errorVariable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "error", Bpl.Type.Bool));  // come up with a better name for the variable

+      program.TopLevelDeclarations.Add(errorVariable);

+

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Contract.Assert(decl != null);

         Implementation impl = decl as Implementation;

@@ -168,9 +188,8 @@ namespace VC {
           continue;

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

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

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

+          LazyInliningInfo info = new LazyInliningInfo(impl, program, checker.TheoremProver.Context, QuantifierExpr.GetNextSkolemId(), errorVariable);

           implName2LazyInliningInfo[impl.Name] = info;

-          impl.LocVars.Add(info.controlFlowVariable);

           ExprSeq exprs = new ExprSeq();

           foreach (Variable v in program.GlobalVariables()) {

             Contract.Assert(v != null);

@@ -216,12 +235,16 @@ namespace VC {
       Hashtable/*<int, Absy!>*/ label2absy;

       VCExpressionGenerator gen = checker.VCExprGen;

       Contract.Assert(gen != null);

+      Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;

+      Contract.Assert(translator != null);

+      

       VCExpr vcexpr = gen.Not(GenerateVC(impl, info.controlFlowVariable, out label2absy, checker));

       Contract.Assert(vcexpr != null);

+      ResetPredecessors(impl.Blocks);

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

+      vcexpr = gen.And(vcexpr, reachvcexpr);

       info.label2absy = label2absy;

-

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

-      Contract.Assert(translator != null);

+      

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

       foreach (Variable v in impl.LocVars) {

         Contract.Assert(v != null);

@@ -272,6 +295,49 @@ namespace VC {
       info.vcexpr = vcexpr;

       checker.TheoremProver.PushVCExpression(vcexpr);

     }

+

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

+      Variable controlFlowVariable = info.controlFlowVariable;

+      VCExpressionGenerator gen = ch.VCExprGen;

+      Boogie2VCExprTranslator translator = ch.TheoremProver.Context.BoogieExprTranslator;

+      ProverContext proverCtxt = ch.TheoremProver.Context;

+      VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.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;

+    }

     #endregion

 

 

@@ -1515,7 +1581,6 @@ namespace VC {
     }

     #endregion

 

-

     protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

     {

       Contract.Requires(impl != null);

@@ -1598,6 +1663,10 @@ namespace VC {
           watch.Reset();

           watch.Start();

       }

+

+      if (errorVariable != null) {

+        impl.Proc.Modifies.Add(new IdentifierExpr(Token.NoToken, errorVariable));

+      }

       ConvertCFG2DAG(impl, program);

 

       SmokeTester smoke_tester = null;

@@ -2367,12 +2436,20 @@ namespace VC {
     // Used by lazy/stratified inlining

     protected virtual void addExitAssert(string implName, Block exitBlock)

     {

-        if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(implName))

-        {

-            Expr assertExpr = implName2LazyInliningInfo[implName].assertExpr;

-            Contract.Assert(assertExpr != null);

-            exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

-        }

+      if (CommandLineOptions.Clo.LazyInlining == 0) return;

+      Debug.Assert(implName2LazyInliningInfo != null);

+

+      if (implName2LazyInliningInfo.ContainsKey(implName)) {

+        Expr assertExpr = implName2LazyInliningInfo[implName].assertExpr;

+        Contract.Assert(assertExpr != null);

+        exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

+      }

+      else {

+        Expr oldExpr = new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, errorVariable));

+        Expr expr = new IdentifierExpr(Token.NoToken, errorVariable);

+        Expr assertExpr = NAryExpr.Imp(oldExpr, expr);

+        exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));

+      }

     }

 

     protected virtual void storeIncarnationMaps(string implName, Hashtable exitIncarnationMap)

@@ -2575,7 +2652,7 @@ namespace VC {
         {

           Cmd cmd = cce.NonNull( cmds[i]);

           AssertCmd assertCmd = cmd as AssertCmd;

-          if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)

+          if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId) == assertCmd.UniqueId)

           {

             Counterexample newCounterexample;

             newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, mvInfo, context, cce.NonNull(info.incarnationOriginMap));

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 1c67e06b..0b2c3225 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -64,7 +64,7 @@ namespace VC {
 

       for (int i = b.Cmds.Length; --i >= 0; )

       {

-        res = Cmd(cce.NonNull( b.Cmds[i]), res, ctxt);

+        res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);

       }

       

       int id = b.UniqueId;

@@ -83,7 +83,7 @@ namespace VC {
     /// <summary>

     /// Computes the wlp for an assert or assume command "cmd".

     /// </summary>

-    public static VCExpr Cmd(Cmd cmd, VCExpr N, VCContext ctxt)

+    public static VCExpr Cmd(Block b, Cmd cmd, VCExpr N, VCContext ctxt)

     {

       Contract.Requires(cmd!= null);

       Contract.Requires(N != null);

@@ -122,17 +122,12 @@ namespace VC {
           

           if (ctxt.ControlFlowVariable != null)

           {

-            VCExpr controlFlowVariableExpr = 

-              ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);

+            VCExpr controlFlowVariableExpr = ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);

             Contract.Assert(controlFlowVariableExpr != null);

-            VCExpr controlFlowFunctionAppl1 = 

-              gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

-            Contract.Assert(controlFlowFunctionAppl1 != null);

-            VCExpr controlFlowFunctionAppl2 = 

-              gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

-            VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl1, gen.Integer(BigNum.FromInt(0)));

-            VCExpr assertSuccess = gen.Neq(controlFlowFunctionAppl2, gen.Integer(BigNum.FromInt(0)));

-            return gen.And(gen.Implies(assertFailure, C), gen.Implies(assertSuccess, N));

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

+            Contract.Assert(controlFlowFunctionAppl != null);

+            VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId)));

+            return gen.And(gen.Implies(assertFailure, C), gen.Implies(C, N));

           }

           else

             return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);

diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer
index 1feac694..eb3baae3 100644
--- a/Test/lazyinline/Answer
+++ b/Test/lazyinline/Answer
@@ -2,31 +2,31 @@
 bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.

 bar1.bpl(21,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-        bar1.bpl(24,3): anon0

-        Inlined call to procedure foo begins

-            bar1.bpl(13,5): anon0

-            Inlined call to procedure bar begins

-                bar1.bpl(7,5): anon0

-            Inlined call to procedure bar ends

-            Inlined call to procedure bar begins

-                bar1.bpl(7,5): anon0

-            Inlined call to procedure bar ends

-        Inlined call to procedure foo ends

+    bar1.bpl(24,3): anon0

+    Inlined call to procedure foo begins

+        bar1.bpl(13,5): anon0

+        Inlined call to procedure bar begins

+            bar1.bpl(7,5): anon0

+        Inlined call to procedure bar ends

+        Inlined call to procedure bar begins

+            bar1.bpl(7,5): anon0

+        Inlined call to procedure bar ends

+    Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test bar2.bpl

 bar2.bpl(21,3): Error BP5001: This assertion might not hold.

 Execution trace:

-        bar2.bpl(19,3): anon0

-        Inlined call to procedure foo begins

-            bar2.bpl(5,3): anon0

-            bar2.bpl(6,7): anon3_Then

-        Inlined call to procedure foo ends

-        Inlined call to procedure foo begins

-            bar2.bpl(5,3): anon0

-            bar2.bpl(9,7): anon3_Else

-        Inlined call to procedure foo ends

+    bar2.bpl(19,3): anon0

+    Inlined call to procedure foo begins

+        bar2.bpl(5,3): anon0

+        bar2.bpl(6,7): anon3_Then

+    Inlined call to procedure foo ends

+    Inlined call to procedure foo begins

+        bar2.bpl(5,3): anon0

+        bar2.bpl(9,7): anon3_Else

+    Inlined call to procedure foo ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

@@ -34,23 +34,23 @@ Boogie program verifier finished with 0 verified, 1 error
 bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.

 bar3.bpl(34,1): Related location: This is the postcondition that might not hold.

 Execution trace:

-        bar3.bpl(38,3): anon0

-        Inlined call to procedure foo begins

-            bar3.bpl(18,3): anon0

-            bar3.bpl(19,7): anon3_Then

-            Inlined call to procedure bar begins

-                bar3.bpl(7,3): anon0

-                bar3.bpl(8,7): anon3_Then

-            Inlined call to procedure bar ends

-            Inlined call to procedure bar begins

-                bar3.bpl(7,3): anon0

-                bar3.bpl(8,7): anon3_Then

-            Inlined call to procedure bar ends

-        Inlined call to procedure foo ends

+    bar3.bpl(38,3): anon0

+    Inlined call to procedure foo begins

+        bar3.bpl(18,3): anon0

+        bar3.bpl(19,7): anon3_Then

         Inlined call to procedure bar begins

             bar3.bpl(7,3): anon0

-            bar3.bpl(10,7): anon3_Else

+            bar3.bpl(8,7): anon3_Then

         Inlined call to procedure bar ends

+        Inlined call to procedure bar begins

+            bar3.bpl(7,3): anon0

+            bar3.bpl(8,7): anon3_Then

+        Inlined call to procedure bar ends

+    Inlined call to procedure foo ends

+    Inlined call to procedure bar begins

+        bar3.bpl(7,3): anon0

+        bar3.bpl(10,7): anon3_Else

+    Inlined call to procedure bar ends

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

@@ -58,10 +58,34 @@ Boogie program verifier finished with 0 verified, 1 error
 

 Boogie program verifier finished with 1 verified, 0 errors

 -----

+----- Running regression test bar5.bpl

+(0,0): Error BP5001: This assertion might not hold.

+Execution trace:

+    bar5.bpl(24,3): anon0

+    Inlined call to procedure foo begins

+        bar5.bpl(13,5): anon0

+    Inlined call to procedure foo ends

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

 ----- Running regression test bar6.bpl

 

 Boogie program verifier finished with 1 verified, 0 errors

 -----

+----- Running regression test bar7.bpl

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

+----- Running regression test bar8.bpl

+(0,0): Error BP5001: This assertion might not hold.

+Execution trace:

+    bar8.bpl(13,5): anon0

+    Inlined call to procedure foo begins

+        bar8.bpl(6,3): anon0

+    Inlined call to procedure foo ends

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

 ----- Running regression test foo.bpl

 

 Boogie program verifier finished with 2 verified, 0 errors

diff --git a/Test/lazyinline/bar5.bpl b/Test/lazyinline/bar5.bpl
new file mode 100644
index 00000000..ec399b4a
--- /dev/null
+++ b/Test/lazyinline/bar5.bpl
@@ -0,0 +1,26 @@
+var x: int;

+var y: int;

+

+procedure {:inline 1} bar()

+modifies y;

+{

+  y := y + 1;

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  x := x + 1;

+  assert x == y;

+  call bar();

+  call bar();

+  x := x + 1;

+}

+

+procedure main()

+requires x == y;

+modifies x, y;

+{

+  call foo();

+}

+

diff --git a/Test/lazyinline/bar7.bpl b/Test/lazyinline/bar7.bpl
new file mode 100644
index 00000000..0eff6a7d
--- /dev/null
+++ b/Test/lazyinline/bar7.bpl
@@ -0,0 +1,27 @@
+var x: int;

+var y: int;

+

+procedure {:inline 1} bar()

+modifies y;

+{

+  y := y + 1;

+}

+

+procedure {:inline 1} foo() 

+modifies x, y;

+{

+  x := x + 1;

+  assert x != y;

+  call bar();

+  call bar();

+  x := x + 1;

+  assert x == y;

+}

+

+procedure main()

+requires x == y;

+modifies x, y;

+{

+  call foo();

+}

+

diff --git a/Test/lazyinline/bar8.bpl b/Test/lazyinline/bar8.bpl
new file mode 100644
index 00000000..dd6dab31
--- /dev/null
+++ b/Test/lazyinline/bar8.bpl
@@ -0,0 +1,16 @@
+var x: int;

+var y: int;

+

+procedure {:inline 1} foo() 

+{

+  assert x == y;

+}

+

+procedure main()

+requires x == y;

+modifies x, y;

+{

+  x := x + 1;

+  call foo();

+}

+

diff --git a/Test/lazyinline/runtest.bat b/Test/lazyinline/runtest.bat
index 6cf0ee1b..e7e86446 100644
--- a/Test/lazyinline/runtest.bat
+++ b/Test/lazyinline/runtest.bat
@@ -16,9 +16,18 @@ echo -----
 echo ----- Running regression test bar4.bpl

 %BGEXE% %* /noinfer /lazyInline:1 bar4.bpl

 echo -----

+echo ----- Running regression test bar5.bpl

+%BGEXE% %* /noinfer /lazyInline:1 bar5.bpl

+echo -----

 echo ----- Running regression test bar6.bpl

 %BGEXE% %* /noinfer /lazyInline:1 bar6.bpl

 echo -----

+echo ----- Running regression test bar7.bpl

+%BGEXE% %* /noinfer /lazyInline:1 bar7.bpl

+echo -----

+echo ----- Running regression test bar8.bpl

+%BGEXE% %* /noinfer /lazyInline:1 bar8.bpl

+echo -----

 echo ----- Running regression test foo.bpl

 %BGEXE% %* /noinfer /lazyInline:1 /extractLoops foo.bpl

 echo -----