summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/Absy.cs7
-rw-r--r--Source/Core/DeadVarElim.cs7
-rw-r--r--Source/Core/Inline.cs1
-rw-r--r--Source/Core/LinearSets.cs108
-rw-r--r--Source/Core/OwickiGries.cs37
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs1
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs36
-rw-r--r--Source/VCGeneration/StratifiedVC.cs8
-rw-r--r--Source/VCGeneration/VC.cs229
-rw-r--r--Source/VCGeneration/Wlp.cs16
10 files changed, 336 insertions, 114 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 009fb071..33c4e91a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2354,9 +2354,10 @@ namespace Microsoft.Boogie {
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
bool isAtomicSpecification =
- QKeyValue.FindIntAttribute(this.Attributes, "atomic", -1) != -1 ||
- QKeyValue.FindIntAttribute(this.Attributes, "rightmover", -1) != -1 ||
- QKeyValue.FindIntAttribute(this.Attributes, "leftmover", -1) != -1;
+ QKeyValue.FindBoolAttribute(this.Attributes, "atomic") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "right") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "left") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "both");
bool oldYields = tc.Yields;
tc.Yields = isAtomicSpecification;
this.Condition.Typecheck(tc);
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index f3056e4f..cb6ce689 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -42,6 +42,7 @@ namespace Microsoft.Boogie {
static Procedure enclosingProc;
static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;
static HashSet<Procedure> yieldingProcs;
+ static HashSet<Procedure> asyncAndParallelCallTargetProcs;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));
@@ -69,6 +70,7 @@ namespace Microsoft.Boogie {
modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();
yieldingProcs = new HashSet<Procedure>();
+ asyncAndParallelCallTargetProcs = new HashSet<Procedure>();
HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();
foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
@@ -118,6 +120,10 @@ namespace Microsoft.Boogie {
{
x.AddAttribute("yields");
}
+ if (asyncAndParallelCallTargetProcs.Contains(x) && !QKeyValue.FindBoolAttribute(x.Attributes, "stable"))
+ {
+ x.AddAttribute("stable");
+ }
}
if (false /*CommandLineOptions.Clo.Trace*/) {
@@ -209,6 +215,7 @@ namespace Microsoft.Boogie {
var curr = callCmd;
while (curr != null)
{
+ asyncAndParallelCallTargetProcs.Add(curr.Proc);
if (!yieldingProcs.Contains(curr.Proc))
{
yieldingProcs.Add(curr.Proc);
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 61b3a322..ad9ecef0 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -50,6 +50,7 @@ namespace Microsoft.Boogie {
Inliner codeExprInliner = new Inliner(program, inlineCallback, CommandLineOptions.Clo.InlineDepth);
codeExprInliner.newLocalVars = new List<Variable>(node.LocVars);
codeExprInliner.newModifies = new List<IdentifierExpr>();
+ codeExprInliner.inlinedProcLblMap = this.inlinedProcLblMap;
List<Block> newCodeExprBlocks = codeExprInliner.DoInlineBlocks(node.Blocks, ref inlinedSomething);
return new CodeExpr(codeExprInliner.newLocalVars, newCodeExprBlocks);
}
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 5769cbdf..3a9de5fb 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -9,16 +9,16 @@ namespace Microsoft.Boogie
{
public class LinearEraser : StandardVisitor
{
- private QKeyValue Remove(QKeyValue iter)
+ private QKeyValue RemoveLinearAttribute(QKeyValue iter)
{
if (iter == null) return null;
- iter.Next = Remove(iter.Next);
+ iter.Next = RemoveLinearAttribute(iter.Next);
return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next;
}
public override Variable VisitVariable(Variable node)
{
- node.Attributes = Remove(node.Attributes);
+ node.Attributes = RemoveLinearAttribute(node.Attributes);
return base.VisitVariable(node);
}
}
@@ -29,9 +29,10 @@ namespace Microsoft.Boogie
public int errorCount;
public CheckingContext checkingContext;
public Dictionary<string, Type> domainNameToType;
- public Dictionary<Absy, HashSet<Variable>> availableLocalLinearVars;
+ public Dictionary<Absy, HashSet<Variable>> availableLinearVars;
public Dictionary<Variable, string> inoutParamToDomainName;
public Dictionary<Variable, string> varToDomainName;
+ public Dictionary<Variable, string> globalVarToDomainName;
public Dictionary<string, LinearDomain> linearDomains;
public LinearTypechecker(Program program)
@@ -41,7 +42,7 @@ namespace Microsoft.Boogie
this.checkingContext = new CheckingContext(null);
this.domainNameToType = new Dictionary<string, Type>();
this.parallelCallInvars = new HashSet<Variable>();
- this.availableLocalLinearVars = new Dictionary<Absy, HashSet<Variable>>();
+ this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
this.inoutParamToDomainName = new Dictionary<Variable, string>();
this.varToDomainName = new Dictionary<Variable, string>();
this.linearDomains = new Dictionary<string, LinearDomain>();
@@ -59,9 +60,22 @@ namespace Microsoft.Boogie
checkingContext.Error(node, message);
errorCount++;
}
+ public override Program VisitProgram(Program node)
+ {
+ globalVarToDomainName = new Dictionary<Variable, string>();
+ foreach (GlobalVariable g in program.GlobalVariables())
+ {
+ string domainName = FindDomainName(g);
+ if (domainName != null)
+ {
+ globalVarToDomainName[g] = domainName;
+ }
+ }
+ return base.VisitProgram(node);
+ }
public override Implementation VisitImplementation(Implementation node)
{
- HashSet<Variable> start = new HashSet<Variable>();
+ HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);
for (int i = 0; i < node.InParams.Count; i++)
{
string domainName = FindDomainName(node.Proc.InParams[i]);
@@ -87,7 +101,7 @@ namespace Microsoft.Boogie
Stack<Block> dfsStack = new Stack<Block>();
HashSet<Block> dfsStackAsSet = new HashSet<Block>();
- availableLocalLinearVars[node.Blocks[0]] = start;
+ availableLinearVars[node.Blocks[0]] = start;
dfsStack.Push(node.Blocks[0]);
dfsStackAsSet.Add(node.Blocks[0]);
while (dfsStack.Count > 0)
@@ -97,27 +111,31 @@ namespace Microsoft.Boogie
HashSet<Variable> end = PropagateAvailableLinearVarsAcrossBlock(b);
if (b.TransferCmd is ReturnCmd)
{
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a return", g.Name));
+ }
foreach (Variable v in node.OutParams)
{
if (FindDomainName(v) == null || end.Contains(v)) continue;
- Error(b, "output variable must be available at a return");
+ Error(b, string.Format("Output variable {0} must be available at a return", v.Name));
}
+ continue;
}
- if (b.TransferCmd is ReturnCmd) continue;
GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
foreach (Block target in gotoCmd.labelTargets)
{
- if (!availableLocalLinearVars.ContainsKey(target))
+ if (!availableLinearVars.ContainsKey(target))
{
- availableLocalLinearVars[target] = new HashSet<Variable>(end);
+ availableLinearVars[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))
+ var savedAvailableVars = new HashSet<Variable>(availableLinearVars[target]);
+ availableLinearVars[target].IntersectWith(end);
+ if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target))
{
dfsStack.Push(target);
dfsStackAsSet.Add(target);
@@ -128,7 +146,7 @@ namespace Microsoft.Boogie
return impl;
}
private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {
- HashSet<Variable> start = new HashSet<Variable>(availableLocalLinearVars[b]);
+ HashSet<Variable> start = new HashSet<Variable>(availableLinearVars[b]);
foreach (Cmd cmd in b.Cmds)
{
if (cmd is AssignCmd)
@@ -155,6 +173,10 @@ namespace Microsoft.Boogie
}
else if (cmd is CallCmd)
{
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a call", g.Name));
+ }
CallCmd callCmd = (CallCmd)cmd;
while (callCmd != null)
{
@@ -174,7 +196,7 @@ namespace Microsoft.Boogie
callCmd = callCmd.InParallelWith;
}
callCmd = (CallCmd)cmd;
- availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);
+ availableLinearVars[callCmd] = new HashSet<Variable>(start);
while (callCmd != null)
{
foreach (IdentifierExpr ie in callCmd.Outs)
@@ -196,13 +218,19 @@ namespace Microsoft.Boogie
}
else if (cmd is YieldCmd)
{
- availableLocalLinearVars[cmd] = new HashSet<Variable>(start);
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a yield", g.Name));
+ }
+ availableLinearVars[cmd] = new HashSet<Variable>(start);
}
}
return start;
}
public string FindDomainName(Variable v)
{
+ if (globalVarToDomainName.ContainsKey(v))
+ return globalVarToDomainName[v];
if (inoutParamToDomainName.ContainsKey(v))
return inoutParamToDomainName[v];
return QKeyValue.FindStringAttribute(v.Attributes, "linear");
@@ -233,7 +261,7 @@ namespace Microsoft.Boogie
}
if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type))
{
- Error(node, "a linear domain must be consistently attached to variables of a particular type");
+ Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName));
}
else
{
@@ -248,44 +276,35 @@ namespace Microsoft.Boogie
for (int i = 0; i < node.Lhss.Count; i++)
{
AssignLhs lhs = node.Lhss[i];
- string domainName = FindDomainName(lhs.DeepAssignedVariable);
+ Variable lhsVar = lhs.DeepAssignedVariable;
+ string domainName = FindDomainName(lhsVar);
if (domainName == null) continue;
SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
if (salhs == null)
{
- Error(node, "Only simple assignment allowed on linear sets");
- continue;
- }
- if (salhs.DeepAssignedVariable is GlobalVariable)
- {
- Error(node, "Linear global variable cannot be written to");
+ Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name));
continue;
}
IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;
if (rhs == null)
{
- Error(node, "Only variable can be assigned to a linear variable");
+ Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name));
continue;
}
string rhsDomainName = FindDomainName(rhs.Decl);
if (rhsDomainName == null)
{
- Error(node, "Only linear variable can be assigned to another linear variable");
+ Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name));
continue;
}
if (domainName != rhsDomainName)
{
- Error(node, "Variable of one domain being assigned to a variable of another domain");
+ Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName));
continue;
}
if (rhsVars.Contains(rhs.Decl))
{
- Error(node, "A linear variable can occur only once in the rhs");
- continue;
- }
- if (rhs.Decl is GlobalVariable)
- {
- Error(node, "Linear global variable cannot be read from");
+ Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name));
continue;
}
rhsVars.Add(rhs.Decl);
@@ -304,13 +323,13 @@ namespace Microsoft.Boogie
IdentifierExpr actual = node.Ins[i] as IdentifierExpr;
if (actual == null)
{
- Error(node, "Only variable can be assigned to a linear variable");
+ Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name));
continue;
}
string actualDomainName = FindDomainName(actual.Decl);
if (actualDomainName == null)
{
- Error(node, "Only a linear argument can be passed to a linear parameter");
+ Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name));
continue;
}
if (domainName != actualDomainName)
@@ -320,7 +339,7 @@ namespace Microsoft.Boogie
}
if (parallelCallInvars.Contains(actual.Decl))
{
- Error(node, "A linear set can occur only once as an in parameter");
+ Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name));
continue;
}
if (actual.Decl is GlobalVariable)
@@ -373,13 +392,7 @@ namespace Microsoft.Boogie
domainNameToScope[domainName] = new HashSet<Variable>();
domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
}
- foreach (Variable v in program.GlobalVariables())
- {
- var domainName = FindDomainName(v);
- if (domainName == null) continue;
- domainNameToScope[domainName].Add(v);
- }
- foreach (Variable v in availableLocalLinearVars[absy])
+ foreach (Variable v in availableLinearVars[absy])
{
var domainName = FindDomainName(v);
domainNameToScope[domainName].Add(v);
@@ -453,7 +466,7 @@ namespace Microsoft.Boogie
{
domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
}
- foreach (Variable v in availableLocalLinearVars[callCmd])
+ foreach (Variable v in availableLinearVars[callCmd])
{
var domainName = FindDomainName(v);
var domain = linearDomains[domainName];
@@ -510,10 +523,9 @@ namespace Microsoft.Boogie
domainNameToOutputScope[domainName] = new HashSet<Variable>();
}
- foreach (Variable v in program.GlobalVariables())
+ foreach (Variable v in globalVarToDomainName.Keys)
{
- var domainName = FindDomainName(v);
- if (domainName == null) continue;
+ var domainName = globalVarToDomainName[v];
domainNameToInputScope[domainName].Add(v);
domainNameToOutputScope[domainName].Add(v);
}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index ed4d8dbb..dd6276c2 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Boogie
newCmds.Add(yieldCallCmd);
}
- private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLocalLinearVars, Dictionary<string, Variable> domainNameToInputVar)
+ private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
foreach (var domainName in linearTypechecker.linearDomains.Keys)
@@ -77,7 +77,7 @@ namespace Microsoft.Boogie
expr.Typecheck(new TypecheckingContext(null));
domainNameToExpr[domainName] = expr;
}
- foreach (Variable v in availableLocalLinearVars)
+ foreach (Variable v in availableLinearVars)
{
var domainName = linearTypechecker.FindDomainName(v);
var domain = linearTypechecker.linearDomains[domainName];
@@ -118,7 +118,7 @@ namespace Microsoft.Boogie
{
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
}
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[yieldCmd], domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
for (int j = 0; j < cmds.Count; j++)
@@ -264,7 +264,7 @@ namespace Microsoft.Boogie
PredicateCmd predCmd = (PredicateCmd)cmd;
var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
if (predCmd is AssertCmd)
- newCmds.Add(new AssertCmd(predCmd.tok, newExpr));
+ newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes));
else
newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
}
@@ -440,13 +440,13 @@ namespace Microsoft.Boogie
if (callCmd.InParallelWith != null || callCmd.IsAsync ||
QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
{
- HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);
+ HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypechecker.availableLinearVars[callCmd]);
foreach (IdentifierExpr ie in callCmd.Outs)
{
if (linearTypechecker.FindDomainName(ie.Decl) == null) continue;
- availableLocalLinearVars.Add(ie.Decl);
+ availableLinearVars.Add(ie.Decl);
}
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLocalLinearVars, domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
}
@@ -473,7 +473,7 @@ namespace Microsoft.Boogie
foreach (Block header in yieldingHeaders)
{
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[header], domainNameToInputVar);
foreach (Block pred in header.Predecessors)
{
AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
@@ -582,7 +582,7 @@ namespace Microsoft.Boogie
}
else
{
- cmds.Add(new AssertCmd(r.tok, r.Condition));
+ cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes));
}
}
yields.Add(cmds);
@@ -621,7 +621,7 @@ namespace Microsoft.Boogie
}
else
{
- cmds.Add(new AssertCmd(e.tok, e.Condition));
+ cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes));
}
}
yields.Add(cmds);
@@ -680,6 +680,13 @@ namespace Microsoft.Boogie
program.TopLevelDeclarations.Add(yieldImpl);
}
+ private QKeyValue RemoveYieldsAttribute(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = RemoveYieldsAttribute(iter.Next);
+ return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;
+ }
+
public void Transform()
{
Program program = linearTypechecker.program;
@@ -708,12 +715,22 @@ namespace Microsoft.Boogie
if (proc == null) continue;
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
{
+ HashSet<Variable> modifiedVars = new HashSet<Variable>();
+ proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));
foreach (GlobalVariable g in program.GlobalVariables())
{
+ if (modifiedVars.Contains(g)) continue;
proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));
}
+ proc.Attributes = RemoveYieldsAttribute(proc.Attributes);
}
}
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ impl.Attributes = RemoveYieldsAttribute(impl.Attributes);
+ }
}
}
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 4ebe17dc..81a2ad39 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -443,6 +443,7 @@ namespace Microsoft.Boogie
}
}
+ if(CommandLineOptions.Clo.StratifiedInlining == 0)
{
OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker);
ogTransform.Transform();
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 0b92b1c3..a6b01760 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST {
}
}
- public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings);
+ public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);
public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
// Stack on which the various Visit-methods put the result of the translation
@@ -375,13 +375,42 @@ namespace Microsoft.Boogie.VCExprAST {
return node;
}
+ public bool isPositiveContext = true;
private VCExpr TranslateNAryExpr(NAryExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ bool flipContextForArg0 = false;
+ if (node.Fun is UnaryOperator)
+ {
+ UnaryOperator oper = (UnaryOperator)node.Fun;
+ if (oper.Op == UnaryOperator.Opcode.Not)
+ flipContextForArg0 = true;
+ }
+ else if (node.Fun is BinaryOperator)
+ {
+ BinaryOperator oper = (BinaryOperator)node.Fun;
+ if (oper.Op == BinaryOperator.Opcode.Imp)
+ flipContextForArg0 = true;
+ else if (oper.Op == BinaryOperator.Opcode.Iff) {
+ Expr one = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[0], node.Args[1] });
+ Expr two = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[1], node.Args[0] });
+ NAryExpr cmpd = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.And), new List<Expr> { one, two });
+ TypecheckingContext tc = new TypecheckingContext(null);
+ cmpd.Typecheck(tc);
+ return TranslateNAryExpr(cmpd);
+ }
+ }
+
int n = node.Args.Count;
List<VCExpr/*!*/>/*!*/ vcs = new List<VCExpr/*!*/>(n);
+
for (int i = 0; i < n; i++) {
+ if (i == 0 && flipContextForArg0)
+ isPositiveContext = !isPositiveContext;
vcs.Add(Translate(cce.NonNull(node.Args)[i]));
+ if (i == 0 && flipContextForArg0)
+ isPositiveContext = !isPositiveContext;
}
if (node.Type == null) {
@@ -611,19 +640,18 @@ namespace Microsoft.Boogie.VCExprAST {
Contract.Assert(false);
throw new cce.UnreachableException();
}
- CodeExprConverter codeExprConverter = null;
+ public CodeExprConverter codeExprConverter = null;
public void SetCodeExprConverter(CodeExprConverter f) {
this.codeExprConverter = f;
}
public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {
//Contract.Requires(codeExpr != null);
Contract.Ensures(Contract.Result<Expr>() != null);
-
Contract.Assume(codeExprConverter != null);
Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();
- VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);
+ VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, isPositiveContext);
Push(e);
return codeExpr;
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 7d8d749c..086dde15 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -266,13 +266,19 @@ namespace VC {
VCExpressionGenerator gen = proverInterface.VCExprGen;
var exprGen = proverInterface.Context.ExprGen;
var translator = proverInterface.Context.BoogieExprTranslator;
+
VCExpr controlFlowVariableExpr = null;
if (!CommandLineOptions.Clo.UseLabels) {
controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);
vcgen.InstrumentCallSites(impl);
}
- vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));
+
+ label2absy = new Dictionary<int, Absy>();
+ VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(label2absy, proverInterface.Context);
+ translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
+ vcexpr = gen.Not(vcgen.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverInterface.Context));
+
if (controlFlowVariableExpr != null) {
VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 85d0fb31..2abe4a1b 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1245,44 +1245,8 @@ namespace VC {
ProverContext ctx = checker.TheoremProver.Context;
Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
- bet.SetCodeExprConverter(
- new CodeExprConverter(
- delegate(CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings)
- {
- VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
- vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
- vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
- vcgen.CurrentLocalVariables = codeExpr.LocVars;
- // codeExpr.Blocks.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
-
- ResetPredecessors(codeExpr.Blocks);
- vcgen.AddBlocksBetween(codeExpr.Blocks);
- Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));
- int ac; // computed, but then ignored for this CodeExpr
- VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
- VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
-
- if (vcgen.CurrentLocalVariables.Count != 0)
- {
- Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
- List<VCExprVar> boundVars = new List<VCExprVar>();
- foreach (Variable v in vcgen.CurrentLocalVariables)
- {
- Contract.Assert(v != null);
- VCExprVar ev = translator.LookupVariable(v);
- Contract.Assert(ev != null);
- boundVars.Add(ev);
- if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))
- {
- // add an antecedent (tickleBool ev) to help the prover find a possible trigger
- vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
- }
- }
- vce = checker.VCExprGen.Forall(boundVars, new List<VCTrigger>(), vce);
- }
- return vce;
- }
- ));
+ CodeExprConversionClosure cc = new CodeExprConversionClosure(label2absy, ctx);
+ bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition);
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
@@ -1370,6 +1334,56 @@ namespace VC {
}
#endregion
+
+ public class CodeExprConversionClosure
+ {
+ Dictionary<int, Absy> label2absy;
+ ProverContext ctx;
+ public CodeExprConversionClosure(Dictionary<int, Absy> label2absy, ProverContext ctx)
+ {
+ this.label2absy = label2absy;
+ this.ctx = ctx;
+ }
+
+ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext)
+ {
+ VCGen vcgen = new VCGen(new Program(), null, false, new List<Checker>());
+ vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();
+ vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
+ vcgen.CurrentLocalVariables = codeExpr.LocVars;
+
+ ResetPredecessors(codeExpr.Blocks);
+ vcgen.AddBlocksBetween(codeExpr.Blocks);
+ Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));
+ int ac; // computed, but then ignored for this CodeExpr
+ VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isPositiveContext);
+ VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
+ if (vcgen.CurrentLocalVariables.Count != 0)
+ {
+ Boogie2VCExprTranslator translator = ctx.BoogieExprTranslator;
+ List<VCExprVar> boundVars = new List<VCExprVar>();
+ foreach (Variable v in vcgen.CurrentLocalVariables)
+ {
+ Contract.Assert(v != null);
+ VCExprVar ev = translator.LookupVariable(v);
+ Contract.Assert(ev != null);
+ boundVars.Add(ev);
+ if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))
+ {
+ // add an antecedent (tickleBool ev) to help the prover find a possible trigger
+ vce = ctx.ExprGen.Implies(ctx.ExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
+ }
+ }
+ vce = ctx.ExprGen.Forall(boundVars, new List<VCTrigger>(), vce);
+ }
+ if (isPositiveContext)
+ {
+ vce = ctx.ExprGen.Not(vce);
+ }
+ return vce;
+ }
+ }
+
public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext)
{
Contract.Requires(impl != null);
@@ -1381,7 +1395,7 @@ namespace VC {
return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
}
- protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
+ public VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary<int, Absy>/*!*/ label2absy, ProverContext proverContext) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1467,6 +1481,133 @@ namespace VC {
ModelViewInfo mvInfo;
var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
+ // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct
+ foreach (var b in impl.Blocks)
+ {
+ List<Cmd> newCmds = new List<Cmd>();
+ bool changed = false;
+ foreach (var c in b.Cmds)
+ {
+ var a = c as AssertCmd;
+ var ar = c as AssertRequiresCmd;
+ var ae = c as AssertEnsuresCmd;
+ var ai = c as LoopInitAssertCmd;
+ var am = c as LoopInvMaintainedAssertCmd;
+ // TODO:
+ //use Duplicator and Substituter rather than new
+ //nested IToken?
+ //document expand attribute (search for {:ignore}, for example)
+ //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs
+ Func<Expr,Expr,Expr> withType = (Expr from, Expr to) =>
+ {
+ NAryExpr nFrom = from as NAryExpr;
+ NAryExpr nTo = to as NAryExpr;
+ to.Type = from.Type;
+ if (nFrom != null && nTo != null) nTo.TypeParameters = nFrom.TypeParameters;
+ return to;
+ };
+
+ Action<int,Expr,Action<Expr>> traverse = null;
+ traverse = (depth, e, act) =>
+ {
+ ForallExpr forall = e as ForallExpr;
+ NAryExpr nary = e as NAryExpr;
+ if (forall != null)
+ {
+ traverse(depth, forall.Body, e1 => act(withType(forall,
+ new ForallExpr(e1.tok, forall.TypeParameters, forall.Dummies, forall.Attributes, forall.Triggers, e1))));
+ return;
+ }
+ if (nary != null)
+ {
+ var args = nary.Args;
+ IAppliable fun = nary.Fun;
+ BinaryOperator bop = fun as BinaryOperator;
+ FunctionCall call = fun as FunctionCall;
+ if (bop != null)
+ {
+ switch (bop.Op)
+ {
+ case BinaryOperator.Opcode.And:
+ traverse(depth, args[0], act);
+ traverse(depth, args[1], act);
+ return;
+ case BinaryOperator.Opcode.Imp:
+ traverse(depth, args[1], e1 => act(withType(nary,
+ new NAryExpr(e1.tok, fun, new List<Expr>() { args[0], e1 }))));
+ return;
+ }
+ }
+ if (depth > 0 && call != null && call.Func != null)
+ {
+ Function cf = call.Func;
+ Expr body = cf.Body;
+ List<Variable> ins = cf.InParams;
+ if (body == null && cf.DefinitionAxiom != null)
+ {
+ ForallExpr all = cf.DefinitionAxiom.Expr as ForallExpr;
+ if (all != null)
+ {
+ NAryExpr def = all.Body as NAryExpr;
+ if (def != null && def.Fun is BinaryOperator && ((BinaryOperator) (def.Fun)).Op == BinaryOperator.Opcode.Iff)
+ {
+ body = def.Args[1];
+ ins = all.Dummies;
+ }
+ }
+ }
+ if (body != null)
+ {
+ Func<Expr,Expr> new_f = e1 =>
+ {
+ Function f = new Function(cf.tok, "expand<" + cf.Name + ">", cf.TypeParameters, ins, cf.OutParams[0], cf.Comment);
+ f.Body = e1;
+ Token tok = new Token(e1.tok.line, e1.tok.col);
+ tok.filename = e.tok.filename + "(" + e.tok.line + "," + e.tok.col + ") --> " + e1.tok.filename;
+ return withType(nary, new NAryExpr(tok, new FunctionCall(f), args));
+ };
+ traverse(depth - 1, body, e1 => act(new_f(e1)));
+ return;
+ }
+ }
+ }
+ act(e);
+ };
+
+ if (a != null)
+ {
+ var attr = a.Attributes;
+ if (ar != null && ar.Requires.Attributes != null) attr = ar.Requires.Attributes;
+ if (ar != null && ar.Call.Attributes != null) attr = ar.Call.Attributes;
+ if (ae != null && ae.Ensures.Attributes != null) attr = ae.Ensures.Attributes;
+ if (QKeyValue.FindExprAttribute(attr, "expand") != null || QKeyValue.FindBoolAttribute(attr, "expand"))
+ {
+ int depth = QKeyValue.FindIntAttribute(attr, "expand", 100);
+ Func<Expr,Expr> fe = e => Expr.Or(a.Expr, e);
+ //traverse(depth, a.Expr, e => System.Console.WriteLine(e.GetType() + " :: " + e + " @ " + e.tok.line + ", " + e.tok.col));
+ traverse(depth, a.Expr, e =>
+ {
+ AssertCmd new_c =
+ (ar != null) ? new AssertRequiresCmd(ar.Call, new Requires(e.tok, ar.Requires.Free, fe(e), ar.Requires.Comment)) :
+ (ae != null) ? new AssertEnsuresCmd(new Ensures(e.tok, ae.Ensures.Free, fe(e), ae.Ensures.Comment)) :
+ (ai != null) ? new LoopInitAssertCmd(e.tok, fe(e)) :
+ (am != null) ? new LoopInvMaintainedAssertCmd(e.tok, fe(e)) :
+ new AssertCmd(e.tok, fe(e));
+ new_c.Attributes = new QKeyValue(e.tok, "subsumption", new List<object>() { new LiteralExpr(e.tok, BigNum.FromInt(0)) }, a.Attributes);
+ newCmds.Add(new_c);
+ });
+ }
+ newCmds.Add(c);
+ changed = true;
+ }
+ else
+ {
+ newCmds.Add(c);
+ }
+ }
+ if (changed) b.Cmds = newCmds;
+ }
+
double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;
int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,
max_kg_splits = CommandLineOptions.Clo.VcsMaxKeepGoingSplits;
@@ -2589,7 +2730,9 @@ namespace VC {
VCExpr controlFlowVariableExpr,
Dictionary<int, Absy> label2absy,
ProverContext proverCtxt,
- out int assertionCount) {
+ out int assertionCount,
+ bool isPositiveContext = true)
+ {
Contract.Requires(blocks != null);
Contract.Requires(proverCtxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -2625,6 +2768,10 @@ namespace VC {
}
else {
SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);
+ if (isPositiveContext)
+ {
+ SuccCorrect = gen.Not(SuccCorrect);
+ }
}
}
else {
@@ -2643,7 +2790,7 @@ namespace VC {
SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);
}
- VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr);
+ VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);
VCExpr vc = Wlp.Block(block, SuccCorrect, context);
assertionCount += context.AssertionCount;
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 277d9a94..bb2a2785 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -24,22 +24,24 @@ namespace VC {
[Rep] public readonly ProverContext Ctxt;
public readonly VCExpr ControlFlowVariableExpr;
public int AssertionCount; // counts the number of assertions for which Wlp has been computed
-
- public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt)
+ public bool isPositiveContext;
+
+ public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, bool isPositiveContext = true)
{
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
+ this.isPositiveContext = isPositiveContext;
}
-
- public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)
+
+ public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr, bool isPositiveContext = true)
{
Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
this.ControlFlowVariableExpr = controlFlowVariableExpr;
+ this.isPositiveContext = isPositiveContext;
}
-
}
#region A class to compute wlp of a passive command program
@@ -95,7 +97,9 @@ namespace VC {
Contract.Assert(gen != null);
if (cmd is AssertCmd) {
AssertCmd ac = (AssertCmd)cmd;
+ ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
+ ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
return gen.Implies(C, N);
} else {
@@ -159,9 +163,7 @@ namespace VC {
}
}
}
-
return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);
-
} else {
Console.WriteLine(cmd.ToString());
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected command
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 02:08:25 +0000