diff options
| author |  qadeer <unknown> | 2013-11-22 13:04:51 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-11-22 13:04:51 -0800 |
| commit | 3c65f1b879a19c5ab1ed78ebfbcdb434fe7afe06 (patch) | |
| tree | 0703268a6d7676a2efb9da6b58e3351f41373d22 /Source/Core | |
| parent | f0d11b78f3453b5cfbb524e6d0c7214442814351 (diff) | |
factored the concurrency checking code into a separate project
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Core.csproj | 3 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 757 | ||||
| -rw-r--r-- | Source/Core/MoverChecking.cs | 641 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 738 |
4 files changed, 0 insertions, 2139 deletions
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 @@ <Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
<Compile Include="BitvectorAnalysis.cs" />
- <Compile Include="MoverChecking.cs" />
<Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
<Compile Include="Duplicator.cs" />
<Compile Include="Inline.cs" />
<Compile Include="LambdaHelper.cs" />
- <Compile Include="LinearSets.cs" />
<Compile Include="LoopUnroll.cs" />
<Compile Include="OOLongUtil.cs" />
- <Compile Include="OwickiGries.cs" />
<Compile Include="Parser.cs" />
<Compile Include="ResolutionContext.cs" />
<Compile Include="Scanner.cs" />
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<string, Type> domainNameToType;
- public Dictionary<Absy, HashSet<Variable>> availableLinearVars;
- public Dictionary<Variable, string> inoutParamToDomainName;
- public Dictionary<Variable, string> varToDomainName;
- public Dictionary<Variable, string> globalVarToDomainName;
- public Dictionary<string, LinearDomain> linearDomains;
-
- public LinearTypeChecker(Program program)
- {
- this.program = program;
- this.errorCount = 0;
- this.checkingContext = new CheckingContext(null);
- this.domainNameToType = new Dictionary<string, Type>();
- this.parallelCallInvars = new HashSet<Variable>();
- this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
- this.inoutParamToDomainName = new Dictionary<Variable, string>();
- this.varToDomainName = new Dictionary<Variable, string>();
- this.linearDomains = new Dictionary<string, LinearDomain>();
- }
- 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<Variable, string>();
- 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<Variable> start = new HashSet<Variable>(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<Block> dfsStack = new Stack<Block>();
- HashSet<Block> dfsStackAsSet = new HashSet<Block>();
- 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<Variable> 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<Variable>(end);
- dfsStack.Push(target);
- dfsStackAsSet.Add(target);
- }
- else
- {
- var savedAvailableVars = new HashSet<Variable>(availableLinearVars[target]);
- availableLinearVars[target].IntersectWith(end);
- if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target))
- {
- dfsStack.Push(target);
- dfsStackAsSet.Add(target);
- }
- }
- }
- }
- return impl;
- }
- private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {
- HashSet<Variable> start = new HashSet<Variable>(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<Variable>(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<Variable>(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<Variable> rhsVars = new HashSet<Variable>();
- 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<Variable> parallelCallInvars;
- public override Cmd VisitCallCmd(CallCmd node)
- {
- HashSet<Variable> inVars = new HashSet<Variable>();
- 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<Cmd> newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
- {
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- 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<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
- 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<TypeVariable>(),
- new List<Type> { domain.elementType }, Type.Bool)), true);
- impl.InParams.Add(f);
- domainNameToInputVar[domainName] = f;
- }
-
- foreach (Block b in impl.Blocks)
- {
- List<Cmd> newCmds = new List<Cmd>();
- 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> { 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> { Expr.False });
- expr.Resolve(new ResolutionContext(null));
- expr.Typecheck(new TypecheckingContext(null));
- callCmd.Ins.Add(expr);
- }
- callCmd = callCmd.InParallelWith;
- }
- }
- else
- {
- Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- 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<Expr> { 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<Block> g = Program.GraphFromImpl(impl);
- g.ComputeLoops();
- if (g.Reducible)
- {
- foreach (Block header in g.Headers)
- {
- List<Cmd> newCmds = new List<Cmd>();
- 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<string, HashSet<Variable>> domainNameToInputScope = new Dictionary<string, HashSet<Variable>>();
- Dictionary<string, HashSet<Variable>> domainNameToOutputScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearDomains.Keys)
- {
- domainNameToInputScope[domainName] = new HashSet<Variable>();
- domainNameToOutputScope[domainName] = new HashSet<Variable>();
-
- }
- 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<TypeVariable>(), new List<Type> { 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> { Expr.False }), e, Expr.True);
- }
-
- List<Expr> MkExprs(params Expr[] args)
- {
- return new List<Expr>(args);
- }
-
- public Expr DisjointnessExpr(string domainName, HashSet<Variable> 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<TypeVariable>(), new List<Type> { 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<Expr>{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } );
- e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List<Expr> { new IdentifierExpr(Token.NoToken, partition), e } );
- e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List<Expr> { 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> { Expr.True }));
- disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);
- }
- var expr = new ExistsExpr(Token.NoToken, new List<Variable> { 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<Axiom> axioms;
-
- public LinearDomain(Program program, string domainName, Type elementType)
- {
- this.elementType = elementType;
- this.axioms = new List<Axiom>();
-
- MapType mapTypeBool = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Bool);
- MapType mapTypeInt = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Int);
- this.mapOrBool = new Function(Token.NoToken, "linear_" + domainName + "_MapOr",
- new List<Variable> { 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<Expr> { aie, bie } );
- var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie } );
- var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,
- new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie } ),
- new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie} ));
- var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,
- new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }),
- new ForallExpr(Token.NoToken, new List<Variable> { 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<Variable> { 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<Expr> { aie, bie });
- var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });
- var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,
- new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),
- new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));
- var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,
- new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }),
- new ForallExpr(Token.NoToken, new List<Variable> { 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<Variable> { 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<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.True }), xie });
- var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { 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<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.False }), xie });
- var falseAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { 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<Variable> { 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<Expr> { aie, bie });
- var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });
- var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,
- new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),
- new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));
- var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,
- new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }),
- new ForallExpr(Token.NoToken, new List<Variable> { 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<Variable> { 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<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List<Expr> { aie }), xie });
- var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { 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<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;
- HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;
- HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;
- LinearTypeChecker linearTypeChecker;
- Program moverCheckerProgram;
- private MoverChecking(LinearTypeChecker linearTypeChecker)
- {
- this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
- this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
- this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
- this.linearTypeChecker = linearTypeChecker;
- this.moverCheckerProgram = new Program();
- foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations)
- {
- if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom)
- this.moverCheckerProgram.TopLevelDeclarations.Add(decl);
- }
- foreach (Variable v in linearTypeChecker.program.GlobalVariables())
- {
- this.moverCheckerProgram.TopLevelDeclarations.Add(v);
- }
- }
- private sealed class MySubstituter : Duplicator
- {
- private readonly Substitution outsideOld;
- private readonly Substitution insideOld;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(insideOld != null);
- }
-
- public MySubstituter(Substitution outsideOld, Substitution insideOld)
- : base()
- {
- Contract.Requires(outsideOld != null && insideOld != null);
- this.outsideOld = outsideOld;
- this.insideOld = insideOld;
- }
-
- private bool insideOldExpr = false;
-
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- Contract.Ensures(Contract.Result<Expr>() != null);
- Expr e = null;
-
- if (insideOldExpr)
- {
- e = insideOld(node.Decl);
- }
- else
- {
- e = outsideOld(node.Decl);
- }
- return e == null ? base.VisitIdentifierExpr(node) : e;
- }
-
- public override Expr VisitOldExpr(OldExpr node)
- {
- Contract.Ensures(Contract.Result<Expr>() != null);
- bool previouslyInOld = insideOldExpr;
- insideOldExpr = true;
- Expr tmp = (Expr)this.Visit(node.Expr);
- OldExpr e = new OldExpr(node.tok, tmp);
- insideOldExpr = previouslyInOld;
- return e;
- }
- }
-
- enum MoverType
- {
- Top,
- Atomic,
- Right,
- Left,
- Both
- }
-
- class ActionInfo
- {
- public Procedure proc;
- public MoverType moverType;
- public List<AssertCmd> thisGate;
- public CodeExpr thisAction;
- public List<Variable> thisInParams;
- public List<Variable> thisOutParams;
- public List<AssertCmd> thatGate;
- public CodeExpr thatAction;
- public List<Variable> thatInParams;
- public List<Variable> thatOutParams;
-
- public bool IsRightMover
- {
- get { return moverType == MoverType.Right || moverType == MoverType.Both; }
- }
-
- public bool IsLeftMover
- {
- get { return moverType == MoverType.Left || moverType == MoverType.Both; }
- }
-
- public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType)
- {
- this.proc = proc;
- this.moverType = moverType;
- this.thisGate = new List<AssertCmd>();
- this.thisAction = codeExpr;
- this.thisInParams = new List<Variable>();
- this.thisOutParams = new List<Variable>();
- this.thatGate = new List<AssertCmd>();
- this.thatInParams = new List<Variable>();
- this.thatOutParams = new List<Variable>();
-
- var cmds = thisAction.Blocks[0].Cmds;
- for (int i = 0; i < cmds.Count; i++)
- {
- AssertCmd assertCmd = cmds[i] as AssertCmd;
- if (assertCmd == null) break;
- thisGate.Add(assertCmd);
- cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
- }
-
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (Variable x in proc.InParams)
- {
- this.thisInParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
- this.thatInParams.Add(y);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- }
- foreach (Variable x in proc.OutParams)
- {
- this.thisOutParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- this.thatOutParams.Add(y);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- }
- List<Variable> otherLocVars = new List<Variable>();
- foreach (Variable x in thisAction.LocVars)
- {
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- map[x] = new IdentifierExpr(Token.NoToken, y);
- otherLocVars.Add(y);
- }
- Contract.Assume(proc.TypeParameters.Count == 0);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in thisGate)
- {
- thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
- }
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- List<Block> otherBlocks = new List<Block>();
- foreach (Block block in thisAction.Blocks)
- {
- List<Cmd> otherCmds = new List<Cmd>();
- foreach (Cmd cmd in block.Cmds)
- {
- otherCmds.Add(Substituter.Apply(subst, cmd));
- }
- Block otherBlock = new Block();
- otherBlock.Cmds = otherCmds;
- otherBlock.Label = "that_" + block.Label;
- block.Label = "this_" + block.Label;
- otherBlocks.Add(otherBlock);
- blockMap[block] = otherBlock;
- if (block.TransferCmd is GotoCmd)
- {
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- for (int i = 0; i < gotoCmd.labelNames.Count; i++)
- {
- gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
- }
- }
- }
- foreach (Block block in thisAction.Blocks)
- {
- if (block.TransferCmd is ReturnExprCmd)
- {
- blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
- continue;
- }
- List<Block> otherGotoCmdLabelTargets = new List<Block>();
- List<string> otherGotoCmdLabelNames = new List<string>();
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- otherGotoCmdLabelTargets.Add(blockMap[target]);
- otherGotoCmdLabelNames.Add(blockMap[target].Label);
- }
- blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
- }
- this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
- }
- }
-
- public static void AddCheckers(LinearTypeChecker linearTypeChecker)
- {
- Program program = linearTypeChecker.program;
- List<ActionInfo> gatedActions = new List<ActionInfo>();
- foreach (Declaration decl in program.TopLevelDeclarations)
- {
- Procedure proc = decl as Procedure;
- if (proc == null) continue;
- foreach (Ensures e in proc.Ensures)
- {
- MoverType moverType = GetMoverType(e);
- if (moverType == MoverType.Top) continue;
- CodeExpr codeExpr = e.Condition as CodeExpr;
- if (codeExpr == null)
- {
- Console.WriteLine("Warning: an atomic action must be a CodeExpr");
- continue;
- }
- ActionInfo info = new ActionInfo(proc, codeExpr, moverType);
- gatedActions.Add(info);
- }
- }
- if (gatedActions.Count == 0)
- return;
- MoverChecking moverChecking = new MoverChecking(linearTypeChecker);
- foreach (ActionInfo first in gatedActions)
- {
- Debug.Assert(first.moverType != MoverType.Top);
- if (first.moverType == MoverType.Atomic)
- continue;
- foreach (ActionInfo second in gatedActions)
- {
- if (first.IsRightMover)
- {
- moverChecking.CreateCommutativityChecker(program, first, second);
- moverChecking.CreateGatePreservationChecker(program, second, first);
- }
- if (first.IsLeftMover)
- {
- moverChecking.CreateCommutativityChecker(program, second, first);
- moverChecking.CreateGatePreservationChecker(program, first, second);
- moverChecking.CreateFailurePreservationChecker(program, second, first);
- }
- }
- }
- var eraser = new LinearEraser();
- eraser.VisitProgram(moverChecking.moverCheckerProgram);
- {
- int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
- CommandLineOptions.Clo.PrintUnstructured = 1;
- using (TokenTextWriter writer = new TokenTextWriter("MoverChecker.bpl", false))
- {
- if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)
- {
- writer.WriteLine("// " + CommandLineOptions.Clo.Version);
- writer.WriteLine("// " + CommandLineOptions.Clo.Environment);
- }
- writer.WriteLine();
- moverChecking.moverCheckerProgram.Emit(writer);
- }
- CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
- }
- }
-
- private static MoverType GetMoverType(Ensures e)
- {
- if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
- return MoverType.Atomic;
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
- return MoverType.Right;
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
- return MoverType.Left;
- else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
- return MoverType.Both;
- else
- return MoverType.Top;
- }
-
- class TransitionRelationComputation
- {
- private Program program;
- private ActionInfo first;
- private ActionInfo second;
- private Stack<Block> dfsStack;
- private Expr transitionRelation;
-
- public TransitionRelationComputation(Program program, ActionInfo second)
- {
- this.program = program;
- this.first = null;
- this.second = second;
- this.dfsStack = new Stack<Block>();
- this.transitionRelation = Expr.False;
- }
-
- public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)
- {
- this.program = program;
- this.first = first;
- this.second = second;
- this.dfsStack = new Stack<Block>();
- this.transitionRelation = Expr.False;
- }
-
- public Expr Compute()
- {
- Search(second.thatAction.Blocks[0], false);
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- List<Variable> boundVars = new List<Variable>();
- if (first != null)
- {
- foreach (Variable v in first.thisAction.LocVars)
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
- map[v] = new IdentifierExpr(Token.NoToken, bv);
- boundVars.Add(bv);
- }
- }
- foreach (Variable v in second.thatAction.LocVars)
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
- map[v] = new IdentifierExpr(Token.NoToken, bv);
- boundVars.Add(bv);
- }
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- if (boundVars.Count > 0)
- return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation));
- else
- return transitionRelation;
- }
-
- private Expr CalculatePathCondition()
- {
- Expr returnExpr = Expr.True;
- foreach (Variable v in program.GlobalVariables())
- {
- var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
- returnExpr = Expr.And(eqExpr, returnExpr);
- }
- if (first != null)
- {
- foreach (Variable v in first.thisOutParams)
- {
- var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
- returnExpr = Expr.And(eqExpr, returnExpr);
- }
- }
- foreach (Variable v in second.thatOutParams)
- {
- var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
- returnExpr = Expr.And(eqExpr, returnExpr);
- }
- Block[] dfsStackAsArray = dfsStack.Reverse().ToArray();
- for (int i = dfsStackAsArray.Length - 1; i >= 0; i--)
- {
- Block b = dfsStackAsArray[i];
- for (int j = b.Cmds.Count - 1; j >= 0; j--)
- {
- Cmd cmd = b.Cmds[j];
- if (cmd is AssumeCmd)
- {
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);
- }
- else if (cmd is AssignCmd)
- {
- AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- for (int k = 0; k < assignCmd.Lhss.Count; k++)
- {
- map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];
- }
- Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);
- returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr);
- }
- else
- {
- Debug.Assert(false);
- }
- }
- }
- return returnExpr;
- }
-
- private void Search(Block b, bool inFirst)
- {
- dfsStack.Push(b);
- if (b.TransferCmd is ReturnExprCmd)
- {
- if (first == null || inFirst)
- {
- transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition());
- }
- else
- {
- Search(first.thisAction.Blocks[0], true);
- }
- }
- else
- {
- GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- Search(target, inFirst);
- }
- }
- dfsStack.Pop();
- }
- }
-
- private static List<Block> CloneBlocks(List<Block> blocks)
- {
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- List<Block> otherBlocks = new List<Block>();
- foreach (Block block in blocks)
- {
- List<Cmd> otherCmds = new List<Cmd>();
- foreach (Cmd cmd in block.Cmds)
- {
- otherCmds.Add(cmd);
- }
- Block otherBlock = new Block();
- otherBlock.Cmds = otherCmds;
- otherBlock.Label = block.Label;
- otherBlocks.Add(otherBlock);
- blockMap[block] = otherBlock;
- }
- foreach (Block block in blocks)
- {
- if (block.TransferCmd is ReturnExprCmd)
- {
- blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
- continue;
- }
- List<Block> otherGotoCmdLabelTargets = new List<Block>();
- List<string> otherGotoCmdLabelNames = new List<string>();
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- otherGotoCmdLabelTargets.Add(blockMap[target]);
- otherGotoCmdLabelNames.Add(blockMap[target].Label);
- }
- blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
- }
- return otherBlocks;
- }
-
- private List<Requires> DisjointnessRequires(Program program, ActionInfo first, ActionInfo second)
- {
- List<Requires> requires = new List<Requires>();
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- }
- foreach (Variable v in program.GlobalVariables())
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- domainNameToScope[domainName].Add(v);
- }
- foreach (Variable v in first.thisInParams)
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- domainNameToScope[domainName].Add(v);
- }
- for (int i = 0; i < second.thatInParams.Count; i++)
- {
- var domainName = linearTypeChecker.FindDomainName(second.thisInParams[i]);
- if (domainName == null) continue;
- domainNameToScope[domainName].Add(second.thatInParams[i]);
- }
- foreach (string domainName in domainNameToScope.Keys)
- {
- requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
- }
- return requires;
- }
-
- private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)
- {
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
- if (commutativityCheckerCache.Contains(actionPair))
- return;
- commutativityCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thisInParams);
- inputs.AddRange(second.thatInParams);
- List<Variable> outputs = new List<Variable>();
- outputs.AddRange(first.thisOutParams);
- outputs.AddRange(second.thatOutParams);
- List<Variable> locals = new List<Variable>();
- locals.AddRange(first.thisAction.LocVars);
- locals.AddRange(second.thatAction.LocVars);
- List<Block> firstBlocks = CloneBlocks(first.thisAction.Blocks);
- List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
- foreach (Block b in firstBlocks)
- {
- if (b.TransferCmd is ReturnCmd)
- {
- List<Block> bs = new List<Block>();
- bs.Add(secondBlocks[0]);
- List<string> ls = new List<string>();
- ls.Add(secondBlocks[0].Label);
- b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);
- }
- }
- List<Block> blocks = new List<Block>();
- blocks.AddRange(firstBlocks);
- blocks.AddRange(secondBlocks);
- List<Requires> requires = DisjointnessRequires(program, first, second);
- List<Ensures> ensures = new List<Ensures>();
- Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();
- ensures.Add(new Ensures(false, transitionRelation));
- string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
- impl.Proc = proc;
- this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
- this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
- }
-
- private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)
- {
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
- if (gatePreservationCheckerCache.Contains(actionPair))
- return;
- gatePreservationCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thisInParams);
- inputs.AddRange(second.thatInParams);
- List<Variable> outputs = new List<Variable>();
- outputs.AddRange(first.thisOutParams);
- outputs.AddRange(second.thatOutParams);
- List<Variable> locals = new List<Variable>();
- locals.AddRange(second.thatAction.LocVars);
- List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
- List<Requires> requires = DisjointnessRequires(program, first, second);
- List<Ensures> ensures = new List<Ensures>();
- foreach (AssertCmd assertCmd in first.thisGate)
- {
- requires.Add(new Requires(false, assertCmd.Expr));
- ensures.Add(new Ensures(false, assertCmd.Expr));
- }
- string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
- impl.Proc = proc;
- this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
- this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
- }
-
- private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
- {
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
- if (failurePreservationCheckerCache.Contains(actionPair))
- return;
- failurePreservationCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thisInParams);
- inputs.AddRange(second.thatInParams);
-
- Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute();
- Expr expr = Expr.True;
- foreach (AssertCmd assertCmd in first.thisGate)
- {
- expr = Expr.And(assertCmd.Expr, expr);
- }
- List<Requires> requires = DisjointnessRequires(program, first, second);
- requires.Add(new Requires(false, Expr.Not(expr)));
- foreach (AssertCmd assertCmd in second.thatGate)
- {
- requires.Add(new Requires(false, assertCmd.Expr));
- }
-
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();
- List<Variable> boundVars = new List<Variable>();
- foreach (Variable v in program.GlobalVariables())
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
- boundVars.Add(bv);
- map[v] = new IdentifierExpr(Token.NoToken, bv);
- }
- foreach (Variable v in second.thatOutParams)
- {
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
- boundVars.Add(bv);
- map[v] = new IdentifierExpr(Token.NoToken, bv);
- }
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
- boundVars.Add(bv);
- oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
- }
- }
- foreach (Variable v in second.thatAction.LocVars)
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
- boundVars.Add(bv);
- oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
- }
-
- Expr ensuresExpr = Expr.And(transitionRelation, Expr.Not(expr));
- if (boundVars.Count > 0)
- {
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
- ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, (Expr)new MySubstituter(subst, oldSubst).Visit(ensuresExpr));
- }
- List<Ensures> ensures = new List<Ensures>();
- ensures.Add(new Ensures(false, ensuresExpr));
- List<Block> blocks = new List<Block>();
- blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
- string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, new List<IdentifierExpr>(), ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
- impl.Proc = proc;
- this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
- this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
- }
- }
-}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs 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<IdentifierExpr> globalMods;
- LinearTypeChecker linearTypeChecker;
- Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
- List<Procedure> yieldCheckerProcs;
- List<Implementation> yieldCheckerImpls;
- Procedure yieldProc;
-
- public OwickiGriesTransform(LinearTypeChecker linearTypeChecker)
- {
- this.linearTypeChecker = linearTypeChecker;
- Program program = linearTypeChecker.program;
- globalMods = new List<IdentifierExpr>();
- foreach (Variable g in program.GlobalVariables())
- {
- globalMods.Add(new IdentifierExpr(Token.NoToken, g));
- }
- asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
- yieldCheckerProcs = new List<Procedure>();
- yieldCheckerImpls = new List<Implementation>();
- yieldProc = null;
- }
-
- private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
- {
- List<Expr> exprSeq = new List<Expr>();
- 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<Variable> inputs = new List<Variable>();
- 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<TypeVariable>(), new List<Type> { 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<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- }
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
- yieldCallCmd.Proc = yieldProc;
- newCmds.Add(yieldCallCmd);
- }
-
- private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
- {
- Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- 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<Expr> { 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<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
- {
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- 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<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
- {
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
-
- if (globalMods.Count > 0)
- {
- newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
- }
- Dictionary<string, Expr> 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<Expr> ins, out List<IdentifierExpr> outs)
- {
- List<string> parallelCalleeNames = new List<string>();
- CallCmd iter = callCmd;
- ins = new List<Expr>();
- outs = new List<IdentifierExpr>();
- 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<Variable> inParams = new List<Variable>();
- List<Variable> outParams = new List<Variable>();
- List<Requires> requiresSeq = new List<Requires>();
- List<Ensures> ensuresSeq = new List<Ensures>();
- int count = 0;
- while (callCmd != null)
- {
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- 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<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);
- proc.AddAttribute("yields");
- asyncAndParallelCallDesugarings[procName] = proc;
- return proc;
- }
-
- private void CreateYieldCheckerImpl(DeclWithFormals decl, List<List<Cmd>> yields, Dictionary<Variable, Expr> map)
- {
- if (yields.Count == 0) return;
-
- Program program = linearTypeChecker.program;
- List<Variable> locals = new List<Variable>();
- List<Variable> inputs = new List<Variable>();
- 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<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
- Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(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<Block> yieldCheckerBlocks = new List<Block>();
- List<String> labels = new List<String>();
- List<Block> labelTargets = new List<Block>();
- Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- int yieldCount = 0;
- foreach (List<Cmd> cs in yields)
- {
- var linearDomains = linearTypeChecker.linearDomains;
- List<Cmd> newCmds = new List<Cmd>();
- 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<Cmd>(), 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<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- 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<Variable>(), 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<Block> 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<Block> graph = Program.GraphFromImpl(impl);
- graph.ComputeLoops();
- if (!graph.Reducible)
- {
- throw new Exception("Irreducible flow graphs are unsupported.");
- }
- HashSet<Block> yieldingHeaders = new HashSet<Block>();
- IEnumerable<Block> 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<Variable, Expr> map = new Dictionary<Variable, Expr>();
- 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<Variable, Variable> ogOldGlobalMap = new Dictionary<Variable, Variable>();
- 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<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
- Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();
- {
- 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<List<Cmd>> yields = new List<List<Cmd>>();
- List<Cmd> cmds = new List<Cmd>();
- foreach (Block b in impl.Blocks)
- {
- YieldCmd yieldCmd = null;
- List<Cmd> newCmds = new List<Cmd>();
- 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<Cmd>();
- }
- 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<Expr> ins;
- List<IdentifierExpr> 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<IdentifierExpr>(), new List<Ensures>());
- }
- 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<Variable> availableLinearVars = new HashSet<Variable>(linearTypeChecker.availableLinearVars[callCmd]);
- foreach (IdentifierExpr ie in callCmd.Outs)
- {
- if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue;
- availableLinearVars.Add(ie.Decl);
- }
- Dictionary<string, Expr> 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<Cmd>();
- }
- }
- if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
- {
- AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
- }
- b.Cmds = newCmds;
- }
-
- foreach (Block header in yieldingHeaders)
- {
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[header], domainNameToInputVar);
- foreach (Block pred in header.Predecessors)
- {
- AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
- AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- List<Cmd> newCmds = new List<Cmd>();
- 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<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- 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<Expr> { 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<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { 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<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
- {
- 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<List<Cmd>> yields = new List<List<Cmd>>();
- List<Cmd> cmds = new List<Cmd>();
- if (proc.Requires.Count > 0)
- {
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- 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<Cmd>();
- }
- if (proc.Ensures.Count > 0)
- {
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- 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<Cmd>();
- }
- CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());
- }
-
- private void AddYieldProcAndImpl()
- {
- if (yieldProc == null) return;
-
- Program program = linearTypeChecker.program;
- List<Variable> inputs = new List<Variable>();
- 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<TypeVariable>(), new List<Type> { 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<Block> blocks = new List<Block>();
- TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
- if (yieldCheckerProcs.Count > 0)
- {
- List<Block> blockTargets = new List<Block>();
- List<String> labelTargets = new List<String>();
- int labelCount = 0;
- foreach (Procedure proc in yieldCheckerProcs)
- {
- List<Expr> exprSeq = new List<Expr>();
- foreach (Variable v in inputs)
- {
- exprSeq.Add(new IdentifierExpr(Token.NoToken, v));
- }
- CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());
- callCmd.Proc = proc;
- string label = string.Format("L_{0}", labelCount++);
- Block block = new Block(Token.NoToken, label, new List<Cmd> { 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<Cmd>(), transferCmd));
-
- var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), 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<Variable> modifiedVars = new HashSet<Variable>();
- 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);
- }
- }
- }
-}
|