some refactoring to separate the concept of shared variables under refinement checking with all global variables

3 files changed, 36 insertions, 22 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 1dd350de..b10cd6cd 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -508,7 +508,7 @@ namespace Microsoft.Boogie
             ensures.Add(ensureCheck);

             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);

             impl.Proc = proc;

@@ -551,7 +551,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

             impl.Proc = proc;

@@ -599,7 +599,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

             impl.Proc = proc;

@@ -633,7 +633,7 @@ namespace Microsoft.Boogie
             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

             string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             impl.Proc = proc;

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index e485e1bc..8865b69e 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -198,7 +198,7 @@ namespace Microsoft.Boogie
                 }

                 procMap[node] = proc;

                 proc.Modifies = new List<IdentifierExpr>();

-                moverTypeChecker.program.GlobalVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));

+                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));

             }

             return procMap[node];

         }

@@ -279,7 +279,7 @@ namespace Microsoft.Boogie
             this.yieldingProcs = duplicator.yieldingProcs;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

-            foreach (Variable g in program.GlobalVariables)

+            foreach (Variable g in moverTypeChecker.SharedVariables)

             {

                 globalMods.Add(Expr.Ident(g));

             }

@@ -738,15 +738,16 @@ namespace Microsoft.Boogie
                     foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

                 }

                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

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

+                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);

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

-                foreach (Variable v in program.GlobalVariables)

+                foreach (Variable v in moverTypeChecker.SharedVariables)

                 {

-                    if (moverTypeChecker.hideLayerNums[v] <= actionInfo.createdAtLayerNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.createdAtLayerNum)

+                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 

+                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)

                     {

                         frame.Remove(v);

                     }

-                    if (moverTypeChecker.introduceLayerNums[v] == actionInfo.createdAtLayerNum)

+                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)

                     {

                         introducedVars.Add(v);

                     }

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index d6ccce45..22aae914 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -199,12 +199,23 @@ namespace Microsoft.Boogie
         }

     }

 

+    public class SharedVariableInfo

+    {

+        public int introLayerNum;

+        public int hideLayerNum;

+

+        public SharedVariableInfo(int introLayerNum, int hideLayerNum)

+        {

+            this.introLayerNum = introLayerNum;

+            this.hideLayerNum = hideLayerNum;

+        }

+    }

+

     public class MoverTypeChecker : ReadOnlyVisitor

     {

         CheckingContext checkingContext;

         public int errorCount;

-        public Dictionary<Variable, int> introduceLayerNums;

-        public Dictionary<Variable, int> hideLayerNums;

+        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;

         Procedure enclosingProc;

         Implementation enclosingImpl;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

@@ -334,12 +345,16 @@ namespace Microsoft.Boogie
             YieldTypeChecker.PerformYieldSafeCheck(this);

         }

 

+        public IEnumerable<Variable> SharedVariables

+        {

+            get { return this.globalVarToSharedVarInfo.Keys;  }

+        }

+

         public MoverTypeChecker(Program program)

         {

             this.auxVars = new HashSet<Variable>();

             this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();

-            this.introduceLayerNums = new Dictionary<Variable, int>();

-            this.hideLayerNums = new Dictionary<Variable, int>();

+            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();

             this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

@@ -359,13 +374,11 @@ namespace Microsoft.Boogie
                 }

                 else if (layerNums.Count == 1)

                 {

-                    this.introduceLayerNums[g] = layerNums[0];

-                    this.hideLayerNums[g] = int.MaxValue;

+                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);

                 }

                 else if (layerNums.Count == 2)

                 {

-                    this.introduceLayerNums[g] = layerNums[0];

-                    this.hideLayerNums[g] = layerNums[1];

+                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);

                 }

                 else

                 {

@@ -506,13 +519,13 @@ namespace Microsoft.Boogie
                 }

                 else

                 {

-                    if (hideLayerNums[node.Decl] < minLayerNum)

+                    if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)

                     {

-                        minLayerNum = hideLayerNums[node.Decl];

+                        minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;

                     }

-                    if (introduceLayerNums[node.Decl] > maxLayerNum)

+                    if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)

                     {

-                        maxLayerNum = introduceLayerNums[node.Decl];

+                        maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;

                     }

                 }

             }