diff options
| author |  qadeer <unknown> | 2013-10-25 12:37:44 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-10-25 12:37:44 -0700 |
| commit | 7c6276c0713adbc8b6cfbf9325a7cf1a103f7acc (patch) | |
| tree | b0052d4845cbe140dfbbe6336e5abfc7e68e1924 | |
| parent | cfd809c669908fd5c00344901e4d146308860f49 (diff) | |
a minor refactoring + implemented mover checking
| -rw-r--r-- | Source/Core/Core.csproj | 1 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 6 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 4 | ||||
| -rw-r--r-- | Source/Core/MoverChecking.cs | 641 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 6 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 8 |
6 files changed, 655 insertions, 11 deletions
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 6d5b7bd9..03eefccd 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -156,6 +156,7 @@ <Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
<Compile Include="BitvectorAnalysis.cs" />
+ <Compile Include="MoverChecking.cs" />
<Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index ef958fa6..402ea7dc 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -407,9 +407,9 @@ namespace Microsoft.Boogie { /// <summary>
/// Apply a substitution to an expression replacing "old" expressions.
/// Outside "old" expressions, the substitution "always" is applied; any variable not in
- /// domain(always) is not changed. Inside "old" expressions, apply map "oldExpr" to
- /// variables in domain(oldExpr), apply map "always" to variables in
- /// domain(always)-domain(oldExpr), and leave variable unchanged otherwise.
+ /// domain(always) is not changed. Inside "old" expressions, apply map "forOld" to
+ /// variables in domain(forOld), apply map "always" to variables in
+ /// domain(always)-domain(forOld), and leave variable unchanged otherwise.
/// </summary>
public static Expr ApplyReplacingOldExprs(Substitution always, Substitution forold, Expr expr) {
Contract.Requires(expr != null);
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 3a9de5fb..9af9661c 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -23,7 +23,7 @@ namespace Microsoft.Boogie }
}
- public class LinearTypechecker : StandardVisitor
+ public class LinearTypeChecker : StandardVisitor
{
public Program program;
public int errorCount;
@@ -35,7 +35,7 @@ namespace Microsoft.Boogie public Dictionary<Variable, string> globalVarToDomainName;
public Dictionary<string, LinearDomain> linearDomains;
- public LinearTypechecker(Program program)
+ public LinearTypeChecker(Program program)
{
this.program = program;
this.errorCount = 0;
diff --git a/Source/Core/MoverChecking.cs b/Source/Core/MoverChecking.cs new file mode 100644 index 00000000..aeea3947 --- /dev/null +++ b/Source/Core/MoverChecking.cs @@ -0,0 +1,641 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+ /*
+ * Typechecking rules:
+ * At most one atomic specification per procedure
+ * The gate of an atomic specification refers only to global and input variables
+ */
+ public class MoverChecking
+ {
+ HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;
+ HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;
+ HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;
+ LinearTypeChecker linearTypeChecker;
+ Program moverCheckerProgram;
+ private MoverChecking(LinearTypeChecker linearTypeChecker)
+ {
+ 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.moverCheckerProgram = new Program();
+ foreach (Declaration decl in linearTypeChecker.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 linearTypeChecker.program.GlobalVariables())
+ {
+ this.moverCheckerProgram.TopLevelDeclarations.Add(v);
+ }
+ }
+ private sealed class MySubstituter : Duplicator
+ {
+ private readonly Substitution outsideOld;
+ private readonly Substitution insideOld;
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(insideOld != null);
+ }
+
+ public MySubstituter(Substitution outsideOld, Substitution insideOld)
+ : base()
+ {
+ Contract.Requires(outsideOld != null && insideOld != null);
+ this.outsideOld = outsideOld;
+ this.insideOld = insideOld;
+ }
+
+ private bool insideOldExpr = false;
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ Expr e = null;
+
+ if (insideOldExpr)
+ {
+ e = insideOld(node.Decl);
+ }
+ else
+ {
+ e = outsideOld(node.Decl);
+ }
+ return e == null ? base.VisitIdentifierExpr(node) : e;
+ }
+
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ bool previouslyInOld = insideOldExpr;
+ insideOldExpr = true;
+ Expr tmp = (Expr)this.Visit(node.Expr);
+ OldExpr e = new OldExpr(node.tok, tmp);
+ insideOldExpr = previouslyInOld;
+ return e;
+ }
+ }
+
+ enum MoverType
+ {
+ Top,
+ Atomic,
+ Right,
+ Left,
+ Both
+ }
+
+ class ActionInfo
+ {
+ public Procedure proc;
+ public MoverType moverType;
+ public List<AssertCmd> thisGate;
+ public CodeExpr thisAction;
+ public List<Variable> thisInParams;
+ public List<Variable> thisOutParams;
+ public List<AssertCmd> thatGate;
+ public CodeExpr thatAction;
+ public List<Variable> thatInParams;
+ public List<Variable> thatOutParams;
+
+ public bool IsRightMover
+ {
+ get { return moverType == MoverType.Right || moverType == MoverType.Both; }
+ }
+
+ public bool IsLeftMover
+ {
+ get { return moverType == MoverType.Left || moverType == MoverType.Both; }
+ }
+
+ public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType)
+ {
+ this.proc = proc;
+ this.moverType = moverType;
+ this.thisGate = new List<AssertCmd>();
+ this.thisAction = codeExpr;
+ this.thisInParams = new List<Variable>();
+ this.thisOutParams = new List<Variable>();
+ this.thatGate = new List<AssertCmd>();
+ this.thatInParams = new List<Variable>();
+ this.thatOutParams = new List<Variable>();
+
+ var cmds = thisAction.Blocks[0].Cmds;
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ AssertCmd assertCmd = cmds[i] as AssertCmd;
+ if (assertCmd == null) break;
+ thisGate.Add(assertCmd);
+ cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in proc.InParams)
+ {
+ this.thisInParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
+ this.thatInParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in proc.OutParams)
+ {
+ this.thisOutParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ this.thatOutParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ List<Variable> otherLocVars = new List<Variable>();
+ foreach (Variable x in thisAction.LocVars)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ otherLocVars.Add(y);
+ }
+ Contract.Assume(proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (AssertCmd assertCmd in thisGate)
+ {
+ thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+ }
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in thisAction.Blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(Substituter.Apply(subst, cmd));
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = "that_" + block.Label;
+ block.Label = "this_" + block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ for (int i = 0; i < gotoCmd.labelNames.Count; i++)
+ {
+ gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
+ }
+ }
+ }
+ foreach (Block block in thisAction.Blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
+ }
+ }
+
+ public static void AddCheckers(LinearTypeChecker linearTypeChecker)
+ {
+ Program program = linearTypeChecker.program;
+ List<ActionInfo> gatedActions = new List<ActionInfo>();
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ foreach (Ensures e in proc.Ensures)
+ {
+ MoverType moverType = GetMoverType(e);
+ if (moverType == MoverType.Top) continue;
+ CodeExpr codeExpr = e.Condition as CodeExpr;
+ if (codeExpr == null)
+ {
+ Console.WriteLine("Warning: an atomic action must be a CodeExpr");
+ continue;
+ }
+ ActionInfo info = new ActionInfo(proc, codeExpr, moverType);
+ gatedActions.Add(info);
+ }
+ }
+ if (gatedActions.Count == 0)
+ return;
+ MoverChecking moverChecking = new MoverChecking(linearTypeChecker);
+ foreach (ActionInfo first in gatedActions)
+ {
+ Debug.Assert(first.moverType != MoverType.Top);
+ if (first.moverType == MoverType.Atomic)
+ continue;
+ foreach (ActionInfo second in gatedActions)
+ {
+ if (first.IsRightMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, first, second);
+ moverChecking.CreateGatePreservationChecker(program, second, first);
+ }
+ if (first.IsLeftMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, second, first);
+ moverChecking.CreateGatePreservationChecker(program, first, second);
+ moverChecking.CreateFailurePreservationChecker(program, second, first);
+ }
+ }
+ }
+ 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;
+ }
+ }
+
+ private static MoverType GetMoverType(Ensures e)
+ {
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
+ return MoverType.Atomic;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
+ return MoverType.Right;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
+ return MoverType.Left;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
+ return MoverType.Both;
+ else
+ return MoverType.Top;
+ }
+
+ class TransitionRelationComputation
+ {
+ private Program program;
+ private ActionInfo first;
+ private ActionInfo second;
+ private Stack<Block> dfsStack;
+ private Expr transitionRelation;
+
+ public TransitionRelationComputation(Program program, ActionInfo second)
+ {
+ this.program = program;
+ this.first = null;
+ this.second = second;
+ this.dfsStack = new Stack<Block>();
+ this.transitionRelation = Expr.False;
+ }
+
+ public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)
+ {
+ this.program = program;
+ this.first = first;
+ this.second = second;
+ this.dfsStack = new Stack<Block>();
+ this.transitionRelation = Expr.False;
+ }
+
+ public Expr Compute()
+ {
+ Search(second.thatAction.Blocks[0], false);
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ List<Variable> boundVars = new List<Variable>();
+ if (first != null)
+ {
+ foreach (Variable v in first.thisAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ boundVars.Add(bv);
+ }
+ }
+ foreach (Variable v in second.thatAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ boundVars.Add(bv);
+ }
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ if (boundVars.Count > 0)
+ return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation));
+ else
+ return transitionRelation;
+ }
+
+ private Expr CalculatePathCondition()
+ {
+ Expr returnExpr = Expr.True;
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ if (first != null)
+ {
+ foreach (Variable v in first.thisOutParams)
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ }
+ foreach (Variable v in second.thatOutParams)
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ Block[] dfsStackAsArray = dfsStack.Reverse().ToArray();
+ for (int i = dfsStackAsArray.Length - 1; i >= 0; i--)
+ {
+ Block b = dfsStackAsArray[i];
+ for (int j = b.Cmds.Count - 1; j >= 0; j--)
+ {
+ Cmd cmd = b.Cmds[j];
+ if (cmd is AssumeCmd)
+ {
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);
+ }
+ else if (cmd is AssignCmd)
+ {
+ AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ for (int k = 0; k < assignCmd.Lhss.Count; k++)
+ {
+ map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];
+ }
+ Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);
+ returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr);
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+ }
+ return returnExpr;
+ }
+
+ private void Search(Block b, bool inFirst)
+ {
+ dfsStack.Push(b);
+ if (b.TransferCmd is ReturnExprCmd)
+ {
+ if (first == null || inFirst)
+ {
+ transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition());
+ }
+ else
+ {
+ Search(first.thisAction.Blocks[0], true);
+ }
+ }
+ else
+ {
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ Search(target, inFirst);
+ }
+ }
+ dfsStack.Pop();
+ }
+ }
+
+ private static List<Block> CloneBlocks(List<Block> blocks)
+ {
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(cmd);
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ }
+ foreach (Block block in blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ return otherBlocks;
+ }
+
+ private List<Requires> DisjointnessRequires(Program program, ActionInfo first, ActionInfo second)
+ {
+ List<Requires> requires = new List<Requires>();
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ domainNameToScope[domainName] = new HashSet<Variable>();
+ }
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (Variable v in first.thisInParams)
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ for (int i = 0; i < second.thatInParams.Count; i++)
+ {
+ var domainName = linearTypeChecker.FindDomainName(second.thisInParams[i]);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(second.thatInParams[i]);
+ }
+ foreach (string domainName in domainNameToScope.Keys)
+ {
+ requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ return requires;
+ }
+
+ private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (commutativityCheckerCache.Contains(actionPair))
+ return;
+ commutativityCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thisOutParams);
+ outputs.AddRange(second.thatOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(first.thisAction.LocVars);
+ locals.AddRange(second.thatAction.LocVars);
+ List<Block> firstBlocks = CloneBlocks(first.thisAction.Blocks);
+ List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
+ foreach (Block b in firstBlocks)
+ {
+ if (b.TransferCmd is ReturnCmd)
+ {
+ List<Block> bs = new List<Block>();
+ bs.Add(secondBlocks[0]);
+ List<string> ls = new List<string>();
+ ls.Add(secondBlocks[0].Label);
+ b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);
+ }
+ }
+ List<Block> blocks = new List<Block>();
+ blocks.AddRange(firstBlocks);
+ blocks.AddRange(secondBlocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ List<Ensures> ensures = new List<Ensures>();
+ Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();
+ ensures.Add(new Ensures(false, transitionRelation));
+ string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ 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);
+ }
+
+ private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (gatePreservationCheckerCache.Contains(actionPair))
+ return;
+ gatePreservationCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thisOutParams);
+ outputs.AddRange(second.thatOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(second.thatAction.LocVars);
+ List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ List<Ensures> ensures = new List<Ensures>();
+ foreach (AssertCmd assertCmd in first.thisGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ ensures.Add(new Ensures(false, assertCmd.Expr));
+ }
+ string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ 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);
+ }
+
+ private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (failurePreservationCheckerCache.Contains(actionPair))
+ return;
+ failurePreservationCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+
+ Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute();
+ Expr expr = Expr.True;
+ foreach (AssertCmd assertCmd in first.thisGate)
+ {
+ expr = Expr.And(assertCmd.Expr, expr);
+ }
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ requires.Add(new Requires(false, Expr.Not(expr)));
+ foreach (AssertCmd assertCmd in second.thatGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();
+ List<Variable> boundVars = new List<Variable>();
+ foreach (Variable v in program.GlobalVariables())
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ foreach (Variable v in second.thatOutParams)
+ {
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ }
+ foreach (Variable v in second.thatAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+
+ Expr ensuresExpr = Expr.And(transitionRelation, Expr.Not(expr));
+ if (boundVars.Count > 0)
+ {
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
+ ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, (Expr)new MySubstituter(subst, oldSubst).Visit(ensuresExpr));
+ }
+ List<Ensures> ensures = new List<Ensures>();
+ ensures.Add(new Ensures(false, ensuresExpr));
+ List<Block> blocks = new List<Block>();
+ blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
+ string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ 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);
+ }
+ }
+}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index dd6276c2..8396e82e 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -13,13 +13,13 @@ namespace Microsoft.Boogie public class OwickiGriesTransform
{
List<IdentifierExpr> globalMods;
- LinearTypechecker linearTypechecker;
+ LinearTypeChecker linearTypechecker;
Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
List<Procedure> yieldCheckerProcs;
List<Implementation> yieldCheckerImpls;
Procedure yieldProc;
- public OwickiGriesTransform(LinearTypechecker linearTypechecker)
+ public OwickiGriesTransform(LinearTypeChecker linearTypechecker)
{
this.linearTypechecker = linearTypechecker;
Program program = linearTypechecker.program;
@@ -689,6 +689,8 @@ namespace Microsoft.Boogie public void Transform()
{
+ MoverChecking.AddCheckers(linearTypechecker);
+
Program program = linearTypechecker.program;
foreach (var decl in program.TopLevelDeclarations)
{
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 92cc7429..18de44d4 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -419,7 +419,7 @@ namespace Microsoft.Boogie PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
}
- LinearTypechecker linearTypechecker;
+ LinearTypeChecker linearTypechecker;
PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypechecker);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
@@ -576,7 +576,7 @@ namespace Microsoft.Boogie /// - TypeCheckingError if a type checking error occurred
/// - ResolvedAndTypeChecked if both resolution and type checking succeeded
/// </summary>
- public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypechecker linearTypechecker)
+ public static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName, out LinearTypeChecker linearTypechecker)
{
Contract.Requires(program != null);
Contract.Requires(bplFileName != null);
@@ -611,7 +611,7 @@ namespace Microsoft.Boogie return PipelineOutcome.TypeCheckingError;
}
- linearTypechecker = new LinearTypechecker(program);
+ linearTypechecker = new LinearTypeChecker(program);
linearTypechecker.Typecheck();
if (linearTypechecker.errorCount == 0)
{
@@ -1142,7 +1142,7 @@ namespace Microsoft.Boogie private static Program ProgramFromFile(string filename) {
Program p = ParseBoogieProgram(new List<string> { filename }, false);
System.Diagnostics.Debug.Assert(p != null);
- LinearTypechecker linearTypechecker;
+ LinearTypeChecker linearTypechecker;
PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypechecker);
System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
return p;
|