From 3c65f1b879a19c5ab1ed78ebfbcdb434fe7afe06 Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 22 Nov 2013 13:04:51 -0800 Subject: factored the concurrency checking code into a separate project --- Source/Boogie.sln | 26 + Source/Concurrency/App.config | 6 + Source/Concurrency/Concurrency.csproj | 88 +++ Source/Concurrency/LinearSets.cs | 757 ++++++++++++++++++++++++++ Source/Concurrency/MoverChecking.cs | 641 ++++++++++++++++++++++ Source/Concurrency/OwickiGries.cs | 738 +++++++++++++++++++++++++ Source/Concurrency/Properties/AssemblyInfo.cs | 36 ++ Source/Core/Core.csproj | 3 - Source/Core/LinearSets.cs | 757 -------------------------- Source/Core/MoverChecking.cs | 641 ---------------------- Source/Core/OwickiGries.cs | 738 ------------------------- Source/ExecutionEngine/ExecutionEngine.csproj | 4 + 12 files changed, 2296 insertions(+), 2139 deletions(-) create mode 100644 Source/Concurrency/App.config create mode 100644 Source/Concurrency/Concurrency.csproj create mode 100644 Source/Concurrency/LinearSets.cs create mode 100644 Source/Concurrency/MoverChecking.cs create mode 100644 Source/Concurrency/OwickiGries.cs create mode 100644 Source/Concurrency/Properties/AssemblyInfo.cs delete mode 100644 Source/Core/LinearSets.cs delete mode 100644 Source/Core/MoverChecking.cs delete mode 100644 Source/Core/OwickiGries.cs diff --git a/Source/Boogie.sln b/Source/Boogie.sln index cadcaacb..2b821255 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -37,6 +37,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "Executio EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8A05D14E-F2BF-4890-BBE0-D76B18A50797}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "Concurrency\Concurrency.csproj", "{D07B8E38-E172-47F4-AD02-0373014A46D3}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Checked|.NET = Checked|.NET @@ -481,6 +483,30 @@ Global {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|x86.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Checked|.NET.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Checked|Any CPU.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Checked|Any CPU.Build.0 = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Checked|Mixed Platforms.Build.0 = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Checked|x86.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|.NET.ActiveCfg = Debug|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|Any CPU.Build.0 = Debug|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Debug|x86.ActiveCfg = Debug|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|.NET.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|Any CPU.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|Any CPU.Build.0 = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|Mixed Platforms.Build.0 = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.Release|x86.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|.NET.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Any CPU.Build.0 = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU + {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|x86.ActiveCfg = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/Source/Concurrency/App.config b/Source/Concurrency/App.config new file mode 100644 index 00000000..84bc4207 --- /dev/null +++ b/Source/Concurrency/App.config @@ -0,0 +1,6 @@ + + + + + + diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj new file mode 100644 index 00000000..ba9a1dda --- /dev/null +++ b/Source/Concurrency/Concurrency.csproj @@ -0,0 +1,88 @@ + + + + + Debug + AnyCPU + {D07B8E38-E172-47F4-AD02-0373014A46D3} + Library + Properties + Concurrency + Concurrency + v4.0 + 512 + Client + + + AnyCPU + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + AnyCPU + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + + + true + + + ..\InterimKey.snk + + + + + + + + + + + + + + + + + + + + + + {43dfad18-3e35-4558-9be2-caff6b5ba8a0} + Basetypes + + + {b230a69c-c466-4065-b9c1-84d80e76d802} + Core + + + {69a2b0b8-bcac-4101-ae7a-556fcc58c06e} + Graph + + + {fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5} + ParserHelper + + + + + \ No newline at end of file diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs new file mode 100644 index 00000000..51f7f328 --- /dev/null +++ b/Source/Concurrency/LinearSets.cs @@ -0,0 +1,757 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; + +namespace Microsoft.Boogie +{ + public class LinearEraser : StandardVisitor + { + private QKeyValue RemoveLinearAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveLinearAttribute(iter.Next); + return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next; + } + + public override Variable VisitVariable(Variable node) + { + node.Attributes = RemoveLinearAttribute(node.Attributes); + return base.VisitVariable(node); + } + } + + public class LinearTypeChecker : StandardVisitor + { + public Program program; + public int errorCount; + public CheckingContext checkingContext; + public Dictionary domainNameToType; + public Dictionary> availableLinearVars; + public Dictionary inoutParamToDomainName; + public Dictionary varToDomainName; + public Dictionary globalVarToDomainName; + public Dictionary linearDomains; + + public LinearTypeChecker(Program program) + { + this.program = program; + this.errorCount = 0; + this.checkingContext = new CheckingContext(null); + this.domainNameToType = new Dictionary(); + this.parallelCallInvars = new HashSet(); + this.availableLinearVars = new Dictionary>(); + this.inoutParamToDomainName = new Dictionary(); + this.varToDomainName = new Dictionary(); + this.linearDomains = new Dictionary(); + } + public void Typecheck() + { + this.VisitProgram(program); + foreach (string domainName in domainNameToType.Keys) + { + this.linearDomains[domainName] = new LinearDomain(program, domainName, domainNameToType[domainName]); + } + } + private void Error(Absy node, string message) + { + checkingContext.Error(node, message); + errorCount++; + } + public override Program VisitProgram(Program node) + { + globalVarToDomainName = new Dictionary(); + foreach (GlobalVariable g in program.GlobalVariables()) + { + string domainName = FindDomainName(g); + if (domainName != null) + { + globalVarToDomainName[g] = domainName; + } + } + return base.VisitProgram(node); + } + public override Implementation VisitImplementation(Implementation node) + { + HashSet start = new HashSet(globalVarToDomainName.Keys); + for (int i = 0; i < node.InParams.Count; i++) + { + string domainName = FindDomainName(node.Proc.InParams[i]); + if (domainName != null) + { + inoutParamToDomainName[node.InParams[i]] = domainName; + start.Add(node.InParams[i]); + } + } + for (int i = 0; i < node.OutParams.Count; i++) + { + string domainName = FindDomainName(node.Proc.OutParams[i]); + if (domainName != null) + { + inoutParamToDomainName[node.OutParams[i]] = domainName; + } + } + + var oldErrorCount = this.errorCount; + var impl = base.VisitImplementation(node); + if (oldErrorCount < this.errorCount) + return impl; + + Stack dfsStack = new Stack(); + HashSet dfsStackAsSet = new HashSet(); + availableLinearVars[node.Blocks[0]] = start; + dfsStack.Push(node.Blocks[0]); + dfsStackAsSet.Add(node.Blocks[0]); + while (dfsStack.Count > 0) + { + Block b = dfsStack.Pop(); + dfsStackAsSet.Remove(b); + HashSet end = PropagateAvailableLinearVarsAcrossBlock(b); + if (b.TransferCmd is ReturnCmd) + { + foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end)) + { + Error(b, string.Format("Global variable {0} must be available at a return", g.Name)); + } + foreach (Variable v in node.OutParams) + { + if (FindDomainName(v) == null || end.Contains(v)) continue; + Error(b, string.Format("Output variable {0} must be available at a return", v.Name)); + } + continue; + } + GotoCmd gotoCmd = b.TransferCmd as GotoCmd; + foreach (Block target in gotoCmd.labelTargets) + { + if (!availableLinearVars.ContainsKey(target)) + { + availableLinearVars[target] = new HashSet(end); + dfsStack.Push(target); + dfsStackAsSet.Add(target); + } + else + { + var savedAvailableVars = new HashSet(availableLinearVars[target]); + availableLinearVars[target].IntersectWith(end); + if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target)) + { + dfsStack.Push(target); + dfsStackAsSet.Add(target); + } + } + } + } + return impl; + } + private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) { + HashSet start = new HashSet(availableLinearVars[b]); + foreach (Cmd cmd in b.Cmds) + { + if (cmd is AssignCmd) + { + AssignCmd assignCmd = (AssignCmd)cmd; + for (int i = 0; i < assignCmd.Lhss.Count; i++) + { + if (FindDomainName(assignCmd.Lhss[i].DeepAssignedVariable) == null) continue; + IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr; + if (start.Contains(ie.Decl)) + { + start.Remove(ie.Decl); + } + else + { + Error(ie, "unavailable source for a linear read"); + } + } + foreach (AssignLhs assignLhs in assignCmd.Lhss) + { + if (FindDomainName(assignLhs.DeepAssignedVariable) == null) continue; + start.Add(assignLhs.DeepAssignedVariable); + } + } + else if (cmd is CallCmd) + { + foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) + { + Error(b, string.Format("Global variable {0} must be available at a call", g.Name)); + } + CallCmd callCmd = (CallCmd)cmd; + while (callCmd != null) + { + for (int i = 0; i < callCmd.Proc.InParams.Count; i++) + { + if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue; + IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr; + if (start.Contains(ie.Decl)) + { + start.Remove(ie.Decl); + } + else + { + Error(ie, "unavailable source for a linear read"); + } + } + callCmd = callCmd.InParallelWith; + } + callCmd = (CallCmd)cmd; + availableLinearVars[callCmd] = new HashSet(start); + while (callCmd != null) + { + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (FindDomainName(ie.Decl) == null) continue; + start.Add(ie.Decl); + } + callCmd = callCmd.InParallelWith; + } + } + else if (cmd is HavocCmd) + { + HavocCmd havocCmd = (HavocCmd) cmd; + foreach (IdentifierExpr ie in havocCmd.Vars) + { + if (FindDomainName(ie.Decl) == null) continue; + start.Remove(ie.Decl); + } + } + else if (cmd is YieldCmd) + { + foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) + { + Error(b, string.Format("Global variable {0} must be available at a yield", g.Name)); + } + availableLinearVars[cmd] = new HashSet(start); + } + } + return start; + } + public string FindDomainName(Variable v) + { + if (globalVarToDomainName.ContainsKey(v)) + return globalVarToDomainName[v]; + if (inoutParamToDomainName.ContainsKey(v)) + return inoutParamToDomainName[v]; + return QKeyValue.FindStringAttribute(v.Attributes, "linear"); + } + public override Variable VisitVariable(Variable node) + { + string domainName = FindDomainName(node); + if (domainName != null) + { + Type type = node.TypedIdent.Type; + MapType mapType = type as MapType; + if (mapType != null) + { + if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool)) + { + type = mapType.Arguments[0]; + if (type is MapType) + { + Error(node, "the domain of a linear set must be a scalar type"); + return base.VisitVariable(node); + } + } + else + { + Error(node, "a linear domain can be attached to either a set or a scalar type"); + return base.VisitVariable(node); + } + } + if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type)) + { + Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName)); + } + else + { + domainNameToType[domainName] = type; + } + } + return base.VisitVariable(node); + } + public override Cmd VisitAssignCmd(AssignCmd node) + { + HashSet rhsVars = new HashSet(); + for (int i = 0; i < node.Lhss.Count; i++) + { + AssignLhs lhs = node.Lhss[i]; + Variable lhsVar = lhs.DeepAssignedVariable; + string domainName = FindDomainName(lhsVar); + if (domainName == null) continue; + SimpleAssignLhs salhs = lhs as SimpleAssignLhs; + if (salhs == null) + { + Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name)); + continue; + } + IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr; + if (rhs == null) + { + Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name)); + continue; + } + string rhsDomainName = FindDomainName(rhs.Decl); + if (rhsDomainName == null) + { + Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name)); + continue; + } + if (domainName != rhsDomainName) + { + Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName)); + continue; + } + if (rhsVars.Contains(rhs.Decl)) + { + Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name)); + continue; + } + rhsVars.Add(rhs.Decl); + } + return base.VisitAssignCmd(node); + } + HashSet parallelCallInvars; + public override Cmd VisitCallCmd(CallCmd node) + { + HashSet inVars = new HashSet(); + for (int i = 0; i < node.Proc.InParams.Count; i++) + { + Variable formal = node.Proc.InParams[i]; + string domainName = FindDomainName(formal); + if (domainName == null) continue; + IdentifierExpr actual = node.Ins[i] as IdentifierExpr; + if (actual == null) + { + Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name)); + continue; + } + string actualDomainName = FindDomainName(actual.Decl); + if (actualDomainName == null) + { + Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name)); + continue; + } + if (domainName != actualDomainName) + { + Error(node, "The domains of formal and actual parameters must be the same"); + continue; + } + if (parallelCallInvars.Contains(actual.Decl)) + { + Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name)); + continue; + } + if (actual.Decl is GlobalVariable) + { + Error(node, "Only local linear variable can be an actual input parameter of a procedure call"); + continue; + } + inVars.Add(actual.Decl); + parallelCallInvars.Add(actual.Decl); + } + for (int i = 0; i < node.Proc.OutParams.Count; i++) + { + IdentifierExpr actual = node.Outs[i]; + string actualDomainName = FindDomainName(actual.Decl); + if (actualDomainName == null) continue; + Variable formal = node.Proc.OutParams[i]; + string domainName = FindDomainName(formal); + if (domainName == null) + { + Error(node, "Only a linear variable can be passed to a linear parameter"); + continue; + } + if (domainName != actualDomainName) + { + Error(node, "The domains of formal and actual parameters must be the same"); + continue; + } + if (actual.Decl is GlobalVariable) + { + Error(node, "Only local linear variable can be actual output parameter of a procedure call"); + continue; + } + } + if (node.InParallelWith != null) + { + VisitCallCmd(node.InParallelWith); + } + foreach (Variable v in inVars) + { + parallelCallInvars.Remove(v); + } + return base.VisitCallCmd(node); + } + + private void AddDisjointnessExpr(List newCmds, Absy absy, Dictionary domainNameToInputVar) + { + Dictionary> domainNameToScope = new Dictionary>(); + foreach (var domainName in linearDomains.Keys) + { + domainNameToScope[domainName] = new HashSet(); + domainNameToScope[domainName].Add(domainNameToInputVar[domainName]); + } + foreach (Variable v in availableLinearVars[absy]) + { + var domainName = FindDomainName(v); + domainNameToScope[domainName].Add(v); + } + foreach (string domainName in linearDomains.Keys) + { + newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName]))); + } + } + + public void Transform() + { + foreach (var decl in program.TopLevelDeclarations) + { + Implementation impl = decl as Implementation; + if (impl == null) continue; + Dictionary domainNameToInputVar = new Dictionary(); + foreach (string domainName in linearDomains.Keys) + { + var domain = linearDomains[domainName]; + Formal f = new Formal( + Token.NoToken, + new TypedIdent(Token.NoToken, + "linear_" + domainName + "_in", + new MapType(Token.NoToken, new List(), + new List { domain.elementType }, Type.Bool)), true); + impl.InParams.Add(f); + domainNameToInputVar[domainName] = f; + } + + foreach (Block b in impl.Blocks) + { + List newCmds = new List(); + for (int i = 0; i < b.Cmds.Count; i++) + { + Cmd cmd = b.Cmds[i]; + newCmds.Add(cmd); + if (cmd is CallCmd) + { + CallCmd callCmd = cmd as CallCmd; + if (callCmd.IsAsync) + { + foreach (var domainName in linearDomains.Keys) + { + var domain = linearDomains[domainName]; + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + callCmd.Ins.Add(expr); + } + } + else if (callCmd.InParallelWith != null) + { + while (callCmd != null) + { + foreach (var domainName in linearDomains.Keys) + { + var domain = linearDomains[domainName]; + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + callCmd.Ins.Add(expr); + } + callCmd = callCmd.InParallelWith; + } + } + else + { + Dictionary domainNameToExpr = new Dictionary(); + foreach (var domainName in linearDomains.Keys) + { + domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); + } + foreach (Variable v in availableLinearVars[callCmd]) + { + var domainName = FindDomainName(v); + var domain = linearDomains[domainName]; + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), + new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + foreach (var domainName in linearDomains.Keys) + { + callCmd.Ins.Add(domainNameToExpr[domainName]); + } + } + } + else if (cmd is YieldCmd) + { + AddDisjointnessExpr(newCmds, cmd, domainNameToInputVar); + } + } + b.Cmds = newCmds; + } + + { + // Loops + impl.PruneUnreachableBlocks(); + impl.ComputePredecessorsForBlocks(); + GraphUtil.Graph g = Program.GraphFromImpl(impl); + g.ComputeLoops(); + if (g.Reducible) + { + foreach (Block header in g.Headers) + { + List newCmds = new List(); + AddDisjointnessExpr(newCmds, header, domainNameToInputVar); + newCmds.AddRange(header.Cmds); + header.Cmds = newCmds; + } + } + } + } + + foreach (var decl in program.TopLevelDeclarations) + { + Procedure proc = decl as Procedure; + if (proc == null) continue; + + Dictionary> domainNameToInputScope = new Dictionary>(); + Dictionary> domainNameToOutputScope = new Dictionary>(); + foreach (var domainName in linearDomains.Keys) + { + domainNameToInputScope[domainName] = new HashSet(); + domainNameToOutputScope[domainName] = new HashSet(); + + } + foreach (Variable v in globalVarToDomainName.Keys) + { + var domainName = globalVarToDomainName[v]; + domainNameToInputScope[domainName].Add(v); + domainNameToOutputScope[domainName].Add(v); + } + foreach (Variable v in proc.InParams) + { + var domainName = FindDomainName(v); + if (domainName == null) continue; + domainNameToInputScope[domainName].Add(v); + } + foreach (Variable v in proc.OutParams) + { + var domainName = FindDomainName(v); + if (domainName == null) continue; + domainNameToOutputScope[domainName].Add(v); + } + foreach (var domainName in linearDomains.Keys) + { + proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName]))); + var domain = linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); + proc.InParams.Add(f); + domainNameToOutputScope[domainName].Add(f); + proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName]))); + } + } + + foreach (LinearDomain domain in linearDomains.Values) + { + program.TopLevelDeclarations.Add(domain.mapConstBool); + program.TopLevelDeclarations.Add(domain.mapConstInt); + program.TopLevelDeclarations.Add(domain.mapEqInt); + program.TopLevelDeclarations.Add(domain.mapImpBool); + program.TopLevelDeclarations.Add(domain.mapOrBool); + foreach (Axiom axiom in domain.axioms) + { + program.TopLevelDeclarations.Add(axiom); + } + } + + //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; + //CommandLineOptions.Clo.PrintUnstructured = 1; + //PrintBplFile("lsd.bpl", program, false, false); + //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; + } + + public Expr Singleton(Expr e, string domainName) + { + var domain = linearDomains[domainName]; + return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }), e, Expr.True); + } + + List MkExprs(params Expr[] args) + { + return new List(args); + } + + public Expr DisjointnessExpr(string domainName, HashSet scope) + { + LinearDomain domain = linearDomains[domainName]; + BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List(), new List { domain.elementType }, Microsoft.Boogie.Type.Int))); + Expr disjointExpr = Expr.True; + int count = 0; + foreach (Variable v in scope) + { + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } ); + e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List { new IdentifierExpr(Token.NoToken, partition), e } ); + e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } ); + e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.True })); + disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr); + } + var expr = new ExistsExpr(Token.NoToken, new List { partition }, disjointExpr); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + return expr; + } + } + + public class LinearDomain + { + public Microsoft.Boogie.Type elementType; + public Function mapEqInt; + public Function mapConstInt; + public Function mapOrBool; + public Function mapImpBool; + public Function mapConstBool; + public List axioms; + + public LinearDomain(Program program, string domainName, Type elementType) + { + this.elementType = elementType; + this.axioms = new List(); + + MapType mapTypeBool = new MapType(Token.NoToken, new List(), new List { this.elementType }, Type.Bool); + MapType mapTypeInt = new MapType(Token.NoToken, new List(), new List { this.elementType }, Type.Int); + this.mapOrBool = new Function(Token.NoToken, "linear_" + domainName + "_MapOr", + new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true), + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) }, + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); + if (CommandLineOptions.Clo.UseArrayTheory) + { + this.mapOrBool.AddAttribute("builtin", "MapOr"); + } + else + { + BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool)); + IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool)); + IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); + BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); + IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List { aie, bie } ); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie } ); + var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or, + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie } ), + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie} )); + var axiomExpr = new ForallExpr(Token.NoToken, new List(), new List { a, b }, null, + new Trigger(Token.NoToken, true, new List { mapApplTerm }), + new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); + axiomExpr.Typecheck(new TypecheckingContext(null)); + axioms.Add(new Axiom(Token.NoToken, axiomExpr)); + } + + this.mapImpBool = new Function(Token.NoToken, "linear_" + domainName + "_MapImp", + new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true), + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) }, + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); + if (CommandLineOptions.Clo.UseArrayTheory) + { + this.mapImpBool.AddAttribute("builtin", "MapImp"); + } + else + { + BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool)); + IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool)); + IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); + BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); + IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List { aie, bie }); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); + var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp, + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie }), + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie })); + var axiomExpr = new ForallExpr(Token.NoToken, new List(), new List { a, b }, null, + new Trigger(Token.NoToken, true, new List { mapApplTerm }), + new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); + axiomExpr.Typecheck(new TypecheckingContext(null)); + axioms.Add(new Axiom(Token.NoToken, axiomExpr)); + } + + this.mapConstBool = new Function(Token.NoToken, "linear_" + domainName + "_MapConstBool", + new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true) }, + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); + if (CommandLineOptions.Clo.UseArrayTheory) + { + this.mapConstBool.AddAttribute("builtin", "MapConst"); + } + else + { + BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); + IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), + new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.True }), xie }); + var trueAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, trueTerm); + trueAxiomExpr.Typecheck(new TypecheckingContext(null)); + axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr)); + var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), + new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.False }), xie }); + var falseAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm)); + falseAxiomExpr.Typecheck(new TypecheckingContext(null)); + axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr)); + } + + this.mapEqInt = new Function(Token.NoToken, "linear_" + domainName + "_MapEq", + new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true), + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true) }, + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); + if (CommandLineOptions.Clo.UseArrayTheory) + { + this.mapEqInt.AddAttribute("builtin", "MapEq"); + } + else + { + BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt)); + IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt)); + IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); + BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); + IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List { aie, bie }); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); + var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq, + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie }), + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie })); + var axiomExpr = new ForallExpr(Token.NoToken, new List(), new List { a, b }, null, + new Trigger(Token.NoToken, true, new List { mapApplTerm }), + new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); + axiomExpr.Typecheck(new TypecheckingContext(null)); + axioms.Add(new Axiom(Token.NoToken, axiomExpr)); + } + + this.mapConstInt = new Function(Token.NoToken, "linear_" + domainName + "_MapConstInt", + new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true) }, + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false)); + if (CommandLineOptions.Clo.UseArrayTheory) + { + this.mapConstInt.AddAttribute("builtin", "MapConst"); + } + else + { + BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int)); + IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); + BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); + IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List { aie }), xie }); + var axiomExpr = new ForallExpr(Token.NoToken, new List { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie)); + axiomExpr.Typecheck(new TypecheckingContext(null)); + axioms.Add(new Axiom(Token.NoToken, axiomExpr)); + } + + foreach (var axiom in axioms) + { + axiom.Expr.Resolve(new ResolutionContext(null)); + axiom.Expr.Typecheck(new TypecheckingContext(null)); + } + } + } +} diff --git a/Source/Concurrency/MoverChecking.cs b/Source/Concurrency/MoverChecking.cs new file mode 100644 index 00000000..aeea3947 --- /dev/null +++ b/Source/Concurrency/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/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs new file mode 100644 index 00000000..4f0c7a4b --- /dev/null +++ b/Source/Concurrency/OwickiGries.cs @@ -0,0 +1,738 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; +using System.Diagnostics; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie +{ + public class OwickiGriesTransform + { + List globalMods; + LinearTypeChecker linearTypeChecker; + Dictionary asyncAndParallelCallDesugarings; + List yieldCheckerProcs; + List yieldCheckerImpls; + Procedure yieldProc; + + public OwickiGriesTransform(LinearTypeChecker linearTypeChecker) + { + this.linearTypeChecker = linearTypeChecker; + Program program = linearTypeChecker.program; + globalMods = new List(); + foreach (Variable g in program.GlobalVariables()) + { + globalMods.Add(new IdentifierExpr(Token.NoToken, g)); + } + asyncAndParallelCallDesugarings = new Dictionary(); + yieldCheckerProcs = new List(); + yieldCheckerImpls = new List(); + yieldProc = null; + } + + private void AddCallToYieldProc(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) + { + List exprSeq = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName])); + } + foreach (IdentifierExpr ie in globalMods) + { + exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl])); + } + if (yieldProc == null) + { + List inputs = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + var domain = linearTypeChecker.linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); + inputs.Add(f); + } + foreach (IdentifierExpr ie in globalMods) + { + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); + inputs.Add(f); + } + yieldProc = new Procedure(Token.NoToken, "og_yield", new List(), inputs, new List(), new List(), new List(), new List()); + yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + } + CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); + yieldCallCmd.Proc = yieldProc; + newCmds.Add(yieldCallCmd); + } + + private Dictionary ComputeAvailableExprs(HashSet availableLinearVars, Dictionary domainNameToInputVar) + { + Dictionary domainNameToExpr = new Dictionary(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + foreach (Variable v in availableLinearVars) + { + var domainName = linearTypeChecker.FindDomainName(v); + var domain = linearTypeChecker.linearDomains[domainName]; + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + return domainNameToExpr; + } + + private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) + { + List lhss = new List(); + List rhss = new List(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(new IdentifierExpr(Token.NoToken, g)); + } + if (lhss.Count > 0) + { + newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); + } + } + + private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) + { + AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); + + if (globalMods.Count > 0) + { + newCmds.Add(new HavocCmd(Token.NoToken, globalMods)); + } + Dictionary domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[yieldCmd], domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + + for (int j = 0; j < cmds.Count; j++) + { + PredicateCmd predCmd = (PredicateCmd)cmds[j]; + newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr)); + } + } + + public Procedure DesugarParallelCallCmd(CallCmd callCmd, out List ins, out List outs) + { + List parallelCalleeNames = new List(); + CallCmd iter = callCmd; + ins = new List(); + outs = new List(); + while (iter != null) + { + parallelCalleeNames.Add(iter.Proc.Name); + ins.AddRange(iter.Ins); + outs.AddRange(iter.Outs); + iter = iter.InParallelWith; + } + parallelCalleeNames.Sort(); + string procName = "og"; + foreach (string calleeName in parallelCalleeNames) + { + procName = procName + "_" + calleeName; + } + if (asyncAndParallelCallDesugarings.ContainsKey(procName)) + return asyncAndParallelCallDesugarings[procName]; + + List inParams = new List(); + List outParams = new List(); + List requiresSeq = new List(); + List ensuresSeq = new List(); + int count = 0; + while (callCmd != null) + { + Dictionary map = new Dictionary(); + foreach (Variable x in callCmd.Proc.InParams) + { + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); + inParams.Add(y); + map[x] = new IdentifierExpr(Token.NoToken, y); + } + foreach (Variable x in callCmd.Proc.OutParams) + { + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false); + outParams.Add(y); + map[x] = new IdentifierExpr(Token.NoToken, y); + } + Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (Requires req in callCmd.Proc.Requires) + { + requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition))); + } + foreach (Ensures ens in callCmd.Proc.Ensures) + { + ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition))); + } + count++; + callCmd = callCmd.InParallelWith; + } + + Procedure proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, new List(), ensuresSeq); + proc.AddAttribute("yields"); + asyncAndParallelCallDesugarings[procName] = proc; + return proc; + } + + private void CreateYieldCheckerImpl(DeclWithFormals decl, List> yields, Dictionary map) + { + if (yields.Count == 0) return; + + Program program = linearTypeChecker.program; + List locals = new List(); + List inputs = new List(); + foreach (IdentifierExpr ie in map.Values) + { + locals.Add(ie.Decl); + } + for (int i = 0; i < decl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable inParam = decl.InParams[i]; + Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); + locals.Add(copy); + map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); + } + { + int i = decl.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = decl.InParams[i]; + Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); + inputs.Add(copy); + map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); + i++; + } + } + for (int i = 0; i < decl.OutParams.Count; i++) + { + Variable outParam = decl.OutParams[i]; + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); + locals.Add(copy); + map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy); + } + Dictionary ogOldLocalMap = new Dictionary(); + Dictionary assumeMap = new Dictionary(map); + foreach (IdentifierExpr ie in globalMods) + { + Variable g = ie.Decl; + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type)); + locals.Add(copy); + ogOldLocalMap[g] = Expr.Ident(copy); + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true); + inputs.Add(f); + assumeMap[g] = Expr.Ident(f); + } + + Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap); + Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + List yieldCheckerBlocks = new List(); + List labels = new List(); + List labelTargets = new List(); + Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + int yieldCount = 0; + foreach (List cs in yields) + { + var linearDomains = linearTypeChecker.linearDomains; + List newCmds = new List(); + foreach (Cmd cmd in cs) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr))); + } + foreach (Cmd cmd in cs) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr); + if (predCmd is AssertCmd) + newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes)); + else + newCmds.Add(new AssumeCmd(Token.NoToken, newExpr)); + } + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + } + yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List(), new GotoCmd(Token.NoToken, labels, labelTargets))); + + // Create the yield checker procedure + var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name); + var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List(), new List(), new List(), new List()); + yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerProcs.Add(yieldCheckerProc); + + // Create the yield checker implementation + var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks); + yieldCheckerImpl.Proc = yieldCheckerProc; + yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerImpls.Add(yieldCheckerImpl); + } + + private bool IsYieldingHeader(GraphUtil.Graph graph, Block header) + { + foreach (Block backEdgeNode in graph.BackEdgeNodes(header)) + { + foreach (Block x in graph.NaturalLoops(header, backEdgeNode)) + { + foreach (Cmd cmd in x.Cmds) + { + if (cmd is YieldCmd) + return true; + CallCmd callCmd = cmd as CallCmd; + if (callCmd == null) continue; + if (callCmd.IsAsync || callCmd.InParallelWith != null || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + return true; + } + } + } + return false; + } + + private void TransformImpl(Implementation impl) + { + if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return; + + TransformProc(impl.Proc); + + // Find the yielding loop headers + impl.PruneUnreachableBlocks(); + impl.ComputePredecessorsForBlocks(); + GraphUtil.Graph graph = Program.GraphFromImpl(impl); + graph.ComputeLoops(); + if (!graph.Reducible) + { + throw new Exception("Irreducible flow graphs are unsupported."); + } + HashSet yieldingHeaders = new HashSet(); + IEnumerable sortedHeaders = graph.SortHeadersByDominance(); + foreach (Block header in sortedHeaders) + { + if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header))) + { + yieldingHeaders.Add(header); + } + else if (IsYieldingHeader(graph, header)) + { + yieldingHeaders.Add(header); + } + else + { + continue; + } + } + + Program program = linearTypeChecker.program; + Dictionary map = new Dictionary(); + foreach (Variable local in impl.LocVars) + { + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); + map[local] = new IdentifierExpr(Token.NoToken, copy); + } + Dictionary ogOldGlobalMap = new Dictionary(); + foreach (IdentifierExpr ie in globalMods) + { + Variable g = ie.Decl; + LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type)); + ogOldGlobalMap[g] = l; + impl.LocVars.Add(l); + } + Dictionary domainNameToInputVar = new Dictionary(); + Dictionary domainNameToLocalVar = new Dictionary(); + { + int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = impl.InParams[i]; + domainNameToInputVar[domainName] = inParam; + Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type)); + domainNameToLocalVar[domainName] = l; + impl.LocVars.Add(l); + i++; + } + } + + // Collect the yield predicates and desugar yields + List> yields = new List>(); + List cmds = new List(); + foreach (Block b in impl.Blocks) + { + YieldCmd yieldCmd = null; + List newCmds = new List(); + for (int i = 0; i < b.Cmds.Count; i++) + { + Cmd cmd = b.Cmds[i]; + if (cmd is YieldCmd) + { + yieldCmd = (YieldCmd)cmd; + continue; + } + if (yieldCmd != null) + { + PredicateCmd pcmd = cmd as PredicateCmd; + if (pcmd == null) + { + DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); + if (cmds.Count > 0) + { + yields.Add(cmds); + cmds = new List(); + } + yieldCmd = null; + } + else + { + cmds.Add(pcmd); + } + } + CallCmd callCmd = cmd as CallCmd; + if (callCmd != null) + { + if (callCmd.InParallelWith != null || callCmd.IsAsync || + QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + { + AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); + } + if (callCmd.InParallelWith != null) + { + List ins; + List outs; + Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs); + CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs); + dummyCallCmd.Proc = dummyParallelCallDesugaring; + newCmds.Add(dummyCallCmd); + } + else if (callCmd.IsAsync) + { + if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) + { + asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List(), new List()); + } + var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name]; + CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs); + dummyCallCmd.Proc = dummyAsyncTargetProc; + newCmds.Add(dummyCallCmd); + } + else + { + newCmds.Add(callCmd); + } + if (callCmd.InParallelWith != null || callCmd.IsAsync || + QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + { + HashSet availableLinearVars = new HashSet(linearTypeChecker.availableLinearVars[callCmd]); + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue; + availableLinearVars.Add(ie.Decl); + } + Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + } + else + { + newCmds.Add(cmd); + } + } + if (yieldCmd != null) + { + DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); + if (cmds.Count > 0) + { + yields.Add(cmds); + cmds = new List(); + } + } + if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) + { + AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); + } + b.Cmds = newCmds; + } + + foreach (Block header in yieldingHeaders) + { + Dictionary domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[header], domainNameToInputVar); + foreach (Block pred in header.Predecessors) + { + AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); + AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + List newCmds = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName]))); + } + foreach (Variable v in ogOldGlobalMap.Keys) + { + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v])))); + } + newCmds.AddRange(header.Cmds); + header.Cmds = newCmds; + } + + { + // Add initial block + List lhss = new List(); + List rhss = new List(); + Dictionary domainNameToExpr = new Dictionary(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); + } + for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable v = impl.InParams[i]; + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + var domain = linearTypeChecker.linearDomains[domainName]; + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(Expr.Ident(g)); + } + if (lhss.Count > 0) + { + Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); + impl.Blocks.Insert(0, initBlock); + } + } + + CreateYieldCheckerImpl(impl, yields, map); + } + + public void TransformProc(Procedure proc) + { + if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return; + + Program program = linearTypeChecker.program; + Dictionary domainNameToInputVar = new Dictionary(); + { + int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = proc.InParams[i]; + domainNameToInputVar[domainName] = inParam; + i++; + } + } + + // Collect the yield predicates and desugar yields + List> yields = new List>(); + List cmds = new List(); + if (proc.Requires.Count > 0) + { + Dictionary> domainNameToScope = new Dictionary>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToScope[domainName] = new HashSet(); + domainNameToScope[domainName].Add(domainNameToInputVar[domainName]); + } + foreach (Variable v in program.GlobalVariables()) + { + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + domainNameToScope[domainName].Add(v); + } + for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable v = proc.InParams[i]; + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + domainNameToScope[domainName].Add(v); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName]))); + } + foreach (Requires r in proc.Requires) + { + if (r.Free) + { + cmds.Add(new AssumeCmd(r.tok, r.Condition)); + } + else + { + cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes)); + } + } + yields.Add(cmds); + cmds = new List(); + } + if (proc.Ensures.Count > 0) + { + Dictionary> domainNameToScope = new Dictionary>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToScope[domainName] = new HashSet(); + domainNameToScope[domainName].Add(domainNameToInputVar[domainName]); + } + foreach (Variable v in program.GlobalVariables()) + { + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + domainNameToScope[domainName].Add(v); + } + for (int i = 0; i < proc.OutParams.Count; i++) + { + Variable v = proc.OutParams[i]; + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + domainNameToScope[domainName].Add(v); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName]))); + } + foreach (Ensures e in proc.Ensures) + { + if (e.Free) + { + cmds.Add(new AssumeCmd(e.tok, e.Condition)); + } + else + { + cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes)); + } + } + yields.Add(cmds); + cmds = new List(); + } + CreateYieldCheckerImpl(proc, yields, new Dictionary()); + } + + private void AddYieldProcAndImpl() + { + if (yieldProc == null) return; + + Program program = linearTypeChecker.program; + List inputs = new List(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + var domain = linearTypeChecker.linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); + inputs.Add(f); + } + foreach (IdentifierExpr ie in globalMods) + { + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); + inputs.Add(f); + } + List blocks = new List(); + TransferCmd transferCmd = new ReturnCmd(Token.NoToken); + if (yieldCheckerProcs.Count > 0) + { + List blockTargets = new List(); + List labelTargets = new List(); + int labelCount = 0; + foreach (Procedure proc in yieldCheckerProcs) + { + List exprSeq = new List(); + foreach (Variable v in inputs) + { + exprSeq.Add(new IdentifierExpr(Token.NoToken, v)); + } + CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); + callCmd.Proc = proc; + string label = string.Format("L_{0}", labelCount++); + Block block = new Block(Token.NoToken, label, new List { callCmd }, new ReturnCmd(Token.NoToken)); + labelTargets.Add(label); + blockTargets.Add(block); + blocks.Add(block); + } + transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets); + } + blocks.Insert(0, new Block(Token.NoToken, "enter", new List(), transferCmd)); + + var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List(), inputs, new List(), new List(), blocks); + yieldImpl.Proc = yieldProc; + yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + program.TopLevelDeclarations.Add(yieldProc); + program.TopLevelDeclarations.Add(yieldImpl); + } + + private QKeyValue RemoveYieldsAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveYieldsAttribute(iter.Next); + return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter; + } + + public void Transform() + { + MoverChecking.AddCheckers(linearTypeChecker); + + Program program = linearTypeChecker.program; + foreach (var decl in program.TopLevelDeclarations) + { + Implementation impl = decl as Implementation; + if (impl == null) continue; + TransformImpl(impl); + } + foreach (Procedure proc in yieldCheckerProcs) + { + program.TopLevelDeclarations.Add(proc); + } + foreach (Implementation impl in yieldCheckerImpls) + { + program.TopLevelDeclarations.Add(impl); + } + foreach (Procedure proc in asyncAndParallelCallDesugarings.Values) + { + program.TopLevelDeclarations.Add(proc); + } + AddYieldProcAndImpl(); + foreach (var decl in program.TopLevelDeclarations) + { + Procedure proc = decl as Procedure; + if (proc == null) continue; + if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) + { + HashSet modifiedVars = new HashSet(); + proc.Modifies.Iter(x => modifiedVars.Add(x.Decl)); + foreach (GlobalVariable g in program.GlobalVariables()) + { + if (modifiedVars.Contains(g)) continue; + proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g)); + } + proc.Attributes = RemoveYieldsAttribute(proc.Attributes); + } + } + foreach (var decl in program.TopLevelDeclarations) + { + Implementation impl = decl as Implementation; + if (impl == null) continue; + impl.Attributes = RemoveYieldsAttribute(impl.Attributes); + } + } + } +} diff --git a/Source/Concurrency/Properties/AssemblyInfo.cs b/Source/Concurrency/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..48430488 --- /dev/null +++ b/Source/Concurrency/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("Concurrency")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("")] +[assembly: AssemblyProduct("Concurrency")] +[assembly: AssemblyCopyright("Copyright © 2013")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("867039c5-87dc-4f76-9f90-4f52afc90116")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 03eefccd..f71144d5 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -156,17 +156,14 @@ - - - diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs deleted file mode 100644 index 51f7f328..00000000 --- a/Source/Core/LinearSets.cs +++ /dev/null @@ -1,757 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Threading.Tasks; -using Microsoft.Boogie; - -namespace Microsoft.Boogie -{ - public class LinearEraser : StandardVisitor - { - private QKeyValue RemoveLinearAttribute(QKeyValue iter) - { - if (iter == null) return null; - iter.Next = RemoveLinearAttribute(iter.Next); - return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next; - } - - public override Variable VisitVariable(Variable node) - { - node.Attributes = RemoveLinearAttribute(node.Attributes); - return base.VisitVariable(node); - } - } - - public class LinearTypeChecker : StandardVisitor - { - public Program program; - public int errorCount; - public CheckingContext checkingContext; - public Dictionary domainNameToType; - public Dictionary> availableLinearVars; - public Dictionary inoutParamToDomainName; - public Dictionary varToDomainName; - public Dictionary globalVarToDomainName; - public Dictionary linearDomains; - - public LinearTypeChecker(Program program) - { - this.program = program; - this.errorCount = 0; - this.checkingContext = new CheckingContext(null); - this.domainNameToType = new Dictionary(); - this.parallelCallInvars = new HashSet(); - this.availableLinearVars = new Dictionary>(); - this.inoutParamToDomainName = new Dictionary(); - this.varToDomainName = new Dictionary(); - this.linearDomains = new Dictionary(); - } - public void Typecheck() - { - this.VisitProgram(program); - foreach (string domainName in domainNameToType.Keys) - { - this.linearDomains[domainName] = new LinearDomain(program, domainName, domainNameToType[domainName]); - } - } - private void Error(Absy node, string message) - { - checkingContext.Error(node, message); - errorCount++; - } - public override Program VisitProgram(Program node) - { - globalVarToDomainName = new Dictionary(); - foreach (GlobalVariable g in program.GlobalVariables()) - { - string domainName = FindDomainName(g); - if (domainName != null) - { - globalVarToDomainName[g] = domainName; - } - } - return base.VisitProgram(node); - } - public override Implementation VisitImplementation(Implementation node) - { - HashSet start = new HashSet(globalVarToDomainName.Keys); - for (int i = 0; i < node.InParams.Count; i++) - { - string domainName = FindDomainName(node.Proc.InParams[i]); - if (domainName != null) - { - inoutParamToDomainName[node.InParams[i]] = domainName; - start.Add(node.InParams[i]); - } - } - for (int i = 0; i < node.OutParams.Count; i++) - { - string domainName = FindDomainName(node.Proc.OutParams[i]); - if (domainName != null) - { - inoutParamToDomainName[node.OutParams[i]] = domainName; - } - } - - var oldErrorCount = this.errorCount; - var impl = base.VisitImplementation(node); - if (oldErrorCount < this.errorCount) - return impl; - - Stack dfsStack = new Stack(); - HashSet dfsStackAsSet = new HashSet(); - availableLinearVars[node.Blocks[0]] = start; - dfsStack.Push(node.Blocks[0]); - dfsStackAsSet.Add(node.Blocks[0]); - while (dfsStack.Count > 0) - { - Block b = dfsStack.Pop(); - dfsStackAsSet.Remove(b); - HashSet end = PropagateAvailableLinearVarsAcrossBlock(b); - if (b.TransferCmd is ReturnCmd) - { - foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end)) - { - Error(b, string.Format("Global variable {0} must be available at a return", g.Name)); - } - foreach (Variable v in node.OutParams) - { - if (FindDomainName(v) == null || end.Contains(v)) continue; - Error(b, string.Format("Output variable {0} must be available at a return", v.Name)); - } - continue; - } - GotoCmd gotoCmd = b.TransferCmd as GotoCmd; - foreach (Block target in gotoCmd.labelTargets) - { - if (!availableLinearVars.ContainsKey(target)) - { - availableLinearVars[target] = new HashSet(end); - dfsStack.Push(target); - dfsStackAsSet.Add(target); - } - else - { - var savedAvailableVars = new HashSet(availableLinearVars[target]); - availableLinearVars[target].IntersectWith(end); - if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target)) - { - dfsStack.Push(target); - dfsStackAsSet.Add(target); - } - } - } - } - return impl; - } - private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) { - HashSet start = new HashSet(availableLinearVars[b]); - foreach (Cmd cmd in b.Cmds) - { - if (cmd is AssignCmd) - { - AssignCmd assignCmd = (AssignCmd)cmd; - for (int i = 0; i < assignCmd.Lhss.Count; i++) - { - if (FindDomainName(assignCmd.Lhss[i].DeepAssignedVariable) == null) continue; - IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr; - if (start.Contains(ie.Decl)) - { - start.Remove(ie.Decl); - } - else - { - Error(ie, "unavailable source for a linear read"); - } - } - foreach (AssignLhs assignLhs in assignCmd.Lhss) - { - if (FindDomainName(assignLhs.DeepAssignedVariable) == null) continue; - start.Add(assignLhs.DeepAssignedVariable); - } - } - else if (cmd is CallCmd) - { - foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) - { - Error(b, string.Format("Global variable {0} must be available at a call", g.Name)); - } - CallCmd callCmd = (CallCmd)cmd; - while (callCmd != null) - { - for (int i = 0; i < callCmd.Proc.InParams.Count; i++) - { - if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue; - IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr; - if (start.Contains(ie.Decl)) - { - start.Remove(ie.Decl); - } - else - { - Error(ie, "unavailable source for a linear read"); - } - } - callCmd = callCmd.InParallelWith; - } - callCmd = (CallCmd)cmd; - availableLinearVars[callCmd] = new HashSet(start); - while (callCmd != null) - { - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (FindDomainName(ie.Decl) == null) continue; - start.Add(ie.Decl); - } - callCmd = callCmd.InParallelWith; - } - } - else if (cmd is HavocCmd) - { - HavocCmd havocCmd = (HavocCmd) cmd; - foreach (IdentifierExpr ie in havocCmd.Vars) - { - if (FindDomainName(ie.Decl) == null) continue; - start.Remove(ie.Decl); - } - } - else if (cmd is YieldCmd) - { - foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) - { - Error(b, string.Format("Global variable {0} must be available at a yield", g.Name)); - } - availableLinearVars[cmd] = new HashSet(start); - } - } - return start; - } - public string FindDomainName(Variable v) - { - if (globalVarToDomainName.ContainsKey(v)) - return globalVarToDomainName[v]; - if (inoutParamToDomainName.ContainsKey(v)) - return inoutParamToDomainName[v]; - return QKeyValue.FindStringAttribute(v.Attributes, "linear"); - } - public override Variable VisitVariable(Variable node) - { - string domainName = FindDomainName(node); - if (domainName != null) - { - Type type = node.TypedIdent.Type; - MapType mapType = type as MapType; - if (mapType != null) - { - if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool)) - { - type = mapType.Arguments[0]; - if (type is MapType) - { - Error(node, "the domain of a linear set must be a scalar type"); - return base.VisitVariable(node); - } - } - else - { - Error(node, "a linear domain can be attached to either a set or a scalar type"); - return base.VisitVariable(node); - } - } - if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type)) - { - Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName)); - } - else - { - domainNameToType[domainName] = type; - } - } - return base.VisitVariable(node); - } - public override Cmd VisitAssignCmd(AssignCmd node) - { - HashSet rhsVars = new HashSet(); - for (int i = 0; i < node.Lhss.Count; i++) - { - AssignLhs lhs = node.Lhss[i]; - Variable lhsVar = lhs.DeepAssignedVariable; - string domainName = FindDomainName(lhsVar); - if (domainName == null) continue; - SimpleAssignLhs salhs = lhs as SimpleAssignLhs; - if (salhs == null) - { - Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name)); - continue; - } - IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr; - if (rhs == null) - { - Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name)); - continue; - } - string rhsDomainName = FindDomainName(rhs.Decl); - if (rhsDomainName == null) - { - Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name)); - continue; - } - if (domainName != rhsDomainName) - { - Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName)); - continue; - } - if (rhsVars.Contains(rhs.Decl)) - { - Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name)); - continue; - } - rhsVars.Add(rhs.Decl); - } - return base.VisitAssignCmd(node); - } - HashSet parallelCallInvars; - public override Cmd VisitCallCmd(CallCmd node) - { - HashSet inVars = new HashSet(); - for (int i = 0; i < node.Proc.InParams.Count; i++) - { - Variable formal = node.Proc.InParams[i]; - string domainName = FindDomainName(formal); - if (domainName == null) continue; - IdentifierExpr actual = node.Ins[i] as IdentifierExpr; - if (actual == null) - { - Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name)); - continue; - } - string actualDomainName = FindDomainName(actual.Decl); - if (actualDomainName == null) - { - Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name)); - continue; - } - if (domainName != actualDomainName) - { - Error(node, "The domains of formal and actual parameters must be the same"); - continue; - } - if (parallelCallInvars.Contains(actual.Decl)) - { - Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name)); - continue; - } - if (actual.Decl is GlobalVariable) - { - Error(node, "Only local linear variable can be an actual input parameter of a procedure call"); - continue; - } - inVars.Add(actual.Decl); - parallelCallInvars.Add(actual.Decl); - } - for (int i = 0; i < node.Proc.OutParams.Count; i++) - { - IdentifierExpr actual = node.Outs[i]; - string actualDomainName = FindDomainName(actual.Decl); - if (actualDomainName == null) continue; - Variable formal = node.Proc.OutParams[i]; - string domainName = FindDomainName(formal); - if (domainName == null) - { - Error(node, "Only a linear variable can be passed to a linear parameter"); - continue; - } - if (domainName != actualDomainName) - { - Error(node, "The domains of formal and actual parameters must be the same"); - continue; - } - if (actual.Decl is GlobalVariable) - { - Error(node, "Only local linear variable can be actual output parameter of a procedure call"); - continue; - } - } - if (node.InParallelWith != null) - { - VisitCallCmd(node.InParallelWith); - } - foreach (Variable v in inVars) - { - parallelCallInvars.Remove(v); - } - return base.VisitCallCmd(node); - } - - private void AddDisjointnessExpr(List newCmds, Absy absy, Dictionary domainNameToInputVar) - { - Dictionary> domainNameToScope = new Dictionary>(); - foreach (var domainName in linearDomains.Keys) - { - domainNameToScope[domainName] = new HashSet(); - domainNameToScope[domainName].Add(domainNameToInputVar[domainName]); - } - foreach (Variable v in availableLinearVars[absy]) - { - var domainName = FindDomainName(v); - domainNameToScope[domainName].Add(v); - } - foreach (string domainName in linearDomains.Keys) - { - newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName]))); - } - } - - public void Transform() - { - foreach (var decl in program.TopLevelDeclarations) - { - Implementation impl = decl as Implementation; - if (impl == null) continue; - Dictionary domainNameToInputVar = new Dictionary(); - foreach (string domainName in linearDomains.Keys) - { - var domain = linearDomains[domainName]; - Formal f = new Formal( - Token.NoToken, - new TypedIdent(Token.NoToken, - "linear_" + domainName + "_in", - new MapType(Token.NoToken, new List(), - new List { domain.elementType }, Type.Bool)), true); - impl.InParams.Add(f); - domainNameToInputVar[domainName] = f; - } - - foreach (Block b in impl.Blocks) - { - List newCmds = new List(); - for (int i = 0; i < b.Cmds.Count; i++) - { - Cmd cmd = b.Cmds[i]; - newCmds.Add(cmd); - if (cmd is CallCmd) - { - CallCmd callCmd = cmd as CallCmd; - if (callCmd.IsAsync) - { - foreach (var domainName in linearDomains.Keys) - { - var domain = linearDomains[domainName]; - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - callCmd.Ins.Add(expr); - } - } - else if (callCmd.InParallelWith != null) - { - while (callCmd != null) - { - foreach (var domainName in linearDomains.Keys) - { - var domain = linearDomains[domainName]; - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - callCmd.Ins.Add(expr); - } - callCmd = callCmd.InParallelWith; - } - } - else - { - Dictionary domainNameToExpr = new Dictionary(); - foreach (var domainName in linearDomains.Keys) - { - domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); - } - foreach (Variable v in availableLinearVars[callCmd]) - { - var domainName = FindDomainName(v); - var domain = linearDomains[domainName]; - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), - new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - domainNameToExpr[domainName] = expr; - } - foreach (var domainName in linearDomains.Keys) - { - callCmd.Ins.Add(domainNameToExpr[domainName]); - } - } - } - else if (cmd is YieldCmd) - { - AddDisjointnessExpr(newCmds, cmd, domainNameToInputVar); - } - } - b.Cmds = newCmds; - } - - { - // Loops - impl.PruneUnreachableBlocks(); - impl.ComputePredecessorsForBlocks(); - GraphUtil.Graph g = Program.GraphFromImpl(impl); - g.ComputeLoops(); - if (g.Reducible) - { - foreach (Block header in g.Headers) - { - List newCmds = new List(); - AddDisjointnessExpr(newCmds, header, domainNameToInputVar); - newCmds.AddRange(header.Cmds); - header.Cmds = newCmds; - } - } - } - } - - foreach (var decl in program.TopLevelDeclarations) - { - Procedure proc = decl as Procedure; - if (proc == null) continue; - - Dictionary> domainNameToInputScope = new Dictionary>(); - Dictionary> domainNameToOutputScope = new Dictionary>(); - foreach (var domainName in linearDomains.Keys) - { - domainNameToInputScope[domainName] = new HashSet(); - domainNameToOutputScope[domainName] = new HashSet(); - - } - foreach (Variable v in globalVarToDomainName.Keys) - { - var domainName = globalVarToDomainName[v]; - domainNameToInputScope[domainName].Add(v); - domainNameToOutputScope[domainName].Add(v); - } - foreach (Variable v in proc.InParams) - { - var domainName = FindDomainName(v); - if (domainName == null) continue; - domainNameToInputScope[domainName].Add(v); - } - foreach (Variable v in proc.OutParams) - { - var domainName = FindDomainName(v); - if (domainName == null) continue; - domainNameToOutputScope[domainName].Add(v); - } - foreach (var domainName in linearDomains.Keys) - { - proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName]))); - var domain = linearDomains[domainName]; - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); - proc.InParams.Add(f); - domainNameToOutputScope[domainName].Add(f); - proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName]))); - } - } - - foreach (LinearDomain domain in linearDomains.Values) - { - program.TopLevelDeclarations.Add(domain.mapConstBool); - program.TopLevelDeclarations.Add(domain.mapConstInt); - program.TopLevelDeclarations.Add(domain.mapEqInt); - program.TopLevelDeclarations.Add(domain.mapImpBool); - program.TopLevelDeclarations.Add(domain.mapOrBool); - foreach (Axiom axiom in domain.axioms) - { - program.TopLevelDeclarations.Add(axiom); - } - } - - //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured; - //CommandLineOptions.Clo.PrintUnstructured = 1; - //PrintBplFile("lsd.bpl", program, false, false); - //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; - } - - public Expr Singleton(Expr e, string domainName) - { - var domain = linearDomains[domainName]; - return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }), e, Expr.True); - } - - List MkExprs(params Expr[] args) - { - return new List(args); - } - - public Expr DisjointnessExpr(string domainName, HashSet scope) - { - LinearDomain domain = linearDomains[domainName]; - BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List(), new List { domain.elementType }, Microsoft.Boogie.Type.Int))); - Expr disjointExpr = Expr.True; - int count = 0; - foreach (Variable v in scope) - { - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } ); - e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List { new IdentifierExpr(Token.NoToken, partition), e } ); - e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } ); - e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.True })); - disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr); - } - var expr = new ExistsExpr(Token.NoToken, new List { partition }, disjointExpr); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - return expr; - } - } - - public class LinearDomain - { - public Microsoft.Boogie.Type elementType; - public Function mapEqInt; - public Function mapConstInt; - public Function mapOrBool; - public Function mapImpBool; - public Function mapConstBool; - public List axioms; - - public LinearDomain(Program program, string domainName, Type elementType) - { - this.elementType = elementType; - this.axioms = new List(); - - MapType mapTypeBool = new MapType(Token.NoToken, new List(), new List { this.elementType }, Type.Bool); - MapType mapTypeInt = new MapType(Token.NoToken, new List(), new List { this.elementType }, Type.Int); - this.mapOrBool = new Function(Token.NoToken, "linear_" + domainName + "_MapOr", - new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true), - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) }, - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); - if (CommandLineOptions.Clo.UseArrayTheory) - { - this.mapOrBool.AddAttribute("builtin", "MapOr"); - } - else - { - BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); - BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool)); - IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); - BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List { aie, bie } ); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie } ); - var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or, - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie } ), - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie} )); - var axiomExpr = new ForallExpr(Token.NoToken, new List(), new List { a, b }, null, - new Trigger(Token.NoToken, true, new List { mapApplTerm }), - new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); - axiomExpr.Typecheck(new TypecheckingContext(null)); - axioms.Add(new Axiom(Token.NoToken, axiomExpr)); - } - - this.mapImpBool = new Function(Token.NoToken, "linear_" + domainName + "_MapImp", - new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true), - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true) }, - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); - if (CommandLineOptions.Clo.UseArrayTheory) - { - this.mapImpBool.AddAttribute("builtin", "MapImp"); - } - else - { - BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); - BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool)); - IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); - BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List { aie, bie }); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); - var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp, - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie }), - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie })); - var axiomExpr = new ForallExpr(Token.NoToken, new List(), new List { a, b }, null, - new Trigger(Token.NoToken, true, new List { mapApplTerm }), - new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); - axiomExpr.Typecheck(new TypecheckingContext(null)); - axioms.Add(new Axiom(Token.NoToken, axiomExpr)); - } - - this.mapConstBool = new Function(Token.NoToken, "linear_" + domainName + "_MapConstBool", - new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true) }, - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); - if (CommandLineOptions.Clo.UseArrayTheory) - { - this.mapConstBool.AddAttribute("builtin", "MapConst"); - } - else - { - BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), - new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.True }), xie }); - var trueAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, trueTerm); - trueAxiomExpr.Typecheck(new TypecheckingContext(null)); - axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr)); - var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), - new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.False }), xie }); - var falseAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm)); - falseAxiomExpr.Typecheck(new TypecheckingContext(null)); - axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr)); - } - - this.mapEqInt = new Function(Token.NoToken, "linear_" + domainName + "_MapEq", - new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true), - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true) }, - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false)); - if (CommandLineOptions.Clo.UseArrayTheory) - { - this.mapEqInt.AddAttribute("builtin", "MapEq"); - } - else - { - BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); - BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt)); - IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); - BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List { aie, bie }); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); - var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq, - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie }), - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie })); - var axiomExpr = new ForallExpr(Token.NoToken, new List(), new List { a, b }, null, - new Trigger(Token.NoToken, true, new List { mapApplTerm }), - new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); - axiomExpr.Typecheck(new TypecheckingContext(null)); - axioms.Add(new Axiom(Token.NoToken, axiomExpr)); - } - - this.mapConstInt = new Function(Token.NoToken, "linear_" + domainName + "_MapConstInt", - new List { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true) }, - new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false)); - if (CommandLineOptions.Clo.UseArrayTheory) - { - this.mapConstInt.AddAttribute("builtin", "MapConst"); - } - else - { - BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int)); - IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); - BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); - IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List { aie }), xie }); - var axiomExpr = new ForallExpr(Token.NoToken, new List { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie)); - axiomExpr.Typecheck(new TypecheckingContext(null)); - axioms.Add(new Axiom(Token.NoToken, axiomExpr)); - } - - foreach (var axiom in axioms) - { - axiom.Expr.Resolve(new ResolutionContext(null)); - axiom.Expr.Typecheck(new TypecheckingContext(null)); - } - } - } -} diff --git a/Source/Core/MoverChecking.cs b/Source/Core/MoverChecking.cs deleted file mode 100644 index aeea3947..00000000 --- a/Source/Core/MoverChecking.cs +++ /dev/null @@ -1,641 +0,0 @@ -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 deleted file mode 100644 index 4f0c7a4b..00000000 --- a/Source/Core/OwickiGries.cs +++ /dev/null @@ -1,738 +0,0 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Threading.Tasks; -using Microsoft.Boogie; -using System.Diagnostics; -using System.Diagnostics.Contracts; - -namespace Microsoft.Boogie -{ - public class OwickiGriesTransform - { - List globalMods; - LinearTypeChecker linearTypeChecker; - Dictionary asyncAndParallelCallDesugarings; - List yieldCheckerProcs; - List yieldCheckerImpls; - Procedure yieldProc; - - public OwickiGriesTransform(LinearTypeChecker linearTypeChecker) - { - this.linearTypeChecker = linearTypeChecker; - Program program = linearTypeChecker.program; - globalMods = new List(); - foreach (Variable g in program.GlobalVariables()) - { - globalMods.Add(new IdentifierExpr(Token.NoToken, g)); - } - asyncAndParallelCallDesugarings = new Dictionary(); - yieldCheckerProcs = new List(); - yieldCheckerImpls = new List(); - yieldProc = null; - } - - private void AddCallToYieldProc(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) - { - List exprSeq = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName])); - } - foreach (IdentifierExpr ie in globalMods) - { - exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl])); - } - if (yieldProc == null) - { - List inputs = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - var domain = linearTypeChecker.linearDomains[domainName]; - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); - inputs.Add(f); - } - foreach (IdentifierExpr ie in globalMods) - { - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); - inputs.Add(f); - } - yieldProc = new Procedure(Token.NoToken, "og_yield", new List(), inputs, new List(), new List(), new List(), new List()); - yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - } - CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); - yieldCallCmd.Proc = yieldProc; - newCmds.Add(yieldCallCmd); - } - - private Dictionary ComputeAvailableExprs(HashSet availableLinearVars, Dictionary domainNameToInputVar) - { - Dictionary domainNameToExpr = new Dictionary(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - domainNameToExpr[domainName] = expr; - } - foreach (Variable v in availableLinearVars) - { - var domainName = linearTypeChecker.FindDomainName(v); - var domain = linearTypeChecker.linearDomains[domainName]; - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - domainNameToExpr[domainName] = expr; - } - return domainNameToExpr; - } - - private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) - { - List lhss = new List(); - List rhss = new List(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]))); - rhss.Add(domainNameToExpr[domainName]); - } - foreach (Variable g in ogOldGlobalMap.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); - rhss.Add(new IdentifierExpr(Token.NoToken, g)); - } - if (lhss.Count > 0) - { - newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); - } - } - - private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) - { - AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); - - if (globalMods.Count > 0) - { - newCmds.Add(new HavocCmd(Token.NoToken, globalMods)); - } - Dictionary domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[yieldCmd], domainNameToInputVar); - AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - - for (int j = 0; j < cmds.Count; j++) - { - PredicateCmd predCmd = (PredicateCmd)cmds[j]; - newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr)); - } - } - - public Procedure DesugarParallelCallCmd(CallCmd callCmd, out List ins, out List outs) - { - List parallelCalleeNames = new List(); - CallCmd iter = callCmd; - ins = new List(); - outs = new List(); - while (iter != null) - { - parallelCalleeNames.Add(iter.Proc.Name); - ins.AddRange(iter.Ins); - outs.AddRange(iter.Outs); - iter = iter.InParallelWith; - } - parallelCalleeNames.Sort(); - string procName = "og"; - foreach (string calleeName in parallelCalleeNames) - { - procName = procName + "_" + calleeName; - } - if (asyncAndParallelCallDesugarings.ContainsKey(procName)) - return asyncAndParallelCallDesugarings[procName]; - - List inParams = new List(); - List outParams = new List(); - List requiresSeq = new List(); - List ensuresSeq = new List(); - int count = 0; - while (callCmd != null) - { - Dictionary map = new Dictionary(); - foreach (Variable x in callCmd.Proc.InParams) - { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); - inParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); - } - foreach (Variable x in callCmd.Proc.OutParams) - { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false); - outParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); - } - Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); - Substitution subst = Substituter.SubstitutionFromHashtable(map); - foreach (Requires req in callCmd.Proc.Requires) - { - requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition))); - } - foreach (Ensures ens in callCmd.Proc.Ensures) - { - ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition))); - } - count++; - callCmd = callCmd.InParallelWith; - } - - Procedure proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, new List(), ensuresSeq); - proc.AddAttribute("yields"); - asyncAndParallelCallDesugarings[procName] = proc; - return proc; - } - - private void CreateYieldCheckerImpl(DeclWithFormals decl, List> yields, Dictionary map) - { - if (yields.Count == 0) return; - - Program program = linearTypeChecker.program; - List locals = new List(); - List inputs = new List(); - foreach (IdentifierExpr ie in map.Values) - { - locals.Add(ie.Decl); - } - for (int i = 0; i < decl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) - { - Variable inParam = decl.InParams[i]; - Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); - locals.Add(copy); - map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); - } - { - int i = decl.InParams.Count - linearTypeChecker.linearDomains.Count; - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - Variable inParam = decl.InParams[i]; - Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); - inputs.Add(copy); - map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy); - i++; - } - } - for (int i = 0; i < decl.OutParams.Count; i++) - { - Variable outParam = decl.OutParams[i]; - var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); - locals.Add(copy); - map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy); - } - Dictionary ogOldLocalMap = new Dictionary(); - Dictionary assumeMap = new Dictionary(map); - foreach (IdentifierExpr ie in globalMods) - { - Variable g = ie.Decl; - var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type)); - locals.Add(copy); - ogOldLocalMap[g] = Expr.Ident(copy); - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true); - inputs.Add(f); - assumeMap[g] = Expr.Ident(f); - } - - Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap); - Substitution subst = Substituter.SubstitutionFromHashtable(map); - List yieldCheckerBlocks = new List(); - List labels = new List(); - List labelTargets = new List(); - Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); - labels.Add(yieldCheckerBlock.Label); - labelTargets.Add(yieldCheckerBlock); - yieldCheckerBlocks.Add(yieldCheckerBlock); - int yieldCount = 0; - foreach (List cs in yields) - { - var linearDomains = linearTypeChecker.linearDomains; - List newCmds = new List(); - foreach (Cmd cmd in cs) - { - PredicateCmd predCmd = (PredicateCmd)cmd; - newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr))); - } - foreach (Cmd cmd in cs) - { - PredicateCmd predCmd = (PredicateCmd)cmd; - var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr); - if (predCmd is AssertCmd) - newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes)); - else - newCmds.Add(new AssumeCmd(Token.NoToken, newExpr)); - } - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); - yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken)); - labels.Add(yieldCheckerBlock.Label); - labelTargets.Add(yieldCheckerBlock); - yieldCheckerBlocks.Add(yieldCheckerBlock); - } - yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List(), new GotoCmd(Token.NoToken, labels, labelTargets))); - - // Create the yield checker procedure - var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name); - var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List(), new List(), new List(), new List()); - yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - yieldCheckerProcs.Add(yieldCheckerProc); - - // Create the yield checker implementation - var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks); - yieldCheckerImpl.Proc = yieldCheckerProc; - yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - yieldCheckerImpls.Add(yieldCheckerImpl); - } - - private bool IsYieldingHeader(GraphUtil.Graph graph, Block header) - { - foreach (Block backEdgeNode in graph.BackEdgeNodes(header)) - { - foreach (Block x in graph.NaturalLoops(header, backEdgeNode)) - { - foreach (Cmd cmd in x.Cmds) - { - if (cmd is YieldCmd) - return true; - CallCmd callCmd = cmd as CallCmd; - if (callCmd == null) continue; - if (callCmd.IsAsync || callCmd.InParallelWith != null || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) - return true; - } - } - } - return false; - } - - private void TransformImpl(Implementation impl) - { - if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return; - - TransformProc(impl.Proc); - - // Find the yielding loop headers - impl.PruneUnreachableBlocks(); - impl.ComputePredecessorsForBlocks(); - GraphUtil.Graph graph = Program.GraphFromImpl(impl); - graph.ComputeLoops(); - if (!graph.Reducible) - { - throw new Exception("Irreducible flow graphs are unsupported."); - } - HashSet yieldingHeaders = new HashSet(); - IEnumerable sortedHeaders = graph.SortHeadersByDominance(); - foreach (Block header in sortedHeaders) - { - if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header))) - { - yieldingHeaders.Add(header); - } - else if (IsYieldingHeader(graph, header)) - { - yieldingHeaders.Add(header); - } - else - { - continue; - } - } - - Program program = linearTypeChecker.program; - Dictionary map = new Dictionary(); - foreach (Variable local in impl.LocVars) - { - var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); - map[local] = new IdentifierExpr(Token.NoToken, copy); - } - Dictionary ogOldGlobalMap = new Dictionary(); - foreach (IdentifierExpr ie in globalMods) - { - Variable g = ie.Decl; - LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type)); - ogOldGlobalMap[g] = l; - impl.LocVars.Add(l); - } - Dictionary domainNameToInputVar = new Dictionary(); - Dictionary domainNameToLocalVar = new Dictionary(); - { - int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - Variable inParam = impl.InParams[i]; - domainNameToInputVar[domainName] = inParam; - Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type)); - domainNameToLocalVar[domainName] = l; - impl.LocVars.Add(l); - i++; - } - } - - // Collect the yield predicates and desugar yields - List> yields = new List>(); - List cmds = new List(); - foreach (Block b in impl.Blocks) - { - YieldCmd yieldCmd = null; - List newCmds = new List(); - for (int i = 0; i < b.Cmds.Count; i++) - { - Cmd cmd = b.Cmds[i]; - if (cmd is YieldCmd) - { - yieldCmd = (YieldCmd)cmd; - continue; - } - if (yieldCmd != null) - { - PredicateCmd pcmd = cmd as PredicateCmd; - if (pcmd == null) - { - DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); - if (cmds.Count > 0) - { - yields.Add(cmds); - cmds = new List(); - } - yieldCmd = null; - } - else - { - cmds.Add(pcmd); - } - } - CallCmd callCmd = cmd as CallCmd; - if (callCmd != null) - { - if (callCmd.InParallelWith != null || callCmd.IsAsync || - QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) - { - AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); - } - if (callCmd.InParallelWith != null) - { - List ins; - List outs; - Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs); - CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs); - dummyCallCmd.Proc = dummyParallelCallDesugaring; - newCmds.Add(dummyCallCmd); - } - else if (callCmd.IsAsync) - { - if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) - { - asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List(), new List()); - } - var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name]; - CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs); - dummyCallCmd.Proc = dummyAsyncTargetProc; - newCmds.Add(dummyCallCmd); - } - else - { - newCmds.Add(callCmd); - } - if (callCmd.InParallelWith != null || callCmd.IsAsync || - QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) - { - HashSet availableLinearVars = new HashSet(linearTypeChecker.availableLinearVars[callCmd]); - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue; - availableLinearVars.Add(ie.Decl); - } - Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); - AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - } - } - else - { - newCmds.Add(cmd); - } - } - if (yieldCmd != null) - { - DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); - if (cmds.Count > 0) - { - yields.Add(cmds); - cmds = new List(); - } - } - if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) - { - AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); - } - b.Cmds = newCmds; - } - - foreach (Block header in yieldingHeaders) - { - Dictionary domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[header], domainNameToInputVar); - foreach (Block pred in header.Predecessors) - { - AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); - AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - } - List newCmds = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName]))); - } - foreach (Variable v in ogOldGlobalMap.Keys) - { - newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v])))); - } - newCmds.AddRange(header.Cmds); - header.Cmds = newCmds; - } - - { - // Add initial block - List lhss = new List(); - List rhss = new List(); - Dictionary domainNameToExpr = new Dictionary(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]); - } - for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) - { - Variable v = impl.InParams[i]; - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - var domain = linearTypeChecker.linearDomains[domainName]; - IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); - } - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]))); - rhss.Add(domainNameToExpr[domainName]); - } - foreach (Variable g in ogOldGlobalMap.Keys) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); - rhss.Add(Expr.Ident(g)); - } - if (lhss.Count > 0) - { - Block initBlock = new Block(Token.NoToken, "og_init", new List { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); - impl.Blocks.Insert(0, initBlock); - } - } - - CreateYieldCheckerImpl(impl, yields, map); - } - - public void TransformProc(Procedure proc) - { - if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return; - - Program program = linearTypeChecker.program; - Dictionary domainNameToInputVar = new Dictionary(); - { - int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count; - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - Variable inParam = proc.InParams[i]; - domainNameToInputVar[domainName] = inParam; - i++; - } - } - - // Collect the yield predicates and desugar yields - List> yields = new List>(); - List cmds = new List(); - if (proc.Requires.Count > 0) - { - Dictionary> domainNameToScope = new Dictionary>(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToScope[domainName] = new HashSet(); - domainNameToScope[domainName].Add(domainNameToInputVar[domainName]); - } - foreach (Variable v in program.GlobalVariables()) - { - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - domainNameToScope[domainName].Add(v); - } - for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++) - { - Variable v = proc.InParams[i]; - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - domainNameToScope[domainName].Add(v); - } - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName]))); - } - foreach (Requires r in proc.Requires) - { - if (r.Free) - { - cmds.Add(new AssumeCmd(r.tok, r.Condition)); - } - else - { - cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes)); - } - } - yields.Add(cmds); - cmds = new List(); - } - if (proc.Ensures.Count > 0) - { - Dictionary> domainNameToScope = new Dictionary>(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToScope[domainName] = new HashSet(); - domainNameToScope[domainName].Add(domainNameToInputVar[domainName]); - } - foreach (Variable v in program.GlobalVariables()) - { - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - domainNameToScope[domainName].Add(v); - } - for (int i = 0; i < proc.OutParams.Count; i++) - { - Variable v = proc.OutParams[i]; - var domainName = linearTypeChecker.FindDomainName(v); - if (domainName == null) continue; - domainNameToScope[domainName].Add(v); - } - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName]))); - } - foreach (Ensures e in proc.Ensures) - { - if (e.Free) - { - cmds.Add(new AssumeCmd(e.tok, e.Condition)); - } - else - { - cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes)); - } - } - yields.Add(cmds); - cmds = new List(); - } - CreateYieldCheckerImpl(proc, yields, new Dictionary()); - } - - private void AddYieldProcAndImpl() - { - if (yieldProc == null) return; - - Program program = linearTypeChecker.program; - List inputs = new List(); - foreach (string domainName in linearTypeChecker.linearDomains.Keys) - { - var domain = linearTypeChecker.linearDomains[domainName]; - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List(), new List { domain.elementType }, Type.Bool)), true); - inputs.Add(f); - } - foreach (IdentifierExpr ie in globalMods) - { - Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); - inputs.Add(f); - } - List blocks = new List(); - TransferCmd transferCmd = new ReturnCmd(Token.NoToken); - if (yieldCheckerProcs.Count > 0) - { - List blockTargets = new List(); - List labelTargets = new List(); - int labelCount = 0; - foreach (Procedure proc in yieldCheckerProcs) - { - List exprSeq = new List(); - foreach (Variable v in inputs) - { - exprSeq.Add(new IdentifierExpr(Token.NoToken, v)); - } - CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); - callCmd.Proc = proc; - string label = string.Format("L_{0}", labelCount++); - Block block = new Block(Token.NoToken, label, new List { callCmd }, new ReturnCmd(Token.NoToken)); - labelTargets.Add(label); - blockTargets.Add(block); - blocks.Add(block); - } - transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets); - } - blocks.Insert(0, new Block(Token.NoToken, "enter", new List(), transferCmd)); - - var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List(), inputs, new List(), new List(), blocks); - yieldImpl.Proc = yieldProc; - yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - program.TopLevelDeclarations.Add(yieldProc); - program.TopLevelDeclarations.Add(yieldImpl); - } - - private QKeyValue RemoveYieldsAttribute(QKeyValue iter) - { - if (iter == null) return null; - iter.Next = RemoveYieldsAttribute(iter.Next); - return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter; - } - - public void Transform() - { - MoverChecking.AddCheckers(linearTypeChecker); - - Program program = linearTypeChecker.program; - foreach (var decl in program.TopLevelDeclarations) - { - Implementation impl = decl as Implementation; - if (impl == null) continue; - TransformImpl(impl); - } - foreach (Procedure proc in yieldCheckerProcs) - { - program.TopLevelDeclarations.Add(proc); - } - foreach (Implementation impl in yieldCheckerImpls) - { - program.TopLevelDeclarations.Add(impl); - } - foreach (Procedure proc in asyncAndParallelCallDesugarings.Values) - { - program.TopLevelDeclarations.Add(proc); - } - AddYieldProcAndImpl(); - foreach (var decl in program.TopLevelDeclarations) - { - Procedure proc = decl as Procedure; - if (proc == null) continue; - if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) - { - HashSet modifiedVars = new HashSet(); - proc.Modifies.Iter(x => modifiedVars.Add(x.Decl)); - foreach (GlobalVariable g in program.GlobalVariables()) - { - if (modifiedVars.Contains(g)) continue; - proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g)); - } - proc.Attributes = RemoveYieldsAttribute(proc.Attributes); - } - } - foreach (var decl in program.TopLevelDeclarations) - { - Implementation impl = decl as Implementation; - if (impl == null) continue; - impl.Attributes = RemoveYieldsAttribute(impl.Attributes); - } - } - } -} diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj index 3c50afae..a6fed551 100644 --- a/Source/ExecutionEngine/ExecutionEngine.csproj +++ b/Source/ExecutionEngine/ExecutionEngine.csproj @@ -92,6 +92,10 @@ {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} CodeContractsExtender + + {d07b8e38-e172-47f4-ad02-0373014a46d3} + Concurrency + {B230A69C-C466-4065-B9C1-84D80E76D802} Core -- cgit v1.2.3