14 Advanced topics and tool internals🔗

This chapter describes the machinery between a Boogie program and the SMT solver: how the program is lowered, how types are encoded, which declarations survive to the solver, how the verification condition is split, and which transformations are approximations rather than faithful translations.

None of this is described in This is Boogie 2. The paper’s section 11 says only that “the Boogie language does not assign any formal meaning to the attributes” and leaves the rest to the tools. Everything below therefore comes from the implementation: Source/ExecutionEngine/ExecutionEngine.cs for the pipeline, Source/Core/Monomorphization.cs for type encoding, Source/VCGeneration/Prune/ for pruning, Source/VCGeneration/Splits/ for splitting, Source/VCExpr/QuantifierInstantiationEngine.cs for pool instantiation, and Source/Provers/SMTLib/ for the solver interface.

Throughout this chapter, /print-family output is shown with its two-line version and command-line banner removed, and long SMT-LIB and /traceverify dumps are shown as excerpts. Everything else is verbatim.

14.1 The verification pipeline🔗

Boogie’s pipeline has two halves. The first runs once over the whole program; the second runs once per implementation and is what actually produces a verification condition.

14.1.1 Whole-program phases🔗

In order, as driven by ExecutionEngine.ProcessProgram:

1. Parse. All input files (plus any /lib: libraries) are parsed and concatenated into one Program. /print:<file> dumps the program here, before resolution.

2. Resolve. Names are bound. /noResolve stops before this.

3. Type check. Includes a function-dependency check — call cycles among {:inline} and {:define} functions are rejected with Call cycle detected among functions: ... — and collection of implicit modifies clauses. /noTypecheck stops before this.

4. Choose a type encoding and, if needed, monomorphise. See Type encodings and monomorphisation.

5. Civl type check, after which /print:<file> combined with /printDesugared dumps the program, already monomorphised.

6. Control-flow-graph dump (/printCFG:<prefix>, Graphviz, one file <prefix>.<impl>.dot per implementation). Note that this happens before the Civl rewrite below, not after it.

7. Civl rewrite. Layered concurrency constructs are desugared into plain Boogie. /civlDesugaredFile:<file> dumps the result.

8. Measure desugaring (/printMeasureDesugaring).

9. Dead variable elimination and block coalescing (/coalesceBlocks:0 disables the latter).

10. Inlining of calls to procedures marked {:inline N}. /printInlined dumps each implementation afterwards.

11. Lambda lifting (/printLambdaLifting), abstract interpretation (/infer), loop unrolling (/loopUnroll:<n>) and loop extraction (/extractLoops). /printInstrumented dumps the program here.

12. Computation of the pruning dependency graph (Pruner.ComputeDeclarationDependencies), which returns null immediately unless /prune:1 was given.

14.1.2 Per-implementation phases🔗

Each implementation is then turned into one or more verification conditions. /traceverify prints the intermediate program after each step, and its banner lines are the authoritative names of the phases (the first is emitted once for the whole program, the rest once per implementation):

Desugaring of lambda expressions produced 0 functions and 0 axioms:

after desugaring sugared commands like procedure calls

after conversion into a DAG

after creating a unified exit block

after inserting pre- and post-conditions

after adding empty blocks as needed to catch join assumptions

after conversion to passive commands

after peep-hole optimizations

In more detail:

1. Desugar structured statements. if, while, break and goto become a flat list of labelled blocks. This step is performed lazily by the printer as well, so /print:- /printUnstructured shows blocks even under /noResolve.

2. Desugar calls. Each call becomes: assert the preconditions, havoc the modified globals and out-parameters, assume the postconditions.

3. Convert the CFG to a DAG (“loop cutting”). Back edges are removed. At each loop head the invariants become an assert on entry, then a havoc of everything the loop can modify, then an assume of the invariants; the back edge becomes assert of the invariants followed by assume false.

4. Create a unified exit block, then inject pre- and postconditions and where clauses as assume/assert.

5. Add empty blocks between blocks with multiple predecessors, so that join assumptions have somewhere to live.

6. Live variable analysis (/liveVariableAnalysis:0 disables it).

7. Passify: convert to a passive (assignment-free, SSA) program. Each assignment x := e becomes assume x#AT#k == e’.

8. Peep-hole optimisation: remove empty blocks (/removeEmptyBlocks:0 disables).

9. Split into parts (see Splitting the verification condition).

10. Prune: keep only the declarations reachable from each part (Checker.Setup asks the part for its PrunedDeclarations).

11. Generate the VC by weakest preconditions over the DAG, as a let-bound expression per block.

12. Pool-based quantifier instantiation, if the implementation contains a usable {:add_to_pool} (see the conditions below).

13. Solve: emit SMT-LIB and call the solver.

14.1.3 Watching a program go through the pipeline🔗

var g: int;

procedure {:inline 1} Bump()

modifies g;

ensures g == old(g) + 1;

{

g := g + 1;

}

procedure Main()

modifies g;

{

var i: int;

i := 0;

while (i < 3)

invariant i <= 3;

{

call Bump();

i := i + 1;

}

assert i == 3;

}

After desugaring the structured statements (/print:- /printUnstructured):

implementation Main()

{

var i: int;

/*** structured program:

i := 0;

while (i < 3)

invariant i <= 3;

{

call Bump();

i := i + 1;

}

assert i == 3;

**** end structured program */

anon0:

i := 0;

goto anon3_LoopHead;

anon3_LoopHead:

assert i <= 3;

goto anon3_LoopDone, anon3_LoopBody;

anon3_LoopBody:

assume {:partition} i < 3;

call Bump();

i := i + 1;

goto anon3_LoopHead;

anon3_LoopDone:

assume {:partition} 3 <= i;

goto anon2;

anon2:

assert i == 3;

return;

}

After inlining Bump and cutting the loop (/traceverify, phase “after conversion into a DAG”):

implementation Main()

{

var i: int;

var inline$Bump$0$g: int;

0:

goto anon0;

anon0:

i := 0;

assert i <= 3;

goto anon3_LoopHead;

anon3_LoopHead:

havoc i, g, inline$Bump$0$g;

assume i <= 3;

goto anon3_LoopDone, anon3_LoopBody;

anon3_LoopBody:

assume {:partition} i < 3;

goto inline$Bump$0$Entry;

inline$Bump$0$Entry:

inline$Bump$0$g := g;

goto inline$Bump$0$anon0;

inline$Bump$0$anon0:

g := g + 1;

goto inline$Bump$0$Return;

inline$Bump$0$Return:

assert g == inline$Bump$0$g + 1;

goto anon3_LoopBody$1;

anon3_LoopBody$1:

i := i + 1;

assert i <= 3;

assume false;

return;

anon3_LoopDone:

assume {:partition} 3 <= i;

assert i == 3;

return;

}

The three ways the loop invariant is used are all visible here: asserted on entry, assumed after the havoc, and asserted again before the cut.

And after passification (/printPassive:<file>):

implementation Main()

{

var i: int;

var inline$Bump$0$g: int;

var i#AT#0: int;

var g#AT#0: int;

var inline$Bump$0$g#AT#0: int;

var g#AT#1: int;

var i#AT#1: int;

PreconditionGeneratedEntry:

goto anon0;

anon0:

assert 0 <= 3;

goto anon3_LoopHead;

anon3_LoopHead:

assume i#AT#0 <= 3;

goto anon3_LoopDone, anon3_LoopBody;

anon3_LoopBody:

assume {:partition} i#AT#0 < 3;

goto inline$Bump$0$anon0;

inline$Bump$0$anon0:

assume g#AT#1 == g#AT#0 + 1;

goto inline$Bump$0$Return;

inline$Bump$0$Return:

assert g#AT#1 == g#AT#0 + 1;

goto anon3_LoopBody$1;

anon3_LoopBody$1:

assume i#AT#1 == i#AT#0 + 1;

assert i#AT#1 <= 3;

assume false;

return;

anon3_LoopDone:

assume {:partition} 3 <= i#AT#0;

assert i#AT#0 == 3;

goto ;

}

