Legend:

Library

Module

Module type

Parameter

Class

Class type

Library

Module

Module type

Parameter

Class

Class type

Legend:

Library

Module

Module type

Parameter

Class

Class type

Library

Module

Module type

Parameter

Class

Class type

The Core Theory signature.

The Core Theory signature includes operations on booleans, bitvectors, floating point numbers, and memories, as well as denotations of various control-flow and data-flow effects.

`include Basic`

`include Minimal`

`include Init`

`val unk : 'a Value.sort -> 'a pure`

`unk s`

an unknown value of sort `s`

.

This term explicitly denotes a term with undefined or unknown value.

`include Bitv`

`val int : 's Bitv.t Value.sort -> word -> 's bitv`

`int s x`

is a bitvector constant `x`

of sort `s`

.

`div x y`

unsigned division modulo `2^'s`

truncating towards 0.

The division by zero is defined to be a vector of all ones of size `'s`

.

`sdiv x y`

is signed division of `x`

by `y`

modulo `2^'s`

,

The signed division operator is defined in terms of the `div`

operator as follows:

/ | div x y : if not mx /\ not my | neg (div (neg x) y) if mx /\ not my x sdiv y = < | neg (div x (neg y)) if not mx /\ my | div (neg x) (neg y) if mx /\ my \ where mx = msb x, and my = msb y.

`smodulo x y`

is the signed remainder of `div x y`

modulo `2^'s`

.

This version of the signed remainder where the sign follows the dividend, and is defined via the `% = modulo`

operation as follows

/ | x % y : if not mx /\ not my | neg (neg x % y) if mx /\ not my x smodulo y = < | neg (x % (neg y)) if not mx /\ my | neg (neg x % neg y) mod m if mx /\ my \ where mx = msb x and my = msb y.

`shiftr s x m`

shifts `x`

right by `m`

bits filling with `s`

.

`shiftl s x m`

shifts `x`

left by `m`

bits filling with `s`

.

`val cast : 'a Bitv.t Value.sort -> bool -> 'b bitv -> 'a bitv`

`cast s b x`

casts `x`

to sort `s`

filling with `b`

.

If `m = size s - size (sort b) > 0`

then `m`

bits `b`

are prepended to the most significant part of the vector.

Otherwise, if `m <= 0`

, i.e., it is a narrowing cast, then the value of `b`

doesn't affect the result of evaluation.

`val concat : 'a Bitv.t Value.sort -> 'b bitv list -> 'a bitv`

`concat s xs`

concatenates a list of vectors `xs`

.

All vectors are concatenated from left to right (so that the most significant bits of the resulting vector are defined by the first element of the list and so on).

The result of concatenation are then casted to sort `s`

with all extra bits (if any) set to `zero`

.

`val append : 'a Bitv.t Value.sort -> 'b bitv -> 'c bitv -> 'a bitv`

`append s x y`

appends `x`

and `y`

and casts to `s`

.

Appends `x`

and `y`

so that in the resulting vector the vector `x`

occupies the most significant part and `y`

the least significant part. The resulting vector is then casted to the sort `s`

with extra bits (if any) set to zero.

`include Effect`

`val perform : 'a Effect.sort -> 'a eff`

`perform s`

performs a generic effect of sort `s`

.

`repeat c data`

repeats data effects until the condition `c`

holds.

`val zero : 'a Bitv.t Value.sort -> 'a bitv`

`zero s`

creates a bitvector of all zeros of sort `s`

.

`val high : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`high s x`

is the high cast of `x`

to sort `s`

.

if `m = size (sort x) - size s > 0`

then `high s x`

evaluates to `m`

most significant bits of `x`

; else if `m = 0`

then `high s x`

evaluates to the value of `x`

; else `m`

zeros are prepended to the most significant part of `x`

.

`val low : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`low s x = cast s b0 x`

is the low cast of `x`

to sort `s`

.

if `m = size (sort x) - size s < 0`

then `low s x`

evaluates to `size s`

least significant bits of `x`

; else if `m = 0`

then `high s x`

evaluates to the value of `x`

; else `m`

zeros are prepended to the most significant part of `x`

.

`val signed : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`signed s x = cast s (msb x) x`

is the signed cast of `x`

to sort `s`

.

if `m = size s - (size (sort x)) > 0`

then extends `x`

on its most significant side with `m`

bits equal to `msb x`

; else if `m = 0`

then `signed s x`

evaluates to `x`

else it evaluates to `size s`

least significant bits of `x`

.

`val unsigned : 'a Bitv.t Value.sort -> 'b bitv -> 'a bitv`

