7 Statements and control flow🔗

Boogie has two statement languages layered on top of each other. The structured layer has if, while and break; the unstructured layer has labels, goto and return. They are not alternatives: a single implementation body may freely mix them. Immediately after parsing, the structured layer is compiled away — every if, while and break becomes labelled basic blocks connected by goto — and everything downstream of that point (type checking of control flow, verification-condition generation, error traces) sees only basic blocks.

This chapter describes both layers, the translation between them, and the separate transformation that gives loops their meaning. Section 9 of This is Boogie 2 is the baseline; the differences are collected in Divergences from This is Boogie 2.

Throughout, listings are followed by the output the tool actually produced. Where printed-program output is quoted (/print:-, /printPassive:, /traceverify), boilerplate has been elided: the version banner, the echoed command line, the /*** structured program: ... */ comment, the procedure declarations that /print re-emits alongside each implementation, and the trailing Boogie program verifier finished with ... line. Nothing inside a quoted implementation body has been edited. Elisions elsewhere are called out where they occur.

7.1 The shape of an implementation body🔗

An implementation body is a brace-enclosed block of local variable declarations followed by statements:

ImplBody = "{" { LocalVars } StmtList .

StmtList = { LabelOrCmd | StructuredCmd | TransferCmd } "}" .

StmtList is unusual in that it consumes the closing brace itself, which is why an opening brace appears without a matching closing brace in the productions for if and while below.

The three alternatives inside StmtList are the three kinds of statement:

• LabelOrCmd — a label, or one of the simple commands (assert, assume, havoc, assignment, unpack, call, measure, hide, reveal, push, pop);

• StructuredCmd — if, while or break;

• TransferCmd — goto or return.

In full:

LabelOrCmd =

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

| "pop" ";"

| "push" ";"

| LabelOrAssign

| "assert" { Attribute } Proposition ";"

| "assume" { Attribute } Proposition ";"

| "measure" { Attribute } Expressions ";"

| "havoc" Idents ";"

| CallCmd ";" .

StructuredCmd = IfCmd | WhileCmd | BreakCmd .

TransferCmd = ( "goto" { Attribute } Idents | "return" { Attribute } ) ";" .

LabelOrAssign covers labels, assignment and datatype unpacking; it is given in Assignment.

The parser groups these into big blocks. A big block is an optional label, a run of simple commands, and then at most one terminator: either a structured command or a transfer command. A label always starts a new big block, and a structured or transfer command always ends one. This is why labels behave the way they do: a label is not a statement sitting between two other statements, it is the name of everything that follows it up to the next terminator.

A body needs no explicit return; falling off the end of the body returns. An empty body, and a body whose last thing is a bare label, are both legal:

procedure P()

{

}

procedure Q()

{

var i: int;

i := 0;

Done:

}

boogie /noVerify /print:- /printUnstructured empty1.bpl

implementation P()

{

anon0:

return;

}

implementation Q()

{

var i: int;

anon0:

i := 0;

goto Done;

Done:

return;

}

Two labels in a row produce an empty block that falls through to the next:

procedure P() returns (r: int)

{

L1:

L2:

r := 1;

goto L1;

}

implementation P() returns (r: int)

{

L1:

goto L2;

L2:

r := 1;

goto L1;

}

7.2 assert and assume🔗

"assert" { Attribute } Proposition ";"

"assume" { Attribute } Proposition ";"

The proposition must be of type bool. assert states a proof obligation: the verifier must show the expression holds at that point on every path that reaches it. assume states a hypothesis: paths on which the expression does not hold are not considered.

A checked assert is also assumed downstream — once Boogie has reported the failure of an assertion, it does not report the consequences of that same failure again. assume false; cuts off all further checking on the path:

procedure P(x: int, y: int, z: int)

{

assert z != 0;                 // fails: nothing constrains z

assume 0 <= x;

assert 0 <= x;                 // holds: assumed above

assume false;

assert 1 == 2;                 // unreachable, so it holds

}

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

Execution trace:

basic1.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

The assert-then-assume behaviour is controlled per-assertion by {:subsumption n}: 0 never assumes the assertion afterwards, 1 assumes it unless the translated condition is a quantifier, and 2 always assumes it. Any other value (including no attribute) falls back to /subsumption:<c>, whose own default is 2. With {:subsumption 0} the same failure is reported twice:

procedure P(x: int)

{

assert x == 1;

assert x == 1;

}

procedure Q(x: int)

{

assert {:subsumption 0} x == 1;

assert x == 1;

}

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

Execution trace:

subs.bpl(3,3): anon0

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

Execution trace:

subs.bpl(9,3): anon0

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

Execution trace:

subs.bpl(9,3): anon0

Boogie program verifier finished with 0 verified, 3 errors

{:msg "..."} replaces the entire error line — location prefix included — for a failing assertion:

procedure P(x: int)

{

assert {:msg "x must be positive here"} x > 0;

}

x must be positive here

Execution trace:

msg1.bpl(3,3): anon0

Boogie program verifier finished with 0 verified, 1 error

7.3 Assignment🔗

LabelOrAssign =

Ident

( ":"

| "(" Idents ")" ":=" { Attribute } Expression ";"

| { MapAssignIndex | FieldAccess }

{ "," Ident { MapAssignIndex | FieldAccess } }

":=" { Attribute } Expression { "," Expression } ";"

) .

MapAssignIndex = "[" [ Expression { "," Expression } ] "]" .

FieldAccess = "->" Ident .

A single production covers labels (Ident ":"), datatype unpacking (Unpacking a datatype value) and assignment, because all three begin with an identifier.