Note that the havoc at the loop head has disappeared: havocking a variable in a passive program is exactly “start a new incarnation”, so it costs nothing. The trailing goto ; is a printing artifact of a block whose successors were all removed.

14.1.4 Which flag prints which intermediate form🔗

Three details of this table are worth spelling out. /printPassive takes an argument, so it is written /printPassive:<file>. /printPruned:<file> and /printSplit:<file> are the same option: both set PrintSplitFile, and the argument is a filename prefix, not a file (the output goes to <prefix>-<name>.spl, unless the prefix is -, which means the console). And Split.DumpDot writes the /vcsDumpSplits output as <implementation>.split.<n>.dot and <implementation>.split.<n>.bpl in the current directory.

14.2 Type encodings and monomorphisation🔗

SMT-LIB is many-sorted and has no polymorphism. A Boogie program with type variables therefore has to be encoded. Boogie supports three encodings, selected with /typeEncoding:<t>:

• m — monomorphic (the default). The program is monomorphised: every polymorphic declaration is replicated once per type instance actually used, and the result is emitted using native SMT sorts.

• p — predicates. All values live in one uninterpreted sort T@U. A function type : T@U -> T@T recovers the type of a value, and axioms constrain it.

• a — arguments. All values live in T@U, and every polymorphic function takes its type arguments as extra explicit parameters of sort T@T.

14.2.1 How the encoding is actually chosen🔗

The option is not the last word. Immediately after type checking, ExecutionEngine.ResolveAndTypecheck does this:

1. If MonomorphismChecker.IsMonomorphic(program) holds, the encoding is forced to monomorphic, overriding whatever /typeEncoding said.

2. Otherwise, if the requested encoding is monomorphic, the program is run through Monomorphizer.Monomorphize, which either succeeds or aborts the whole run.

3. Otherwise (a genuinely polymorphic program with p or a), two features are rejected outright: datatypes (Datatypes only supported with monomorphic encoding) and {:define} functions (Functions with :define attribute only supported with monomorphic encoding).

The order matters. A program whose only datatype is monomorphic passes step 1, so the encoding is silently switched to m and /typeEncoding:p succeeds:

datatype Color { Red(), Green() }

procedure P()

{

var c: Color;

c := Red();

assert c is Red;

}

boogie /typeEncoding:p dtmono.bpl

Boogie program verifier finished with 1 verified, 0 errors

The error appears only when the program is genuinely polymorphic — as it is when the datatype itself takes type parameters, or when some unrelated declaration does.

A program counts as already monomorphic when it contains no declaration with type parameters, no binder (quantifier or lambda) with type parameters, no map type with type parameters, and no type constructor of arity greater than zero. The last clause has a carve-out: a type constructor carrying a {:builtin "..."} string is exempt, because it is mapped directly onto a solver sort.

So /typeEncoding:p on a monomorphic program does nothing at all:

function f(x: int): int;

axiom (forall x: int :: f(x) == x + 1);

procedure P()

{

assert f(1) == 2;

}

boogie /typeEncoding:p /proverLog:log.smt2 monoprog.bpl

produces (declare-fun f (Int) Int) and no occurrence of T@U anywhere in the log.

14.2.2 Monomorphisation🔗

Monomorphisation replaces each polymorphic declaration by one copy per type instantiation reachable from the program. Given

function Id<T>(x: T): T { x }

procedure P()

{

assert Id(3) == 3;

assert Id(true);

}

/print:- /printDesugared shows the program after the transformation:

procedure P();

implementation P()

{

assert Id_3(3) == 3;

assert Id_5(true);

}

function Id_3(x: int) : int

uses {

axiom (forall x: int :: { Id_3(x) } Id_3(x) == x);

axiom (forall x: int :: { Id_3(x) } Id_3(x) == x);

}

function Id_5(x: bool) : bool

uses {

axiom (forall x: bool :: { Id_5(x) } Id_5(x) == x);

axiom (forall x: bool :: { Id_5(x) } Id_5(x) == x);

}

axiom (forall x: int :: { Id_3(x) } Id_3(x) == x);

axiom (forall x: bool :: { Id_5(x) } Id_5(x) == x);

The instance names are the original name plus an internal counter, so they are not stable across edits to the program. The duplication of each definition axiom inside the uses block is a printing artifact of monomorphisation; the SMT log contains each axiom once.

Datatypes always take this route, because the alternative encodings cannot represent them. A polymorphic datatype is monomorphised into one datatype per instance:

datatype Option<T> { None(), Some(val: T) }

procedure P()

{

var o: Option int;

o := Some(3);

assert o is Some;

assert o->val == 3;

}

implementation P()

{

var o: Option_29;

o := Some_29(3);

assert o is Some_29;

assert o->val == 3;

}

datatype Option_29 {

None_29(),

Some_29(val: int)

}

and asking for another encoding fails:

boogie /typeEncoding:p dt.bpl

Datatypes only supported with monomorphic encoding

14.2.3 When monomorphisation fails🔗

Monomorphisation is a fixpoint over type instantiations, so it only terminates when the set of instantiations is finite. MonomorphizableChecker reports one of two failures — unhandled polymorphic features detected and expanding type cycle detected — and both are fatal: nothing is verified. The precise rule that decides between them is a property of the program’s types rather than of the pipeline, and is stated with worked examples in When monomorphisation fails.

What matters here is the consequence: this is the one situation in which the other two encodings earn their keep. The expanding-cycle program

type Box _;

function box<T>(x: T): Box T;

procedure A<T>(i: T)

{

call A(box(i));

}

is rejected by the default pipeline, but both

boogie /typeEncoding:p mono-cycle2.bpl

and /typeEncoding:a verify it:

Boogie program verifier finished with 1 verified, 0 errors

14.2.4 What the three encodings look like at the solver🔗

Take the Id example above and log the query for each encoding.

boogie /typeEncoding:m /proverLog:log-m.smt2 poly.bpl

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun Id_3 (Int) Int)

(declare-fun Id_5 (Bool) Bool)

(assert (forall ((x Int) ) (! (= (Id_3 x) x)

:qid |polybpl.1:16|

:skolemid |0|

:pattern ( (Id_3 x))

)))

(assert (forall ((x@@0 Bool) ) (! (= (Id_5 x@@0) x@@0)

:qid |polybpl.1:16|

:skolemid |0|

:pattern ( (Id_5 x@@0))

)))

Native sorts, one symbol per instance.

boogie /typeEncoding:p /proverLog:log-p.smt2 poly.bpl

(declare-sort |T@U| 0)

(declare-sort |T@T| 0)

(declare-fun real_pow (Real Real) Real)

(declare-fun UOrdering2 (|T@U| |T@U|) Bool)

(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun Id (T@U) T@U)

(declare-fun U_2_int (T@U) Int)

(declare-fun U_2_bool (T@U) Bool)

(declare-fun type (T@U) T@T)

(declare-fun int_2_U (Int) T@U)

(declare-fun Ctor (T@T) Int)

(declare-fun intType () T@T)

(declare-fun bool_2_U (Bool) T@U)

(declare-fun boolType () T@T)

