Parameter Elementary.Theory

include Bap_core_theory.Theory.Basic
include Bap_core_theory.Theory.Minimal
include Bap_core_theory.Theory.Init

var v is the value of the variable v.

unk s an unknown value of sort s.

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

val let_ : 'a Bap_core_theory.Theory.var -> 'a Bap_core_theory.Theory.pure -> 'b Bap_core_theory.Theory.pure -> 'b Bap_core_theory.Theory.pure

let_ v exp body bind the value of exp to v body.

ite c x y is x if c evaluates to b1 else y.

include Bap_core_theory.Theory.Bool

b0 is false aka 0 bit

b1 is true aka 1 bit

inv x inverts x.

val and_ : Bap_core_theory.Theory.bool -> Bap_core_theory.Theory.bool -> Bap_core_theory.Theory.bool

and_ x y is a conjunction of x and y.

val or_ : Bap_core_theory.Theory.bool -> Bap_core_theory.Theory.bool -> Bap_core_theory.Theory.bool

or_ x y is a disjunction of x and y.

include Bap_core_theory.Theory.Bitv

int s x is a bitvector constant x of sort s.

msb x is the most significant bit of x.

lsb x is the least significant bit of x.

neg x is two-complement unary minus

not x is one-complement negation.

add x y addition modulo 2^'s

sub x y subtraction modulo 2^'s

mul x y multiplication modulo 2^'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.

modulo x y is the remainder of div x y modulo 2^'s.

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.

logand x y is a bitwise logical and of x and y.

logor x y is a bitwise logical or of x and y.

logxor x y is a bitwise logical xor of x and 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.

sle x y binary predicate for singed less than or equal

ule x y binary predicate for unsigned less than or equal

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.

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.

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 Bap_core_theory.Theory.Memory

load m k is the value associated with the key k in the memory m.

store m k x a memory m in which the key k is associated with the word x.

include Bap_core_theory.Theory.Effect

perform s performs a generic effect of sort s.

set v x changes the value stored in v to the value of x.

jmp dst passes the control to a program located at dst.

goto lbl passes the control to a program labeled with lbl.

seq x y performs effect x, after that perform effect y.

blk lbl data ctrl a labeled sequence of effects.

repeat c data repeats data effects until the condition c holds.

branch c lhs rhs if c holds then performs lhs else rhs.

zero s creates a bitvector of all zeros of sort s.

is_zero x holds if x is a bitvector of all zeros

non_zero x holds if x is not a zero bitvector.

succ x is the successor of x.

pred x is the predecessor of x.

nsucc x n is the nth successor of x.

npred x is the nth predecessor of x.

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.

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.

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.

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.

rshift x m = shiftr b0 x m shifts x right by m bits

lshift x y = shiftl b0 x m shifts x left by m bits.

eq x y holds if x and y are bitwise equal.

eq x y holds if x and y are not bitwise equal.

slt x y signed strict less than.

ult x y unsigned strict less than.

sgt x y signed strict greater than.

ugt x y unsigned strict greater than.

sge x y signed greater or equal than.

sge x y signed greater or equal than.

include Bap_core_theory.Theory.Float
include Bap_core_theory.Theory.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_fzero x holds if x represents a zero.

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.

Rounding modes

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.

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.

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.

rounding towards positive.

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

rounding towards negative.

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

rounding towards zero.

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

requal x y holds if rounding modes are equal.

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.

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.

cast_int s rm x returns an integer closest to x.

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

cast_sint s rm x returns an integer closest to x.

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

fneg x is -x

fabs x the absolute value of x.

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.

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.

forder x y holds if floating point number x is less than y.

The denotation is not defined if either of arguments do not represent a floating point number.

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.

hypot m x y is the closest floating point number to sqrt(x^2 + y^2).

The denotation is not defined if x or y do not represent finite floating point numbers.

include Bap_core_theory.Theory.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.

log m x is the floating point number closest to log x.

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.

sin m x is the floating point number closest to sin x.

cos m x is the floating point number closest to cos x.

tan m x is the floating point number closest to tan x.

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).

asin m x is the floating point number closest to asin x.

acos m x is the floating point number closest to acos x.

atan m x is the floating point number closest to atan x.

atan2 m y x is the floating point number closest to atan (y/x).

sinh m x is the floating point number closest to sinh x.

cosh m x is the floating point number closest to cosh x.

tanh m x is the floating point number closest to tanh x.

asinh m x is the floating point number closest to asinh x.

acosh m x is the floating point number closest to acosh x.

atanh m x is the floating point number closest to atanh x.