more refactoring of the concurrency stuff

6 files changed, 103 insertions, 77 deletions

diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index caa58956..7d0febf5 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

@@ -74,6 +74,7 @@
     <Compile Include="LinearSets.cs" />

     <Compile Include="MoverCheck.cs" />

     <Compile Include="OwickiGries.cs" />

+    <Compile Include="Program.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="RefinementCheck.cs" />

     <Compile Include="TypeCheck.cs" />

@@ -111,4 +112,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 79f0f519..38902d57 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -26,29 +26,20 @@ namespace Microsoft.Boogie
             return MoverType.Top;

         }

 

+        LinearTypeChecker linearTypeChecker;

+        MoverTypeChecker moverTypeChecker;

+        List<Declaration> decls;

         HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;

         HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;

         HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;

-        LinearTypeChecker linearTypeChecker;

-        MoverTypeChecker moverTypeChecker;

-        Program moverCheckerProgram;

-        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

+        private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

+            this.linearTypeChecker = linearTypeChecker;

+            this.moverTypeChecker = moverTypeChecker;

+            this.decls = decls;

             this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

             this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

             this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

-            this.linearTypeChecker = linearTypeChecker;

-            this.moverTypeChecker = moverTypeChecker;

-            this.moverCheckerProgram = new Program();

-            foreach (Declaration decl in moverTypeChecker.program.TopLevelDeclarations)

-            {

-                if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom)

-                    this.moverCheckerProgram.TopLevelDeclarations.Add(decl);

-            }

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

-            {

-                this.moverCheckerProgram.TopLevelDeclarations.Add(v);

-            }

         }

         private sealed class MySubstituter : Duplicator

         {

@@ -98,7 +89,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             if (moverTypeChecker.procToActionInfo.Count == 0)

                 return;

@@ -117,7 +108,7 @@ namespace Microsoft.Boogie
             }

 

             Program program = moverTypeChecker.program;

-            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker);

+            MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);

             foreach (int phaseNum in pools.Keys)

             {

                 foreach (ActionInfo first in pools[phaseNum])

@@ -141,23 +132,6 @@ namespace Microsoft.Boogie
                     }

                 }

             }

-            var eraser = new LinearEraser();

-            eraser.VisitProgram(moverChecking.moverCheckerProgram);

-            {

-                int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

-                CommandLineOptions.Clo.PrintUnstructured = 1;

-                using (TokenTextWriter writer = new TokenTextWriter("MoverChecker.bpl", false))

-                {

-                    if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)

-                    {

-                        writer.WriteLine("// " + CommandLineOptions.Clo.Version);

-                        writer.WriteLine("// " + CommandLineOptions.Clo.Environment);

-                    }

-                    writer.WriteLine();

-                    moverChecking.moverCheckerProgram.Emit(writer);

-                }

-                CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

-            }

         }

 

         class TransitionRelationComputation

@@ -167,6 +141,7 @@ namespace Microsoft.Boogie
             private ActionInfo second;

             private Stack<Block> dfsStack;

             private Expr transitionRelation;

+            private int boundVariableCount;

 

             public TransitionRelationComputation(Program program, ActionInfo second)

             {

@@ -175,6 +150,7 @@ namespace Microsoft.Boogie
                 this.second = second;

                 this.dfsStack = new Stack<Block>();

                 this.transitionRelation = Expr.False;

+                this.boundVariableCount = 0;

             }

 

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

@@ -184,6 +160,12 @@ namespace Microsoft.Boogie
                 this.second = second;

                 this.dfsStack = new Stack<Block>();

                 this.transitionRelation = Expr.False;

+                this.boundVariableCount = 0;

+            }

+

+            private BoundVariable GetBoundVariable(Type type)

+            {

+                return new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, type));

             }

 

             public Expr Compute()

@@ -258,6 +240,21 @@ namespace Microsoft.Boogie
                             Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

                             returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr);

                         }

+                        else if (cmd is HavocCmd)