(assert  (and (and (and (and (and (and (and (and (forall ((arg0 T@U) ) (! (let ((T (type arg0)))

(=> (= (type arg0) T) (= (type (Id arg0)) T)))

:qid |funType:Id|

:pattern ( (Id arg0))

)) (forall ((arg0@@0 Int) ) (! (= (U_2_int (int_2_U arg0@@0)) arg0@@0)

:qid |typeInv:U_2_int|

:pattern ( (int_2_U arg0@@0))

))) (= (Ctor intType) 0)) (forall ((x T@U) ) (!  (=> (= (type x) intType) (= (int_2_U (U_2_int x)) x))

:qid |cast:U_2_int|

:pattern ( (U_2_int x))

))) ...

(assert (forall ((x@@1 T@U) ) (! (= (Id x@@1) x@@1)

:qid |polybpl.1:16|

:skolemid |0|

:pattern ( (Id x@@1))

)))

One Id, one universe sort T@U, a type function, and a boxing pair int_2_U/U_2_int per Boogie type.

boogie /typeEncoding:a /proverLog:log-a.smt2 poly.bpl

(declare-sort |T@U| 0)

(declare-sort |T@T| 0)

(declare-fun real_pow (Real Real) Real)

(declare-fun UOrdering2 (|T@U| |T@U|) Bool)

(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun Id (T@T T@U) T@U)

(assert (forall ((x T@U) (T T@T) ) (! (= (Id T x) x)

:qid |polybpl.1:16|

:skolemid |0|

:pattern ( (Id T x))

)))

Here Id takes its type argument explicitly, so no type function is needed — but the boxing remains, and the assertion Id(3) == 3 comes out as

(= (U_2_int (Id intType (int_2_U 3))) 3)

The practical consequence: m gives the solver native integers, booleans, bitvectors and arrays; p and a bury everything in one uninterpreted sort with explicit boxing and unboxing functions, which is dramatically worse for arithmetic and array reasoning. Prefer m, and reach for p or a only when monomorphisation genuinely fails.

14.2.5 Maps: theory of arrays versus axioms🔗

With the monomorphic encoding, map types are emitted as SMT arrays. For

procedure P(a: [int]int)

{

assert a[1 := 5][1] == 5;

}

boogie /proverLog:m1.smt2 map1.bpl

logs

(declare-fun a () (Array Int Int))

...

(=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (= (ControlFlow 0 2) (- 0 1)) (= (select (store a 1 5) 1) 5))))

/useArrayAxioms switches to an uninterpreted sort plus explicit select/store axioms:

boogie /useArrayAxioms /proverLog:m2.smt2 map1.bpl

(declare-sort |T@[Int]Int| 0)

(declare-fun |Select__T@[Int]Int_| (|T@[Int]Int| Int) Int)

(declare-fun |Store__T@[Int]Int_| (|T@[Int]Int| Int Int) |T@[Int]Int|)

(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?x2 Int)) (! (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| ?x0 ?x1 ?x2) ?x1)  ?x2) :weight 0)))

(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?y1 Int) ( ?x2 Int)) (! (=>  (not (= ?x1 ?y1)) (= (|Select__T@[Int]Int_| (|Store__T@[Int]Int_| ?x0 ?x1 ?x2) ?y1) (|Select__T@[Int]Int_| ?x0 ?y1))) :weight 0)))

(declare-fun a () |T@[Int]Int|)

One sort and one Select/Store pair, with the two select-over-store axioms, are emitted per map type that occurs in the program. The solver’s array decision procedure is then unavailable, so only what these axioms entail can be derived. /useArrayAxioms is meaningful only with the monomorphic encoding (CommandLineOptions.UseArrayTheory is !useArrayAxioms && TypeEncodingMethod == Monomorphic); the p and a encodings always use axioms.

14.3 Pruning🔗

Because SMT solvers are unstable, an axiom that is irrelevant to the property at hand can still change whether that property is proved. Pruning removes, per verification condition, every constant, function and axiom that the VC cannot reach. The declaration forms that feed it — uses clauses, hideable axioms, revealed functions and the {:include_dep} and {:keep} attributes — are described in Top-level declarations; this section is about what the pruner does with them.

14.3.1 /prune defaults to off🔗

CommandLineOptions.Prune is declared as public bool Prune { get; set; } with no initialiser, so it is false unless /prune:1 appears on the command line. Every example in this section therefore passes /prune:1 explicitly, and so should you. (/smoke also forces pruning off.)

14.3.2 What pruning keeps🔗

Pruning is a reachability computation on a graph whose nodes are the axioms, functions and constants of the program.

• The outgoing edges of a declaration point at every function and constant it mentions. Axioms, functions with bodies, and constants with uses clauses all have them.

• The incoming edges of an axiom come from its triggers: an axiom (forall x, y :: {P(x,y), Q(y)} {R(x)} ...) is reachable either from the pair (P, Q) together, or from R alone. A multi-term trigger becomes a merge node that is only traversable once all its sources are reached.

• The roots are the functions and constants mentioned in the blocks of the VC, plus any declaration carrying {:keep}.

• For a forall axiom that has triggers (or an exists in negated position), the body contributes no incoming edges at all — only the triggers do. An axiom with no triggers falls back to its body, so it is reachable from everything the body mentions in a positive position.

Global variables, type constructors, type synonyms, procedures, implementations and datatype constructor declarations are never pruned.

function f(x: int): int uses {

axiom (forall x: int :: {f(x)} f(x) == x + 1);

}

function g(x: int): int uses {

axiom (forall x: int :: {g(x)} g(x) == x + 2);

}

procedure UsesF()

{

assert f(1) == 2;

}

boogie /prune:1 /proverLog:log.smt2 prune2.bpl

The log contains only what UsesF can reach:

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun f (Int) Int)

(assert (forall ((x Int) ) (! (= (f x) (+ x 1))

:qid |prune2bpl.2:17|

:skolemid |0|

:pattern ( (f x))

)))

(push 1)

(declare-fun ControlFlow (Int Int) Int)

Without /prune:1, g and its axiom appear as well.

14.3.3 uses clauses🔗

An axiom written at top level is an independent declaration; an axiom written in a uses clause belongs to the function or constant it is attached to, and is pruned together with it. The grammar attaches uses to constants and functions:

Consts

= "const" { Attribute } [ "unique" ] IdsType

( ";" | "uses" "{" { Axiom } "}" ) .

/* Function, elided */

[ "revealed" ] "function" { Attribute } Ident [ TypeParams ]

"(" [ VarOrType { "," VarOrType } ] ")"

( "returns" "(" VarOrType ")" | ":" Type )

( "{" Expression "}" [ "uses" "{" { Axiom } "}" ]

| "uses" "{" { Axiom } "}"

| ";"

) .