An assignment updates one or more targets simultaneously. The number of targets must equal the number of right-hand sides, corresponding types must unify, and all right-hand sides are evaluated in the pre-state. Each target is a variable, optionally followed by any number of map indexings [...] and datatype field selections ->f.

type Ref;

type Field a;

type HeapType = <a>[Ref, Field a]a;

var Heap: HeapType;

var x: int;

var y: int;

procedure P(o: Ref, f: Field int, i: int, a: [int][int,int]int)

returns (b: [int][int,int]int)

modifies Heap, x, y;

{

x, y := y, x;                 // parallel: swap

x, Heap[o, f] := x + 1, x;    // set the field to the *old* x

b := a;

b[i][3, 4] := 12;             // nested map target

}

Boogie program verifier finished with 1 verified, 0 errors

7.3.1 Map and field targets are sugar for whole-variable assignment🔗

A target with indexings or field selections is rewritten into an assignment to the base variable alone, using map-update and datatype-update expressions. a[j] := E means a := a[j := E], and b[i][m,n] := F means b := b[i := b[i][m,n := F]]. The rewriting is visible in the passive form of the program:

procedure P(i: int, a: [int][int,int]int) returns (b: [int][int,int]int)

{

b := a;

b[i][3, 4] := 12;

assert b[i][3, 4] == 12;

}

boogie /printPassive:passive.bpl assign4.bpl

/printPassive: always writes to a file — unlike /print:, it does not accept - for standard output — so what follows is the body of passive.bpl:

implementation P(i: int, a: [int][int,int]int) returns (b: [int][int,int]int)

{

var b#AT#0: [int][int,int]int;

PreconditionGeneratedEntry:

goto anon0;

anon0:

assume b#AT#0 == a[i := a[i][3, 4 := 12]];

assert b#AT#0[i][3, 4] == 12;

return;

}

A field target is rewritten the same way, but the update expression is a full reconstruction of the datatype value — every other field is copied across:

datatype Point { Point(x: int, y: int) }

procedure Shift(p: Point, d: int) returns (q: Point)

ensures q->x == p->x + d && q->y == p->y;

{

q := p;

q->x := q->x + d;

}

boogie /printPassive:pf.bpl field1.bpl

implementation Shift(p: Point, d: int) returns (q: Point)

{

var q#AT#0: Point;

PreconditionGeneratedEntry:

goto anon0;

anon0:

assume q#AT#0 == Point(p->x + d, p->y);

assert q#AT#0->x == p->x + d && q#AT#0->y == p->y;

return;

}

An index list may be empty, which is how you assign to a nullary map:

procedure P(a: []int) returns (b: []int)

ensures b[] == 5;

{

b := a;

b[] := 5;

}

Boogie program verifier finished with 1 verified, 0 errors

7.3.2 Restrictions🔗

The base variables of the targets must be pairwise distinct. Because a map or field target is sugar for an assignment to its base variable, this rules out the natural-looking in-place swap:

procedure P(a: [int]int, i: int, j: int) returns (b: [int]int)

{

b := a;

b[i], b[j] := b[j], b[i];

}

assign2.bpl(4,9): Error: variable b is assigned more than once in parallel assignment

1 name resolution errors detected in assign2.bpl

Targets must be mutable: local variables, out-parameters, and global variables listed in the enclosing procedure’s modifies clause. In-parameters and constants are not assignable, and neither assignment nor havoc may target them.

const c: int;

procedure P(n: int)

{

n := 3;

}

procedure Q()

{

c := 3;

}

procedure R(n: int)

{

havoc n;

}

inparam.bpl(4,4): Error: command assigns to an immutable variable: n

inparam.bpl(8,4): Error: command assigns to an immutable variable: c

inparam.bpl(12,2): Error: command assigns to an immutable variable: n

3 type checking errors detected in inparam.bpl

var g: int;

var h: int;

procedure P()

modifies g;

{

g := 1;

h := 2;

havoc h;

}