+                        {

+                            HavocCmd havocCmd = cmd as HavocCmd;

+                            List<Variable> existVars = new List<Variable>();

+                            Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

+                            foreach (IdentifierExpr ie in havocCmd.Vars)

+                            {

+                                BoundVariable bv = GetBoundVariable(ie.Decl.TypedIdent.Type);

+                                map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv);

+                                existVars.Add(bv);

+                            }

+                            Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

+                            Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);

+                            returnExpr = new ExistsExpr(Token.NoToken, existVars, (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr));

+                        }

                         else

                         {

                             Debug.Assert(false);

@@ -399,8 +396,8 @@ namespace Microsoft.Boogie
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);

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

             impl.Proc = proc;

-            this.moverCheckerProgram.TopLevelDeclarations.Add(impl);

-            this.moverCheckerProgram.TopLevelDeclarations.Add(proc);

+            this.decls.Add(impl);

+            this.decls.Add(proc);

         }

 

         private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)

@@ -430,8 +427,8 @@ namespace Microsoft.Boogie
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);

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

             impl.Proc = proc;

-            this.moverCheckerProgram.TopLevelDeclarations.Add(impl);

-            this.moverCheckerProgram.TopLevelDeclarations.Add(proc);

+            this.decls.Add(impl);

+            this.decls.Add(proc);

         }

 

         private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

@@ -502,8 +499,8 @@ namespace Microsoft.Boogie
             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, new List<IdentifierExpr>(), ensures);

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

             impl.Proc = proc;

-            this.moverCheckerProgram.TopLevelDeclarations.Add(impl);

-            this.moverCheckerProgram.TopLevelDeclarations.Add(proc);

+            this.decls.Add(impl);

+            this.decls.Add(proc);

         }

     }

 }
\ No newline at end of file
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index b16e4978..ee1547f2 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -158,20 +158,22 @@ namespace Microsoft.Boogie
         }

     }

 

-    public class OwickiGriesTransform

+    public class OwickiGries

     {

-        List<IdentifierExpr> globalMods;

         LinearTypeChecker linearTypeChecker;

         Dictionary<Absy, Absy> absyMap;

+        List<Declaration> decls;

+        List<IdentifierExpr> globalMods;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

         List<Procedure> yieldCheckerProcs;

         List<Implementation> yieldCheckerImpls;

         Procedure yieldProc;

 

-        public OwickiGriesTransform(LinearTypeChecker linearTypeChecker, Dictionary<Absy, Absy> absyMap)

+        public OwickiGries(LinearTypeChecker linearTypeChecker, Dictionary<Absy, Absy> absyMap, List<Declaration> decls)

         {

             this.linearTypeChecker = linearTypeChecker;

             this.absyMap = absyMap;

+            this.decls = decls;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

             foreach (Variable g in program.GlobalVariables())

@@ -795,7 +797,7 @@ namespace Microsoft.Boogie
             CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());

         }

 

-        private void AddYieldProcAndImpl(List<Declaration> decls) 

+        private void AddYieldProcAndImpl() 

         {

             if (yieldProc == null) return;

 

@@ -852,7 +854,7 @@ namespace Microsoft.Boogie
             return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;

         }

 

-        public void Transform(List<Implementation> impls, List<Procedure> procs, List<Declaration> decls)

