-
Notifications
You must be signed in to change notification settings - Fork 112
Draft floating point Boogie language extension
This wiki details the proposed syntax for the floating-point extension for Boogie. The float type proposed is the IEEE-754 floating point, a standard which can be found at http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=4610935&filter=AND(p_Publication_Number:4610933)
The proposed floating point syntax is based on the SMT-LIB standard, a summary of which can be found here: http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml
The proposal and discussion history for this extension can be found at https://github.com/boogie-org/boogie/issues/29
A floating point variable 'name' with 'exp' exponent bits and 'sig' significand bits can be declared using the syntax:
var name : float<exp, sig>;
Standard predefined types are also accepted as listed below:
| Predefined Type | Equivalent Declaration |
|---|---|
| float16 | float<5, 11> |
| float32 | float<8, 24> |
| float64 | float<11, 53> |
| float128 | float<15, 113> |
For example, a variable 'name' with type equivalent to IEEE-binary64 could be declared with:
var name : float64;
A floating point constant with a 'sign' sign, 'exp_value' exponent, and 'sig_value' significand can be declared using the syntax:
float(sign, exp_value, sig_value)
Where sign is a boolean and exp_value and sig_value are bitvectors, declared in the existing bitvector constant syntax. The size of these bitvectors determines the size of each field of the generated constant. For example, the declaration:
float(true, 15bv05, 0bv10)
Gives us an IEEE-binary16 sized floating point with decimal value 1.0
An additional proposed syntax for declaring a constant with 'exp' exponent bits, 'sig' significand bits, and 'bitvalue' constant value is:
float<exp, sig>(bitvalue)
For example, we can generate the same constant given in the earlier example with the line:
float<5, 11>(15360bv16)
Special constants with 'exp' exponent bits and 'sig' significand bits can of course be generated by constructing a floating point constant using the bitvector associated constant. Alternatively, it is possible to use the following syntax:
| Value | Declaration |
|---|---|
| NaN | float<exp, sig>(NaN) |
| +oo | float<exp, sig>(+oo) |
| -oo | float<exp, sig>(-oo) |
| +zero | float<exp, sig>(+zero) |
| -zero | float<exp, sig>(-zero) |
The following operators are built into Boogie with the following syntax, where x and y are floating point values with identical exponent and significand sizes. Note that each of these operators is assumed to use the round to nearest (RNE) rounding mode. For an explanation on how to use different rouding modes, see the section "SMT-LIBv2 operators via 'builtin' attribute." Note also that the data type returned by each operation is listed in the third column; when a function returns data of type float, that return value is assumed to have the same exponent and significand bit sizes as x and y.
| Operator | Boogie Equivalent | Return Type |
|---|---|---|
| fp.neg(x) | -x | float |
| fp.add(x, y) | x + y | float |
| fp.sub(x, y) | x - y | float |
| fp.mul(x, y) | x * y | float |
| fp.div(x, y) | x / y | float |
| fp.leq(x, y) | x <= y | boolean |
| fp.lt(x, y) | x < y | boolean |
| fp.geq(x, y) | x >= y | boolean |
| fp.gt(x, y) | x > y | boolean |
| fp.eq(x, y) | x == y | boolean |
First, the operators listed in the section "built-in operators" can be modified to use the following rounding modes:
| Rounding Mode | Acronym |
|---|---|
| Round Nearest Ties To Even | RNE |
| Round Nearest Ties To Away | RNA |
| Round Toward Positive | RTP |
| Round Toward Negative | RTN |
| Round Toward Zero | RTZ |
A given operator 'fp.op' can be set to use the rounding mode 'rounding_mode' by creating a new function with 'function_name' that takes in type arguments 'args' and returns a value of type 'return_type' with the syntax below:
function {:builtin "fp.op" :rm "rounding_mode"} 'function_name'(args) returns(return_type);
For example, to create a function that acts as the operator "fp.add" with rouding mode "RTZ" that takes in IEEE_binary16 sized values, we could use the following declaration:
function {:builtin "fp.add" :rm "RTZ" } FP_ADD_FLOAT16_RTZ(float16, float16) returns(float16);
Second, the "builtin" attribute can be used to generate the floating point operators listed below using similar syntax to that above. Descriptions of these functions can be found in the SMT-LIB standard. Note that 'x', 'y', and 'z' are all floating points with equal exponent and significand bit sizes. Note also that when functions return a value of type float, that value is assumed to have the same exponent and significand bit sizes as the arguments to the function.
| Operators | Return Type |
|---|---|
| fp.abs(x) | float |
| fp.fma(x, y, z) | float |
| fp.sqrt(x) | float |
| fp.rem(x, y) | float |
| fp.roundToIntegral(x) | float |
| fp.min(x, y) | boolean |
| fp.max(x, y) | boolean |
| fp.isNormal(x) | boolean |
| fp.isSubnormal(x) | boolean |
| fp.isZero(x) | boolean |
| fp.isInfinite(x) | boolean |
| fp.isNaN(x) | boolean |
| fp.isNegative(x) | boolean |
| fp.isPositive(x) | boolean |
For example, to create a function to calculate the absolute value of an IEEE-binary32 sized 'x' with rounding mode RNA:
function {:builtin "fp.abs" :rm "RNA" } FP_ABS_FLOAT32_RNA(float32) returns(float32);
Conversion to and from floating point values in Boogie is also done using the "builtin" attribute. The following conversions are well defined, where the argument given to an operator is the data type given to the function. Note that when float is given as an argument or return type, the number of exponent and significand bits are defined as part of the function declaration. Also note that a rounding mode may be defined for each conversion to a floating point type:
| Operator | Return Type |
|---|---|
| to_fp(float) | float |
| to_fp(real) | float |
| to_fp(bit_vec)* | float |
| to_fp_unsigned(bit_vec) | float |
| fp.to_ubv(float) | bit_vec |
| fp.to_sbv(float) | bit_vec |
| fp.to_real(float) | real |
*When converting from a bit vector to a floating point value using this builtin definition, the bitvector must be the same size as the resulting floating point value and, in particular, the first 'exp' bits of the bitvector become the exponent bits of the resulting floating point while the remaining bits become the significand of the resulting floating point. To treat the given bitvector as a signed two's complement integer, a special attribute 'ai' must be given with the value "True." For example, to convert a size 16 bitvector to a IEEE-binary16 floating point value directly, one could declare the following function:
function {:builtin "to_fp" } TO_FLOAT16_BITVECTOR(bv) returns(float16);
While to convert a bitvector representing signed two's complement integer to a IEEE-binary16 floating point with rouding mode RNA, one could declare the following function:
function {:builtin "to_fp" :rm "RNA" :ai "True" } TO_FLOAT16_SINTEGER_RNA(bv) returns(float16);