mod1.bpl(8,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h

mod1.bpl(9,2): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h

2 type checking errors detected in mod1.bpl

7.3.3 where clauses do not apply to assignment🔗

An assignment may store a value that violates the target’s where clause. where constrains only the values that arise from nondeterminism — havoc, loop-head havocking, procedure-call results, initial values — never the value written by an assignment. If you want the condition re-established after an assignment, say so with assume.

procedure P()

{

var x: int where 0 <= x;

x := -1;

assert x == -1;   // holds

assert 0 <= x;    // fails: the where clause was not re-imposed

}

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

Execution trace:

where1.bpl(4,5): anon0

Boogie program verifier finished with 0 verified, 1 error

7.3.4 Attributes on assignments are parsed and dropped🔗

The grammar allows attributes between := and the first right-hand side, as in r := {:myattr 1} x + 1;. They are stored on the assignment command, but the printer never emits them, so they vanish from /print output. {:print} on an assignment is still honoured, because it is read off the command rather than from printed text.

7.4 havoc🔗

"havoc" Idents ";"

havoc x, y; assigns arbitrary values to x and y. The values are of the right type, satisfy the program’s axioms, and satisfy the where clauses of the havoc’d variables. Every identifier must be a mutable variable; havoc cannot target a map element or a datatype field (use a temporary variable and an assignment).

Because where clauses are re-imposed after the havoc, a multi-variable havoc constrains the variables jointly, and a havoc can be infeasible:

procedure P()

{

var x: int where 0 <= x;

var y: int where 0 <= y && y < x;

havoc x, y;

assert 0 <= y && y < x;

x := 0;

havoc y;

assert false;   // unreachable: no y satisfies 0 <= y && y < 0

}

Boogie program verifier finished with 1 verified, 0 errors

7.5 Unpacking a datatype value🔗

Ident "(" Idents ")" ":=" { Attribute } Expression ";"

An unpack statement destructures a datatype value, binding one variable per constructor argument. The left-hand side must be an application of a datatype constructor to distinct assignable variables.

datatype Tree { Leaf(), Node(left: Tree, val: int, right: Tree) }

procedure P(t: Tree) returns (v: int)

requires t is Node;

ensures v == t->val;

{

var l: Tree, r: Tree;

Node(l, v, r) := t;

}

It desugars to an assertion that the value really has that constructor, followed by a parallel assignment of the field selections:

boogie /printPassive:pu.bpl unpack2.bpl

implementation P(t: Tree) returns (v: int)

{

var l: Tree;

var r: Tree;

var l#AT#0: Tree;

var v#AT#0: int;

var r#AT#0: Tree;

PreconditionGeneratedEntry:

assume t is Node;

goto anon0;

anon0:

assert t is Node;

assume l#AT#0 == t->left && v#AT#0 == t->val && r#AT#0 == t->right;

assert v#AT#0 == t->val;

return;

}

Without the precondition the constructor test fails, with a dedicated message. The reported location is the := of the unpack statement, not the start of the line:

datatype Tree { Leaf(), Node(left: Tree, val: int, right: Tree) }

procedure P(t: Tree) returns (v: int)

{

var l: Tree, r: Tree;

Node(l, v, r) := t;

}

unpack1.bpl(6,17): Error: the precondition for unpack could not be proved

Execution trace:

unpack1.bpl(6,17): anon0

Boogie program verifier finished with 0 verified, 1 error

7.6 Procedure calls🔗

CallCmd = [ "async" ] [ "free" ] "call" CallParams { "|" CallParams } .

CallParams =

{ Attribute } Ident

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

| [ "," Ident { "," Ident } ] ":="

Ident "(" [ Expression { "," Expression } ] ")"

) .

The two CallParams alternatives are call P(args) — no results — and call x, y := P(args). The out-parameter list is a list of plain identifiers, which must be assignable and pairwise distinct; it cannot contain map or field targets. Attributes belong to the arm and are written immediately after call, that is before the callee name in the first form and before the first out-parameter in the second (call {:myattr} x, y := Q();).

7.6.1 What a call means🔗

A call is a sugared command. It expands to fresh locals for the actual in-parameters, an assert for each checked precondition, a snapshot of every variable in the modifies clause (so that old in the postcondition has something to refer to), a havoc of the modified globals and of fresh locals standing for the out-parameters, an assume for each postcondition, and finally an assignment of those locals to the actual out-parameters.

var g: int;

procedure Incr(n: int) returns (m: int)

requires 0 <= n;

modifies g;

ensures m == n + 1;

ensures g == old(g) + n;

{

g := g + n;

m := n + 1;

}

procedure Client()

modifies g;

{

var k: int;

call k := Incr(3);

assert k == 4;

}

boogie /noVerify /print:- /printDesugared call1.bpl

implementation Client()

{

var k: int;

call k := Incr(3);

/*** desugaring:

{

var call0formal#AT#n: int;

var call1old#AT#g: int;

var call2formal#AT#m: int;

call0formal#AT#n := 3;

assert 0 <= call0formal#AT#n;

call1old#AT#g := g;

havoc g, call2formal#AT#m;

assume call2formal#AT#m == call0formal#AT#n + 1;

assume g == call1old#AT#g + call0formal#AT#n;

k := call2formal#AT#m;

}

**** end desugaring */

assert k == 4;

}

Three consequences worth stating explicitly. A call is defined entirely by the specification of the callee; the callee’s body is irrelevant unless it is inlined. Everything in the callee’s modifies clause is havoc’d, so any fact you knew about a modified global is lost unless a postcondition re-establishes it. And the actual in-parameters are copied into fresh locals before anything else happens, so aliasing between an in-parameter expression and an actual out-parameter is harmless.

/printDesugared prints the whole program twice: once immediately after parsing (before desugarings have been computed, so no desugaring is shown) and once after resolution and type checking. Only the second copy is interesting.

7.6.2 free call🔗

free call skips the precondition assertions but keeps the havoc and the postcondition assumptions:

procedure Q(n: int) returns (m: int);

requires 0 <= n;

ensures m == n + 1;

procedure P()

{

var k: int;

free call k := Q(-5);

assert k == -4;

}

Boogie program verifier finished with 1 verified, 0 errors

implementation P()

{

var k: int;

free call k := Q(-5);

/*** desugaring:

{

var call0formal#AT#n: int;

var call1formal#AT#m: int;

call0formal#AT#n := -5;

havoc call1formal#AT#m;

assume call1formal#AT#m == call0formal#AT#n + 1;

k := call1formal#AT#m;

}

**** end desugaring */

assert k == -4;

}

Compare with the checked call above: the assert 0 <= call0formal#AT#n; is gone, and so is the -5 >= 0 obligation it would have imposed.

7.6.3 Asynchronous and parallel calls🔗

async call P(...) and call A(...) | B(...) | C(...) belong to Civl, Boogie’s concurrency layer, and are rejected in ordinary procedures. The parallel form has as many arms as you like; attributes and out-parameters are per-arm, and neither async nor free may be combined with it.

var g: int;

procedure Q()

modifies g;

ensures g == old(g) + 1;

{

g := g + 1;

}

procedure P()

modifies g;

{

async call Q();

assert g == old(g) + 1;

}