uses is what makes pruning usable: without it, an axiom’s only incoming edges are its triggers, so an untriggered axiom about a constant is never reachable and is always dropped. This is what the Test/pruning/UsesClauses.bpl regression demonstrates (reproduced here without its // RUN header, so the line numbers differ from the original):

const unique four: int;

const unique ProducerConst: bool uses {

axiom four == 4;

}

function ConsumerFunc(x: int): int;

function ProducerFunc(x: int): bool uses {

axiom (forall x: int :: ConsumerFunc(x) == 3);

}

procedure hasAxioms()

requires ProducerFunc(2);

requires ProducerConst;

ensures ConsumerFunc(4) == 3;

ensures four == 4;

{

}

procedure doesNotHaveAxioms()

ensures ConsumerFunc(4) == 3;

ensures four == 4;

{

}

boogie /prune:1 /errorTrace:0 uses.bpl

uses.bpl(24,1): Error: a postcondition could not be proved on this return path

uses.bpl(21,3): Related location: this is the postcondition that could not be proved

uses.bpl(24,1): Error: a postcondition could not be proved on this return path

uses.bpl(22,3): Related location: this is the postcondition that could not be proved

Boogie program verifier finished with 1 verified, 2 errors

hasAxioms mentions ProducerFunc and ProducerConst in its preconditions, which pulls in their uses axioms; doesNotHaveAxioms does not, so both of its postconditions fail.

14.3.4 Escape hatches: {:include_dep} and {:keep}🔗

{:include_dep} on an axiom gives it an incoming edge from every declaration it references, not just from its triggers. It exists for migration: mark all axioms with it, turn pruning on, then remove the attributes one at a time as you add uses clauses.

function f1(x: int): int;

function Q(x: int): bool;

function R(x: int): bool;

axiom (forall x: int :: Q(f1(x)));

procedure NoDep(x: int)

requires R(x);

ensures Q(f1(x));   // fails: the axiom is not reachable

{

}

function f2(x: int): int;

axiom {:include_dep} (forall x: int :: Q(f2(x)));

procedure WithDep(x: int)

requires R(x);

ensures Q(f2(x));   // proved: {:include_dep} adds an edge from f2

{

}

boogie /prune:1 /errorTrace:0 incdep.bpl

incdep.bpl(11,1): Error: a postcondition could not be proved on this return path

incdep.bpl(9,3): Related location: this is the postcondition that could not be proved

Boogie program verifier finished with 1 verified, 1 error

The attribute is subject to the trigger rule above: on a forall axiom that does have a trigger, the body’s incoming edges — including the ones {:include_dep} would add — are discarded, and only the trigger counts. Test/pruning/IncludeDep.bpl exercises exactly that corner.

{:keep} is undocumented in /attrHelp. A declaration carrying it is added to the root set, so it and everything it reaches survive unconditionally:

function f(x: int): int;

function g(x: int): int;

axiom {:keep} (forall x: int :: {g(x)} g(x) == x + 2);

procedure UsesF()

{

assert f(1) == f(1);

}

boogie /prune:1 /proverLog:keep.smt2 keep.bpl

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun g (Int) Int)

(assert (forall ((x Int) ) (! (= (g x) (+ x 2))

:qid |keepbpl.4:23|

:skolemid |0|

:pattern ( (g x))

)))

(push 1)

(declare-fun ControlFlow (Int Int) Int)

(declare-fun f (Int) Int)

14.3.5 Inspecting the result🔗

/printSplit:<prefix> /printSplitDeclarations writes, per VC part, the part’s blocks followed by the declarations that survived pruning:

boogie /prune:1 /printSplit:p /printSplitDeclarations prune2.bpl

implementation UsesF--1()

{

PreconditionGeneratedEntry:

goto anon0;

anon0:

assert f(1) == 2;

return;

}

function f(x: int) : int

uses {

axiom (forall x: int :: { f(x) } f(x) == x + 1);

}

procedure UsesF();

implementation UsesF()

{

assert f(1) == 2;

}

Split.PrintSplitDeclarations returns immediately unless both /prune:1 and /printSplitDeclarations are given, so without /prune:1 you still get the part’s blocks but the declaration listing is silently empty — a good way to notice that you forgot /prune:1.

14.4 Hiding and revealing function definitions🔗

Pruning also drives an explicit opacity mechanism: a function’s defining axiom can be marked as suppressible, and statements in an implementation can turn it off and on. The statement forms are catalogued in hide, reveal, push and pop and the declaration modifiers in Top-level declarations; what follows is what they mean.

14.4.1 Syntax🔗

Three pieces of grammar are involved. An axiom may be prefixed with hideable:

Axiom

= [ "hideable" ] "axiom" { Attribute } Proposition ";" .

A function may be prefixed with revealed:

[ "revealed" ] "function" { Attribute } Ident ...

and four commands manipulate the current state:

LabelOrCmd

= ( ( "reveal" | "hide" ) ( ident | "*" ) ";"

| "pop" ";"

| "push" ";"

| ... ) .

hide/reveal take either a single function name or * for “all functions”. push and pop save and restore the whole hide/reveal state.

14.4.2 Semantics🔗

Only hideable axioms can be suppressed. When the pruner walks from a function to one of its axioms, it refuses to traverse the edge if the axiom is hideable and the function is not revealed. A function declared revealed is always revealed, whatever the commands say.

function plain(x: int): int uses {

axiom (forall x: int :: {plain(x)} plain(x) == x + 1);

}

function hid(x: int): int uses {

hideable axiom (forall x: int :: {hid(x)} hid(x) == x + 1);

}

revealed function always(x: int): int uses {

hideable axiom (forall x: int :: {always(x)} always(x) == x + 1);

}

procedure P()

{

hide *;

assert plain(1) == 2;    // not hideable, so still available

}

procedure Q()

{

hide *;

assert hid(1) == 2;      // hidden

}

procedure R()

{

hide *;

assert always(1) == 2;   // declared 'revealed', never hidden

}

boogie /prune:1 /errorTrace:0 /vcsSplitOnEveryAssert reveal2.bpl

reveal2.bpl(22,3): Error: this assertion could not be proved

Boogie program verifier finished with 2 verified, 1 error

14.4.3 The granularity is one verification condition, not one statement🔗

This is the single most surprising thing about the mechanism. The dataflow analysis computes a hide/reveal state at every command, but then it takes the state at each assert in the VC and merges them by taking the union of what is revealed. One VC therefore has one set of hidden functions; a function revealed anywhere in the VC is revealed everywhere in it.

function fib(n: int): int uses {

hideable axiom (forall n: int :: {fib(n)}

fib(n) == if n <= 1 then n else fib(n - 1) + fib(n - 2));

}

procedure Opaque()

{

hide fib;

assert fib(2) == 1;   // definition is hidden here

}

procedure Transparent()

{

assert fib(2) == 1;   // definition is visible by default

}

procedure Scoped()

{

hide *;

push;

reveal fib;

assert fib(2) == 1;   // ok, revealed inside the scope

pop;

assert fib(3) == 2;   // hidden again

}

boogie /prune:1 /errorTrace:0 reveal.bpl

reveal.bpl(9,3): Error: this assertion could not be proved

Boogie program verifier finished with 2 verified, 1 error

Scoped verifies — both of its assertions get fib’s definition, because one of them revealed it. Splitting the VC gives the finer granularity:

boogie /prune:1 /errorTrace:0 /vcsSplitOnEveryAssert reveal.bpl

reveal.bpl(9,3): Error: this assertion could not be proved

reveal.bpl(24,3): Error: this assertion could not be proved

Boogie program verifier finished with 1 verified, 2 errors

This is why Test/pruning/Reveal.bpl runs with /vcsSplitOnEveryAssert. If you use hide/reveal for anything finer than whole procedures, you need splitting as well.

One further consequence: hide and reveal do nothing at all without /prune:1.

14.4.4 There is no {:opaque} attribute🔗

Boogie has no {:opaque} attribute. The identifier does appear in Boogie files generated by Dafny (Test/dafny/Seq.bpl has procedure {:opaque} CheckWellformed$$Seq...), but nothing in Source/ ever reads it: it is inert metadata that Dafny attaches for its own purposes. The same is true of {:opaque_reveal}. If you want opacity in Boogie, use hideable axiom plus hide/reveal.

14.5 Pool-based quantifier instantiation🔗

Trigger-based instantiation is the solver’s job and is famously unpredictable. Boogie offers an alternative for cases where you know exactly which instances you need: you name a pool, you say which terms go into it, and Boogie instantiates the quantifier at those terms before the VC ever reaches the solver. The two attributes are catalogued in Attributes; the standard library’s Vec_Concat, Vec_Slice and Loc_New are real users of the mechanism (The standard library).

14.5.1 {:pool} and {:add_to_pool}🔗

{:pool "name"} goes on a bound variable of a quantifier or lambda, and says “instantiate this variable with the terms in pool name”.

{:add_to_pool "name", e0, e1, ...} goes on an assert or assume command, where the expressions are substituted with the variable incarnations in force at that command; or on a quantifier, where the expressions are substituted with fresh Skolem constants when the quantifier is skolemised.

function F(x: int): bool;

procedure P()