`unsigned s x = cast s b0 x`

is the unsigned cast of `x`

to sort `s`

.

if `m = size s - (size (sort x)) > 0`

then extends `x`

on its most significant side with `m`

zeros; else if `m = 0`

then `unsigned s x`

evaluates to `x`

else it evaluates to `size s`

least significant bits of `x`

.

`extract s hi lo x`

extracts bits of `x`

between `hi`

and `lo`

.

Extracts `hi-lo+1`

consecutive bits of `x`

from `hi`

to `lo`

, and casts them to sort `s`

with any excessive bits set to zero.

Note that `hi-lo+1`

is taken modulo `2^'b`

, so this operation is defined even if `lo`

is greater or equal to `hi`

.

`loadw s e m k`

loads a word from the memory `m`

.

if `e`

evaluates to `b1`

(big endian case), then the term evaluates to `low s (m[k] @ m[k+1] @ ... @ m[k+n] )`

, else the term evaluates to `low s (m[k+n] @ m[k+n-1] @ ... @ m[k] )`

where `x @ y`

is `append (vals m) x y`

, and `n`

is the smallest natural number such that `n * size (vals (sort m)) >= size s`

, an `m[i]`

is the `i`

'th value of memory `m`

. .

This is a generic function that loads words using specified endianess (`e`

could be read as `is_big_endian`

) with arbitrary byte size.

`storew e m k x`

stores a word in the memory `m`

.

Splits the word `x`

into chunks of size equal to the size of memory elements and lays them out in the big endian order, if `e`

evaluates to `b1`

, or little endian order otherwise.

`arshift x m = shiftr (msb x) m`

arithmetically shifts `x`

right by `m`

bits.

`include Float`

`include Fbasic`

`float s x`

interprets `x`

as a floating point number.

`fbits x`

is a bitvector representation of the floating point number `x`

.

`is_finite x`

holds if `x`

represents a finite number.

A floating point number is finite if it represents a number from the set of real numbers `R`

.

The predicate always holds for formats in which only finite floating point numbers are representable.

`is_nan x`

holds if `x`

represents a not-a-number.

A floating point value is not-a-number if it is neither finite nor infinite number.

The predicated never holds for formats that represent only numbers.

`is_inf x`

holds if `x`

represents an infinite number.

Never holds for formats in which infinite numbers are not representable.

`is_fpos x`

holds if `x`

represents a positive number.

The denotation is not defined if `x`

represents zero.

`is_fneg x`

hold if `x`

represents a negative number.

The denotation is not defined if `x`

represents zero.

Many operations in the Theory of Floating Point numbers are defined using the rounding mode parameter.

The rounding mode gives a precise meaning to the phrase "the closest floating point number to `x`

", where `x`

is a real number. When `x`

is not representable by the given format, some other number `x'`

is selected based on rules of the rounding mode.

`val rne : rmode`

rounding to nearest, ties to even.

The denotation is the floating point number nearest to the denoted real number. If the two nearest numbers are equally close, then the one with an even least significant digit shall be selected. The denotation is not defined, if both numbers have an even least significant digit.

`val rna : rmode`

rounding to nearest, ties away.

The denotation is the floating point number nearest to the denoted real number. If the two nearest numbers are equally close, then the one with larger magnitude shall be selected.

`val rtp : rmode`

rounding towards positive.

The denotation is the floating point number that is nearest but no less than the denoted real number.

`val rtn : rmode`

rounding towards negative.

The denotation is the floating point number that is nearest but not greater than the denoted real number.

`val rtz : rmode`

rounding towards zero.

The denotation is the floating point number that is nearest but not greater in magnitude than the denoted real number.

`val cast_float : 'f Float.t Value.sort -> rmode -> 'a bitv -> 'f float`

`cast_float s m x`

is the closest to `x`

floating number of sort `s`

.

The bitvector `x`

is interpreted as an unsigned integer in the two-complement form.

`val cast_sfloat : 'f Float.t Value.sort -> rmode -> 'a bitv -> 'f float`

`cast_sfloat s rm x`

is the closest to `x`

floating point number of sort `x`

.

The bitvector `x`

is interpreted as a signed integer in the two-complement form.