async2.bpl(13,8): Error: async call allowed only from a yield procedure or an action

1 name resolution errors detected in async2.bpl

procedure A() returns (r: int);

procedure B(n: int) returns (r: int);

procedure P()

{

var a: int, b: int;

async call a := A() | b := B(a);

}

par4.bpl(7,9): error: parallel call not allowed

1 parse errors detected in par4.bpl

Inside Civl both forms work. An asynchronous call to a yield procedure that has a mover type or refines an action must be marked {:sync}, and the refined action must then be a left mover; without a mover type or a refined action the callee is a pending async and no marking is required. The details belong to Calls; what matters here is that async and | are ordinary parts of the call statement’s grammar.

var {:layer 0,2} x: int;

left action {:layer 1,2} AtomicIncr()

modifies x;

{ x := x + 1; }

left action {:layer 2} AtomicIncr2()

modifies x;

{ x := x + 2; }

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield procedure {:layer 1} Caller()

refines AtomicIncr2;

{

async call {:sync} Incr();

async call {:sync} Incr();

}

Boogie program verifier finished with 4 verified, 0 errors

var {:layer 0,2} x: int;

right action {:layer 1} AtomicIncr()

modifies x;

{ x := x + 1; }

right action {:layer 2} AtomicIncr2()

modifies x;

{ x := x + 2; }

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield procedure {:layer 1} Incr2()

refines AtomicIncr2;

{

call Incr() | Incr();

}

Boogie program verifier finished with 2 verified, 0 errors

The arms of a parallel call must not interfere: no variable may be an out-parameter of two arms, and no out-parameter of one arm may be read by another arm.

var {:layer 0,1} x: int;

yield procedure {:layer 0} A() returns (r: int);

yield procedure {:layer 0} B(n: int) returns (r: int);

yield procedure {:layer 1} P()

{

var a: int, b: int;

call a := A() | b := B(a);

}

par5.bpl(8,2): Error: left-hand side of parallel call command contains variable accessed on the right-hand side of a different arm: a

1 name resolution errors detected in par5.bpl

7.7 if🔗

IfCmd = "if" { Attribute } Guard "{" StmtList

[ "else" ( IfCmd | "{" StmtList ) ] .

Guard = "(" ( "*" | Expression ) ")" .

The guard is either a boolean expression or *. With * the branch is chosen nondeterministically and no assumption is added on either side. The else part is either another if (an else if chain) or a braced block; there is no elseif keyword and no dangling-else ambiguity, since both branches are always braced.

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

{

if (x < 0) {

r := -x;

} else if (x == 0) {

r := 0;

} else {

r := x;

}

if (*) {

r := r + 1;

}

}

boogie /noVerify /print:- /printUnstructured if1.bpl

implementation P(x: int) returns (r: int)

{

anon0:

goto anon6_Then, anon6_Else;

anon6_Then:

assume {:partition} x < 0;

r := -x;

goto anon4;

anon6_Else:

assume {:partition} 0 <= x;

goto anon7_Then, anon7_Else;

anon7_Then:

assume {:partition} x == 0;

r := 0;

goto anon4;

anon7_Else:

assume {:partition} x != 0;

r := x;

goto anon4;

anon4:

goto anon8_Then, anon8_Else;

anon8_Then:

r := r + 1;

return;

anon8_Else:

return;

}

The generated assume commands carry the {:partition} attribute, which marks them as encoding a control-flow decision rather than a user assumption. The negated guard is simplified where possible: !(x < 0) prints as 0 <= x and !(x == 0) as x != 0. The simplification is syntactic and covers ==, !=, <, <=, >, >=, ! and the internal true/false constants — if (true) still yields assume {:partition} !true; on the else side, because a source-level true is a fresh literal rather than the shared constant.

An attribute on the if lands on the two-way goto that dispatches to the branches:

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

{

r := {:myattr 1} x + 1;

if {:iattr} (r > 0) {

goto {:gattr} Done;

}

Done:

return {:rattr};

}

implementation P(x: int) returns (r: int)

{

anon0:

r := x + 1;

goto {:iattr}anon2_Then, anon2_Else;

anon2_Then:

assume {:partition} r > 0;

goto {:gattr}Done;

anon2_Else:

assume {:partition} 0 >= r;

goto Done;

Done:

return;

}

Of the four attributes written above, only the two on goto survive printing; the ones on the assignment and on return are parsed, stored, and never emitted.

7.8 while🔗

WhileCmd = "while" Guard

{ [ "free" ] "invariant" { Attribute } ( Expression | CallCmd ) ";"

| "measure" { Attribute } Expressions ";" }

"{" StmtList .

As with if, the guard is a boolean expression or *; while (*) exits after an arbitrary number of iterations.

7.8.1 invariant and free invariant🔗

An invariant clause becomes an assert at the loop head; a free invariant becomes an assume there. Clauses appear at the head in source order.

procedure Search(a: [int]int, N: int, X: int) returns (i: int)

{

i := 0;

Outer:

while (i < N)

invariant 0 <= i;

free invariant i <= N + 1;

{

if (a[i] == X) { break Outer; }

i := i + 1;

}

}

implementation Search(a: [int]int, N: int, X: int) returns (i: int)

{

anon0:

i := 0;

goto Outer;

Outer:

goto anon4_LoopHead;

anon4_LoopHead:

assert 0 <= i;

assume i <= N + 1;

goto anon4_LoopDone, anon4_LoopBody;

anon4_LoopBody:

assume {:partition} i < N;

goto anon5_Then, anon5_Else;

anon5_Then:

assume {:partition} a[i] == X;

return;

anon5_Else:

assume {:partition} a[i] != X;

goto anon3;

anon3:

i := i + 1;

goto anon4_LoopHead;

anon4_LoopDone:

assume {:partition} N <= i;

return;

}

