- added async precondition checkers (#216)

- some renaming and documentation - disabled linear type checking in introduction procedures
boogie-org · Apr 3, 2020 · 7350a2a · 7350a2a
1 parent dc9ff7d
commit 7350a2a
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 19 deletions.
diff --git a/Source/Concurrency/CivlVCGeneration.cs b/Source/Concurrency/CivlVCGeneration.cs
@@ -42,7 +42,7 @@ public static void Transform(CivlTypeChecker civlTypeChecker)
 
             BackwardAssignmentSubstituter.SubstituteBackwardAssignments(civlTypeChecker.procToAtomicAction.Values);
 
-            linearTypeChecker.Transform();
+            linearTypeChecker.AddDeclarations();
             linearTypeChecker.EraseLinearAnnotations();
         }
     }

diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs
@@ -286,8 +286,10 @@ private void MapLeInt()
     /// The functionality is basically grouped into four parts (see #region's).
     /// 1) TypeCheck parses linear type attributes, sets up the data structures,
     ///    and performs a dataflow check on procedure implementations.
-    /// 2) Generation of linearity-invariant checker procedures for atomic actions.
-    /// 3) Erasure procedure to remove all linearity attributes
+    /// 2) Useful public methods to generate expressions for permissions, their disjointness,
+    ///    and their union.
+    /// 3) Generation of linearity-invariant checker procedures for atomic actions.
+    /// 4) Erasure procedure to remove all linearity attributes
     ///    (invoked after all other CIVL transformations).
     /// </summary>
     public class LinearTypeChecker : ReadOnlyVisitor
@@ -296,7 +298,7 @@ public class LinearTypeChecker : ReadOnlyVisitor
         public CheckingContext checkingContext;
         public Dictionary<string, LinearDomain> linearDomains;
 
-        private CivlTypeChecker ctc;
+        private CivlTypeChecker civlTypeChecker;
 
         private Dictionary<Absy, HashSet<Variable>> availableLinearVars;
         private Dictionary<Variable, LinearQualifier> inParamToLinearQualifier;
@@ -307,11 +309,11 @@ public class LinearTypeChecker : ReadOnlyVisitor
         private Dictionary<string, Dictionary<Type, Function>> domainNameToCollectors;
         private Dictionary<Variable, string> varToDomainName;
 
-        public LinearTypeChecker(CivlTypeChecker ctc)
+        public LinearTypeChecker(CivlTypeChecker civlTypeChecker)
         {
-            this.ctc = ctc;
-            this.program = ctc.program;
-            this.checkingContext = ctc.checkingContext;
+            this.civlTypeChecker = civlTypeChecker;
+            this.program = civlTypeChecker.program;
+            this.checkingContext = civlTypeChecker.checkingContext;
             this.domainNameToCollectors = new Dictionary<string, Dictionary<Type, Function>>();
             this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
             this.inParamToLinearQualifier = new Dictionary<Variable, LinearQualifier>();
@@ -455,7 +457,7 @@ public override Function VisitFunction(Function node)
         }
         public override Implementation VisitImplementation(Implementation node)
         {
-            if (ctc.procToAtomicAction.ContainsKey(node.Proc))
+            if (civlTypeChecker.procToAtomicAction.ContainsKey(node.Proc) || civlTypeChecker.procToIntroductionProc.ContainsKey(node.Proc))
                 return node;
 
             node.PruneUnreachableBlocks();
@@ -852,7 +854,7 @@ public override Ensures VisitEnsures(Ensures ensures)
         #endregion
 
         #region Useful public methods
-        public void Transform()
+        public void AddDeclarations()
         {
             foreach (LinearDomain domain in linearDomains.Values)
             {

diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs
@@ -257,16 +257,16 @@ private void DesugarAsyncCall(CallCmd newCall)
             if (!asyncCallPreconditionCheckers.ContainsKey(newCall.Proc.Name))
             {
                 asyncCallPreconditionCheckers[newCall.Proc.Name] = new Procedure(Token.NoToken,
-                    $"DummyAsyncTarget_{newCall.Proc.Name}",
+                    $"AsyncCallPreconditionChecker_{newCall.Proc.Name}",
                     newCall.Proc.TypeParameters, newCall.Proc.InParams, newCall.Proc.OutParams,
                     newCall.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
             }
 
-            var dummyAsyncTargetProc = asyncCallPreconditionCheckers[newCall.Proc.Name];
-            CallCmd dummyCallCmd = new CallCmd(newCall.tok, dummyAsyncTargetProc.Name, newCall.Ins,
+            var asyncCallPreconditionChecker = asyncCallPreconditionCheckers[newCall.Proc.Name];
+            CallCmd checkerCallCmd = new CallCmd(newCall.tok, asyncCallPreconditionChecker.Name, newCall.Ins,
                 newCall.Outs, newCall.Attributes);
-            dummyCallCmd.Proc = dummyAsyncTargetProc;
-            newCmdSeq.Add(dummyCallCmd);
+            checkerCallCmd.Proc = asyncCallPreconditionChecker;
+            newCmdSeq.Add(checkerCallCmd);
         }
 
         private void CollectPendingAsync(CallCmd call, CallCmd newCall, ActionProc actionProc)
@@ -459,6 +459,7 @@ public List<Declaration> Collect()
             decls.AddRange(procMap.Values);
             var newImpls = absyMap.Keys.OfType<Implementation>();
             decls.AddRange(newImpls);
+            decls.AddRange(asyncCallPreconditionCheckers.Values);
             decls.AddRange(YieldingProcInstrumentation.TransformImplementations(
                 civlTypeChecker,
                 linearTypeChecker,

diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs
@@ -574,7 +574,7 @@ private List<Cmd> DesugarParCallCmd(ParCallCmd parCallCmd)
             var newCmds = new List<Cmd>();
             List<Expr> ins = new List<Expr>();
             List<IdentifierExpr> outs = new List<IdentifierExpr>();
-            string procName = "og";
+            string procName = "ParallelCallPreconditionChecker";
             foreach (CallCmd callCmd in parCallCmd.CallCmds)
             {
                 procName = procName + "_" + callCmd.Proc.Name;
@@ -624,9 +624,9 @@ private List<Cmd> DesugarParCallCmd(ParCallCmd parCallCmd)
             }
 
             Procedure proc = parallelCallPreconditionCheckers[procName];
-            CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
-            dummyCallCmd.Proc = proc;
-            newCmds.Add(dummyCallCmd);
+            CallCmd checkerCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
+            checkerCallCmd.Proc = proc;
+            newCmds.Add(checkerCallCmd);
             return newCmds;
         }