diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-18 21:15:20 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-18 21:15:20 -0700 |
| commit | 64d8963508ce048d00db3766f4ca597b792c1b95 (patch) | |
| tree | 67801fe71cd2ceb7eb851833dd489751baa21ce2 /Source | |
| parent | 89b20adf23750478098578895fef9ca3b9170927 (diff) | |
reworked the linear and og implementation based on available variables theory
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 25 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 645 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 288 |
3 files changed, 512 insertions, 446 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 3e2b83de..f448bcd2 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -194,23 +194,16 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
{
- OwickiGriesTransform ogTransform = new OwickiGriesTransform(program);
+ OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker);
ogTransform.Transform();
+ var eraser = new LinearEraser();
+ eraser.VisitProgram(program);
int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
CommandLineOptions.Clo.PrintUnstructured = 1;
PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);
CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
}
- {
- LinearSetTransform linearTransform = new LinearSetTransform(program);
- linearTransform.Transform();
- //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
- //CommandLineOptions.Clo.PrintUnstructured = 1;
- //PrintBplFile("lsd.bpl", program, false, false);
- //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
- }
-
EliminateDeadVariablesAndInline(program);
if (CommandLineOptions.Clo.StagedHoudini > 0)
@@ -379,6 +372,8 @@ namespace Microsoft.Boogie { VerificationCompleted
}
+ static LinearTypechecker linearTypechecker;
+
/// <summary>
/// Resolves and type checks the given Boogie program. Any errors are reported to the
/// console. Returns:
@@ -414,9 +409,13 @@ namespace Microsoft.Boogie { return PipelineOutcome.TypeCheckingError;
}
- LinearTypechecker linearTypechecker = new LinearTypechecker();
- linearTypechecker.VisitProgram(program);
- if (linearTypechecker.errorCount > 0)
+ linearTypechecker = new LinearTypechecker(program);
+ linearTypechecker.Typecheck();
+ if (linearTypechecker.errorCount == 0)
+ {
+ linearTypechecker.Transform();
+ }
+ else
{
Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);
return PipelineOutcome.TypeCheckingError;
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 3f31a8aa..84ce264d 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -25,50 +25,182 @@ namespace Microsoft.Boogie public class LinearTypechecker : StandardVisitor
{
+ public Program program;
public int errorCount;
- CheckingContext checkingContext;
- Dictionary<string, Type> domainNameToType;
- public LinearTypechecker()
+ public CheckingContext checkingContext;
+ public Dictionary<string, Type> domainNameToType;
+ public Dictionary<Absy, HashSet<Variable>> availableLocalLinearVars;
+ public Dictionary<Variable, string> inoutParamToDomainName;
+ public Dictionary<Variable, string> varToDomainName;
+ 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.availableLocalLinearVars = 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++;
}
- private Dictionary<Variable, string> scope;
- private HashSet<Variable> frame;
public override Implementation VisitImplementation(Implementation node)
{
- scope = new Dictionary<Variable, string>();
- frame = new HashSet<Variable>();
- foreach (IdentifierExpr ie in node.Proc.Modifies)
+ HashSet<Variable> start = new HashSet<Variable>();
+ for (int i = 0; i < node.InParams.Length; i++)
{
- frame.Add(ie.Decl);
+ 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.Length; i++)
{
- string domainName = QKeyValue.FindStringAttribute(node.Proc.OutParams[i].Attributes, "linear");
+ string domainName = FindDomainName(node.Proc.OutParams[i]);
if (domainName != null)
{
- scope[node.OutParams[i]] = domainName;
+ inoutParamToDomainName[node.OutParams[i]] = domainName;
}
}
- return base.VisitImplementation(node);
+
+ 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>();
+ availableLocalLinearVars[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 (Variable v in node.OutParams)
+ {
+ if (FindDomainName(v) == null || end.Contains(v)) continue;
+ Error(b, "output variable must be available at a return");
+ }
+ }
+ if (b.TransferCmd is ReturnCmd) continue;
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ if (!availableLocalLinearVars.ContainsKey(target))
+ {
+ availableLocalLinearVars[target] = new HashSet<Variable>(end);
+ dfsStack.Push(target);
+ dfsStackAsSet.Add(target);
+ }
+ else
+ {
+ var savedAvailableVars = new HashSet<Variable>(availableLocalLinearVars[target]);
+ availableLocalLinearVars[target].IntersectWith(end);
+ if (savedAvailableVars.IsProperSupersetOf(availableLocalLinearVars[target]) && !dfsStackAsSet.Contains(target))
+ {
+ dfsStack.Push(target);
+ dfsStackAsSet.Add(target);
+ }
+ }
+ }
+ }
+ return impl;
}
- private string FindDomainName(Variable v)
+ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {
+ HashSet<Variable> start = new HashSet<Variable>(availableLocalLinearVars[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)
+ {
+ CallCmd callCmd = (CallCmd)cmd;
+ 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");
+ }
+ }
+ availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (FindDomainName(ie.Decl) == null) continue;
+ start.Add(ie.Decl);
+ }
+ }
+ 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)
+ {
+ availableLocalLinearVars[cmd] = new HashSet<Variable>(start);
+ }
+ }
+ return start;
+ }
+ public string FindDomainName(Variable v)
{
- if (scope.ContainsKey(v))
- return scope[v];
+ if (inoutParamToDomainName.ContainsKey(v))
+ return inoutParamToDomainName[v];
return QKeyValue.FindStringAttribute(v.Attributes, "linear");
}
public override Variable VisitVariable(Variable node)
{
- string domainName = QKeyValue.FindStringAttribute(node.Attributes, "linear");
+ string domainName = FindDomainName(node);
if (domainName != null)
{
Type type = node.TypedIdent.Type;
@@ -115,6 +247,11 @@ namespace Microsoft.Boogie Error(node, "Only simple assignment allowed on linear sets");
continue;
}
+ if (salhs.DeepAssignedVariable is GlobalVariable)
+ {
+ Error(node, "Linear global variable cannot be written to");
+ continue;
+ }
IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;
if (rhs == null)
{
@@ -134,14 +271,15 @@ namespace Microsoft.Boogie }
if (rhsVars.Contains(rhs.Decl))
{
- Error(node, "A linear set can occur only once in the rhs");
+ Error(node, "A linear variable can occur only once in the rhs");
continue;
}
- rhsVars.Add(rhs.Decl);
- if (!CommandLineOptions.Clo.DoModSetAnalysis && rhs.Decl is GlobalVariable && !frame.Contains(rhs.Decl))
+ if (rhs.Decl is GlobalVariable)
{
- Error(node, "A linear variable on the right hand side of an assignment must be in the modifies set");
+ Error(node, "Linear global variable cannot be read from");
+ continue;
}
+ rhsVars.Add(rhs.Decl);
}
return base.VisitAssignCmd(node);
}
@@ -152,7 +290,7 @@ namespace Microsoft.Boogie for (int i = 0; i < node.Proc.InParams.Length; i++)
{
Variable formal = node.Proc.InParams[i];
- string domainName = QKeyValue.FindStringAttribute(formal.Attributes, "linear");
+ string domainName = FindDomainName(formal);
if (domainName == null) continue;
IdentifierExpr actual = node.Ins[i] as IdentifierExpr;
if (actual == null)
@@ -190,7 +328,7 @@ namespace Microsoft.Boogie string actualDomainName = FindDomainName(actual.Decl);
if (actualDomainName == null) continue;
Variable formal = node.Proc.OutParams[i];
- string domainName = QKeyValue.FindStringAttribute(formal.Attributes, "linear");
+ string domainName = FindDomainName(formal);
if (domainName == null)
{
Error(node, "Only a linear variable can be passed to a linear parameter");
@@ -217,54 +355,43 @@ namespace Microsoft.Boogie }
return base.VisitCallCmd(node);
}
- }
-
- public 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)
+ private void TransformCallCmd(CallCmd callCmd, Dictionary<string, Expr> domainNameToExpr)
{
- var domainName = QKeyValue.FindStringAttribute(impl.Proc.OutParams[outParamIndex].Attributes, "linear");
- if (domainName == null) return;
- AddVariableToScopeHelper(impl.OutParams[outParamIndex], domainName, domainNameToScope);
+ foreach (var domainName in linearDomains.Keys)
+ {
+ callCmd.Ins.Add(domainNameToExpr[domainName]);
+ }
+ CallCmd parallelCallCmd = callCmd.InParallelWith;
+ if (parallelCallCmd != null)
+ {
+ TransformCallCmd(parallelCallCmd, domainNameToExpr);
+ }
}
- private void AddVariableToScopeHelper(Variable v, string domainName, Dictionary<string, HashSet<Variable>> domainNameToScope)
+ private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
{
- if (!varToDomainName.ContainsKey(v))
+ 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 program.GlobalVariables())
{
- varToDomainName[v] = domainName;
+ var domainName = FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
}
- if (!linearDomains.ContainsKey(domainName))
+ foreach (Variable v in availableLocalLinearVars[absy])
{
- var domain = new LinearDomain(program, v, domainName);
- linearDomains[domainName] = domain;
- varToDomainName[domain.allocator] = domainName;
- }
- if (!domainNameToScope.ContainsKey(domainName))
+ var domainName = FindDomainName(v);
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (string domainName in linearDomains.Keys)
{
- HashSet<Variable> scope = new HashSet<Variable>();
- scope.Add(linearDomains[domainName].allocator);
- domainNameToScope[domainName] = scope;
+ newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
}
- domainNameToScope[domainName].Add(v);
}
public void Transform()
@@ -273,58 +400,53 @@ namespace Microsoft.Boogie {
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)
+ Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
+ foreach (string domainName in linearDomains.Keys)
{
- AddVariableToScope(v, domainNameToScope);
+ var domain = linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);
+ impl.InParams.Add(f);
+ domainNameToInputVar[domainName] = f;
}
- 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, domainNameToScope);
- }
- else if (cmd is HavocCmd)
+ newCmds.Add(cmd);
+ if (cmd is CallCmd)
{
- HavocCmd havocCmd = (HavocCmd)cmd;
- foreach (IdentifierExpr ie in havocCmd.Vars)
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd.IsAsync)
{
- Variable v = ie.Decl;
- if (!varToDomainName.ContainsKey(v)) continue;
- Drain(newCmds, ie.Decl, varToDomainName[v]);
+ foreach (var domainName in linearDomains.Keys)
+ {
+ var domain = linearDomains[domainName];
+ callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)));
+ }
+ }
+ 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 availableLocalLinearVars[callCmd])
+ {
+ var domainName = FindDomainName(v);
+ var domain = linearDomains[domainName];
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName]));
+ }
+ TransformCallCmd(callCmd, domainNameToExpr);
}
- TransformHavocCmd(newCmds, havocCmd, copies, domainNameToScope);
}
- else if (cmd is CallCmd)
+ else if (cmd is YieldCmd)
{
- 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]);
+ AddDisjointnessExpr(newCmds, cmd, domainNameToInputVar);
}
}
b.Cmds = newCmds;
@@ -341,42 +463,12 @@ namespace Microsoft.Boogie 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])));
- }
+ AddDisjointnessExpr(newCmds, header, domainNameToInputVar);
newCmds.AddRange(header.Cmds);
header.Cmds = newCmds;
}
}
}
-
- {
- // Initialization
- CmdSeq newCmds = new CmdSeq();
- IdentifierExprSeq havocVars = new IdentifierExprSeq();
- foreach (Variable v in impl.OutParams)
- {
- if (!varToDomainName.ContainsKey(v)) continue;
- havocVars.Add(new IdentifierExpr(Token.NoToken, v));
- }
- foreach (Variable v in impl.LocVars)
- {
- if (!varToDomainName.ContainsKey(v)) continue;
- havocVars.Add(new IdentifierExpr(Token.NoToken, v));
- }
- if (havocVars.Length > 0)
- {
- TransformHavocCmd(newCmds, new HavocCmd(Token.NoToken, havocVars), copies, domainNameToScope);
- }
- newCmds.AddRange(impl.Blocks[0].Cmds);
- impl.Blocks[0].Cmds = newCmds;
- }
-
- foreach (var v in copies.Values)
- {
- impl.LocVars.Add(v);
- }
}
foreach (var decl in program.TopLevelDeclarations)
@@ -384,86 +476,46 @@ namespace Microsoft.Boogie Procedure proc = decl as Procedure;
if (proc == null) continue;
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (Variable v in program.GlobalVariables())
+ 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)
{
- AddVariableToScope(v, domainNameToScope);
+ domainNameToInputScope[domainName] = new HashSet<Variable>();
+ domainNameToOutputScope[domainName] = new HashSet<Variable>();
+
}
- foreach (string domainName in domainNameToScope.Keys)
+ foreach (Variable v in program.GlobalVariables())
{
- proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ var domainName = FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToInputScope[domainName].Add(v);
+ domainNameToOutputScope[domainName].Add(v);
}
- Dictionary<string, HashSet<Variable>> domainNameToInParams = new Dictionary<string, HashSet<Variable>>();
foreach (Variable v in proc.InParams)
{
- var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");
+ var domainName = FindDomainName(v);
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];
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), 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])));
+ domainNameToInputScope[domainName].Add(v);
}
- Dictionary<string, HashSet<Variable>> domainNameToOutParams = new Dictionary<string, HashSet<Variable>>();
foreach (Variable v in proc.OutParams)
{
- var domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");
+ var domainName = FindDomainName(v);
if (domainName == null) continue;
- if (!linearDomains.ContainsKey(domainName))
- {
- linearDomains[domainName] = new LinearDomain(program, v, domainName);
- }
- if (!domainNameToOutParams.ContainsKey(domainName))
- {
- domainNameToOutParams[domainName] = new HashSet<Variable>();
- }
- domainNameToOutParams[domainName].Add(v);
+ domainNameToOutputScope[domainName].Add(v);
}
- foreach (string domainName in linearDomains.Keys)
+ foreach (var domainName in linearDomains.Keys)
{
- LinearDomain domain = linearDomains[domainName];
- var allocator = domain.allocator;
- proc.Modifies.Add(new IdentifierExpr(Token.NoToken, allocator));
- Expr oldExpr = new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, allocator));
- Expr newExpr = new IdentifierExpr(Token.NoToken, allocator);
- if (domainNameToScope.ContainsKey(domainName))
- {
- foreach (Variable v in domainNameToScope[domainName])
- {
- Expr oldVarExpr = new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v));
- Expr newVarExpr = new IdentifierExpr(Token.NoToken, v);
- oldExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? oldVarExpr : Singleton(oldVarExpr, domainName), oldExpr));
- newExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? newVarExpr : Singleton(newVarExpr, domainName), newExpr));
- }
- }
- if (domainNameToOutParams.ContainsKey(domainName))
- {
- foreach (Variable v in domainNameToOutParams[domainName])
- {
- Expr newVarExpr = new IdentifierExpr(Token.NoToken, v);
- newExpr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? newVarExpr : Singleton(newVarExpr, domainName), newExpr));
- }
- }
- proc.Ensures.Add(new Ensures(true, Expr.Binary(BinaryOperator.Opcode.Eq, oldExpr, newExpr)));
+ proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));
+ var domain = linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(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.allocator);
program.TopLevelDeclarations.Add(domain.mapConstBool);
program.TopLevelDeclarations.Add(domain.mapConstInt);
program.TopLevelDeclarations.Add(domain.mapEqInt);
@@ -475,28 +527,18 @@ namespace Microsoft.Boogie }
}
- var eraser = new LinearEraser();
- eraser.VisitProgram(program);
+ //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ //CommandLineOptions.Clo.PrintUnstructured = 1;
+ //PrintBplFile("lsd.bpl", program, false, false);
+ //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
}
- private Expr Singleton(Expr e, string domainName)
+ public Expr Singleton(Expr e, string domainName)
{
var domain = linearDomains[domainName];
return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)), e, Expr.True);
}
- void Drain(CmdSeq newCmds, Variable v, string domainName)
- {
- var domain = linearDomains[domainName];
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- List<AssignLhs> lhss = MkAssignLhss(domain.allocator);
- List<Expr> rhss =
- v.TypedIdent.Type is MapType
- ? MkExprs(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(new IdentifierExpr(Token.NoToken, domain.allocator), ie)))
- : MkExprs(Expr.Store(new IdentifierExpr(Token.NoToken, domain.allocator), ie, Expr.True));
- newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
- }
-
List<AssignLhs> MkAssignLhss(params Variable[] args)
{
List<AssignLhs> lhss = new List<AssignLhs>();
@@ -512,173 +554,7 @@ namespace Microsoft.Boogie 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>>();
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- foreach (IdentifierExpr ie in havocCmd.Vars)
- {
- Variable v = ie.Decl;
- if (!varToDomainName.ContainsKey(v)) continue;
- var domainName = varToDomainName[v];
- var allocator = linearDomains[domainName].allocator;
- if (!copies.ContainsKey(allocator))
- {
- copies[allocator] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", allocator.Name), allocator.TypedIdent.Type));
- }
- if (!domainNameToHavocVars.ContainsKey(domainName))
- {
- domainNameToHavocVars[domainName] = new HashSet<Variable>();
- lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));
- rhss.Add(new IdentifierExpr(Token.NoToken, allocator));
- }
- domainNameToHavocVars[domainName].Add(v);
- }
- if (lhss.Count > 0)
- {
- newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
- }
- foreach (string domainName in domainNameToHavocVars.Keys)
- {
- var allocator = linearDomains[domainName].allocator;
- havocCmd.Vars.Add(new IdentifierExpr(Token.NoToken, allocator));
- }
- newCmds.Add(havocCmd);
- foreach (string domainName in domainNameToHavocVars.Keys)
- {
- var domain = linearDomains[domainName];
- var allocator = domain.allocator;
- Expr oldExpr = new IdentifierExpr(Token.NoToken, copies[allocator]);
- Expr expr = new IdentifierExpr(Token.NoToken, allocator);
- foreach (var v in domainNameToHavocVars[domainName])
- {
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
- expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), 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)
- {
- Dictionary<string, HashSet<Variable>> domainNameToRhsVars = new Dictionary<string, HashSet<Variable>>();
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- for (int i = 0; i < callCmd.Proc.InParams.Length; i++)
- {
- if (QKeyValue.FindStringAttribute(callCmd.Proc.InParams[i].Attributes, "linear") == null) continue;
- IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
- Variable source = ie.Decl;
- var domainName = varToDomainName[source];
- var allocator = linearDomains[domainName].allocator;
- if (!copies.ContainsKey(allocator))
- {
- copies[allocator] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", allocator.Name), allocator.TypedIdent.Type));
- }
- if (!copies.ContainsKey(source))
- {
- copies[source] = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("copy_{0}", source.Name), source.TypedIdent.Type));
- }
- if (!domainNameToRhsVars.ContainsKey(domainName))
- {
- domainNameToRhsVars[domainName] = new HashSet<Variable>();
- lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[allocator])));
- rhss.Add(new IdentifierExpr(Token.NoToken, allocator));
- }
- domainNameToRhsVars[domainName].Add(source);
- lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, copies[source])));
- rhss.Add(new IdentifierExpr(Token.NoToken, source));
- callCmd.Ins[i] = new IdentifierExpr(Token.NoToken, copies[source]);
- }
- newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
-
- HashSet<Variable> lhsVars = new HashSet<Variable>();
- HashSet<string> lhsDomainNames = new HashSet<string>();
- foreach (IdentifierExpr ie in callCmd.Outs)
- {
- Variable v = ie.Decl;
- if (!varToDomainName.ContainsKey(v)) continue;
- lhsVars.Add(v);
- lhsDomainNames.Add(varToDomainName[v]);
- }
-
- foreach (var domainName in domainNameToRhsVars.Keys)
- {
- var domain = linearDomains[domainName];
- HashSet<Variable> scope = new HashSet<Variable>();
- IdentifierExprSeq havocExprs = new IdentifierExprSeq();
- foreach (Variable v in domainNameToRhsVars[domainName])
- {
- if (lhsVars.Contains(v)) continue;
- havocExprs.Add(new IdentifierExpr(Token.NoToken, v));
- scope.Add(v);
- }
- if (havocExprs.Length > 0)
- {
- scope.Add(domain.allocator);
- havocExprs.Add(new IdentifierExpr(Token.NoToken, domain.allocator));
- newCmds.Add(new HavocCmd(Token.NoToken, havocExprs));
- newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, scope)));
- Expr expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False));
- foreach (IdentifierExpr ie in havocExprs)
- {
- expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(ie.Decl.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), expr));
- }
- expr = Expr.Binary(BinaryOperator.Opcode.Eq, expr, new IdentifierExpr(Token.NoToken, copies[domain.allocator]));
- newCmds.Add(new AssumeCmd(Token.NoToken, expr));
- foreach (Variable v in scope)
- {
- if (v == domain.allocator) continue;
- Drain(newCmds, copies[v], varToDomainName[v]);
- }
- }
- }
-
- foreach (Variable v in lhsVars)
- {
- Drain(newCmds, v, varToDomainName[v]);
- }
-
- newCmds.Add(callCmd);
-
- foreach (string domainName in lhsDomainNames)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
- }
- }
-
- void TransformAssignCmd(CmdSeq newCmds, AssignCmd assignCmd, Dictionary<Variable, LocalVariable> copies, Dictionary<string, HashSet<Variable>> domainNameToScope)
- {
- HashSet<Variable> rhsVars = new HashSet<Variable>();
- HashSet<Variable> lhsVars = new HashSet<Variable>();
- for (int i = 0; i < assignCmd.Lhss.Count; i++)
- {
- Variable target = assignCmd.Lhss[i].DeepAssignedVariable;
- if (!varToDomainName.ContainsKey(target)) continue;
- IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr;
- Variable source = ie.Decl;
- rhsVars.Add(source);
- lhsVars.Add(target);
- }
- foreach (Variable v in lhsVars.Except(rhsVars))
- {
- Drain(newCmds, v, varToDomainName[v]);
- }
- newCmds.Add(assignCmd);
- IdentifierExprSeq havocExprs = new IdentifierExprSeq();
- foreach (Variable v in rhsVars.Except(lhsVars))
- {
- havocExprs.Add(new IdentifierExpr(Token.NoToken, v));
- }
- if (havocExprs.Length > 0)
- {
- TransformHavocCmd(newCmds, new HavocCmd(Token.NoToken, havocExprs), copies, domainNameToScope);
- }
- }
-
- Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)
+ 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 TypeVariableSeq(), new TypeSeq(domain.elementType), Microsoft.Boogie.Type.Int)));
@@ -697,9 +573,8 @@ namespace Microsoft.Boogie }
}
- class LinearDomain
+ public class LinearDomain
{
- public GlobalVariable allocator;
public Microsoft.Boogie.Type elementType;
public Function mapEqInt;
public Function mapConstInt;
@@ -708,20 +583,14 @@ namespace Microsoft.Boogie public Function mapConstBool;
public List<Axiom> axioms;
- public LinearDomain(Program program, Variable var, string domainName)
+ public LinearDomain(Program program, string domainName, Type elementType)
{
- this.elementType = var.TypedIdent.Type;
- if (var.TypedIdent.Type is MapType)
- {
- MapType mapType = (MapType)var.TypedIdent.Type;
- this.elementType = mapType.Arguments[0];
- }
- this.allocator = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("allocator_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool)));
+ this.elementType = elementType;
this.axioms = new List<Axiom>();
MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool);
MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Int);
- this.mapOrBool = new Function(Token.NoToken, "linear@MapOr",
+ this.mapOrBool = new Function(Token.NoToken, domainName + "_linear_MapOr",
new VariableSeq(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));
@@ -749,7 +618,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
- this.mapImpBool = new Function(Token.NoToken, "linear@MapImp",
+ this.mapImpBool = new Function(Token.NoToken, domainName + "_linear_MapImp",
new VariableSeq(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));
@@ -777,7 +646,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
- this.mapConstBool = new Function(Token.NoToken, "linear@MapConstBool",
+ this.mapConstBool = new Function(Token.NoToken, domainName + "_linear_MapConstBool",
new VariableSeq(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)
@@ -800,7 +669,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));
}
- this.mapEqInt = new Function(Token.NoToken, "linear@MapEq",
+ this.mapEqInt = new Function(Token.NoToken, domainName + "_linear_MapEq",
new VariableSeq(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));
@@ -828,7 +697,7 @@ namespace Microsoft.Boogie axioms.Add(new Axiom(Token.NoToken, axiomExpr));
}
- this.mapConstInt = new Function(Token.NoToken, "linear@MapConstInt",
+ this.mapConstInt = new Function(Token.NoToken, domainName + "_linear_MapConstInt",
new VariableSeq(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)
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 949efab4..f93fe198 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -30,7 +30,18 @@ namespace Microsoft.Boogie inParallelCall = false;
}
}
-
+ /*
+ struct YieldInfo
+ {
+ public YieldCmd yieldCmd;
+ public CmdSeq cmds;
+ public YieldInfo(YieldCmd yieldCmd, CmdSeq cmds)
+ {
+ this.yieldCmd = yieldCmd;
+ this.cmds = cmds;
+ }
+ }
+ */
class AsyncAndYieldTraverser : StandardVisitor
{
Dictionary<string, ProcedureInfo> procNameToInfo = new Dictionary<string, ProcedureInfo>();
@@ -145,15 +156,16 @@ namespace Microsoft.Boogie Dictionary<string, ProcedureInfo> procNameToInfo;
IdentifierExprSeq globalMods;
Hashtable ogOldGlobalMap;
- Program program;
+ LinearTypechecker linearTypechecker;
Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
List<Procedure> yieldCheckerProcs;
List<Implementation> yieldCheckerImpls;
Procedure yieldProc;
- public OwickiGriesTransform(Program program)
+ public OwickiGriesTransform(LinearTypechecker linearTypechecker)
{
- this.program = program;
+ this.linearTypechecker = linearTypechecker;
+ Program program = linearTypechecker.program;
procNameToInfo = AsyncAndYieldTraverser.Traverse(program);
AtomicTraverser.Traverse(program, procNameToInfo);
ogOldGlobalMap = new Hashtable();
@@ -167,18 +179,47 @@ namespace Microsoft.Boogie asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
yieldCheckerProcs = new List<Procedure>();
yieldCheckerImpls = new List<Implementation>();
- yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ VariableSeq inputs = new VariableSeq();
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ var domain = linearTypechecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);
+ inputs.Add(f);
+ }
+ yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
}
- private void AddCallToYieldProc(CmdSeq newCmds)
+ private void AddCallToYieldProc(CmdSeq newCmds, Dictionary<string, Variable> domainNameToLocalVar)
{
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, new ExprSeq(), new IdentifierExprSeq());
+ ExprSeq exprSeq = new ExprSeq();
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ exprSeq.Add(new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName]));
+ }
+ CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new IdentifierExprSeq());
yieldCallCmd.Proc = yieldProc;
newCmds.Add(yieldCallCmd);
}
- private void AddUpdatesToOldGlobalVars(CmdSeq newCmds)
+ private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLocalLinearVars, Dictionary<string, Variable> domainNameToInputVar)
+ {
+ Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
+ foreach (var domainName in linearTypechecker.linearDomains.Keys)
+ {
+ domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
+ }
+ foreach (Variable v in availableLocalLinearVars)
+ {
+ var domainName = linearTypechecker.FindDomainName(v);
+ var domain = linearTypechecker.linearDomains[domainName];
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName]));
+ }
+ return domainNameToExpr;
+ }
+
+ private void AddUpdatesToOldGlobalVars(CmdSeq newCmds, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
{
if (ogOldGlobalMap.Count == 0) return;
List<AssignLhs> lhss = new List<AssignLhs>();
@@ -189,17 +230,27 @@ namespace Microsoft.Boogie rhss.Add(new IdentifierExpr(Token.NoToken, g));
}
newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+
+ lhss = new List<AssignLhs>();
+ 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]);
+ }
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
}
- private void DesugarYield(CmdSeq cmds, CmdSeq newCmds)
+ private void DesugarYield(YieldCmd yieldCmd, CmdSeq cmds, CmdSeq newCmds, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
{
- AddCallToYieldProc(newCmds);
+ AddCallToYieldProc(newCmds, domainNameToLocalVar);
if (globalMods.Length > 0)
{
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
}
- AddUpdatesToOldGlobalVars(newCmds);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);
+ AddUpdatesToOldGlobalVars(newCmds, domainNameToLocalVar, domainNameToExpr);
for (int j = 0; j < cmds.Length; j++)
{
@@ -274,10 +325,10 @@ namespace Microsoft.Boogie return proc;
}
- private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, VariableSeq locals, Hashtable map, Hashtable assumeMap, Hashtable ogOldLocalMap)
+ private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, VariableSeq inputs, VariableSeq locals, Hashtable map, Hashtable assumeMap, Hashtable ogOldLocalMap)
{
if (yields.Count == 0) return;
-
+ Program program = linearTypechecker.program;
ProcedureInfo info = procNameToInfo[decl.Name];
Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
@@ -292,6 +343,7 @@ namespace Microsoft.Boogie int yieldCount = 0;
foreach (CmdSeq cs in yields)
{
+ var linearDomains = linearTypechecker.linearDomains;
CmdSeq newCmds = new CmdSeq();
foreach (Cmd cmd in cs)
{
@@ -317,12 +369,12 @@ namespace Microsoft.Boogie // 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, new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
+ var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
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, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);
+ var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), locals, yieldCheckerBlocks);
yieldCheckerImpl.Proc = yieldCheckerProc;
yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
yieldCheckerImpls.Add(yieldCheckerImpl);
@@ -330,6 +382,7 @@ namespace Microsoft.Boogie private void TransformImpl(Implementation impl)
{
+ Program program = linearTypechecker.program;
ProcedureInfo info = procNameToInfo[impl.Name];
// Add free requires
@@ -346,14 +399,31 @@ namespace Microsoft.Boogie // Create substitution maps
Hashtable map = new Hashtable();
VariableSeq locals = new VariableSeq();
- for (int i = 0; i < impl.Proc.InParams.Length; i++)
+ VariableSeq inputs = new VariableSeq();
+ Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
+ Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();
+ int count = 0;
+ while (count < impl.Proc.InParams.Length - linearTypechecker.linearDomains.Count)
{
- Variable inParam = impl.Proc.InParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
- var ie = new IdentifierExpr(Token.NoToken, copy);
+ Variable inParam = impl.Proc.InParams[count];
+ Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
locals.Add(copy);
- map[impl.InParams[i]] = ie;
+ map[impl.InParams[count]] = new IdentifierExpr(Token.NoToken, copy);
+ count++;
+ }
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ Variable inParam = impl.Proc.InParams[count];
+ Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
+ domainNameToInputVar[domainName] = copy;
+ inputs.Add(copy);
+ Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));
+ domainNameToLocalVar[domainName] = l;
+ impl.LocVars.Add(l);
+ map[impl.InParams[count]] = new IdentifierExpr(Token.NoToken, copy);
+ count++;
}
+
for (int i = 0; i < impl.Proc.OutParams.Length; i++)
{
Variable outParam = impl.Proc.OutParams[i];
@@ -387,28 +457,28 @@ namespace Microsoft.Boogie CmdSeq cmds = new CmdSeq();
foreach (Block b in impl.Blocks)
{
- bool insideYield = false;
+ YieldCmd yieldCmd = null;
CmdSeq newCmds = new CmdSeq();
for (int i = 0; i < b.Cmds.Length; i++)
{
Cmd cmd = b.Cmds[i];
if (cmd is YieldCmd)
{
- insideYield = true;
+ yieldCmd = (YieldCmd)cmd;
continue;
}
- if (insideYield)
+ if (yieldCmd != null)
{
PredicateCmd pcmd = cmd as PredicateCmd;
if (pcmd == null)
{
- DesugarYield(cmds, newCmds);
+ DesugarYield(yieldCmd, cmds, newCmds, domainNameToInputVar, domainNameToLocalVar);
if (cmds.Length > 0)
{
yields.Add(cmds);
cmds = new CmdSeq();
}
- insideYield = false;
+ yieldCmd = null;
}
else
{
@@ -444,9 +514,16 @@ namespace Microsoft.Boogie }
else
{
- AddCallToYieldProc(newCmds);
+ AddCallToYieldProc(newCmds, domainNameToLocalVar);
newCmds.Add(callCmd);
- AddUpdatesToOldGlobalVars(newCmds);
+ HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (linearTypechecker.FindDomainName(ie.Decl) == null) continue;
+ availableLocalLinearVars.Add(ie.Decl);
+ }
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLocalLinearVars, domainNameToInputVar);
+ AddUpdatesToOldGlobalVars(newCmds, domainNameToLocalVar, domainNameToExpr);
}
}
else
@@ -454,9 +531,9 @@ namespace Microsoft.Boogie newCmds.Add(cmd);
}
}
- if (insideYield)
+ if (yieldCmd != null)
{
- DesugarYield(cmds, newCmds);
+ DesugarYield(yieldCmd, cmds, newCmds, domainNameToInputVar, domainNameToLocalVar);
if (cmds.Length > 0)
{
yields.Add(cmds);
@@ -465,7 +542,7 @@ namespace Microsoft.Boogie }
if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))
{
- AddCallToYieldProc(newCmds);
+ AddCallToYieldProc(newCmds, domainNameToLocalVar);
}
b.Cmds = newCmds;
}
@@ -481,39 +558,87 @@ namespace Microsoft.Boogie {
foreach (Block header in g.Headers)
{
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);
foreach (Block pred in header.Predecessors)
{
- AddCallToYieldProc(pred.Cmds);
- AddUpdatesToOldGlobalVars(pred.Cmds);
+ AddCallToYieldProc(pred.Cmds, domainNameToLocalVar);
+ AddUpdatesToOldGlobalVars(pred.Cmds, domainNameToLocalVar, domainNameToExpr);
}
CmdSeq newCmds = new CmdSeq();
foreach (Variable v in ogOldGlobalMap.Keys)
{
newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), (IdentifierExpr)ogOldGlobalMap[v])));
}
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
+ }
newCmds.AddRange(header.Cmds);
header.Cmds = newCmds;
}
}
}
- CreateYieldCheckerImpl(impl, yields, locals, map, assumeMap, ogOldLocalMap);
+
+ {
+ // Add initial block
+ 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.Proc.InParams.Length - 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 ExprSeq(v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName]));
+ }
+ CmdSeq initCmds = new CmdSeq();
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ List<Expr> rhss = new List<Expr>();
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));
+ rhss.Add(domainNameToExpr[domainName]);
+ }
+ initCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ Block initBlock = new Block(Token.NoToken, "linear_init", initCmds, new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0])));
+ impl.Blocks.Insert(0, initBlock);
+ }
+
+ CreateYieldCheckerImpl(impl, yields, inputs, locals, map, assumeMap, ogOldLocalMap);
}
public void TransformProc(Procedure proc)
{
+ Program program = linearTypechecker.program;
ProcedureInfo info = procNameToInfo[proc.Name];
if (!info.isThreadStart) return;
// Create substitution maps
Hashtable map = new Hashtable();
VariableSeq locals = new VariableSeq();
- for (int i = 0; i < proc.InParams.Length; i++)
+ VariableSeq inputs = new VariableSeq();
+ Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
+ int count = 0;
+ while (count < proc.InParams.Length - linearTypechecker.linearDomains.Count)
{
- Variable inParam = proc.InParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
- var ie = new IdentifierExpr(Token.NoToken, copy);
+ Variable inParam = proc.InParams[count];
+ Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
locals.Add(copy);
- map[proc.InParams[i]] = ie;
+ map[proc.InParams[count]] = new IdentifierExpr(Token.NoToken, copy);
+ count++;
+ }
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ Variable inParam = proc.InParams[count];
+ Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
+ domainNameToInputVar[domainName] = copy;
+ inputs.Add(copy);
+ map[proc.InParams[count]] = new IdentifierExpr(Token.NoToken, copy);
+ count++;
}
for (int i = 0; i < proc.OutParams.Length; i++)
{
@@ -542,29 +667,95 @@ namespace Microsoft.Boogie CmdSeq cmds = new CmdSeq();
if (proc.Requires.Length > 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.Length - 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) continue;
- cmds.Add(new AssertCmd(r.tok, r.Condition));
+ if (r.Free)
+ {
+ cmds.Add(new AssumeCmd(r.tok, r.Condition));
+ }
+ else
+ {
+ cmds.Add(new AssertCmd(r.tok, r.Condition));
+ }
}
yields.Add(cmds);
cmds = new CmdSeq();
}
if (info.inParallelCall && proc.Ensures.Length > 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.Length; 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) continue;
- cmds.Add(new AssertCmd(e.tok, e.Condition));
+ if (e.Free)
+ {
+ cmds.Add(new AssumeCmd(e.tok, e.Condition));
+ }
+ else
+ {
+ cmds.Add(new AssertCmd(e.tok, e.Condition));
+ }
}
yields.Add(cmds);
cmds = new CmdSeq();
}
- CreateYieldCheckerImpl(proc, yields, locals, map, assumeMap, ogOldLocalMap);
+ CreateYieldCheckerImpl(proc, yields, inputs, locals, map, assumeMap, ogOldLocalMap);
}
private void AddYieldProcAndImpl()
{
+ Program program = linearTypechecker.program;
+ VariableSeq inputs = new VariableSeq();
+ foreach (string domainName in linearTypechecker.linearDomains.Keys)
+ {
+ var domain = linearTypechecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(domain.elementType), Type.Bool)), true);
+ inputs.Add(f);
+ }
List<Block> blocks = new List<Block>();
TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
if (yieldCheckerProcs.Count > 0)
@@ -574,7 +765,12 @@ namespace Microsoft.Boogie int labelCount = 0;
foreach (Procedure proc in yieldCheckerProcs)
{
- CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, new ExprSeq(), new IdentifierExprSeq());
+ ExprSeq exprSeq = new ExprSeq();
+ foreach (Variable v in inputs)
+ {
+ exprSeq.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new IdentifierExprSeq());
callCmd.Proc = proc;
string label = string.Format("L_{0}", labelCount++);
Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));
@@ -585,7 +781,8 @@ namespace Microsoft.Boogie transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);
}
blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd));
- var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), blocks);
+
+ var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new VariableSeq(), new VariableSeq(), blocks);
yieldImpl.Proc = yieldProc;
yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
program.TopLevelDeclarations.Add(yieldProc);
@@ -594,6 +791,7 @@ namespace Microsoft.Boogie public void Transform()
{
+ Program program = linearTypechecker.program;
foreach (var decl in program.TopLevelDeclarations)
{
Procedure proc = decl as Procedure;
|