What that assert at the head means is decided by a later transformation; see Loop semantics.

The third form of invariant, invariant call Inv(args);, is a Civl yield invariant. The following program (Test/civl/samples/inc-dec-x.bpl) carries one on its loop:

var {:layer 0,1} x:int;

yield invariant {:layer 1} Inv ();

preserves x >= 0;

yield procedure {:layer 1} main ()

requires call Inv();

{

while (*)

invariant {:yields} true;

invariant call Inv();

{

async call incdec();

}

}

yield procedure {:layer 1} incdec()

preserves call Inv();

{

call geq0_inc();

call geq0_dec();

}

right action {:layer 1} GEQ0_INC ()

modifies x;

{

assert x >= 0;

x := x + 1;

}

atomic action {:layer 1} GEQ0_DEC ()

modifies x;

{

assert x >= 0;

x := x - 1;

}

yield procedure {:layer 0} geq0_inc ();

refines GEQ0_INC;

yield procedure {:layer 0} geq0_dec ();

refines GEQ0_DEC;

Boogie program verifier finished with 7 verified, 0 errors

7.8.2 measure🔗

"measure" { Attribute } Expressions ";"

A measure clause is a termination measure: a comma-separated list of int or bool expressions, compared lexicographically. It generates, at the loop head, an assertion that each int component is non-negative plus a snapshot of the tuple; and, at the end of the body, an assertion that the tuple has strictly decreased.

procedure Countdown(n: int)

{

var k: int;

k := n;

while (k > 0)

measure k;

{

k := k - 1;

}

}

boogie /noVerify /print:- /printMeasureDesugaring meas1.bpl

implementation Countdown(n: int)

{

var k: int;

var old_28_27: int;

anon0:

k := n;

goto anon2_LoopHead;

anon2_LoopHead:

assert k >= 0;

old_28_27 := k;

goto anon2_LoopDone, anon2_LoopBody;

anon2_LoopBody:

assume {:partition} k > 0;

k := k - 1;

assert k < old_28_27;

goto anon2_LoopHead;

anon2_LoopDone:

assume {:partition} 0 >= k;

return;

}

Since n may be negative, the non-negativity assertion is not provable on entry here — and note that it is reported as a loop invariant, which is exactly what it has become:

meas1.bpl(6,13): Error: this loop invariant could not be proved on entry

Execution trace:

meas1.bpl(4,5): anon0

Boogie program verifier finished with 0 verified, 1 error

Adding requires 0 <= n; makes it verify. A lexicographic pair works as expected:

procedure Nested(n: int, m: int)

requires 0 <= n && 0 <= m;

{

var i: int, j: int;

i, j := n, m;

while (i > 0 || j > 0)

measure i, j;

{

if (j > 0) { j := j - 1; }

else { i := i - 1; j := m; }

}

}

Boogie program verifier finished with 1 verified, 0 errors

Invariants are always placed before measures at the loop head, whatever order they appear in the source. A sequential procedure’s loop head may carry at most one measure; a Civl yield procedure may carry one per layer.

measure is also a simple statement, usable in an unstructured loop, where it must occur in the header block of a natural loop:

procedure Countdown(n: int)

requires 0 <= n;

{

var k: int;

k := n;

Head:

measure k;

if (k > 0) {

k := k - 1;

goto Head;

}

}

Boogie program verifier finished with 1 verified, 0 errors

procedure P()

{

measure 3;

}

meas3.bpl(3,2): Error: Measure command must not occur outside a loop head

1 type checking errors detected in meas3.bpl

7.9 break🔗

BreakCmd = "break" [ Ident ] ";" .

A bare break transfers control to the point immediately after the innermost enclosing while. break L transfers control to the point after the statement labelled L, which may be an if as well as a while. The search for L walks strictly outwards from the big block containing the break, so L must label a big block that properly encloses it, and that big block must contain no simple commands of its own — its label has to name the if or while, not a command in front of one.

procedure P()

{

var i: int;

i := 0;

break;

}

brk1.bpl(5,3): error: Error: break statement is not inside a loop

1 parse errors detected in brk1.bpl

procedure P()

{

var i: int;

L: i := 0;

while (i < 10) {

break L;

}

}

brk2.bpl(6,5): error: Error: break label 'L' must designate an enclosing statement

1 parse errors detected in brk2.bpl

Here L labels an assignment, not the loop, so it is not a legal break target. Note that these are reported as parse errors with a doubled error: Error: prefix: the check runs inside the parser’s big-block resolution, which routes semantic errors through the parse-error channel.

Breaking out of an if works and simply jumps to the block that follows it:

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

{

r := 0;

Skip:

if (x > 0) {

r := 1;

if (x > 10) { break Skip; }

r := 2;

}

r := r + 100;

}

implementation P(x: int) returns (r: int)

{

anon0:

r := 0;

goto Skip;

Skip:

goto anon5_Then, anon5_Else;

anon5_Then:

assume {:partition} x > 0;

r := 1;

goto anon6_Then, anon6_Else;

anon6_Then:

assume {:partition} x > 10;

goto anon4;

anon6_Else:

assume {:partition} 10 >= x;

goto anon3;

anon3:

r := 2;

goto anon4;

anon5_Else:

assume {:partition} 0 >= x;

goto anon4;

anon4:

r := r + 100;

return;

}

