From 7c6276c0713adbc8b6cfbf9325a7cf1a103f7acc Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 25 Oct 2013 12:37:44 -0700 Subject: a minor refactoring + implemented mover checking --- Source/Core/Core.csproj | 1 + Source/Core/Duplicator.cs | 6 +- Source/Core/LinearSets.cs | 4 +- Source/Core/MoverChecking.cs | 641 ++++++++++++++++++++++++++++++ Source/Core/OwickiGries.cs | 6 +- Source/ExecutionEngine/ExecutionEngine.cs | 8 +- 6 files changed, 655 insertions(+), 11 deletions(-) create mode 100644 Source/Core/MoverChecking.cs 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 @@ + 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 { /// /// 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. /// 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 globalVarToDomainName; public Dictionary 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> commutativityCheckerCache; + HashSet> gatePreservationCheckerCache; + HashSet> failurePreservationCheckerCache; + LinearTypeChecker linearTypeChecker; + Program moverCheckerProgram; + private MoverChecking(LinearTypeChecker linearTypeChecker) + { + this.commutativityCheckerCache = new HashSet>(); + this.gatePreservationCheckerCache = new HashSet>(); + this.failurePreservationCheckerCache = new HashSet>(); + 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() != 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() != 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 thisGate; + public CodeExpr thisAction; + public List thisInParams; + public List thisOutParams; + public List thatGate; + public CodeExpr thatAction; + public List thatInParams; + public List 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(); + this.thisAction = codeExpr; + this.thisInParams = new List(); + this.thisOutParams = new List(); + this.thatGate = new List(); + this.thatInParams = new List(); + this.thatOutParams = new List(); + + 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 map = new Dictionary(); + 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 otherLocVars = new List(); + 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 blockMap = new Dictionary(); + List otherBlocks = new List(); + foreach (Block block in thisAction.Blocks) + { + List otherCmds = new List(); + 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 otherGotoCmdLabelTargets = new List(); + List otherGotoCmdLabelNames = new List(); + 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 gatedActions = new List(); + 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 dfsStack; + private Expr transitionRelation; + + public TransitionRelationComputation(Program program, ActionInfo second) + { + this.program = program; + this.first = null; + this.second = second; + this.dfsStack = new Stack(); + 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(); + this.transitionRelation = Expr.False; + } + + public Expr Compute() + { + Search(second.thatAction.Blocks[0], false); + Dictionary map = new Dictionary(); + List boundVars = new List(); + 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 map = new Dictionary(); + for (int k = 0; k < assignCmd.Lhss.Count; k++) + { + map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; + } + Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); + 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 CloneBlocks(List blocks) + { + Dictionary blockMap = new Dictionary(); + List otherBlocks = new List(); + foreach (Block block in blocks) + { + List otherCmds = new List(); + 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 otherGotoCmdLabelTargets = new List(); + List otherGotoCmdLabelNames = new List(); + 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 DisjointnessRequires(Program program, ActionInfo first, ActionInfo second) + { + List requires = new List(); + Dictionary> domainNameToScope = new Dictionary>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToScope[domainName] = new HashSet(); + } + 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 actionPair = new Tuple(first, second); + if (commutativityCheckerCache.Contains(actionPair)) + return; + commutativityCheckerCache.Add(actionPair); + + List inputs = new List(); + inputs.AddRange(first.thisInParams); + inputs.AddRange(second.thatInParams); + List outputs = new List(); + outputs.AddRange(first.thisOutParams); + outputs.AddRange(second.thatOutParams); + List locals = new List(); + locals.AddRange(first.thisAction.LocVars); + locals.AddRange(second.thatAction.LocVars); + List firstBlocks = CloneBlocks(first.thisAction.Blocks); + List secondBlocks = CloneBlocks(second.thatAction.Blocks); + foreach (Block b in firstBlocks) + { + if (b.TransferCmd is ReturnCmd) + { + List bs = new List(); + bs.Add(secondBlocks[0]); + List ls = new List(); + ls.Add(secondBlocks[0].Label); + b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs); + } + } + List blocks = new List(); + blocks.AddRange(firstBlocks); + blocks.AddRange(secondBlocks); + List requires = DisjointnessRequires(program, first, second); + List ensures = new List(); + 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(), inputs, outputs, requires, new List(), ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 actionPair = new Tuple(first, second); + if (gatePreservationCheckerCache.Contains(actionPair)) + return; + gatePreservationCheckerCache.Add(actionPair); + + List inputs = new List(); + inputs.AddRange(first.thisInParams); + inputs.AddRange(second.thatInParams); + List outputs = new List(); + outputs.AddRange(first.thisOutParams); + outputs.AddRange(second.thatOutParams); + List locals = new List(); + locals.AddRange(second.thatAction.LocVars); + List secondBlocks = CloneBlocks(second.thatAction.Blocks); + List requires = DisjointnessRequires(program, first, second); + List ensures = new List(); + 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(), inputs, outputs, requires, new List(), ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 actionPair = new Tuple(first, second); + if (failurePreservationCheckerCache.Contains(actionPair)) + return; + failurePreservationCheckerCache.Add(actionPair); + + List inputs = new List(); + 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 = 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 map = new Dictionary(); + Dictionary oldMap = new Dictionary(); + List boundVars = new List(); + 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 = new List(); + ensures.Add(new Ensures(false, ensuresExpr)); + List blocks = new List(); + blocks.Add(new Block(Token.NoToken, "L", new List(), 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(), inputs, new List(), requires, new List(), ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), 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 globalMods; - LinearTypechecker linearTypechecker; + LinearTypeChecker linearTypechecker; Dictionary asyncAndParallelCallDesugarings; List yieldCheckerProcs; List 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 /// - 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 { 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; -- cgit v1.2.3