added the framing for the refinement check

5 files changed, 44 insertions, 11 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index db2bfb23..4957c829 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -141,13 +141,28 @@ namespace Microsoft.Boogie
             private ActionInfo second; // corresponds to this*

             private Stack<Cmd> cmdStack;

             private List<PathInfo> paths;

+            private HashSet<Variable> frame;

 

-            public TransitionRelationComputation(Program program, ActionInfo second) : this(program, null, second)

+            public TransitionRelationComputation(Program program, ActionInfo second, HashSet<Variable> frame)

             {

+                this.frame = frame;

+                TransitionRelationComputationHelper(program, null, second);

+            }

+

+            public TransitionRelationComputation(Program program, ActionInfo second)

+            {

+                this.frame = new HashSet<Variable>(program.GlobalVariables());

+                TransitionRelationComputationHelper(program, null, second);

             }

 

             public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)

             {

+                this.frame = new HashSet<Variable>(program.GlobalVariables());

+                TransitionRelationComputationHelper(program, first, second);

+            }

+

+            private void TransitionRelationComputationHelper(Program program, ActionInfo first, ActionInfo second)

+            {

                 this.program = program;

                 this.first = first;

                 this.second = second;

@@ -213,7 +228,7 @@ namespace Microsoft.Boogie
             {

                 HashSet<Variable> existsVars = new HashSet<Variable>();

                 Dictionary<Variable, Expr> varToExpr = new Dictionary<Variable, Expr>();

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

+                foreach (Variable v in frame)

                 {

                     varToExpr[v] = Expr.Ident(v);

                 }

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 9de83635..3c5c53c8 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -781,7 +781,15 @@ namespace Microsoft.Boogie
                         foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

                     }

                     Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

-                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo)).TransitionRelationCompute();

+                    HashSet<Variable> frame = new HashSet<Variable>(program.GlobalVariables());

+                    foreach (Variable v in moverTypeChecker.qedGlobalVariables.Keys)

+                    {

+                        if (moverTypeChecker.qedGlobalVariables[v] <= actionInfo.phaseNum)

+                        {

+                            frame.Remove(v);

+                        }

+                    }

+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo, frame)).TransitionRelationCompute();

                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);

                     Expr alphaExpr = Expr.True;

                     foreach (AssertCmd assertCmd in actionInfo.thisGate)

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index a8266e79..5a15c707 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie
 

         CheckingContext checkingContext;

         public int errorCount;

-        Dictionary<Variable, int> qedGlobalVariables;

+        public Dictionary<Variable, int> qedGlobalVariables;

         Procedure enclosingProc;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

diff --git a/Test/og/Answer b/Test/og/Answer
index 4b880cac..f64868f7 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -118,4 +118,4 @@ Boogie program verifier finished with 104 verified, 0 errors
 

 -------------------- civl-paper.bpl --------------------

 

-Boogie program verifier finished with 35 verified, 0 errors

+Boogie program verifier finished with 37 verified, 0 errors

diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 0449a166..4f2da717 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -72,13 +72,13 @@ function {:inline} Inv(g: lmap) : bool
 }

 

 

-var {:qed} b: bool;

+var {:qed 1} b: bool;

 var {:qed} lock: X;

 

 procedure {:yields} Acquire({:cnst "tid"} tid: X)

 requires {:phase 1} InvLock(lock, b);

 ensures {:phase 1} InvLock(lock, b);

-ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; b := true; lock := tid; return true; }|;

+ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;

 {

     var status: bool;

     var tmp: X;

@@ -99,6 +99,16 @@ ensures {:right 1} |{ A: assert tid != nil; assume lock == nil; b := true; lock
 	goto L;

 }

 

+procedure {:yields} Release({:cnst "tid"} tid: X)

+ensures {:left 1} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;

+requires {:phase 1} InvLock(lock, b);

+ensures {:phase 1} InvLock(lock, b);

+{

+    par YieldLock();

+    call CLEAR(tid, false);

+    par YieldLock();

+}

+

 procedure {:yields} CAS(tid: X, prev: bool, next: bool) returns (status: bool);

 ensures {:atomic 0,1} |{ 

 A: goto B, C; 

@@ -106,10 +116,10 @@ B: assume b == prev; b := next; status := true; lock := tid; return true;
 C: status := false; return true; 

 }|;

 

-procedure {:yields} Release({:cnst "tid"} tid: X);

-ensures {:left 1} |{ A: assert lock == tid && tid != nil; b := false; lock := nil; return true; }|;

-requires {:phase 1} InvLock(lock, b);

-ensures {:phase 1} InvLock(lock, b);

+procedure {:yields} CLEAR(tid: X, next: bool);

+ensures {:atomic 0,1} |{ 

+A: b := next; lock := nil; return true; 

+}|;

 

 procedure {:yields} {:stable} YieldLock()

 requires {:phase 1} InvLock(lock, b);