The paper’s degenerate case L: break L;, which section 9.5 calls a no-op equivalent to L: assert true;, is not accepted by the implementation. L labels the very big block that the break terminates, and the search only considers big blocks that strictly enclose it:

procedure P() returns (r: int)

{

r := 0;

L: break L;

r := 1;

}

brk4.bpl(4,6): error: Error: break label 'L' must designate an enclosing statement

1 parse errors detected in brk4.bpl

Breaking out of an outer loop from an inner one:

procedure Search(m: [int,int]int, N: int, X: int) returns (i: int, j: int)

{

i := 0;

Outer:

while (i < N)

{

j := 0;

while (j < i)

{

if (m[i, j] == X) { break Outer; }

j := j + 1;

}

i := i + 1;

}

}

implementation Search(m: [int,int]int, N: int, X: int) returns (i: int, j: int)

{

anon0:

i := 0;

goto Outer;

Outer:

goto anon6_LoopHead;

anon6_LoopHead:

goto anon6_LoopDone, anon6_LoopBody;

anon6_LoopBody:

assume {:partition} i < N;

j := 0;

goto anon7_LoopHead;

anon7_LoopHead:

goto anon7_LoopDone, anon7_LoopBody;

anon7_LoopBody:

assume {:partition} j < i;

goto anon8_Then, anon8_Else;

anon8_Then:

assume {:partition} m[i, j] == X;

return;

anon8_Else:

assume {:partition} m[i, j] != X;

goto anon4;

anon4:

j := j + 1;

goto anon7_LoopHead;

anon7_LoopDone:

assume {:partition} i <= j;

goto anon5;

anon5:

i := i + 1;

goto anon6_LoopHead;

anon6_LoopDone:

assume {:partition} N <= i;

return;

}

break Outer; became a plain return, because the labelled loop is the last thing in the body and the point after it is the end of the procedure.

When a loop body ends with a nested loop, the resolver injects an empty big block after the nested loop so that a break inside it has somewhere to go that is not the outer loop head. In the following program that injected block is anon5:

procedure P(N: int)

{

var i: int, j: int;

i := 0;

while (i < N)

{

i := i + 1;

j := 0;

while (j < N)

{

if (j == 3) { break; }

j := j + 1;

}

}

}

anon7_LoopBody:

assume {:partition} j < N;

goto anon8_Then, anon8_Else;

anon8_Then:

assume {:partition} j == 3;

goto anon5;

anon8_Else:

assume {:partition} j != 3;

goto anon4;

anon4:

j := j + 1;

goto anon7_LoopHead;

anon7_LoopDone:

assume {:partition} N <= j;

goto anon5;

anon5:

goto anon6_LoopHead;

anon6_LoopDone:

assume {:partition} N <= i;

return;

}

7.10 Labels, goto and return🔗

TransferCmd = ( "goto" { Attribute } Idents | "return" { Attribute } ) ";" .

goto L1, L2, ... transfers control to one of the listed labels, chosen demonically: verification must succeed for every listed successor. A single-target goto is an ordinary jump; a multi-target goto is the primitive from which all branching is built.

procedure P() returns (r: int)

ensures r == 1;

{

goto A, B;

A:

r := 1;

return;

B:

r := 2;

return;

}

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

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

Execution trace:

goto3.bpl(4,3): anon0

goto3.bpl(8,3): B

Boogie program verifier finished with 0 verified, 1 error

return ends the trace at that point. There is an implicit return at the end of every body, and any statements after a goto or return within a big block, up to the next label, are unreachable.

7.10.1 Label scoping🔗

Labels within an implementation body must be distinct:

procedure P()

{

var i: int;

L: i := 0;

goto L2;

L: i := 1;

L2: i := 2;

}

dup1.bpl(6,2): Error: more than one declaration of block name: L

1 name resolution errors detected in dup1.bpl

A goto target must exist somewhere in the same body, and that is the only restriction. There is no requirement that the target be in an enclosing statement list; the stricter check the paper describes exists in the source but is commented out. A goto may therefore jump into the body of an if or a while from outside, bypassing the assume that encodes the guard:

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

{

if (x > 0) {

Pos:

r := 1;

} else {

r := -1;

}

goto Pos;

}

implementation P(x: int) returns (r: int)

{

anon0:

goto anon3_Then, anon3_Else;

anon3_Then:

assume {:partition} x > 0;

goto Pos;

Pos:

r := 1;

goto anon2;

anon3_Else:

assume {:partition} 0 >= x;

r := -1;

goto anon2;

anon2:

goto Pos;

}

Jumping into a loop body is the more dangerous case, because it enters the loop without passing the loop head. This is Test/irreduciblecfg/Unsound.bpl from the Boogie test suite:

procedure unsound() {

var x: int;

assume(x == 0);

if (true) {

goto Inside;

}

while (x < 10000) {

Inside: x := x + 1;

}

assert(x == -1);

}

implementation unsound()

{

var x: int;

anon0:

assume x == 0;

goto anon4_Then, anon4_Else;

anon4_Then:

assume {:partition} true;

goto Inside;

anon4_Else:

assume {:partition} !true;

goto anon2;

anon2:

goto anon5_LoopHead;

anon5_LoopHead:

goto anon5_LoopDone, anon5_LoopBody;

anon5_LoopBody:

assume {:partition} x < 10000;

goto Inside;

Inside:

x := x + 1;

goto anon5_LoopHead;

anon5_LoopDone:

assume {:partition} 10000 <= x;

goto anon3;

anon3:

assert x == -1;

return;

}

7.11 From structured statements to basic blocks🔗

