//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Threading;
using System.IO;
using Microsoft.Boogie;
using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
namespace VC {
using Bpl = Microsoft.Boogie;
using System.Threading.Tasks;
public class VCGen : ConditionGeneration {
private const bool _print_time = false;
///
/// Constructor. Initializes the theorem prover.
///
[NotDelayed]
public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List checkers)
: base(program, checkers)
{
Contract.Requires(program != null);
this.appendLogFile = appendLogFile;
this.logFilePath = logFilePath;
}
private static AssumeCmd AssertTurnedIntoAssume(AssertCmd assrt) {
Contract.Requires(assrt != null);
Contract.Ensures(Contract.Result() != null);
Expr expr = assrt.Expr;
Contract.Assert(expr != null);
switch (Wlp.Subsumption(assrt)) {
case CommandLineOptions.SubsumptionOption.Never:
expr = Expr.True;
break;
case CommandLineOptions.SubsumptionOption.Always:
break;
case CommandLineOptions.SubsumptionOption.NotForQuantifiers:
if (expr is QuantifierExpr) {
expr = Expr.True;
}
break;
default:
Contract.Assert(false);
throw new cce.UnreachableException(); // unexpected case
}
return new AssumeCmd(assrt.tok, expr);
}
#region Soundness smoke tester
class SmokeTester {
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(parent != null);
Contract.Invariant(impl != null);
Contract.Invariant(initial != null);
Contract.Invariant(cce.NonNullDictionaryAndValues(copies));
Contract.Invariant(cce.NonNull(visited));
Contract.Invariant(callback != null);
}
VCGen parent;
Implementation impl;
Block initial;
int id;
Dictionary copies = new Dictionary();
HashSet visited = new HashSet();
VerifierCallback callback;
internal SmokeTester(VCGen par, Implementation i, VerifierCallback callback) {
Contract.Requires(par != null);
Contract.Requires(i != null);
Contract.Requires(callback != null);
parent = par;
impl = i;
initial = i.Blocks[0];
this.callback = callback;
}
internal void Copy() {
CloneBlock(impl.Blocks[0]);
initial = GetCopiedBlocks()[0];
}
internal void Test() {
Contract.EnsuresOnThrow(true);
DFS(initial);
}
void TopologicalSortImpl() {
Graph dag = new Graph();
dag.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph
foreach (Block b in impl.Blocks) {
GotoCmd gtc = b.TransferCmd as GotoCmd;
if (gtc != null) {
Contract.Assume(gtc.labelTargets != null);
foreach (Block dest in gtc.labelTargets) {
Contract.Assert(dest != null);
dag.AddEdge(b, dest);
}
}
}
impl.Blocks = new List();
foreach (Block b in dag.TopologicalSort()) {
Contract.Assert(b != null);
impl.Blocks.Add(b);
}
}
void Emit() {
TopologicalSortImpl();
EmitImpl(impl, false);
}
// this one copies forward
Block CloneBlock(Block b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result() != null);
Block fake_res;
if (copies.TryGetValue(b, out fake_res)) {
return cce.NonNull(fake_res);
}
Block res = new Block(b.tok, b.Label, new CmdSeq(b.Cmds), null);
copies[b] = res;
if (b.TransferCmd is GotoCmd) {
foreach (Block ch in cce.NonNull((GotoCmd)b.TransferCmd).labelTargets) {
Contract.Assert(ch != null);
CloneBlock(ch);
}
}
foreach (Block p in b.Predecessors) {
Contract.Assert(p != null);
res.Predecessors.Add(CloneBlock(p));
}
return res;
}
// this one copies backwards
Block CopyBlock(Block b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result() != null);
Block fake_res;
if (copies.TryGetValue(b, out fake_res)) {
// fake_res should be Block! but the compiler fails
return cce.NonNull(fake_res);
}
Block res;
CmdSeq seq = new CmdSeq();
foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null);
AssertCmd turn = c as AssertCmd;
if (!turnAssertIntoAssumes || turn == null) {
seq.Add(c);
} else {
seq.Add(AssertTurnedIntoAssume(turn));
}
}
res = new Block(b.tok, b.Label, seq, null);
copies[b] = res;
foreach (Block p in b.Predecessors) {
Contract.Assert(p != null);
res.Predecessors.Add(CopyBlock(p));
}
return res;
}
List GetCopiedBlocks() {
Contract.Ensures(cce.NonNullElements(Contract.Result>()));
// the order of nodes in res is random (except for the first one, being the entry)
List res = new List();
res.Add(copies[initial]);
foreach (KeyValuePair kv in copies) {
Contract.Assert(kv.Key != null&&kv.Value!=null);
GotoCmd go = kv.Key.TransferCmd as GotoCmd;
ReturnCmd ret = kv.Key.TransferCmd as ReturnCmd;
if (kv.Key != initial) {
res.Add(kv.Value);
}
if (go != null) {
GotoCmd copy = new GotoCmd(go.tok, new StringSeq(), new BlockSeq());
kv.Value.TransferCmd = copy;
foreach (Block b in cce.NonNull(go.labelTargets)) {
Contract.Assert(b != null);
Block c;
if (copies.TryGetValue(b, out c)) {
copy.AddTarget(cce.NonNull(c));
}
}
} else if (ret != null) {
kv.Value.TransferCmd = ret;
} else {
Contract.Assume(false);
throw new cce.UnreachableException();
}
}
copies.Clear();
return res;
}
// check if e is true, false, !true, !false
// if so return true and the value of the expression in val
bool BooleanEval(Expr e, ref bool val) {
Contract.Requires(e != null);
LiteralExpr lit = e as LiteralExpr;
NAryExpr call = e as NAryExpr;
if (lit != null && lit.isBool) {
val = lit.asBool;
return true;
} else if (call != null &&
call.Fun is UnaryOperator &&
((UnaryOperator)call.Fun).Op == UnaryOperator.Opcode.Not &&
BooleanEval(cce.NonNull(call.Args[0]), ref val)) {
val = !val;
return true;
}
// this is for the 0bv32 != 0bv32 generated by vcc
else if (call != null &&
call.Fun is BinaryOperator &&
((BinaryOperator)call.Fun).Op == BinaryOperator.Opcode.Neq &&
call.Args[0] is LiteralExpr &&
cce.NonNull(call.Args[0]).Equals(call.Args[1])) {
val = false;
return true;
}
return false;
}
bool IsFalse(Expr e) {
Contract.Requires(e != null);
bool val = false;
return BooleanEval(e, ref val) && !val;
}
bool CheckUnreachable(Block cur, CmdSeq seq) {
Contract.Requires(cur != null);
Contract.Requires(seq != null);
Contract.EnsuresOnThrow(true);
foreach (Cmd cmd in seq) {
AssertCmd assrt = cmd as AssertCmd;
if (assrt != null && QKeyValue.FindBoolAttribute(assrt.Attributes, "PossiblyUnreachable"))
return false;
}
DateTime start = DateTime.UtcNow;
if (CommandLineOptions.Clo.Trace) {
System.Console.Write(" soundness smoke test #{0} ... ", id);
}
callback.OnProgress("smoke", id, id, 0.0);
Token tok = new Token();
tok.val = "soundness smoke test assertion";
seq.Add(new AssertCmd(tok, Expr.False));
Block copy = CopyBlock(cur);
Contract.Assert(copy != null);
copy.Cmds = seq;
List backup = impl.Blocks;
Contract.Assert(backup != null);
impl.Blocks = GetCopiedBlocks();
copy.TransferCmd = new ReturnCmd(Token.NoToken);
if (CommandLineOptions.Clo.TraceVerify) {
System.Console.WriteLine();
System.Console.WriteLine(" --- smoke #{0}, before passify", id);
Emit();
}
parent.CurrentLocalVariables = impl.LocVars;
ModelViewInfo mvInfo;
parent.PassifyImpl(impl, out mvInfo);
Hashtable label2Absy;
Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);
Contract.Assert(ch != null);
lock (ch)
{
var exprGen = ch.TheoremProver.Context.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
VCExpr vc = parent.GenerateVC(impl, controlFlowVariableExpr, out label2Absy, ch.TheoremProver.Context);
Contract.Assert(vc != null);
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);
}
impl.Blocks = backup;
if (CommandLineOptions.Clo.TraceVerify)
{
System.Console.WriteLine(" --- smoke #{0}, after passify", id);
Emit();
}
ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
ch.ProverTask.Wait();
ProverInterface.Outcome outcome = ch.ReadOutcome();
ch.GoBackToIdle();
parent.CurrentLocalVariables = null;
DateTime end = DateTime.UtcNow;
TimeSpan elapsed = end - start;
if (CommandLineOptions.Clo.Trace)
{
System.Console.WriteLine(" [{0} s] {1}", elapsed.TotalSeconds,
outcome == ProverInterface.Outcome.Valid ? "OOPS" :
"OK" + (outcome == ProverInterface.Outcome.Invalid ? "" : " (" + outcome + ")"));
}
if (outcome == ProverInterface.Outcome.Valid)
{
// copy it again, so we get the version with calls, assignments and such
copy = CopyBlock(cur);
copy.Cmds = seq;
impl.Blocks = GetCopiedBlocks();
TopologicalSortImpl();
callback.OnUnreachableCode(impl);
impl.Blocks = backup;
return true;
}
return false;
}
}
const bool turnAssertIntoAssumes = false;
void DFS(Block cur) {
Contract.Requires(cur != null);
Contract.EnsuresOnThrow(true);
if (visited.Contains(cur))
return;
visited.Add(cur);
CmdSeq seq = new CmdSeq();
foreach (Cmd cmd_ in cur.Cmds) {
Cmd cmd = cmd_;
Contract.Assert(cmd != null);
AssertCmd assrt = cmd as AssertCmd;
AssumeCmd assm = cmd as AssumeCmd;
CallCmd call = cmd as CallCmd;
bool assumeFalse = false;
if (assrt != null) {
// we're not going any further
// it's clear the user expected unreachable code here
// it's not clear where did he expect it, maybe it would be right to insert
// a check just one command before
if (IsFalse(assrt.Expr))
return;
#if TURN_ASSERT_INFO_ASSUMES
if (turnAssertIntoAssumes) {
cmd = AssertTurnedIntoAssume(assrt);
}
#endif
} else if (assm != null) {
if (IsFalse(assm.Expr))
assumeFalse = true;
} else if (call != null) {
foreach (Ensures e in (cce.NonNull(call.Proc)).Ensures) {
Contract.Assert(e != null);
if (IsFalse(e.Condition))
assumeFalse = true;
}
}
if (assumeFalse) {
CheckUnreachable(cur, seq);
return;
}
seq.Add(cmd);
}
GotoCmd go = cur.TransferCmd as GotoCmd;
ReturnCmd ret = cur.TransferCmd as ReturnCmd;
Contract.Assume(!(go != null && go.labelTargets == null && go.labelNames != null && go.labelNames.Length > 0));
if (ret != null || (go != null && cce.NonNull(go.labelTargets).Length == 0)) {
// we end in return, so there will be no more places to check
CheckUnreachable(cur, seq);
} else if (go != null) {
bool needToCheck = true;
// if all of our children have more than one parent, then
// we're in the right place to check
foreach (Block target in cce.NonNull(go.labelTargets)) {
Contract.Assert(target != null);
if (target.Predecessors.Length == 1) {
needToCheck = false;
}
}
if (needToCheck) {
CheckUnreachable(cur, seq);
}
foreach (Block target in go.labelTargets) {
Contract.Assert(target != null);
DFS(target);
}
}
}
class ErrorHandler : ProverInterface.ErrorHandler {
Hashtable label2Absy;
VerifierCallback callback;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(label2Absy != null);
Contract.Invariant(callback != null);
}
public ErrorHandler(Hashtable label2Absy, VerifierCallback callback) {
Contract.Requires(label2Absy != null);
Contract.Requires(callback != null);
this.label2Absy = label2Absy;
this.callback = callback;
}
public override Absy Label2Absy(string label) {
//Contract.Requires(label != null);
Contract.Ensures(Contract.Result() != null);
int id = int.Parse(label);
return cce.NonNull((Absy)label2Absy[id]);
}
public override void OnProverWarning(string msg) {
//Contract.Requires(msg != null);
this.callback.OnWarning(msg);
}
}
}
#endregion
#region Splitter
class Split {
class BlockStats {
public bool big_block;
public int id;
public double assertion_cost;
public double assumption_cost; // before multiplier
public double incomming_paths;
public List/*!>!*/ virtual_successors = new List();
public List/*!>!*/ virtual_predecesors = new List();
public HashSet reachable_blocks;
public readonly Block block;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(virtual_successors));
Contract.Invariant(cce.NonNullElements(virtual_predecesors));
Contract.Invariant(block != null);
}
public BlockStats(Block b, int i) {
Contract.Requires(b != null);
block = b;
assertion_cost = -1;
id = i;
}
}
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(blocks));
Contract.Invariant(cce.NonNullElements(big_blocks));
Contract.Invariant(cce.NonNullDictionaryAndValues(stats));
Contract.Invariant(cce.NonNullElements(assumized_branches));
Contract.Invariant(gotoCmdOrigins != null);
Contract.Invariant(parent != null);
Contract.Invariant(impl != null);
Contract.Invariant(copies != null);
Contract.Invariant(cce.NonNull(protected_from_assert_to_assume));
Contract.Invariant(cce.NonNull(keep_at_all));
}
readonly List blocks;
readonly List big_blocks = new List();
readonly Dictionary/*!*/ stats = new Dictionary();
readonly int id;
static int current_id;
Block split_block;
bool assert_to_assume;
List/*!*/ assumized_branches = new List();
double score;
bool score_computed;
double total_cost;
int assertion_count;
double assertion_cost; // without multiplication by paths
Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;
readonly public VCGen/*!*/ parent;
Implementation/*!*/ impl;
Dictionary/*!*/ copies = new Dictionary();
bool doing_slice;
double slice_initial_limit;
double slice_limit;
bool slice_pos;
HashSet/*!*/ protected_from_assert_to_assume = new HashSet();
HashSet/*!*/ keep_at_all = new HashSet();
// async interface
private Checker checker;
private int splitNo;
internal ErrorReporter reporter;
public Split(List/*!*/ blocks, Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {
Contract.Requires(cce.NonNullElements(blocks));
Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(par != null);
Contract.Requires(impl != null);
this.blocks = blocks;
this.gotoCmdOrigins = gotoCmdOrigins;
this.parent = par;
this.impl = impl;
this.id = current_id++;
}
public double Cost {
get {
ComputeBestSplit();
return total_cost;
}
}
public bool LastChance {
get {
ComputeBestSplit();
return assertion_count == 1 && score < 0;
}
}
public string Stats {
get {
ComputeBestSplit();
return string.Format("(cost:{0:0}/{1:0}{2})", total_cost, assertion_cost, LastChance ? " last" : "");
}
}
public void DumpDot(int no) {
using (System.IO.StreamWriter sw = System.IO.File.CreateText(string.Format("split.{0}.dot", no))) {
sw.WriteLine("digraph G {");
ComputeBestSplit();
List saved = assumized_branches;
Contract.Assert(saved != null);
assumized_branches = new List();
DoComputeScore(false);
assumized_branches = saved;
foreach (Block b in big_blocks) {
Contract.Assert(b != null);
BlockStats s = GetBlockStats(b);
foreach (Block t in s.virtual_successors) {
Contract.Assert(t != null);
sw.WriteLine("n{0} -> n{1};", s.id, GetBlockStats(t).id);
}
sw.WriteLine("n{0} [label=\"{1}:\\n({2:0.0}+{3:0.0})*{4:0.0}\"{5}];",
s.id, b.Label,
s.assertion_cost, s.assumption_cost, s.incomming_paths,
s.assertion_cost > 0 ? ",shape=box" : "");
}
sw.WriteLine("}");
sw.Close();
}
string filename = string.Format("split.{0}.bpl", no);
using (System.IO.StreamWriter sw = System.IO.File.CreateText(filename)) {
int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
CommandLineOptions.Clo.PrintUnstructured = 2; // print only the unstructured program
bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings;
CommandLineOptions.Clo.PrintDesugarings = false;
List backup = impl.Blocks;
Contract.Assert(backup != null);
impl.Blocks = blocks;
impl.Emit(new TokenTextWriter(filename, sw, false), 0);
impl.Blocks = backup;
CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;
CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
}
}
int bsid;
BlockStats GetBlockStats(Block b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result() != null);
BlockStats s;
if (!stats.TryGetValue(b, out s)) {
s = new BlockStats(b, bsid++);
stats[b] = s;
}
return cce.NonNull(s);
}
double AssertionCost(PredicateCmd c) {
return 1.0;
}
void CountAssertions(Block b) {
Contract.Requires(b != null);
BlockStats s = GetBlockStats(b);
if (s.assertion_cost >= 0)
return; // already done
s.big_block = true;
s.assertion_cost = 0;
s.assumption_cost = 0;
foreach (Cmd c in b.Cmds) {
if (c is AssertCmd) {
double cost = AssertionCost((AssertCmd)c);
s.assertion_cost += cost;
assertion_count++;
assertion_cost += cost;
} else if (c is AssumeCmd) {
s.assumption_cost += AssertionCost((AssumeCmd)c);
}
}
foreach (Block c in Exits(b)) {
Contract.Assert(c != null);
s.virtual_successors.Add(c);
}
if (s.virtual_successors.Count == 1) {
Block next = s.virtual_successors[0];
BlockStats se = GetBlockStats(next);
CountAssertions(next);
if (next.Predecessors.Length > 1 || se.virtual_successors.Count != 1)
return;
s.virtual_successors[0] = se.virtual_successors[0];
s.assertion_cost += se.assertion_cost;
s.assumption_cost += se.assumption_cost;
se.big_block = false;
}
}
HashSet/*!*/ ComputeReachableNodes(Block/*!*/ b) {
Contract.Requires(b != null);
Contract.Ensures(cce.NonNull(Contract.Result>()));
BlockStats s = GetBlockStats(b);
if (s.reachable_blocks != null) {
return s.reachable_blocks;
}
HashSet blocks = new HashSet();
s.reachable_blocks = blocks;
blocks.Add(b);
foreach (Block/*!*/ succ in Exits(b)) {
Contract.Assert(succ != null);
foreach (Block r in ComputeReachableNodes(succ)) {
Contract.Assert(r != null);
blocks.Add(r);
}
}
return blocks;
}
double ProverCost(double vc_cost) {
return vc_cost * vc_cost;
}
void ComputeBestSplit() {
if (score_computed)
return;
score_computed = true;
assertion_count = 0;
foreach (Block b in blocks) {
Contract.Assert(b != null);
CountAssertions(b);
}
foreach (Block b in blocks) {
Contract.Assert(b != null);
BlockStats bs = GetBlockStats(b);
if (bs.big_block) {
big_blocks.Add(b);
foreach (Block ch in bs.virtual_successors) {
Contract.Assert(ch != null);
BlockStats chs = GetBlockStats(ch);
if (!chs.big_block) {
Console.WriteLine("non-big {0} accessed from {1}", ch, b);
DumpDot(-1);
Contract.Assert(false);
throw new cce.UnreachableException();
}
chs.virtual_predecesors.Add(b);
}
}
}
assumized_branches.Clear();
total_cost = ProverCost(DoComputeScore(false));
score = double.PositiveInfinity;
Block best_split = null;
List saved_branches = new List();
foreach (Block b in big_blocks) {
Contract.Assert(b != null);
GotoCmd gt = b.TransferCmd as GotoCmd;
if (gt == null)
continue;
BlockSeq targ = cce.NonNull(gt.labelTargets);
if (targ.Length < 2)
continue;
// caution, we only consider two first exits
double left0, right0, left1, right1;
split_block = b;
assumized_branches.Clear();
assumized_branches.Add(cce.NonNull(targ[0]));
left0 = DoComputeScore(true);
right0 = DoComputeScore(false);
assumized_branches.Clear();
for (int idx = 1; idx < targ.Length; idx++) {
assumized_branches.Add(cce.NonNull(targ[idx]));
}
left1 = DoComputeScore(true);
right1 = DoComputeScore(false);
double current_score = ProverCost(left1) + ProverCost(right1);
double other_score = ProverCost(left0) + ProverCost(right0);
if (other_score < current_score) {
current_score = other_score;
assumized_branches.Clear();
assumized_branches.Add(cce.NonNull(targ[0]));
}
if (current_score < score) {
score = current_score;
best_split = split_block;
saved_branches.Clear();
saved_branches.AddRange(assumized_branches);
}
}
if (CommandLineOptions.Clo.VcsPathSplitMult * score > total_cost) {
split_block = null;
score = -1;
} else {
assumized_branches = saved_branches;
split_block = best_split;
}
}
void UpdateIncommingPaths(BlockStats s) {
Contract.Requires(s != null);
if (s.incomming_paths < 0.0) {
int count = 0;
s.incomming_paths = 0.0;
if (!keep_at_all.Contains(s.block))
return;
foreach (Block b in s.virtual_predecesors) {
Contract.Assert(b != null);
BlockStats ch = GetBlockStats(b);
Contract.Assert(ch != null);
UpdateIncommingPaths(ch);
if (ch.incomming_paths > 0.0) {
s.incomming_paths += ch.incomming_paths;
count++;
}
}
if (count > 1) {
s.incomming_paths *= CommandLineOptions.Clo.VcsPathJoinMult;
}
}
}
void ComputeBlockSetsHelper(Block b, bool allow_small) {
Contract.Requires(b != null);
if (keep_at_all.Contains(b))
return;
keep_at_all.Add(b);
if (allow_small) {
foreach (Block ch in Exits(b)) {
Contract.Assert(ch != null);
if (b == split_block && assumized_branches.Contains(ch))
continue;
ComputeBlockSetsHelper(ch, allow_small);
}
} else {
foreach (Block ch in GetBlockStats(b).virtual_successors) {
Contract.Assert(ch != null);
if (b == split_block && assumized_branches.Contains(ch))
continue;
ComputeBlockSetsHelper(ch, allow_small);
}
}
}
void ComputeBlockSets(bool allow_small) {
protected_from_assert_to_assume.Clear();
keep_at_all.Clear();
Debug.Assert(split_block == null || GetBlockStats(split_block).big_block);
Debug.Assert(GetBlockStats(blocks[0]).big_block);
if (assert_to_assume) {
foreach (Block b in allow_small ? blocks : big_blocks) {
Contract.Assert(b != null);
if (ComputeReachableNodes(b).Contains(cce.NonNull(split_block))) {
keep_at_all.Add(b);
}
}
foreach (Block b in assumized_branches) {
Contract.Assert(b != null);
foreach (Block r in ComputeReachableNodes(b)) {
Contract.Assert(r != null);
if (allow_small || GetBlockStats(r).big_block) {
keep_at_all.Add(r);
protected_from_assert_to_assume.Add(r);
}
}
}
} else {
ComputeBlockSetsHelper(blocks[0], allow_small);
}
}
bool ShouldAssumize(Block b) {
Contract.Requires(b != null);
return assert_to_assume && !protected_from_assert_to_assume.Contains(b);
}
double DoComputeScore(bool aa) {
assert_to_assume = aa;
ComputeBlockSets(false);
foreach (Block b in big_blocks) {
Contract.Assert(b != null);
GetBlockStats(b).incomming_paths = -1.0;
}
GetBlockStats(blocks[0]).incomming_paths = 1.0;
double cost = 0.0;
foreach (Block b in big_blocks) {
Contract.Assert(b != null);
if (keep_at_all.Contains(b)) {
BlockStats s = GetBlockStats(b);
UpdateIncommingPaths(s);
double local = s.assertion_cost;
if (ShouldAssumize(b)) {
local = (s.assertion_cost + s.assumption_cost) * CommandLineOptions.Clo.VcsAssumeMult;
} else {
local = s.assumption_cost * CommandLineOptions.Clo.VcsAssumeMult + s.assertion_cost;
}
local = local + local * s.incomming_paths * CommandLineOptions.Clo.VcsPathCostMult;
cost += local;
}
}
return cost;
}
CmdSeq SliceCmds(Block b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result() != null);
CmdSeq seq = b.Cmds;
Contract.Assert(seq != null);
if (!doing_slice && !ShouldAssumize(b))
return seq;
CmdSeq res = new CmdSeq();
foreach (Cmd c in seq) {
Contract.Assert(c != null);
AssertCmd a = c as AssertCmd;
Cmd the_new = c;
bool swap = false;
if (a != null) {
if (doing_slice) {
double cost = AssertionCost(a);
bool first = (slice_limit - cost) >= 0 || slice_initial_limit == slice_limit;
slice_limit -= cost;
swap = slice_pos == first;
} else if (assert_to_assume) {
swap = true;
} else {
Contract.Assert(false);
throw new cce.UnreachableException();
}
if (swap) {
the_new = AssertTurnedIntoAssume(a);
}
}
res.Add(the_new);
}
return res;
}
Block CloneBlock(Block b) {
Contract.Requires(b != null);
Contract.Ensures(Contract.Result() != null);
Block res;
if (copies.TryGetValue(b, out res)) {
return cce.NonNull(res);
}
res = new Block(b.tok, b.Label, SliceCmds(b), b.TransferCmd);
GotoCmd gt = b.TransferCmd as GotoCmd;
copies[b] = res;
if (gt != null) {
GotoCmd newGoto = new GotoCmd(gt.tok, new StringSeq(), new BlockSeq());
res.TransferCmd = newGoto;
int pos = 0;
foreach (Block ch in cce.NonNull(gt.labelTargets)) {
Contract.Assert(ch != null);
Contract.Assert(doing_slice ||
(assert_to_assume || (keep_at_all.Contains(ch) || assumized_branches.Contains(ch))));
if (doing_slice ||
((b != split_block || assumized_branches.Contains(ch) == assert_to_assume) &&
keep_at_all.Contains(ch))) {
newGoto.AddTarget(CloneBlock(ch));
}
pos++;
}
}
return res;
}
Split DoSplit() {
Contract.Ensures(Contract.Result() != null);
copies.Clear();
CloneBlock(blocks[0]);
List newBlocks = new List();
Hashtable newGotoCmdOrigins = new Hashtable();
foreach (Block b in blocks) {
Contract.Assert(b != null);
Block tmp;
if (copies.TryGetValue(b, out tmp)) {
newBlocks.Add(cce.NonNull(tmp));
if (gotoCmdOrigins.ContainsKey(b)) {
newGotoCmdOrigins[tmp] = gotoCmdOrigins[b];
}
foreach (Block p in b.Predecessors) {
Contract.Assert(p != null);
Block tmp2;
if (copies.TryGetValue(p, out tmp2)) {
tmp.Predecessors.Add(tmp2);
}
}
}
}
return new Split(newBlocks, newGotoCmdOrigins, parent, impl);
}
Split SplitAt(int idx) {
Contract.Ensures(Contract.Result() != null);
assert_to_assume = idx == 0;
doing_slice = false;
ComputeBlockSets(true);
return DoSplit();
}
Split SliceAsserts(double limit, bool pos) {
Contract.Ensures(Contract.Result() != null);
slice_pos = pos;
slice_limit = limit;
slice_initial_limit = limit;
doing_slice = true;
Split r = DoSplit();
/*
Console.WriteLine("split {0} / {1} -->", limit, pos);
List tmp = impl.Blocks;
impl.Blocks = r.blocks;
EmitImpl(impl, false);
impl.Blocks = tmp;
*/
return r;
}
void Print() {
List tmp = impl.Blocks;
Contract.Assert(tmp != null);
impl.Blocks = blocks;
EmitImpl(impl, false);
impl.Blocks = tmp;
}
public Counterexample ToCounterexample(ProverContext context) {
Contract.Requires(context != null);
Contract.Ensures(Contract.Result() != null);
BlockSeq trace = new BlockSeq();
foreach (Block b in blocks) {
Contract.Assert(b != null);
trace.Add(b);
}
foreach (Block b in blocks) {
Contract.Assert(b != null);
foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null);
if (c is AssertCmd) {
return AssertCmdToCounterexample((AssertCmd)c, cce.NonNull(b.TransferCmd), trace, null, null, context);
}
}
}
Contract.Assume(false);
throw new cce.UnreachableException();
}
public static List/*!*/ DoSplit(Split initial, double max_cost, int max) {
Contract.Requires(initial != null);
Contract.Ensures(cce.NonNullElements(Contract.Result>()));
List res = new List();
res.Add(initial);
while (res.Count < max) {
Split best = null;
int best_idx = 0, pos = 0;
foreach (Split s in res) {
Contract.Assert(s != null);
s.ComputeBestSplit(); // TODO check total_cost first
if (s.total_cost > max_cost &&
(best == null || best.total_cost < s.total_cost) &&
(s.assertion_count > 1 || s.split_block != null)) {
best = s;
best_idx = pos;
}
pos++;
}
if (best == null)
break; // no split found
Split s0, s1;
bool split_stats = CommandLineOptions.Clo.TraceVerify;
if (split_stats) {
Console.WriteLine("{0} {1} -->", best.split_block == null ? "SLICE" : ("SPLIT@" + best.split_block.Label), best.Stats);
if (best.split_block != null) {
GotoCmd g = best.split_block.TransferCmd as GotoCmd;
if (g != null) {
Console.Write(" exits: ");
foreach (Block b in cce.NonNull(g.labelTargets)) {
Contract.Assert(b != null);
Console.Write("{0} ", b.Label);
}
Console.WriteLine("");
Console.Write(" assumized: ");
foreach (Block b in best.assumized_branches) {
Contract.Assert(b != null);
Console.Write("{0} ", b.Label);
}
Console.WriteLine("");
}
}
}
if (best.split_block != null) {
s0 = best.SplitAt(0);
s1 = best.SplitAt(1);
} else {
best.split_block = null;
s0 = best.SliceAsserts(best.assertion_cost / 2, true);
s1 = best.SliceAsserts(best.assertion_cost / 2, false);
}
if (true) {
List ss = new List();
ss.Add(s0.blocks[0]);
ss.Add(s1.blocks[0]);
try {
best.SoundnessCheck(new HashSet(), best.blocks[0], ss);
} catch (System.Exception e) {
Console.WriteLine(e);
best.DumpDot(-1);
s0.DumpDot(-2);
s1.DumpDot(-3);
Contract.Assert(false);
throw new cce.UnreachableException();
}
}
if (split_stats) {
s0.ComputeBestSplit();
s1.ComputeBestSplit();
Console.WriteLine(" --> {0}", s0.Stats);
Console.WriteLine(" --> {0}", s1.Stats);
}
if (CommandLineOptions.Clo.TraceVerify) {
best.Print();
}
res[best_idx] = s0;
res.Add(s1);
}
return res;
}
public Checker Checker {
get {
Contract.Ensures(Contract.Result() != null);
Contract.Assert(checker != null);
return checker;
}
}
public Task ProverTask {
get {
Contract.Assert(checker != null);
return checker.ProverTask;
}
}
public void ReadOutcome(ref Outcome cur_outcome, out bool prover_failed) {
Contract.EnsuresOnThrow(true);
ProverInterface.Outcome outcome = cce.NonNull(checker).ReadOutcome();
if (CommandLineOptions.Clo.Trace && splitNo >= 0) {
System.Console.WriteLine(" --> split #{0} done, [{1} s] {2}", splitNo, checker.ProverRunTime.TotalSeconds, outcome);
}
if (CommandLineOptions.Clo.VcsDumpSplits) {
DumpDot(splitNo);
}
prover_failed = false;
switch (outcome) {
case ProverInterface.Outcome.Valid:
return;
case ProverInterface.Outcome.Invalid:
cur_outcome = Outcome.Errors;
return;
case ProverInterface.Outcome.OutOfMemory:
prover_failed = true;
if (cur_outcome != Outcome.Errors && cur_outcome != Outcome.Inconclusive)
cur_outcome = Outcome.OutOfMemory;
return;
case ProverInterface.Outcome.TimeOut:
prover_failed = true;
if (cur_outcome != Outcome.Errors && cur_outcome != Outcome.Inconclusive)
cur_outcome = Outcome.TimedOut;
return;
case ProverInterface.Outcome.Undetermined:
if (cur_outcome != Outcome.Errors)
cur_outcome = Outcome.Inconclusive;
return;
default:
Contract.Assert(false);
throw new cce.UnreachableException();
}
}
///
/// As a side effect, updates "this.parent.CumulativeAssertionCount".
///
public void BeginCheck(VerifierCallback callback, ModelViewInfo mvInfo, int no, int timeout) {
Contract.Requires(callback != null);
splitNo = no;
impl.Blocks = blocks;
checker = parent.FindCheckerFor(timeout);
lock (checker)
{
Hashtable/**/ label2absy = new Hashtable/**/();
ProverContext ctx = checker.TheoremProver.Context;
Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
bet.SetCodeExprConverter(
new CodeExprConverter(
delegate(CodeExpr codeExpr, Hashtable/**/ blockVariables, List bindings)
{
VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);
vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
vcgen.incarnationOriginMap = new Dictionary();
vcgen.CurrentLocalVariables = codeExpr.LocVars;
// codeExpr.Blocks.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
ResetPredecessors(codeExpr.Blocks);
vcgen.AddBlocksBetween(codeExpr.Blocks);
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));
int ac; // computed, but then ignored for this CodeExpr
VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
if (vcgen.CurrentLocalVariables.Length != 0)
{
Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
List boundVars = new List();
foreach (Variable v in vcgen.CurrentLocalVariables)
{
Contract.Assert(v != null);
VCExprVar ev = translator.LookupVariable(v);
Contract.Assert(ev != null);
boundVars.Add(ev);
if (v.TypedIdent.Type.Equals(Bpl.Type.Bool))
{
// add an antecedent (tickleBool ev) to help the prover find a possible trigger
vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
}
}
vce = checker.VCExprGen.Forall(boundVars, new List(), vce);
}
return vce;
}
));
var exprGen = ctx.ExprGen;
VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO);
VCExpr vc = parent.GenerateVCAux(impl, controlFlowVariableExpr, label2absy, checker.TheoremProver.Context);
Contract.Assert(vc != null);
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);
}
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local)
{
reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, cce.NonNull(this.Checker.TheoremProver.Context), parent.program);
}
else
{
reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, mvInfo, this.Checker.TheoremProver.Context, parent.program);
}
if (CommandLineOptions.Clo.TraceVerify && no >= 0)
{
Console.WriteLine("-- after split #{0}", no);
Print();
}
string desc = cce.NonNull(impl.Name);
if (no >= 0)
desc += "_split" + no;
checker.BeginCheck(desc, vc, reporter);
}
}
private void SoundnessCheck(HashSet/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) {
Contract.Requires(cce.NonNull(cache));
Contract.Requires(orig != null);
Contract.Requires(copies != null);
{
PureCollections.Tuple t = new PureCollections.Tuple(new PureCollections.Capacity(1 + copies.Count));
int i = 0;
t[i++] = orig;
foreach (Block b in copies) {
Contract.Assert(b != null);
t[i++] = b;
}
if (cache.Contains(t)) {
return;
}
cache.Add(t);
}
for (int i = 0; i < orig.Cmds.Length; ++i) {
Cmd cmd = orig.Cmds[i];
if (cmd is AssertCmd) {
int found = 0;
foreach (Block c in copies) {
Contract.Assert(c != null);
if (c.Cmds[i] == cmd) {
found++;
}
}
if (found == 0) {
throw new System.Exception(string.Format("missing assertion: {0}({1})", cmd.tok.filename, cmd.tok.line));
}
}
}
foreach (Block exit in Exits(orig)) {
Contract.Assert(exit != null);
List newcopies = new List();
foreach (Block c in copies) {
foreach (Block cexit in Exits(c)) {
Contract.Assert(cexit != null);
if (cexit.Label == exit.Label) {
newcopies.Add(cexit);
}
}
}
if (newcopies.Count == 0) {
throw new System.Exception("missing exit " + exit.Label);
}
SoundnessCheck(cache, exit, newcopies);
}
}
}
#endregion
public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/**//*!*/ label2absy, ProverContext proverContext)
{
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);
Contract.Ensures(Contract.Result() != null);
label2absy = new Hashtable/**/();
return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext);
}
protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/**//*!*/ label2absy, ProverContext proverContext) {
Contract.Requires(impl != null);
Contract.Requires(proverContext != null);
Contract.Ensures(Contract.Result() != null);
TypecheckingContext tc = new TypecheckingContext(null);
impl.Typecheck(tc);
VCExpr vc;
int assertionCount;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Structured:
vc = VCViaStructuredProgram(impl, label2absy, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Block:
vc = FlatBlockVC(impl, label2absy, false, false, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockReach:
vc = FlatBlockVC(impl, label2absy, false, true, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Local:
vc = FlatBlockVC(impl, label2absy, true, false, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockNested:
vc = NestedBlockVC(impl, label2absy, false, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.BlockNestedReach:
vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Dag:
if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags || CommandLineOptions.Clo.FixedPointEngine != null) {
vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/**/(), proverContext, out assertionCount);
} else {
vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
}
break;
case CommandLineOptions.VCVariety.DagIterative:
vc = LetVCIterative(impl.Blocks, controlFlowVariableExpr, label2absy, proverContext, out assertionCount);
break;
case CommandLineOptions.VCVariety.Doomed:
vc = FlatBlockVC(impl, label2absy, false, false, true, proverContext, out assertionCount);
break;
default:
Contract.Assert(false);
throw new cce.UnreachableException(); // unexpected enumeration value
}
CumulativeAssertionCount += assertionCount;
return vc;
}
void CheckIntAttributeOnImpl(Implementation impl, string name, ref int val) {
Contract.Requires(impl != null);
Contract.Requires(name != null);
if (!(cce.NonNull(impl.Proc).CheckIntAttribute(name, ref val) || !impl.CheckIntAttribute(name, ref val))) {
Console.WriteLine("ignoring ill-formed {:{0} ...} attribute on {1}, parameter should be an int", name, impl.Name);
}
}
public override Outcome VerifyImplementation(Implementation/*!*/ impl, VerifierCallback/*!*/ callback) {
Contract.EnsuresOnThrow(true);
if (impl.SkipVerification) {
return Outcome.Inconclusive; // not sure about this one
}
callback.OnProgress("VCgen", 0, 0, 0.0);
Stopwatch watch = new Stopwatch();
if (_print_time)
{
Console.WriteLine("Checking function {0}", impl.Name);
watch.Reset();
watch.Start();
}
ConvertCFG2DAG(impl);
SmokeTester smoke_tester = null;
if (CommandLineOptions.Clo.SoundnessSmokeTest) {
smoke_tester = new SmokeTester(this, impl, callback);
smoke_tester.Copy();
}
ModelViewInfo mvInfo;
var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);
double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;
int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits,
max_kg_splits = CommandLineOptions.Clo.VcsMaxKeepGoingSplits;
CheckIntAttributeOnImpl(impl, "vcs_max_cost", ref tmp_max_vc_cost);
CheckIntAttributeOnImpl(impl, "vcs_max_splits", ref max_splits);
CheckIntAttributeOnImpl(impl, "vcs_max_keep_going_splits", ref max_kg_splits);
if (tmp_max_vc_cost >= 0) {
max_vc_cost = tmp_max_vc_cost;
}
Outcome outcome = Outcome.Correct;
Cores = CommandLineOptions.Clo.VcsCores;
Stack work = new Stack();
List currently_running = new List();
ResetPredecessors(impl.Blocks);
work.Push(new Split(impl.Blocks, gotoCmdOrigins, this, impl));
bool keep_going = max_kg_splits > 1;
int total = 0;
int no = max_splits == 1 && !keep_going ? -1 : 0;
bool first_round = true;
bool do_splitting = keep_going || max_splits > 1;
double remaining_cost = 0.0, proven_cost = 0.0;
if (do_splitting) {
remaining_cost = work.Peek().Cost;
}
while (work.Any() || currently_running.Any()) {
bool prover_failed = false;
Split s;
if (work.Any() && currently_running.Count < Cores) {
s = work.Pop();
if (first_round && max_splits > 1) {
prover_failed = true;
remaining_cost -= s.Cost;
} else {
if (CommandLineOptions.Clo.Trace && no >= 0) {
System.Console.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...",
s.Stats, no + 1, total, 100 * proven_cost / (proven_cost + remaining_cost));
}
callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
Contract.Assert(s.parent == this);
s.BeginCheck(callback, mvInfo, no,
(keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :
keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :
CommandLineOptions.Clo.ProverKillTime);
no++;
currently_running.Add(s);
}
} else {
// Wait for one split to terminate.
var tasks = currently_running.Select(splt => splt.ProverTask).ToArray();
int index = Task.WaitAny(tasks);
s = currently_running[index];
currently_running.RemoveAt(index);
if (do_splitting) {
remaining_cost -= s.Cost;
}
s.ReadOutcome(ref outcome, out prover_failed);
if (do_splitting) {
if (prover_failed) {
// even if the prover fails, we have learned something, i.e., it is
// annoying to watch Boogie say Timeout, 0.00% a couple of times
proven_cost += s.Cost / 100;
} else {
proven_cost += s.Cost;
}
}
callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));
if (prover_failed && !first_round && s.LastChance) {
string msg = "some timeout";
if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
msg = s.reporter.resourceExceededMessage;
}
callback.OnCounterexample(s.ToCounterexample(s.Checker.TheoremProver.Context), msg);
outcome = Outcome.Errors;
break;
}
s.Checker.GoBackToIdle();
Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);
}
if (prover_failed) {
int splits = first_round && max_splits > 1 ? max_splits : max_kg_splits;
if (splits > 1) {
List tmp = Split.DoSplit(s, max_vc_cost, splits);
Contract.Assert(tmp != null);
max_vc_cost = 1.0; // for future
first_round = false;
//tmp.Sort(new Comparison(Split.Compare));
foreach (Split a in tmp) {
Contract.Assert(a != null);
work.Push(a);
total++;
remaining_cost += a.Cost;
}
if (outcome != Outcome.Errors) {
outcome = Outcome.Correct;
}
} else {
Contract.Assert( outcome != Outcome.Correct);
if (outcome == Outcome.TimedOut) {
string msg = "some timeout";
if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
msg = s.reporter.resourceExceededMessage;
}
callback.OnTimeout(msg);
} else if (outcome == Outcome.OutOfMemory) {
string msg = "out of memory";
if (s.reporter != null && s.reporter.resourceExceededMessage != null) {
msg = s.reporter.resourceExceededMessage;
}
callback.OnOutOfMemory(msg);
}
break;
}
}
}
if (outcome == Outcome.Correct && smoke_tester != null) {
smoke_tester.Test();
}
callback.OnProgress("done", 0, 0, 1.0);
if (_print_time)
{
watch.Stop();
Console.WriteLine("Total time for this method: {0}", watch.Elapsed.ToString());
}
return outcome;
}
public class ErrorReporter : ProverInterface.ErrorHandler {
Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins;
Hashtable/**//*!*/ label2absy;
List/*!*/ blocks;
protected Dictionary/*!*/ incarnationOriginMap;
protected VerifierCallback/*!*/ callback;
protected ModelViewInfo MvInfo;
internal string resourceExceededMessage;
static System.IO.TextWriter modelWriter;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(gotoCmdOrigins != null);
Contract.Invariant(label2absy != null);
Contract.Invariant(cce.NonNullElements(blocks));
Contract.Invariant(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Invariant(callback != null);
Contract.Invariant(context != null);
Contract.Invariant(program != null);
}
public static TextWriter ModelWriter {
get {
Contract.Ensures(Contract.Result() != null);
if (ErrorReporter.modelWriter == null)
ErrorReporter.modelWriter = CommandLineOptions.Clo.PrintErrorModelFile == null ? Console.Out : new StreamWriter(CommandLineOptions.Clo.PrintErrorModelFile, false);
return ErrorReporter.modelWriter;
}
}
protected ProverContext/*!*/ context;
Program/*!*/ program;
public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
Hashtable/**//*!*/ label2absy,
List/*!*/ blocks,
Dictionary/*!*/ incarnationOriginMap,
VerifierCallback/*!*/ callback,
ModelViewInfo mvInfo,
ProverContext/*!*/ context,
Program/*!*/ program) {
Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(label2absy != null);
Contract.Requires(cce.NonNullElements(blocks));
Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(callback != null);
Contract.Requires(context!=null);
Contract.Requires(program!=null);
this.gotoCmdOrigins = gotoCmdOrigins;
this.label2absy = label2absy;
this.blocks = blocks;
this.incarnationOriginMap = incarnationOriginMap;
this.callback = callback;
this.MvInfo = mvInfo;
this.context = context;
this.program = program;
}
public override void OnModel(IList/*!*/ labels, Model model) {
//Contract.Requires(cce.NonNullElements(labels));
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
if (VC.ConditionGeneration.errorModelList != null)
{
VC.ConditionGeneration.errorModelList.Add(model);
}
model.Write(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
Hashtable traceNodes = new Hashtable();
foreach (string s in labels) {
Contract.Assert(s != null);
Absy absy = Label2Absy(s);
Contract.Assert(absy != null);
if (traceNodes.ContainsKey(absy))
System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");
else
traceNodes.Add(absy, null);
}
BlockSeq trace = new BlockSeq();
Block entryBlock = cce.NonNull(this.blocks[0]);
Contract.Assert(traceNodes.Contains(entryBlock));
trace.Add(entryBlock);
Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, model, MvInfo, incarnationOriginMap, context, new Dictionary());
if (newCounterexample == null)
return;
#region Map passive program errors back to original program errors
ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;
if (returnExample != 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
callback.OnCounterexample(newCounterexample, null);
}
public override Absy Label2Absy(string label) {
//Contract.Requires(label != null);
Contract.Ensures(Contract.Result() != null);
int id = int.Parse(label);
return cce.NonNull((Absy)label2absy[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);
}
}
public class ErrorReporterLocal : ErrorReporter {
public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
Hashtable/**//*!*/ label2absy,
List/*!*/ blocks,
Dictionary/*!*/ incarnationOriginMap,
VerifierCallback/*!*/ callback,
ModelViewInfo mvInfo,
ProverContext/*!*/ context,
Program/*!*/ program)
: base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, mvInfo, context, program) // here for aesthetic purposes //TODO: Maybe nix?
{
Contract.Requires(gotoCmdOrigins != null);
Contract.Requires(label2absy != null);
Contract.Requires(cce.NonNullElements(blocks));
Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
Contract.Requires(callback != null);
Contract.Requires(context != null);
Contract.Requires(program != null);
}
public override void OnModel(IList/*!*/ labels, Model model) {
//Contract.Requires(cce.NonNullElements(labels));
// We ignore the error model here for enhanced error message purposes.
// It is only printed to the command line.
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
if (CommandLineOptions.Clo.PrintErrorModelFile != null) {
model.Write(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
}
List traceNodes = new List();
List assertNodes = new List();
foreach (string s in labels) {
Contract.Assert(s != null);
Absy node = Label2Absy(s);
if (node is Block) {
Block b = (Block)node;
traceNodes.Add(b);
} else {
AssertCmd a = (AssertCmd)node;
assertNodes.Add(a);
}
}
Contract.Assert(assertNodes.Count > 0);
Contract.Assert(traceNodes.Count == assertNodes.Count);
foreach (AssertCmd a in assertNodes) {
// find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)
foreach (Block b in traceNodes) {
if (b.Cmds.Has(a)) {
BlockSeq trace = new BlockSeq();
trace.Add(b);
Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, model, MvInfo, context);
callback.OnCounterexample(newCounterexample, null);
goto NEXT_ASSERT;
}
}
Contract.Assert(false);
throw new cce.UnreachableException(); // there was no block that contains the assert
NEXT_ASSERT: {
}
}
}
}
private void RecordCutEdge(Dictionary> edgesCut, Block from, Block to){
if (edgesCut != null)
{
if (!edgesCut.ContainsKey(from))
edgesCut.Add(from, new List());
edgesCut[from].Add(to);
}
}
public void ConvertCFG2DAG(Implementation impl, Dictionary> edgesCut = null)
{
Contract.Requires(impl != null);
impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
CurrentLocalVariables = impl.LocVars;
variable2SequenceNumber = new Hashtable/*Variable -> int*/();
incarnationOriginMap = new Dictionary();
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("original implementation");
EmitImpl(impl, false);
}
#endregion
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("after desugaring sugared commands like procedure calls");
EmitImpl(impl, true);
}
#endregion
// Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges
// below assumes that the start node has no predecessor)
impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new CmdSeq(), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))));
ResetPredecessors(impl.Blocks);
#region Convert program CFG into a DAG
#region Use the graph library to figure out where the (natural) loops are
#region Create the graph by adding the source node and each edge
Graph g = Program.GraphFromImpl(impl);
#endregion
//Graph g = program.ProcessLoops(impl);
g.ComputeLoops(); // this is the call that does all of the processing
if (!g.Reducible)
{
throw new VCGenException("Irreducible flow graphs are unsupported.");
}
#endregion
#region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements
foreach (Block header in cce.NonNull( g.Headers))
{
Contract.Assert(header != null);
IDictionary backEdgeNodes = new Dictionary();
foreach (Block b in cce.NonNull( g.BackEdgeNodes(header))) {Contract.Assert(b != null); backEdgeNodes.Add(b, null); }
#region Find the (possibly empty) prefix of assert commands in the header, replace each assert with an assume of the same condition
CmdSeq prefixOfPredicateCmdsInit = new CmdSeq();
CmdSeq prefixOfPredicateCmdsMaintained = new CmdSeq();
for (int i = 0, n = header.Cmds.Length; i < n; i++)
{
PredicateCmd a = header.Cmds[i] as PredicateCmd;
if (a != null)
{
if (a is AssertCmd) {
Bpl.AssertCmd c = (AssertCmd) a;
Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsInit.Add(b);
b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsMaintained.Add(b);
header.Cmds[i] = new AssumeCmd(c.tok,c.Expr);
} else {
Contract.Assert( a is AssumeCmd);
if (Bpl.CommandLineOptions.Clo.AlwaysAssumeFreeLoopInvariants) {
// Usually, "free" stuff, like free loop invariants (and the assume statements
// that stand for such loop invariants) are ignored on the checking side. This
// command-line option changes that behavior to always assume the conditions.
prefixOfPredicateCmdsInit.Add(a);
prefixOfPredicateCmdsMaintained.Add(a);
}
}
}
else if ( header.Cmds[i] is CommentCmd )
{
// ignore
}
else
{
break; // stop when an assignment statement (or any other non-predicate cmd) is encountered
}
}
#endregion
#region Copy the prefix of predicate commands into each predecessor. Do this *before* cutting the backedge!!
for ( int predIndex = 0, n = header.Predecessors.Length; predIndex < n; predIndex++ )
{
Block pred = cce.NonNull(header.Predecessors[predIndex]);
// Create a block between header and pred for the predicate commands if pred has more than one successor
GotoCmd gotocmd = cce.NonNull((GotoCmd)pred.TransferCmd);
Contract.Assert( gotocmd.labelNames != null); // if "pred" is really a predecessor, it may be a GotoCmd with at least one label
if (gotocmd.labelNames.Length > 1)
{
Block newBlock = CreateBlockBetween(predIndex, header);
impl.Blocks.Add(newBlock);
// if pred is a back edge node, then now newBlock is the back edge node
if (backEdgeNodes.ContainsKey(pred))
{
backEdgeNodes.Remove(pred);
backEdgeNodes.Add(newBlock,null);
}
pred = newBlock;
}
// Add the predicate commands
if (backEdgeNodes.ContainsKey(pred)){
pred.Cmds.AddRange(prefixOfPredicateCmdsMaintained);
}
else {
pred.Cmds.AddRange(prefixOfPredicateCmdsInit);
}
}
#endregion
#region Cut the back edge
foreach (Block backEdgeNode in cce.NonNull(backEdgeNodes.Keys))
{Contract.Assert(backEdgeNode != null);
Debug.Assert(backEdgeNode.TransferCmd is GotoCmd,"An node was identified as the source for a backedge, but it does not have a goto command.");
GotoCmd gtc = backEdgeNode.TransferCmd as GotoCmd;
if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length > 1 )
{
// then remove the backedge by removing the target block from the list of gotos
BlockSeq remainingTargets = new BlockSeq();
StringSeq remainingLabels = new StringSeq();
Contract.Assume( gtc.labelNames != null);
for (int i = 0, n = gtc.labelTargets.Length; i < n; i++)
{
if (gtc.labelTargets[i] != header)
{
remainingTargets.Add(gtc.labelTargets[i]);
remainingLabels.Add(gtc.labelNames[i]);
}
else
RecordCutEdge(edgesCut,backEdgeNode, header);
}
gtc.labelTargets = remainingTargets;
gtc.labelNames = remainingLabels;
}
else
{
// This backedge is the only out-going edge from this node.
// Add an "assume false" statement to the end of the statements
// inside of the block and change the goto command to a return command.
AssumeCmd ac = new AssumeCmd(Token.NoToken,Expr.False);
backEdgeNode.Cmds.Add(ac);
backEdgeNode.TransferCmd = new ReturnCmd(Token.NoToken);
if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length == 1)
RecordCutEdge(edgesCut, backEdgeNode, gtc.labelTargets[0]);
}
#region Remove the backedge node from the list of predecessor nodes in the header
BlockSeq newPreds = new BlockSeq();
foreach ( Block p in header.Predecessors )
{
if ( p != backEdgeNode )
newPreds.Add(p);
}
header.Predecessors = newPreds;
#endregion
}
#endregion
#region Collect all variables that are assigned to in all of the natural loops for which this is the header
VariableSeq varsToHavoc = new VariableSeq();
foreach (Block backEdgeNode in cce.NonNull( g.BackEdgeNodes(header)))
{
Contract.Assert(backEdgeNode != null);
foreach ( Block b in g.NaturalLoops(header,backEdgeNode) )
{
Contract.Assert(b != null);
foreach ( Cmd c in b.Cmds )
{
Contract.Assert(c != null);
c.AddAssignedVariables(varsToHavoc);
}
}
}
IdentifierExprSeq havocExprs = new IdentifierExprSeq();
foreach ( Variable v in varsToHavoc )
{
Contract.Assert(v != null);
IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
if(!havocExprs.Has(ie))
havocExprs.Add(ie);
}
// pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
// the source location for this later on
HavocCmd hc = new HavocCmd(header.tok,havocExprs);
CmdSeq newCmds = new CmdSeq();
newCmds.Add(hc);
foreach ( Cmd c in header.Cmds )
{
newCmds.Add(c);
}
header.Cmds = newCmds;
#endregion
}
#endregion
#endregion Convert program CFG into a DAG
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("after conversion into a DAG");
EmitImpl(impl, true);
}
#endregion
}
public void DesugarCalls(Implementation impl) {
foreach (Block block in impl.Blocks) {
CmdSeq newCmds = new CmdSeq();
foreach (Cmd cmd in block.Cmds) {
SugaredCmd sugaredCmd = cmd as SugaredCmd;
if (sugaredCmd != null) {
StateCmd stateCmd = sugaredCmd.Desugaring as StateCmd;
foreach (Variable v in stateCmd.Locals) {
impl.LocVars.Add(v);
}
newCmds.AddRange(stateCmd.Cmds);
}
else {
newCmds.Add(cmd);
}
}
block.Cmds = newCmds;
}
}
public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
{
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Ensures(Contract.Result() != null);
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();
Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("after creating a unified exit block");
EmitImpl(impl, true);
}
#endregion
#region Insert pre- and post-conditions and where clauses as assume and assert statements
{
CmdSeq cc = new CmdSeq();
// where clauses of global variables
lock (program.TopLevelDeclarations)
{
foreach (var gvar in program.TopLevelDeclarations.OfType())
{
if (gvar != null && gvar.TypedIdent.WhereExpr != null)
{
Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);
cc.Add(c);
}
}
}
// where clauses of in- and out-parameters
cc.AddRange(GetParamWhereClauses(impl));
// where clauses of local variables
foreach (Variable lvar in impl.LocVars) {Contract.Assert(lvar != null);
if (lvar.TypedIdent.WhereExpr != null) {
Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);
cc.Add(c);
}
}
// add cc and the preconditions to new blocks preceding impl.Blocks[0]
InjectPreconditions(impl, cc);
// append postconditions, starting in exitBlock and continuing into other blocks, if needed
exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);
}
#endregion
#region Support for stratified inlining
addExitAssert(impl.Name, exitBlock);
#endregion
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("after inserting pre- and post-conditions");
EmitImpl(impl, true);
}
#endregion
AddBlocksBetween(impl.Blocks);
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("after adding empty blocks as needed to catch join assumptions");
EmitImpl(impl, true);
}
#endregion
if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {
Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
}
mvInfo = new ModelViewInfo(program, impl);
Convert2PassiveCmd(impl, mvInfo);
#region Peep-hole optimizations
if (CommandLineOptions.Clo.RemoveEmptyBlocks){
#region Get rid of empty blocks
{
Block entryBlock = cce.NonNull( impl.Blocks[0]);
RemoveEmptyBlocks(entryBlock);
impl.PruneUnreachableBlocks();
}
#endregion Get rid of empty blocks
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
{
Console.WriteLine("after peep-hole optimizations");
EmitImpl(impl, true);
}
#endregion
}
#endregion Peep-hole optimizations
if (CommandLineOptions.Clo.ExpandLambdas)
{
List axioms;
List functions;
LambdaHelper.Desugar(impl, out axioms, out functions);
lock (program.TopLevelDeclarations)
{
program.TopLevelDeclarations.AddRange(functions);
}
if (axioms.Count > 0) {
CmdSeq cmds = new CmdSeq();
foreach (Expr ax in axioms) {
Contract.Assert(ax != null);
cmds.Add(new AssumeCmd(ax.tok, ax));
}
Block entryBlock = cce.NonNull( impl.Blocks[0]);
cmds.AddRange(entryBlock.Cmds);
entryBlock.Cmds = cmds;
// Make sure that all added commands are passive commands.
Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable());
TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,
ComputeOldExpressionSubstitution(impl.Proc.Modifies));
}
}
HandleSelectiveChecking(impl);
// #region Constant Folding
// #endregion
// #region Debug Tracing
// if (CommandLineOptions.Clo.TraceVerify)
// {
// Console.WriteLine("after constant folding");
// EmitImpl(impl, true);
// }
// #endregion
return gotoCmdOrigins;
}
private static void HandleSelectiveChecking(Implementation impl)
{
if (QKeyValue.FindBoolAttribute(impl.Attributes, "selective_checking") ||
QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "selective_checking")) {
var startPoints = new List();
foreach (var b in impl.Blocks) {
foreach (Cmd c in b.Cmds) {
var p = c as PredicateCmd;
if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here")) {
startPoints.Add(b);
break;
}
}
}
var blocksToCheck = new HashSet();
foreach (var b in startPoints) {
var todo = new Stack();
var wasThere = blocksToCheck.Contains(b);
todo.Push(b);
while (todo.Count > 0) {
var x = todo.Pop();
if (blocksToCheck.Contains(x)) continue;
blocksToCheck.Add(x);
var ex = x.TransferCmd as GotoCmd;
if (ex != null)
foreach (Block e in ex.labelTargets)
todo.Push(e);
}
if (!wasThere) blocksToCheck.Remove(b);
}
foreach (var b in impl.Blocks) {
if (blocksToCheck.Contains(b)) continue;
var newCmds = new CmdSeq();
var copyMode = false;
foreach (Cmd c in b.Cmds) {
var p = c as PredicateCmd;
if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "start_checking_here"))
copyMode = true;
var asrt = c as AssertCmd;
if (copyMode || asrt == null)
newCmds.Add(c);
else
newCmds.Add(AssertTurnedIntoAssume(asrt));
}
b.Cmds = newCmds;
}
}
}
// Used by stratified inlining
protected virtual void addExitAssert(string implName, Block exitBlock)
{
}
public virtual Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary> extractLoopMappingInfo)
{
// Construct the set of inlined procs in the original program
var inlinedProcs = new HashSet();
foreach (var decl in program.TopLevelDeclarations)
{
if (decl is Procedure)
{
if (!(decl is LoopProcedure))
{
var p = decl as Procedure;
inlinedProcs.Add(p.Name);
}
}
}
return extractLoopTraceRec(
new CalleeCounterexampleInfo(cex, new List