diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:57:09 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 14:57:09 -0700 |
| commit | df71b461ff9284991c06b04d17b6e6b50f8151ae (patch) | |
| tree | bdba7a3de0b91741ec5b08b08a2cffa558b51b3a | |
| parent | 0ef24f03ddd336f5efb5b7349d1957288a9343ef (diff) | |
| parent | 6029a149a7cbc012121430cfd50ef433f130da09 (diff) | |
Merge
38 files changed, 3224 insertions, 3337 deletions
diff --git a/Chalice/tests/examples/list-reverse.chalice b/Chalice/tests/examples/list-reverse.chalice new file mode 100644 index 00000000..c694b4c9 --- /dev/null +++ b/Chalice/tests/examples/list-reverse.chalice @@ -0,0 +1,44 @@ +class Node {
+ var next : Node;
+ var val : int;
+
+ predicate list {
+ acc(next) && acc(val) && (next!=null ==> next.list)
+ }
+
+ function vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : [val] ++ next.vals())
+ }
+
+ function reverse_vals() : seq<int>
+ requires list
+ {
+ unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
+ }
+
+ method reverse_in_place() returns (r:Node)
+ requires list;
+ ensures r != null && r.list;
+ ensures r.vals() == old(this.reverse_vals());
+ {
+ var l : Node := this;
+ r := null;
+
+ while (l != null)
+ invariant l!=null ==> l.list;
+ invariant r!=null ==> r.list;
+ invariant old(this.reverse_vals()) == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
+ {
+ var y: Node;
+ unfold l.list;
+
+ y := l.next;
+ l.next := r;
+ r := l;
+ fold r.list;
+ l := y;
+ }
+ }
+}
\ No newline at end of file diff --git a/Chalice/tests/predicates/list-reverse.output.txt b/Chalice/tests/examples/list-reverse.output.txt index d8e19122..d8e19122 100644 --- a/Chalice/tests/predicates/list-reverse.output.txt +++ b/Chalice/tests/examples/list-reverse.output.txt diff --git a/Chalice/tests/predicates/list-reverse.chalice b/Chalice/tests/predicates/list-reverse.chalice deleted file mode 100644 index 5a596409..00000000 --- a/Chalice/tests/predicates/list-reverse.chalice +++ /dev/null @@ -1,158 +0,0 @@ -// this would be nice in the "examples" folder (at least, the version without the commented blocks), once the problem with old(..) is fixed
-
-class Node {
- var next : Node;
- var val : int;
-
- predicate list {
- acc(next) && acc(val) && (next!=null ==> next.list)
- }
-
- function vals() : seq<int>
- requires list
- {
- unfolding list in (next == null ? [val] : [val] ++ next.vals())
- }
-
- function reverse_vals() : seq<int>
- requires list
- {
- unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])
- }
-
- method reverse_in_place() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
-// if (r != null) {
-// unfold r.list; fold r.list;
-// }
- unfold l.list;
-// if (l.next != null) {
-// unfold l.next.list; fold l.next.list;
-// }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
- method reverse_in_place_01() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
-// if (r != null) {
-// unfold r.list; fold r.list;
-// }
- unfold l.list;
- if (l.next != null) {
- unfold l.next.list; fold l.next.list;
- }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-
- method reverse_in_place_10() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
- if (r != null) {
- unfold r.list; fold r.list;
- }
- unfold l.list;
-// if (l.next != null) {
-// unfold l.next.list; fold l.next.list;
-// }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-
-
- method reverse_in_place_11() returns (r:Node)
- requires list;
- ensures true;
- {
- var l : Node := this;
- r := null;
-
- var rev : seq<int> := this.reverse_vals(); // cached here, because old(this.reverse_vals()) doesn't work properly
-
- while (l != null)
- invariant l!=null ==> l.list;
- invariant r!=null ==> r.list;
- invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());
- {
- var y: Node;
- if (r != null) {
- unfold r.list; fold r.list;
- }
- unfold l.list;
- if (l.next != null) {
- unfold l.next.list; fold l.next.list;
- }
-
- y := l.next;
- l.next := r;
- r := l;
- fold r.list;
- l := y;
- }
- assert r.vals() == rev; // should be the post-condition
- }
-
-
-}
\ No newline at end of file diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 61943cf0..0911cbd3 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -404,7 +404,7 @@ namespace Microsoft.Boogie { inline = true;
}
}
- if (inline && CommandLineOptions.Clo.StratifiedInlining == 0) {
+ if (inline) {
foreach (var d in TopLevelDeclarations) {
var impl = d as Implementation;
if (impl != null) {
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index bdc74152..d7fcca7a 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -407,6 +407,8 @@ namespace Microsoft.Boogie { AddToFullMap(fullMap, impl.Name, block.Label, block);
}
+ bool detLoopExtract = CommandLineOptions.Clo.DeterministicExtractLoops;
+
Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
Dictionary<Block/*!*/, Hashtable/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Hashtable/*!*/>();
@@ -521,10 +523,6 @@ namespace Microsoft.Boogie { loopHeaderToOutputs[header] = outputs;
loopHeaderToSubstMap[header] = substMap;
LoopProcedure loopProc = new LoopProcedure(impl, header, inputs, outputs, globalMods);
- if (CommandLineOptions.Clo.StratifiedInlining > 0) {
- loopProc.AddAttribute("inline", Expr.Literal(1));
- loopProc.AddAttribute("verify", Expr.Literal(false));
- }
loopHeaderToLoopProc[header] = loopProc;
CallCmd callCmd1 = new CallCmd(Token.NoToken, loopProc.Name, callInputs1, callOutputs1);
@@ -576,6 +574,28 @@ namespace Microsoft.Boogie { newBlock2.Cmds = codeCopier.CopyCmdSeq(newBlocksCreated[block].Cmds);
blockMap[newBlocksCreated[block]] = newBlock2;
}
+ //for detLoopExtract, need the immediate successors even outside the loop
+ if (detLoopExtract) {
+ GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
+ Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
+ auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Length >= 1);
+ foreach(var bl in auxGotoCmd.labelTargets) {
+ bool found = false;
+ foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains?
+ if (bl == n) { //clarify: is this the right comparison?
+ found = true;
+ break;
+ }
+ }
+ if (!found) {
+ Block auxNewBlock = new Block();
+ auxNewBlock.Label = ((Block)bl).Label;
+ auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)block).Cmds);
+ blockMap[(Block)bl] = auxNewBlock;
+ }
+ }
+
+ }
}
CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone();
@@ -611,17 +631,21 @@ namespace Microsoft.Boogie { new StringSeq(cce.NonNull(blockMap[header]).Label, exit.Label),
new BlockSeq(blockMap[header], exit));
+ if (detLoopExtract) //cutting the non-determinism
+ cmd = new GotoCmd(Token.NoToken,
+ new StringSeq(cce.NonNull(blockMap[header]).Label),
+ new BlockSeq(blockMap[header]));
+
Block entry;
- if (loopHeaderToAssignCmd.ContainsKey(header))
- {
+ CmdSeq initCmds = new CmdSeq();
+ if (loopHeaderToAssignCmd.ContainsKey(header)) {
AssignCmd assignCmd = loopHeaderToAssignCmd[header];
- entry = new Block(Token.NoToken, "entry", new CmdSeq(assignCmd), cmd);
- }
- else
- {
- entry = new Block(Token.NoToken, "entry", new CmdSeq(), cmd);
+ initCmds.Add(assignCmd);
}
+
+ entry = new Block(Token.NoToken, "entry", initCmds, cmd);
blocks.Add(entry);
+
foreach (Block/*!*/ block in blockMap.Keys) {
Contract.Assert(block != null);
Block/*!*/ newBlock = cce.NonNull(blockMap[block]);
@@ -637,11 +661,27 @@ namespace Microsoft.Boogie { if (blockMap.ContainsKey(target)) {
newLabels.Add(gotoCmd.labelNames[i]);
newTargets.Add(blockMap[target]);
- }
+ }
}
if (newTargets.Length == 0) {
- newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+ if (!detLoopExtract)
+ newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
+ else {
+ if (loopHeaderToAssignCmd.ContainsKey(header)) {
+ AssignCmd assignCmd = loopHeaderToAssignCmd[header];
+ newBlock.Cmds.Add(assignCmd);
+ }
+ List<AssignLhs> lhsg = new List<AssignLhs>();
+ IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
+ foreach (IdentifierExpr gl in globalsMods)
+ lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
+ List<Expr> rhsg = new List<Expr>();
+ foreach (IdentifierExpr gl in globalsMods)
+ rhsg.Add(new OldExpr(Token.NoToken, gl));
+ AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);
+ newBlock.Cmds.Add(globalAssignCmd);
+ }
+ newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
} else {
newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);
}
@@ -2438,6 +2478,10 @@ namespace Microsoft.Boogie { }
}
+ if (CommandLineOptions.Clo.StratifiedInlining > 0) {
+ return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint");
+ }
+
return false;
}
}
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 3e7fd79e..5baf8667 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -562,11 +562,11 @@ namespace Microsoft.Boogie { public Inlining ProcedureInlining = Inlining.Assume;
public bool PrintInlined = false;
public bool ExtractLoops = false;
+ public bool DeterministicExtractLoops = false;
public int StratifiedInlining = 0;
public int StratifiedInliningOption = 0;
public bool StratifiedInliningWithoutModels = false; // disable model generation for SI
public int StratifiedInliningVerbose = 0; // verbosity level
- public bool BctModeForStratifiedInlining = false;
public int RecursionBound = 500;
public bool NonUniformUnfolding = false;
public string inferLeastForUnsat = null;
@@ -954,6 +954,12 @@ namespace Microsoft.Boogie { if (ps.ConfirmArgumentCount(0)) {
ExtractLoops = true;
}
+ return true;
+
+ case "deterministicExtractLoops":
+ if (ps.ConfirmArgumentCount(0)) {
+ DeterministicExtractLoops = true;
+ }
return true;
case "inline":
@@ -999,12 +1005,6 @@ namespace Microsoft.Boogie { StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));
}
return true;
- case "siBct":
- if (ps.ConfirmArgumentCount(1))
- {
- BctModeForStratifiedInlining = (Int32.Parse(cce.NonNull(args[ps.i])) == 1);
- }
- return true;
case "recursionBound":
if (ps.ConfirmArgumentCount(1)) {
RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));
@@ -1559,6 +1559,7 @@ namespace Microsoft.Boogie { n = none (unsound)
p = predicates (default)
a = arguments
+ m = monomorphic
/monomorphize
Do not abstract map types in the encoding (this is an
experimental feature that will not do the right thing if
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs new file mode 100644 index 00000000..15ad2432 --- /dev/null +++ b/Source/GPUVerify/BlockPredicator.cs @@ -0,0 +1,191 @@ +using Microsoft.Boogie; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace GPUVerify { + +class BlockPredicator { + + Program prog; + Implementation impl; + + Expr returnBlockId; + + LocalVariable curVar, pVar; + IdentifierExpr cur, p; + Expr pExpr; + Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars = + new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>(); + Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>(); + + BlockPredicator(Program p, Implementation i) { + prog = p; + impl = i; + } + + void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) { + if (cmd is AssignCmd) { + var aCmd = (AssignCmd)cmd; + cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss, + new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) => + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(p, rhs, lhs.AsExpr)))))); + } else if (cmd is AssertCmd) { + var aCmd = (AssertCmd)cmd; + if (cmdSeq.Last() is AssignCmd && + cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) { + // This may be a loop invariant. Make sure it continues to appear as + // the first statement in the block. + var assign = cmdSeq.Last(); + cmdSeq.Truncate(cmdSeq.Length-1); + cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr))); + cmdSeq.Add(assign); + } else { + cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr))); + } + } else if (cmd is AssumeCmd) { + var aCmd = (AssumeCmd)cmd; + cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr))); + } else if (cmd is HavocCmd) { + var hCmd = (HavocCmd)cmd; + foreach (IdentifierExpr v in hCmd.Vars) { + Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type; + Contract.Assert(type != null); + + IdentifierExpr havocTempExpr; + if (havocVars.ContainsKey(type)) { + havocTempExpr = havocVars[type]; + } else { + var havocVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, + "_HAVOC_" + type.ToString(), type)); + impl.LocVars.Add(havocVar); + havocVars[type] = havocTempExpr = + new IdentifierExpr(Token.NoToken, havocVar); + } + cmdSeq.Add(new HavocCmd(Token.NoToken, + new IdentifierExprSeq(havocTempExpr))); + cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v, + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(p, havocTempExpr, v)))); + } + } else if (cmd is CallCmd) { + var cCmd = (CallCmd)cmd; + cCmd.Ins.Insert(0, p); + cmdSeq.Add(cCmd); + } else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) { + if (cmd is GotoCmd) { + var gCmd = (GotoCmd)cmd; + var targets = new List<Expr>( + gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b])); + if (targets.Count == 1) { + PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0])); + } else { + PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken, + new IdentifierExprSeq(cur))); + PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken, + targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or))); + } + } else if (cmd is ReturnCmd) { + PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId)); + } else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + void PredicateImplementation() { + var g = prog.ProcessLoops(impl); + var sortedBlocks = g.LoopyTopSort(); + + int blockId = 0; + foreach (var block in impl.Blocks) + blockIds[block] = Expr.Literal(blockId++); + returnBlockId = Expr.Literal(blockId++); + + curVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, "cur", + Microsoft.Boogie.Type.Int)); + impl.LocVars.Add(curVar); + cur = Expr.Ident(curVar); + + pVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, "p", + Microsoft.Boogie.Type.Bool)); + impl.LocVars.Add(pVar); + p = Expr.Ident(pVar); + + var newBlocks = new List<Block>(); + + var fp = Expr.Ident(impl.InParams[0]); + Block entryBlock = new Block(); + entryBlock.Label = "entry"; + entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(fp, blockIds[sortedBlocks[0].Item1], + returnBlockId)))); + newBlocks.Add(entryBlock); + + var prevBlock = entryBlock; + foreach (var n in sortedBlocks) { + if (n.Item2) { + var tailBlock = new Block(); + newBlocks.Add(tailBlock); + + tailBlock.Label = n.Item1.Label + ".tail"; + tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, + Expr.Neq(cur, blockIds[n.Item1]))); + + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(tailBlock, n.Item1)); + prevBlock = tailBlock; + } else { + var runBlock = n.Item1; + newBlocks.Add(runBlock); + + pExpr = Expr.Eq(cur, blockIds[runBlock]); + CmdSeq newCmdSeq = new CmdSeq(); + newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); + foreach (Cmd cmd in runBlock.Cmds) + PredicateCmd(newCmdSeq, cmd); + PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd); + runBlock.Cmds = newCmdSeq; + + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(runBlock)); + prevBlock = runBlock; + } + } + + prevBlock.TransferCmd = new ReturnCmd(Token.NoToken); + impl.Blocks = newBlocks; + } + + public static void Predicate(Program p) { + foreach (var decl in p.TopLevelDeclarations) { + if (decl is DeclWithFormals && !(decl is Function)) { + var dwf = (DeclWithFormals)decl; + var fpVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, "fp", + Microsoft.Boogie.Type.Bool)); + dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar)) + .Cast<Variable>().ToArray()); + } + var impl = decl as Implementation; + if (impl != null) + new BlockPredicator(p, impl).PredicateImplementation(); + } + } + +} + +} diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 502844b2..7e6324b2 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -40,6 +40,8 @@ namespace GPUVerify public static bool NoLoopPredicateInvariants = false;
+ public static bool Unstructured = false;
+
public static int Parse(string[] args)
{
for (int i = 0; i < args.Length; i++)
@@ -177,6 +179,11 @@ namespace GPUVerify NoLoopPredicateInvariants = true;
break;
+ case "-unstructured":
+ case "/unstructured":
+ Unstructured = true;
+ break;
+
default:
inputFiles.Add(args[i]);
break;
@@ -216,6 +223,7 @@ namespace GPUVerify /divided : check individual pairs of possibly racing statements separately
/dividedArray : check races on arrays one at a time
/dividedElement : ???
+ /unstructured : operate on the unstructured form of the program
");
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index c249ef0f..7b78f0f1 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -312,7 +312,7 @@ namespace GPUVerify Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));
- Expr AccessedOffsetLtCTimesLocalIdPlusC = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT", OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);
+ Expr AccessedOffsetLtCTimesLocalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);
return Expr.Imp(
AccessHasOccurred(v, ReadOrWrite, Thread),
@@ -346,7 +346,7 @@ namespace GPUVerify Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));
- Expr AccessedOffsetLtCTimesGlobalIdPlusC = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT", OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);
+ Expr AccessedOffsetLtCTimesGlobalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);
Expr implication = Expr.Imp(
AccessHasOccurred(v, ReadOrWrite, Thread),
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index f6ba390b..6659566b 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -14,6 +14,7 @@ namespace GPUVerify {
public string outputFilename;
public Program Program;
+ public ResolutionContext ResContext;
public Procedure KernelProcedure;
public Implementation KernelImplementation;
@@ -71,15 +72,16 @@ namespace GPUVerify public LiveVariableAnalyser liveVariableAnalyser;
public ArrayControlFlowAnalyser arrayControlFlowAnalyser;
- public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter) : this(filename, program, raceInstrumenter, false)
+ public GPUVerifier(string filename, Program program, ResolutionContext rc, IRaceInstrumenter raceInstrumenter) : this(filename, program, rc, raceInstrumenter, false)
{
}
- public GPUVerifier(string filename, Program program, IRaceInstrumenter raceInstrumenter, bool skipCheck)
+ public GPUVerifier(string filename, Program program, ResolutionContext rc, IRaceInstrumenter raceInstrumenter, bool skipCheck)
: base((IErrorSink)null)
{
this.outputFilename = filename;
this.Program = program;
+ this.ResContext = rc;
this.RaceInstrumenter = raceInstrumenter;
if(!skipCheck)
CheckWellFormedness();
@@ -102,19 +104,35 @@ namespace GPUVerify private Procedure CheckExactlyOneKernelProcedure()
{
- return CheckSingleInstanceOfAttributedProcedure(Program, "kernel");
+ var p = CheckSingleInstanceOfAttributedProcedure("kernel");
+ if (p == null)
+ {
+ Error(Program, "\"kernel\" attribute has not been specified for any procedure. You must mark exactly one procedure with this attribute");
+ }
+
+ return p;
}
- private Procedure CheckExactlyOneBarrierProcedure()
+ private Procedure FindOrCreateBarrierProcedure()
{
- return CheckSingleInstanceOfAttributedProcedure(Program, "barrier");
+ var p = CheckSingleInstanceOfAttributedProcedure("barrier");
+ if (p == null)
+ {
+ p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),
+ new VariableSeq(), new VariableSeq(),
+ new RequiresSeq(), new IdentifierExprSeq(),
+ new EnsuresSeq(),
+ new QKeyValue(Token.NoToken, "barrier", new List<object>(), null));
+ Program.TopLevelDeclarations.Add(p);
+ }
+ return p;
}
- private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)
+ private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute)
{
Procedure attributedProcedure = null;
- foreach (Declaration decl in program.TopLevelDeclarations)
+ foreach (Declaration decl in Program.TopLevelDeclarations)
{
if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))
{
@@ -144,11 +162,6 @@ namespace GPUVerify }
}
- if (attributedProcedure == null)
- {
- Error(program, "\"{0}\" attribute has not been specified for any procedure. You must mark exactly one procedure with this attribute", attribute);
- }
-
return attributedProcedure;
}
@@ -189,10 +202,20 @@ namespace GPUVerify return true;
}
- private bool FindNonLocalVariables(Program program)
+ private void MaybeCreateAttributedConst(string attr, ref Constant constFieldRef)
+ {
+ if (constFieldRef == null)
+ {
+ constFieldRef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, attr, Microsoft.Boogie.Type.GetBvType(32)), /*unique=*/false);
+ constFieldRef.AddAttribute(attr);
+ Program.TopLevelDeclarations.Add(constFieldRef);
+ }
+ }
+
+ private bool FindNonLocalVariables()
{
bool success = true;
- foreach (Declaration D in program.TopLevelDeclarations)
+ foreach (Declaration D in Program.TopLevelDeclarations)
{
if (D is Variable && (D as Variable).IsMutable)
{
@@ -232,6 +255,22 @@ namespace GPUVerify }
}
+ MaybeCreateAttributedConst(LOCAL_ID_X_STRING, ref _X);
+ MaybeCreateAttributedConst(LOCAL_ID_Y_STRING, ref _Y);
+ MaybeCreateAttributedConst(LOCAL_ID_Z_STRING, ref _Z);
+
+ MaybeCreateAttributedConst(GROUP_SIZE_X_STRING, ref _GROUP_SIZE_X);
+ MaybeCreateAttributedConst(GROUP_SIZE_Y_STRING, ref _GROUP_SIZE_Y);
+ MaybeCreateAttributedConst(GROUP_SIZE_Z_STRING, ref _GROUP_SIZE_Z);
+
+ MaybeCreateAttributedConst(GROUP_ID_X_STRING, ref _GROUP_X);
+ MaybeCreateAttributedConst(GROUP_ID_Y_STRING, ref _GROUP_Y);
+ MaybeCreateAttributedConst(GROUP_ID_Z_STRING, ref _GROUP_Z);
+
+ MaybeCreateAttributedConst(NUM_GROUPS_X_STRING, ref _NUM_GROUPS_X);
+ MaybeCreateAttributedConst(NUM_GROUPS_Y_STRING, ref _NUM_GROUPS_Y);
+ MaybeCreateAttributedConst(NUM_GROUPS_Z_STRING, ref _NUM_GROUPS_Z);
+
return success;
}
@@ -307,6 +346,10 @@ namespace GPUVerify internal void doit()
{
+ if (CommandLineOptions.Unstructured)
+ {
+ Microsoft.Boogie.CommandLineOptions.Clo.PrintUnstructured = 2;
+ }
if (CommandLineOptions.ShowStages)
{
@@ -395,7 +438,8 @@ namespace GPUVerify {
Program p = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { outputFilename + ".bpl" }), true);
- p.Resolve();
+ ResolutionContext rc = new ResolutionContext(null);
+ p.Resolve(rc);
p.Typecheck();
Contract.Assert(p != null);
@@ -403,7 +447,7 @@ namespace GPUVerify Implementation impl = null;
{
- GPUVerifier tempGPUV = new GPUVerifier("not_used", p, new NullRaceInstrumenter(), true);
+ GPUVerifier tempGPUV = new GPUVerifier("not_used", p, rc, new NullRaceInstrumenter(), true);
tempGPUV.KernelProcedure = tempGPUV.CheckExactlyOneKernelProcedure();
tempGPUV.GetKernelImplementation();
impl = tempGPUV.KernelImplementation;
@@ -1148,7 +1192,7 @@ namespace GPUVerify private void GeneratePreconditionsForDimension(ref Expr AssumeDistinctThreads, ref Expr AssumeThreadIdsInRange, IToken tok, String dimension)
{
- foreach (Declaration D in Program.TopLevelDeclarations)
+ foreach (Declaration D in Program.TopLevelDeclarations.ToList())
{
if (!(D is Procedure))
{
@@ -1162,10 +1206,10 @@ namespace GPUVerify if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))
{
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV(tok))));
- Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
+ Proc.Requires.Add(new Requires(false, MakeBVSgt(new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBVSgt(new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBVSge(new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBVSlt(new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
}
else
{
@@ -1188,12 +1232,12 @@ namespace GPUVerify GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)) ?
Expr.And(
Expr.And(
- MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), ZeroBV(tok)),
- MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), ZeroBV(tok))
+ MakeBVSge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), ZeroBV(tok)),
+ MakeBVSge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), ZeroBV(tok))
),
Expr.And(
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
+ MakeBVSlt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ MakeBVSlt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
))
:
Expr.And(
@@ -1209,6 +1253,41 @@ namespace GPUVerify AssumeThreadIdsInRange = (null == AssumeThreadIdsInRange) ? AssumeThreadIdsInRangeInDimension : Expr.And(AssumeThreadIdsInRange, AssumeThreadIdsInRangeInDimension);
}
+ private Function GetOrCreateBVFunction(string functionName, string smtName, Microsoft.Boogie.Type resultType, params Microsoft.Boogie.Type[] argTypes)
+ {
+ Function f = (Function)ResContext.LookUpProcedure(functionName);
+ if (f != null)
+ return f;
+
+ f = new Function(Token.NoToken, functionName,
+ new VariableSeq(argTypes.Select(t => new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "", t))).ToArray()),
+ new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "", resultType)));
+ f.AddAttribute("bvbuiltin", smtName);
+ Program.TopLevelDeclarations.Add(f);
+ ResContext.AddProcedure(f);
+ return f;
+ }
+
+ private Expr MakeBVFunctionCall(string functionName, string smtName, Microsoft.Boogie.Type resultType, params Expr[] args)
+ {
+ Function f = GetOrCreateBVFunction(functionName, smtName, resultType, args.Select(a => a.Type).ToArray());
+ return new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));
+ }
+
+ private Expr MakeBitVectorBinaryBoolean(string suffix, string smtName, Expr lhs, Expr rhs)
+ {
+ return MakeBVFunctionCall("BV" + lhs.Type.BvBits + "_" + suffix, smtName, Microsoft.Boogie.Type.Bool, lhs, rhs);
+ }
+
+ private Expr MakeBitVectorBinaryBitVector(string suffix, string smtName, Expr lhs, Expr rhs)
+ {
+ return MakeBVFunctionCall("BV" + lhs.Type.BvBits + "_" + suffix, smtName, lhs.Type, lhs, rhs);
+ }
+
+ internal Expr MakeBVSlt(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SLT", "bvslt", lhs, rhs); }
+ internal Expr MakeBVSgt(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGT", "bvsgt", lhs, rhs); }
+ internal Expr MakeBVSge(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGE", "bvsge", lhs, rhs); }
+
internal static Expr MakeBitVectorBinaryBoolean(string functionName, Expr lhs, Expr rhs)
{
return new NAryExpr(lhs.tok, new FunctionCall(new Function(lhs.tok, functionName, new VariableSeq(new Variable[] {
@@ -1920,7 +1999,7 @@ namespace GPUVerify if (d is Implementation)
{
- new KernelDualiser(this).DualiseImplementation(d as Implementation);
+ new KernelDualiser(this).DualiseImplementation(d as Implementation, CommandLineOptions.Unstructured);
NewTopLevelDeclarations.Add(d as Implementation);
@@ -1946,6 +2025,12 @@ namespace GPUVerify private void MakeKernelPredicated()
{
+ if (CommandLineOptions.Unstructured)
+ {
+ BlockPredicator.Predicate(Program);
+ return;
+ }
+
foreach (Declaration d in Program.TopLevelDeclarations)
{
if (d is Procedure)
@@ -2007,7 +2092,7 @@ namespace GPUVerify private int Check()
{
- BarrierProcedure = CheckExactlyOneBarrierProcedure();
+ BarrierProcedure = FindOrCreateBarrierProcedure();
KernelProcedure = CheckExactlyOneKernelProcedure();
if (ErrorCount > 0)
@@ -2025,101 +2110,15 @@ namespace GPUVerify Error(BarrierProcedure, "Barrier procedure must not return any results");
}
- if (!FindNonLocalVariables(Program))
+ if (!FindNonLocalVariables())
{
return ErrorCount;
}
CheckKernelImplementation();
-
- if (!KernelHasIdX())
- {
- MissingKernelAttributeError(LOCAL_ID_X_STRING);
- }
-
- if (!KernelHasGroupSizeX())
- {
- MissingKernelAttributeError(GROUP_SIZE_X_STRING);
- }
-
- if (!KernelHasNumGroupsX())
- {
- MissingKernelAttributeError(NUM_GROUPS_X_STRING);
- }
-
- if (!KernelHasGroupIdX())
- {
- MissingKernelAttributeError(GROUP_ID_X_STRING);
- }
-
- if (!KernelHasIdY())
- {
- MissingKernelAttributeError(LOCAL_ID_Y_STRING);
- }
-
- if (!KernelHasGroupSizeY())
- {
- MissingKernelAttributeError(GROUP_SIZE_Y_STRING);
- }
-
- if (!KernelHasNumGroupsY())
- {
- MissingKernelAttributeError(NUM_GROUPS_Y_STRING);
- }
-
- if (!KernelHasGroupIdY())
- {
- MissingKernelAttributeError(GROUP_ID_Y_STRING);
- }
-
- if (!KernelHasIdY())
- {
- MissingKernelAttributeError(LOCAL_ID_Y_STRING);
- }
-
- if (!KernelHasGroupSizeY())
- {
- MissingKernelAttributeError(GROUP_SIZE_Y_STRING);
- }
-
- if (!KernelHasNumGroupsY())
- {
- MissingKernelAttributeError(NUM_GROUPS_Y_STRING);
- }
-
- if (!KernelHasGroupIdY())
- {
- MissingKernelAttributeError(GROUP_ID_Y_STRING);
- }
-
- if (!KernelHasIdZ())
- {
- MissingKernelAttributeError(LOCAL_ID_Z_STRING);
- }
-
- if (!KernelHasGroupSizeZ())
- {
- MissingKernelAttributeError(GROUP_SIZE_Z_STRING);
- }
-
- if (!KernelHasNumGroupsZ())
- {
- MissingKernelAttributeError(NUM_GROUPS_Z_STRING);
- }
-
- if (!KernelHasGroupIdZ())
- {
- MissingKernelAttributeError(GROUP_ID_Z_STRING);
- }
-
return ErrorCount;
}
- private void MissingKernelAttributeError(string attribute)
- {
- Error(KernelProcedure.tok, "Kernel must declare global constant marked with attribute ':" + attribute + "'");
- }
-
public static bool IsThreadLocalIdConstant(Variable variable)
{
return variable.Name.Equals(_X.Name) || variable.Name.Equals(_Y.Name) || variable.Name.Equals(_Z.Name);
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index b375efd9..27b9abe5 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -108,6 +108,8 @@ <Compile Include="AccessRecord.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
+ <Compile Include="BlockPredicator.cs" />
+ <Compile Include="GraphAlgorithms.cs" />
<Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
<Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
<Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
@@ -158,6 +160,10 @@ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
<Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/GPUVerify/GraphAlgorithms.cs new file mode 100644 index 00000000..3442a64d --- /dev/null +++ b/Source/GPUVerify/GraphAlgorithms.cs @@ -0,0 +1,84 @@ +using Graphing; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace GPUVerify { + +public static class GraphAlgorithms { + + public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) { + Contract.Assert(g.Reducible); + + int n = g.Nodes.Count; + var nodeToNumber = new Dictionary<Node, int>(n); + var numberToNode = new Node[n]; + var allNodes = new List<int>(); + int counter = 0; + foreach (Node node in g.Nodes) { + numberToNode[counter] = node; + nodeToNumber[node] = counter; + allNodes.Add(counter); + counter++; + } + + var loops = new List<int>[n]; + foreach (var h in g.Headers) { + var loopNodes = new HashSet<Node>(); + foreach (var b in g.BackEdgeNodes(h)) + loopNodes.UnionWith(g.NaturalLoops(h, b)); + loops[nodeToNumber[h]] = + new List<int>(loopNodes.Select(node => nodeToNumber[node])); + } + + var successors = new List<int>[n]; + int[] incomingEdges = new int[n]; + + foreach (var e in g.Edges) { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2]; + if (loops[target] == null || !loops[target].Contains(source)) { + if (successors[source] == null) + successors[source] = new List<int>(); + successors[source].Add(target); + incomingEdges[target]++; + } + } + + var sortedNodes = new List<Tuple<Node, bool>>(); + + var regionStack = new Stack<Tuple<Node, List<int>>>(); + regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes)); + + while (regionStack.Count != 0) { + int rootIndex = -1; + foreach (var i in regionStack.Peek().Item2) { + if (incomingEdges[i] == 0) { + rootIndex = i; + break; + } + } + if (rootIndex == -1) { + var region = regionStack.Pop(); + if (regionStack.Count != 0) + sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true)); + continue; + } + incomingEdges[rootIndex] = -1; + sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false)); + if (successors[rootIndex] != null) + foreach (int s in successors[rootIndex]) + incomingEdges[s]--; + if (loops[rootIndex] != null) + regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex], + loops[rootIndex])); + } + + return sortedNodes; + } + +} + +} diff --git a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs index 233b3b45..af5f8d71 100644 --- a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs +++ b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs @@ -35,7 +35,7 @@ namespace GPUVerify.InvariantGenerationRules int BVWidth = (v.TypedIdent.Type as BvType).Bits;
verifier.AddCandidateInvariant(wc,
- GPUVerifier.MakeBitVectorBinaryBoolean("BV" + BVWidth + "_GEQ",
+ verifier.MakeBVSge(
new IdentifierExpr(v.tok, v),
new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");
}
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 0496a4e0..8d51e74e 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -82,145 +82,150 @@ namespace GPUVerify return result;
}
- private BigBlock MakeDual(BigBlock bb)
+ private void MakeDual(CmdSeq cs, Cmd c)
{
- // Not sure what to do about the transfer command
-
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
- foreach (Cmd c in bb.simpleCmds)
+ if (c is CallCmd)
{
- if (c is CallCmd)
- {
- CallCmd Call = c as CallCmd;
+ CallCmd Call = c as CallCmd;
- List<Expr> uniformNewIns = new List<Expr>();
- List<Expr> nonUniformNewIns = new List<Expr>();
- for (int i = 0; i < Call.Ins.Count; i++)
+ List<Expr> uniformNewIns = new List<Expr>();
+ List<Expr> nonUniformNewIns = new List<Expr>();
+ for (int i = 0; i < Call.Ins.Count; i++)
+ {
+ if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))
{
- if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))
- {
- uniformNewIns.Add(Call.Ins[i]);
- }
- else
- {
- nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
- }
+ uniformNewIns.Add(Call.Ins[i]);
}
- for (int i = 0; i < Call.Ins.Count; i++)
+ else
{
- if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
- {
- nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
- }
+ nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
}
+ }
+ for (int i = 0; i < Call.Ins.Count; i++)
+ {
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))
+ {
+ nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));
+ }
+ }
- List<Expr> newIns = uniformNewIns;
- newIns.AddRange(nonUniformNewIns);
+ List<Expr> newIns = uniformNewIns;
+ newIns.AddRange(nonUniformNewIns);
- List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();
- List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();
- for (int i = 0; i < Call.Outs.Count; i++)
+ List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();
+ List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();
+ for (int i = 0; i < Call.Outs.Count; i++)
+ {
+ if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))
{
- if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))
- {
- uniformNewOuts.Add(Call.Outs[i]);
- }
- else
- {
- nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
- }
-
+ uniformNewOuts.Add(Call.Outs[i]);
}
- for (int i = 0; i < Call.Outs.Count; i++)
+ else
{
- if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
- {
- nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
- }
+ nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
}
- List<IdentifierExpr> newOuts = uniformNewOuts;
- newOuts.AddRange(nonUniformNewOuts);
-
- CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
-
- NewCallCmd.Proc = Call.Proc;
-
- result.simpleCmds.Add(NewCallCmd);
}
- else if (c is AssignCmd)
+ for (int i = 0; i < Call.Outs.Count; i++)
{
- AssignCmd assign = c as AssignCmd;
-
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- if (assign.Lhss[0] is SimpleAssignLhs &&
- verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))
+ if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))
{
- result.simpleCmds.Add(assign);
+ nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);
}
- else
- {
- List<AssignLhs> newLhss = new List<AssignLhs>();
- List<Expr> newRhss = new List<Expr>();
+ }
- newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
- newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+ List<IdentifierExpr> newOuts = uniformNewOuts;
+ newOuts.AddRange(nonUniformNewOuts);
- newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
- newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);
- AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
+ NewCallCmd.Proc = Call.Proc;
- result.simpleCmds.Add(newAssign);
- }
+ cs.Add(NewCallCmd);
+ }
+ else if (c is AssignCmd)
+ {
+ AssignCmd assign = c as AssignCmd;
+
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+
+ if (assign.Lhss[0] is SimpleAssignLhs &&
+ verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))
+ {
+ cs.Add(assign);
}
- else if (c is HavocCmd)
+ else
{
- HavocCmd havoc = c as HavocCmd;
- Debug.Assert(havoc.Vars.Length == 1);
+ List<AssignLhs> newLhss = new List<AssignLhs>();
+ List<Expr> newRhss = new List<Expr>();
+
+ newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+ newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
+
+ newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+ newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
+
+ AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);
+
+ cs.Add(newAssign);
+ }
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havoc = c as HavocCmd;
+ Debug.Assert(havoc.Vars.Length == 1);
- HavocCmd newHavoc;
+ HavocCmd newHavoc;
- newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
- (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
- }));
+ newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)),
+ (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
+ }));
- result.simpleCmds.Add(newHavoc);
+ cs.Add(newHavoc);
+ }
+ else if (c is AssertCmd)
+ {
+ AssertCmd ass = c as AssertCmd;
+ if (ContainsAsymmetricExpression(ass.Expr))
+ {
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
}
- else if (c is AssertCmd)
+ else
{
- AssertCmd ass = c as AssertCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else
- {
- result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
- }
+ cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
- else if (c is AssumeCmd)
+ }
+ else if (c is AssumeCmd)
+ {
+ AssumeCmd ass = c as AssumeCmd;
+ if (ContainsAsymmetricExpression(ass.Expr))
{
- AssumeCmd ass = c as AssumeCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else
- {
- result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
- }
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
}
else
{
- Debug.Assert(false);
+ cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
+ new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
}
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+
+ private BigBlock MakeDual(BigBlock bb)
+ {
+ // Not sure what to do about the transfer command
+
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ MakeDual(result.simpleCmds, c);
+ }
if (bb.ec is WhileCmd)
{
@@ -262,6 +267,16 @@ namespace GPUVerify }
+ private Block MakeDual(Block b)
+ {
+ Block result = new Block(b.tok, b.Label, new CmdSeq(), b.TransferCmd);
+ foreach (Cmd c in b.Cmds)
+ {
+ MakeDual(result.Cmds, c);
+ }
+ return result;
+ }
+
private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)
{
List<PredicateCmd> result = new List<PredicateCmd>();
@@ -345,14 +360,17 @@ namespace GPUVerify }
- internal void DualiseImplementation(Implementation impl)
+ internal void DualiseImplementation(Implementation impl, bool unstructured)
{
procName = impl.Name;
impl.InParams = DualiseVariableSequence(impl.InParams);
impl.OutParams = DualiseVariableSequence(impl.OutParams);
MakeDualLocalVariables(impl);
- impl.StructuredStmts = MakeDual(impl.StructuredStmts);
+ if (unstructured)
+ impl.Blocks = new List<Block>(impl.Blocks.Select(MakeDual));
+ else
+ impl.StructuredStmts = MakeDual(impl.StructuredStmts);
procName = null;
}
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 1e0a6b4a..c8d29282 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -48,7 +48,7 @@ namespace GPUVerify parseProcessOutput();
}
- public static Program parse()
+ public static Program parse(out ResolutionContext rc)
{
Program program = ParseBoogieProgram(CommandLineOptions.inputFiles, false);
if (program == null)
@@ -58,15 +58,15 @@ namespace GPUVerify Microsoft.Boogie.CommandLineOptions.Clo.DoModSetAnalysis = true;
- int errorCount = program.Resolve();
- if (errorCount != 0)
+ rc = new ResolutionContext(null);
+ program.Resolve(rc);
+ if (rc.ErrorCount != 0)
{
- Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
+ Console.WriteLine("{0} name resolution errors detected in {1}", rc.ErrorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
Environment.Exit(1);
}
- errorCount = program.Typecheck();
-
+ int errorCount = program.Typecheck();
if (errorCount != 0)
{
Console.WriteLine("{0} type checking errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);
@@ -90,9 +90,10 @@ namespace GPUVerify public static bool doit(string filename, Variable v, int a1, int a2)
{
- Program newProgram = parse();
+ ResolutionContext rc;
+ Program newProgram = parse(out rc);
RaceInstrumenterBase ri = new ElementEncodingRaceInstrumenter();
- GPUVerifier newGp = new GPUVerifier(filename, newProgram, ri);
+ GPUVerifier newGp = new GPUVerifier(filename, newProgram, rc, ri);
ri.setVerifier(newGp);
@@ -128,9 +129,10 @@ namespace GPUVerify {
fn = CommandLineOptions.outputFile;
}
- Program program = parse();
+ ResolutionContext rc;
+ Program program = parse(out rc);
IList<GPUVerifier> result = new List<GPUVerifier>();
- GPUVerifier g = new GPUVerifier(fn, program, new NullRaceInstrumenter());
+ GPUVerifier g = new GPUVerifier(fn, program, rc, new NullRaceInstrumenter());
if (CommandLineOptions.DividedArray)
{
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 7ae7ca44..11feb017 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -798,9 +798,17 @@ namespace GPUVerify return result;
}
+ private Block AddRaceCheckCalls(Block b)
+ {
+ return new Block(Token.NoToken, b.Label, AddRaceCheckCalls(b.Cmds), b.TransferCmd);
+ }
+
private void AddRaceCheckCalls(Implementation impl)
{
- impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
+ if (CommandLineOptions.Unstructured)
+ impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
+ else
+ impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
}
private bool shouldAddLogCallAndIncr()
@@ -828,13 +836,12 @@ namespace GPUVerify return false;
}
- private BigBlock AddRaceCheckCalls(BigBlock bb)
+ private CmdSeq AddRaceCheckCalls(CmdSeq cs)
{
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
- foreach (Cmd c in bb.simpleCmds)
+ var result = new CmdSeq();
+ foreach (Cmd c in cs)
{
- result.simpleCmds.Add(c);
+ result.Add(c);
if (c is AssignCmd)
{
AssignCmd assign = c as AssignCmd;
@@ -873,8 +880,8 @@ namespace GPUVerify logAccessCallCmd.Proc = logProcedure;
- result.simpleCmds.Add(logAccessCallCmd);
-
+ cs.Add(logAccessCallCmd);
+
}
}
@@ -907,17 +914,20 @@ namespace GPUVerify logAccessCallCmd.Proc = logProcedure;
- result.simpleCmds.Add(logAccessCallCmd);
-
+ cs.Add(logAccessCallCmd);
+
addedLogWrite = true;
-
+
}
}
-
-
-
}
}
+ return result;
+ }
+
+ private BigBlock AddRaceCheckCalls(BigBlock bb)
+ {
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, AddRaceCheckCalls(bb.simpleCmds), null, bb.tc);
if (bb.ec is WhileCmd)
{
@@ -941,7 +951,6 @@ namespace GPUVerify }
return result;
-
}
private Procedure GetLogAccessProcedure(IToken tok, string name)
diff --git a/Source/GPUVerify/UniformityAnalyser.cs b/Source/GPUVerify/UniformityAnalyser.cs index c910e64d..bd0e3f74 100644 --- a/Source/GPUVerify/UniformityAnalyser.cs +++ b/Source/GPUVerify/UniformityAnalyser.cs @@ -41,6 +41,9 @@ namespace GPUVerify internal void Analyse()
{
+ if (CommandLineOptions.Unstructured)
+ return;
+
foreach (Declaration D in verifier.Program.TopLevelDeclarations)
{
if(D is Implementation)
@@ -283,6 +286,9 @@ namespace GPUVerify internal bool IsUniform(string procedureName)
{
+ if (CommandLineOptions.Unstructured)
+ return false;
+
if (!uniformityInfo.ContainsKey(procedureName))
{
return false;
@@ -292,6 +298,9 @@ namespace GPUVerify internal bool IsUniform(string procedureName, Expr expr)
{
+ if (CommandLineOptions.Unstructured)
+ return false;
+
UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value);
visitor.VisitExpr(expr);
return visitor.IsUniform();
@@ -299,6 +308,9 @@ namespace GPUVerify internal bool IsUniform(string procedureName, string v)
{
+ if (CommandLineOptions.Unstructured)
+ return false;
+
if (!uniformityInfo.ContainsKey(procedureName))
{
return false;
@@ -363,11 +375,17 @@ namespace GPUVerify internal string GetInParameter(string procName, int i)
{
+ if (CommandLineOptions.Unstructured)
+ return null;
+
return inParameters[procName][i];
}
internal string GetOutParameter(string procName, int i)
{
+ if (CommandLineOptions.Unstructured)
+ return null;
+
return outParameters[procName][i];
}
@@ -388,6 +406,9 @@ namespace GPUVerify internal bool IsUniform(string proc, WhileCmd wc)
{
+ if (CommandLineOptions.Unstructured)
+ return false;
+
return !nonUniformLoops[proc].Contains(GetLoopId(wc));
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 8f9f7498..65aa8486 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -13,3041 +13,2624 @@ using System.Diagnostics.Contracts; using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
-namespace VC
-{
- using Bpl = Microsoft.Boogie;
-
- public class StratifiedVCGen : VCGen
- {
- public override void Close() {
- prover.Close();
- base.Close();
- }
- private Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
- public bool PersistCallTree;
- public static Dictionary<string, int> callTree = null;
- public int numInlined = 0;
- public readonly static string recordProcName = "boogie_si_record";
- private bool useSummary;
- private SummaryComputation summaryComputation;
- private HashSet<string> procsThatReachedRecBound;
- ProverInterface prover;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- }
-
- /// <summary>
- /// Constructor. Initializes the theorem prover.
- /// </summary>
- [NotDelayed]
- public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
- : base(program, logFilePath, appendLogFile)
- {
- implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
- prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
- foreach (Declaration decl in program.TopLevelDeclarations) {
- Implementation impl = decl as Implementation;
- if (impl == null) continue;
- Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");
- if (impl.Proc.FindExprAttribute("inline") != null) {
- implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
- }
- }
- this.GenerateRecordFunctions();
- PersistCallTree = false;
- useSummary = false;
- procsThatReachedRecBound = new HashSet<string>();
- }
-
- internal class CallSitesSimplifier : StandardVisitor {
- VariableSeq localVars;
- StratifiedVCGen vcgen;
- public static void SimplifyCallSites(Implementation implementation, StratifiedVCGen vcgen) {
- CallSitesSimplifier visitor = new CallSitesSimplifier(vcgen);
- visitor.Visit(implementation);
- implementation.LocVars.AddRange(visitor.localVars);
+namespace VC {
+ using Bpl = Microsoft.Boogie;
+
+ public class StratifiedVC {
+ public StratifiedInliningInfo info;
+ public int id;
+ public List<VCExprVar> interfaceExprVars;
+ public Dictionary<Block, List<StratifiedCallSite>> callSites;
+ public VCExpr vcexpr;
+ public Dictionary<Block, VCExprVar> reachVars;
+
+ public StratifiedVC(StratifiedInliningInfo siInfo) {
+ info = siInfo;
+ if (!info.initialized) {
+ info.GenerateVC();
+ }
+
+ vcexpr = info.vcexpr;
+ var vcgen = info.vcgen;
+ var prover = vcgen.prover;
+ VCExpressionGenerator gen = prover.VCExprGen;
+ var bet = prover.Context.BoogieExprTranslator;
+ VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);
+ id = vcgen.CreateNewId();
+ VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));
+ vcexpr = gen.And(eqExpr, vcexpr);
+
+ var impl = info.impl;
+ reachVars = new Dictionary<Block, VCExprVar>();
+ Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();
+ foreach (Block b in impl.Blocks) {
+ reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);
+ reachExprs[b] = VCExpressionGenerator.False;
+ }
+ foreach (Block currBlock in impl.Blocks) {
+ GotoCmd gotoCmd = currBlock.TransferCmd as GotoCmd;
+ if (gotoCmd == null) continue;
+ foreach (Block successorBlock in gotoCmd.labelTargets) {
+ VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(currBlock.UniqueId)));
+ VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successorBlock.UniqueId)));
+ reachExprs[successorBlock] = gen.Or(reachExprs[successorBlock], gen.And(reachVars[currBlock], controlTransferExpr));
+ }
+ }
+ // The binding for entry block should be left defined;
+ // it will get filled in when the call tree is constructed
+ for (int i = 1; i < impl.Blocks.Count; i++) {
+ Block b = impl.Blocks[i];
+ vcexpr = gen.And(vcexpr, gen.Eq(reachVars[b], reachExprs[b]));
+ }
+
+ interfaceExprVars = new List<VCExprVar>();
+ Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
+ foreach (VCExprVar v in info.interfaceExprVars) {
+ VCExprVar newVar = vcgen.CreateNewVar(v.Type);
+ interfaceExprVars.Add(newVar);
+ substDict.Add(v, newVar);
+ }
+ foreach (VCExprVar v in info.privateExprVars) {
+ substDict.Add(v, vcgen.CreateNewVar(v.Type));
+ }
+ VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+ SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ vcexpr = substVisitor.Mutate(vcexpr, subst);
+
+ callSites = new Dictionary<Block, List<StratifiedCallSite>>();
+ foreach (Block b in info.callSites.Keys) {
+ callSites[b] = new List<StratifiedCallSite>();
+ foreach (CallSite cs in info.callSites[b]) {
+ callSites[b].Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
+ }
+ }
+ }
+
+ public List<StratifiedCallSite> CallSites {
+ get {
+ var ret = new List<StratifiedCallSite>();
+ foreach (var b in callSites.Keys) {
+ foreach (var cs in callSites[b]) {
+ ret.Add(cs);
+ }
+ }
+ return ret;
+ }
+ }
+ }
+
+ public class CallSite {
+ public string calleeName;
+ public List<VCExpr> interfaceExprs;
+ public Block block;
+ public int numInstr; // for TraceLocation
+ public CallSite(string callee, List<VCExpr> interfaceExprs, Block block, int numInstr) {
+ this.calleeName = callee;
+ this.interfaceExprs = interfaceExprs;
+ this.block = block;
+ this.numInstr = numInstr;
+ }
+ }
+
+ public class StratifiedCallSite {
+ public CallSite callSite;
+ public List<VCExpr> interfaceExprs;
+ public VCExprVar reachVar;
+
+ public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {
+ callSite = cs;
+ interfaceExprs = new List<VCExpr>();
+ foreach (VCExpr v in cs.interfaceExprs) {
+ interfaceExprs.Add(substVisitor.Mutate(v, subst));
+ }
+ reachVar = reachVars[cs.block];
+ }
+
+ public VCExpr Attach(StratifiedVC svc) {
+ Contract.Assert(interfaceExprs.Count == svc.interfaceExprVars.Count);
+ StratifiedInliningInfo info = svc.info;
+ VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;
+ VCExpr ret = gen.Eq(reachVar, svc.reachVars[info.impl.Blocks[0]]);
+ for (int i = 0; i < interfaceExprs.Count; i++) {
+ ret = gen.And(ret, gen.Eq(interfaceExprs[i], svc.interfaceExprVars[i]));
+ }
+ return ret;
+ }
+ }
+
+ public class StratifiedInliningInfo {
+ public StratifiedVCGenBase vcgen;
+ public Implementation impl;
+ public Function function;
+ public Variable controlFlowVariable;
+ public Expr assertExpr;
+ public VCExpr vcexpr;
+ public List<VCExprVar> interfaceExprVars;
+ public List<VCExprVar> privateExprVars;
+ public Hashtable/*<int, Absy!>*/ label2absy;
+ public ModelViewInfo mvInfo;
+ public Dictionary<Block, List<CallSite>> callSites;
+ public bool initialized { get; private set; }
+
+ public StratifiedInliningInfo(Implementation implementation, StratifiedVCGenBase stratifiedVcGen) {
+ vcgen = stratifiedVcGen;
+ impl = implementation;
+
+ VariableSeq functionInterfaceVars = new VariableSeq();
+ foreach (Variable v in vcgen.program.GlobalVariables()) {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (Variable v in impl.InParams) {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (Variable v in impl.OutParams) {
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
+ }
+ foreach (IdentifierExpr e in impl.Proc.Modifies) {
+ if (e.Decl == null) continue;
+ functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true));
+ }
+ Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false);
+ function = new Function(Token.NoToken, impl.Name, functionInterfaceVars, returnVar);
+ vcgen.prover.Context.DeclareFunction(function, "");
+
+ ExprSeq exprs = new ExprSeq();
+ foreach (Variable v in vcgen.program.GlobalVariables()) {
+ Contract.Assert(v != null);
+ exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ }
+ foreach (Variable v in impl.Proc.InParams) {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (Variable v in impl.Proc.OutParams) {
+ Contract.Assert(v != null);
+ exprs.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ foreach (IdentifierExpr ie in impl.Proc.Modifies) {
+ Contract.Assert(ie != null);
+ if (ie.Decl == null)
+ continue;
+ exprs.Add(ie);
+ }
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
+ impl.Proc.Ensures.Add(new Ensures(Token.NoToken, true, freePostExpr, "", new QKeyValue(Token.NoToken, "si_fcall", new List<object>(), null)));
+
+ initialized = false;
+ }
+
+ public void GenerateVC() {
+ if (initialized) return;
+ List<Variable> outputVariables = new List<Variable>();
+ assertExpr = new LiteralExpr(Token.NoToken, true);
+ foreach (Variable v in impl.OutParams) {
+ Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ outputVariables.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertExpr = Expr.And(assertExpr, eqExpr);
+ }
+ foreach (IdentifierExpr e in impl.Proc.Modifies) {
+ if (e.Decl == null) continue;
+ Variable v = e.Decl;
+ Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
+ outputVariables.Add(c);
+ Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
+ assertExpr = Expr.And(assertExpr, eqExpr);
+ }
+ assertExpr = Expr.Not(assertExpr);
+
+ Program program = vcgen.program;
+ ProverInterface proverInterface = vcgen.prover;
+ vcgen.ConvertCFG2DAG(impl);
+ ModelViewInfo mvInfo;
+ vcgen.PassifyImpl(impl, out mvInfo);
+
+ controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
+ impl.LocVars.Add(controlFlowVariable);
+
+ VCExpressionGenerator gen = proverInterface.VCExprGen;
+ var exprGen = proverInterface.Context.ExprGen;
+ var translator = proverInterface.Context.BoogieExprTranslator;
+ VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : translator.LookupVariable(controlFlowVariable);
+
+ vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));
+ if (!CommandLineOptions.Clo.UseLabels) {
+ VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
+ VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+ vcexpr = exprGen.And(eqExpr, vcexpr);
+ }
+
+ privateExprVars = new List<VCExprVar>();
+ foreach (Variable v in impl.LocVars) {
+ privateExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.OutParams) {
+ privateExprVars.Add(translator.LookupVariable(v));
+ }
+
+ interfaceExprVars = new List<VCExprVar>();
+ foreach (Variable v in program.GlobalVariables()) {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in impl.InParams) {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+ foreach (Variable v in outputVariables) {
+ interfaceExprVars.Add(translator.LookupVariable(v));
+ }
+
+ callSites = vcgen.CollectCallSites(impl);
+ initialized = true;
+ }
+ }
+
+ public class CallSitesSimplifier : StandardVisitor {
+ VariableSeq localVars;
+ StratifiedVCGenBase vcgen;
+ public static void SimplifyCallSites(Implementation implementation, StratifiedVCGenBase vcgen) {
+ CallSitesSimplifier visitor = new CallSitesSimplifier(vcgen);
+ visitor.Visit(implementation);
+ implementation.LocVars.AddRange(visitor.localVars);
+ }
+ private CallSitesSimplifier(StratifiedVCGenBase vcgen) {
+ this.vcgen = vcgen;
+ this.localVars = new VariableSeq();
+ }
+ public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ CmdSeq newCmdSeq = new CmdSeq();
+ foreach (Cmd cmd in cmdSeq) {
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ if (assumeCmd == null) {
+ newCmdSeq.Add(cmd);
+ continue;
+ }
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null || !vcgen.implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) {
+ newCmdSeq.Add(cmd);
+ continue;
+ }
+
+ ExprSeq exprs = new ExprSeq();
+ foreach (Expr e in naryExpr.Args) {
+ LocalVariable newVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "CallSiteSimplification@" + localVars.Length, e.Type));
+ localVars.Add(newVar);
+ newCmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(newVar), e)));
+ exprs.Add(Expr.Ident(newVar));
+ }
+ newCmdSeq.Add(new AssumeCmd(Token.NoToken, new NAryExpr(Token.NoToken, naryExpr.Fun, exprs)));
+ }
+ return newCmdSeq;
+ }
+ }
+
+ public class StratifiedVCGenBase : VCGen {
+ public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
+ public ProverInterface prover;
+
+ public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile)
+ : base(program, logFilePath, appendLogFile) {
+ implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();
+ prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);
+ }
+ }
+
+ public override void Close() {
+ prover.Close();
+ base.Close();
+ }
+
+ public Dictionary<Block, List<CallSite>> CollectCallSites(Implementation implementation) {
+ var callSites = new Dictionary<Block, List<CallSite>>();
+ foreach (Block block in implementation.Blocks) {
+ for (int i = 0; i < block.Cmds.Length; i++) {
+ AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;
+ if (assumeCmd == null) continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null) continue;
+ if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;
+ List<VCExpr> interfaceExprs = new List<VCExpr>();
+ foreach (Expr e in naryExpr.Args) {
+ interfaceExprs.Add(prover.Context.BoogieExprTranslator.Translate(e));
}
- private CallSitesSimplifier(StratifiedVCGen vcgen) {
- this.vcgen = vcgen;
- this.localVars = new VariableSeq();
+ CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprs, block, i);
+ if (!callSites.ContainsKey(block))
+ callSites[block] = new List<CallSite>();
+ callSites[block].Add(cs);
+ }
+ }
+ return callSites;
+ }
+
+ private int newVarCountForStratifiedInlining = 0;
+ public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {
+ string newName = "StratifiedInlining@" + newVarCountForStratifiedInlining.ToString();
+ newVarCountForStratifiedInlining++;
+ Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
+ prover.Context.DeclareConstant(newVar, false, null);
+ return prover.VCExprGen.Variable(newVar.Name, type);
+ }
+ private int idCountForStratifiedInlining = 0;
+ public int CreateNewId() {
+ return idCountForStratifiedInlining++;
+ }
+ }
+
+ public class StratifiedVCGen : StratifiedVCGenBase {
+ public bool PersistCallTree;
+ public static Dictionary<string, int> callTree = null;
+ public int numInlined = 0;
+ public readonly static string recordProcName = "boogie_si_record";
+ private bool useSummary;
+ private SummaryComputation summaryComputation;
+ private HashSet<string> procsThatReachedRecBound;
+ public int boundUsedInLastQuery { get; private set; }
+ public HashSet<string> procsToSkip;
+ public Dictionary<string, int> extraRecBound;
+
+ public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)
+ : base(program, logFilePath, appendLogFile) {
+ this.GenerateRecordFunctions();
+ PersistCallTree = false;
+ useSummary = false;
+ procsThatReachedRecBound = new HashSet<string>();
+ procsToSkip = new HashSet<string>();
+ extraRecBound = new Dictionary<string, int>();
+ boundUsedInLastQuery = -1;
+ }
+
+ // Is this procedure to be "skipped"
+ // Currently this is experimental
+ public bool isSkipped(string procName) {
+ return procsToSkip.Contains(procName);
+ }
+ public bool isSkipped(int candidate, FCallHandler calls) {
+ return isSkipped(calls.getProc(candidate));
+ }
+ // Extra rec bound for procedures
+ public int GetExtraRecBound(string procName) {
+ if (!extraRecBound.ContainsKey(procName))
+ return 0;
+ else return extraRecBound[procName];
+ }
+
+ public void GenerateRecordFunctions() {
+ foreach (var decl in program.TopLevelDeclarations) {
+ var proc = decl as Procedure;
+ if (proc == null) continue;
+ if (!proc.Name.StartsWith(recordProcName)) continue;
+ Contract.Assert(proc.InParams.Length == 1);
+
+ // Make a new function
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
+ Contract.Assert(ti != null);
+ Formal returnVar = new Formal(Token.NoToken, ti, false);
+ Contract.Assert(returnVar != null);
+
+ // Get record type
+ var argtype = proc.InParams[0].TypedIdent.Type;
+
+ var ins = new VariableSeq();
+ ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
+
+ var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
+ prover.Context.DeclareFunction(recordFunc, "");
+
+ var exprs = new ExprSeq();
+ exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
+
+ Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
+ proc.Ensures.Add(new Ensures(true, freePostExpr));
+ }
+ }
+
+ public class SummaryComputation {
+ // The verification state
+ VerificationState vState;
+ // The call tree
+ FCallHandler calls;
+ // Fully-inlined guys we have already queried
+ HashSet<string> fullyInlinedCache;
+
+ // The summary: boolean guards that are true
+ HashSet<VCExprVar> trueSummaryConst;
+ HashSet<VCExprVar> trueSummaryConstUndeBound;
+
+ // Compute summaries under recursion bound or not?
+ bool ComputeUnderBound;
+
+ public SummaryComputation(VerificationState vState, bool ComputeUnderBound) {
+ this.vState = vState;
+ this.calls = vState.calls;
+ this.fullyInlinedCache = new HashSet<string>();
+ this.trueSummaryConst = new HashSet<VCExprVar>();
+ this.trueSummaryConstUndeBound = new HashSet<VCExprVar>();
+ this.ComputeUnderBound = false;
+ }
+
+ public void boundChanged() {
+ if (ComputeUnderBound) {
+ var s = "";
+ trueSummaryConstUndeBound.Iter(v => s = s + v.ToString() + ",");
+ Console.WriteLine("Clearing summaries: {0}", s);
+
+ // start from scratch
+ trueSummaryConst.ExceptWith(trueSummaryConstUndeBound);
+ trueSummaryConstUndeBound = new HashSet<VCExprVar>();
+ }
+ }
+
+ public void compute(HashSet<int> goodCandidates, int bound) {
+ var start = DateTime.UtcNow;
+ goodCandidates = calls.currCandidates;
+
+ var found = 0;
+
+ // Find all nodes that have children only in goodCandidates
+ var overApproxNodes = FindNodes(calls.candidateParent, calls.currCandidates, goodCandidates);
+ overApproxNodes.IntersectWith(calls.summaryCandidates.Keys);
+
+ var roots = FindTopMostAncestors(calls.candidateParent, overApproxNodes);
+ var prover2 = vState.checker2.prover;
+ var reporter2 = vState.checker2.reporter;
+
+ prover2.Push();
+
+ // candidates to block
+ var block = new HashSet<int>();
+ var usesBound = new HashSet<int>();
+ if (ComputeUnderBound) {
+ calls.currCandidates.Iter(id => { if (calls.getRecursionBound(id) > bound) block.Add(id); });
+ foreach (var id in block) {
+ prover2.Assert(calls.getFalseExpr(id), true);
+ var curr = id;
+ usesBound.Add(id);
+ while (curr != 0) {
+ curr = calls.candidateParent[curr];
+ usesBound.Add(curr);
+ }
}
- public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
- CmdSeq newCmdSeq = new CmdSeq();
- foreach (Cmd cmd in cmdSeq) {
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null) {
- newCmdSeq.Add(cmd);
- continue;
- }
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null || !vcgen.implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) {
- newCmdSeq.Add(cmd);
- continue;
- }
-
- ExprSeq exprs = new ExprSeq();
- foreach (Expr e in naryExpr.Args) {
- LocalVariable newVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "CallSiteSimplification@" + localVars.Length, e.Type));
- localVars.Add(newVar);
- newCmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(newVar), e)));
- exprs.Add(Expr.Ident(newVar));
+
+ }
+
+ // Iterate over the roots
+ foreach (var id in roots) {
+ // inline procedures in post order
+ var post = getPostOrder(calls.candidateParent, id);
+
+ vState.checker.prover.Push();
+ foreach (var cid in post) {
+ if (goodCandidates.Contains(cid)) continue;
+
+ prover2.Assert(calls.id2VC[cid], true);
+ if (!overApproxNodes.Contains(cid)) continue;
+ prover2.Assert(calls.id2ControlVar[cid], true);
+
+ foreach (var tup in calls.summaryCandidates[cid]) {
+ if (trueSummaryConst.Contains(tup.Item1)) continue;
+
+ //Console.WriteLine("Going to try ({0} ==> {1}) on {2}", tup.Item1, tup.Item2, id);
+ //Console.WriteLine("Call expr: {0}", calls.id2Candidate[id]);
+
+ // It is OK to assume the summary while trying to prove it
+ var summary = getSummary(tup.Item1);
+
+ prover2.Push();
+ prover2.Assert(summary, true);
+ prover2.Assert(prover2.VCExprGen.Not(tup.Item2), true);
+ prover2.Check();
+ var outcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(prover2.CheckOutcomeCore(reporter2));
+
+ prover2.Pop();
+ if (outcome == Outcome.Correct) {
+ //Console.WriteLine("Found summary: {0}", tup.Item1);
+ found++;
+ trueSummaryConst.Add(tup.Item1);
+ if (usesBound.Contains(cid)) trueSummaryConstUndeBound.Add(tup.Item1);
}
- newCmdSeq.Add(new AssumeCmd(Token.NoToken, new NAryExpr(Token.NoToken, naryExpr.Fun, exprs)));
}
- return newCmdSeq;
}
+ prover2.Pop();
+ }
+ prover2.Pop();
+
+ var end = DateTime.UtcNow;
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
+ Console.WriteLine(">> Summary computation took {0} sec and inferred {1} of {2} contracts",
+ (end - start).TotalSeconds, found, calls.allSummaryConst.Count);
}
- internal class CallSitesCollector : StandardVisitor {
- List<CallSite> callSites;
- StratifiedVCGen vcgen;
- StratifiedInliningInfo info;
- Block currBlock;
- public static List<CallSite> CollectCallSites(Implementation implementation, StratifiedVCGen vcgen) {
- var visitor = new CallSitesCollector(implementation, vcgen);
- visitor.Visit(implementation);
- return visitor.callSites;
+ }
+
+
+ public VCExpr getSummary() {
+ return getSummary(new HashSet<VCExprVar>());
+ }
+
+ public VCExpr getSummary(params VCExprVar[] p) {
+ var s = new HashSet<VCExprVar>();
+ p.Iter(v => s.Add(v));
+ return getSummary(s);
+ }
+
+ public VCExpr getSummary(HashSet<VCExprVar> extraToSet) {
+ if (calls.allSummaryConst.Count == 0) return null;
+ // TODO: does it matter which checker we use here?
+ var Gen = vState.checker.prover.VCExprGen;
+
+ var ret = VCExpressionGenerator.True;
+ foreach (var c in calls.allSummaryConst) {
+ if (trueSummaryConst.Contains(c) || extraToSet.Contains(c)) {
+ ret = Gen.And(ret, c);
+ }
+ else {
+ ret = Gen.And(ret, Gen.Not(c));
}
- private CallSitesCollector(Implementation implementation, StratifiedVCGen vcgen) {
- this.vcgen = vcgen;
- this.info = vcgen.implName2StratifiedInliningInfo[implementation.Name];
- callSites = new List<CallSite>();
+ }
+ return ret;
+ }
+
+ // Return a subset of nodes such that all other nodes are their decendent
+ private HashSet<int> FindTopMostAncestors(Dictionary<int, int> parents, HashSet<int> nodes) {
+ var ret = new HashSet<int>();
+ //var ancestorFound = new HashSet<int>();
+ foreach (var n in nodes) {
+ var ancestor = n;
+ var curr = n;
+ while (curr != 0) {
+ curr = parents[curr];
+ if (nodes.Contains(curr)) ancestor = curr;
}
- public override Block VisitBlock(Block node) {
- this.currBlock = node;
- return base.VisitBlock(node);
+ ret.Add(ancestor);
+ }
+ return ret;
+ }
+
+ // Returns the set of candidates whose child leaves are all "good". Remove fully inlined ones.
+ HashSet<int> FindNodes(Dictionary<int, int> parents, HashSet<int> allLeaves,
+ HashSet<int> goodLeaves) {
+ var ret = new HashSet<int>();
+ var leaves = new Dictionary<int, HashSet<int>>();
+ leaves.Add(0, new HashSet<int>());
+ parents.Keys.Iter(n => leaves.Add(n, new HashSet<int>()));
+ allLeaves.Iter(l => leaves[l].Add(l));
+
+ foreach (var l in allLeaves) {
+ var curr = l;
+ leaves[curr].Add(l);
+ while (parents.ContainsKey(curr)) {
+ curr = parents[curr];
+ leaves[curr].Add(l);
}
- public override Cmd VisitAssumeCmd(AssumeCmd node) {
- NAryExpr naryExpr = node.Expr as NAryExpr;
- if (naryExpr == null)
- return node;
- if (!vcgen.implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName))
- return node;
- List<VCExpr> interfaceExprVars = new List<VCExpr>();
- foreach (Expr e in naryExpr.Args) {
- IdentifierExpr ie = e as IdentifierExpr;
- interfaceExprVars.Add(vcgen.prover.Context.BoogieExprTranslator.LookupVariable(ie.Decl));
+ }
+
+ foreach (var kvp in leaves) {
+ if (kvp.Value.Count == 0) {
+ var proc = calls.getProc(kvp.Key);
+ if (fullyInlinedCache.Contains(proc)) continue;
+ else {
+ ret.Add(kvp.Key);
+ fullyInlinedCache.Add(proc);
}
- CallSite cs = new CallSite(naryExpr.Fun.FunctionName, interfaceExprVars, currBlock);
- callSites.Add(cs);
- return node;
+ }
+
+ if (kvp.Value.IsSubsetOf(goodLeaves)) {
+ ret.Add(kvp.Key);
+ }
+ }
+
+ return ret;
+ }
+
+
+ // returns children of root in post order
+ static List<int> getPostOrder(Dictionary<int, int> parents, int root) {
+ var children = new Dictionary<int, HashSet<int>>();
+ foreach (var id in parents.Keys) children.Add(id, new HashSet<int>());
+ children.Add(0, new HashSet<int>());
+ foreach (var kvp in parents) children[kvp.Value].Add(kvp.Key);
+ return getPostOrder(children, root);
+ }
+ static List<int> getPostOrder(Dictionary<int, HashSet<int>> children, int root) {
+ var ret = new List<int>();
+ foreach (var ch in children[root]) ret.AddRange(getPostOrder(children, ch));
+ ret.Add(root);
+ return ret;
+ }
+ }
+
+ public class CoverageGraphManager {
+ public static int timeStamp = 0;
+
+ public class Task {
+ public enum TaskType { NONE, STEP, INLINE, BLOCK, REACHABLE };
+
+ public TaskType type;
+ private string query_string;
+ public List<int> nodes;
+ public int queryNode {
+ get {
+ Debug.Assert(nodes.Count == 1);
+ return nodes[0];
}
}
-
- public class StratifiedVC {
- private static int newVarCount = 0;
- private static VCExprVar CreateNewVar(ProverInterface prover, Microsoft.Boogie.Type type) {
- string newName = "StratifiedInlining@" + newVarCnt.ToString();
- newVarCount++;
- Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));
- prover.Context.DeclareConstant(newVar, false, null);
- return prover.VCExprGen.Variable(newVar.Name, type);
+
+ public Task(string q, FCallHandler calls) {
+ query_string = q;
+ nodes = new List<int>();
+ if (q.StartsWith("step")) {
+ type = TaskType.STEP;
+ return;
}
- private static int idCount = 0;
-
- int id;
- Implementation impl;
- List<VCExprVar> interfaceExprVars;
- List<StratifiedCallSite> callSites;
- VCExpr vcexpr;
- public Dictionary<Block, VCExprVar> reachVars;
-
- public StratifiedVC(StratifiedInliningInfo info, StratifiedVCGen vcgen) {
- if (!info.initialized) {
- info.GenerateVC(vcgen);
+ var split = q.Split(' ');
+ switch (split[0].ToLower()) {
+ case "inline":
+ type = TaskType.INLINE;
+ break;
+ case "block":
+ type = TaskType.BLOCK;
+ break;
+ case "reachable":
+ type = TaskType.REACHABLE;
+ break;
+ default:
+ Debug.Assert(false);
+ break;
+ }
+ for (int i = 1; i < split.Length; i++) {
+ var node = calls.getCandidateFromGraphNode(split[i]);
+ if (node != -1) {
+ nodes.Add(node);
}
- impl = info.impl;
- interfaceExprVars = new List<VCExprVar>();
- VCExpr expansion = info.vcexpr;
- var prover = vcgen.prover;
- VCExpressionGenerator gen = prover.VCExprGen;
- var bet = prover.Context.BoogieExprTranslator;
- VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);
- id = idCount++;
- VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));
- expansion = gen.And(eqExpr, expansion);
-
- Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (VCExprVar v in info.interfaceExprVars) {
- VCExprVar newVar = CreateNewVar(prover, v.Type);
- interfaceExprVars.Add(newVar);
- substDict.Add(v, newVar);
- }
- foreach (VCExprVar v in info.privateExprVars) {
- substDict.Add(v, CreateNewVar(prover, v.Type));
- }
- VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
- SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);
- expansion = substVisitor.Mutate(expansion, subst);
-
- reachVars = new Dictionary<Block, VCExprVar>();
- Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();
- foreach (Block b in impl.Blocks) {
- reachVars[b] = CreateNewVar(prover, Bpl.Type.Bool);
- reachExprs[b] = VCExpressionGenerator.False;
- }
- foreach (Block b in impl.Blocks) {
- foreach (Block pb in b.Predecessors) {
- VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(pb.UniqueId)));
- VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(b.UniqueId)));
- reachExprs[b] = gen.Or(reachExprs[b], gen.And(reachVars[pb], controlTransferExpr));
+ }
+ // Prune nodes according to which are current candidates
+ var pruned = new List<int>();
+ foreach (var n in nodes) {
+ if (calls.currCandidates.Contains(n)) {
+ if (type == TaskType.INLINE || type == TaskType.BLOCK) {
+ pruned.Add(n);
}
}
- // The binding for entry block should be left defined;
- // it will get filled in when the call tree is constructed
- vcexpr = expansion;
- for (int i = 1; i < impl.Blocks.Count; i++) {
- Block b = impl.Blocks[i];
- vcexpr = gen.And(vcexpr, gen.Eq(reachVars[b], reachExprs[b]));
- }
-
- callSites = new List<StratifiedCallSite>();
- foreach (CallSite cs in info.callSites) {
- callSites.Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));
+ else {
+ if (type == TaskType.REACHABLE) {
+ pruned.Add(n);
+ }
}
+ }
+ nodes = pruned;
+ if (type == TaskType.REACHABLE && nodes.Count != 1) {
+ type = TaskType.NONE;
+ }
+ else if (nodes.Count == 0) {
+ type = TaskType.NONE;
}
}
- public class CallSite {
- public string callee;
- public List<VCExpr> interfaceExprVars;
- public Block block;
- public CallSite(string callee, List<VCExpr> interfaceExprVars, Block block) {
- this.callee = callee;
- this.interfaceExprVars = interfaceExprVars;
- this.block = block;
- }
+ public bool isStep() {
+ return (type == TaskType.STEP);
}
- public class StratifiedCallSite {
- CallSite callSite;
- List<VCExpr> interfaceExprVars;
- VCExprVar reachVar;
+ public override string ToString() {
+ return query_string;
+ }
+ }
- public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {
- callSite = cs;
- interfaceExprVars = new List<VCExpr>();
- foreach (VCExpr v in cs.interfaceExprVars) {
- interfaceExprVars.Add(substVisitor.Mutate(v, subst));
+ public string getQuery(int ts) {
+ var ret = "";
+ while (true) {
+ string str = coverageProcess.StandardOutput.ReadLine();
+ if (str.StartsWith("query ")) {
+ var split = str.Split(' ');
+ if (split.Length < 1) continue;
+ if (ts.ToString() == split[1]) {
+ for (int i = 2; i < split.Length; i++) ret = ret + split[i] + " ";
+ break;
}
- reachVar = reachVars[cs.block];
}
}
+ return ret;
+ }
- public class StratifiedInliningInfo {
- public Implementation impl;
- public Function function;
- public Variable controlFlowVariable;
- public Expr assertExpr;
- public VCExpr vcexpr;
- public List<VCExprVar> interfaceExprVars;
- public List<VCExprVar> privateExprVars;
- public Hashtable/*<int, Absy!>*/ label2absy;
- public ModelViewInfo mvInfo;
- public List<CallSite> callSites;
- public bool initialized;
-
- public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen vcgen) {
- impl = implementation;
-
- VariableSeq functionInterfaceVars = new VariableSeq();
- foreach (Variable v in vcgen.program.GlobalVariables()) {
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
- }
- foreach (Variable v in impl.InParams) {
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
- }
- foreach (Variable v in impl.OutParams) {
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));
- }
- foreach (IdentifierExpr e in impl.Proc.Modifies) {
- if (e.Decl == null) continue;
- functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", e.Decl.TypedIdent.Type), true));
- }
- Formal returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Bpl.Type.Bool), false);
- function = new Function(Token.NoToken, impl.Name, functionInterfaceVars, returnVar);
- vcgen.prover.Context.DeclareFunction(function, "");
-
- ExprSeq exprs = new ExprSeq();
- foreach (Variable v in vcgen.program.GlobalVariables()) {
- Contract.Assert(v != null);
- exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
- }
- foreach (Variable v in impl.Proc.InParams) {
- Contract.Assert(v != null);
- exprs.Add(new IdentifierExpr(Token.NoToken, v));
- }
- foreach (Variable v in impl.Proc.OutParams) {
- Contract.Assert(v != null);
- exprs.Add(new IdentifierExpr(Token.NoToken, v));
- }
- foreach (IdentifierExpr ie in impl.Proc.Modifies) {
- Contract.Assert(ie != null);
- if (ie.Decl == null)
- continue;
- exprs.Add(ie);
- }
- Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
- impl.Proc.Ensures.Add(new Ensures(Token.NoToken, true, freePostExpr, "", new QKeyValue(Token.NoToken, "si_fcall", new List<object>(), null)));
-
- initialized = false;
+ public static Process coverageProcess;
+ public bool stopCoverageProcess;
+ //private System.Threading.Thread readerThread;
+ private FCallHandler calls;
+ // Set of edges to send off to the coverageProcess
+ private List<KeyValuePair<int, int>> edges;
+ // Set of nodes to send off to the coverageProcess
+ private HashSet<int> newNodes;
+ // Set of nodes already declared
+ private HashSet<int> declaredNodes;
+
+ public CoverageGraphManager(FCallHandler calls) {
+ stopCoverageProcess = true;
+ coverageProcess = null;
+ this.calls = calls;
+ this.edges = new List<KeyValuePair<int, int>>();
+ declaredNodes = new HashSet<int>();
+ newNodes = new HashSet<int>();
+
+ coverageProcess = CommandLineOptions.Clo.coverageReporter;
+ if (coverageProcess != null) {
+ stopCoverageProcess = false;
+ if (!coverageProcess.StartInfo.RedirectStandardInput) {
+ coverageProcess = null;
}
+ }
+ else {
+ if (CommandLineOptions.Clo.CoverageReporterPath != null) {
+ coverageProcess = new Process();
+ var coverageProcessInfo = new ProcessStartInfo();
+ coverageProcessInfo.CreateNoWindow = true;
+ coverageProcessInfo.FileName = CommandLineOptions.Clo.CoverageReporterPath + @"\CoverageGraph.exe";
+ coverageProcessInfo.RedirectStandardInput = true;
+ coverageProcessInfo.RedirectStandardOutput = true;
+ coverageProcessInfo.RedirectStandardError = false;
+ coverageProcessInfo.UseShellExecute = false;
+ coverageProcessInfo.Arguments = "interactive";
+
+ coverageProcess.StartInfo = coverageProcessInfo;
+ try {
+ coverageProcess.Start();
+ }
+ catch (System.ComponentModel.Win32Exception) {
+ coverageProcess.Dispose();
+ coverageProcess = null;
+ }
+ //readerThread = new System.Threading.Thread(new System.Threading.ThreadStart(CoverageGraphInterface));
+ //readerThread.Start();
+ }
+ }
- public void GenerateVC(StratifiedVCGen vcgen) {
- List<Variable> outputVariables = new List<Variable>();
- assertExpr = new LiteralExpr(Token.NoToken, true);
- foreach (Variable v in impl.OutParams) {
- Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
- outputVariables.Add(c);
- Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
- assertExpr = Expr.And(assertExpr, eqExpr);
- }
- foreach (IdentifierExpr e in impl.Proc.Modifies) {
- if (e.Decl == null) continue;
- Variable v = e.Decl;
- Constant c = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, impl.Name + "_" + v.Name, v.TypedIdent.Type));
- outputVariables.Add(c);
- Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));
- assertExpr = Expr.And(assertExpr, eqExpr);
- }
- assertExpr = Expr.Not(assertExpr);
-
- Program program = vcgen.program;
- ProverInterface proverInterface = vcgen.prover;
- vcgen.ConvertCFG2DAG(impl);
- ModelViewInfo mvInfo;
- vcgen.PassifyImpl(impl, out mvInfo);
-
- controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
- impl.LocVars.Add(controlFlowVariable);
-
- VCExpressionGenerator gen = proverInterface.VCExprGen;
- var exprGen = proverInterface.Context.ExprGen;
- var translator = proverInterface.Context.BoogieExprTranslator;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : translator.LookupVariable(controlFlowVariable);
-
- CallSitesSimplifier.SimplifyCallSites(impl, vcgen);
- vcexpr = gen.Not(vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context));
- if (!CommandLineOptions.Clo.UseLabels) {
- VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, exprGen.Integer(BigNum.ZERO));
- VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vcexpr = exprGen.And(eqExpr, vcexpr);
- }
+ if (coverageProcess != null) {
+ coverageProcess.StandardInput.WriteLine("clear-all");
+ }
+ }
- privateExprVars = new List<VCExprVar>();
- foreach (Variable v in impl.LocVars) {
- privateExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in impl.OutParams) {
- privateExprVars.Add(translator.LookupVariable(v));
- }
+ public void addMain() {
+ newNodes.Add(0);
+ foreach (var n in calls.currCandidates) {
+ addEdge(0, n);
+ }
+ calls.recentlyAddedCandidates = new HashSet<int>();
+ }
- interfaceExprVars = new List<VCExprVar>();
- foreach (Variable v in program.GlobalVariables()) {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in impl.InParams) {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
- foreach (Variable v in outputVariables) {
- interfaceExprVars.Add(translator.LookupVariable(v));
- }
+ public void addNode(int src) {
+ newNodes.Add(src);
+ }
- callSites = CallSitesCollector.CollectCallSites(impl, vcgen);
+ public void addEdge(int src_id, int tgt_id) {
+ newNodes.Add(src_id);
+ newNodes.Add(tgt_id);
+ edges.Add(new KeyValuePair<int, int>(src_id, tgt_id));
+ }
- initialized = true;
- }
+ public void addRecentEdges(int src_id) {
+ newNodes.Add(src_id);
+ foreach (var tgt in calls.recentlyAddedCandidates) {
+ addEdge(src_id, tgt);
}
+ calls.recentlyAddedCandidates = new HashSet<int>();
+ }
- public void GenerateRecordFunctions() {
- foreach (var decl in program.TopLevelDeclarations) {
- var proc = decl as Procedure;
- if (proc == null) continue;
- if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Length == 1);
+ private void declareNodes() {
+ var send = false;
+ var declarenode = "declare-node";
+ foreach (var n in newNodes) {
+ if (declaredNodes.Contains(n)) continue;
+ declaredNodes.Add(n);
+ send = true;
+ declarenode += string.Format(" {0} {1}", calls.getPersistentId(n), calls.getProc(n));
+ }
+ if (send)
+ coverageProcess.StandardInput.WriteLine(declarenode);
+ }
- // Make a new function
- TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
- Contract.Assert(ti != null);
- Formal returnVar = new Formal(Token.NoToken, ti, false);
- Contract.Assert(returnVar != null);
+ private void declareEdges() {
+ if (edges.Count == 0) return;
- // Get record type
- var argtype = proc.InParams[0].TypedIdent.Type;
+ var declareedge = "declare-edge";
+ foreach (var e in edges) {
+ declareedge += string.Format(" {0} {1}", calls.getPersistentId(e.Key), calls.getPersistentId(e.Value));
+ }
+ coverageProcess.StandardInput.WriteLine(declareedge);
+ }
- var ins = new VariableSeq();
- ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));
+ public void syncGraph() {
+ if (coverageProcess == null || newNodes.Count == 0) {
+ edges.Clear();
+ return;
+ }
- var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);
- prover.Context.DeclareFunction(recordFunc, "");
+ coverageProcess.StandardInput.WriteLine("batch-graph-command-begin");
+ coverageProcess.StandardInput.WriteLine("reset-color");
- var exprs = new ExprSeq();
- exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));
+ // Go through the edges
+ var greenNodes = new HashSet<int>();
+ var redNodes = new HashSet<int>();
+ foreach (var node in calls.currCandidates) {
+ if (calls.getRecursionBound(node) > CommandLineOptions.Clo.RecursionBound) {
+ redNodes.Add(node);
+ }
+ else {
+ greenNodes.Add(node);
+ }
- Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);
- proc.Ensures.Add(new Ensures(true, freePostExpr));
+ }
+ // Send data across
+ declareNodes();
+ declareEdges();
+
+ if (greenNodes.Count != 0) {
+ var color = "color green";
+ foreach (var n in greenNodes) {
+ color += string.Format(" {0}", calls.getPersistentId(n));
}
+ coverageProcess.StandardInput.WriteLine(color);
}
- public class SummaryComputation
- {
- // The verification state
- VerificationState vState;
- // The call tree
- FCallHandler calls;
- // Fully-inlined guys we have already queried
- HashSet<string> fullyInlinedCache;
-
- // The summary: boolean guards that are true
- HashSet<VCExprVar> trueSummaryConst;
- HashSet<VCExprVar> trueSummaryConstUndeBound;
-
- // Compute summaries under recursion bound or not?
- bool ComputeUnderBound;
-
- public SummaryComputation(VerificationState vState, bool ComputeUnderBound)
- {
- this.vState = vState;
- this.calls = vState.calls;
- this.fullyInlinedCache = new HashSet<string>();
- this.trueSummaryConst = new HashSet<VCExprVar>();
- this.trueSummaryConstUndeBound = new HashSet<VCExprVar>();
- this.ComputeUnderBound = false;
- }
+ if (redNodes.Count != 0) {
+ var color = "color red";
+ foreach (var n in redNodes) {
+ color += string.Format(" {0}", calls.getPersistentId(n));
+ }
+ coverageProcess.StandardInput.WriteLine(color);
+ }
- public void boundChanged()
- {
- if (ComputeUnderBound)
- {
- var s = "";
- trueSummaryConstUndeBound.Iter(v => s = s + v.ToString() + ",");
- Console.WriteLine("Clearing summaries: {0}", s);
-
- // start from scratch
- trueSummaryConst.ExceptWith(trueSummaryConstUndeBound);
- trueSummaryConstUndeBound = new HashSet<VCExprVar>();
- }
- }
+ coverageProcess.StandardInput.WriteLine("batch-graph-command-end");
- public void compute(HashSet<int> goodCandidates, int bound)
- {
- var start = DateTime.UtcNow;
- goodCandidates = calls.currCandidates;
-
- var found = 0;
-
- // Find all nodes that have children only in goodCandidates
- var overApproxNodes = FindNodes(calls.candidateParent, calls.currCandidates, goodCandidates);
- overApproxNodes.IntersectWith(calls.summaryCandidates.Keys);
-
- var roots = FindTopMostAncestors(calls.candidateParent, overApproxNodes);
- var prover2 = vState.checker2.prover;
- var reporter2 = vState.checker2.reporter;
-
- prover2.Push();
-
- // candidates to block
- var block = new HashSet<int>();
- var usesBound = new HashSet<int>();
- if (ComputeUnderBound)
- {
- calls.currCandidates.Iter(id => { if (calls.getRecursionBound(id) > bound) block.Add(id); });
- foreach (var id in block)
- {
- prover2.Assert(calls.getFalseExpr(id), true);
- var curr = id;
- usesBound.Add(id);
- while (curr != 0)
- {
- curr = calls.candidateParent[curr];
- usesBound.Add(curr);
- }
- }
+ edges.Clear();
+ newNodes = new HashSet<int>();
+ }
- }
-
- // Iterate over the roots
- foreach (var id in roots)
- {
- // inline procedures in post order
- var post = getPostOrder(calls.candidateParent, id);
-
- vState.checker.prover.Push();
- foreach (var cid in post)
- {
- if (goodCandidates.Contains(cid)) continue;
-
- prover2.Assert(calls.id2VC[cid], true);
- if (!overApproxNodes.Contains(cid)) continue;
- prover2.Assert(calls.id2ControlVar[cid], true);
-
- foreach (var tup in calls.summaryCandidates[cid])
- {
- if (trueSummaryConst.Contains(tup.Item1)) continue;
-
- //Console.WriteLine("Going to try ({0} ==> {1}) on {2}", tup.Item1, tup.Item2, id);
- //Console.WriteLine("Call expr: {0}", calls.id2Candidate[id]);
-
- // It is OK to assume the summary while trying to prove it
- var summary = getSummary(tup.Item1);
-
- prover2.Push();
- prover2.Assert(summary, true);
- prover2.Assert(prover2.VCExprGen.Not(tup.Item2), true);
- prover2.Check();
- var outcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(prover2.CheckOutcomeCore(reporter2));
-
- prover2.Pop();
- if (outcome == Outcome.Correct)
- {
- //Console.WriteLine("Found summary: {0}", tup.Item1);
- found++;
- trueSummaryConst.Add(tup.Item1);
- if (usesBound.Contains(cid)) trueSummaryConstUndeBound.Add(tup.Item1);
- }
- }
- }
- prover2.Pop();
- }
- prover2.Pop();
+ public void reportBug() {
+ if (coverageProcess == null) return;
+ coverageProcess.StandardInput.WriteLine("set-status bug");
+ }
- var end = DateTime.UtcNow;
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
- {
- Console.WriteLine(">> Summary computation took {0} sec and inferred {1} of {2} contracts",
- (end - start).TotalSeconds, found, calls.allSummaryConst.Count);
- }
+ public void reportCorrect() {
+ if (coverageProcess == null) return;
+ coverageProcess.StandardInput.WriteLine("set-status correct");
+ }
- }
+ public void reportCorrect(int bound) {
+ if (coverageProcess == null) return;
+ coverageProcess.StandardInput.WriteLine("set-status bound {0}", bound);
+ }
+ public void reportError() {
+ if (coverageProcess == null) return;
+ coverageProcess.StandardInput.WriteLine("set-status error");
+ }
- public VCExpr getSummary()
- {
- return getSummary(new HashSet<VCExprVar>());
- }
+ public Task getNextTask() {
+ if (coverageProcess == null) return new Task("step", calls);
+ if (coverageProcess.HasExited) {
+ coverageProcess = null;
+ return new Task("step", calls);
+ }
- public VCExpr getSummary(params VCExprVar[] p)
- {
- var s = new HashSet<VCExprVar>();
- p.Iter(v => s.Add(v));
- return getSummary(s);
- }
+ var ts = getNextTimeStamp();
+ coverageProcess.StandardInput.WriteLine("get-input " + ts.ToString());
+ string q = getQuery(ts);
+ return new Task(q, calls);
+ }
- public VCExpr getSummary(HashSet<VCExprVar> extraToSet)
- {
- if (calls.allSummaryConst.Count == 0) return null;
- // TODO: does it matter which checker we use here?
- var Gen = vState.checker.prover.VCExprGen;
-
- var ret = VCExpressionGenerator.True;
- foreach (var c in calls.allSummaryConst)
- {
- if (trueSummaryConst.Contains(c) || extraToSet.Contains(c))
- {
- ret = Gen.And(ret, c);
- }
- else
- {
- ret = Gen.And(ret, Gen.Not(c));
- }
- }
- return ret;
- }
+ public void stop() {
+ if (coverageProcess != null) {
+ if (stopCoverageProcess) {
+ coverageProcess.StandardInput.WriteLine("done");
+ do {
+ coverageProcess.WaitForExit(100);
+ coverageProcess.StandardInput.WriteLine();
+ } while (!coverageProcess.HasExited);
+ }
+ }
+ }
- // Return a subset of nodes such that all other nodes are their decendent
- private HashSet<int> FindTopMostAncestors(Dictionary<int, int> parents, HashSet<int> nodes)
- {
- var ret = new HashSet<int>();
- //var ancestorFound = new HashSet<int>();
- foreach (var n in nodes)
- {
- var ancestor = n;
- var curr = n;
- while (curr != 0)
- {
- curr = parents[curr];
- if (nodes.Contains(curr)) ancestor = curr;
- }
- ret.Add(ancestor);
- }
- return ret;
- }
+ public int getNextTimeStamp() {
+ timeStamp++;
+ return timeStamp - 1;
+ }
+ }
- // Returns the set of candidates whose child leaves are all "good". Remove fully inlined ones.
- HashSet<int> FindNodes(Dictionary<int, int> parents, HashSet<int> allLeaves,
- HashSet<int> goodLeaves)
- {
- var ret = new HashSet<int>();
- var leaves = new Dictionary<int, HashSet<int>>();
- leaves.Add(0, new HashSet<int>());
- parents.Keys.Iter(n => leaves.Add(n, new HashSet<int>()));
- allLeaves.Iter(l => leaves[l].Add(l));
-
- foreach (var l in allLeaves)
- {
- var curr = l;
- leaves[curr].Add(l);
- while (parents.ContainsKey(curr))
- {
- curr = parents[curr];
- leaves[curr].Add(l);
- }
- }
+ public class ApiChecker {
+ public ProverInterface prover;
+ public ProverInterface.ErrorHandler reporter;
- foreach (var kvp in leaves)
- {
- if (kvp.Value.Count == 0)
- {
- var proc = calls.getProc(kvp.Key);
- if (fullyInlinedCache.Contains(proc)) continue;
- else
- {
- ret.Add(kvp.Key);
- fullyInlinedCache.Add(proc);
- }
- }
-
- if (kvp.Value.IsSubsetOf(goodLeaves))
- {
- ret.Add(kvp.Key);
- }
- }
+ public ApiChecker(ProverInterface prover, ProverInterface.ErrorHandler reporter) {
+ this.reporter = reporter;
+ this.prover = prover;
+ }
- return ret;
- }
+ private Outcome CheckVC() {
+ prover.Check();
+ ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);
+ return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
+ public Outcome CheckAssumptions(List<VCExpr> assumptions) {
+ if (assumptions.Count == 0) {
+ return CheckVC();
+ }
- // returns children of root in post order
- static List<int> getPostOrder(Dictionary<int, int> parents, int root)
- {
- var children = new Dictionary<int, HashSet<int>>();
- foreach (var id in parents.Keys) children.Add(id, new HashSet<int>());
- children.Add(0, new HashSet<int>());
- foreach (var kvp in parents) children[kvp.Value].Add(kvp.Key);
- return getPostOrder(children, root);
- }
- static List<int> getPostOrder(Dictionary<int, HashSet<int>> children, int root)
- {
- var ret = new List<int>();
- foreach (var ch in children[root]) ret.AddRange(getPostOrder(children, ch));
- ret.Add(root);
- return ret;
- }
+ prover.Push();
+ foreach (var a in assumptions) {
+ prover.Assert(a, true);
}
+ Outcome ret = CheckVC();
+ prover.Pop();
+ return ret;
+ }
- public class CoverageGraphManager
- {
- public static int timeStamp = 0;
-
- public class Task
- {
- public enum TaskType { NONE, STEP, INLINE, BLOCK, REACHABLE };
-
- public TaskType type;
- private string query_string;
- public List<int> nodes;
- public int queryNode
- {
- get
- {
- Debug.Assert(nodes.Count == 1);
- return nodes[0];
- }
- }
+ public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {
+ List<int> unsatisfiedSoftAssumptions;
+ ProverInterface.Outcome outcome = prover.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);
+ return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
- public Task(string q, FCallHandler calls)
- {
- query_string = q;
- nodes = new List<int>();
- if (q.StartsWith("step"))
- {
- type = TaskType.STEP;
- return;
- }
- var split = q.Split(' ');
- switch (split[0].ToLower())
- {
- case "inline":
- type = TaskType.INLINE;
- break;
- case "block":
- type = TaskType.BLOCK;
- break;
- case "reachable":
- type = TaskType.REACHABLE;
- break;
- default:
- Debug.Assert(false);
- break;
- }
- for (int i = 1; i < split.Length; i++)
- {
- var node = calls.getCandidateFromGraphNode(split[i]);
- if (node != -1)
- {
- nodes.Add(node);
- }
-
- }
- // Prune nodes according to which are current candidates
- var pruned = new List<int>();
- foreach (var n in nodes)
- {
- if (calls.currCandidates.Contains(n))
- {
- if (type == TaskType.INLINE || type == TaskType.BLOCK)
- {
- pruned.Add(n);
- }
- }
- else
- {
- if (type == TaskType.REACHABLE)
- {
- pruned.Add(n);
- }
- }
- }
-
- nodes = pruned;
- if (type == TaskType.REACHABLE && nodes.Count != 1)
- {
- type = TaskType.NONE;
- }
- else if (nodes.Count == 0)
- {
- type = TaskType.NONE;
- }
- }
+ public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore) {
+ ProverInterface.Outcome outcome = prover.CheckAssumptions(assumptions, out unsatCore, reporter);
+ return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+ }
+ }
+
+ // Store important information related to a single VerifyImplementation query
+ public class VerificationState {
+ // The call tree
+ public FCallHandler calls;
+ public ApiChecker checker;
+ // The coverage graph reporter
+ public CoverageGraphManager coverageManager;
+ // For statistics
+ public int vcSize;
+ public int expansionCount;
+
+ // For making summary queries on the side
+ public ApiChecker checker2;
+
+ public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {
+ prover.Assert(vcMain, true);
+ this.calls = calls;
+ this.checker = new ApiChecker(prover, reporter);
+ vcSize = 0;
+ expansionCount = 0;
+ }
+ public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter,
+ ProverInterface prover2, ProverInterface.ErrorHandler reporter2)
+ : this(vcMain, calls, prover, reporter) {
+ this.checker2 = new ApiChecker(prover2, reporter2);
+ }
+ }
- public bool isStep()
- {
- return (type == TaskType.STEP);
- }
+ public Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars) {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- public override string ToString()
- {
- return query_string;
- }
- }
+ // Record current time
+ var startTime = DateTime.UtcNow;
- public string getQuery(int ts)
- {
- var ret = "";
- while (true)
- {
- string str = coverageProcess.StandardOutput.ReadLine();
- if (str.StartsWith("query "))
- {
- var split = str.Split(' ');
- if (split.Length < 1) continue;
- if (ts.ToString() == split[1])
- {
- for (int i = 2; i < split.Length; i++) ret = ret + split[i] + " ";
- break;
- }
- }
- }
- return ret;
- }
+ // No Max: avoids theorem prover restarts
+ CommandLineOptions.Clo.MaxProverMemory = 0;
- public static Process coverageProcess;
- public bool stopCoverageProcess;
- //private System.Threading.Thread readerThread;
- private FCallHandler calls;
- // Set of edges to send off to the coverageProcess
- private List<KeyValuePair<int, int>> edges;
- // Set of nodes to send off to the coverageProcess
- private HashSet<int> newNodes;
- // Set of nodes already declared
- private HashSet<int> declaredNodes;
-
- public CoverageGraphManager(FCallHandler calls)
- {
- stopCoverageProcess = true;
- coverageProcess = null;
- this.calls = calls;
- this.edges = new List<KeyValuePair<int, int>>();
- declaredNodes = new HashSet<int>();
- newNodes = new HashSet<int>();
-
- coverageProcess = CommandLineOptions.Clo.coverageReporter;
- if (coverageProcess != null)
- {
- stopCoverageProcess = false;
- if (!coverageProcess.StartInfo.RedirectStandardInput)
- {
- coverageProcess = null;
- }
- }
- else
- {
- if (CommandLineOptions.Clo.CoverageReporterPath != null)
- {
- coverageProcess = new Process();
- var coverageProcessInfo = new ProcessStartInfo();
- coverageProcessInfo.CreateNoWindow = true;
- coverageProcessInfo.FileName = CommandLineOptions.Clo.CoverageReporterPath + @"\CoverageGraph.exe";
- coverageProcessInfo.RedirectStandardInput = true;
- coverageProcessInfo.RedirectStandardOutput = true;
- coverageProcessInfo.RedirectStandardError = false;
- coverageProcessInfo.UseShellExecute = false;
- coverageProcessInfo.Arguments = "interactive";
-
- coverageProcess.StartInfo = coverageProcessInfo;
- try
- {
- coverageProcess.Start();
- }
- catch (System.ComponentModel.Win32Exception)
- {
- coverageProcess.Dispose();
- coverageProcess = null;
- }
- //readerThread = new System.Threading.Thread(new System.Threading.ThreadStart(CoverageGraphInterface));
- //readerThread.Start();
- }
- }
+ // Initialize cache
+ satQueryCache = new Dictionary<int, List<HashSet<string>>>();
+ unsatQueryCache = new Dictionary<int, List<HashSet<string>>>();
- if (coverageProcess != null)
- {
- coverageProcess.StandardInput.WriteLine("clear-all");
- }
- }
+ Contract.Assert(implName2StratifiedInliningInfo != null);
- public void addMain()
- {
- newNodes.Add(0);
- foreach (var n in calls.currCandidates)
- {
- addEdge(0, n);
- }
- calls.recentlyAddedCandidates = new HashSet<int>();
- }
+ // Build VCs for all procedures
+ implName2StratifiedInliningInfo.Values
+ .Iter(info => info.GenerateVC());
- public void addNode(int src)
- {
- newNodes.Add(src);
- }
+ // Get the VC of the current procedure
+ VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr;
+ Hashtable/*<int, Absy!>*/ mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy;
- public void addEdge(int src_id, int tgt_id)
- {
- newNodes.Add(src_id);
- newNodes.Add(tgt_id);
- edges.Add(new KeyValuePair<int, int>(src_id, tgt_id));
- }
+ // Find all procedure calls in vc and put labels on them
+ FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
+ calls.setCurrProcAsMain();
+ vcMain = calls.Mutate(vcMain, true);
- public void addRecentEdges(int src_id)
- {
- newNodes.Add(src_id);
- foreach (var tgt in calls.recentlyAddedCandidates)
- {
- addEdge(src_id, tgt);
- }
- calls.recentlyAddedCandidates = new HashSet<int>();
- }
+ // Put all of the necessary state into one object
+ var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());
+ vState.coverageManager = null;
- private void declareNodes()
- {
- var send = false;
- var declarenode = "declare-node";
- foreach (var n in newNodes)
- {
- if (declaredNodes.Contains(n)) continue;
- declaredNodes.Add(n);
- send = true;
- declarenode += string.Format(" {0} {1}", calls.getPersistentId(n), calls.getProc(n));
- }
- if(send)
- coverageProcess.StandardInput.WriteLine(declarenode);
- }
+ // We'll restore the original state of the theorem prover at the end
+ // of this procedure
+ vState.checker.prover.Push();
- private void declareEdges()
- {
- if (edges.Count == 0) return;
+ // Do eager inlining
+ while (calls.currCandidates.Count > 0) {
+ List<int> toExpand = new List<int>();
- var declareedge = "declare-edge";
- foreach (var e in edges)
- {
- declareedge += string.Format(" {0} {1}", calls.getPersistentId(e.Key), calls.getPersistentId(e.Value));
- }
- coverageProcess.StandardInput.WriteLine(declareedge);
- }
+ foreach (int id in calls.currCandidates) {
+ Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");
+ toExpand.Add(id);
+ }
+ DoExpansion(toExpand, vState);
+ }
- public void syncGraph()
- {
- if (coverageProcess == null || newNodes.Count == 0)
- {
- edges.Clear();
- return;
- }
+ // Find all the boolean constants
+ var allConsts = new HashSet<VCExprVar>();
+ foreach (var decl in program.TopLevelDeclarations) {
+ var constant = decl as Constant;
+ if (constant == null) continue;
+ if (!allBoolVars.Contains(constant.Name)) continue;
+ var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);
+ allConsts.Add(v);
+ }
- coverageProcess.StandardInput.WriteLine("batch-graph-command-begin");
- coverageProcess.StandardInput.WriteLine("reset-color");
-
- // Go through the edges
- var greenNodes = new HashSet<int>();
- var redNodes = new HashSet<int>();
- foreach (var node in calls.currCandidates)
- {
- if (calls.getRecursionBound(node) > CommandLineOptions.Clo.RecursionBound)
- {
- redNodes.Add(node);
- }
- else
- {
- greenNodes.Add(node);
- }
+ // Now, lets start the algo
+ var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);
- }
- // Send data across
- declareNodes();
- declareEdges();
-
- if (greenNodes.Count != 0)
- {
- var color = "color green";
- foreach (var n in greenNodes)
- {
- color += string.Format(" {0}", calls.getPersistentId(n));
- }
- coverageProcess.StandardInput.WriteLine(color);
- }
+ var ret = new HashSet<string>();
+ foreach (var v in min) {
+ //Console.WriteLine(v.Name);
+ ret.Add(v.Name);
+ }
+ allBoolVars = ret;
- if (redNodes.Count != 0)
- {
- var color = "color red";
- foreach (var n in redNodes)
- {
- color += string.Format(" {0}", calls.getPersistentId(n));
- }
- coverageProcess.StandardInput.WriteLine(color);
- }
+ vState.checker.prover.Pop();
- coverageProcess.StandardInput.WriteLine("batch-graph-command-end");
+ return Outcome.Correct;
+ }
- edges.Clear();
- newNodes = new HashSet<int>();
- }
+ private HashSet<VCExprVar> refinementLoop(ApiChecker apiChecker, HashSet<VCExprVar> trackedVars, HashSet<VCExprVar> trackedVarsUpperBound, HashSet<VCExprVar> allVars) {
+ Debug.Assert(trackedVars.IsSubsetOf(trackedVarsUpperBound));
- public void reportBug()
- {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status bug");
- }
+ // If we already know the fate of all vars, then we're done.
+ if (trackedVars.Count == trackedVarsUpperBound.Count)
+ return new HashSet<VCExprVar>(trackedVars);
- public void reportCorrect()
- {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status correct");
- }
+ // See if we already have enough variables tracked
+ var success = refinementLoopCheckPath(apiChecker, trackedVars, allVars);
+ if (success) {
+ // We have enough
+ return new HashSet<VCExprVar>(trackedVars);
+ }
- public void reportCorrect(int bound)
- {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status bound {0}", bound);
- }
+ // If all that remains is 1 variable, then we know that we must track it
+ if (trackedVars.Count + 1 == trackedVarsUpperBound.Count)
+ return new HashSet<VCExprVar>(trackedVarsUpperBound);
+
+ // Partition the remaining set of variables
+ HashSet<VCExprVar> part1, part2;
+ var temp = new HashSet<VCExprVar>(trackedVarsUpperBound);
+ temp.ExceptWith(trackedVars);
+ Partition<VCExprVar>(temp, out part1, out part2);
+
+ // First half
+ var fh = new HashSet<VCExprVar>(trackedVars); fh.UnionWith(part2);
+ var s1 = refinementLoop(apiChecker, fh, trackedVarsUpperBound, allVars);
+
+ var a = new HashSet<VCExprVar>(part1); a.IntersectWith(s1);
+ var b = new HashSet<VCExprVar>(part1); b.ExceptWith(s1);
+ var c = new HashSet<VCExprVar>(trackedVarsUpperBound); c.ExceptWith(b);
+ a.UnionWith(trackedVars);
+
+ // Second half
+ return refinementLoop(apiChecker, a, c, allVars);
+ }
+
+ Dictionary<int, List<HashSet<string>>> satQueryCache;
+ Dictionary<int, List<HashSet<string>>> unsatQueryCache;
+
+ private bool refinementLoopCheckPath(ApiChecker apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars) {
+ var assumptions = new List<VCExpr>();
+ var prover = apiChecker.prover;
+ var query = new HashSet<string>();
+ varsToSet.Iter(v => query.Add(v.Name));
+
+ if (checkCache(query, unsatQueryCache)) {
+ prover.LogComment("FindLeast: Query Cache Hit");
+ return true;
+ }
+ if (checkCache(query, satQueryCache)) {
+ prover.LogComment("FindLeast: Query Cache Hit");
+ return false;
+ }
- public void reportError()
- {
- if (coverageProcess == null) return;
- coverageProcess.StandardInput.WriteLine("set-status error");
- }
+ prover.LogComment("FindLeast: Query Begin");
- public Task getNextTask()
- {
- if (coverageProcess == null) return new Task("step", calls);
- if (coverageProcess.HasExited)
- {
- coverageProcess = null;
- return new Task("step", calls);
- }
+ foreach (var c in allVars) {
+ if (varsToSet.Contains(c)) {
+ assumptions.Add(c);
+ }
+ else {
+ assumptions.Add(prover.VCExprGen.Not(c));
+ }
+ }
- var ts = getNextTimeStamp();
- coverageProcess.StandardInput.WriteLine("get-input " + ts.ToString());
- string q = getQuery(ts);
- return new Task(q, calls);
- }
+ var o = apiChecker.CheckAssumptions(assumptions);
+ Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);
+ //Console.WriteLine("Result = " + o.ToString());
+ prover.LogComment("FindLeast: Query End");
- public void stop()
- {
- if (coverageProcess != null)
- {
- if (stopCoverageProcess)
- {
- coverageProcess.StandardInput.WriteLine("done");
- do
- {
- coverageProcess.WaitForExit(100);
- coverageProcess.StandardInput.WriteLine();
- } while (!coverageProcess.HasExited);
- }
- }
- }
+ if (o == Outcome.Correct) {
+ insertCache(query, unsatQueryCache);
+ return true;
+ }
- public int getNextTimeStamp()
- {
- timeStamp++;
- return timeStamp - 1;
- }
- }
+ insertCache(query, satQueryCache);
+ return false;
+ }
- public class ApiChecker {
- public ProverInterface prover;
- public ProverInterface.ErrorHandler reporter;
+ private bool checkCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache) {
+ if (!cache.ContainsKey(q.Count)) return false;
+ foreach (var s in cache[q.Count]) {
+ if (q.SetEquals(s)) return true;
+ }
+ return false;
+ }
- public ApiChecker(ProverInterface prover, ProverInterface.ErrorHandler reporter) {
- this.reporter = reporter;
- this.prover = prover;
- }
+ private void insertCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache) {
+ if (!cache.ContainsKey(q.Count)) {
+ cache.Add(q.Count, new List<HashSet<string>>());
+ }
+ cache[q.Count].Add(q);
+ }
+
+ public static void Partition<T>(HashSet<T> values, out HashSet<T> part1, out HashSet<T> part2) {
+ part1 = new HashSet<T>();
+ part2 = new HashSet<T>();
+ var size = values.Count;
+ var crossed = false;
+ var curr = 0;
+ foreach (var s in values) {
+ if (crossed) part2.Add(s);
+ else part1.Add(s);
+ curr++;
+ if (!crossed && curr >= size / 2) crossed = true;
+ }
+ }
+
+ public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback) {
+ Debug.Assert(QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"));
+ Debug.Assert(this.program == program);
+
+ var computeUnderBound = true;
+
+ #region stratified inlining options
+ switch (CommandLineOptions.Clo.StratifiedInliningOption) {
+ case 1:
+ useSummary = true;
+ break;
+ case 2:
+ useSummary = true;
+ computeUnderBound = false;
+ break;
+ }
+ #endregion
- private Outcome CheckVC() {
- prover.Check();
- ProverInterface.Outcome outcome = prover.CheckOutcomeCore(reporter);
- return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
+ ProverInterface prover2 = null;
+ if (useSummary) {
+ prover2 = ProverInterface.CreateProver(program, "prover2.txt", true, CommandLineOptions.Clo.ProverKillTime);
+ }
- public Outcome CheckAssumptions(List<VCExpr> assumptions) {
- if (assumptions.Count == 0) {
- return CheckVC();
- }
+ // Record current time
+ var startTime = DateTime.UtcNow;
- prover.Push();
- foreach (var a in assumptions) {
- prover.Assert(a, true);
- }
- Outcome ret = CheckVC();
- prover.Pop();
- return ret;
- }
-
- public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {
- List<int> unsatisfiedSoftAssumptions;
- ProverInterface.Outcome outcome = prover.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);
- return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
+ // Flush any axioms that came with the program before we start SI on this implementation
+ prover.AssertAxioms();
- public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore) {
- ProverInterface.Outcome outcome = prover.CheckAssumptions(assumptions, out unsatCore, reporter);
- return ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
- }
- }
+ // Run live variable analysis
+ if (CommandLineOptions.Clo.LiveVariableAnalysis == 2) {
+ Microsoft.Boogie.InterProcGenKill.ComputeLiveVars(impl, program);
+ }
- // Store important information related to a single VerifyImplementation query
- public class VerificationState
- {
- // The call tree
- public FCallHandler calls;
- public ApiChecker checker;
- // The coverage graph reporter
- public CoverageGraphManager coverageManager;
- // For statistics
- public int vcSize;
- public int expansionCount;
-
- // For making summary queries on the side
- public ApiChecker checker2;
-
- public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {
- prover.Assert(vcMain, false);
- this.calls = calls;
- this.checker = new ApiChecker(prover, reporter);
- vcSize = 0;
- expansionCount = 0;
- }
- public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter,
- ProverInterface prover2, ProverInterface.ErrorHandler reporter2)
- : this(vcMain, calls, prover, reporter) {
- this.checker2 = new ApiChecker(prover2, reporter2);
- }
- }
+ // Get the VC of the current procedure
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];
+ info.GenerateVC();
+ VCExpr vc = info.vcexpr;
+ Hashtable mainLabel2absy = info.label2absy;
+ var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info);
- public Outcome FindLeastToVerify(Implementation impl, ref HashSet<string> allBoolVars)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ // Find all procedure calls in vc and put labels on them
+ FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
+ calls.setCurrProcAsMain();
+ vc = calls.Mutate(vc, true);
+ reporter.SetCandidateHandler(calls);
+ calls.id2VC.Add(0, vc);
+ calls.extraRecursion = extraRecBound;
- // Record current time
- var startTime = DateTime.UtcNow;
+ // Identify summary candidates: Match ensure clauses with the appropriate call site
+ if (useSummary) calls.matchSummaries();
- // No Max: avoids theorem prover restarts
- CommandLineOptions.Clo.MaxProverMemory = 0;
+ // create a process for displaying coverage information
+ var coverageManager = new CoverageGraphManager(calls);
+ coverageManager.addMain();
- // Initialize cache
- satQueryCache = new Dictionary<int, List<HashSet<string>>>();
- unsatQueryCache = new Dictionary<int, List<HashSet<string>>>();
- Contract.Assert(implName2StratifiedInliningInfo != null);
+ // We'll restore the original state of the theorem prover at the end
+ // of this procedure
+ prover.Push();
- // Build VCs for all procedures
- foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)
- {
- Contract.Assert(info != null);
- info.GenerateVC(this);
- }
+ // Put all of the necessary state into one object
+ var vState = new VerificationState(vc, calls, prover, reporter, prover2, new EmptyErrorHandler());
+ vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
+ vState.coverageManager = coverageManager;
- // Get the VC of the current procedure
- VCExpr vcMain;
- Hashtable/*<int, Absy!>*/ mainLabel2absy;
- ModelViewInfo mvInfo;
-
- ConvertCFG2DAG(impl);
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
- var exprGen = prover.Context.ExprGen;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
- vcMain = GenerateVC(impl, controlFlowVariableExpr, out mainLabel2absy, prover.Context);
- if (!CommandLineOptions.Clo.UseLabels) {
- VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
- VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vcMain = exprGen.Implies(eqExpr, vcMain);
- }
+ if (useSummary) summaryComputation = new SummaryComputation(vState, computeUnderBound);
- // Find all procedure calls in vc and put labels on them
- FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
- calls.setCurrProcAsMain();
- vcMain = calls.Mutate(vcMain, true);
- // Put all of the necessary state into one object
- var vState = new VerificationState(vcMain, calls, prover, new EmptyErrorHandler());
- vState.coverageManager = null;
+ Outcome ret = Outcome.ReachedBound;
- // We'll restore the original state of the theorem prover at the end
- // of this procedure
- vState.checker.prover.Push();
+ #region eager inlining
+ for (int i = 1; i < CommandLineOptions.Clo.StratifiedInlining && calls.currCandidates.Count > 0; i++) {
+ List<int> toExpand = new List<int>();
- // Do eager inlining
- while (calls.currCandidates.Count > 0)
- {
- List<int> toExpand = new List<int>();
+ foreach (int id in calls.currCandidates) {
+ if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound) {
+ toExpand.Add(id);
+ }
+ }
+ DoExpansion(toExpand, vState);
+ }
+ #endregion
- foreach (int id in calls.currCandidates)
- {
- Debug.Assert(calls.getRecursionBound(id) <= 1, "Recursion not supported");
- toExpand.Add(id);
- }
- DoExpansion(toExpand, vState);
+ #region Repopulate call tree, if there is one
+ if (PersistCallTree && callTree != null) {
+ bool expand = true;
+ while (expand) {
+ List<int> toExpand = new List<int>();
+ foreach (int id in calls.currCandidates) {
+ if (callTree.ContainsKey(calls.getPersistentId(id))) {
+ toExpand.Add(id);
}
+ }
+ if (toExpand.Count == 0) expand = false;
+ else {
+ DoExpansion(toExpand, vState);
+ }
+ }
+ }
+ #endregion
- // Find all the boolean constants
- var allConsts = new HashSet<VCExprVar>();
- foreach (var decl in program.TopLevelDeclarations)
- {
- var constant = decl as Constant;
- if (constant == null) continue;
- if (!allBoolVars.Contains(constant.Name)) continue;
- var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);
- allConsts.Add(v);
- }
+ #region Coverage reporter
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
+ Console.WriteLine(">> SI: Size of VC after eager inlining: {0}", vState.vcSize);
+ }
+ #endregion
- // Now, lets start the algo
- var min = refinementLoop(vState.checker, new HashSet<VCExprVar>(), allConsts, allConsts);
+ // Under-approx query is only needed if something was inlined since
+ // the last time an under-approx query was made
+ // TODO: introduce this
+ // bool underApproxNeeded = true;
- var ret = new HashSet<string>();
- foreach (var v in min)
- {
- //Console.WriteLine(v.Name);
- ret.Add(v.Name);
- }
- allBoolVars = ret;
+ // The recursion bound for stratified search
+ int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;
- vState.checker.prover.Pop();
+ int done = 0;
- return Outcome.Correct;
- }
+ int iters = 0;
- private HashSet<VCExprVar> refinementLoop(ApiChecker apiChecker, HashSet<VCExprVar> trackedVars, HashSet<VCExprVar> trackedVarsUpperBound, HashSet<VCExprVar> allVars)
- {
- Debug.Assert(trackedVars.IsSubsetOf(trackedVarsUpperBound));
+ // for blocking candidates (and focusing on a counterexample)
+ var block = new HashSet<int>();
- // If we already know the fate of all vars, then we're done.
- if (trackedVars.Count == trackedVarsUpperBound.Count)
- return new HashSet<VCExprVar>(trackedVars);
+ // Process tasks while not done. We're done when:
+ // case 1: (correct) We didn't find a bug (either an over-approx query was valid
+ // or we reached the recursion bound) and the task is "step"
+ // case 2: (bug) We find a bug
+ // case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
+ while (true) {
+ boundUsedInLastQuery = bound;
- // See if we already have enough variables tracked
- var success = refinementLoopCheckPath(apiChecker, trackedVars, allVars);
- if (success)
- {
- // We have enough
- return new HashSet<VCExprVar>(trackedVars);
- }
+ // Check timeout
+ if (CommandLineOptions.Clo.ProverKillTime != -1) {
+ if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime) {
+ ret = Outcome.TimedOut;
+ break;
+ }
+ }
- // If all that remains is 1 variable, then we know that we must track it
- if (trackedVars.Count + 1 == trackedVarsUpperBound.Count)
- return new HashSet<VCExprVar>(trackedVarsUpperBound);
-
- // Partition the remaining set of variables
- HashSet<VCExprVar> part1, part2;
- var temp = new HashSet<VCExprVar>(trackedVarsUpperBound);
- temp.ExceptWith(trackedVars);
- Partition<VCExprVar>(temp, out part1, out part2);
-
- // First half
- var fh = new HashSet<VCExprVar>(trackedVars); fh.UnionWith(part2);
- var s1 = refinementLoop(apiChecker, fh, trackedVarsUpperBound, allVars);
-
- var a = new HashSet<VCExprVar>(part1); a.IntersectWith(s1);
- var b = new HashSet<VCExprVar>(part1); b.ExceptWith(s1);
- var c = new HashSet<VCExprVar>(trackedVarsUpperBound); c.ExceptWith(b);
- a.UnionWith(trackedVars);
-
- // Second half
- return refinementLoop(apiChecker, a, c, allVars);
- }
-
- Dictionary<int, List<HashSet<string>>> satQueryCache;
- Dictionary<int, List<HashSet<string>>> unsatQueryCache;
-
- private bool refinementLoopCheckPath(ApiChecker apiChecker, HashSet<VCExprVar> varsToSet, HashSet<VCExprVar> allVars)
- {
- var assumptions = new List<VCExpr>();
- var prover = apiChecker.prover;
- var query = new HashSet<string>();
- varsToSet.Iter(v => query.Add(v.Name));
-
- if (checkCache(query, unsatQueryCache))
- {
- prover.LogComment("FindLeast: Query Cache Hit");
- return true;
- }
- if (checkCache(query, satQueryCache))
- {
- prover.LogComment("FindLeast: Query Cache Hit");
- return false;
- }
+ // Note: in the absence of a coverage graph process, the task is always "step"
+ coverageManager.syncGraph();
+ var task = coverageManager.getNextTask();
+ if (task.type == CoverageGraphManager.Task.TaskType.INLINE) {
+ if (done == 2) continue;
+ foreach (var id in task.nodes) {
+ calls.setRecursionIncrement(id, 0);
+ coverageManager.addNode(id);
+ }
+ DoExpansion(task.nodes, vState);
+ }
+ else if (task.type == CoverageGraphManager.Task.TaskType.BLOCK) {
+ if (done == 2) continue;
+ foreach (var id in task.nodes) {
+ calls.setRecursionIncrement(id, CommandLineOptions.Clo.RecursionBound + 1);
+ coverageManager.addNode(id);
+ }
+ }
+ else if (task.type == CoverageGraphManager.Task.TaskType.STEP) {
+ if (done > 0) {
+ break;
+ }
- prover.LogComment("FindLeast: Query Begin");
+ VCExpr summary = null;
+ if (useSummary) summary = summaryComputation.getSummary();
- foreach (var c in allVars)
- {
- if (varsToSet.Contains(c))
- {
- assumptions.Add(c);
- }
- else
- {
- assumptions.Add(prover.VCExprGen.Not(c));
- }
- }
+ if (useSummary && summary != null) {
+ vState.checker.prover.Push();
+ vState.checker.prover.Assert(summary, true);
+ }
- var o = apiChecker.CheckAssumptions(assumptions);
- Debug.Assert(o == Outcome.Correct || o == Outcome.Errors);
- //Console.WriteLine("Result = " + o.ToString());
- prover.LogComment("FindLeast: Query End");
+ // Stratified Step
+ ret = stratifiedStep(bound, vState, block);
+ iters++;
- if (o == Outcome.Correct)
- {
- insertCache(query, unsatQueryCache);
- return true;
- }
+ if (useSummary && summary != null) {
+ vState.checker.prover.Pop();
+ }
- insertCache(query, satQueryCache);
- return false;
- }
+ // Sorry, out of luck (time/memory)
+ if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut) {
+ done = 3;
+ coverageManager.reportError();
+ continue;
+ }
- private bool checkCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache)
- {
- if (!cache.ContainsKey(q.Count)) return false;
- foreach (var s in cache[q.Count])
- {
- if (q.SetEquals(s)) return true;
+ if (ret == Outcome.Errors && reporter.underapproximationMode) {
+ // Found a bug
+ done = 2;
+ coverageManager.reportBug();
+ }
+ else if (ret == Outcome.Correct) {
+ if (block.Count == 0) {
+ // Correct
+ done = 1;
+ coverageManager.reportCorrect();
}
- return false;
- }
-
- private void insertCache(HashSet<string> q, Dictionary<int, List<HashSet<string>>> cache)
- {
- if (!cache.ContainsKey(q.Count))
- {
- cache.Add(q.Count, new List<HashSet<string>>());
+ else {
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
}
- cache[q.Count].Add(q);
- }
-
- public static void Partition<T>(HashSet<T> values, out HashSet<T> part1, out HashSet<T> part2)
- {
- part1 = new HashSet<T>();
- part2 = new HashSet<T>();
- var size = values.Count;
- var crossed = false;
- var curr = 0;
- foreach (var s in values)
- {
- if (crossed) part2.Add(s);
- else part1.Add(s);
- curr++;
- if (!crossed && curr >= size / 2) crossed = true;
+ }
+ else if (ret == Outcome.ReachedBound) {
+ if (block.Count == 0) {
+ // Increment bound
+ bound++;
+ if (useSummary) summaryComputation.boundChanged();
+
+ if (bound > CommandLineOptions.Clo.RecursionBound) {
+ // Correct under bound
+ done = 1;
+ coverageManager.reportCorrect(bound);
+ }
}
- }
-
- public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- Debug.Assert(this.program == program);
- var computeUnderBound = true;
-
- #region stratified inlining options
- switch (CommandLineOptions.Clo.StratifiedInliningOption)
- {
- case 1:
- useSummary = true;
- break;
- case 2:
- useSummary = true;
- computeUnderBound = false;
- break;
+ else {
+ Contract.Assert(useSummary);
+ // reset blocked and continue loop
+ block.Clear();
}
- #endregion
-
- ProverInterface prover2 = null;
+ }
+ else {
+ // Do inlining
+ Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
+ Contract.Assert(reporter.candidatesToExpand.Count != 0);
if (useSummary) {
- prover2 = ProverInterface.CreateProver(program, "prover2.txt", true, CommandLineOptions.Clo.ProverKillTime);
+ // compute candidates to block
+ block = new HashSet<int>(calls.currCandidates);
+ block.ExceptWith(reporter.candidatesToExpand);
}
- // Record current time
- var startTime = DateTime.UtcNow;
+ #region expand call tree
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
+ Console.Write(">> SI Inlining: ");
+ reporter.candidatesToExpand
+ .Select(c => calls.getProc(c))
+ .Iter(c => { if (!isSkipped(c)) Console.Write("{0} ", c); });
- // Flush any axioms that came with the program before we start SI on this implementation
- prover.AssertAxioms();
+ Console.WriteLine();
+ Console.Write(">> SI Skipping: ");
+ reporter.candidatesToExpand
+ .Select(c => calls.getProc(c))
+ .Iter(c => { if (isSkipped(c)) Console.Write("{0} ", c); });
- // Run live variable analysis
- if (CommandLineOptions.Clo.LiveVariableAnalysis == 2)
- {
- Microsoft.Boogie.InterProcGenKill.ComputeLiveVars(impl, program);
- }
+ Console.WriteLine();
- // Get the VC of the current procedure
- VCExpr vc;
- Hashtable/*<int, Absy!>*/ mainLabel2absy;
- StratifiedInliningErrorReporter reporter;
- GetVC(impl, program, prover, callback, out vc, out mainLabel2absy, out reporter);
-
- // Find all procedure calls in vc and put labels on them
- FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);
- calls.setCurrProcAsMain();
- vc = calls.Mutate(vc, true);
- reporter.SetCandidateHandler(calls);
- calls.id2VC.Add(0, vc);
-
- // Identify summary candidates: Match ensure clauses with the appropriate call site
- if (useSummary) calls.matchSummaries();
-
- // create a process for displaying coverage information
- var coverageManager = new CoverageGraphManager(calls);
- coverageManager.addMain();
-
-
- // We'll restore the original state of the theorem prover at the end
- // of this procedure
- prover.Push();
-
- // Put all of the necessary state into one object
- var vState = new VerificationState(vc, calls, prover, reporter, prover2, new EmptyErrorHandler());
- vState.vcSize += SizeComputingVisitor.ComputeSize(vc);
- vState.coverageManager = coverageManager;
-
- if (useSummary) summaryComputation = new SummaryComputation(vState, computeUnderBound);
-
-
- Outcome ret = Outcome.ReachedBound;
-
- #region eager inlining
- for (int i = 1; i < CommandLineOptions.Clo.StratifiedInlining && calls.currCandidates.Count > 0; i++)
- {
- List<int> toExpand = new List<int>();
-
- foreach (int id in calls.currCandidates)
- {
- if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)
- {
- toExpand.Add(id);
- }
- }
- DoExpansion(toExpand, vState);
}
- #endregion
- #region Repopulate call tree, if there is one
- if (PersistCallTree && callTree != null)
- {
- bool expand = true;
- while (expand)
- {
- List<int> toExpand = new List<int>();
- foreach (int id in calls.currCandidates)
- {
- if (callTree.ContainsKey(calls.getPersistentId(id)))
- {
- toExpand.Add(id);
- }
- }
- if (toExpand.Count == 0) expand = false;
- else {
- DoExpansion(toExpand, vState);
- }
- }
- }
- #endregion
+ // Expand and try again
+ vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
+ DoExpansion(reporter.candidatesToExpand, vState);
+ vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
- #region Coverage reporter
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
- {
- Console.WriteLine(">> SI: Size of VC after eager inlining: {0}", vState.vcSize);
- }
#endregion
+ }
+ }
+ else if (task.type == CoverageGraphManager.Task.TaskType.REACHABLE) {
+ if (done == 2) continue;
+ var node = task.queryNode;
+ // assert that any path must pass through this node
+ var expr = calls.getTrueExpr(node);
+ vState.checker.prover.Assert(expr, true);
+ }
+ else {
+ Console.WriteLine("Ignoring task: " + task.ToString());
+ }
- // Under-approx query is only needed if something was inlined since
- // the last time an under-approx query was made
- // TODO: introduce this
- // bool underApproxNeeded = true;
-
- // The recursion bound for stratified search
- int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;
-
- int done = 0;
-
- int iters = 0;
-
- // for blocking candidates (and focusing on a counterexample)
- var block = new HashSet<int>();
-
- // Process tasks while not done. We're done when:
- // case 1: (correct) We didn't find a bug (either an over-approx query was valid
- // or we reached the recursion bound) and the task is "step"
- // case 2: (bug) We find a bug
- // case 3: (internal error) The theorem prover TimesOut of runs OutOfMemory
- while (true)
- {
- // Check timeout
- if (CommandLineOptions.Clo.ProverKillTime != -1)
- {
- if ((DateTime.UtcNow - startTime).TotalSeconds > CommandLineOptions.Clo.ProverKillTime)
- {
- ret = Outcome.TimedOut;
- break;
- }
- }
+ }
- // Note: in the absence of a coverage graph process, the task is always "step"
- coverageManager.syncGraph();
- var task = coverageManager.getNextTask();
- if (task.type == CoverageGraphManager.Task.TaskType.INLINE)
- {
- if (done == 2) continue;
- foreach (var id in task.nodes)
- {
- calls.setRecursionIncrement(id, 0);
- coverageManager.addNode(id);
- }
- DoExpansion(task.nodes, vState);
- }
- else if (task.type == CoverageGraphManager.Task.TaskType.BLOCK)
- {
- if (done == 2) continue;
- foreach (var id in task.nodes)
- {
- calls.setRecursionIncrement(id, CommandLineOptions.Clo.RecursionBound + 1);
- coverageManager.addNode(id);
- }
- }
- else if (task.type == CoverageGraphManager.Task.TaskType.STEP)
- {
- if (done > 0)
- {
- break;
- }
-
- VCExpr summary = null;
- if (useSummary) summary = summaryComputation.getSummary();
-
- if (useSummary && summary != null)
- {
- vState.checker.prover.Push();
- vState.checker.prover.Assert(summary, true);
- }
-
- // Stratified Step
- ret = stratifiedStep(bound, vState, block);
- iters++;
-
- if (useSummary && summary != null)
- {
- vState.checker.prover.Pop();
- }
-
- // Sorry, out of luck (time/memory)
- if (ret == Outcome.Inconclusive || ret == Outcome.OutOfMemory || ret == Outcome.TimedOut)
- {
- done = 3;
- coverageManager.reportError();
- continue;
- }
-
- if (ret == Outcome.Errors && reporter.underapproximationMode)
- {
- // Found a bug
- done = 2;
- coverageManager.reportBug();
- }
- else if (ret == Outcome.Correct)
- {
- if (block.Count == 0)
- {
- // Correct
- done = 1;
- coverageManager.reportCorrect();
- }
- else
- {
- Contract.Assert(useSummary);
- // reset blocked and continue loop
- block.Clear();
- }
- }
- else if (ret == Outcome.ReachedBound)
- {
- if (block.Count == 0)
- {
- // Increment bound
- bound++;
- if (useSummary) summaryComputation.boundChanged();
-
- if (bound > CommandLineOptions.Clo.RecursionBound)
- {
- // Correct under bound
- done = 1;
- coverageManager.reportCorrect(bound);
- }
- }
- else
- {
- Contract.Assert(useSummary);
- // reset blocked and continue loop
- block.Clear();
- }
- }
- else
- {
- // Do inlining
- Debug.Assert(ret == Outcome.Errors && !reporter.underapproximationMode);
- Contract.Assert(reporter.candidatesToExpand.Count != 0);
- if (useSummary)
- {
- // compute candidates to block
- block = new HashSet<int>(calls.currCandidates);
- block.ExceptWith(reporter.candidatesToExpand);
- }
-
- #region expand call tree
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
- {
- Console.Write(">> SI Inlining: ");
- reporter.candidatesToExpand.ForEach(c =>
- { if (!calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });
-
- Console.WriteLine();
- Console.Write(">> SI Skipping: ");
- reporter.candidatesToExpand.ForEach(c =>
- { if (calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });
-
- Console.WriteLine();
- }
- // Expand and try again
- vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion begin ;;;;;;;;;;");
- DoExpansion(reporter.candidatesToExpand, vState);
- vState.checker.prover.LogComment(";;;;;;;;;;;; Expansion end ;;;;;;;;;;");
-
- #endregion
- }
- }
- else if (task.type == CoverageGraphManager.Task.TaskType.REACHABLE)
- {
- if (done == 2) continue;
- var node = task.queryNode;
- // assert that any path must pass through this node
- var expr = calls.getTrueExpr(node);
- vState.checker.prover.Assert(expr, true);
- }
- else
- {
- Console.WriteLine("Ignoring task: " + task.ToString());
- }
+ // Pop off everything that we pushed so that there are no side effects from
+ // this call to VerifyImplementation
+ vState.checker.prover.Pop();
- }
+ #region Coverage reporter
+ if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0) {
+ Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
+ Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
+ Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => isSkipped(i, calls)).Count());
+ Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);
+ }
+ #endregion
+ coverageManager.stop();
- // Pop off everything that we pushed so that there are no side effects from
- // this call to VerifyImplementation
- vState.checker.prover.Pop();
+ numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);
- #region Coverage reporter
- if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)
- {
- Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);
- Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);
- Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => calls.isSkipped(i)).Count());
- Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);
- }
- #endregion
- coverageManager.stop();
-
- numInlined = (calls.candidateParent.Keys.Count + 1) - (calls.currCandidates.Count);
-
- var rbound = "Procs that reached bound: ";
- foreach (var s in procsThatReachedRecBound) rbound += " " + s;
- if(ret == Outcome.ReachedBound) Helpers.ExtraTraceInformation(rbound);
-
- // Store current call tree
- if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound))
- {
- callTree = new Dictionary<string, int>();
- //var persistentNodes = new HashSet<int>(calls.candidateParent.Values);
- var persistentNodes = new HashSet<int>(calls.candidateParent.Keys);
- persistentNodes.Add(0);
- persistentNodes.ExceptWith(calls.currCandidates);
-
- foreach (var id in persistentNodes)
- {
- callTree.Add(calls.getPersistentId(id), 0);
- }
- }
- if (prover2 != null) prover2.Close();
- return ret;
- }
-
- // A step of the stratified inlining algorithm: both under-approx and over-approx queries
- private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block)
- {
- var calls = vState.calls;
- var checker = vState.checker;
- var prover = checker.prover;
- var reporter = checker.reporter as StratifiedInliningErrorReporter;
-
- reporter.underapproximationMode = true;
- prover.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
- List<VCExpr> assumptions = new List<VCExpr>();
-
- foreach (int id in calls.currCandidates)
- {
- if (!calls.isSkipped(id))
- assumptions.Add(calls.getFalseExpr(id));
- }
- Outcome ret = checker.CheckAssumptions(assumptions);
- prover.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
-
- if (ret != Outcome.Correct)
- {
- // Either the query returned an error or it ran out of memory or time.
- // In all cases, we are done.
- return ret;
- }
+ var rbound = "Procs that reached bound: ";
+ foreach (var s in procsThatReachedRecBound) rbound += " " + s;
+ if (ret == Outcome.ReachedBound) Helpers.ExtraTraceInformation(rbound);
- if (calls.currCandidates.Count == 0)
- {
- // If we didn't underapproximate, then we're done
- return ret;
- }
+ // Store current call tree
+ if (PersistCallTree && (ret == Outcome.Correct || ret == Outcome.Errors || ret == Outcome.ReachedBound)) {
+ callTree = new Dictionary<string, int>();
+ //var persistentNodes = new HashSet<int>(calls.candidateParent.Values);
+ var persistentNodes = new HashSet<int>(calls.candidateParent.Keys);
+ persistentNodes.Add(0);
+ persistentNodes.ExceptWith(calls.currCandidates);
- prover.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");
-
- // Over-approx query
- reporter.underapproximationMode = false;
-
- // Push "true" for all, except:
- // push "false" for all candidates that have reached
- // the recursion bounds
-
- bool allTrue = true;
- bool allFalse = true;
- List<VCExpr> softAssumptions = new List<VCExpr>();
-
- assumptions = new List<VCExpr>();
- procsThatReachedRecBound.Clear();
-
- foreach (int id in calls.currCandidates)
- {
- if (calls.isSkipped(id)) continue;
-
- int idBound = calls.getRecursionBound(id);
- if (idBound <= bound)
- {
- if (idBound > 1)
- softAssumptions.Add(calls.getFalseExpr(id));
-
- if (block.Contains(id))
- {
- Contract.Assert(useSummary);
- assumptions.Add(calls.getFalseExpr(id));
- allTrue = false;
- }
- else
- {
- allFalse = false;
- }
- }
- else
- {
- procsThatReachedRecBound.Add(calls.getProc(id));
- assumptions.Add(calls.getFalseExpr(id));
- allTrue = false;
- }
- }
+ foreach (var id in persistentNodes) {
+ callTree.Add(calls.getPersistentId(id), 0);
+ }
+ }
+ if (prover2 != null) prover2.Close();
+ return ret;
+ }
+
+ // A step of the stratified inlining algorithm: both under-approx and over-approx queries
+ private Outcome stratifiedStep(int bound, VerificationState vState, HashSet<int> block) {
+ var calls = vState.calls;
+ var checker = vState.checker;
+ var prover = checker.prover;
+ var reporter = checker.reporter as StratifiedInliningErrorReporter;
+
+ reporter.underapproximationMode = true;
+ prover.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");
+ List<VCExpr> assumptions = new List<VCExpr>();
+
+ foreach (int id in calls.currCandidates) {
+ if (!isSkipped(id, calls))
+ assumptions.Add(calls.getFalseExpr(id));
+ }
+ Outcome ret = checker.CheckAssumptions(assumptions);
+ prover.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
- if (allFalse)
- {
- // If we made all candidates false, then this is the same
- // as the underapprox query. We already know the answer.
- ret = Outcome.Correct;
- }
- else
- {
- ret = CommandLineOptions.Clo.NonUniformUnfolding
- ? checker.CheckAssumptions(assumptions, softAssumptions)
- : checker.CheckAssumptions(assumptions);
- }
+ if (ret != Outcome.Correct) {
+ // Either the query returned an error or it ran out of memory or time.
+ // In all cases, we are done.
+ return ret;
+ }
- if (ret != Outcome.Correct && ret != Outcome.Errors)
- {
- // The query ran out of memory or time, that's it,
- // we cannot do better. Give up!
- return ret;
- }
+ if (calls.currCandidates.Count == 0) {
+ // If we didn't underapproximate, then we're done
+ return ret;
+ }
- if (ret == Outcome.Correct)
- {
- // If nothing was made false, then the program is correct
- if (allTrue)
- {
- return ret;
- }
+ prover.LogComment(";;;;;;;;;;;; Overapprox mode begin ;;;;;;;;;;");
- if (useSummary)
- {
- // Find the set of candidates with valid over-approximations
- var assumeTrueCandidates = new HashSet<int>(vState.calls.currCandidates);
- assumeTrueCandidates.ExceptWith(block);
- summaryComputation.compute(assumeTrueCandidates, bound);
- }
+ // Over-approx query
+ reporter.underapproximationMode = false;
- // Nothing more can be done with current recursion bound.
- return Outcome.ReachedBound;
- }
+ // Push "true" for all, except:
+ // push "false" for all candidates that have reached
+ // the recursion bounds
+
+ bool allTrue = true;
+ bool allFalse = true;
+ List<VCExpr> softAssumptions = new List<VCExpr>();
+
+ assumptions = new List<VCExpr>();
+ procsThatReachedRecBound.Clear();
- Contract.Assert(ret == Outcome.Errors);
+ foreach (int id in calls.currCandidates) {
+ if (isSkipped(id, calls)) continue;
- prover.LogComment(";;;;;;;;;;;; Overapprox mode end ;;;;;;;;;;");
+ int idBound = calls.getRecursionBound(id);
+ if (idBound <= bound) {
+ if (idBound > 1)
+ softAssumptions.Add(calls.getFalseExpr(id));
- return ret;
+ if (block.Contains(id)) {
+ Contract.Assert(useSummary);
+ assumptions.Add(calls.getFalseExpr(id));
+ allTrue = false;
+ }
+ else {
+ allFalse = false;
+ }
}
+ else {
+ procsThatReachedRecBound.Add(calls.getProc(id));
+ assumptions.Add(calls.getFalseExpr(id));
+ allTrue = false;
+ }
+ }
- // A counter for adding new variables
- static int newVarCnt = 0;
+ if (allFalse) {
+ // If we made all candidates false, then this is the same
+ // as the underapprox query. We already know the answer.
+ ret = Outcome.Correct;
+ }
+ else {
+ ret = CommandLineOptions.Clo.NonUniformUnfolding
+ ? checker.CheckAssumptions(assumptions, softAssumptions)
+ : checker.CheckAssumptions(assumptions);
+ }
- // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
- private void DoExpansion(List<int>/*!*/ candidates, VerificationState vState)
- {
- Contract.Requires(candidates != null);
- Contract.Requires(vState.calls != null);
- Contract.Requires(vState.checker.prover != null);
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ if (ret != Outcome.Correct && ret != Outcome.Errors) {
+ // The query ran out of memory or time, that's it,
+ // we cannot do better. Give up!
+ return ret;
+ }
- // Skipped calls don't get inlined
- candidates = candidates.FindAll(id => !vState.calls.isSkipped(id));
+ if (ret == Outcome.Correct) {
+ // If nothing was made false, then the program is correct
+ if (allTrue) {
+ return ret;
+ }
- vState.expansionCount += candidates.Count;
-
- var prover = vState.checker.prover;
- var calls = vState.calls;
+ if (useSummary) {
+ // Find the set of candidates with valid over-approximations
+ var assumeTrueCandidates = new HashSet<int>(vState.calls.currCandidates);
+ assumeTrueCandidates.ExceptWith(block);
+ summaryComputation.compute(assumeTrueCandidates, bound);
+ }
- VCExpr exprToPush = VCExpressionGenerator.True;
- Contract.Assert(exprToPush != null);
- foreach (int id in candidates)
- {
- VCExprNAry expr = calls.id2Candidate[id];
- Contract.Assert(expr != null);
- string procName = cce.NonNull(expr.Op as VCExprBoogieFunctionOp).Func.Name;
- if (!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
+ // Nothing more can be done with current recursion bound.
+ return Outcome.ReachedBound;
+ }
- StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
- if (!info.initialized)
- {
- info.GenerateVC(this);
- }
- //Console.WriteLine("Inlining {0}", procName);
- VCExpr expansion = cce.NonNull(info.vcexpr);
-
- if (!CommandLineOptions.Clo.UseLabels) {
- var ctx = prover.Context;
- var bet = ctx.BoogieExprTranslator;
- VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);
- VCExpr eqExpr = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.FromInt(id)));
- expansion = ctx.ExprGen.And(eqExpr, expansion);
- }
+ Contract.Assert(ret == Outcome.Errors);
- // Instantiate the "forall" variables
- Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
- Contract.Assert(info.interfaceExprVars.Count == expr.Length);
- for (int i = 0; i < info.interfaceExprVars.Count; i++)
- {
- substForallDict.Add(info.interfaceExprVars[i], expr[i]);
- }
- VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
-
- SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
- Contract.Assert(subst != null);
- expansion = subst.Mutate(expansion, substForall);
-
- // Instantiate and declare the "exists" variables
- Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
- foreach (VCExprVar v in info.privateExprVars)
- {
- Contract.Assert(v != null);
- string newName = v.Name + "_si_" + newVarCnt.ToString();
- newVarCnt++;
- prover.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
- substExistsDict.Add(v, prover.VCExprGen.Variable(newName, v.Type));
- }
- if (CommandLineOptions.Clo.ModelViewFile != null) {
- SaveSubstitution(vState, id, substForallDict, substExistsDict);
- }
- VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+ prover.LogComment(";;;;;;;;;;;; Overapprox mode end ;;;;;;;;;;");
- subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
- expansion = subst.Mutate(expansion, substExists);
+ return ret;
+ }
- if (!calls.currCandidates.Contains(id))
- {
- Console.WriteLine("Don't know what we just expanded");
- }
+ // A counter for adding new variables
+ static int newVarCnt = 0;
- calls.currCandidates.Remove(id);
+ // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.
+ private void DoExpansion(List<int>/*!*/ candidates, VerificationState vState) {
+ Contract.Requires(candidates != null);
+ Contract.Requires(vState.calls != null);
+ Contract.Requires(vState.checker.prover != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
- // Record the new set of candidates and rename absy labels
- calls.currInlineCount = id;
- calls.setCurrProc(procName);
- expansion = calls.Mutate(expansion, true);
- if (useSummary) calls.matchSummaries();
- if(vState.coverageManager != null) vState.coverageManager.addRecentEdges(id);
-
- //expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
- expansion = prover.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
- calls.id2VC.Add(id, expansion);
+ // Skipped calls don't get inlined
+ candidates = candidates.FindAll(id => !isSkipped(id, vState.calls));
- exprToPush = prover.VCExprGen.And(exprToPush, expansion);
- }
- vState.checker.prover.Assert(exprToPush, true);
- vState.vcSize += SizeComputingVisitor.ComputeSize(exprToPush);
- }
-
- private void SaveSubstitution(VerificationState vState, int id,
- Dictionary<VCExprVar, VCExpr> substForallDict, Dictionary<VCExprVar, VCExpr> substExistsDict) {
- var prover = vState.checker.prover;
- var calls = vState.calls;
- Boogie2VCExprTranslator translator = prover.Context.BoogieExprTranslator;
- VCExprVar mvStateConstant = translator.LookupVariable(ModelViewInfo.MVState_ConstantDef);
- substExistsDict.Add(mvStateConstant, prover.VCExprGen.Integer(BigNum.FromInt(id)));
- Dictionary<VCExprVar, VCExpr> mapping = new Dictionary<VCExprVar, VCExpr>();
- foreach (var key in substForallDict.Keys)
- mapping[key] = substForallDict[key];
- foreach (var key in substExistsDict.Keys)
- mapping[key] = substExistsDict[key];
- calls.id2Vars[id] = mapping;
- }
-
- // Return the VC for the impl (don't pass it to the theorem prover).
- // GetVC is a cheap imitation of VerifyImplementation, except that the VC is not passed to the theorem prover.
- private void GetVC(Implementation/*!*/ impl, Program/*!*/ program, ProverInterface prover, VerifierCallback/*!*/ callback, out VCExpr/*!*/ vc, out Hashtable/*<int, Absy!>*//*!*/ label2absy, out StratifiedInliningErrorReporter/*!*/ reporter)
- {
- Contract.Requires(impl != null);
- Contract.Requires(program != null);
- Contract.Requires(callback != null);
- Contract.Ensures(Contract.ValueAtReturn(out vc) != null);
- Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);
- Contract.Ensures(Contract.ValueAtReturn(out reporter) != null);
-
- ConvertCFG2DAG(impl);
- ModelViewInfo mvInfo;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
-
- var exprGen = prover.Context.ExprGen;
- VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
-
- vc = GenerateVC(impl, controlFlowVariableExpr, out label2absy, prover.Context);
-
- if (!CommandLineOptions.Clo.UseLabels) {
- VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO));
- VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
- vc = exprGen.Implies(eqExpr, vc);
- }
+ vState.expansionCount += candidates.Count;
- reporter = new StratifiedInliningErrorReporter(
- cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, gotoCmdOrigins, program, impl);
+ var prover = vState.checker.prover;
+ var calls = vState.calls;
+
+ VCExpr exprToPush = VCExpressionGenerator.True;
+ Contract.Assert(exprToPush != null);
+ foreach (int id in candidates) {
+ VCExprNAry expr = calls.id2Candidate[id];
+ Contract.Assert(expr != null);
+ string procName = cce.NonNull(expr.Op as VCExprBoogieFunctionOp).Func.Name;
+ if (!implName2StratifiedInliningInfo.ContainsKey(procName)) continue;
+
+ StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];
+ if (!info.initialized) {
+ info.GenerateVC();
+ }
+ //Console.WriteLine("Inlining {0}", procName);
+ VCExpr expansion = cce.NonNull(info.vcexpr);
+
+ // Instantiate the "forall" variables
+ Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();
+ Contract.Assert(info.interfaceExprVars.Count == expr.Length);
+ for (int i = 0; i < info.interfaceExprVars.Count; i++) {
+ substForallDict.Add(info.interfaceExprVars[i], expr[i]);
+ }
+ VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+
+ SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ Contract.Assert(subst != null);
+ expansion = subst.Mutate(expansion, substForall);
+
+ // Instantiate and declare the "exists" variables
+ Dictionary<VCExprVar, VCExpr> substExistsDict = new Dictionary<VCExprVar, VCExpr>();
+ foreach (VCExprVar v in info.privateExprVars) {
+ Contract.Assert(v != null);
+ string newName = v.Name + "_si_" + newVarCnt.ToString();
+ newVarCnt++;
+ prover.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, v.Type)), false, null);
+ substExistsDict.Add(v, prover.VCExprGen.Variable(newName, v.Type));
}
+ if (CommandLineOptions.Clo.ModelViewFile != null) {
+ SaveSubstitution(vState, id, substForallDict, substExistsDict);
+ }
+ VCExprSubstitution substExists = new VCExprSubstitution(substExistsDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());
+ subst = new SubstitutingVCExprVisitor(prover.VCExprGen);
+ expansion = subst.Mutate(expansion, substExists);
- // Uniquely identifies a procedure call (the call expr, instance)
- public class BoogieCallExpr : IEquatable<BoogieCallExpr>
- {
- public NAryExpr expr;
- public int inlineCnt;
+ if (!calls.currCandidates.Contains(id)) {
+ Console.WriteLine("Don't know what we just expanded");
+ }
- public BoogieCallExpr(NAryExpr expr, int inlineCnt)
- {
- this.expr = expr;
- this.inlineCnt = inlineCnt;
- }
+ calls.currCandidates.Remove(id);
- public override int GetHashCode()
- {
- return expr.GetHashCode() + 131 * inlineCnt.GetHashCode();
- }
+ // Record the new set of candidates and rename absy labels
+ calls.currInlineCount = id;
+ calls.setCurrProc(procName);
+ expansion = calls.Mutate(expansion, true);
+ if (useSummary) calls.matchSummaries();
+ if (vState.coverageManager != null) vState.coverageManager.addRecentEdges(id);
- public override bool Equals(object obj)
- {
- BoogieCallExpr that = obj as BoogieCallExpr;
- return (expr == that.expr && inlineCnt == that.inlineCnt);
- }
+ //expansion = checker.VCExprGen.Eq(calls.id2ControlVar[id], expansion);
+ expansion = prover.VCExprGen.Implies(calls.id2ControlVar[id], expansion);
+ calls.id2VC.Add(id, expansion);
- public bool Equals(BoogieCallExpr that)
- {
- return (expr == that.expr && inlineCnt == that.inlineCnt);
- }
- }
+ exprToPush = prover.VCExprGen.And(exprToPush, expansion);
+ }
+ vState.checker.prover.Assert(exprToPush, true);
+ vState.vcSize += SizeComputingVisitor.ComputeSize(exprToPush);
+ }
+
+ private void SaveSubstitution(VerificationState vState, int id,
+ Dictionary<VCExprVar, VCExpr> substForallDict, Dictionary<VCExprVar, VCExpr> substExistsDict) {
+ var prover = vState.checker.prover;
+ var calls = vState.calls;
+ Boogie2VCExprTranslator translator = prover.Context.BoogieExprTranslator;
+ VCExprVar mvStateConstant = translator.LookupVariable(ModelViewInfo.MVState_ConstantDef);
+ substExistsDict.Add(mvStateConstant, prover.VCExprGen.Integer(BigNum.FromInt(id)));
+ Dictionary<VCExprVar, VCExpr> mapping = new Dictionary<VCExprVar, VCExpr>();
+ foreach (var key in substForallDict.Keys)
+ mapping[key] = substForallDict[key];
+ foreach (var key in substExistsDict.Keys)
+ mapping[key] = substExistsDict[key];
+ calls.id2Vars[id] = mapping;
+ }
+
+ // Uniquely identifies a procedure call (the call expr, instance)
+ public class BoogieCallExpr : IEquatable<BoogieCallExpr> {
+ public NAryExpr expr;
+ public int inlineCnt;
+
+ public BoogieCallExpr(NAryExpr expr, int inlineCnt) {
+ this.expr = expr;
+ this.inlineCnt = inlineCnt;
+ }
- // This class is used to traverse VCs and do the following:
- // -- collect the set of FunctionCall nodes and label them with a unique string
- // -- Rename all other labels (so that calling this on the same VC results in
- // VCs with different labels each time)
- public class FCallHandler : MutatingVCExprVisitor<bool>
- {
- Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
- public readonly Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy;
- public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;
- public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
- public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
- public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;
- public Dictionary<int, VCExpr> id2VC;
- public Dictionary<string/*!*/, int>/*!*/ label2Id;
- // Stores the candidate from which this one originated
- public Dictionary<int, int> candidateParent;
- // Mapping from candidate Id to the "si_unique_call" id that led to
- // this candidate. This is useful for getting persistent names for
- // candidates
- public Dictionary<int, int> candidate2callId;
- // A cache for candidate id to its persistent name
- public Dictionary<int, string> persistentNameCache;
- // Inverse of the above map
- public Dictionary<string, int> persistentNameInv;
- // Used to record candidates recently added
- public HashSet<int> recentlyAddedCandidates;
- // Name of main procedure
- private string mainProcName;
- // A map from candidate id to the VCExpr that represents its
- // first argument (used for obtaining concrete values in error trace)
- public Dictionary<int, VCExpr> argExprMap;
-
- // map from candidate to summary candidates
- public Dictionary<int, List<Tuple<VCExprVar, VCExpr>>> summaryCandidates;
- private Dictionary<string, List<Tuple<VCExprVar, VCExpr>>> summaryTemp;
- // set of all boolean guards of summaries
- public HashSet<VCExprVar> allSummaryConst;
-
- public HashSet<int> forcedCandidates;
-
- // User info -- to decrease/increase calculation of recursion bound
- public Dictionary<int, int> recursionIncrement;
-
- public HashSet<int> currCandidates;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Invariant(mainLabel2absy != null);
- Contract.Invariant(boogieExpr2Id != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(id2Candidate));
- Contract.Invariant(cce.NonNullDictionaryAndValues(id2ControlVar));
- Contract.Invariant(label2Id != null);
- }
+ public override int GetHashCode() {
+ return expr.GetHashCode() + 131 * inlineCnt.GetHashCode();
+ }
- // Name of the procedure whose VC we're mutating
- string currProc;
-
- // The 0^th candidate is main
- static int candidateCount = 1;
- public int currInlineCount;
-
- public Dictionary<int, Dictionary<VCExprVar, VCExpr>> id2Vars;
-
- public FCallHandler(VCExpressionGenerator/*!*/ gen,
- Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
- string mainProcName, Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy)
- : base(gen)
- {
- Contract.Requires(gen != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Requires(mainLabel2absy != null);
- this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
- this.mainProcName = mainProcName;
- this.mainLabel2absy = mainLabel2absy;
- id2Candidate = new Dictionary<int, VCExprNAry>();
- id2ControlVar = new Dictionary<int, VCExprVar>();
- boogieExpr2Id = new Dictionary<BoogieCallExpr, int>();
- label2Id = new Dictionary<string, int>();
- currCandidates = new HashSet<int>();
- currInlineCount = 0;
- currProc = null;
- labelRenamer = new Dictionary<string, int>();
- labelRenamerInv = new Dictionary<string, string>();
- candidateParent = new Dictionary<int, int>();
- //callGraphMapping = new Dictionary<int, int>();
- recursionIncrement = new Dictionary<int, int>();
- candidate2callId = new Dictionary<int, int>();
- persistentNameCache = new Dictionary<int, string>();
- persistentNameInv = new Dictionary<string, int>();
- persistentNameCache[0] = "0";
- persistentNameInv["0"] = 0;
- recentlyAddedCandidates = new HashSet<int>();
- argExprMap = new Dictionary<int, VCExpr>();
- recordExpr2Var = new Dictionary<BoogieCallExpr, VCExpr>();
-
- forcedCandidates = new HashSet<int>();
-
- id2Vars = new Dictionary<int, Dictionary<VCExprVar, VCExpr>>();
- summaryCandidates = new Dictionary<int, List<Tuple<VCExprVar, VCExpr>>>();
- summaryTemp = new Dictionary<string, List<Tuple<VCExprVar, VCExpr>>>();
- allSummaryConst = new HashSet<VCExprVar>();
- id2VC = new Dictionary<int, VCExpr>();
- }
+ public override bool Equals(object obj) {
+ BoogieCallExpr that = obj as BoogieCallExpr;
+ return (expr == that.expr && inlineCnt == that.inlineCnt);
+ }
- public void Clear()
- {
- currCandidates = new HashSet<int>();
- }
+ public bool Equals(BoogieCallExpr that) {
+ return (expr == that.expr && inlineCnt == that.inlineCnt);
+ }
+ }
+
+ // This class is used to traverse VCs and do the following:
+ // -- collect the set of FunctionCall nodes and label them with a unique string
+ // -- Rename all other labels (so that calling this on the same VC results in
+ // VCs with different labels each time)
+ public class FCallHandler : MutatingVCExprVisitor<bool> {
+ Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
+ public readonly Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy;
+ public Dictionary<BoogieCallExpr/*!*/, int>/*!*/ boogieExpr2Id;
+ public Dictionary<BoogieCallExpr/*!*/, VCExpr>/*!*/ recordExpr2Var;
+ public Dictionary<int, VCExprNAry/*!*/>/*!*/ id2Candidate;
+ public Dictionary<int, VCExprVar/*!*/>/*!*/ id2ControlVar;
+ public Dictionary<int, VCExpr> id2VC;
+ public Dictionary<string/*!*/, int>/*!*/ label2Id;
+ // Stores the candidate from which this one originated
+ public Dictionary<int, int> candidateParent;
+ // Mapping from candidate Id to the "si_unique_call" id that led to
+ // this candidate. This is useful for getting persistent names for
+ // candidates
+ public Dictionary<int, int> candidate2callId;
+ // A cache for candidate id to its persistent name
+ public Dictionary<int, string> persistentNameCache;
+ // Inverse of the above map
+ public Dictionary<string, int> persistentNameInv;
+ // Used to record candidates recently added
+ public HashSet<int> recentlyAddedCandidates;
+ // Name of main procedure
+ private string mainProcName;
+ // A map from candidate id to the VCExpr that represents its
+ // first argument (used for obtaining concrete values in error trace)
+ public Dictionary<int, VCExpr> argExprMap;
+
+ // map from candidate to summary candidates
+ public Dictionary<int, List<Tuple<VCExprVar, VCExpr>>> summaryCandidates;
+ private Dictionary<string, List<Tuple<VCExprVar, VCExpr>>> summaryTemp;
+ // set of all boolean guards of summaries
+ public HashSet<VCExprVar> allSummaryConst;
+
+ public HashSet<int> forcedCandidates;
+
+ // User info -- to decrease/increase calculation of recursion bound
+ public Dictionary<int, int> recursionIncrement;
+ public Dictionary<string, int> extraRecursion;
+
+ public HashSet<int> currCandidates;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Invariant(mainLabel2absy != null);
+ Contract.Invariant(boogieExpr2Id != null);
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2Candidate));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(id2ControlVar));
+ Contract.Invariant(label2Id != null);
+ }
- // Return the set of all candidates
- public HashSet<int> getAllCandidates()
- {
- var ret = new HashSet<int>(candidateParent.Keys);
- ret.Add(0);
- return ret;
- }
+ // Name of the procedure whose VC we're mutating
+ string currProc;
+
+ // The 0^th candidate is main
+ static int candidateCount = 1;
+ public int currInlineCount;
+
+ public Dictionary<int, Dictionary<VCExprVar, VCExpr>> id2Vars;
+
+ public FCallHandler(VCExpressionGenerator/*!*/ gen,
+ Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
+ string mainProcName, Hashtable/*<int, Absy!>*//*!*/ mainLabel2absy)
+ : base(gen) {
+ Contract.Requires(gen != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Requires(mainLabel2absy != null);
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.mainProcName = mainProcName;
+ this.mainLabel2absy = mainLabel2absy;
+ id2Candidate = new Dictionary<int, VCExprNAry>();
+ id2ControlVar = new Dictionary<int, VCExprVar>();
+ boogieExpr2Id = new Dictionary<BoogieCallExpr, int>();
+ label2Id = new Dictionary<string, int>();
+ currCandidates = new HashSet<int>();
+ currInlineCount = 0;
+ currProc = null;
+ labelRenamer = new Dictionary<string, int>();
+ labelRenamerInv = new Dictionary<string, string>();
+ candidateParent = new Dictionary<int, int>();
+ //callGraphMapping = new Dictionary<int, int>();
+ recursionIncrement = new Dictionary<int, int>();
+ candidate2callId = new Dictionary<int, int>();
+ persistentNameCache = new Dictionary<int, string>();
+ persistentNameInv = new Dictionary<string, int>();
+ persistentNameCache[0] = "0";
+ persistentNameInv["0"] = 0;
+ recentlyAddedCandidates = new HashSet<int>();
+ argExprMap = new Dictionary<int, VCExpr>();
+ recordExpr2Var = new Dictionary<BoogieCallExpr, VCExpr>();
+
+ forcedCandidates = new HashSet<int>();
+ extraRecursion = new Dictionary<string, int>();
+
+ id2Vars = new Dictionary<int, Dictionary<VCExprVar, VCExpr>>();
+ summaryCandidates = new Dictionary<int, List<Tuple<VCExprVar, VCExpr>>>();
+ summaryTemp = new Dictionary<string, List<Tuple<VCExprVar, VCExpr>>>();
+ allSummaryConst = new HashSet<VCExprVar>();
+ id2VC = new Dictionary<int, VCExpr>();
+ }
- // Given a candidate "id", let proc(id) be the
- // procedure corresponding to id. This procedure returns
- // the number of times proc(id) appears as an ancestor
- // of id. This is the same as the number of times we've
- // recursed on proc(id)
- public int getRecursionBound(int id)
- {
- int ret = 1;
- var str = getProc(id);
-
- while (candidateParent.ContainsKey(id))
- {
- if (recursionIncrement.ContainsKey(id)) ret += recursionIncrement[id];
- id = candidateParent[id];
- if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;
- }
- return ret;
- }
+ public void Clear() {
+ currCandidates = new HashSet<int>();
+ }
- // Set user-define increment/decrement to recursionBound
- public void setRecursionIncrement(int id, int incr)
- {
- if (recursionIncrement.ContainsKey(id))
- recursionIncrement[id] = incr;
- else
- recursionIncrement.Add(id, incr);
- }
+ // Return the set of all candidates
+ public HashSet<int> getAllCandidates() {
+ var ret = new HashSet<int>(candidateParent.Keys);
+ ret.Add(0);
+ return ret;
+ }
- // Returns the name of the procedure corresponding to candidate id
- public string getProc(int id)
- {
- if (id == 0) return mainProcName;
+ // Given a candidate "id", let proc(id) be the
+ // procedure corresponding to id. This procedure returns
+ // the number of times proc(id) appears as an ancestor
+ // of id. This is the same as the number of times we've
+ // recursed on proc(id)
+ public int getRecursionBound(int id) {
+ int ret = 1;
+ var str = getProc(id);
+
+ while (candidateParent.ContainsKey(id)) {
+ if (recursionIncrement.ContainsKey(id)) ret += recursionIncrement[id];
+ id = candidateParent[id];
+ if (getProc(id) == str && !forcedCandidates.Contains(id)) ret++;
+ }
- return (id2Candidate[id].Op as VCExprBoogieFunctionOp).Func.Name;
- }
+ if (extraRecursion.ContainsKey(str)) ret -= extraRecursion[str];
- // Get a unique id for this candidate (dependent only on the Call
- // graph of the program). The persistent id is:
- // 0: for main
- // a_b_c: where a is the persistent id of parent, and b is the procedure name
- // and c is the unique call id (if any)
- public string getPersistentId(int top_id)
- {
- if (top_id == 0) return "0";
- Debug.Assert(candidateParent.ContainsKey(top_id));
- if (persistentNameCache.ContainsKey(top_id))
- return persistentNameCache[top_id];
-
- var parent_id = getPersistentId(candidateParent[top_id]);
- var call_id = candidate2callId.ContainsKey(top_id) ? candidate2callId[top_id] : -1;
- var ret = string.Format("{0}_131_{1}_131_{2}", parent_id, getProc(top_id), call_id);
- persistentNameCache[top_id] = ret;
- persistentNameInv[ret] = top_id;
- return ret;
- }
+ return ret;
+ }
- public int getCandidateFromGraphNode(string n)
- {
- if (!persistentNameInv.ContainsKey(n))
- {
- return -1;
- }
- return persistentNameInv[n];
- }
+ // Set user-define increment/decrement to recursionBound
+ public void setRecursionIncrement(int id, int incr) {
+ if (recursionIncrement.ContainsKey(id))
+ recursionIncrement[id] = incr;
+ else
+ recursionIncrement.Add(id, incr);
+ }
- private int GetNewId(VCExprNAry vc)
- {
- Contract.Requires(vc != null);
- int id = candidateCount;
+ // Returns the name of the procedure corresponding to candidate id
+ public string getProc(int id) {
+ if (id == 0) return mainProcName;
- id2Candidate[id] = vc;
- id2ControlVar[id] = Gen.Variable("si_control_var_bool_" + id.ToString(), Microsoft.Boogie.Type.Bool);
+ return (id2Candidate[id].Op as VCExprBoogieFunctionOp).Func.Name;
+ }
- candidateCount++;
- currCandidates.Add(id);
- recentlyAddedCandidates.Add(id);
+ // Get a unique id for this candidate (dependent only on the Call
+ // graph of the program). The persistent id is:
+ // 0: for main
+ // a_b_c: where a is the persistent id of parent, and b is the procedure name
+ // and c is the unique call id (if any)
+ public string getPersistentId(int top_id) {
+ if (top_id == 0) return "0";
+ Debug.Assert(candidateParent.ContainsKey(top_id));
+ if (persistentNameCache.ContainsKey(top_id))
+ return persistentNameCache[top_id];
+
+ var parent_id = getPersistentId(candidateParent[top_id]);
+ var call_id = candidate2callId.ContainsKey(top_id) ? candidate2callId[top_id] : -1;
+ var ret = string.Format("{0}_131_{1}_131_{2}", parent_id, getProc(top_id), call_id);
+ persistentNameCache[top_id] = ret;
+ persistentNameInv[ret] = top_id;
+ return ret;
+ }
- return id;
- }
+ public int getCandidateFromGraphNode(string n) {
+ if (!persistentNameInv.ContainsKey(n)) {
+ return -1;
+ }
+ return persistentNameInv[n];
+ }
- private string GetLabel(int id)
- {
- Contract.Ensures(Contract.Result<string>() != null);
+ private int GetNewId(VCExprNAry vc) {
+ Contract.Requires(vc != null);
+ int id = candidateCount;
- string ret = "si_fcall_" + id.ToString();
- if (!label2Id.ContainsKey(ret))
- label2Id[ret] = id;
+ id2Candidate[id] = vc;
+ id2ControlVar[id] = Gen.Variable("si_control_var_bool_" + id.ToString(), Microsoft.Boogie.Type.Bool);
- return ret;
- }
+ candidateCount++;
+ currCandidates.Add(id);
+ recentlyAddedCandidates.Add(id);
- public int GetId(string label)
- {
- Contract.Requires(label != null);
- if (!label2Id.ContainsKey(label))
- return -1;
- return label2Id[label];
- }
+ return id;
+ }
- Dictionary<string, int> labelRenamer;
- Dictionary<string, string> labelRenamerInv;
+ private string GetLabel(int id) {
+ Contract.Ensures(Contract.Result<string>() != null);
- public string RenameAbsyLabel(string label)
- {
- Contract.Requires(label != null);
- Contract.Requires(label.Length >= 1);
- Contract.Ensures(Contract.Result<string>() != null);
+ string ret = "si_fcall_" + id.ToString();
+ if (!label2Id.ContainsKey(ret))
+ label2Id[ret] = id;
- // Remove the sign from the label
- string nosign = label.Substring(1);
- var ret = "si_inline_" + currInlineCount.ToString() + "_" + nosign;
+ return ret;
+ }
- if (!labelRenamer.ContainsKey(ret))
- {
- var c = labelRenamer.Count + 11; // two digit labels only
- labelRenamer.Add(ret, c);
- labelRenamerInv.Add(c.ToString(), ret);
- }
- return labelRenamer[ret].ToString();
- }
+ public int GetId(string label) {
+ Contract.Requires(label != null);
+ if (!label2Id.ContainsKey(label))
+ return -1;
+ return label2Id[label];
+ }
- public string ParseRenamedAbsyLabel(string label, int cnt)
- {
- Contract.Requires(label != null);
- if (!labelRenamerInv.ContainsKey(label))
- {
- return null;
- }
- var str = labelRenamerInv[label];
- var prefix = "si_inline_" + cnt.ToString() + "_";
- if (!str.StartsWith(prefix)) return null;
- return str.Substring(prefix.Length);
- }
+ Dictionary<string, int> labelRenamer;
+ Dictionary<string, string> labelRenamerInv;
- public void setCurrProc(string name)
- {
- Contract.Requires(name != null);
- currProc = name;
- Contract.Assert(implName2StratifiedInliningInfo.ContainsKey(name));
- }
+ public string RenameAbsyLabel(string label) {
+ Contract.Requires(label != null);
+ Contract.Requires(label.Length >= 1);
+ Contract.Ensures(Contract.Result<string>() != null);
- public void setCurrProcAsMain()
- {
- currProc = "";
- }
+ // Remove the sign from the label
+ string nosign = label.Substring(1);
+ var ret = "si_inline_" + currInlineCount.ToString() + "_" + nosign;
- // Return the formula (candidate IFF false)
- public VCExpr getFalseExpr(int candidateId)
- {
- //return Gen.Eq(VCExpressionGenerator.False, id2ControlVar[candidateId]);
- return Gen.Not(id2ControlVar[candidateId]);
- }
+ if (!labelRenamer.ContainsKey(ret)) {
+ var c = labelRenamer.Count + 11; // two digit labels only
+ labelRenamer.Add(ret, c);
+ labelRenamerInv.Add(c.ToString(), ret);
+ }
+ return labelRenamer[ret].ToString();
+ }
- // Return the formula (candidate IFF true)
- public VCExpr getTrueExpr(int candidateId)
- {
- return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);
- }
+ public string ParseRenamedAbsyLabel(string label, int cnt) {
+ Contract.Requires(label != null);
+ if (!labelRenamerInv.ContainsKey(label)) {
+ return null;
+ }
+ var str = labelRenamerInv[label];
+ var prefix = "si_inline_" + cnt.ToString() + "_";
+ if (!str.StartsWith(prefix)) return null;
+ return str.Substring(prefix.Length);
+ }
- public Hashtable/*<int,absy>*/ getLabel2absy()
- {
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ public void setCurrProc(string name) {
+ Contract.Requires(name != null);
+ currProc = name;
+ Contract.Assert(implName2StratifiedInliningInfo.ContainsKey(name));
+ }
- Contract.Assert(currProc != null);
- if (currProc == "")
- {
- return mainLabel2absy;
- }
- return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);
- }
+ public void setCurrProcAsMain() {
+ currProc = "";
+ }
- // Is this candidate a "skipped" call
- // Currently this is experimental
- public bool isSkipped(int id)
- {
- if (!CommandLineOptions.Clo.BctModeForStratifiedInlining) return false;
-
- var proc = getProc(id);
- if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;
- var modSet = new HashSet<string>();
- implName2StratifiedInliningInfo[proc].impl.Proc.Modifies
- .Cast<IdentifierExpr>()
- .Select(ie => ie.Decl.Name)
- .Iter(s => modSet.Add(s));
- modSet.Remove("$Alloc");
- modSet.Remove("assertsPassed");
- modSet.Remove("$Exception");
- return modSet.Count == 0;
- }
+ // Return the formula (candidate IFF false)
+ public VCExpr getFalseExpr(int candidateId) {
+ //return Gen.Eq(VCExpressionGenerator.False, id2ControlVar[candidateId]);
+ return Gen.Not(id2ControlVar[candidateId]);
+ }
- // Finds labels and changes them:
- // si_fcall_id: if "id" corresponds to a tracked procedure call, then
- // si_control_var_candidateId
- // si_fcall_id: if "id" does not corresponds to a tracked procedure call, then
- // delete
- // num: si_inline_num
- //
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg)
- {
- //Contract.Requires(originalNode != null);
- //Contract.Requires(cce.NonNullElements(newSubExprs));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
- if (lop == null) return ret;
- if (!(ret is VCExprNAry)) return ret;
-
- VCExprNAry retnary = (VCExprNAry)ret;
- Contract.Assert(retnary != null);
- string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
- if (lop.label.Substring(1).StartsWith(prefix))
- {
- int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
- Hashtable label2absy = getLabel2absy();
- Absy cmd = label2absy[id] as Absy;
- //label2absy.Remove(id);
-
- Contract.Assert(cmd != null);
- AssumeCmd acmd = cmd as AssumeCmd;
- Contract.Assert(acmd != null);
- NAryExpr naryExpr = acmd.Expr as NAryExpr;
- Contract.Assert(naryExpr != null);
-
- string calleeName = naryExpr.Fun.FunctionName;
-
- VCExprNAry callExpr = retnary[0] as VCExprNAry;
- Contract.Assert(callExpr != null);
-
- if (implName2StratifiedInliningInfo.ContainsKey(calleeName))
- {
- int candidateId = GetNewId(callExpr);
- boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;
- candidateParent[candidateId] = currInlineCount;
- string label = GetLabel(candidateId);
- var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1);
- if (unique_call_id != -1)
- candidate2callId[candidateId] = unique_call_id;
-
- //return Gen.LabelPos(label, callExpr);
- return Gen.LabelPos(label, id2ControlVar[candidateId]);
- }
- else if (calleeName.StartsWith(recordProcName))
- {
- Debug.Assert(callExpr.Length == 1);
- Debug.Assert(callExpr[0] != null);
- recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0];
- return callExpr;
- }
- else
- {
- return callExpr;
- }
- }
+ // Return the formula (candidate IFF true)
+ public VCExpr getTrueExpr(int candidateId) {
+ return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]);
+ }
- // summary candidate
- if (lop.label.Substring(1).StartsWith("candidate_"))
- {
- var pname = lop.label.Substring("candidate_".Length + 1);
-
- if (!summaryTemp.ContainsKey(pname))
- summaryTemp.Add(pname, new List<Tuple<VCExprVar, VCExpr>>());
-
- var expr = retnary[0] as VCExprNAry;
- if (expr == null) return retnary[0];
- if (expr.Op != VCExpressionGenerator.ImpliesOp) return retnary[0];
- var tup = Tuple.Create(expr[0] as VCExprVar, expr[1]);
- summaryTemp[pname].Add(tup);
-
- return retnary[0];
- }
+ public Hashtable/*<int,absy>*/ getLabel2absy() {
+ Contract.Ensures(Contract.Result<Hashtable>() != null);
- // Else, rename label
- string newLabel = RenameAbsyLabel(lop.label);
- if (lop.pos)
- {
- return Gen.LabelPos(newLabel, retnary[0]);
- }
- else
- {
- return Gen.LabelNeg(newLabel, retnary[0]);
- }
+ Contract.Assert(currProc != null);
+ if (currProc == "") {
+ return mainLabel2absy;
+ }
+ return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);
+ }
- }
+ // Finds labels and changes them:
+ // si_fcall_id: if "id" corresponds to a tracked procedure call, then
+ // si_control_var_candidateId
+ // si_fcall_id: if "id" does not corresponds to a tracked procedure call, then
+ // delete
+ // num: si_inline_num
+ //
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg) {
+ //Contract.Requires(originalNode != null);
+ //Contract.Requires(cce.NonNullElements(newSubExprs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
+ if (lop == null) return ret;
+ if (!(ret is VCExprNAry)) return ret;
+
+ VCExprNAry retnary = (VCExprNAry)ret;
+ Contract.Assert(retnary != null);
+ string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...)
+ if (lop.label.Substring(1).StartsWith(prefix)) {
+ int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
+ Hashtable label2absy = getLabel2absy();
+ Absy cmd = label2absy[id] as Absy;
+ //label2absy.Remove(id);
+
+ Contract.Assert(cmd != null);
+ AssumeCmd acmd = cmd as AssumeCmd;
+ Contract.Assert(acmd != null);
+ NAryExpr naryExpr = acmd.Expr as NAryExpr;
+ Contract.Assert(naryExpr != null);
+
+ string calleeName = naryExpr.Fun.FunctionName;
+
+ VCExprNAry callExpr = retnary[0] as VCExprNAry;
+ Contract.Assert(callExpr != null);
+
+ if (implName2StratifiedInliningInfo.ContainsKey(calleeName)) {
+ int candidateId = GetNewId(callExpr);
+ boogieExpr2Id[new BoogieCallExpr(naryExpr, currInlineCount)] = candidateId;
+ candidateParent[candidateId] = currInlineCount;
+ string label = GetLabel(candidateId);
+ var unique_call_id = QKeyValue.FindIntAttribute(acmd.Attributes, "si_unique_call", -1);
+ if (unique_call_id != -1)
+ candidate2callId[candidateId] = unique_call_id;
+
+ //return Gen.LabelPos(label, callExpr);
+ return Gen.LabelPos(label, id2ControlVar[candidateId]);
+ }
+ else if (calleeName.StartsWith(recordProcName)) {
+ Debug.Assert(callExpr.Length == 1);
+ Debug.Assert(callExpr[0] != null);
+ recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0];
+ return callExpr;
+ }
+ else {
+ return callExpr;
+ }
+ }
- // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with
- // the appropriate candidate they came from
- public void matchSummaries()
- {
- var id2Set = new Dictionary<string, List<Tuple<int, HashSet<VCExprVar>>>>();
- foreach (var id in recentlyAddedCandidates)
- {
- var collect = new CollectVCVars();
- var proc = getProc(id);
- if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List<Tuple<int, HashSet<VCExprVar>>>());
- id2Set[proc].Add(Tuple.Create(id, collect.Collect(id2Candidate[id], true)));
- }
-
- foreach (var kvp in summaryTemp)
- {
- Contract.Assert (id2Set.ContainsKey(kvp.Key));
- var ls = id2Set[kvp.Key];
- foreach (var tup in kvp.Value)
- {
- var collect = new CollectVCVars();
- var s1 = collect.Collect(tup.Item2, true);
- var found = false;
- foreach (var t in ls)
- {
- var s2 = t.Item2;
- if (s1.IsSubsetOf(s2))
- {
- if (!summaryCandidates.ContainsKey(t.Item1))
- summaryCandidates.Add(t.Item1, new List<Tuple<VCExprVar, VCExpr>>());
- summaryCandidates[t.Item1].Add(tup);
- allSummaryConst.Add(tup.Item1);
- found = true;
- break;
- }
- }
- Contract.Assert(found);
- }
- }
- summaryTemp.Clear();
- }
+ // summary candidate
+ if (lop.label.Substring(1).StartsWith("candidate_")) {
+ var pname = lop.label.Substring("candidate_".Length + 1);
- public IEnumerable<int> getInlinedCandidates() {
- return candidateParent.Keys.Except(currCandidates).Union(new int[] { 0 });
- }
+ if (!summaryTemp.ContainsKey(pname))
+ summaryTemp.Add(pname, new List<Tuple<VCExprVar, VCExpr>>());
- } // end FCallHandler
+ var expr = retnary[0] as VCExprNAry;
+ if (expr == null) return retnary[0];
+ if (expr.Op != VCExpressionGenerator.ImpliesOp) return retnary[0];
+ var tup = Tuple.Create(expr[0] as VCExprVar, expr[1]);
+ summaryTemp[pname].Add(tup);
- // Collects the set of all VCExprVar in a given VCExpr
- class CollectVCVars : CollectingVCExprVisitor<HashSet<VCExprVar>, bool>
- {
- public override HashSet<VCExprVar> Visit(VCExprVar node, bool arg)
- {
- var ret = new HashSet<VCExprVar>();
- ret.Add(node);
- return ret;
- }
+ return retnary[0];
+ }
- protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg)
- {
- var ret = new HashSet<VCExprVar>();
- results.ForEach(s => ret.UnionWith(s));
- return ret;
- }
+ // Else, rename label
+ string newLabel = RenameAbsyLabel(lop.label);
+ if (lop.pos) {
+ return Gen.LabelPos(newLabel, retnary[0]);
+ }
+ else {
+ return Gen.LabelNeg(newLabel, retnary[0]);
}
- public class FCallInliner : MutatingVCExprVisitor<bool>
- {
- public Dictionary<int, VCExpr/*!*/>/*!*/ subst;
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
- }
+ }
+ // Upgrades summaryTemp to summaryCandidates by matching ensure clauses with
+ // the appropriate candidate they came from
+ public void matchSummaries() {
+ var id2Set = new Dictionary<string, List<Tuple<int, HashSet<VCExprVar>>>>();
+ foreach (var id in recentlyAddedCandidates) {
+ var collect = new CollectVCVars();
+ var proc = getProc(id);
+ if (!id2Set.ContainsKey(proc)) id2Set.Add(proc, new List<Tuple<int, HashSet<VCExprVar>>>());
+ id2Set[proc].Add(Tuple.Create(id, collect.Collect(id2Candidate[id], true)));
+ }
- public FCallInliner(VCExpressionGenerator gen)
- : base(gen)
- {
- Contract.Requires(gen != null);
- subst = new Dictionary<int, VCExpr>();
+ foreach (var kvp in summaryTemp) {
+ Contract.Assert(id2Set.ContainsKey(kvp.Key));
+ var ls = id2Set[kvp.Key];
+ foreach (var tup in kvp.Value) {
+ var collect = new CollectVCVars();
+ var s1 = collect.Collect(tup.Item2, true);
+ var found = false;
+ foreach (var t in ls) {
+ var s2 = t.Item2;
+ if (s1.IsSubsetOf(s2)) {
+ if (!summaryCandidates.ContainsKey(t.Item1))
+ summaryCandidates.Add(t.Item1, new List<Tuple<VCExprVar, VCExpr>>());
+ summaryCandidates[t.Item1].Add(tup);
+ allSummaryConst.Add(tup.Item1);
+ found = true;
+ break;
+ }
}
+ Contract.Assert(found);
+ }
+ }
+ summaryTemp.Clear();
+ }
- public void Clear()
- {
- subst = new Dictionary<int, VCExpr>();
- }
+ public IEnumerable<int> getInlinedCandidates() {
+ return candidateParent.Keys.Except(currCandidates).Union(new int[] { 0 });
+ }
- protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
- List<VCExpr/*!*/>/*!*/ newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- bool arg)
- {
- //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExpr ret;
- if (changed)
- ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments);
- else
- ret = originalNode;
-
- VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
- if (lop == null) return ret;
- if (!(ret is VCExprNAry)) return ret;
-
- string prefix = "si_fcall_"; // from FCallHandler::GetLabel
- if (lop.label.Substring(1).StartsWith(prefix))
- {
- int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
- if (subst.ContainsKey(id))
- {
- return subst[id];
- }
- }
- return ret;
- }
+ } // end FCallHandler
+
+ // Collects the set of all VCExprVar in a given VCExpr
+ class CollectVCVars : CollectingVCExprVisitor<HashSet<VCExprVar>, bool> {
+ public override HashSet<VCExprVar> Visit(VCExprVar node, bool arg) {
+ var ret = new HashSet<VCExprVar>();
+ ret.Add(node);
+ return ret;
+ }
- } // end FCallInliner
+ protected override HashSet<VCExprVar> CombineResults(List<HashSet<VCExprVar>> results, bool arg) {
+ var ret = new HashSet<VCExprVar>();
+ results.ForEach(s => ret.UnionWith(s));
+ return ret;
+ }
+ }
- public class EmptyErrorHandler : ProverInterface.ErrorHandler
- {
- public override void OnModel(IList<string> labels, Model model)
- {
-
- }
+ public class FCallInliner : MutatingVCExprVisitor<bool> {
+ public Dictionary<int, VCExpr/*!*/>/*!*/ subst;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(subst));
+ }
+
+
+ public FCallInliner(VCExpressionGenerator gen)
+ : base(gen) {
+ Contract.Requires(gen != null);
+ subst = new Dictionary<int, VCExpr>();
+ }
+
+ public void Clear() {
+ subst = new Dictionary<int, VCExpr>();
+ }
+
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,
+ List<VCExpr/*!*/>/*!*/ newSubExprs,
+ // has any of the subexpressions changed?
+ bool changed,
+ bool arg) {
+ //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ VCExpr ret;
+ if (changed)
+ ret = Gen.Function(originalNode.Op, newSubExprs, originalNode.TypeArguments);
+ else
+ ret = originalNode;
+
+ VCExprLabelOp lop = originalNode.Op as VCExprLabelOp;
+ if (lop == null) return ret;
+ if (!(ret is VCExprNAry)) return ret;
+
+ string prefix = "si_fcall_"; // from FCallHandler::GetLabel
+ if (lop.label.Substring(1).StartsWith(prefix)) {
+ int id = Int32.Parse(lop.label.Substring(prefix.Length + 1));
+ if (subst.ContainsKey(id)) {
+ return subst[id];
+ }
}
+ return ret;
+ }
- public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler
- {
- Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo;
- ProverInterface/*!*/ theoremProver;
- VerifierCallback/*!*/ callback;
- ModelViewInfo mvInfo;
- FCallHandler calls;
- Program/*!*/ program;
- Implementation/*!*/ mainImpl;
- ProverContext/*!*/ context;
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;
-
- public bool underapproximationMode;
- public List<int>/*!*/ candidatesToExpand;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(candidatesToExpand != null);
- Contract.Invariant(context != null);
- Contract.Invariant(mainImpl != null);
- Contract.Invariant(program != null);
- Contract.Invariant(callback != null);
- Contract.Invariant(theoremProver != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- }
+ } // end FCallInliner
+ public class EmptyErrorHandler : ProverInterface.ErrorHandler {
+ public override void OnModel(IList<string> labels, Model model) {
- public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,
- ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ModelViewInfo mvInfo, ProverContext/*!*/ context,
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,
- Program/*!*/ program, Implementation/*!*/ mainImpl)
- {
- Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
- Contract.Requires(theoremProver != null);
- Contract.Requires(callback != null);
- Contract.Requires(context != null);
- Contract.Requires(mainImpl != null);
- this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
- this.theoremProver = theoremProver;
- this.callback = callback;
- this.mvInfo = mvInfo;
- this.context = context;
- this.program = program;
- this.mainImpl = mainImpl;
- this.underapproximationMode = false;
- this.calls = null;
- this.candidatesToExpand = new List<int>();
- this.gotoCmdOrigins = gotoCmdOrigins;
- }
+ }
+ }
+
+ public class StratifiedInliningErrorReporter : ProverInterface.ErrorHandler {
+ Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;
+ ProverInterface theoremProver;
+ VerifierCallback callback;
+ FCallHandler calls;
+ StratifiedInliningInfo mainInfo;
+ StratifiedVC mainVC;
+
+ public bool underapproximationMode;
+ public List<int> candidatesToExpand;
+ public List<StratifiedCallSite> callSitesToExpand;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(candidatesToExpand != null);
+ Contract.Invariant(mainInfo != null);
+ Contract.Invariant(callback != null);
+ Contract.Invariant(theoremProver != null);
+ Contract.Invariant(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ }
- public void SetCandidateHandler(FCallHandler calls)
- {
- Contract.Requires(calls != null);
- this.calls = calls;
- }
- List<Tuple<int, int>> orderedStateIds;
+ public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,
+ ProverInterface theoremProver, VerifierCallback callback,
+ StratifiedInliningInfo mainInfo) {
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Requires(theoremProver != null);
+ Contract.Requires(callback != null);
+ Contract.Requires(mainInfo != null);
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.theoremProver = theoremProver;
+ this.callback = callback;
+ this.mainInfo = mainInfo;
+ this.underapproximationMode = false;
+ this.calls = null;
+ this.candidatesToExpand = new List<int>();
+ }
- private Model.Element GetModelValue(Model m, Variable v, int candidateId) {
- // first, get the unique name
- string uniqueName;
+ public StratifiedInliningErrorReporter(Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo,
+ ProverInterface theoremProver, VerifierCallback callback,
+ StratifiedVC mainVC) {
+ Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));
+ Contract.Requires(theoremProver != null);
+ Contract.Requires(callback != null);
+ Contract.Requires(mainVC != null);
+ this.implName2StratifiedInliningInfo = implName2StratifiedInliningInfo;
+ this.theoremProver = theoremProver;
+ this.callback = callback;
+ this.mainVC = mainVC;
+ this.underapproximationMode = false;
+ this.candidatesToExpand = new List<int>();
+ }
- VCExprVar vvar = context.BoogieExprTranslator.TryLookupVariable(v);
- if (vvar == null) {
- uniqueName = v.Name;
- }
- else {
- if (candidateId != 0) {
- Dictionary<VCExprVar, VCExpr> mapping = calls.id2Vars[candidateId];
- if (mapping.ContainsKey(vvar)) {
- VCExpr e = mapping[vvar];
- if (e is VCExprLiteral) {
- VCExprLiteral lit = (VCExprLiteral)e;
- return m.MkElement(lit.ToString());
- }
- vvar = (VCExprVar)mapping[vvar];
- }
- }
- uniqueName = context.Lookup(vvar);
- }
+ public void SetCandidateHandler(FCallHandler calls) {
+ Contract.Requires(calls != null);
+ this.calls = calls;
+ }
- var f = m.TryGetFunc(uniqueName);
- if (f == null)
- return m.MkFunc("@undefined", 0).GetConstant();
- return f.GetConstant();
- }
-
- public readonly static int CALL = -1;
- public readonly static int RETURN = -2;
+ List<Tuple<int, int>> orderedStateIds;
- public void PrintModel(Model model) {
- var filename = CommandLineOptions.Clo.ModelViewFile;
- if (model == null || filename == null) return;
+ private Model.Element GetModelValue(Model m, Variable v, int candidateId) {
+ // first, get the unique name
+ string uniqueName;
- if (filename == "-") {
- model.Write(Console.Out);
- Console.Out.Flush();
- }
- else {
- using (var wr = new StreamWriter(filename, !Counterexample.firstModelFile)) {
- Counterexample.firstModelFile = false;
- model.Write(wr);
- }
+ VCExprVar vvar = theoremProver.Context.BoogieExprTranslator.TryLookupVariable(v);
+ if (vvar == null) {
+ uniqueName = v.Name;
+ }
+ else {
+ if (candidateId != 0) {
+ Dictionary<VCExprVar, VCExpr> mapping = calls.id2Vars[candidateId];
+ if (mapping.ContainsKey(vvar)) {
+ VCExpr e = mapping[vvar];
+ if (e is VCExprLiteral) {
+ VCExprLiteral lit = (VCExprLiteral)e;
+ return m.MkElement(lit.ToString());
}
+ vvar = (VCExprVar)mapping[vvar];
}
+ }
+ uniqueName = theoremProver.Context.Lookup(vvar);
+ }
- private void GetModelWithStates(Model m) {
- if (m == null) return;
+ var f = m.TryGetFunc(uniqueName);
+ if (f == null)
+ return m.MkFunc("@undefined", 0).GetConstant();
+ return f.GetConstant();
+ }
- var mvstates = m.TryGetFunc("@MV_state");
- if (mvstates == null)
- return;
+ public readonly static int CALL = -1;
+ public readonly static int RETURN = -2;
- Contract.Assert(mvstates.Arity == 2);
+ public void PrintModel(Model model) {
+ var filename = CommandLineOptions.Clo.ModelViewFile;
+ if (model == null || filename == null) return;
- foreach (Variable v in mvInfo.AllVariables) {
- m.InitialState.AddBinding(v.Name, GetModelValue(m, v, 0));
- }
+ if (filename == "-") {
+ model.Write(Console.Out);
+ Console.Out.Flush();
+ }
+ else {
+ using (var wr = new StreamWriter(filename, !Counterexample.firstModelFile)) {
+ Counterexample.firstModelFile = false;
+ model.Write(wr);
+ }
+ }
+ }
- int lastCandidate = 0;
- int lastCapturePoint = CALL;
- for (int i = 0; i < this.orderedStateIds.Count; ++i) {
- var s = orderedStateIds[i];
- int candidate = s.Item1;
- int capturePoint = s.Item2;
- string implName = calls.getProc(candidate);
- ModelViewInfo info = candidate == 0 ? mvInfo : implName2StratifiedInliningInfo[implName].mvInfo;
-
- if (capturePoint == CALL || capturePoint == RETURN) {
- lastCandidate = candidate;
- lastCapturePoint = capturePoint;
- continue;
- }
+ private void GetModelWithStates(Model m) {
+ if (m == null) return;
+ var mvInfo = mainInfo.mvInfo;
+ var mvstates = m.TryGetFunc("@MV_state");
+ if (mvstates == null)
+ return;
- Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);
- VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];
- var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)
- ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();
- var cs = m.MkState(map.Description);
-
- foreach (Variable v in info.AllVariables) {
- var e = (Expr)map.IncarnationMap[v];
-
- if (e == null) {
- if (lastCapturePoint == CALL || lastCapturePoint == RETURN) {
- cs.AddBinding(v.Name, GetModelValue(m, v, candidate));
- }
- continue;
- }
-
- if (lastCapturePoint != CALL && lastCapturePoint != RETURN && prevInc[v] == e) continue; // skip unchanged variables
-
- Model.Element elt;
- if (e is IdentifierExpr) {
- IdentifierExpr ide = (IdentifierExpr)e;
- elt = GetModelValue(m, ide.Decl, candidate);
- }
- else if (e is LiteralExpr) {
- LiteralExpr lit = (LiteralExpr)e;
- elt = m.MkElement(lit.Val.ToString());
- }
- else {
- Contract.Assume(false);
- elt = m.MkFunc(e.ToString(), 0).GetConstant();
- }
- cs.AddBinding(v.Name, elt);
- }
+ Contract.Assert(mvstates.Arity == 2);
- lastCandidate = candidate;
- lastCapturePoint = capturePoint;
- }
+ foreach (Variable v in mvInfo.AllVariables) {
+ m.InitialState.AddBinding(v.Name, GetModelValue(m, v, 0));
+ }
- return;
- }
+ int lastCandidate = 0;
+ int lastCapturePoint = CALL;
+ for (int i = 0; i < this.orderedStateIds.Count; ++i) {
+ var s = orderedStateIds[i];
+ int candidate = s.Item1;
+ int capturePoint = s.Item2;
+ string implName = calls.getProc(candidate);
+ ModelViewInfo info = candidate == 0 ? mvInfo : implName2StratifiedInliningInfo[implName].mvInfo;
+
+ if (capturePoint == CALL || capturePoint == RETURN) {
+ lastCandidate = candidate;
+ lastCapturePoint = capturePoint;
+ continue;
+ }
- public void OnModelOld(IList<string/*!*/>/*!*/ labels, Model model) {
- Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);
+ Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);
+ VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];
+ var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)
+ ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();
+ var cs = m.MkState(map.Description);
- candidatesToExpand = new List<int>();
+ foreach (Variable v in info.AllVariables) {
+ var e = (Expr)map.IncarnationMap[v];
- if (underapproximationMode) {
- var cex = GenerateTraceMain(labels, model, mvInfo);
- Debug.Assert(candidatesToExpand.All(calls.isSkipped));
- if (cex != null) {
- GetModelWithStates(model);
- callback.OnCounterexample(cex, null);
- this.PrintModel(model);
- }
- return;
+ if (e == null) {
+ if (lastCapturePoint == CALL || lastCapturePoint == RETURN) {
+ cs.AddBinding(v.Name, GetModelValue(m, v, candidate));
}
+ continue;
+ }
- Contract.Assert(calls != null);
+ if (lastCapturePoint != CALL && lastCapturePoint != RETURN && prevInc[v] == e) continue; // skip unchanged variables
- GenerateTraceMain(labels, model, mvInfo);
+ Model.Element elt;
+ if (e is IdentifierExpr) {
+ IdentifierExpr ide = (IdentifierExpr)e;
+ elt = GetModelValue(m, ide.Decl, candidate);
}
+ else if (e is LiteralExpr) {
+ LiteralExpr lit = (LiteralExpr)e;
+ elt = m.MkElement(lit.Val.ToString());
+ }
+ else {
+ Contract.Assume(false);
+ elt = m.MkFunc(e.ToString(), 0).GetConstant();
+ }
+ cs.AddBinding(v.Name, elt);
+ }
- // Construct the interprocedural trace
- private Counterexample GenerateTraceMain(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo) {
- Contract.Requires(cce.NonNullElements(labels));
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
- errModel.Write(ErrorReporter.ModelWriter);
- ErrorReporter.ModelWriter.Flush();
- }
-
- orderedStateIds = new List<Tuple<int, int>>();
- Counterexample newCounterexample =
- GenerateTrace(labels, errModel, 0, mainImpl);
-
- if (newCounterexample == null)
- return null;
-
- #region Map passive program errors back to original program errors
- ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;
- if (returnExample != null && gotoCmdOrigins != null) {
- foreach (Block b in returnExample.Trace) {
- Contract.Assert(b != null);
- Contract.Assume(b.TransferCmd != null);
- ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];
- if (cmd != null) {
- returnExample.FailingReturn = cmd;
- break;
- }
- }
- }
- #endregion
+ lastCandidate = candidate;
+ lastCapturePoint = capturePoint;
+ }
- return newCounterexample;
- }
+ return;
+ }
- private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
- int candidateId, Implementation procImpl) {
- Contract.Requires(cce.NonNullElements(labels));
- Contract.Requires(procImpl != null);
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
+ Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);
- Hashtable traceNodes = new Hashtable();
- //string procPrefix = "si_inline_" + candidateId.ToString() + "_";
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
+ model.Write(ErrorReporter.ModelWriter);
+ ErrorReporter.ModelWriter.Flush();
+ }
- //Console.WriteLine("GenerateTrace: {0}", procImpl.Name);
- foreach (string s in labels) {
- Contract.Assert(s != null);
- var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId);
+ candidatesToExpand = new List<int>();
+ orderedStateIds = new List<Tuple<int, int>>();
+ var cex = GenerateTrace(labels, model, 0, mainInfo.impl, mainInfo.mvInfo);
- if (absylabel == null) continue;
+ if (underapproximationMode && cex != null) {
+ //Debug.Assert(candidatesToExpand.All(calls.isSkipped));
+ GetModelWithStates(model);
+ callback.OnCounterexample(cex, null);
+ this.PrintModel(model);
+ }
+ }
- Absy absy;
+ private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,
+ int candidateId, Implementation procImpl, ModelViewInfo mvInfo) {
+ Contract.Requires(cce.NonNullElements(labels));
+ Contract.Requires(procImpl != null);
- if (candidateId == 0) {
- absy = Label2Absy(absylabel);
- }
- else {
- absy = Label2Absy(procImpl.Name, absylabel);
- }
+ Hashtable traceNodes = new Hashtable();
- if (traceNodes.ContainsKey(absy))
- System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");
- else
- traceNodes.Add(absy, null);
- }
+ foreach (string s in labels) {
+ Contract.Assert(s != null);
+ var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId);
- BlockSeq trace = new BlockSeq();
- Block entryBlock = cce.NonNull(procImpl.Blocks[0]);
- Contract.Assert(entryBlock != null);
- Contract.Assert(traceNodes.Contains(entryBlock));
- trace.Add(entryBlock);
+ if (absylabel == null) continue;
- var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
- Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);
+ Absy absy;
- return newCounterexample;
- }
+ if (candidateId == 0) {
+ absy = Label2Absy(absylabel);
+ }
+ else {
+ absy = Label2Absy(procImpl.Name, absylabel);
+ }
- private Counterexample GenerateTraceRec(
- IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,
- int candidateId,
- Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,
- Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {
- Contract.Requires(cce.NonNullElements(labels));
- Contract.Requires(b != null);
- Contract.Requires(traceNodes != null);
- Contract.Requires(trace != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
- // After translation, all potential errors come from asserts.
- while (true) {
- CmdSeq cmds = b.Cmds;
- TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Length; i++) {
- Cmd cmd = cce.NonNull(cmds[i]);
-
- // Skip if 'cmd' not contained in the trace or not an assert
- if (cmd is AssertCmd && traceNodes.Contains(cmd)) {
- Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context);
- newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
- return newCounterexample;
- }
-
- // Counterexample generation for inlined procedures
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null)
- continue;
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null)
- continue;
- string calleeName = naryExpr.Fun.FunctionName;
- Contract.Assert(calleeName != null);
-
- BinaryOperator binOp = naryExpr.Fun as BinaryOperator;
- if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) {
- Expr expr = naryExpr.Args[0];
- NAryExpr mvStateExpr = expr as NAryExpr;
- if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) {
- LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;
- orderedStateIds.Add(new Tuple<int, int>(candidateId, x.asBigNum.ToInt));
- }
- }
-
- if (calleeName.StartsWith(recordProcName) && errModel != null) {
- var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
-
- // Record concrete value of the argument to this procedure
- var args = new List<Model.Element>();
- if (expr is VCExprIntLit) {
- args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
- }
- else if (expr == VCExpressionGenerator.True) {
- args.Add(errModel.MkElement("true"));
- }
- else if (expr == VCExpressionGenerator.False) {
- args.Add(errModel.MkElement("false"));
- }
- else if (expr is VCExprVar) {
- var idExpr = expr as VCExprVar;
- string name = context.Lookup(idExpr);
- Contract.Assert(name != null);
- Model.Func f = errModel.TryGetFunc(name);
- if (f != null) {
- args.Add(f.GetConstant());
- }
- }
- else {
- Contract.Assert(false);
- }
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(null, args);
- continue;
- }
-
- if (!implName2StratifiedInliningInfo.ContainsKey(calleeName))
- continue;
-
- Contract.Assert(calls != null);
-
- int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
-
- if (calls.currCandidates.Contains(calleeId)) {
- candidatesToExpand.Add(calleeId);
- }
- else {
- orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(
- cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),
- new List<Model.Element>());
- orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
- }
- }
+ if (traceNodes.ContainsKey(absy))
+ System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");
+ else
+ traceNodes.Add(absy, null);
+ }
- GotoCmd gotoCmd = transferCmd as GotoCmd;
- if (gotoCmd != null) {
- b = null;
- foreach (Block bb in cce.NonNull(gotoCmd.labelTargets)) {
- Contract.Assert(bb != null);
- if (traceNodes.Contains(bb)) {
- trace.Add(bb);
- b = bb;
- break;
- }
- }
- if (b != null) continue;
- }
- return null;
- }
- }
+ BlockSeq trace = new BlockSeq();
+ Block entryBlock = cce.NonNull(procImpl.Blocks[0]);
+ Contract.Assert(entryBlock != null);
+ Contract.Assert(traceNodes.Contains(entryBlock));
+ trace.Add(entryBlock);
- public override void OnModel(IList<string> labels, Model model) {
- if (CommandLineOptions.Clo.UseLabels) {
- OnModelOld(labels, model);
- }
- else {
- List<Absy> absyList = new List<Absy>();
- foreach (var label in labels) {
- absyList.Add(Label2Absy(label));
- }
+ var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
+ Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);
- orderedStateIds = new List<Tuple<int, int>>();
- candidatesToExpand = new List<int>();
+ return newCounterexample;
+ }
- var cex = NewTrace(0, absyList, model);
+ private Counterexample GenerateTraceRec(
+ IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,
+ int candidateId,
+ Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,
+ Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {
+ Contract.Requires(cce.NonNullElements(labels));
+ Contract.Requires(b != null);
+ Contract.Requires(traceNodes != null);
+ Contract.Requires(trace != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
+ // After translation, all potential errors come from asserts.
+ while (true) {
+ CmdSeq cmds = b.Cmds;
+ TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
+ for (int i = 0; i < cmds.Length; i++) {
+ Cmd cmd = cce.NonNull(cmds[i]);
+
+ // Skip if 'cmd' not contained in the trace or not an assert
+ if (cmd is AssertCmd && traceNodes.Contains(cmd)) {
+ Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, theoremProver.Context);
+ newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
+ return newCounterexample;
+ }
- if (underapproximationMode) {
- GetModelWithStates(model);
- callback.OnCounterexample(cex, null);
- this.PrintModel(model);
- }
+ // Counterexample generation for inlined procedures
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ if (assumeCmd == null)
+ continue;
+ NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
+ if (naryExpr == null)
+ continue;
+ string calleeName = naryExpr.Fun.FunctionName;
+ Contract.Assert(calleeName != null);
+
+ BinaryOperator binOp = naryExpr.Fun as BinaryOperator;
+ if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) {
+ Expr expr = naryExpr.Args[0];
+ NAryExpr mvStateExpr = expr as NAryExpr;
+ if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) {
+ LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;
+ orderedStateIds.Add(new Tuple<int, int>(candidateId, x.asBigNum.ToInt));
}
}
- private Counterexample NewTrace(int candidateId, List<Absy> absyList, Model model) {
- AssertCmd assertCmd = (AssertCmd)absyList[absyList.Count - 1];
- BlockSeq trace = new BlockSeq();
- var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
- for (int j = 0; j < absyList.Count - 1; j++) {
- Block b = (Block)absyList[j];
- trace.Add(b);
- CmdSeq cmdSeq = b.Cmds;
- for (int i = 0; i < cmdSeq.Length; i++) {
- Cmd cmd = cmdSeq[i];
- if (cmd == assertCmd) break;
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- if (assumeCmd == null) continue;
- NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
- if (naryExpr == null)
- continue;
- string calleeName = naryExpr.Fun.FunctionName;
- Contract.Assert(calleeName != null);
-
- BinaryOperator binOp = naryExpr.Fun as BinaryOperator;
- if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) {
- Expr expr = naryExpr.Args[0];
- NAryExpr mvStateExpr = expr as NAryExpr;
- if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) {
- LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;
- orderedStateIds.Add(new Tuple<int, int>(candidateId, x.asBigNum.ToInt));
- }
- }
-
- if (calleeName.StartsWith(recordProcName) && model != null) {
- var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
-
- // Record concrete value of the argument to this procedure
- var args = new List<Model.Element>();
- if (expr is VCExprIntLit) {
- args.Add(model.MkElement((expr as VCExprIntLit).Val.ToString()));
- }
- else if (expr == VCExpressionGenerator.True) {
- args.Add(model.MkElement("true"));
- }
- else if (expr == VCExpressionGenerator.False) {
- args.Add(model.MkElement("false"));
- }
- else if (expr is VCExprVar) {
- var idExpr = expr as VCExprVar;
- string name = context.Lookup(idExpr);
- Contract.Assert(name != null);
- Model.Func f = model.TryGetFunc(name);
- if (f != null) {
- args.Add(f.GetConstant());
- }
- }
- else {
- Contract.Assert(false);
- }
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(null, args);
- continue;
- }
-
- if (!implName2StratifiedInliningInfo.ContainsKey(calleeName))
- continue;
-
- int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
-
- if (calls.currCandidates.Contains(calleeId)) {
- candidatesToExpand.Add(calleeId);
- }
- else {
- orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
- string[] labels = theoremProver.CalculatePath(calleeId);
- List<Absy> calleeAbsyList = new List<Absy>();
- foreach (string label in labels) {
- VCExprNAry expr = calls.id2Candidate[calleeId];
- string procName = (cce.NonNull(expr.Op as VCExprBoogieFunctionOp)).Func.Name;
- calleeAbsyList.Add(Label2Absy(procName, label));
- }
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
- new CalleeCounterexampleInfo(NewTrace(calleeId, calleeAbsyList, model), new List<Model.Element>());
- orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
- }
+ if (calleeName.StartsWith(recordProcName) && errModel != null) {
+ var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];
+
+ // Record concrete value of the argument to this procedure
+ var args = new List<Model.Element>();
+ if (expr is VCExprIntLit) {
+ args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));
+ }
+ else if (expr == VCExpressionGenerator.True) {
+ args.Add(errModel.MkElement("true"));
+ }
+ else if (expr == VCExpressionGenerator.False) {
+ args.Add(errModel.MkElement("false"));
+ }
+ else if (expr is VCExprVar) {
+ var idExpr = expr as VCExprVar;
+ string name = theoremProver.Context.Lookup(idExpr);
+ Contract.Assert(name != null);
+ Model.Func f = errModel.TryGetFunc(name);
+ if (f != null) {
+ args.Add(f.GetConstant());
}
}
-
- Block lastBlock = (Block)absyList[absyList.Count - 2];
- Counterexample newCounterexample = AssertCmdToCounterexample(assertCmd, lastBlock.TransferCmd, trace, model, mvInfo, context);
- newCounterexample.AddCalleeCounterexample(calleeCounterexamples);
- return newCounterexample;
+ else {
+ Contract.Assert(false);
+ }
+ calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ new CalleeCounterexampleInfo(null, args);
+ continue;
}
- public override Absy Label2Absy(string label)
- {
- //Contract.Requires(label != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
+ if (!implName2StratifiedInliningInfo.ContainsKey(calleeName))
+ continue;
- int id = int.Parse(label);
- Contract.Assert(calls != null);
- return cce.NonNull((Absy)calls.mainLabel2absy[id]);
- }
+ Contract.Assert(calls != null);
- public Absy Label2Absy(string procName, string label)
- {
- Contract.Requires(label != null);
- Contract.Requires(procName != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
+ int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)];
- int id = int.Parse(label);
- Hashtable l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
- return cce.NonNull((Absy)l2a[id]);
+ if (calls.currCandidates.Contains(calleeId)) {
+ candidatesToExpand.Add(calleeId);
}
-
- public override void OnResourceExceeded(string msg)
- {
- //Contract.Requires(msg != null);
- //resourceExceededMessage = msg;
+ else {
+ orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
+ var calleeInfo = implName2StratifiedInliningInfo[calleeName];
+ calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<Model.Element>());
+ orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
}
+ }
- public override void OnProverWarning(string msg)
- {
- //Contract.Requires(msg != null);
- callback.OnWarning(msg);
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if (gotoCmd != null) {
+ b = null;
+ foreach (Block bb in cce.NonNull(gotoCmd.labelTargets)) {
+ Contract.Assert(bb != null);
+ if (traceNodes.Contains(bb)) {
+ trace.Add(bb);
+ b = bb;
+ break;
+ }
}
+ if (b != null) continue;
+ }
+ return null;
}
+ }
- // Used inside PassifyImpl
- protected override void addExitAssert(string implName, Block exitBlock)
- {
- if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName))
- {
- Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;
- Contract.Assert(assertExpr != null);
- exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
- }
- }
+ public override Absy Label2Absy(string label) {
+ //Contract.Requires(label != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
- public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
- {
- // Construct the set of inlined procs in the original program
- var inlinedProcs = new HashSet<string>();
- foreach (var decl in program.TopLevelDeclarations)
- {
- // Implementations
- if (decl is Implementation)
- {
- var impl = decl as Implementation;
- if (!(impl.Proc is LoopProcedure))
- {
- inlinedProcs.Add(impl.Name);
- }
- }
+ int id = int.Parse(label);
+ Contract.Assert(calls != null);
+ return cce.NonNull((Absy)calls.mainLabel2absy[id]);
+ }
- // And recording procedures
- if (decl is Procedure)
- {
- var proc = decl as Procedure;
- if (proc.Name.StartsWith(recordProcName))
- {
- Debug.Assert(!(decl is LoopProcedure));
- inlinedProcs.Add(proc.Name);
- }
- }
- }
+ public Absy Label2Absy(string procName, string label) {
+ Contract.Requires(label != null);
+ Contract.Requires(procName != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
- return extractLoopTraceRec(
- new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
- mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ int id = int.Parse(label);
+ Hashtable l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy;
+ return cce.NonNull((Absy)l2a[id]);
+ }
+
+ public override void OnResourceExceeded(string msg) {
+ //Contract.Requires(msg != null);
+ //resourceExceededMessage = msg;
+ }
+
+ public override void OnProverWarning(string msg) {
+ //Contract.Requires(msg != null);
+ callback.OnWarning(msg);
+ }
+ }
+
+ // Used inside PassifyImpl
+ protected override void addExitAssert(string implName, Block exitBlock) {
+ if (implName2StratifiedInliningInfo != null && implName2StratifiedInliningInfo.ContainsKey(implName)) {
+ Expr assertExpr = implName2StratifiedInliningInfo[implName].assertExpr;
+ Contract.Assert(assertExpr != null);
+ exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, assertExpr));
+ }
+ }
+
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo) {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations) {
+ // Implementations
+ if (decl is Implementation) {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure)) {
+ inlinedProcs.Add(impl.Name);
+ }
}
- protected override bool elIsLoop(string procname)
- {
- StratifiedInliningInfo info = null;
- if (implName2StratifiedInliningInfo.ContainsKey(procname))
- {
- info = implName2StratifiedInliningInfo[procname];
- }
+ // And recording procedures
+ if (decl is Procedure) {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName)) {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
- if (info == null) return false;
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<Model.Element>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
- var lp = info.impl.Proc as LoopProcedure;
+ protected override bool elIsLoop(string procname) {
+ StratifiedInliningInfo info = null;
+ if (implName2StratifiedInliningInfo.ContainsKey(procname)) {
+ info = implName2StratifiedInliningInfo[procname];
+ }
- if (lp == null) return false;
- return true;
- }
+ if (info == null) return false;
+
+ var lp = info.impl.Proc as LoopProcedure;
+
+ if (lp == null) return false;
+ return true;
+ }
- } // class StratifiedVCGen
+ } // class StratifiedVCGen
} // namespace VC
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 957defb0..7e3e3f17 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2361,7 +2361,7 @@ namespace VC { return null;
}
- protected static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context)
+ public static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context)
{
Contract.Requires(cmd != null);
Contract.Requires(transferCmd != null);
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index 954ea799..b9083fae 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -1,58 +1,58 @@ ----- Running regression test t1.bpl
-t1.bpl(38,5): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- t1.bpl(19,3): anon0
- t1.bpl(23,3): anon3_LoopHead
+ t1.bpl(17,3): anon0
+ t1.bpl(22,3): anon3_LoopHead
Inlined call to procedure foo begins
- t1.bpl(11,5): anon0
+ t1.bpl(8,5): anon0
Inlined call to procedure foo ends
- t1.bpl(27,3): anon3_LoopBody
- t1.bpl(23,3): anon3_LoopHead
+ t1.bpl(26,3): anon3_LoopBody
+ t1.bpl(22,3): anon3_LoopHead
Inlined call to procedure foo begins
- t1.bpl(11,5): anon0
+ t1.bpl(8,5): anon0
Inlined call to procedure foo ends
- t1.bpl(27,3): anon3_LoopBody
- t1.bpl(23,3): anon3_LoopHead
+ t1.bpl(26,3): anon3_LoopBody
+ t1.bpl(22,3): anon3_LoopHead
Inlined call to procedure foo begins
- t1.bpl(11,5): anon0
+ t1.bpl(8,5): anon0
Inlined call to procedure foo ends
- t1.bpl(33,3): anon3_LoopDone
- t1.bpl(37,3): anon2
+ t1.bpl(32,3): anon3_LoopDone
+ t1.bpl(36,3): anon2
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test t2.bpl
-t2.bpl(51,5): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- t2.bpl(19,3): anon0
- t2.bpl(23,3): anon3_LoopHead
+ t2.bpl(16,3): anon0
+ t2.bpl(21,3): anon3_LoopHead
Inlined call to procedure foo begins
- t2.bpl(11,5): anon0
+ t2.bpl(7,5): anon0
Inlined call to procedure foo ends
- t2.bpl(27,3): anon3_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(42,3): lab1_LoopDone
- t2.bpl(23,3): anon3_LoopHead
+ t2.bpl(25,3): anon3_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(40,3): lab1_LoopDone
+ t2.bpl(21,3): anon3_LoopHead
Inlined call to procedure foo begins
- t2.bpl(11,5): anon0
+ t2.bpl(7,5): anon0
Inlined call to procedure foo ends
- t2.bpl(27,3): anon3_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(37,3): lab1_LoopBody
- t2.bpl(34,3): lab1_LoopHead
- t2.bpl(42,3): lab1_LoopDone
- t2.bpl(23,3): anon3_LoopHead
+ t2.bpl(25,3): anon3_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(35,3): lab1_LoopBody
+ t2.bpl(32,3): lab1_LoopHead
+ t2.bpl(40,3): lab1_LoopDone
+ t2.bpl(21,3): anon3_LoopHead
Inlined call to procedure foo begins
- t2.bpl(11,5): anon0
+ t2.bpl(7,5): anon0
Inlined call to procedure foo ends
- t2.bpl(46,3): anon3_LoopDone
- t2.bpl(50,3): anon2
+ t2.bpl(44,3): anon3_LoopDone
+ t2.bpl(48,3): anon2
Boogie program verifier finished with 0 verified, 1 error
-----
@@ -61,25 +61,30 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-----
----- Running regression test t3.bpl with recursion bound 4
-t3.bpl(38,5): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- t3.bpl(19,3): anon0
- t3.bpl(23,3): anon3_LoopHead
+ t3.bpl(15,3): anon0
+ t3.bpl(20,3): anon3_LoopHead
Inlined call to procedure foo begins
- t3.bpl(11,5): anon0
+ t3.bpl(6,5): anon0
Inlined call to procedure foo ends
- t3.bpl(27,3): anon3_LoopBody
- t3.bpl(23,3): anon3_LoopHead
+ t3.bpl(24,3): anon3_LoopBody
+ t3.bpl(20,3): anon3_LoopHead
Inlined call to procedure foo begins
- t3.bpl(11,5): anon0
+ t3.bpl(6,5): anon0
Inlined call to procedure foo ends
- t3.bpl(27,3): anon3_LoopBody
- t3.bpl(23,3): anon3_LoopHead
+ t3.bpl(24,3): anon3_LoopBody
+ t3.bpl(20,3): anon3_LoopHead
Inlined call to procedure foo begins
- t3.bpl(11,5): anon0
+ t3.bpl(6,5): anon0
Inlined call to procedure foo ends
- t3.bpl(33,3): anon3_LoopDone
- t3.bpl(37,3): anon2
+ t3.bpl(30,3): anon3_LoopDone
+ t3.bpl(34,3): anon2
Boogie program verifier finished with 0 verified, 1 error
-----
+----- Running regression test detLoopExtract.bpl with deterministicExtractLoops
+Stratified Inlining: Reached recursion bound of 4
+
+Boogie program verifier finished with 1 verified, 0 errors
+-----
diff --git a/Test/extractloops/detLoopExtract.bpl b/Test/extractloops/detLoopExtract.bpl new file mode 100644 index 00000000..976d58d6 --- /dev/null +++ b/Test/extractloops/detLoopExtract.bpl @@ -0,0 +1,44 @@ +var g:int; +var h:int; //not modified +var k:int; //modified in a procedure call + +procedure {:entrypoint} Foo(a:int) +modifies g; +modifies h; +modifies k; +//ensures g == old(g); +{ + var b: int; + b := 0; + g := a; + h := 5; + +LH: //assert (b + g == a); + if (g == 0) { + goto LE; + } + //assume (b + g == a); // to help the loop extraction figure out the loop invariant + b := b + 1; + call Bar(); + g := g - 1; + if (b > 100) { + goto L2; + } + goto LH; + +LE: + + +L2: //g := old(g); + //assert (b == a); + assume (b != a); + return; + +} + +procedure Bar() +modifies k; +{ + k := 0; + return; +}
\ No newline at end of file diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat index 4fbed727..05bfae55 100644 --- a/Test/extractloops/runtest.bat +++ b/Test/extractloops/runtest.bat @@ -16,4 +16,7 @@ echo ----- echo ----- Running regression test t3.bpl with recursion bound 4
%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:4 t3.bpl
echo -----
+echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops
+%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl
+echo -----
diff --git a/Test/extractloops/t1.bpl b/Test/extractloops/t1.bpl index 58b89e6b..00df45e9 100644 --- a/Test/extractloops/t1.bpl +++ b/Test/extractloops/t1.bpl @@ -1,22 +1,21 @@ var g: int;
-procedure A();
- requires g == 0;
- modifies g;
-procedure {:inline 1} {:verify false} foo();
-implementation foo() {
+procedure foo()
+{
var t: int;
t := 0;
}
-implementation A()
+procedure {:entrypoint} A()
+modifies g;
{
var x: int;
var y: int;
anon0:
+ assume g == 0;
x := 4;
goto anon3_LoopHead;
@@ -35,7 +34,7 @@ implementation A() goto anon2;
anon2:
- assert x == 1;
+ assume x != 1;
return;
}
diff --git a/Test/extractloops/t2.bpl b/Test/extractloops/t2.bpl index d0011929..93f80f20 100644 --- a/Test/extractloops/t2.bpl +++ b/Test/extractloops/t2.bpl @@ -1,22 +1,20 @@ var g: int;
-procedure A();
- requires g == 0;
- modifies g;
-procedure {:inline 1} {:verify false} foo();
-
-implementation foo() {
+procedure foo()
+{
var t: int;
t := 0;
}
-implementation A()
+procedure {:entrypoint} A()
+modifies g;
{
var x: int;
var y: int;
anon0:
+ assume g == 0;
x := 4;
goto anon3_LoopHead;
@@ -48,8 +46,6 @@ implementation A() goto anon2;
anon2:
- assert false;
- assert x == 1;
return;
}
diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl index e5fad6d1..d14767ab 100644 --- a/Test/extractloops/t3.bpl +++ b/Test/extractloops/t3.bpl @@ -1,22 +1,19 @@ var g: int;
-procedure A();
- requires g == 0;
- modifies g;
-
-procedure {:inline 1} {:verify false} foo();
-
-implementation foo() {
+procedure foo()
+{
var t: int;
t := 0;
}
-implementation A()
+procedure {:entrypoint} A()
+modifies g;
{
var x: int;
var y: int;
anon0:
+ assume g == 0;
x := 4;
goto anon3_LoopHead, anon3_LoopBody;
@@ -35,7 +32,7 @@ implementation A() goto anon2;
anon2:
- assert x == 1;
+ assume x != 1;
return;
}
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index 77b00b19..dd5344e8 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,8 +1,7 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
-bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar1.bpl(24,3): anon0
+ bar1.bpl(22,3): anon0
Inlined call to procedure foo begins
bar1.bpl(13,5): anon0
Inlined call to procedure bar begins
@@ -16,25 +15,24 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar2.bpl
-bar2.bpl(21,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar2.bpl(19,3): anon0
+ bar2.bpl(18,3): anon0
Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(9,7): anon3_Else
+ bar2.bpl(4,3): anon0
+ bar2.bpl(5,7): anon3_Then
Inlined call to procedure foo ends
Inlined call to procedure foo begins
- bar2.bpl(5,3): anon0
- bar2.bpl(6,7): anon3_Then
+ bar2.bpl(4,3): anon0
+ bar2.bpl(8,7): anon3_Else
Inlined call to procedure foo ends
Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
-bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar3.bpl(38,3): anon0
+ bar3.bpl(35,3): anon0
Inlined call to procedure foo begins
bar3.bpl(18,3): anon0
bar3.bpl(19,7): anon3_Then
@@ -63,7 +61,7 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-----
----- Running regression test bar7.bpl
-bar7.bpl(42,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar7.bpl(35,5): anon0
bar7.bpl(37,5): anon4_Then
@@ -156,7 +154,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar8.bpl
-bar8.bpl(41,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar8.bpl(34,5): anon0
bar8.bpl(36,5): anon4_Then
@@ -249,7 +247,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar9.bpl
-bar9.bpl(44,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar9.bpl(35,5): anon0
bar9.bpl(41,5): anon4_Else
@@ -386,7 +384,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar10.bpl
-bar10.bpl(40,3): Error BP5001: This assertion might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
bar10.bpl(35,5): anon0
Inlined call to procedure bar1 begins
@@ -485,10 +483,9 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar11.bpl
-bar11.bpl(31,1): Error BP5003: A postcondition might not hold on this return path.
-bar11.bpl(26,1): Related location: This is the postcondition that might not hold.
+(0,0): Error BP5001: This assertion might not hold.
Execution trace:
- bar11.bpl(30,3): anon0
+ bar11.bpl(26,3): anon0
Inlined call to procedure foo begins
bar11.bpl(15,3): anon0
value = 0
diff --git a/Test/stratifiedinline/bar1.bpl b/Test/stratifiedinline/bar1.bpl index 845954d5..bd210f70 100644 --- a/Test/stratifiedinline/bar1.bpl +++ b/Test/stratifiedinline/bar1.bpl @@ -1,13 +1,13 @@ var x: int;
var y: int;
-procedure {:inline 1} bar()
+procedure bar()
modifies y;
{
y := y + 1;
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
x := x + 1;
@@ -16,11 +16,11 @@ modifies x, y; x := x + 1;
}
-procedure main()
-requires x == y;
-ensures x != y;
+procedure {:entrypoint} main()
modifies x, y;
{
+ assume x == y;
call foo();
+ assume x == y;
}
diff --git a/Test/stratifiedinline/bar10.bpl b/Test/stratifiedinline/bar10.bpl index 8cfcfc13..ab1e4748 100644 --- a/Test/stratifiedinline/bar10.bpl +++ b/Test/stratifiedinline/bar10.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo()
+procedure foo()
modifies i;
{
if (i < 20) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m)
@@ -20,7 +20,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -29,7 +29,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -37,5 +37,5 @@ modifies i; call bar2(0);
i := 0;
call foo();
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar11.bpl b/Test/stratifiedinline/bar11.bpl index baad27a1..67e21ba6 100644 --- a/Test/stratifiedinline/bar11.bpl +++ b/Test/stratifiedinline/bar11.bpl @@ -2,14 +2,14 @@ var x: int; var y: int;
procedure boogie_si_record_int(x:int);
-procedure {:inline 1} bar()
+procedure bar()
modifies y;
{
y := y + 1;
call boogie_si_record_int(y);
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
call boogie_si_record_int(x);
@@ -20,13 +20,12 @@ modifies x, y; call boogie_si_record_int(x);
}
-procedure main()
-requires x == 0;
-requires x == y;
-ensures x != y;
+procedure {:entrypoint} main()
modifies x, y;
{
-
+ assume x == 0;
+ assume x == y;
call foo();
+ assume x == y;
}
diff --git a/Test/stratifiedinline/bar2.bpl b/Test/stratifiedinline/bar2.bpl index 76991a8f..6c383591 100644 --- a/Test/stratifiedinline/bar2.bpl +++ b/Test/stratifiedinline/bar2.bpl @@ -1,5 +1,4 @@ -
-procedure {:inline 1} foo() returns (x: bool)
+procedure foo() returns (x: bool)
{
var b: bool;
if (b) {
@@ -11,14 +10,14 @@ procedure {:inline 1} foo() returns (x: bool) }
}
-procedure main()
+procedure {:entrypoint} main()
{
var b1: bool;
var b2: bool;
call b1 := foo();
call b2 := foo();
- assert b1 == b2;
+ assume b1 != b2;
}
diff --git a/Test/stratifiedinline/bar3.bpl b/Test/stratifiedinline/bar3.bpl index 7bd91184..a1f0bea3 100644 --- a/Test/stratifiedinline/bar3.bpl +++ b/Test/stratifiedinline/bar3.bpl @@ -1,7 +1,7 @@ var y: int;
var x: int;
-procedure {:inline 1} bar(b: bool)
+procedure bar(b: bool)
modifies y;
{
if (b) {
@@ -11,7 +11,7 @@ modifies y; }
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
var b: bool;
@@ -29,13 +29,11 @@ modifies x, y; }
-procedure main()
-requires x == y;
-ensures x == y;
+procedure {:entrypoint} main()
modifies x, y;
-modifies y;
{
+ assume x == y;
call foo();
- assert x == y;
call bar(false);
+ assume x != y;
}
diff --git a/Test/stratifiedinline/bar4.bpl b/Test/stratifiedinline/bar4.bpl index 84640811..4b3a6ee2 100644 --- a/Test/stratifiedinline/bar4.bpl +++ b/Test/stratifiedinline/bar4.bpl @@ -1,7 +1,7 @@ var y: int;
var x: int;
-procedure {:inline 1} bar() returns (b: bool)
+procedure bar() returns (b: bool)
modifies y;
{
if (b) {
@@ -11,7 +11,7 @@ modifies y; }
}
-procedure {:inline 1} foo()
+procedure foo()
modifies x, y;
{
var b: bool;
@@ -25,14 +25,13 @@ modifies x, y; }
-procedure main() returns (b: bool)
-requires x == y;
-ensures !b ==> x == y+1;
-ensures b ==> x+1 == y;
+procedure {:entrypoint} main() returns (b: bool)
modifies x, y;
-modifies y;
{
+ assume x == y;
call foo();
- assert x == y;
- call b := bar();
+ if (x == y) {
+ call b := bar();
+ assume (if b then x+1 != y else x != y+1);
+ }
}
diff --git a/Test/stratifiedinline/bar6.bpl b/Test/stratifiedinline/bar6.bpl index e133aef7..dd528f6f 100644 --- a/Test/stratifiedinline/bar6.bpl +++ b/Test/stratifiedinline/bar6.bpl @@ -1,6 +1,6 @@ var M: [int]int;
-procedure {:inline 1} bar(y: int) returns (b: bool)
+procedure bar(y: int) returns (b: bool)
modifies M;
{
if (b) {
@@ -10,7 +10,7 @@ modifies M; }
}
-procedure {:inline 1} foo(x: int, y: int)
+procedure foo(x: int, y: int)
modifies M;
{
var b: bool;
@@ -23,14 +23,14 @@ modifies M; }
}
-procedure main(x: int, y: int) returns (b: bool)
-requires x != y;
-requires M[x] == M[y];
-ensures !b ==> M[x] == M[y]+1;
-ensures b ==> M[x]+1 == M[y];
+procedure {:entrypoint} main(x: int, y: int) returns (b: bool)
modifies M;
{
+ assume x != y;
+ assume M[x] == M[y];
call foo(x, y);
- assert M[x] == M[y];
- call b := bar(y);
+ if (M[x] == M[y]) {
+ call b := bar(y);
+ assume (if b then M[x]+1 != M[y] else M[x] != M[y]+1);
+ }
}
diff --git a/Test/stratifiedinline/bar7.bpl b/Test/stratifiedinline/bar7.bpl index b28777bd..41cf612e 100644 --- a/Test/stratifiedinline/bar7.bpl +++ b/Test/stratifiedinline/bar7.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo()
+procedure foo()
modifies i;
{
if (i < 20) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m)
@@ -20,7 +20,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -29,7 +29,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -39,5 +39,5 @@ modifies i; call bar1(0);
call bar2(0);
}
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar8.bpl b/Test/stratifiedinline/bar8.bpl index e96655f3..356645e6 100644 --- a/Test/stratifiedinline/bar8.bpl +++ b/Test/stratifiedinline/bar8.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo()
+procedure foo()
modifies i;
{
if (i < 20) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m) {
@@ -19,7 +19,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -28,7 +28,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -38,5 +38,5 @@ modifies i; call bar1(0);
call bar2(0);
}
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/Test/stratifiedinline/bar9.bpl b/Test/stratifiedinline/bar9.bpl index 12de78ad..d1eacb18 100644 --- a/Test/stratifiedinline/bar9.bpl +++ b/Test/stratifiedinline/bar9.bpl @@ -1,7 +1,7 @@ var i: int;
var m: int;
-procedure {:inline 1} foo(x: int)
+procedure foo(x: int)
modifies i;
{
if (i < x) {
@@ -10,7 +10,7 @@ modifies i; }
}
-procedure {:inline 1} bar1(j: int)
+procedure bar1(j: int)
modifies i;
{
if (j < 2*m)
@@ -20,7 +20,7 @@ modifies i; }
}
-procedure {:inline 1} bar2(j: int)
+procedure bar2(j: int)
modifies i;
{
if (j < m) {
@@ -29,7 +29,7 @@ modifies i; }
}
-procedure main()
+procedure {:entrypoint} main()
modifies i;
{
i := 0;
@@ -41,5 +41,5 @@ modifies i; call bar1(0);
call bar2(0);
}
- assert i < 10;
+ assume !(i < 10);
}
\ No newline at end of file diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 51b48ab5..2d0eae82 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,20 +1,20 @@ -# Aste started: 2012-05-01 07:00:01
+# Aste started: 2012-05-29 07:00:01
# Host id: Boogiebox
# Configuration: boogie.cfg
# Task: aste.tasks.boogie.FullBuild
-# [2012-05-01 07:02:01] SpecSharp revision: 3db7f750e303
-# [2012-05-01 07:02:01] SscBoogie revision: 3db7f750e303
-# [2012-05-01 07:03:39] Boogie revision: cabbad2de19a
-[2012-05-01 07:05:18] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
+# [2012-05-29 07:01:20] SpecSharp revision: 221320b2a485
+# [2012-05-29 07:01:20] SscBoogie revision: 221320b2a485
+# [2012-05-29 07:02:08] Boogie revision: cd6a26bacb0d
+[2012-05-29 07:03:56] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
1>corflags : warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
-[2012-05-01 07:06:46] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
+[2012-05-29 07:05:22] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected
- D:\Temp\aste\Boogie\Source\Core\Absy.cs(708,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.
+ D:\Temp\aste\Boogie\Source\Core\Absy.cs(748,7): warning CC1036: Detected call to method 'Graphing.Graph`1<Microsoft.Boogie.Block>.TopologicalSort' without [Pure] in contracts of method 'Microsoft.Boogie.Program.GraphFromImpl(Microsoft.Boogie.Implementation)'.
EXEC : warning CC1079: Type Microsoft.Boogie.Variable implements Microsoft.AbstractInterpretationFramework.IVariable.get_Name by inheriting Microsoft.Boogie.NamedDeclaration.get_Name causing the interface contract to not be checked at runtime. Consider adding a wrapper method.
D:\Temp\aste\Boogie\Source\Core\Parser.cs(116,3): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Resolve(Microsoft.Boogie.ResolutionContext)' overrides 'Microsoft.Boogie.Absy.Resolve(Microsoft.Boogie.ResolutionContext)', thus cannot add Requires.
D:\Temp\aste\Boogie\Source\Core\Parser.cs(121,5): warning CC1032: Method 'Microsoft.Boogie.Parser+BvBounds.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)' overrides 'Microsoft.Boogie.Expr.Emit(Microsoft.Boogie.TokenTextWriter,System.Int32,System.Boolean)', thus cannot add Requires.
@@ -41,5 +41,5 @@ warning CS0162: Unreachable code detected
warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.
warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.
-[2012-05-01 08:06:00] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
-# [2012-05-01 08:06:41] Released nightly of Boogie
+[2012-05-29 08:04:11] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+# [2012-05-29 08:04:53] Released nightly of Boogie
diff --git a/_admin/Chalice/aste/summary.log b/_admin/Chalice/aste/summary.log index e676ecd8..ade80273 100644 --- a/_admin/Chalice/aste/summary.log +++ b/_admin/Chalice/aste/summary.log @@ -1,9 +1,9 @@ -# Aste started: 2012-05-22 09:04:38
+# Aste started: 2012-05-25 09:05:16
# Host id: Boogiebox
# Configuration: chalice.cfg
# Task: aste.tasks.chalice.FullBuild
-# [2012-05-22 09:05:24] Chalice revision: 5b532a1a7343
-[2012-05-22 09:06:48] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"
+# [2012-05-25 09:06:05] Chalice revision: 8d9c6d63a543
+[2012-05-25 09:07:29] cmd /c "(set JAVA_OPTS=-Dsbt.ivy.home=D:\temp\.ivy2\) && (sbt.bat clean compile)"
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:77: case class `class SeqClass' has case class ancestor `class Class'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:111: case class `class TokenClass' has case class ancestor `class Class'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
@@ -11,6 +11,5 @@ [warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:141: case class `class TokenType' has case class ancestor `class Type'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:168: case class `class SpecialField' has case class ancestor `class Field'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
[warn] D:\temp\aste\Boogie\Chalice\src\main\scala\Ast.scala:227: case class `class SpecialVariable' has case class ancestor `class Variable'. This has been deprecated for unduly complicating both usage and implementation. You should instead use extractors for pattern matching on non-leaf nodes.
-[2012-05-22 10:22:41] 1 out of 83 test(s) failed
-['list-reverse.chalice\r']
-# [2012-05-22 10:23:44] Released nightly of Chalice
+[2012-05-25 10:22:31] 0 out of 83 test(s) failed
+# [2012-05-25 10:23:12] Released nightly of Chalice
|