{

assume (forall {:pool "L"} x: int :: F(x - 1));

assert {:add_to_pool "L", 1} F(0);

}

boogie /proverLog:pool1.smt2 pool1.bpl

(assert (not

(=> (= (ControlFlow 0 0) 3) (=> true (let ((quantifierBinding0 (F (- 1 1))))

(let ((anon0_correct  (=> (and quantifierBinding0 (= (ControlFlow 0 2) (- 0 1))) (F 0))))

(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 3) 2) anon0_correct)))

PreconditionGeneratedEntry_correct)))))

))

(check-sat)

The quantifier is gone. It has been replaced by the single instance F(1 - 1).

14.5.2 What the engine does🔗

QuantifierInstantiationEngine.Execute runs a fixpoint:

1. Collect {:add_to_pool} sources from the commands of the implementation.

2. Skolemise the VC. A quantifier that behaves universally in the goal (or existentially in an assumption) is replaced by fresh Skolem constants; its {:add_to_pool} attributes then feed those constants into the named pools.

3. Repeatedly: move the new pool contents into the accumulated pools, instantiate every bound quantifier whose pool labels overlap the accumulated pools, skolemise the resulting instances, and repeat until no new terms appear.

4. Rewrite. A forall becomes the conjunction of its instances; an exists becomes the disjunction of its instances.

A quantifier is only eligible if every one of its bound variables carries at least one {:pool} label, and it has no type parameters. Instances whose term type does not match the bound variable’s type are discarded, so a pool name may safely be shared between variables of different types.

Lambdas participate too: (lambda {:pool "A"} pa: PA :: ...) has its defining axiom instantiated at the pool terms rather than left as a quantifier, and the instances are emitted as an antecedent of the whole VC.

14.5.3 /keepQuantifier🔗

By default the original quantifier is dropped once instances exist. This is what makes the technique predictable, and also what makes it incomplete: anything not derivable from your instances is not derivable at all. /keepQuantifier keeps the quantifier alongside the instances:

boogie /keepQuantifier /proverLog:pool1k.smt2 pool1.bpl