The translation happens once, in the parser’s big-block resolution, and is purely syntactic. /print:- /printUnstructured shows the result: the original structured body is reproduced as a comment, followed by the basic blocks.

boogie /noVerify /print:- /printUnstructured file.bpl

The rules, stated over big blocks:

• A big block with a transfer command becomes a block with the same commands and that transfer command.

• A big block with no terminator becomes a block ending in a goto to the next big block in the enclosing statement list, or a return if there is none. If it is the last big block of a loop body, the goto targets the loop head instead.

• break becomes a goto to the successor of the big block it breaks out of.

• if becomes goto Then, Else, where the Then block starts with assume {:partition} guard and the Else block with assume {:partition} !guard. With a * guard no assumptions are generated. An else if chain is unrolled: the Else block of the outer if becomes the dispatch block for the inner one.

• while becomes goto LoopHead; a LoopHead block containing the invariants and measures and ending in goto LoopDone, LoopBody; the body, whose last block jumps back to LoopHead; and a LoopDone block starting with assume {:partition} !guard.

Generated labels are prefixn for anonymous big blocks, and prefixn_Then, _Else, _LoopHead, _LoopBody, _LoopDone for the blocks a structured command introduces. The prefix starts out as anon. Every user label that starts with the current prefix extends it by one character: a 1 if the label’s next character is 0, and a 0 otherwise. So a body containing a label anon0 generates anon10, anon11, ..., and a body containing a label anon generates anon00, anon01, ... . Note that the lengthening character is chosen to differ from the colliding label, so it is not simply a run of zeroes.

One optimisation changes the shape of the output. If the first big block of a branch or a loop body is anonymous, the guard’s assume is prepended to it instead of getting a block of its own. If that block is labelled — because something might jump to it — a separate dispatch block is generated, as in the anon3_Then block of the Pos example above.

Every structured construct is expressible directly in the unstructured layer, and the paper’s examples of that still hold. The loop

i := 0;

while (i < N) {

if (a[i] == X) { break; }

i := i + 1;

}

Done:

is the same program as

i := 0;

Head:

if (i < N) {

if (a[i] == X) { goto Done; }

i := i + 1;

goto Head;

}

Done:

7.12 Loop semantics🔗

Basic blocks by themselves describe a control-flow graph that may contain cycles. Verification-condition generation needs an acyclic graph, so before a VC is built Boogie converts the CFG into a DAG. This is where a loop invariant acquires its meaning, and it is worth being precise about it because the transformation is defined on the graph, not on the while statement.

For each header of a natural loop:

• The leading run of assert and assume commands in the header block is identified. This prefix is what plays the role of loop invariant. The run stops at the first command that is not a predicate command — an assignment, a havoc, a call.

• A copy of the prefix is appended to every predecessor of the header. In predecessors that are not back edges the asserts become “loop invariant on entry” obligations; in back-edge predecessors they become “invariant maintained by the loop” obligations. assume commands in the prefix are copied only under /alwaysAssumeFreeLoopInvariants.

• In the header itself, each assert of the prefix is replaced by an assume of the same expression.

• The back edges are cut. A back-edge block that had other successors simply loses the header from its goto; a block whose only successor was the header gets assume false; and a return.

• A havoc of every variable assigned anywhere in the natural loop is inserted at the front of the header block, ahead of the invariant assumptions.

That havoc is the heart of it. On arrival at the loop head the verifier forgets everything it knew about every variable the loop can change, and is given back only what the invariants say. Everything else must be re-derived.

procedure P(N: int)

{

var i: int;

i := 0;

while (i < N)

invariant 0 <= i;

{

i := i + 1;

}

assert 0 <= i;

}

boogie /traceverify loop3.bpl

after conversion into a DAG

implementation P(N: int)

{

var i: int;

0:

goto anon0;

anon0:

i := 0;

assert 0 <= i;

goto anon3_LoopHead;

anon3_LoopHead:

havoc i;

assume 0 <= i;

goto anon3_LoopDone, anon3_LoopBody;

anon3_LoopBody:

assume {:partition} i < N;

i := i + 1;

assert 0 <= i;

assume false;

return;

anon3_LoopDone:

assume {:partition} N <= i;

assert 0 <= i;

return;

}

Read the three copies of assert 0 <= i: the one in anon0 is the entry check, the one at the end of anon3_LoopBody is the preservation check, and the one in anon3_LoopDone is the user’s own assertion after the loop, discharged from the assumption at the head plus the negated guard. The assume false; after the preservation check is what makes the body a leaf: one arbitrary iteration is verified, and nothing follows it.

The two obligations produce distinct messages:

procedure P(N: int)

{

var i: int;

i := 1;

while (i < N)

invariant i == 0;

{

i := i + 1;

}

}

inv1.bpl(6,5): Error: this loop invariant could not be proved on entry

Execution trace:

inv1.bpl(4,5): anon0

Boogie program verifier finished with 0 verified, 1 error

procedure P(N: int)

{

var i: int;

i := 0;

while (i < N)

invariant i == 0;

{

i := i + 1;

}

}

inv2.bpl(6,5): Error: this invariant could not be proved to be maintained by the loop

Execution trace:

inv2.bpl(4,5): anon0

inv2.bpl(5,3): anon2_LoopHead

inv2.bpl(8,7): anon2_LoopBody

Boogie program verifier finished with 0 verified, 1 error

7.12.1 What exactly gets havoc’d🔗

Every variable that appears as an assignment target, a havoc target, or an out-parameter of a call, anywhere in any block of the natural loop. It does not matter whether the assignment can actually change the value:

procedure P(N: int)

