8 Bitvectors, floating point and rounding modes🔗

Boogie has three families of machine-number types: bitvectors bvn, floating-point numbers floatSeE, and the rounding-mode type rmode. All three are thin types: the language gives them literals, a handful of operators, and nothing else. Every real operation — bitvector addition, fp.sqrt, integer/bitvector conversion — is written as an uninterpreted Boogie function carrying a :bvbuiltin or :builtin attribute that names an SMT-LIB symbol. Boogie passes that name through to the solver verbatim and does not check it.

The 2008 paper covers bitvectors in section 4.2 and the :bvBuiltin directive in section 11.1. Floating point, rounding modes, and most of the bitvector operation catalogue postdate it; see Divergences from This is Boogie 2 for the specific divergences.

Every listing below was run with Boogie 3.5.7 against Z3 5.0.0, and the outputs shown are the outputs it produced.

8.1 Bitvector types🔗

A bitvector type is written bvn for a decimal n. It is not a keyword and it does not appear in the type grammar:

TypeAtom<out Bpl.Type ty>

= ( "int"

| "real"

| "bool"

/* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */

| "(" Type<out ty> ")"

)

.

Instead, any type identifier is parsed as an UnresolvedTypeIdentifier and name resolution recognises the shape: a name beginning with bv whose remaining characters are all digits becomes a BvType of that width (Source/Core/AST/AbsyType.cs). Consequently bv itself is an ordinary identifier, but bv16 is not:

type bv16;

name-clash.bpl(1,5): Error: type name: bv16 is registered for bitvectors

1 name resolution errors detected in name-clash.bpl

Because the check is purely syntactic, bv followed by digits is reserved at every width, including widths you will never use, and including bv0, which the paper lists as a legal type.

A bvn is translated to the SMT sort (_ BitVec n). Bitvectors may be used anywhere any other type may: as map domains and ranges, as quantified variables, in old, in havoc, and as procedure parameters.

type Word = bv32;

const unique zero : bv8;

var mem : [bv32]bv8;

procedure P(x: Word) returns (r: bv8)

{

var b: bv8;

b := 5bv8;

assert b == 5bv8;

assert b != 6bv8;

r := mem[x];

assert (forall y: bv8 :: y == y);

}

Boogie program verifier finished with 1 verified, 0 errors

Boogie’s own pretty-printer escapes bitvector type names, so /print emits var b: \bv8;. That form re-parses correctly — a leading backslash is the general escape for identifiers that collide with keywords — but it is startling the first time you see it.

8.1.1 Bitvector literals🔗

A bitvector literal is a single token:

bvlit = digit {digit} 'b' 'v' digit {digit}.

There is no whitespace and no sign: 5bv8, 18446744073709551615bv64. The value is written in decimal and the type is part of the literal, so a literal never needs a type annotation and never unifies with int.

The paper says a literal XbvK is legal when X is 0 or is expressible in K bits. The implementation does not enforce this. An out-of-range literal is silently reduced modulo 2K, because the SMT lineariser emits only the low K bits:

procedure P()

{

assert 256bv8 == 0bv8;    // 256 does not fit in 8 bits

assert 300bv8 == 44bv8;   // literals are reduced modulo 2^8

}

Boogie program verifier finished with 1 verified, 0 errors

