diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 25 | ||||
| -rw-r--r-- | Source/Core/LinearSets.cs | 645 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 288 | ||||
| -rw-r--r-- | Test/linear/allocator.bpl | 2 | ||||
| -rw-r--r-- | Test/linear/f1.bpl | 6 | ||||
| -rw-r--r-- | Test/linear/f2.bpl | 3 | ||||
| -rw-r--r-- | Test/linear/typecheck.bpl | 6 | ||||
| -rw-r--r-- | Test/og/Answer | 24 | ||||
| -rw-r--r-- | Test/og/DeviceCacheSimplified.bpl | 16 | ||||
| -rw-r--r-- | Test/og/FlanaganQadeer.bpl | 11 | ||||
| -rw-r--r-- | Test/og/akash.bpl | 26 | ||||
| -rw-r--r-- | Test/og/linear-set.bpl | 14 | ||||
| -rw-r--r-- | Test/og/linear-set2.bpl | 17 | ||||
| -rw-r--r-- | Test/og/new1.bpl | 38 | ||||
| -rw-r--r-- | Test/og/parallel2.bpl | 10 | ||||
| -rw-r--r-- | Test/og/parallel4.bpl | 6 | ||||
| -rw-r--r-- | Test/og/parallel5.bpl | 10 | ||||
| -rw-r--r-- | Test/og/perm.bpl | 50 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/og/t1.bpl | 26 |
20 files changed, 714 insertions, 511 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;
diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl index 4b162a83..d723cbed 100644 --- a/Test/linear/allocator.bpl +++ b/Test/linear/allocator.bpl @@ -3,7 +3,7 @@ procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int); procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
call i := A(i);
assert false;
}
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl index 0d9189ab..1f451daf 100644 --- a/Test/linear/f1.bpl +++ b/Test/linear/f1.bpl @@ -24,9 +24,7 @@ procedure {:entrypoint} main({:linear "1"} x_in: [int]bool) requires b1 ==> x_in != mapconstbool(false);
{
var {:linear "1"} x: [int] bool;
- assume x == x_in;
-
- assume x == mapconstbool(true);
+ x := x_in;
call foo(x);
@@ -40,7 +38,7 @@ procedure foo({:linear "1"} x_in: [int]bool) requires b3 ==> x_in != mapconstbool(false);
{
var {:linear "1"} x: [int] bool;
- assume x == x_in;
+ x := x_in;
assert b4 ==> x == mapconstbool(true);
assert b5 ==> x != mapconstbool(false);
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl index 4e4bfbcf..82871466 100644 --- a/Test/linear/f2.bpl +++ b/Test/linear/f2.bpl @@ -4,6 +4,7 @@ function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool; procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);
+procedure Allocate() returns ({:linear "1"} x: [int]bool);
procedure {:entrypoint} main()
{
@@ -11,7 +12,7 @@ procedure {:entrypoint} main() var {:linear "1"} x1: [int] bool;
var {:linear "1"} x2: [int] bool;
- havoc x;
+ call x := Allocate();
assume x == mapconstbool(true);
call x1, x2 := Split(x);
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index ff2d7da4..7bdb339e 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -74,3 +74,9 @@ procedure G(i:int) returns({:linear "x"} r:int) {
r := g;
}
+
+procedure H(i:int) returns({:linear "x"} r:int)
+modifies g;
+{
+ g := r;
+}
diff --git a/Test/og/Answer b/Test/og/Answer index 9df32aee..c29d38dc 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -60,11 +60,10 @@ Boogie program verifier finished with 5 verified, 0 errors Boogie program verifier finished with 4 verified, 0 errors
-------------------- parallel4.bpl --------------------
-parallel4.bpl(14,3): Error BP5001: This assertion might not hold.
+parallel4.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- parallel4.bpl(12,3): anon0
- (0,0): inline$og_yield$0$Return
- parallel4.bpl(12,3): anon0$1
+ parallel4.bpl(16,5): anon0
+ parallel4.bpl(16,5): anon0$1
Boogie program verifier finished with 2 verified, 1 error
@@ -85,12 +84,17 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 3 verified, 0 errors
-------------------- t1.bpl --------------------
-t1.bpl(25,5): Error BP5001: This assertion might not hold.
+t1.bpl(35,5): Error BP5001: This assertion might not hold.
Execution trace:
- t1.bpl(11,5): anon0
- (0,0): inline$Proc_YieldChecker_B$0$Return
- (0,0): inline$og_yield$0$L_0$1
- (0,0): inline$og_yield$0$Return
- t1.bpl(11,5): anon0$1
+ t1.bpl(53,13): anon0
+ (0,0): inline$Impl_YieldChecker_A$0$L1
Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- new1.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
+
+-------------------- perm.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl index 68387356..d231e17c 100644 --- a/Test/og/DeviceCacheSimplified.bpl +++ b/Test/og/DeviceCacheSimplified.bpl @@ -12,7 +12,7 @@ ensures Inv(ghostLock, currsize, newsize); ensures old(currsize) <= currsize;
ensures tid == tid';
{
- assume tid == tid';
+ tid := tid';
yield;
assert Inv(ghostLock, currsize, newsize);
assert old(currsize) <= currsize;
@@ -31,7 +31,7 @@ ensures ghostLock == tid; ensures currsize <= i;
ensures newsize == old(newsize);
{
- assume tid == tid';
+ tid := tid';
yield;
assert Inv(ghostLock, currsize, newsize);
assert old(currsize) <= currsize;
@@ -65,7 +65,7 @@ ensures 0 <= bytesread && bytesread <= size; var copy_currsize: int;
var i, j, tmp : int;
var {:linear "tid"} tid: X;
- assume tid == tid';
+ tid := tid';
bytesread := size;
call acquire(tid);
@@ -127,7 +127,7 @@ requires Inv(ghostLock, currsize, newsize); var start, size, bytesread: int;
var {:linear "tid"} tid: X;
- assume tid == tid';
+ tid := tid';
havoc start, size;
assume (0 <= start && 0 <= size);
call bytesread := Read(tid, start, size);
@@ -140,8 +140,10 @@ requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil; while (*)
{
- havoc tid;
- assume tid != nil;
+ call tid := Allocate();
async call thread(tid);
}
-}
\ No newline at end of file +}
+
+procedure Allocate() returns ({:linear "tid"} xls: X);
+ensures xls != nil;
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index 217a0401..434d1f14 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -4,6 +4,9 @@ const nil: X; var l: X;
var x: int;
+procedure Allocate() returns ({:linear "tid"} xls: X);
+ensures xls != nil;
+
procedure {:entrypoint} main()
{
var {:linear "tid"} tid: X;
@@ -11,8 +14,8 @@ procedure {:entrypoint} main() while (*)
{
- havoc tid, val;
- assume tid != nil;
+ call tid := Allocate();
+ havoc val;
async call foo(tid, val);
}
}
@@ -21,7 +24,7 @@ procedure foo({:linear "tid"} tid': X, val: int) requires tid' != nil;
{
var {:linear "tid"} tid: X;
- assume tid == tid';
+ tid := tid';
assume l == nil;
l := tid;
@@ -38,7 +41,7 @@ requires tid' != nil; ensures tid == tid';
ensures old(l) == tid ==> old(l) == l && old(x) == x;
{
- assume tid == tid';
+ tid := tid';
yield;
assert tid != nil;
assert (old(l) == tid ==> old(l) == l && old(x) == x);
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index fbc97d59..f8c32022 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -1,5 +1,14 @@ function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+procedure Allocate() returns ({:linear "tid"} xls: int);
+ensures xls != 0;
+
+procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);
+ensures xls == mapconstbool(true);
+
+procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);
+ensures xls == mapconstbool(true);
+
var g: int;
var h: int;
@@ -8,16 +17,16 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) var {:linear "1"} x: [int]bool;
var {:linear "2"} y: [int]bool;
var {:linear "tid"} tid_child: int;
- assume tid_in == tid_out;
- assume x == mapconstbool(true);
- assume y == mapconstbool(true);
+ tid_out := tid_in;
+ call x := Allocate_1();
+ call y := Allocate_2();
g := 0;
yield;
assert g == 0 && x == mapconstbool(true);
yield;
- assume tid_child != 0;
+ call tid_child := Allocate();
async call B(tid_child, x);
yield;
@@ -27,6 +36,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) assert h == 0 && y == mapconstbool(true);
yield;
+ call tid_child := Allocate();
async call C(tid_child, y);
}
@@ -35,8 +45,8 @@ requires x_in != mapconstbool(false); {
var {:linear "tid"} tid_out: int;
var {:linear "1"} x: [int]bool;
- assume tid_in == tid_out;
- assume x_in == x;
+ tid_out := tid_in;
+ x := x_in;
g := 1;
@@ -50,8 +60,8 @@ requires y_in != mapconstbool(false); {
var {:linear "tid"} tid_out: int;
var {:linear "2"} y: [int]bool;
- assume tid_in == tid_out;
- assume y_in == y;
+ tid_out := tid_in;
+ y := y_in;
h := 1;
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index d188db3a..c2f792ef 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -19,6 +19,8 @@ var l: [X]bool; procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+procedure Allocate() returns ({:linear "tid"} xls: [X]bool);
+
procedure {:entrypoint} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
requires tidls' != None() && xls' == All();
{
@@ -28,18 +30,18 @@ requires tidls' != None() && xls' == All(); var {:linear "x"} xls1: [X]bool;
var {:linear "x"} xls2: [X]bool;
- havoc tidls, xls;
- assume tidls' == tidls && xls' == xls;
+ tidls := tidls';
+ xls := xls';
x := 42;
yield;
assert xls == All();
assert x == 42;
call xls1, xls2 := Split(xls);
- havoc lsChild;
+ call lsChild := Allocate();
assume (lsChild != None());
async call thread(lsChild, xls1);
- havoc lsChild;
+ call lsChild := Allocate();
assume (lsChild != None());
async call thread(lsChild, xls2);
}
@@ -50,8 +52,8 @@ requires tidls' != None() && xls' != None(); var {:linear "x"} xls: [X]bool;
var {:linear "tid"} tidls: [X]bool;
- havoc tidls, xls;
- assume tidls' == tidls && xls' == xls;
+ tidls := tidls';
+ xls := xls';
assume l == None();
l := tidls;
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index 5d627348..ac4a2e21 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -20,6 +20,9 @@ const nil: X; procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
+procedure Allocate() returns ({:linear "tid"} xls: X);
+ensures xls != nil;
+
procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
requires tidls' != nil && xls' == All();
{
@@ -29,19 +32,17 @@ requires tidls' != nil && xls' == All(); var {:linear "x"} xls1: [X]bool;
var {:linear "x"} xls2: [X]bool;
- havoc tidls, xls;
- assume tidls' == tidls && xls' == xls;
+ tidls := tidls';
+ xls := xls';
x := 42;
yield;
assert xls == All();
assert x == 42;
call xls1, xls2 := Split(xls);
- havoc lsChild;
- assume (lsChild != nil);
+ call lsChild := Allocate();
async call thread(lsChild, xls1);
- havoc lsChild;
- assume (lsChild != nil);
+ call lsChild := Allocate();
async call thread(lsChild, xls2);
}
@@ -51,8 +52,8 @@ requires tidls' != nil && xls' != None(); var {:linear "x"} xls: [X]bool;
var {:linear "tid"} tidls: X;
- havoc tidls, xls;
- assume tidls' == tidls && xls' == xls;
+ tidls := tidls';
+ xls := xls';
assume l == nil;
l := tidls;
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl new file mode 100644 index 00000000..472e64c6 --- /dev/null +++ b/Test/og/new1.bpl @@ -0,0 +1,38 @@ +function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
+
+var g:int;
+
+var {:linear "Perm"} Permissions: [int]bool;
+
+procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);
+modifies Permissions;
+requires Permissions == mapconstbool(true);
+ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);
+
+procedure PB({:linear "Perm"} permVar_in:[int]bool)
+requires permVar_in[0] && g == 0;
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+ permVar_out := permVar_in;
+
+ yield;
+ assert permVar_out[0];
+ assert g == 0;
+
+ g := g + 1;
+
+ yield;
+ assert permVar_out[0];
+ assert g == 1;
+}
+
+procedure{:entrypoint} Main()
+requires Permissions == mapconstbool(true);
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+
+ call permVar_out := Allocate_Perm();
+
+ g := 0;
+ async call PB(permVar_out);
+}
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index f2d45204..116612cb 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -1,16 +1,20 @@ var a:[int]int;
+procedure Allocate() returns ({:linear "tid"} xls: int);
+
procedure {:entrypoint} main()
{
var {:linear "tid"} i: int;
var {:linear "tid"} j: int;
+ call i := Allocate();
+ call j := Allocate();
call i := t(i) | j := t(j);
call i := u(i) | j := u(j);
}
procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
a[i] := 42;
call i := Yield(i);
@@ -19,7 +23,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int) procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
a[i] := 42;
yield;
@@ -30,7 +34,7 @@ procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int) ensures i == i';
ensures old(a)[i] == a[i];
{
- assume i == i';
+ i := i';
yield;
assert old(a)[i] == a[i];
}
\ No newline at end of file diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index a5b2768f..8f78fdc5 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -1,15 +1,19 @@ var a:int;
+procedure Allocate() returns ({:linear "tid"} xls: int);
+
procedure {:entrypoint} main()
{
var {:linear "tid"} i: int;
var {:linear "tid"} j: int;
+ call i := Allocate();
+ call j := Allocate();
call i := t(i) | j := t(j);
}
procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
call Yield();
assert a == old(a);
a := a + 1;
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index 8ee5e436..c583cb3c 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -1,16 +1,20 @@ var a:[int]int;
+procedure Allocate() returns ({:linear "tid"} xls: int);
+
procedure {:entrypoint} main()
{
var {:linear "tid"} i: int;
var {:linear "tid"} j: int;
+ call i := Allocate();
+ call j := Allocate();
call i := t(i) | j := Yield(j);
call i := u(i) | j := u(j);
}
procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
a[i] := 42;
call i := Yield(i);
@@ -19,7 +23,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int) procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
{
- assume i == i';
+ i := i';
a[i] := 42;
yield;
@@ -30,7 +34,7 @@ procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int) ensures i == i';
ensures old(a)[i] == a[i];
{
- assume i == i';
+ i := i';
yield;
assert old(a)[i] == a[i];
}
\ No newline at end of file diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl new file mode 100644 index 00000000..78889868 --- /dev/null +++ b/Test/og/perm.bpl @@ -0,0 +1,50 @@ +var x: int;
+function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
+
+function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;
+
+procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);
+ ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);
+
+
+procedure {:entrypoint} mainE({:linear "Perm"} permVar_in: [int]bool)
+ free requires permVar_in == ch_mapconstbool(true);
+ free requires permVar_in[0];
+ modifies x;
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+ var {:linear "Perm"} permVarOut2: [int]bool;
+
+ permVar_out := permVar_in;
+
+ assume x == 0;
+
+ yield;
+ assert x == 0;
+ assert permVar_out[0];
+ assert permVar_out == ch_mapconstbool(true);
+
+ call permVar_out, permVarOut2 := Split(permVar_out);
+ async call foo(permVarOut2);
+}
+
+procedure foo({:linear "Perm"} permVar_in: [int]bool)
+ free requires permVar_in != ch_mapconstbool(false);
+ free requires permVar_in[1];
+ requires x == 0;
+ modifies x;
+{
+ var {:linear "Perm"} permVar_out: [int]bool;
+ permVar_out := permVar_in;
+
+ yield;
+ assert permVar_out[1];
+ assert x == 0;
+
+ x := x + 1;
+
+ yield;
+ assert permVar_out[1];
+ assert x == 1;
+}
+
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 8569f273..dd07b4a4 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do ( %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl index 01451ac9..28ae5b89 100644 --- a/Test/og/t1.bpl +++ b/Test/og/t1.bpl @@ -1,5 +1,14 @@ function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
+procedure Allocate() returns ({:linear "tid"} xls: int);
+ensures xls != 0;
+
+procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);
+ensures xls == mapconstbool(true);
+
+procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);
+ensures xls == mapconstbool(true);
+
var g: int;
var h: int;
@@ -8,9 +17,9 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) var {:linear "1"} x: [int]bool;
var {:linear "2"} y: [int]bool;
var {:linear "tid"} tid_child: int;
- assume tid_in == tid_out;
- assume x == mapconstbool(true);
- assume y == mapconstbool(true);
+ tid_out := tid_in;
+ call x := Allocate_1();
+ call y := Allocate_2();
g := 0;
yield;
@@ -18,7 +27,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) assert g == 0;
yield;
- assume tid_child != 0;
+ call tid_child := Allocate();
async call B(tid_child, x);
yield;
@@ -32,6 +41,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) assert h == 0 && y == mapconstbool(true);
yield;
+ call tid_child := Allocate();
async call C(tid_child, y);
}
@@ -40,8 +50,8 @@ requires x_in != mapconstbool(false); {
var {:linear "tid"} tid_out: int;
var {:linear "1"} x: [int]bool;
- assume tid_in == tid_out;
- assume x_in == x;
+ tid_out := tid_in;
+ x := x_in;
g := 1;
}
@@ -51,8 +61,8 @@ requires y_in != mapconstbool(false); {
var {:linear "tid"} tid_out: int;
var {:linear "2"} y: [int]bool;
- assume tid_in == tid_out;
- assume y_in == y;
+ tid_out := tid_in;
+ y := y_in;
h := 1;
}
|