`val cast_int : 'a Bitv.t Value.sort -> rmode -> 'f float -> 'a bitv`

`cast_int s rm x`

returns an integer closest to `x`

.

The resulting bitvector should be interpreted as an unsigned two-complement integer.

`val cast_sint : 'a Bitv.t Value.sort -> rmode -> 'f float -> 'a bitv`

`cast_sint s rm x`

returns an integer closest to `x`

.

The resulting bitvector should be interpreted as a signed two-complement integer.

`fadd m x y`

is the floating point number closest to `x+y`

.

`fsub m x y`

is the floating point number closest to `x-y`

.

`fmul m x y`

is the floating point number closest to `x*y`

.

`fdiv m x y`

is the floating point number closest to `x/y`

.

`fsqrt m x`

is the floating point number closest to `sqrt x`

.

The denotation is not defined if

`fdiv m x y`

is the floating point number closest to the remainder of `x/y`

.

`fmad m x y z`

is the floating point number closest to `x * y + z`

.

`fround m x`

is the floating point number closest to `x`

rounded to an integral, using the rounding mode `m`

.

`val fconvert : 'f Float.t Value.sort -> rmode -> _ float -> 'f float`

`fconvert f r x`

is the closest to `x`

floating number in format `f`

.

`fsucc m x`

is the least floating point number representable in (sort x) that is greater than `x`

.

`fsucc m x`

is the greatest floating point number representable in (sort x) that is less than `x`

.

`pow m b a`

is a floating point number closest to `b^a`

.

Where `b^a`

is `b`

raised to the power of `a`

.

Values, such as `0^0`

, as well as `1^infinity`

and `infinity^1`

in formats that have a representation for infinity, are not defined.

`compound m x n`

is the floating point number closest to `(1+x)^n`

.

Where `b^a`

is `b`

raised to the power of `a`

.

The denotation is not defined if `x`

is less than `-1`

, or if `x`

is `n`

represent zeros, or if `x`

doesn't represent a finite floating point number.

`rootn m x n`

is the floating point number closest to `x^(1/n)`

.

Where `b^a`

is `b`

raised to the power of `a`

.

The denotation is not defined if:

`n`

is zero;`x`

is zero and n is less than zero;`x`

is not a finite floating point number;

`pown m x n`

is the floating point number closest to `x^n`

.

Where `b^a`

is `b`

raised to the power of `a`

.

The denotation is not defined if `x`

and `n`

both represent zero or if `x`

doesn't represent a finite floating point number.

`rsqrt m x`

is the closest floating point number to `1 / sqrt x`

.

The denotation is not defined if `x`

is less than or equal to zero or doesn't represent a finite floating point number.

`include Trans`

`exp m x`

is the floating point number closes to `e^x`

,

where `b^a`

is `b`

raised to the power of `a`

and `e`

is the base of natural logarithm.

`expm1 m x`

is the floating point number closes to `e^x - 1`

,

where `b^a`

is `b`

raised to the power of `a`

and `e`

is the base of natural logarithm.

`exp2 m x`

is the floating point number closes to `2^x`

,

where `b^a`

is `b`

raised to the power of `a`

.

`exp2 m x`

is the floating point number closes to `2^x - 1`

,

where `b^a`

is `b`

raised to the power of `a`

.

`exp10 m x`

is the floating point number closes to `10^x`

,

where `b^a`

is `b`

raised to the power of `a`

.

`exp10m1 m x`

is the floating point number closes to `10^x - 1`

,

where `b^a`

is `b`

raised to the power of `a`

.

`log2 m x`

is the floating point number closest to `log x / log 2`

.

`log10 m x`

is the floating point number closest to `log x / log 10`

.

`logp1 m x`

is the floating point number closest to `log (1+x)`

.

`logp1 m x`

is the floating point number closest to `log (1+x) / log 2`

.

`logp1 m x`

is the floating point number closest to `log (1+x) / log 10`

.

`sinpi m x`

is the floating point number closest to `sin (pi*x)`

.

`cospi m x`

is the floating point number closest to `cos (pi*x)`

.

`atanpi m y x`

is the floating point number closest to `atan(y/x) / pi`

.

`atanpi m y x`

is the floating point number closest to `atan(y/x) / (2*pi)`

.

`atan2 m y x`

is the floating point number closest to `atan (y/x)`

.

sectionYPositions = computeSectionYPositions($el), 10)" x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)">