+        public void Transform(List<Implementation> impls, List<Procedure> procs)

         {

             foreach (var impl in impls)

             {

@@ -874,7 +876,7 @@ namespace Microsoft.Boogie
             {

                 decls.Add(proc);

             }

-            AddYieldProcAndImpl(decls);

+            AddYieldProcAndImpl();

             foreach (var proc in procs)

             {

                 if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

@@ -897,40 +899,26 @@ namespace Microsoft.Boogie
             }

         }

 

-        public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             Program program = linearTypeChecker.program;

-            List<Procedure> originalProcs = new List<Procedure>();

-            List<Implementation> originalImpls = new List<Implementation>();

-            foreach (var decl in program.TopLevelDeclarations)

-            {

-                Procedure proc = decl as Procedure;

-                if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

-                {

-                    originalProcs.Add(proc);

-                    continue;

-                }

-                Implementation impl = decl as Implementation;

-                if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

-                {

-                    originalImpls.Add(impl);

-                }

-            }

-            List<Declaration> decls = new List<Declaration>();

             foreach (int phaseNum in moverTypeChecker.assertionPhaseNums)

             {

                 MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, int.MaxValue);

                 List<Implementation> impls = new List<Implementation>();

                 List<Procedure> procs = new List<Procedure>();

-                foreach (Implementation impl in originalImpls)

+                foreach (var decl in program.TopLevelDeclarations)

                 {

+                    Implementation impl = decl as Implementation;

+                    if (impl == null || !QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) continue;

                     Implementation duplicateImpl = duplicator.VisitImplementation(impl);

                     impls.Add(duplicateImpl);

                     procs.Add(duplicateImpl.Proc);

                 }

-                foreach (Procedure proc in originalProcs)

+                foreach (var decl in program.TopLevelDeclarations)

                 {

-                    if (duplicator.procMap.ContainsKey(proc)) continue;

+                    Procedure proc = decl as Procedure;

+                    if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields") || duplicator.procMap.ContainsKey(proc)) continue;

                     procs.Add(duplicator.VisitProcedure(proc));

                 }

                 Dictionary<Absy, Absy> reverseAbsyMap = new Dictionary<Absy, Absy>();

@@ -938,12 +926,9 @@ namespace Microsoft.Boogie
                 {

                     reverseAbsyMap[duplicator.absyMap[key]] = key;

                 }

-                OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker, reverseAbsyMap);

-                ogTransform.Transform(impls, procs, decls);

+                OwickiGries ogTransform = new OwickiGries(linearTypeChecker, reverseAbsyMap, decls);

+                ogTransform.Transform(impls, procs);

             }

-            program.TopLevelDeclarations.RemoveAll(x => originalImpls.Contains(x));

-            program.TopLevelDeclarations.RemoveAll(x => originalProcs.Contains(x));

-            program.TopLevelDeclarations.AddRange(decls);

         }

     }

 }

diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
new file mode 100644
index 00000000..592667c8
--- /dev/null
+++ b/Source/Concurrency/Program.cs
@@ -0,0 +1,43 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+namespace Microsoft.Boogie

+{

+    public class Concurrency

+    {

+        public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)

+        {

+            // The order in which originalDecls are computed and then *.AddCheckers are called is 

+            // apparently important.  The MyDuplicator code currently does not duplicate Attributes.

+            // Consequently, all the yield attributes are eliminated by the AddCheckers code.

+

+            List<Declaration> originalDecls = new List<Declaration>();

+            Program program = linearTypeChecker.program;

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                Procedure proc = decl as Procedure;

+                if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

+                {

+                    originalDecls.Add(proc);

+                    continue;

+                }

+                Implementation impl = decl as Implementation;

+                if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

+                {

+                    originalDecls.Add(impl);

+                }

+            }

+

+            List<Declaration> decls = new List<Declaration>();

+            OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

+            MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

+            RefinementCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

+

+            program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));

+            program.TopLevelDeclarations.AddRange(decls);

+        }

+

+    }

+}

diff --git a/Source/Concurrency/RefinementCheck.cs b/Source/Concurrency/RefinementCheck.cs
index f429ba5e..a39afe20 100644
--- a/Source/Concurrency/RefinementCheck.cs
+++ b/Source/Concurrency/RefinementCheck.cs
@@ -8,7 +8,7 @@ namespace Microsoft.Boogie
 {

     class RefinementCheck

     {

-        public static void AddCheckers(LinearTypeChecker linearTypeChecker)

+        public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

         }

     }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index bed9c6c0..35fe4dfe 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -485,7 +485,7 @@ namespace Microsoft.Boogie
 

         if (CommandLineOptions.Clo.StratifiedInlining == 0)

         {

-          OwickiGriesTransform.Transform(linearTypeChecker, moverTypeChecker);

+          Concurrency.Transform(linearTypeChecker, moverTypeChecker);

           var eraser = new LinearEraser();

           eraser.VisitProgram(program);

           if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)