diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-24 22:06:06 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-24 22:06:06 -0800 |
| commit | d3c0a64687656cfc102c21e132eec072efc81b67 (patch) | |
| tree | d018adfefbc9acea3f302061d76bfd4c80b7b957 /Source/Core | |
| parent | a3500827a22df775f67b6f706ce1859e5b6ad981 (diff) | |
first check in of Owicki-Gries and linear sets
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Core.csproj | 2 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 562 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 401 |
3 files changed, 965 insertions, 0 deletions
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 49639822..eb581edd 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -157,8 +157,10 @@ <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="PureCollections.cs" />
<Compile Include="ResolutionContext.cs" />
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs new file mode 100644 index 00000000..94d3c734 --- /dev/null +++ b/Source/Core/LinearSets.cs @@ -0,0 +1,562 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.Boogie;
+
+namespace Microsoft.Boogie
+{
+ class LinearTypechecker : StandardVisitor
+ {
+ CheckingContext checkingContext;
+ public LinearTypechecker()
+ {
+ checkingContext = new CheckingContext(null);
+ }
+
+ 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];
+ string domainName = QKeyValue.FindStringAttribute(lhs.DeepAssignedVariable.Attributes, "linear");
+ if (domainName == null) continue;
+ SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
+ if (salhs == null)
+ {
+ checkingContext.Error(node, "Only simple assignment allowed on linear sets");
+ continue;
+ }
+ IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;
+ if (rhs == null)
+ {
+ checkingContext.Error(node, "Only variable can be assigned to a linear set");
+ continue;
+ }
+ string rhsDomainName = QKeyValue.FindStringAttribute(rhs.Decl.Attributes, "linear");
+ Formal formal = rhs.Decl as Formal;
+ if (formal != null && formal.InComing)
+ {
+ rhsDomainName = null;
+ }
+ if (rhsDomainName == null)
+ {
+ checkingContext.Error(node, "Only linear variable can be assigned to another linear variable");
+ continue;
+ }
+ if (domainName != rhsDomainName)
+ {
+ checkingContext.Error(node, "Variable of one domain being assigned to a variable of another domain");
+ continue;
+ }
+ if (rhsVars.Contains(rhs.Decl))
+ {
+ checkingContext.Error(node, "A linear set can occur only once in the rhs");
+ continue;
+ }
+ rhsVars.Add(rhs.Decl);
+ }
+
+ return base.VisitAssignCmd(node);
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ HashSet<Variable> inVars = new HashSet<Variable>();
+ for (int i = 0; i < node.Proc.InParams.Length; i++)
+ {
+ Variable formal = node.Proc.InParams[i];
+ string domainName = QKeyValue.FindStringAttribute(formal.Attributes, "linear");
+ if (domainName == null) continue;
+ IdentifierExpr actual = node.Ins[i] as IdentifierExpr;
+ if (actual == null)
+ {
+ checkingContext.Error(node, "Only variable can be assigned to a linear set");
+ continue;
+ }
+ string actualDomainName = QKeyValue.FindStringAttribute(actual.Decl.Attributes, "linear");
+ Formal formal2 = actual.Decl as Formal;
+ if (formal2 != null && formal2.InComing)
+ {
+ actualDomainName = null;
+ }
+ if (actualDomainName == null)
+ {
+ checkingContext.Error(node, "Only a linear argument can be passed to a linear parameter");
+ continue;
+ }
+ if (domainName != actualDomainName)
+ {
+ checkingContext.Error(node, "The domains of formal and actual parameters must be the same");
+ continue;
+ }
+ if (inVars.Contains(actual.Decl))
+ {
+ checkingContext.Error(node, "A linear set can occur only once as an in parameter");
+ continue;
+ }
+ inVars.Add(actual.Decl);
+ }
+
+ for (int i = 0; i < node.Proc.OutParams.Length; i++)
+ {
+ IdentifierExpr actual = node.Outs[i];
+ string actualDomainName = QKeyValue.FindStringAttribute(actual.Decl.Attributes, "linear");
+ if (actualDomainName == null) continue;
+ Variable formal = node.Proc.OutParams[i];
+ string domainName = QKeyValue.FindStringAttribute(formal.Attributes, "linear");
+ if (domainName == null)
+ {
+ checkingContext.Error(node, "Only a linear variable can be passed to a linear parameter");
+ continue;
+ }
+ if (domainName != actualDomainName)
+ {
+ checkingContext.Error(node, "The domains of formal and actual parameters must be the same");
+ }
+ }
+ return base.VisitCallCmd(node);
+ }
+ }
+
+ class LinearSetTransform
+ {
+ private Program program;
+ private Dictionary<Variable, string> varToDomainName;
+ private Dictionary<string, LinearDomain> linearDomains;
+
+ public LinearSetTransform(Program program)
+ {
+ this.program = program;
+ this.varToDomainName = new Dictionary<Variable, string>();
+ this.linearDomains = new Dictionary<string, LinearDomain>();
+ }
+
+ private void AddVariableToScope(Variable v, Dictionary<string, HashSet<Variable>> domainNameToScope)
+ {
+ var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");
+ if (domainName == null) return;
+ AddVariableToScopeHelper(v, domainName, domainNameToScope);
+ }
+
+ private void AddVariableToScope(Implementation impl, int outParamIndex, Dictionary<string, HashSet<Variable>> domainNameToScope)
+ {
+ var domainName = QKeyValue.FindStringAttribute(impl.Proc.OutParams[outParamIndex].Attributes, "linear");
+ if (domainName == null) return;
+ AddVariableToScopeHelper(impl.OutParams[outParamIndex], domainName, domainNameToScope);
+ }
+
+ private void AddVariableToScopeHelper(Variable v, string domainName, Dictionary<string, HashSet<Variable>> domainNameToScope)
+ {
+ if (!varToDomainName.ContainsKey(v))
+ {
+ varToDomainName[v] = domainName;
+ }
+ if (!linearDomains.ContainsKey(domainName))
+ {
+ var domain = new LinearDomain(program, v, domainName);
+ linearDomains[domainName] = domain;
+ varToDomainName[domain.allocator] = domainName;
+ }
+ if (!domainNameToScope.ContainsKey(domainName))
+ {
+ HashSet<Variable> scope = new HashSet<Variable>();
+ scope.Add(linearDomains[domainName].allocator);
+ domainNameToScope[domainName] = scope;
+ }
+ domainNameToScope[domainName].Add(v);
+ }
+
+ public void Transform(Program program)
+ {
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (Variable v in program.GlobalVariables())
+ {
+ AddVariableToScope(v, domainNameToScope);
+ }
+ for (int i = 0; i < impl.OutParams.Length; i++)
+ {
+ AddVariableToScope(impl, i, domainNameToScope);
+ }
+ foreach (Variable v in impl.LocVars)
+ {
+ AddVariableToScope(v, domainNameToScope);
+ }
+
+ Dictionary<Variable, LocalVariable> copies = new Dictionary<Variable, LocalVariable>();
+ foreach (Block b in impl.Blocks)
+ {
+ CmdSeq newCmds = new CmdSeq();
+ for (int i = 0; i < b.Cmds.Length; i++)
+ {
+ Cmd cmd = b.Cmds[i];
+ if (cmd is AssignCmd)
+ {
+ TransformAssignCmd(newCmds, (AssignCmd)cmd, copies);
+ }
+ else if (cmd is HavocCmd)
+ {
+ TransformHavocCmd(newCmds, (HavocCmd)cmd, copies, domainNameToScope);
+ }
+ else if (cmd is CallCmd)
+ {
+ TransformCallCmd(newCmds, (CallCmd)cmd, copies, domainNameToScope);
+ }
+ else
+ {
+ newCmds.Add(cmd);
+ }
+ }
+ if (b.TransferCmd is ReturnCmd)
+ {
+ foreach (Variable v in impl.LocVars)
+ {
+ if (varToDomainName.ContainsKey(v))
+ Drain(newCmds, v, varToDomainName[v]);
+ }
+ }
+ b.Cmds = newCmds;
+ }
+
+ foreach (var v in copies.Values)
+ {
+ impl.LocVars.Add(v);
+ }
+
+ {
+ // Loops
+ Microsoft.Boogie.GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);
+ g.ComputeLoops();
+ if (g.Reducible)
+ {
+ foreach (Block header in g.Headers)
+ {
+ CmdSeq newCmds = new CmdSeq();
+ foreach (string domainName in domainNameToScope.Keys)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ newCmds.AddRange(header.Cmds);
+ header.Cmds = newCmds;
+ }
+ }
+ else
+ {
+ Console.WriteLine("Warning: implementation {0} is not reducible", impl.Name);
+ }
+ }
+
+ {
+ // Initialization
+ CmdSeq newCmds = new CmdSeq();
+ foreach (Variable v in impl.OutParams)
+ {
+ if (varToDomainName.ContainsKey(v))
+ Initialize(newCmds, v);
+ }
+ foreach (Variable v in impl.LocVars)
+ {
+ if (varToDomainName.ContainsKey(v))
+ Initialize(newCmds, v);
+ }
+ newCmds.AddRange(impl.Blocks[0].Cmds);
+ impl.Blocks[0].Cmds = newCmds;
+ }
+ }
+
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ Procedure proc = impl.Proc;
+
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (Variable v in program.GlobalVariables())
+ {
+ AddVariableToScope(v, domainNameToScope);
+ }
+ foreach (string domainName in domainNameToScope.Keys)
+ {
+ proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ Dictionary<string, HashSet<Variable>> domainNameToInParams = new Dictionary<string, HashSet<Variable>>();
+ foreach (Variable v in proc.InParams)
+ {
+ var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");
+ if (domainName == null) continue;
+ if (!linearDomains.ContainsKey(domainName))
+ {
+ linearDomains[domainName] = new LinearDomain(program, v, domainName);
+ }
+ if (!domainNameToInParams.ContainsKey(domainName))
+ {
+ domainNameToInParams[domainName] = new HashSet<Variable>();
+ }
+ domainNameToInParams[domainName].Add(v);
+ var domain = linearDomains[domainName];
+ Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new ExprSeq(new IdentifierExpr(Token.NoToken, v), new IdentifierExpr(Token.NoToken, domain.allocator)));
+ e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True)));
+ proc.Requires.Add(new Requires(true, e));
+ }
+ foreach (var domainName in domainNameToInParams.Keys)
+ {
+ proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInParams[domainName])));
+ }
+ }
+
+ foreach (LinearDomain domain in linearDomains.Values)
+ {
+ program.TopLevelDeclarations.Add(domain.allocator);
+ }
+ }
+
+ void Initialize(CmdSeq newCmds, Variable v)
+ {
+ var domainName = varToDomainName[v];
+ var domain = linearDomains[domainName];
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ List<Expr> rhss = new List<Expr>();
+ rhss.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ }
+
+ void Drain(CmdSeq newCmds, Variable v, string domainName)
+ {
+ var domain = linearDomains[domainName];
+ List<AssignLhs> lhss = MkAssignLhss(domain.allocator);
+ List<Expr> rhss = MkExprs(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(new IdentifierExpr(Token.NoToken, domain.allocator), new IdentifierExpr(Token.NoToken, v))));
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ }
+
+ List<AssignLhs> MkAssignLhss(params Variable[] args)
+ {
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ foreach (Variable arg in args)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, arg)));
+ }
+ return lhss;
+ }
+
+ List<Expr> MkExprs(params Expr[] args)
+ {
+ return new List<Expr>(args);
+ }
+
+ void TransformHavocCmd(CmdSeq newCmds, HavocCmd havocCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)
+ {
+ Dictionary<string, HashSet<Variable>> domainNameToHavocVars = new Dictionary<string, HashSet<Variable>>();
+ foreach (IdentifierExpr ie in havocCmd.Vars)
+ {
+ Variable v = ie.Decl;
+ if (!varToDomainName.ContainsKey(v)) continue;
+ var domainName = varToDomainName[v];
+ if (!domainNameToHavocVars.ContainsKey(domainName))
+ {
+ domainNameToHavocVars[domainName] = new HashSet<Variable>();
+ }
+ domainNameToHavocVars[domainName].Add(v);
+ if (!copies.ContainsKey(v))
+ {
+ copies[v] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", v.Name), v.TypedIdent.Type));
+ }
+ var allocator = linearDomains[domainName].allocator;
+ domainNameToHavocVars[domainName].Add(allocator);
+ if (!copies.ContainsKey(allocator))
+ {
+ copies[allocator] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", allocator.Name), allocator.TypedIdent.Type));
+ }
+ }
+ foreach (var domainName in domainNameToHavocVars.Keys)
+ {
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ List<Expr> rhss = new List<Expr>();
+ foreach (var v in domainNameToHavocVars[domainName])
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[v])));
+ rhss.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ havocCmd.Vars.Add(new IdentifierExpr(Token.NoToken, linearDomains[domainName].allocator));
+ }
+ newCmds.Add(havocCmd);
+ foreach (string domainName in domainNameToHavocVars.Keys)
+ {
+ var domain = linearDomains[domainName];
+ Expr oldExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False));
+ Expr expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False));
+ foreach (var v in domainNameToHavocVars[domainName])
+ {
+ oldExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(new IdentifierExpr(Token.NoToken, copies[v]), oldExpr));
+ expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(new IdentifierExpr(Token.NoToken, v), expr));
+ }
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, oldExpr, expr)));
+ newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ }
+
+ void TransformCallCmd(CmdSeq newCmds, CallCmd callCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)
+ {
+ List<Expr> newIns = new List<Expr>();
+ for (int i = 0; i < callCmd.Ins.Count; i++)
+ {
+ IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
+ if (ie == null)
+ {
+ newIns.Add(callCmd.Ins[i]);
+ continue;
+ }
+ Variable source = ie.Decl;
+ Variable target = callCmd.Proc.InParams[i];
+ if (!varToDomainName.ContainsKey(source) || !varToDomainName.ContainsKey(target))
+ {
+ newIns.Add(ie);
+ continue;
+ }
+ if (!copies.ContainsKey(source))
+ {
+ copies[source] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", source.Name), source.TypedIdent.Type));
+ }
+ newIns.Add(new IdentifierExpr(Token.NoToken, copies[source]));
+ newCmds.Add(new AssignCmd(Token.NoToken, MkAssignLhss(copies[source], source), MkExprs(new IdentifierExpr(Token.NoToken, source), new NAryExpr(Token.NoToken, new FunctionCall(linearDomains[varToDomainName[source]].mapConstBool), new ExprSeq(Expr.False)))));
+ }
+ HashSet<Variable> drainedVars = new HashSet<Variable>();
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ Variable v = ie.Decl;
+ if (!varToDomainName.ContainsKey(v)) continue;
+ if (!copies.ContainsKey(v))
+ {
+ copies[v] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", v.Name), v.TypedIdent.Type));
+ }
+ newCmds.Add(new AssignCmd(Token.NoToken, MkAssignLhss(copies[v]), MkExprs(new IdentifierExpr(Token.NoToken, v))));
+ drainedVars.Add(v);
+ }
+ callCmd.Ins = newIns;
+ newCmds.Add(callCmd);
+ foreach (Variable v in drainedVars)
+ {
+ Drain(newCmds, copies[v], varToDomainName[v]);
+ }
+ foreach (Variable v in drainedVars)
+ {
+ string domainName = varToDomainName[v];
+ newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ }
+
+ void TransformAssignCmd(CmdSeq newCmds, AssignCmd assignCmd, Dictionary<Variable, LocalVariable> copies)
+ {
+ List<Expr> newRhss = new List<Expr>();
+ for (int i = 0; i < assignCmd.Rhss.Count; i++)
+ {
+ IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr;
+ if (ie == null)
+ {
+ newRhss.Add(assignCmd.Rhss[i]);
+ continue;
+ }
+ Variable source = ie.Decl;
+ Variable target = assignCmd.Lhss[i].DeepAssignedVariable;
+ if (!varToDomainName.ContainsKey(source) || !varToDomainName.ContainsKey(target))
+ {
+ newRhss.Add(ie);
+ continue;
+ }
+ if (!copies.ContainsKey(source))
+ {
+ copies[source] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", source.Name), source.TypedIdent.Type));
+ }
+ newRhss.Add(new IdentifierExpr(Token.NoToken, copies[source]));
+ newCmds.Add(new AssignCmd(Token.NoToken, MkAssignLhss(copies[source], source), MkExprs(new IdentifierExpr(Token.NoToken, source), new NAryExpr(Token.NoToken, new FunctionCall(linearDomains[varToDomainName[source]].mapConstBool), new ExprSeq(Expr.False)))));
+ }
+ HashSet<Variable> drainedVars = new HashSet<Variable>();
+ foreach (AssignLhs lhs in assignCmd.Lhss)
+ {
+ Variable v = lhs.DeepAssignedVariable;
+ if (!varToDomainName.ContainsKey(v)) continue;
+ if (!copies.ContainsKey(v))
+ {
+ copies[v] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", v.Name), v.TypedIdent.Type));
+ }
+ newCmds.Add(new AssignCmd(Token.NoToken, MkAssignLhss(copies[v]), MkExprs(new IdentifierExpr(Token.NoToken, v))));
+ drainedVars.Add(v);
+ }
+ assignCmd.Rhss = newRhss;
+ newCmds.Add(assignCmd);
+ foreach (Variable v in drainedVars)
+ {
+ Drain(newCmds, copies[v], varToDomainName[v]);
+ }
+ }
+
+ 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 TypeVariableSeq(), new TypeSeq(domain.elementType), Microsoft.Boogie.Type.Int)));
+ Expr disjointExpr = Expr.True;
+ int count = 0;
+ foreach (Variable var in scope)
+ {
+ Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new ExprSeq(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++))));
+ e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new ExprSeq(new IdentifierExpr(Token.NoToken, partition), e));
+ e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new ExprSeq(new IdentifierExpr(Token.NoToken, var), e));
+ e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True)));
+ disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);
+ }
+ return new ExistsExpr(Token.NoToken, new VariableSeq(partition), disjointExpr);
+ }
+ }
+
+ class LinearDomain
+ {
+ public GlobalVariable allocator;
+ public Microsoft.Boogie.Type elementType;
+ public Function mapEqInt;
+ public Function mapConstInt;
+ public Function mapOrBool;
+ public Function mapImpBool;
+ public Function mapConstBool;
+
+ public LinearDomain(Program program, Variable var, string domainName)
+ {
+ this.allocator = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("allocator_{0}", domainName), var.TypedIdent.Type));
+ this.elementType = ((MapType)var.TypedIdent.Type).Arguments[0];
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Function func = decl as Function;
+ if (func == null) continue;
+ var name = QKeyValue.FindStringAttribute(func.Attributes, "builtin");
+ if (name == null) continue;
+ MapType mapType = func.OutParams[0].TypedIdent.Type as MapType;
+ if (mapType == null) continue;
+ if (mapType.Arguments.Length > 1) continue;
+ if (!mapType.Arguments[0].Equals(elementType)) continue;
+ if (mapType.Result.Equals(Microsoft.Boogie.Type.Bool))
+ {
+ if (name == "MapOr")
+ this.mapOrBool = func;
+ else if (name == "MapImp")
+ this.mapImpBool = func;
+ else if (name == "MapConst")
+ this.mapConstBool = func;
+ else if (name == "MapEq")
+ this.mapEqInt = func;
+ }
+ else if (mapType.Result.Equals(Microsoft.Boogie.Type.Int))
+ {
+ if (name == "MapConst")
+ this.mapConstInt = func;
+ }
+ }
+ }
+ }
+}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs new file mode 100644 index 00000000..8fa66704 --- /dev/null +++ b/Source/Core/OwickiGries.cs @@ -0,0 +1,401 @@ +using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.Boogie;
+
+namespace Microsoft.Boogie
+{
+ class ProcedureInfo
+ {
+ public bool hasImplementation;
+ public bool isAtomic;
+ public bool containsYield;
+ public bool isThreadStart;
+ public Procedure yieldCheckerProc;
+ public Implementation yieldCheckerImpl;
+ public Procedure dummyAsyncTargetProc;
+ public ProcedureInfo()
+ {
+ hasImplementation = false;
+ isAtomic = true;
+ containsYield = false;
+ isThreadStart = false;
+ yieldCheckerProc = null;
+ yieldCheckerImpl = null;
+ dummyAsyncTargetProc = null;
+ }
+ }
+
+ class AtomicTraverser : StandardVisitor
+ {
+ Implementation currentImpl;
+ static Dictionary<string, ProcedureInfo> procNameToInfo;
+ static bool moreProcessingRequired;
+ public static void Traverse(Program program, Dictionary<string, ProcedureInfo> procNameToInfo)
+ {
+ AtomicTraverser.procNameToInfo = procNameToInfo;
+ do
+ {
+ moreProcessingRequired = false;
+ AtomicTraverser traverser = new AtomicTraverser();
+ traverser.VisitProgram(program);
+ } while (moreProcessingRequired);
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ if (!procNameToInfo[node.Name].isAtomic)
+ return node;
+ currentImpl = node;
+ return base.VisitImplementation(node);
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ ProcedureInfo info = procNameToInfo[node.callee];
+ if (!info.isAtomic)
+ {
+ procNameToInfo[currentImpl.Name].isAtomic = false;
+ moreProcessingRequired = true;
+ }
+ return base.VisitCallCmd(node);
+ }
+ }
+
+ class AsyncAndYieldTraverser : StandardVisitor
+ {
+ Dictionary<string, ProcedureInfo> procNameToInfo = new Dictionary<string, ProcedureInfo>();
+ Implementation currentImpl = null;
+ public static Dictionary<string, ProcedureInfo> Traverse(Program program)
+ {
+ AsyncAndYieldTraverser traverser = new AsyncAndYieldTraverser();
+ traverser.VisitProgram(program);
+ return traverser.procNameToInfo;
+ }
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ if (!procNameToInfo.ContainsKey(node.Name))
+ {
+ procNameToInfo[node.Name] = new ProcedureInfo();
+ }
+ if (QKeyValue.FindBoolAttribute(node.Attributes, "entrypoint"))
+ {
+ procNameToInfo[node.Name].isThreadStart = true;
+ }
+ if (QKeyValue.FindBoolAttribute(node.Attributes, "yields"))
+ {
+ procNameToInfo[node.Name].containsYield = true;
+ procNameToInfo[node.Name].isAtomic = false;
+ }
+ return base.VisitProcedure(node);
+ }
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ currentImpl = node;
+ if (!procNameToInfo.ContainsKey(node.Name))
+ {
+ procNameToInfo[node.Name] = new ProcedureInfo();
+ }
+ procNameToInfo[node.Name].hasImplementation = true;
+ if (QKeyValue.FindBoolAttribute(node.Attributes, "entrypoint"))
+ {
+ procNameToInfo[node.Name].isThreadStart = true;
+ }
+ return base.VisitImplementation(node);
+ }
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ if (QKeyValue.FindBoolAttribute(node.Attributes, "yield") && !procNameToInfo[currentImpl.Name].containsYield)
+ {
+ procNameToInfo[currentImpl.Name].containsYield = true;
+ procNameToInfo[currentImpl.Name].isAtomic = false;
+ var yieldCheckerName = string.Format("YieldChecker_{0}", currentImpl.Name);
+ var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, currentImpl.TypeParameters, new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ procNameToInfo[currentImpl.Name].yieldCheckerProc = yieldCheckerProc;
+ }
+ return base.VisitAssertCmd(node);
+ }
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ if (!procNameToInfo.ContainsKey(node.Proc.Name))
+ {
+ procNameToInfo[node.Proc.Name] = new ProcedureInfo();
+ }
+ if (QKeyValue.FindBoolAttribute(node.Attributes, "async"))
+ {
+ procNameToInfo[node.Proc.Name].isThreadStart = true;
+ if (procNameToInfo[node.Proc.Name].dummyAsyncTargetProc == null)
+ {
+ var dummyAsyncTargetName = string.Format("DummyAsyncTarget_{0}", node.Proc.Name);
+ var dummyAsyncTargetProc = new Procedure(Token.NoToken, dummyAsyncTargetName, node.Proc.TypeParameters, node.Proc.InParams, node.Proc.OutParams, node.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());
+ procNameToInfo[node.Proc.Name].dummyAsyncTargetProc = dummyAsyncTargetProc;
+ }
+ }
+ return base.VisitCallCmd(node);
+ }
+ }
+
+ class OwickiGriesTransform
+ {
+ Dictionary<string, ProcedureInfo> procNameToInfo;
+ IdentifierExprSeq globalMods;
+ Hashtable globalMap;
+
+ public OwickiGriesTransform(Program program)
+ {
+ procNameToInfo = AsyncAndYieldTraverser.Traverse(program);
+ AtomicTraverser.Traverse(program, procNameToInfo);
+ globalMap = new Hashtable();
+ globalMods = new IdentifierExprSeq();
+ foreach (Variable g in program.GlobalVariables())
+ {
+ var oldg = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("old_{0}", g.Name), g.TypedIdent.Type));
+ globalMap[g] = new IdentifierExpr(Token.NoToken, oldg);
+ globalMods.Add(new IdentifierExpr(Token.NoToken, g));
+ }
+ }
+
+ private void AddCallsToYieldCheckers(CmdSeq newCmds)
+ {
+ foreach (ProcedureInfo info in procNameToInfo.Values)
+ {
+ if (info.containsYield)
+ {
+ CallCmd yieldCallCmd = new CallCmd(Token.NoToken, info.yieldCheckerProc.Name, new ExprSeq(), new IdentifierExprSeq());
+ yieldCallCmd.Proc = info.yieldCheckerProc;
+ newCmds.Add(yieldCallCmd);
+ }
+ }
+ }
+
+ private void AddUpdatesToOldGlobalVars(CmdSeq newCmds)
+ {
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ List<Expr> rhss = new List<Expr>();
+ foreach (Variable g in globalMap.Keys)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, (IdentifierExpr)globalMap[g]));
+ rhss.Add(new IdentifierExpr(Token.NoToken, g));
+ }
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ }
+
+ private void DesugarYield(CmdSeq cmds, CmdSeq newCmds)
+ {
+ AddCallsToYieldCheckers(newCmds);
+
+ newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
+
+ AddUpdatesToOldGlobalVars(newCmds);
+
+ for (int j = 0; j < cmds.Length; j++)
+ {
+ PredicateCmd predCmd = (PredicateCmd)cmds[j];
+ newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));
+ }
+ }
+
+ public void Transform(Program program)
+ {
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ if (procNameToInfo[impl.Name].isAtomic) continue;
+
+ // Add free requires
+ Expr freeRequiresExpr = Expr.True;
+ foreach (Variable g in globalMap.Keys)
+ {
+ freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)globalMap[g]));
+ }
+ impl.Proc.Requires.Add(new Requires(true, freeRequiresExpr));
+
+ // Create substitution maps
+ Hashtable map = new Hashtable();
+ VariableSeq locals = new VariableSeq();
+ foreach (Variable inParam in impl.Proc.InParams)
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
+ locals.Add(copy);
+ map[inParam] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ foreach (Variable outParam in impl.Proc.OutParams)
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);
+ locals.Add(copy);
+ map[outParam] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ foreach (Variable local in impl.LocVars)
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type), local.Attributes);
+ locals.Add(copy);
+ map[local] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ Hashtable oldMap = new Hashtable(map);
+ foreach (var global in globalMap.Keys)
+ {
+ oldMap[global] = globalMap[global];
+ }
+
+ // Collect the yield predicates and desugar yields
+ HashSet<CmdSeq> yields = new HashSet<CmdSeq>();
+ CmdSeq cmds = new CmdSeq();
+ if (procNameToInfo[impl.Name].isThreadStart && impl.Proc.Requires.Length > 0)
+ {
+ foreach (Requires r in impl.Proc.Requires)
+ {
+ if (r.Free) continue;
+ cmds.Add(new AssertCmd(Token.NoToken, r.Condition));
+ }
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ foreach (Block b in impl.Blocks)
+ {
+ bool insideYield = false;
+ CmdSeq newCmds = new CmdSeq();
+ for (int i = 0; i < b.Cmds.Length; i++)
+ {
+ PredicateCmd pcmd = b.Cmds[i] as PredicateCmd;
+ if (pcmd == null || QKeyValue.FindBoolAttribute(pcmd.Attributes, "yield"))
+ {
+ if (cmds.Length > 0)
+ {
+ DesugarYield(cmds, newCmds);
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ insideYield = (pcmd != null);
+ }
+ if (insideYield)
+ {
+ cmds.Add(pcmd);
+ }
+
+ CallCmd callCmd = b.Cmds[i] as CallCmd;
+ if (callCmd != null)
+ {
+ if (QKeyValue.FindBoolAttribute(callCmd.Attributes, "async"))
+ {
+ var dummyAsyncTargetProc = procNameToInfo[callCmd.callee].dummyAsyncTargetProc;
+ CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
+ dummyCallCmd.Proc = dummyAsyncTargetProc;
+ newCmds.Add(dummyCallCmd);
+ }
+ else if (procNameToInfo[callCmd.callee].isAtomic)
+ {
+ newCmds.Add(callCmd);
+ }
+ else
+ {
+ AddCallsToYieldCheckers(newCmds);
+ newCmds.Add(callCmd);
+ AddUpdatesToOldGlobalVars(newCmds);
+ }
+ }
+ else
+ {
+ newCmds.Add(b.Cmds[i]);
+ }
+ }
+ if (b.TransferCmd is ReturnCmd)
+ {
+ AddCallsToYieldCheckers(newCmds);
+ }
+ else if (cmds.Length > 0)
+ {
+ DesugarYield(cmds, newCmds);
+ yields.Add(cmds);
+ cmds = new CmdSeq();
+ }
+ b.Cmds = newCmds;
+ }
+
+ if (!procNameToInfo[impl.Name].containsYield) continue;
+
+ // Create the body of the yield checker procedure
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ List<Block> yieldCheckerBlocks = new List<Block>();
+ StringSeq labels = new StringSeq();
+ BlockSeq labelTargets = new BlockSeq();
+ Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ labels.Add(yieldCheckerBlock.Label);
+ labelTargets.Add(yieldCheckerBlock);
+ yieldCheckerBlocks.Add(yieldCheckerBlock);
+ int yieldCount = 0;
+ foreach (CmdSeq cs in yields)
+ {
+ CmdSeq newCmds = new CmdSeq();
+ foreach (Cmd cmd in cs)
+ {
+ PredicateCmd predCmd = (PredicateCmd)cmd;
+ newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.Apply(oldSubst, predCmd.Expr)));
+ }
+ foreach (Cmd cmd in cs)
+ {
+ PredicateCmd predCmd = (PredicateCmd)cmd;
+ var newExpr = Substituter.Apply(subst, predCmd.Expr);
+ if (predCmd is AssertCmd)
+ newCmds.Add(new AssertCmd(Token.NoToken, newExpr));
+ 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);
+ }
+ IdentifierExprSeq ieSeq = new IdentifierExprSeq();
+ foreach (Variable local in locals)
+ {
+ if (QKeyValue.FindStringAttribute(local.Attributes, "linear") != null)
+ {
+ ieSeq.Add(new IdentifierExpr(Token.NoToken, local));
+ }
+ }
+ CmdSeq initCmds;
+ if (ieSeq.Length == 0)
+ {
+ initCmds = new CmdSeq();
+ }
+ else
+ {
+ initCmds = new CmdSeq(new HavocCmd(Token.NoToken, ieSeq));
+ }
+
+ yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", initCmds, new GotoCmd(Token.NoToken, labels, labelTargets)));
+
+ // Create the yield checker implementation
+ var yieldCheckerImpl = new Implementation(Token.NoToken, procNameToInfo[impl.Name].yieldCheckerProc.Name, impl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);
+ yieldCheckerImpl.Proc = procNameToInfo[impl.Name].yieldCheckerProc;
+ yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ procNameToInfo[impl.Name].yieldCheckerImpl = yieldCheckerImpl;
+ }
+
+ foreach (Variable v in globalMap.Keys)
+ {
+ IdentifierExpr ie = (IdentifierExpr) globalMap[v];
+ program.TopLevelDeclarations.Add(ie.Decl);
+ }
+ foreach (ProcedureInfo info in procNameToInfo.Values)
+ {
+ if (info.containsYield)
+ {
+ program.TopLevelDeclarations.Add(info.yieldCheckerProc);
+ program.TopLevelDeclarations.Add(info.yieldCheckerImpl);
+ }
+ if (info.dummyAsyncTargetProc != null)
+ {
+ program.TopLevelDeclarations.Add(info.dummyAsyncTargetProc);
+ }
+ }
+ }
+ }
+}
|