diff options
| -rw-r--r-- | Source/Concurrency/Concurrency.csproj | 5 | ||||
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 79 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 49 | ||||
| -rw-r--r-- | Source/Concurrency/Program.cs | 43 | ||||
| -rw-r--r-- | Source/Concurrency/RefinementCheck.cs | 2 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 |
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)
|