(=> (= (ControlFlow 0 0) 3) (=> true (let ((quantifierBinding0  (and (forall ((x Int) ) (! (F (- x 1))

:qid |pool1bpl.5:30|

:skolemid |0|

)) (F (- 1 1)))))

14.5.4 Limits and traps🔗

• The whole engine is skipped unless the implementation contains at least one {:add_to_pool} whose pool name has been registered by some {:pool} annotation and whose expression type matches a type registered for that pool. Otherwise the quantifier is emitted verbatim.

• Because a pool-annotated quantifier usually has no triggers, “emitted verbatim” means the solver gets an untriggered quantifier, and Boogie runs Z3 with smt.mbqi false. The result is normally an unproved assertion, not a silent fall-back:

  function F(x: int): bool;

  procedure NoSource()

  {

  assume (forall {:pool "L"} x: int :: F(x - 1));

  assert F(0);

  }

  boogie /errorTrace:0 pool2.bpl

  pool2.bpl(6,3): Error: this assertion could not be proved

  Boogie program verifier finished with 0 verified, 1 error

• The pool-name-to-type registry is a process-wide static, so it is populated by every {:pool} annotation anywhere in the program.

• /attrHelp states the restriction plainly: “These attributes are not effective for quantifiers inside the scope of axioms.” Pool instantiation is a per-implementation transformation of the VC; axioms are shared across implementations and are left alone.

14.6 Splitting the verification condition🔗

A single large VC is often harder for the solver than several small ones. Boogie can divide an implementation into parts, each of which becomes an independent solver query. All of the mechanisms below work the same way: in each part, the assertions that part is responsible for are kept as assert, and every other assertion is turned into assume. That is what makes splitting sound — every original assertion is checked on every path in at least one part, and anything a part assumes is checked by some other part. (The reference entries for the four attributes — their argument shapes and where they may be written — are in Splitting the verification condition.)

The conversion of an assertion into an assumption respects /subsumption: with /subsumption:0 an assertion turned into an assumption becomes assume true instead, which weakens the other parts but never unsoundly. For the {:split_here} example below, /subsumption:0 gives

implementation Three-0/untilFirstSplit(x: int)

{

anon0:

assert x == x;

assume true;

assume true;

return;

}

/subsumption:1 does the same only for assertions whose expression is a quantifier; /subsumption:2 (the default) always keeps the expression.

Parts are discovered by ManualSplitFinder, in a fixed order: {:focus} first, then {:isolate} on jumps, then {:isolate} on assertions, then {:split_here}. Parts containing no assertion at all are discarded; if that leaves nothing, the first focus part is kept so that the implementation is still counted.

14.6.1 {:split_here}🔗

assert {:split_here} P; ends one part and begins another. The first part checks everything up to (but not including) the marked assertion; the next part assumes everything before it and checks from there.

procedure Three(x: int)

{

assert x == x;

assert {:split_here} x + 0 == x;

assert x * 1 == x;

}

boogie /printSplit:- split1.bpl

implementation Three-0/untilFirstSplit(x: int)

{

anon0:

assert x == x;

assume x + 0 == x;

assume x * 1 == x;

return;

}

implementation Three-1/afterSplit@4(x: int)

{

anon0:

assume x == x;

assert {:split_here} x + 0 == x;

assert x * 1 == x;

return;

}

The part names encode their provenance. The ShortName of each origin class in Source/VCGeneration/Splits/ contributes one segment: untilFirstSplit and afterSplit@<line> ({:split_here}), assert@<line> ({:isolate} on an assertion), return@<line> and goto@<line> ({:isolate} on a jump), remainingAssertions (what is left after isolating jumps), focus[...] and path[...]. Segments compose, as in assert@27/path[6,22]. They appear in /printSplit output and in /trace.

Assignment of blocks to splits uses the dominator tree: a block belongs to the last split in its immediate dominator. /attrHelp warns that {:split_here} “may also occasionally double-report errors”.

14.6.2 {:isolate}🔗

assert {:isolate} P; puts P in its own part, in which every other assertion is an assumption — and, crucially, makes P an assumption in the remaining part.

procedure Three(x: int)

{

assert x >= 0;

assert {:isolate} x <= 0;

assert x == 0;

}

boogie /printSplit:- /errorTrace:0 split2.bpl

implementation Three-0/assert@4(x: int)

{

anon0:

assume x >= 0;

assert {:isolate} x <= 0;

return;

}

implementation Three-1(x: int)

{

anon0:

assert x >= 0;

assume x <= 0;

assert x == 0;

return;

}

split2.bpl(3,3): Error: this assertion could not be proved

split2.bpl(4,3): Error: this assertion could not be proved

Boogie program verifier finished with 0 verified, 2 errors

Only two errors are reported: x == 0 follows in part 1 from the two assumptions there, each of which is discharged elsewhere. This is exactly the obligation-preserving discipline; it is also why an isolated assertion that cannot be proved tends to make the remainder trivially provable.

The isolated part is restricted to the blocks that can reach the assertion, so isolation prunes the control flow graph as well.

{:isolate} takes no argument: BlockRewriter.ShouldIsolate tests only whether the attribute is present, so {:isolate false} isolates as well:

procedure P(x: int)

{

assert {:isolate false} x == x;

assert x + 0 == x;

}

boogie /printSplit:- /errorTrace:0 isofalse.bpl

implementation P-0/assert@3(x: int)

{

anon0:

assert {:isolate false} x == x;

return;

}

implementation P-1(x: int)

{

anon0:

assume x == x;

assert x + 0 == x;

return;

}

14.6.3 {:isolate "paths"} and {:allow_path_isolation}🔗

assert {:isolate "paths"} P; creates a separate part for each control-flow path that reaches P. To keep the number of parts finite, only goto commands annotated with {:allow_path_isolation} split the path space; all other branching is left alone.

procedure IsolatePathsAssertion(x: int, y: int)

{

var z: int;

z := 0;

if {:allow_path_isolation} (x > 0) {

z := z + 1;

}

else if {:allow_path_isolation} (x > 1) {

z := z + 2;

}

else {

z := z + 1;

}

if (y > 0) {

z := z + 0;

} else {

z := z + 0;

}

if {:allow_path_isolation} (y > 0) {

z := z + 3;

} else {

z := z + 4;

}

assert z > 1;

assert {:isolate "paths"} z > 5; // fails on three out of four paths

assert z > 6;

}

Three annotated branches give six paths, so six isolated parts plus a remainder:

boogie /printSplit:- /errorTrace:0 paths.bpl

implementation IsolatePathsAssertion-0/assert@27/path[6,22](x: int, y: int)

implementation IsolatePathsAssertion-1/assert@27/path[6,24](x: int, y: int)

implementation IsolatePathsAssertion-2/assert@27/path[8,9,22](x: int, y: int)

implementation IsolatePathsAssertion-3/assert@27/path[8,9,24](x: int, y: int)

implementation IsolatePathsAssertion-4/assert@27/path[8,12,22](x: int, y: int)

implementation IsolatePathsAssertion-5/assert@27/path[8,12,24](x: int, y: int)

implementation IsolatePathsAssertion-6(x: int, y: int)

(only the part headers are shown). The unannotated if (y > 0) in the middle contributes no branching to the path names. Four of the six parts fail, so the run ends 0 verified, 4 errors even though only one source location is reported.

The name the splitter looks for is the constant BlockRewriter.AllowPathIsolation = "allow_path_isolation".

{:isolate} and {:isolate "paths"} may also be placed on a transfer command. The grammar allows attributes on both forms:

TransferCmd

= ( "goto" { Attribute } Idents

| "return" { Attribute }

) ";" .

A return is lowered to a goto before splitting, so return {:isolate}; isolates the postcondition checks on that return path:

procedure IsolateReturn(x: int) returns (r: int)

ensures r > 4;

{

r := 0;

if (x > 0) {

r := r + 3;

return {:isolate};

}

r := r + 4;

}

boogie /printSplit:- /errorTrace:0 isojump.bpl

implementation IsolateReturn-0/remainingAssertions(x: int) returns (r: int)

implementation IsolateReturn-1/return@7(x: int) returns (r: int)

isojump.bpl(10,1): Error: a postcondition could not be proved on this return path

(part headers only).

14.6.4 {:focus}🔗

{:focus} on an assert or assume splits on reachability rather than on assertions. Each focus block yields two problems: one containing the focus block, its ancestors and its descendants (with the ancestors’ asserts turned into assumes); and one containing everything except the focus block and the blocks it dominates.

procedure Branch(b: bool) returns (r: int)

{

if (b) {

r := 1;

assume {:focus} true;

} else {

r := 2;

}

assert r > 0;

}

boogie /printSplit:- /errorTrace:0 focus1.bpl

implementation Branch-0(b: bool) returns (r: int)

{

anon0:

assume {:partition} !b;

assume r#AT#0 == 2;

assert r#AT#0 > 0;

return;

}

implementation Branch-1/focus[+5](b: bool) returns (r: int)

{

anon0:

assume {:partition} b;

assume {:focus} true;

assume r#AT#0 == 1;

assert r#AT#0 > 0;

return;

}

The focus[+5] name records which focus tokens were taken (+) and which were excluded (-), by line. N focus annotations can produce 2^N parts; /relaxFocus processes them bottom-up instead, which yields a linear number of parts at the cost of coarser splits.

The two parts do share blocks: every ancestor of the focus block appears in both. Splitting stays obligation-preserving because the ancestors’ assertions are rewritten to assumptions in the focused part. Adding an assertion before the branch makes that visible:

procedure Anc(b: bool) returns (r: int)

{

r := 0;

assert r == 0;

if (b) {

r := 1;

assume {:focus} true;

} else {

r := 2;

}

assert r > 0;

}

boogie /printSplit:- /errorTrace:0 focus2.bpl

implementation Anc-0(b: bool) returns (r: int)

{

anon0:

assert 0 == 0;

assume {:partition} !b;

assume r#AT#0 == 2;

assert r#AT#0 > 0;

return;

}

implementation Anc-1/focus[+7](b: bool) returns (r: int)

{

anon0:

assume 0 == 0;

assume {:partition} b;

assume {:focus} true;

assume r#AT#0 == 1;

assert r#AT#0 > 0;

return;

}

14.6.5 /vcsSplitOnEveryAssert🔗

/vcsSplitOnEveryAssert behaves as if every assertion carried {:isolate}:

boogie /printSplit:- /errorTrace:0 /vcsSplitOnEveryAssert split1.bpl

implementation Three-0/assert@3(x: int)

{

anon0:

assert x == x;

return;

}

implementation Three-1/assert@4(x: int)

{

anon0:

assume x == x;

assert {:split_here} x + 0 == x;

return;

}

implementation Three-2/assert@5(x: int)

{

anon0:

assume x == x;

assume x + 0 == x;

assert x * 1 == x;

return;

}

The per-implementation form is {:vcs_split_on_every_assert} on the procedure or implementation. /help notes that this “may result in VCs without any assertions” — those are discarded before solving.

14.6.6 Automatic, cost-based splitting🔗

Independently of the manual annotations, Boogie can split a part whose estimated cost exceeds /vcsMaxCost:<f>, up to /vcsMaxSplits:<n> parts (default 1, i.e. off). The cost of a block is

(<assert-cost> + <f2>*<assume-cost>) * (1.0 + <f1>*<entering-paths>)

with f1 from /vcsPathCostMult (default 1.0) and f2 from /vcsAssumeMult (default 0.01). The cost of a single assertion or assumption is always 1.0. /vcsPathSplitMult:<f> chooses between path splitting and assertion splitting.

CommandLineOptions.VcsMaxCost is initialised to 1.0, so with /vcsMaxSplits:2 even a four-assertion procedure of cost 16 is split; adding an explicit /vcsMaxCost:2000 suppresses the split. Since /vcsMaxSplits defaults to 1, the low threshold is invisible until you raise it.

On a procedure with forty independent if/else assertions:

procedure Big(x: int)

{

if (x > 0) { assert x > 0; } else { assert x <= 0; }

if (x > 1) { assert x > 1; } else { assert x <= 1; }

// ... 40 such statements in total

}

boogie /vcsMaxSplits:4 /vcsMaxCost:1 /trace /errorLimit:0 big.bpl

checking split 1/4, 0.00%, (cost:36941902772829600/77) ...

--> split #1 done,  [0.0322733 s] Valid

checking split 2/4, 25.00%, (cost:36941902772829600/77) ...

--> split #2 done,  [0.0112546 s] Valid

checking split 3/4, 50.00%, (cost:36941903533952500/78) ...

--> split #3 done,  [0.0071482 s] Valid

checking split 4/4, 75.00%, (cost:36941903533952500/78) ...

--> split #4 done,  [0.0077331 s] Valid

[0.058 s, solver resource count: 44977, 310 proof obligations]  verified

(the times and the resource count are of course machine-dependent). Without splitting the same run reports 80 proof obligations; the count rose to 310 because the assertions that become assumptions in one part are still counted in the part that proves them. Splitting trades total work for smaller individual queries.

/vcsMaxKeepGoingSplits:<n> enables “keep going” mode: after the first round, parts that time out are split further and retried, with /vcsKeepGoingTimeout for intermediate attempts and /vcsFinalAssertTimeout for the final single-assertion attempt. /vcsCores:<n> (or /vcsLoad:<f>) solves several parts concurrently.

14.7 Loop unrolling🔗

/loopUnroll:<n> replaces every natural loop by n copies of its body. The last copy is cut with assume false, so paths that would need more iterations simply disappear.

procedure Sum(n: int) returns (s: int)

{

var i: int;

i := 0;

s := 0;

while (i < n) {

s := s + i;

i := i + 1;

}

assert i >= n;

assert s == 0;   // only true when the loop body never runs

}

boogie /noVerify /loopUnroll:2 /printInstrumented unroll.bpl

implementation Sum(n: int) returns (s: int)

{

var i: int;

anon0#2:

i := 0;

s := 0;

goto anon3_LoopHead#2;

anon3_LoopHead#2:

goto anon3_LoopDone#2, anon3_LoopBody#2;

anon3_LoopBody#2:

assume {:partition} i < n;

s := s + i;

i := i + 1;

goto anon3_LoopHead#1;

anon3_LoopHead#1:

goto anon3_LoopDone#2, anon3_LoopBody#1;

anon3_LoopBody#1:

assume {:partition} i < n;

s := s + i;

i := i + 1;

goto anon3_LoopHead#0;

anon3_LoopHead#0:

assume false;

return;

anon3_LoopDone#2:

assume {:partition} n <= i;

assert i >= n;

assert s == 0;

return;

}

The key point is that n copies of the body permit exits after 0, 1, ..., n-1 iterations, not n: the last loop head (anon3_LoopHead#0) has no LoopDone successor, only the cut.

Invariants are not discarded. Every copy of the loop head keeps them as plain assertions, and because there is no back edge there is nothing to assume them from — they must be re-established outright at each copy. Unrolling pipeline.bpl from the start of this chapter shows both:

boogie /noVerify /loopUnroll:2 /printInstrumented pipeline.bpl

anon3_LoopHead#2:

assert i <= 3;

goto anon3_LoopDone#2, anon3_LoopBody#2;

...

anon3_LoopHead#1:

assert i <= 3;

goto anon3_LoopDone#2, anon3_LoopBody#1;

...

anon3_LoopHead#0:

assert i <= 3;

assume false;

return;

The final cut point keeps the leading predicate commands of the block — which is exactly where invariants live — and appends the cut.

The plain form is an under-approximation. It can only make verification succeed spuriously:

boogie /loopUnroll:2 unroll.bpl

Boogie program verifier finished with 1 verified, 0 errors

s == 0 is false as soon as the loop runs twice, but with two body copies the only reachable exits are after zero or one iteration, where s really is 0. Raising the bound exposes it:

boogie /loopUnroll:3 unroll.bpl

unroll.bpl(11,3): Error: this assertion could not be proved

Execution trace:

unroll.bpl(4,5): anon0#3

unroll.bpl(7,7): anon3_LoopBody#3

unroll.bpl(7,7): anon3_LoopBody#2

unroll.bpl(6,3): anon3_LoopDone#3

Boogie program verifier finished with 0 verified, 1 error

14.7.1 /soundLoopUnrolling🔗

/soundLoopUnrolling replaces the cutting assume false with assert false, so the tool must prove that the loop cannot run more than n-1 times. The result is a sound bounded proof, at the price of an error whenever the bound is not provable:

boogie /loopUnroll:2 /soundLoopUnrolling unroll.bpl

unroll.bpl(6,3): Error: this assertion could not be proved

Execution trace:

unroll.bpl(4,5): anon0#2

unroll.bpl(7,7): anon3_LoopBody#2

unroll.bpl(7,7): anon3_LoopBody#1

unroll.bpl(6,3): anon3_LoopHead#0

Boogie program verifier finished with 0 verified, 1 error

The error is reported at the loop, not at any user assertion, and the execution trace names the unrolled copies (#2, #1, #0).

14.7.2 Related loop options🔗

/kInductionDepth:<k> soundly eliminates loops by combined-case k-induction, unwinding proportionally to k. Its execution traces name the base and step copies:

boogie /kInductionDepth:2 unroll.bpl

Execution trace:

unroll.bpl(4,5): anon0

unroll.bpl(7,7): anon3_LoopBody_base_1

unroll.bpl(7,7): anon3_LoopBody_base_2

unroll.bpl(7,7): anon3_LoopBody_step_1

unroll.bpl(7,7): anon3_LoopBody_step_2

unroll.bpl(6,3): anon3_LoopDone

/extractLoops converts irreducible loops to reducible form by node splitting and turns every loop into a recursive procedure; the loop head becomes a call:

boogie /noVerify /extractLoops /printInstrumented pipeline.bpl

anon3_LoopHead:

call i, inline$Bump$0$g := Main_loop_anon3_LoopHead(i, inline$Bump$0$g);

goto anon3_LoopHead_last;

Error traces are mapped back through ExtractLoopTrace, so failures are still reported against the original program.

14.8 Inlining🔗

{:inline N} on a procedure or implementation asks for calls to it to be replaced by its body, to a depth of N. /inline:<strategy> chooses what happens when the depth runs out:

The default is assume, which is an under-approximation in exactly the same way as plain loop unrolling:

procedure {:inline 1} Down(n: int) returns (r: int)

{

if (n <= 0) {

r := 0;

} else {

call r := Down(n - 1);

}

}

procedure Client()

{

var x: int;

call x := Down(2);

assert false;

}

boogie inline-depth.bpl

Boogie program verifier finished with 1 verified, 0 errors

assert false “verifies” because Down(2) needs two levels of inlining and only one is available. /printInlined shows why:

boogie /noVerify /printInlined inline-depth.bpl

inline$Down$0$anon3_Else:

assume {:partition} 0 < inline$Down$0$n;

assume false;

goto inline$Down$0$Return;

/inline:assert turns the cut into a proof obligation and reports it at the recursive call:

boogie /inline:assert inline-depth.bpl

inline-depth.bpl(6,5): Error: this assertion could not be proved

Execution trace:

inline-depth.bpl(13,3): anon0

inline-depth.bpl(6,5): inline$Down$0$anon3_Else

Boogie program verifier finished with 0 verified, 1 error

14.8.1 What happens to the specification at an inline site🔗

Inlining does not simply drop the callee’s contract. Checked specifications are re-checked at each site; free specifications are thrown away.

procedure {:inline 1} Q(x: int) returns (r: int)

requires x > 0;

free requires x < 100;

ensures r == x;

free ensures r > 0;

{

r := x;

}

procedure Client()

{

var y: int;

call y := Q(5);

assert y == 5;

}

boogie /noVerify /printInlined inlinespec.bpl

after inlining procedure calls

procedure Client();

implementation Client()

{

var y: int;

var inline$Q$0$x: int;

var inline$Q$0$r: int;

anon0:

goto inline$Q$0$Entry;

inline$Q$0$Entry:

inline$Q$0$x := 5;

assert inline$Q$0$x > 0;

assert true;

havoc inline$Q$0$r;

goto inline$Q$0$anon0;

inline$Q$0$anon0:

inline$Q$0$r := inline$Q$0$x;

goto inline$Q$0$Return;

inline$Q$0$Return:

assert inline$Q$0$r == inline$Q$0$x;

assume true;

y := inline$Q$0$r;

goto anon0$1;

anon0$1:

assert y == 5;

return;

}

The free requires became assert true and the free ensures became assume true. The paper anticipates this (section 11.3 has a to-do item “discuss ... why the inline directive ignores them”); the consequence in practice is that a body relying on a free requires may fail once inlined, because with /inline:assume the body is only verified at the inline site:

procedure {:inline 1} S(x: int)

free requires x > 0;

{

assert x > 0;

}

procedure Client()

{

var y: int;

havoc y;

call S(y);

}

boogie /errorTrace:0 freereq.bpl

freereq.bpl(4,3): Error: this assertion could not be proved

Boogie program verifier finished with 0 verified, 1 error

Removing the {:inline 1} makes it verify, because S is then checked on its own with the free precondition assumed.

14.8.2 Inlining at the call site🔗

Undocumented in /attrHelp: the depth may also be given on the call command itself, and it takes priority over the callee’s attribute (Inliner.TryDefineCount checks the call first). But the inlining pass only runs at all if some procedure or implementation in the program carries an inline attribute, so a call-site annotation on its own is silently ignored:

procedure Helper() returns (r: int)

{

r := 7;

}

procedure Client()

{

var x: int;

call {:inline 1} x := Helper();

assert x == 7;

}

boogie /errorTrace:0 callinline2.bpl

callinline2.bpl(10,3): Error: this assertion could not be proved

Boogie program verifier finished with 1 verified, 1 error

Adding any {:inline 1} declaration elsewhere in the file makes the same call-site annotation take effect:

procedure Helper() returns (r: int)

{

r := 7;

}

procedure {:inline 1} Trigger() { }

procedure Client()

{

var x: int;

call {:inline 1} x := Helper();

assert x == 7;

}

boogie /errorTrace:0 callinline3.bpl

Boogie program verifier finished with 2 verified, 0 errors

(Two, not three: Trigger carries {:inline 1} and so is not verified.)

14.8.3 Function inlining is a different mechanism🔗

{:inline} on a function expands the function’s body at every use before VC generation, and {:define} turns it into an SMT-LIB define-fun. Neither has anything to do with /inline:

function {:define} sq(x: int): int { x * x }

function {:inline} dbl(x: int): int { x + x }

procedure P()

{

assert sq(3) == 9;

assert dbl(3) == 6;

}

boogie /proverLog:fi.smt2 funinline.bpl

(define-fun sq ((x Int) ) Int (* x x))

...

(=> (= (ControlFlow 0 0) 4) (let ((anon0_correct  (and (=> (= (ControlFlow 0 2) (- 0 3)) (= (sq 3) 9)) (=> (= (sq 3) 9) (=> (= (ControlFlow 0 2) (- 0 1)) (= (+ 3 3) 6))))))

sq survives as a solver-level definition; dbl(3) has already become (+ 3 3).

14.9 Abstract interpretation🔗

/infer:<flags> runs an abstract interpreter over each implementation and instruments loop heads with what it found. The flags select exactly one domain — t for the trivial bottom/top lattice, j for intervals — plus optional s for statistics and a digit 0..9 for the number of iterations before widening.

Inferred invariants are assumed, not proved.

procedure Count(n: int) returns (i: int)

{

i := 0;

while (i < n) {

i := i + 1;

}

assert 0 <= i;

}

Without inference the assertion fails, because the loop havocs i and there is no invariant:

boogie infer.bpl

infer.bpl(7,3): Error: this assertion could not be proved

Execution trace:

infer.bpl(3,5): anon0

infer.bpl(4,3): anon3_LoopDone

Boogie program verifier finished with 0 verified, 1 error

With /infer:j it verifies, and /printInstrumented shows why:

boogie /noVerify /infer:j /printInstrumented infer.bpl

implementation Count(n: int) returns (i: int)

{

anon0:

i := 0;

goto anon3_LoopHead;

anon3_LoopHead:  // cut point

assume {:inferred} 0 <= i;

goto anon3_LoopDone, anon3_LoopBody;

anon3_LoopBody:

assume {:partition} i < n;

i := i + 1;

goto anon3_LoopHead;

anon3_LoopDone:

assume {:partition} n <= i;

assert 0 <= i;

return;

}

The assume {:inferred} 0 <= i is trusted. If the abstract interpreter is wrong, the verification result is wrong. /checkInfer converts these into proof obligations:

boogie /noVerify /infer:j /checkInfer /printInstrumented infer.bpl

anon3_LoopHead:  // cut point

assert {:inferred} 0 <= i;

Use /checkInfer whenever you rely on inference for a result you care about; the cost is that a correct-but-unprovable invariant now becomes an error.

/infer:t produces assume {:inferred} true — the trivial domain learns nothing but exercises the plumbing. /instrumentInfer:e instruments at the beginning and end of every block instead of only at loop heads (intended for debugging abstract domains). /printInstrumented prints the program after instrumentation.

The interpreter trusts the {:identity} attribute on a unary function without checking it, per /attrHelp.

14.10 Houdini🔗

/contractInfer runs Houdini: given a set of candidate specification clauses guarded by existentially quantified boolean constants, it computes the largest subset that is simultaneously provable. A candidate is a global constant marked {:existential true} used as the antecedent of a specification clause or loop invariant.

const {:existential true} b0: bool;

const {:existential true} b1: bool;

procedure Loop() returns (i: int)

{

i := 0;

while (i < 10)

invariant b0 ==> 0 <= i;

invariant b1 ==> i < 10;

{

i := i + 1;

}

assert 0 <= i;

}

boogie /contractInfer /printAssignment houdini.bpl

Assignment computed by Houdini:

b0 = True

b1 = False

Boogie program verifier finished with 1 verified, 0 errors

0 <= i is inductive, so b0 is set to True and the invariant is retained; i < 10 is not maintained on exit, so b1 is refuted and that invariant is discarded. The refutation loop is monotone: constants are only ever set from True to False, so it terminates.

/printAssignment is what makes this readable. It, and every Houdini option other than /contractInfer itself, is listed only in CommandLineOptions.cs: /explainHoudini (report why each candidate was refuted, requires the solver to produce models), /reverseHoudiniWorklist, /crossDependencies (which sets HoudiniUseCrossDependencies), /concurrentHoudini together with /debugConcurrentHoudini and /modifyTopologicalSorting, and /stagedHoudini:<strategy> — where <strategy> must be COARSE, FINE or BALANCED — with /stagedHoudiniThreads:<n>, /stagedHoudiniReachabilityAnalysis and /stagedHoudiniMergeIgnoredAnnotations.

When /contractInfer is given, Houdini replaces the normal verification loop entirely: ExecutionEngine.InferAndVerify returns RunHoudini(...) before implementations are prioritised, so per-procedure options such as /proc interact differently than usual.

14.11 The SMT-LIB interface🔗

The shipped prover interface is SMTLib (/proverDll: can select another). It launches a solver process and speaks SMT-LIB 2.6 over pipes.

14.11.1 Reading the query🔗

/proverLog:<file> writes everything Boogie sends. The filename may contain @TIME@, @PREFIX@ (from /logPrefix:<str>), @FILE@, and @PROC@; the last of these produces one file per verification condition. /proverLogAppend appends rather than overwrites.

A whole log for the pruning example of the previous section, under /prune:1, is:

(set-option :print-success false)

(set-info :smt-lib-version 2.6)

(set-option :smt.mbqi false)

(set-option :model.compact false)

(set-option :model.v2 true)

(set-option :pp.bv_literals false)

; done setting options

(declare-fun tickleBool (Bool) Bool)

(assert (and (tickleBool true) (tickleBool false)))

(declare-fun f (Int) Int)

(assert (forall ((x Int) ) (! (= (f x) (+ x 1))

:qid |prune2bpl.2:17|

:skolemid |0|

:pattern ( (f x))

)))

(push 1)

(declare-fun ControlFlow (Int Int) Int)

(set-info :boogie-vc-id UsesF)

(set-option :timeout 0)

(set-option :rlimit 0)

(set-option :smt.mbqi false)

(set-option :model.compact false)

(set-option :model.v2 true)

(set-option :pp.bv_literals false)

(assert (not

(=> (= (ControlFlow 0 0) 3) (let ((anon0_correct  (=> (= (ControlFlow 0 2) (- 0 1)) (= (f 1) 2))))

(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 3) 2) anon0_correct)))

PreconditionGeneratedEntry_correct)))

))

(check-sat)

(get-info :rlimit)

(pop 1)

; Valid