{

var i: int;

var k: int;

i := 0;

k := 7;

while (i < N) {

i := i + 1;

k := k;

}

assert k == 7;

}

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

Execution trace:

loop2.bpl(5,5): anon0

loop2.bpl(7,3): anon3_LoopDone

Boogie program verifier finished with 0 verified, 1 error

Deleting k := k; makes the program verify. This is the single most common source of “why can’t Boogie see that” in loop-heavy programs: an assignment anywhere in the loop, however trivial, removes the variable’s value at the loop head, and only an invariant can put it back.

7.12.2 Loops written with goto🔗

Nothing above mentions the while statement, and nothing needs to. An assert at the front of the header block of a natural loop is a loop invariant, however the loop was written:

procedure P(N: int)

{

var i: int;

i := 0;

Head:

assert 0 <= i;

goto Body, Done;

Body:

assume i < N;

i := i + 1;

goto Head;

Done:

assume N <= i;

}

boogie /traceverify /coalesceBlocks:0 gotoloop.bpl

after conversion into a DAG

implementation P(N: int)

{

var i: int;

0:

goto anon0;

anon0:

i := 0;

assert 0 <= i;

goto Head;

Head:

havoc i;

assume 0 <= i;

goto Body, Done;

Done:

assume N <= i;

return;

Body:

assume i < N;

i := i + 1;

assert 0 <= i;

assume false;

return;

}

The converse is the trap: an assert in the header block that is not in the leading predicate-command prefix is an ordinary assertion, checked after the havoc, with no invariant status at all. A single assignment before the assert is enough to break it:

procedure P(N: int)

{

var i: int;

var t: int;

i := 0;

Head:

t := i;

assert 0 <= i;

goto Body, Done;

Body:

assume i < N;

i := i + 1;

goto Head;

Done:

}

prefix1.bpl(8,5): Error: this assertion could not be proved

Execution trace:

prefix1.bpl(5,5): anon0

prefix1.bpl(6,3): Head

Boogie program verifier finished with 0 verified, 1 error

boogie /traceverify /coalesceBlocks:0 prefix1.bpl

after conversion into a DAG

implementation P(N: int)

{

var i: int;

var t: int;

0:

goto anon0;

anon0:

i := 0;

goto Head;

Head:

havoc t, i;

t := i;

assert 0 <= i;

goto Body, Done;

Done:

return;

Body:

assume i < N;

i := i + 1;

assume false;

return;

}

A while statement can never fall into this trap, because its invariants are emitted at the head ahead of the measures and of the body. (In a Civl yield procedure the yield invariants — invariant call Inv(); — are emitted ahead of the ordinary invariants, and a call is not a predicate command; but the Civl transformation removes them from the header before the CFG is converted to a DAG, so the ordinary invariants still end up in the prefix.)

7.12.3 Irreducible control flow🔗

goto can produce control-flow graphs with no single loop header. Boogie transforms these into reducible graphs by duplicating blocks, and then applies the loop transformation to the result:

procedure P(c: bool)

{

var i: int;

i := 0;

goto A, B;

A:

assert 0 <= i;

i := i + 1;

goto B;

B:

assert 0 <= i;

i := i + 1;

goto A;

}

boogie /traceverify /coalesceBlocks:0 irred.bpl

after conversion into a DAG

implementation P(c: bool)

{

var i: int;

0:

goto anon0;

anon0:

i := 0;

goto anon0_@2_B, A_dup_0;

A_dup_0:

assert 0 <= i;

i := i + 1;

assert 0 <= i;

goto B;

B:

havoc i;

assume 0 <= i;

i := i + 1;

goto A_dup_1;

A_dup_1:

assert 0 <= i;

i := i + 1;

assert 0 <= i;

assume false;

return;

anon0_@2_B:

assert 0 <= i;

goto B;

}

7.12.4 Free invariants: the tool differs from the paper🔗

Section 9.8 of the paper says a free loop invariant is assumed by both parties — the iterations of the past and the iterations of the future — and in particular that it is assumed “just before the loop”. That is not the default behaviour. Only assert commands in the header prefix are copied into the predecessors; assume commands are copied only under /alwaysAssumeFreeLoopInvariants.

procedure P()

{

var i: int;

havoc i;

while (*)

free invariant 0 <= i;

invariant 0 <= i;

{

}

}

freeinv2.bpl(7,5): Error: this loop invariant could not be proved on entry

Execution trace:

freeinv2.bpl(4,3): anon0

Boogie program verifier finished with 0 verified, 1 error

boogie /alwaysAssumeFreeLoopInvariants freeinv2.bpl

Boogie program verifier finished with 1 verified, 0 errors

The DAG shows exactly where the free invariant does and does not appear:

boogie /traceverify /coalesceBlocks:0 freeinv2.bpl

after conversion into a DAG

implementation P()

{

var i: int;

0:

goto anon0;

anon0:

havoc i;

assert 0 <= i;

goto anon2_LoopHead;

anon2_LoopHead:

havoc ;

assume 0 <= i;

assume 0 <= i;

goto anon2_LoopDone, anon2_LoopBody;

anon2_LoopBody:

assert 0 <= i;

assume false;

return;

anon2_LoopDone:

return;

}

The paper’s specific claim about free invariant false; listed first does still hold, but by a different mechanism. The assume false makes the header block a leaf during unreachable-block pruning, which removes the back edge, so there is no loop left and no entry check is generated at all:

procedure P(N: int)

{

var i: int;

i := 0;

while (i < N)

free invariant false;

invariant i == 17;

{

i := i + 1;

}

assert false;

}