Literals whose width is a multiple of 8 are emitted as SMT hexadecimal (#x2c); others as binary (#b111).

8.2 Extraction and concatenation🔗

These are the only two bitvector operations in the language proper.

8.2.1 Extraction🔗

Extraction reuses the map-selection brackets. The parser recognises e[hi:lo] by noticing that the index expression is a Nat followed by a colon and another Nat:

CoercionExpression<out Expr e>

= ArrayExpression<out e>

{ ":"

( Type<out coercedTo>

| Nat<out bn>           /* This means that we really look at a bitvector

expression t[a:b] */

)

}

.

Both bounds must be literal naturals. The index interval is half-open and written high-first: x[hi:lo] selects the bits at positions lo through hi-1, with bit 0 the least significant bit. The result has type bv(hi-lo). In SMT terms, x[hi:lo] becomes ((_ extract hi-1 lo) x).

procedure P(b: bv32)

{

var x: bv8;

x := 5bv8;                     // 0000_0101

assert x[1:0] == 1bv1;         // bit 0

assert x[3:0] == 5bv3;         // bits 2..0

assert x[4:2] == 1bv2;         // bits 3..2

assert x[8:4] == 0bv4;         // bits 7..4

x := 1bv4 ++ 2bv4;             // left operand supplies the high bits

assert x == 18bv8;             // 0001_0010

assert x[8:4] == 1bv4;

assert x[4:0] == 2bv4;

assert (13bv6 ++ 4bv3)[5:2] == 3bv3;

assert b[24:18] ++ b[18:7] == b[24:7];

assert b == b[32:30] ++ b[30:24] ++ b[24:18] ++ b[18:7] ++ b[7:6] ++ b[6:5] ++ b[5:0];

}

Boogie program verifier finished with 1 verified, 0 errors

The last three assertions are the paper’s own worked examples, and they still hold. Half-open intervals make the width arithmetic come out right: b[24:18] is 6 bits wide, and adjacent slices fuse when the middle bound repeats.

8.2.2 Concatenation🔗

BvTerm<out Expr e0>

= Term<out e0>

{ "++"  Term<out e1>   (. e0 = new BvConcatExpr(x, e0, e1); .)

}

.

a ++ b has type bv(m+n) when a: bvm and b: bvn. The left operand supplies the high-order bits (it becomes SMT (concat a b)). The operator is left-associative and sits between the relational operators and the additive operators in the precedence hierarchy: a ++ b == c parses as (a ++ b) == c, and i + j ++ k parses as (i + j) ++ k. Extraction, being a suffix on an atom, binds tighter than both.

8.2.3 Typing rules🔗

BvExtractExpr.Typecheck rejects negative bounds and rejects hi < lo:

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

{

r := x[0:1];        // Error: start index bigger than end index

r := x[16:0];       // Error: operand has too few bits

}

bv-extract-errors.bpl(3,8): Error: start index in extract must be no bigger than the end index

bv-extract-errors.bpl(4,8): Error: extract operand must be a bitvector of at least 16 bits (got bv8)

2 type checking errors detected in bv-extract-errors.bpl

Note the second message carefully. The constraint imposed on the operand is that it have at least hi - lo bits — not at least hi bits. The paper requires K ≥ N ≥ M ≥ 0; the implementation only requires K ≥ N - M and N ≥ M ≥ 0.

Two further restrictions come from the grammar rather than the type checker, and they surface at two different phases. Bounds must be literal Nat tokens; anything else is parsed as an ordinary index expression, and the stray bounds object is caught during name resolution:

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

{

r := x[1+1:3];      // Error

}

bv-extract-errors2.bpl(3,12): Error: bitvector bounds in illegal position

1 name resolution errors detected in bv-extract-errors2.bpl

and they may not be parenthesised:

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

{

r := x[(1:3)];      // Error

}

bv-extract-errors3.bpl(3,13): error: parentheses around bitvector bounds are not allowed

1 parse errors detected in bv-extract-errors3.bpl

8.3 What bitvectors do not have🔗

Literals, ==, !=, extraction and concatenation are the complete list of built-in bitvector operations. There is no arithmetic, no bitwise connective, no shift, no ordering, and no unary negation or complement:

procedure P(x: bv8, y: bv8) returns (r: bv8, b: bool)

{

r := x + y;

r := x * y;

r := x div y;

r := -x;

b := x < y;

}

bv-noarith.bpl(3,9): Error: invalid argument types (bv8 and bv8) to binary operator +

bv-noarith.bpl(4,9): Error: invalid argument types (bv8 and bv8) to binary operator *

bv-noarith.bpl(5,9): Error: invalid argument types (bv8 and bv8) to binary operator div

bv-noarith.bpl(6,7): Error: invalid argument type (bv8) to unary operator -

bv-noarith.bpl(7,9): Error: invalid argument types (bv8 and bv8) to binary operator <

5 type checking errors detected in bv-noarith.bpl

The standard library shipped with the tool (/lib:base, /lib:node, /lib:set_size) contains no bitvector declarations either. Everything else is up to you, via :bvbuiltin.

8.4 :bvbuiltin and the SMT-LIB bitvector operations🔗

A function declared with {:bvbuiltin "op"} is not axiomatised and not declared to the solver. Instead, every application F(a1, ..., an) is printed as (op a1 ... an). The mechanism is a single method, SMTLibExprLineariser.ExtractBuiltin in Source/Provers/SMTLib/SMTLibLineariser.cs: it reads the :bvbuiltin string attribute, and failing that the :builtin string attribute. TypeDeclCollector calls the same method, and skips the (declare-fun ...) when it returns non-null — which is why such a function never reaches the solver as a symbol of its own.

Four consequences follow directly, and all four are worth internalising.

• The string is not validated. Boogie neither knows nor checks the set of legal SMT symbols; whatever you write is what the solver is asked to interpret.

• The signature is not checked against the operation. Boogie checks that your calls match the Boogie signature you wrote; it has no idea what arity or sorts the SMT symbol actually wants.

• :bvbuiltin and :builtin are the same mechanism. :bvbuiltin is consulted first if both are present. The only behavioural difference is described under Indexed operations below.

• The attribute name is case-sensitive, and a misspelling is silent. An unrecognised attribute is ignored, and the function simply stays uninterpreted.

That last point deserves a demonstration, because the 2008 paper spells the attribute :bvBuiltin with a capital B:

function {:bvBuiltin "bvadd"} ADD(bv8, bv8) returns (bv8);   // capital B: not the attribute

procedure P() { assert ADD(1bv8, 2bv8) == 3bv8; }

bv-capitalB.bpl(2,17): Error: this assertion could not be proved

Execution trace:

bv-capitalB.bpl(2,17): anon0

Boogie program verifier finished with 0 verified, 1 error

ADD here is an ordinary uninterpreted function with no axioms, so of course ADD(1bv8, 2bv8) need not be 3bv8. No warning is issued for an unrecognised attribute.

8.4.1 The catalogue🔗

Source/Provers/SMTLib/SmtLibNameUtils.cs holds a list of SMT-LIB reserved words; a Boogie identifier that collides with one is renamed by prefixing q@, so a Boogie function you happen to call bvadd is declared to the solver as q@bvadd and cannot accidentally shadow the theory symbol. That list doubles as a good inventory of the operation names that are expected to work in a builtin string, though nothing stops you from using a name that is not on it. The following declarations were all exercised against Z3 5.0.0. W is the operand width; unless stated otherwise both operands and the result have the same width.

The following program declares one function from every family and checks a concrete value for each. It verifies.

// unary

function {:bvbuiltin "bvnot"} NOT(bv8) returns (bv8);

function {:bvbuiltin "bvneg"} NEG(bv8) returns (bv8);

// bitwise

function {:bvbuiltin "bvand"}  AND(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvor"}   OR(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvxor"}  XOR(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvnand"} NAND(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvnor"}  NOR(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvxnor"} XNOR(bv8, bv8) returns (bv8);

// arithmetic

function {:bvbuiltin "bvadd"}  ADD(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvsub"}  SUB(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvmul"}  MUL(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvudiv"} UDIV(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvurem"} UREM(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvsdiv"} SDIV(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvsrem"} SREM(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvsmod"} SMOD(bv8, bv8) returns (bv8);

// shifts

function {:bvbuiltin "bvshl"}  SHL(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvlshr"} LSHR(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvashr"} ASHR(bv8, bv8) returns (bv8);

// comparisons

function {:bvbuiltin "bvult"} ULT(bv8, bv8) returns (bool);

function {:bvbuiltin "bvule"} ULE(bv8, bv8) returns (bool);

function {:bvbuiltin "bvugt"} UGT(bv8, bv8) returns (bool);

function {:bvbuiltin "bvuge"} UGE(bv8, bv8) returns (bool);

function {:bvbuiltin "bvslt"} SLT(bv8, bv8) returns (bool);

function {:bvbuiltin "bvsle"} SLE(bv8, bv8) returns (bool);

function {:bvbuiltin "bvsgt"} SGT(bv8, bv8) returns (bool);

function {:bvbuiltin "bvsge"} SGE(bv8, bv8) returns (bool);

function {:bvbuiltin "bvcomp"} COMP(bv8, bv8) returns (bv1);

// extend / rotate / repeat (indexed)

function {:bvbuiltin "zero_extend 8"} ZEXT(bv8) returns (bv16);

function {:bvbuiltin "sign_extend 8"} SEXT(bv8) returns (bv16);

function {:bvbuiltin "(_ rotate_left 3)"}  ROL(bv8) returns (bv8);

function {:bvbuiltin "(_ rotate_right 3)"} ROR(bv8) returns (bv8);

function {:bvbuiltin "(_ repeat 2)"} REP(bv8) returns (bv16);

procedure P()

{

assert NOT(1bv8)  == 254bv8;

assert NEG(1bv8)  == 255bv8;

assert AND(12bv8, 10bv8) == 8bv8;

assert OR(12bv8, 10bv8)  == 14bv8;

assert XOR(12bv8, 10bv8) == 6bv8;

assert NAND(12bv8, 10bv8) == 247bv8;

assert NOR(12bv8, 10bv8)  == 241bv8;

assert XNOR(12bv8, 10bv8) == 249bv8;

assert ADD(250bv8, 10bv8) == 4bv8;         // wraps

assert SUB(4bv8, 10bv8)   == 250bv8;

assert MUL(16bv8, 16bv8)  == 0bv8;

assert UDIV(250bv8, 10bv8) == 25bv8;

assert UREM(250bv8, 12bv8) == 10bv8;

assert SDIV(250bv8, 2bv8)  == 253bv8;      // -6 / 2 == -3

assert SREM(250bv8, 4bv8)  == 254bv8;      // -6 srem 4 == -2 (sign of dividend)

assert SMOD(250bv8, 4bv8)  == 2bv8;        // -6 smod 4 ==  2 (sign of divisor)

assert SHL(1bv8, 3bv8)   == 8bv8;

assert LSHR(128bv8, 3bv8) == 16bv8;

assert ASHR(128bv8, 3bv8) == 240bv8;

assert ULT(1bv8, 200bv8);

assert ULE(1bv8, 1bv8);

assert UGT(200bv8, 1bv8);

assert UGE(1bv8, 1bv8);

assert SLT(200bv8, 1bv8);                  // 200 is -56 signed

assert SLE(200bv8, 200bv8);

assert SGT(1bv8, 200bv8);

assert SGE(1bv8, 1bv8);

assert COMP(1bv8, 1bv8) == 1bv1;

assert ZEXT(200bv8) == 200bv16;

assert SEXT(200bv8) == 65480bv16;

assert ROL(129bv8) == 12bv8;

assert ROR(129bv8) == 48bv8;

assert REP(1bv8) == 257bv16;

}

Boogie program verifier finished with 1 verified, 0 errors

Points worth extracting from that listing:

• bvudiv/bvurem are unsigned; bvsdiv/bvsrem truncate toward zero and take the sign of the dividend; bvsmod floors and takes the sign of the divisor. -6 srem 4 == -2 but -6 smod 4 == 2.

• Shift amounts are bitvectors of the same width as the value shifted, not integers.

• Every arithmetic operation wraps modulo 2W. There is no overflow signal.

• bvcomp yields a bv1, not a bool.

Z3 also accepts several non-standard bitvector symbols, which likewise work through :bvbuiltin but are not portable to other solvers:

function {:bvbuiltin "bvredor"}  REDOR(bv8) returns (bv1);

function {:bvbuiltin "bvredand"} REDAND(bv8) returns (bv1);

function {:bvbuiltin "ext_rotate_left"} EROL(bv8, bv8) returns (bv8);

function {:bvbuiltin "bvumul_noovfl"} NOOVFL(bv8, bv8) returns (bool);

procedure P()

{

assert REDOR(0bv8) == 0bv1;

assert REDAND(255bv8) == 1bv1;

assert EROL(129bv8, 3bv8) == 12bv8;

assert NOOVFL(16bv8, 16bv8) == false;

}

Boogie program verifier finished with 1 verified, 0 errors

8.4.2 Indexed operations🔗

SMT-LIB operations that take numeric parameters are written (_ name n ...). Boogie passes the attribute string through unchanged, so you must write the underscore form yourself.

There is exactly one exception, and it is hard-coded: if a :bvbuiltin string starts with "sign_extend " or "zero_extend ", ExtractBuiltin wraps it in (_ ... ) for you. This special case does not apply to :builtin, which is otherwise interchangeable.

Written explicitly, :builtin behaves identically to :bvbuiltin:

function {:builtin "(_ sign_extend 8)"} SEXT_B(bv8) returns (bv16);

function {:builtin "bvadd"}             ADD_B(bv8, bv8) returns (bv8);

procedure P() {

assert SEXT_B(200bv8) == 65480bv16;

assert ADD_B(1bv8, 2bv8) == 3bv8;

}

Boogie program verifier finished with 1 verified, 0 errors

The practical rule: prefer :bvbuiltin for bitvector operations, and always write indexed operations in full (_ ... ) form; the extend special case then costs nothing.

8.4.3 Axioms about builtin functions🔗

The paper pairs :bvBuiltin with a :bvIgnore attribute on axioms, so that a solver with native bitvector support can be told to drop the fallback axiomatisation. :bvIgnore does not exist in the implementation — the string appears nowhere in the source. Axioms mentioning a builtin function are emitted to the solver like any other axiom, with the function replaced by the interpreted SMT symbol.

8.5 Integers and bitvectors🔗

Conversion between int and bvn is also a builtin function. (_ int2bv n) is standard; the reverse direction has several spellings in Z3, and they do not all mean the same thing.

function {:bvbuiltin "(_ int2bv 8)"} int2bv8(int) returns (bv8);

function {:bvbuiltin "bv2int"}       bv2int8(bv8) returns (int);

function {:bvbuiltin "bv2nat"}       bv2nat8(bv8) returns (int);

function {:bvbuiltin "ubv_to_int"}   ubv2int8(bv8) returns (int);

function {:bvbuiltin "sbv_to_int"}   sbv2int8(bv8) returns (int);

procedure P()

{

assert int2bv8(5) == 5bv8;

assert int2bv8(258) == 2bv8;      // taken modulo 2^8

assert int2bv8(-1) == 255bv8;

assert bv2int8(200bv8) == 200;    // unsigned in Z3

assert bv2nat8(200bv8) == 200;

assert ubv2int8(200bv8) == 200;

assert sbv2int8(200bv8) == -56;

assert (forall b: bv8 :: int2bv8(bv2int8(b)) == b);

}

Boogie program verifier finished with 1 verified, 0 errors

With Z3 5.0.0, bv2int, bv2nat and ubv_to_int all interpret the bitvector as unsigned; only sbv_to_int is signed. This is solver behaviour, not Boogie behaviour — Boogie is merely a conduit. Mixing integer and bitvector reasoning is also expensive; if you can stay in one theory, do.

Boogie’s own int(...) and real(...) coercions do not accept bitvectors or floats.

8.6 Floating-point types🔗

A floating-point type is written floatSeE, where S is the significand size including the implicit leading bit and E is the exponent width. Like bitvector types it is recognised by name resolution, not by the grammar. The familiar IEEE 754 formats are

Note that the two components appear in the opposite order in Boogie and in SMT-LIB: Boogie writes significand first, SMT-LIB writes exponent first.

Two float types are the same type only if both components agree. There is no implicit widening, no promotion, and no numeric literal that adapts to the context:

type float32 = float24e8;   // IEEE binary32

type float64 = float53e11;  // IEEE binary64

procedure P(a: float32, b: float64) returns (r: float32)

{

r := a;

r := b;        // Error

r := a + b;    // Error

}

float-types.bpl(7,2): Error: mismatched types in assignment command (cannot assign float64 to float24e8)

float-types.bpl(8,9): Error: invalid argument types (float32 and float64) to binary operator +

2 type checking errors detected in float-types.bpl

Type synonyms are a convenient way to name the formats — Test/floats/Equal1.bpl and Test/floats/TypeMismatch2.bpl do it — but they are not what the test suite generally does: most of the tests that mention two widths, including Test/floats/TypeMismatch1.bpl, Test/floats/CastToLowerPrec.bpl and Test/roundingmodes/CorrectTypeConv.bpl, write float24e8 and float53e11 out in full. Notice also that the assignment diagnostic above prints the synonym on one side and the expanded name on the other.

Boogie validates neither S nor E in a type name. Degenerate sizes are accepted by the front end and left to the solver: Z3 5.0.0 wants at least two significand bits and at least two exponent bits, so float2e2 is the smallest format it accepts.

Float literals are stricter than float type names. The size check inside BigFloat (reached from BigFloat.TryParseExact) requires S > 1 and E > 1, so you can declare a variable of a degenerate format but you can never write a literal of one:

procedure P()

{

var f: float1e2;

var g: float2e1;

f := 0x1.0e0f1e2;

g := 0x1.0e0f2e1;

}

float-litsize.bpl(5,8): error: incorrectly formatted floating point

float-litsize.bpl(6,8): error: incorrectly formatted floating point

2 parse errors detected in float-litsize.bpl

Unlike bvn, float type names are not reserved. You may declare type float24e8; or type rmode; and Boogie will accept the declaration — and then ignore it, because name resolution tries the builtin patterns before consulting the user type table:

type rmode;        // accepted, and then ignored

type float24e8;    // accepted, and then ignored

procedure P(r: rmode, f: float24e8)

{

assert r == RNE;           // Error: r is still the builtin rounding-mode type

assert f == 0x1.0e0f24e8;  // Error: f is still float24e8

}

name-shadow.bpl(6,3): Error: this assertion could not be proved

Execution trace:

name-shadow.bpl(6,3): anon0

name-shadow.bpl(7,3): Error: this assertion could not be proved

Execution trace:

name-shadow.bpl(6,3): anon0

Boogie program verifier finished with 0 verified, 2 errors

Both assertions fail because r and f really do have the builtin types; the user declarations are dead. No warning is issued.

8.7 Floating-point literals🔗

Float literals are single lexer tokens:

float = [ '-' ] '0' 'x' hexdigit {hexdigit} '.' hexdigit {hexdigit}

'e' [ '-' ] digit {digit} 'f' digit {digit} 'e' digit {digit}

| '0' 'N' 'a' 'N' digit {digit} 'e' digit {digit}

| '0' 'n' 'a' 'n' digit {digit} 'e' digit {digit}

| '0' '+' 'o' 'o' digit {digit} 'e' digit {digit}

| '0' '-' 'o' 'o' digit {digit} 'e' digit {digit} .

So the finite form is

[-]0xHH.HHeDfSeE

where HH are hexadecimal digits, D is a signed decimal exponent, and fSeE is the type suffix, spelled exactly as the type name. No whitespace anywhere.

The exponent is a power of sixteen, not of two or ten. The value is the hexadecimal fraction multiplied by 16D (BigFloat.TryParseHexFormat computes the binary exponent as decExp * 4 plus the position of the leading significand bit). This differs from C99 hex float literals, where the p exponent is a power of two.

function {:builtin "(_ to_fp 11 53) RNE"} R2D(real) returns (float53e11);

procedure P()

{

assert 0x1.0e0f53e11  == R2D(1.0);

assert 0x3.2e1f53e11  == R2D(50.0);      // 0x3.2 * 16^1

assert 0x1.0e1f53e11  == R2D(16.0);      // the exponent is a power of 16

assert 0x1.0e-1f53e11 == R2D(0.0625);

assert 0xf.0e0f53e11  == R2D(15.0);

}

Boogie program verifier finished with 1 verified, 0 errors

8.7.1 Literals must be exact🔗

The parser uses BigFloat.TryParseExact, which is strict in three ways: the value must be representable without any rounding, it must not overflow to infinity, and it must not underflow. A literal that violates any of these is a parse error, not a type error, and the message is always the same.

procedure P()

{

var f: float24e8;

f := 0x0.ffffffe0f24e8;    // 24 significand bits: fine

f := 0x1.ffffffe0f24e8;    // 25 bits: rejected

f := 0x0.8e32f24e8;        // 2^127: fine

f := 0x1.0e32f24e8;        // 2^128 would round to +oo: rejected

f := 0x0.000008e-32f24e8;  // 2^-149, the least positive value: fine

f := 0x0.000004e-32f24e8;  // underflows to zero: rejected

}

float-strict.bpl(5,8): error: incorrectly formatted floating point

float-strict.bpl(7,8): error: incorrectly formatted floating point

float-strict.bpl(9,8): error: incorrectly formatted floating point

3 parse errors detected in float-strict.bpl

The accepted lines really do denote the extremal values:

function {:builtin "fp.isSubnormal"} isSubnormal(float24e8) returns (bool);

function {:builtin "fp.isNormal"}    isNormal(float24e8) returns (bool);

function {:builtin "fp.isInfinite"}  isInf(float24e8) returns (bool);

function {:builtin "fp.mul"}         MUL(rmode, float24e8, float24e8) returns (float24e8);

procedure P()

{

assert isSubnormal(0x0.000008e-32f24e8);

assert isNormal(0x0.8e32f24e8);

assert isInf(MUL(RNE, 0x0.8e32f24e8, 0x2.0e0f24e8));

}

Boogie program verifier finished with 1 verified, 0 errors

The consequence of exactness is that the natural way to write a "round" decimal such as 0.1 is not to write a literal at all, but to convert a real with a to_fp builtin, as the examples throughout this chapter do. Note also that the significand you write is not normalised for you: whether 0x1.ffffff or 0x0.ffffff fits depends on where the leading bit lands.

8.7.2 NaN and infinity🔗

0NaNSeE (or 0nanSeE) and 0+ooSeE / 0-ooSeE are the special literals. There is only one NaN value per format — SMT-LIB’s floating-point theory has a single NaN, with no payload and no sign.

function {:builtin "fp.isNaN"}      isNaN(float24e8) returns (bool);

function {:builtin "fp.isInfinite"} isInf(float24e8) returns (bool);

function {:builtin "fp.isZero"}     isZero(float24e8) returns (bool);

function {:builtin "fp.isNegative"} isNeg(float24e8) returns (bool);

procedure P()

{

assert isNaN(0NaN24e8);

assert isNaN(0nan24e8);

assert 0NaN24e8 == 0nan24e8;      // one NaN value, spelled two ways

assert isInf(0+oo24e8);

assert isInf(0-oo24e8);

assert isNeg(0-oo24e8);

assert isZero(0x0.0e0f24e8);

assert isZero(-0x0.0e0f24e8);

assert isNeg(-0x0.0e0f24e8);

}

Boogie program verifier finished with 1 verified, 0 errors

Signed zeros are written as ordinary literals, 0x0.0e0f24e8 and -0x0.0e0f24e8. Older versions of Boogie had 0+zeroSeE and 0-zeroSeE literals; they were removed, and the token grammar no longer admits them:

procedure P()

{

var d: float53e11;

d := 0+zero53e11;

d := 0-zero53e11;

}

float-nozero.bpl(4,9): Error: undeclared identifier: zero53e11

float-nozero.bpl(5,9): Error: undeclared identifier: zero53e11

2 name resolution errors detected in float-nozero.bpl

8.7.3 The sign is part of the token🔗

There is no unary minus on floats. The leading - in -0x1.0e0f24e8 belongs to the float token; a space, or applying it to a special literal, changes the parse and then fails type checking:

procedure P()

{

var f: float24e8;

f := -0x1.0e0f24e8;    // fine: the sign is part of the literal token

f := - 0x1.0e0f24e8;   // Error

f := -0NaN24e8;        // Error

}

float-negation.bpl(5,7): Error: invalid argument type (float24e8) to unary operator -

float-negation.bpl(6,7): Error: invalid argument type (float24e8) to unary operator -

2 type checking errors detected in float-negation.bpl

To negate a float value use {:builtin "fp.neg"}.

8.8 The built-in float operators🔗

Unlike bitvectors, floats do get some operators from the language itself. BinaryOperator.Typecheck admits +, -, *, /, <, <=, >, >=, == and != when both operands have the same float type. It does not admit div, mod, **, or unary -:

procedure P(x: float24e8, y: float24e8) returns (r: float24e8)

{

r := x ** y;

r := x div y;

r := x mod y;

}

float-nopow.bpl(3,9): Error: invalid argument types (float24e8 and float24e8) to binary operator **

float-nopow.bpl(4,9): Error: invalid argument types (float24e8 and float24e8) to binary operator div

float-nopow.bpl(5,9): Error: invalid argument types (float24e8 and float24e8) to binary operator mod

3 type checking errors detected in float-nopow.bpl

8.8.1 Arithmetic rounds to nearest, ties to even🔗

SMTLibExprLineariser emits fp.add RNE, fp.sub RNE, fp.mul RNE and fp.div RNE for the four arithmetic operators. The rounding mode is hard-wired; there is no way to change what + means.

function {:builtin "fp.add"} ADD(rmode, float24e8, float24e8) returns (float24e8);

procedure P(a: float24e8, b: float24e8)

{

assert a + b == ADD(RNE, a, b);        // native + is fp.add RNE

assert a + b == ADD(RTZ, a, b);        // Error: not every mode agrees

}

float-rne.bpl(6,3): Error: this assertion could not be proved

Execution trace:

float-rne.bpl(5,3): anon0

Boogie program verifier finished with 0 verified, 1 error

If you need any other mode, declare the operation as a builtin and pass the mode explicitly.

8.8.2 Comparison is IEEE; equality is not🔗

The four ordering operators become fp.leq, fp.lt, fp.geq, fp.gt, which are the IEEE comparisons: every comparison involving NaN is false.

== and !=, however, are not fp.eq. They do become a float-specific VC operator, but VCExprBinaryFloatOp.Accept dispatches the "==" and "!=" cases to the generic equality visitor, so they print as SMT = and (not (= ...)) on the floating-point sort — structural identity of values. The two notions of equality disagree exactly on NaN and on signed zero:

function {:builtin "fp.eq"} FEQ(float24e8, float24e8) returns (bool);

procedure P()

{

// structural (==) versus IEEE (fp.eq)

assert 0x0.0e0f24e8 != -0x0.0e0f24e8;      // +0 and -0 are different values

assert FEQ(0x0.0e0f24e8, -0x0.0e0f24e8);   // but IEEE-equal

assert 0NaN24e8 == 0NaN24e8;               // there is one NaN value

assert !FEQ(0NaN24e8, 0NaN24e8);           // and it is not IEEE-equal to itself

assert 0+oo24e8 != 0-oo24e8;

assert !(0NaN24e8 < 0x0.0e0f24e8);

assert !(0NaN24e8 >= 0x0.0e0f24e8);

}

Boogie program verifier finished with 1 verified, 0 errors

This is the single most important thing to know about floats in Boogie. If you are modelling a language whose == is IEEE equality, you must declare {:builtin "fp.eq"} and use that; == in Boogie is substitutivity-preserving equality, which is what makes floats usable as map keys and under old, but which is not what a C compiler does.

The same asymmetry shows up in a subtler way: because == is real equality, a NaN flows through an :inline function or an assignment unchanged, and fp.isNaN still holds afterwards. Test/floats/Equal1.bpl is exactly this test.

8.9 Rounding modes🔗

rmode is a builtin type with five values. The constants have both a long and a short spelling, and they are parser keywords rather than identifiers:

| ("roundNearestTiesToEven" | "RNE")    (. e = new LiteralExpr(t, RoundingMode.RNE); .)

| ("roundNearestTiesToAway" | "RNA")    (. e = new LiteralExpr(t, RoundingMode.RNA); .)

| ("roundTowardPositive" | "RTP")       (. e = new LiteralExpr(t, RoundingMode.RTP); .)

| ("roundTowardNegative" | "RTN")       (. e = new LiteralExpr(t, RoundingMode.RTN); .)

| ("roundTowardZero" | "RTZ")           (. e = new LiteralExpr(t, RoundingMode.RTZ); .)

The type is exactly these five values — the solver cannot invent a sixth:

procedure P(r: rmode)

{

assert r == RNE || r == RNA || r == RTP || r == RTN || r == RTZ;

assert RNE == roundNearestTiesToEven;

assert RNA == roundNearestTiesToAway;

assert RTP == roundTowardPositive;

assert RTN == roundTowardNegative;

assert RTZ == roundTowardZero;

assert RNE != RNA && RNA != RTP && RTP != RTN && RTN != RTZ;

}

Boogie program verifier finished with 1 verified, 0 errors

rmode values can be stored in variables, passed to and returned from procedures, havocked, quantified over, and used as map keys. The only operators defined on them are == and !=; arithmetic and ordering are type errors (Test/roundingmodes/InvalidOperators.bpl).

Because the ten constant names are keywords, they cannot be used as identifiers:

var RNE: int;

reserved.bpl(1,5): error: invalid Ident

1 parse errors detected in reserved.bpl

The backslash escape works if you really need the name: var \RNE: int; declares an integer variable. Note also that a function cannot be named RNA and friends (Test/roundingmodes/InvalidFuncName.bpl).

There is no :rm attribute for pinning a rounding mode onto a function. Test/roundingmodes/RMAttributeInvalid.bpl shows {:builtin "fp.add" :rm "RNE"} failing, but read that test carefully: the failure is a parse error, and it has nothing to do with :rm. Boogie’s attribute syntax admits exactly one key/value group per pair of braces, so {:builtin "fp.add" :other "x"} fails identically. Written as two attributes, {:builtin "fp.add"} {:rm "RNE"}, the program parses and :rm is simply ignored: the rounding mode of a builtin function is fixed either by the builtin string or by an rmode parameter (see below).

8.10 Float operations via :builtin🔗

Everything beyond the ten built-in operators is a :builtin function naming an SMT-LIB floating-point symbol. Operations that round take a rounding mode as their first argument, either as an rmode parameter or baked into the attribute string.

Note that fp.rem, fp.abs, fp.neg, fp.min and fp.max are exact and therefore take no rounding mode. Here is one declaration of each, with a checked value:

type f32 = float24e8;

// arithmetic taking an explicit rounding mode

function {:builtin "fp.add"}  ADD(rmode, f32, f32) returns (f32);

function {:builtin "fp.sub"}  SUB(rmode, f32, f32) returns (f32);

function {:builtin "fp.mul"}  MUL(rmode, f32, f32) returns (f32);

function {:builtin "fp.div"}  DIV(rmode, f32, f32) returns (f32);

function {:builtin "fp.fma"}  FMA(rmode, f32, f32, f32) returns (f32);

function {:builtin "fp.sqrt"} SQRT(rmode, f32) returns (f32);

function {:builtin "fp.roundToIntegral"} RTI(rmode, f32) returns (f32);

// arithmetic with no rounding mode

function {:builtin "fp.abs"} ABS(f32) returns (f32);

function {:builtin "fp.neg"} NEG(f32) returns (f32);

function {:builtin "fp.rem"} REM(f32, f32) returns (f32);

function {:builtin "fp.min"} MIN(f32, f32) returns (f32);

function {:builtin "fp.max"} MAX(f32, f32) returns (f32);

// predicates

function {:builtin "fp.leq"} LEQ(f32, f32) returns (bool);

function {:builtin "fp.lt"}  LT(f32, f32) returns (bool);

function {:builtin "fp.geq"} GEQ(f32, f32) returns (bool);

function {:builtin "fp.gt"}  GT(f32, f32) returns (bool);

function {:builtin "fp.eq"}  EQ(f32, f32) returns (bool);

// classification

function {:builtin "fp.isNormal"}    isNormal(f32) returns (bool);

function {:builtin "fp.isSubnormal"} isSubnormal(f32) returns (bool);

function {:builtin "fp.isZero"}      isZero(f32) returns (bool);

function {:builtin "fp.isInfinite"}  isInfinite(f32) returns (bool);

function {:builtin "fp.isNaN"}       isNaN(f32) returns (bool);

function {:builtin "fp.isNegative"}  isNegative(f32) returns (bool);

function {:builtin "fp.isPositive"}  isPositive(f32) returns (bool);

procedure P()

{

assert ADD(RNE, 0x1.0e0f24e8, 0x1.0e0f24e8) == 0x2.0e0f24e8;

assert SUB(RNE, 0x2.0e0f24e8, 0x1.0e0f24e8) == 0x1.0e0f24e8;

assert MUL(RNE, 0x2.0e0f24e8, 0x2.0e0f24e8) == 0x4.0e0f24e8;

assert DIV(RNE, 0x2.0e0f24e8, 0x4.0e0f24e8) == 0x8.0e-1f24e8;

assert FMA(RNE, 0x2.0e0f24e8, 0x2.0e0f24e8, 0x1.0e0f24e8) == 0x5.0e0f24e8;

assert SQRT(RNE, 0x4.0e0f24e8) == 0x2.0e0f24e8;

assert RTI(RTZ, 0x1.8e0f24e8) == 0x1.0e0f24e8;

assert ABS(-0x1.0e0f24e8) == 0x1.0e0f24e8;

assert NEG(0x1.0e0f24e8) == -0x1.0e0f24e8;

assert REM(0x5.0e0f24e8, 0x4.0e0f24e8) == 0x1.0e0f24e8;

assert MIN(0x1.0e0f24e8, 0x2.0e0f24e8) == 0x1.0e0f24e8;

assert MAX(0x1.0e0f24e8, 0x2.0e0f24e8) == 0x2.0e0f24e8;

assert LEQ(0x1.0e0f24e8, 0x2.0e0f24e8);

assert LT(0x1.0e0f24e8, 0x2.0e0f24e8);

assert GEQ(0x2.0e0f24e8, 0x1.0e0f24e8);

assert GT(0x2.0e0f24e8, 0x1.0e0f24e8);

assert EQ(0x1.0e0f24e8, 0x1.0e0f24e8);

assert isNormal(0x1.0e0f24e8);

assert !isSubnormal(0x1.0e0f24e8);

assert isZero(-0x0.0e0f24e8);

assert isInfinite(0+oo24e8);

assert isNaN(0NaN24e8);

assert isNegative(0-oo24e8);

assert isPositive(0x1.0e0f24e8);

}

Boogie program verifier finished with 1 verified, 0 errors

8.10.1 Fixing the rounding mode in the attribute🔗

An SMT builtin string is pasted in as the head of an application, so it may carry arguments. {:builtin "fp.add RNE"} declares a two-argument addition whose mode is fixed. Both styles work, and they agree:

function {:builtin "fp.add"}        ADD(rmode, float24e8, float24e8) returns (float24e8);

function {:builtin "fp.add RTN"}    ADD_RTN(float24e8, float24e8) returns (float24e8);

function {:builtin "(_ fp.to_sbv 32)"} TO_SBV(rmode, float24e8) returns (bv32);

function {:builtin "(_ to_fp 8 24) RNE"} f32(real) returns (float24e8);

procedure P()

{

// 1 + 1.5*2^-24 is not representable; the mode decides which way it goes

assert ADD(RNE, 0x1.0e0f24e8, 0x1.8e-6f24e8) == 0x1.000002e0f24e8;

assert ADD(RTN, 0x1.0e0f24e8, 0x1.8e-6f24e8) == 0x1.0e0f24e8;

assert ADD_RTN(0x1.0e0f24e8, 0x1.8e-6f24e8)  == 0x1.0e0f24e8;

assert TO_SBV(RNE, f32(2.5)) == 2bv32;

assert TO_SBV(RNA, f32(2.5)) == 3bv32;

assert TO_SBV(RTP, f32(2.5)) == 3bv32;

assert TO_SBV(RTN, f32(2.5)) == 2bv32;

assert TO_SBV(RTZ, f32(2.5)) == 2bv32;

}

Boogie program verifier finished with 1 verified, 0 errors

Passing the mode as an rmode argument is more flexible: it can be a variable, so a procedure can be verified for all five modes at once, or for a mode chosen by the caller.

8.10.2 Conversions🔗

(_ to_fp e s) is heavily overloaded in SMT-LIB, and which overload you get depends on the argument sorts you declare in Boogie. This is the one place where getting the Boogie signature right really matters, because Boogie will not tell you if it is wrong.

Note again the argument order: SMT-LIB writes (_ to_fp E S) with the exponent width first, while the Boogie result type floatSeE names the significand first.

// into float24e8, rounding mode fixed in the attribute

function {:builtin "(_ to_fp 8 24) RNE"} f32_of_int(int) returns (float24e8);

function {:builtin "(_ to_fp 8 24) RNE"} f32_of_real(real) returns (float24e8);

// rounding mode supplied as an argument

function {:builtin "(_ to_fp 8 24)"} f32_of_real_rm(rmode, real) returns (float24e8);

function {:builtin "(_ to_fp 8 24)"} f32_of_f64(rmode, float53e11) returns (float24e8);

function {:builtin "(_ to_fp 11 53)"} f64_of_f32(rmode, float24e8) returns (float53e11);

// bitvector reinterpretation (no rounding mode: bit pattern -> float)

function {:builtin "(_ to_fp 8 24)"} f32_of_bits(bv32) returns (float24e8);

// signed / unsigned bitvector -> float (rounding mode required)

function {:builtin "(_ to_fp 8 24)"} f32_of_sbv(rmode, bv32) returns (float24e8);

function {:builtin "(_ to_fp_unsigned 8 24)"} f32_of_ubv(rmode, bv32) returns (float24e8);

// float -> bitvector / real

function {:builtin "(_ fp.to_sbv 32)"} sbv32_of_f32(rmode, float24e8) returns (bv32);

function {:builtin "(_ fp.to_ubv 32)"} ubv32_of_f32(rmode, float24e8) returns (bv32);

function {:builtin "fp.to_real"} real_of_f32(float24e8) returns (real);

procedure P()

{

assert f32_of_int(5) == 0x5.0e0f24e8;

assert f32_of_real(0.5) == 0x8.0e-1f24e8;

assert f32_of_real_rm(RTZ, 0.5) == 0x8.0e-1f24e8;

assert f32_of_f64(RNE, 0x1.0e0f53e11) == 0x1.0e0f24e8;

assert f64_of_f32(RNE, 0x1.0e0f24e8) == 0x1.0e0f53e11;

assert f32_of_bits(1065353216bv32) == 0x1.0e0f24e8;   // 0x3f800000

assert f32_of_sbv(RNE, 4294967295bv32) == -0x1.0e0f24e8;

assert f32_of_ubv(RNE, 4294967295bv32) == 0x1.0e8f24e8;

assert sbv32_of_f32(RTZ, -0x2.0e0f24e8) == 4294967294bv32;

assert ubv32_of_f32(RTZ, 0x2.0e0f24e8) == 2bv32;

assert real_of_f32(0x2.0e0f24e8) == 2.0;

}

Boogie program verifier finished with 1 verified, 0 errors

fp.to_sbv and fp.to_ubv are partial in SMT-LIB: the result is unspecified when the value is NaN, infinite, or out of range. fp.to_real is likewise unspecified on NaN and infinities. Guard your calls with fp.isNaN / fp.isInfinite if that matters.

8.11 Interaction with the rest of the language🔗

Floats, bitvectors and rounding modes are ordinary types for every other purpose. They can be global or local variables, procedure parameters, map domains and ranges, quantified variables, and havoc targets:

var g: float24e8;

var m: [rmode]float24e8;

var mem: [bv32]bv8;

procedure P() returns (r: rmode)

modifies g, m;

{

havoc g;

havoc r;

m := m[RNE := 0x1.0e0f24e8];

assert m[RNE] == 0x1.0e0f24e8;

assert (exists x: float24e8 :: x == g);

assert (forall a: bv32 :: mem[a] == mem[a]);

}

Boogie program verifier finished with 1 verified, 0 errors

Because == on floats is real equality, floats are usable as map keys, and havoc x; assert x == x; holds even when x is NaN. This is precisely why Test/floats/Havoc.bpl needs a bound on x before fp.eq(x,x) becomes provable.

8.11.1 Counterexamples🔗

Verification failures involving floats behave as usual. A classic:

function {:builtin "(_ to_fp 8 24) RNE"} f32(int) returns (float24e8);

procedure Sum()

{

var tick, time: float24e8;

var i: int;

tick := f32(1) / f32(10);

time := f32(0);

i := 0;

while (i < 10)

invariant 0 <= i;

{

time := time + tick;

i := i + 1;

}

assert time == f32(1);

}

float-roundoff.bpl(17,3): Error: this assertion could not be proved

Execution trace:

float-roundoff.bpl(8,8): anon0

float-roundoff.bpl(11,3): anon3_LoopHead

float-roundoff.bpl(11,3): anon3_LoopDone

Boogie program verifier finished with 0 verified, 1 error

With /printModel:1, float values appear in the model in the solver’s own notation, as an (fp sign exponent significand) triple of bitvectors, and bitvector values appear in Boogie literal syntax:

procedure P(x: float24e8, b: bv8)

{

assert x == 0x1.0e0f24e8;

assert b == 1bv8;

}

boogie /printModel:1 /normalizeNames:1 float-model.bpl

float-model.bpl(3,3): Error: this assertion could not be proved

Execution trace:

float-model.bpl(3,3): anon0

*** MODEL

b -> 0bv8

x -> (fp 1bv1 0bv8 128bv23)

ControlFlow -> {

0 0 -> 4

0 2 -> (- 3)

0 4 -> 2

else -> (- 3)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

b -> 0bv8

x -> (fp 1bv1 0bv8 128bv23)

*** END_STATE

*** END_MODEL

float-model.bpl(4,3): Error: this assertion could not be proved

Execution trace:

float-model.bpl(3,3): anon0

*** MODEL

b -> 0bv8

x -> (fp 0bv1 127bv8 0bv23)

ControlFlow -> {

0 0 -> 4

0 2 -> (- 1)

0 4 -> 2

else -> (- 1)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

b -> 0bv8

x -> (fp 0bv1 127bv8 0bv23)

*** END_STATE

*** END_MODEL

Boogie program verifier finished with 0 verified, 2 errors

The triple is (fp sign biased-exponent trailing-significand): (fp 1bv1 0bv8 128bv23) is a negative subnormal, and (fp 0bv1 127bv8 0bv23) is 1.0. Boogie passes the solver’s text through unchanged; it does not translate float values back into Boogie literal syntax, and /printModel takes only the values 0 and 1.

8.11.2 Solver dependence🔗

Apart from literal parsing, type checking and the fixed RNE rounding of the built-in float operators, none of the semantics in this chapter is implemented by Boogie; it is delegated to the solver. One practical consequence is that no command-line option affects bitvectors or floats. The only mentions of the subject in CommandLineOptions.cs are the {:builtin} and {:bvbuiltin} entries in the /attrHelp text; there is no option to switch bitvector encodings or float semantics. The one relevant knob is the SMT logic, which by default Boogie does not set at all for Z3 (CVC5 and Yices2 get (set-logic ALL)); /proverOpt:LOGIC=string sends an explicit (set-logic ...) if you need one.

/proverLog:file records the SMT stream actually sent to the solver, which is where to look when you want to see exactly how a builtin string, a signature, or an extraction was rendered.

8.12 Divergences from This is Boogie 2🔗

• Floating point, rounding modes, and the float/rmode types do not exist in the paper at all. Section 4.2 covers only bitvectors.

• Extraction bounds. The paper requires K ≥ N ≥ M ≥ 0 for b[N:M] on a bvK. The implementation checks only N ≥ M ≥ 0 and K ≥ N-M.

• Literal range. The paper says XbvK is legal only when X fits in K bits. The implementation accepts any X and truncates modulo 2K.

• Attribute spelling. The paper writes {:bvBuiltin "bvadd 8"} — capital B, and a width appended to the operation. The attribute is spelled :bvbuiltin, all lower case; attribute names are case-sensitive and an unrecognised one is silently dropped, so the paper’s spelling produces an uninterpreted function rather than an error. The string is an SMT-LIB symbol with no width appended: the width comes from the argument sorts. The paper predates SMT-LIB 2, which is why the syntax differs.

• :bvIgnore does not exist. The paper’s mechanism for telling a bitvector-aware prover to skip fallback axioms was never implemented. Axioms about builtin functions are emitted as-is.

• bv0. The paper lists it as a type; Boogie accepts it and Z3 rejects it.