Desugar (bap-core-theory.Bap_core_theory.Theory.Pass.Desugar)

Parameters

module CT : Core

Signature

include Basic

include Minimal

include Init

val var : 'a var -> 'a pure

var v is the value of the variable v.

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.

val let_ : 'a var -> 'a pure -> 'b pure -> 'b pure

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

val ite : bool -> 'a pure -> 'a pure -> 'a pure

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

include Bool

val b0 : bool

b0 is false aka 0 bit

val b1 : bool

b1 is true aka 1 bit

val inv : bool -> bool

inv x inverts x.

val and_ : bool -> bool -> bool

and_ x y is a conjunction of x and y.

val or_ : bool -> bool -> bool

or_ x y is a disjunction of x and y.

include Bitv

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

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

val msb : 's bitv -> bool

msb x is the most significant bit of x.

val lsb : 's bitv -> bool

lsb x is the least significant bit of x.

val neg : 's bitv -> 's bitv

neg x is two-complement unary minus

val not : 's bitv -> 's bitv

not x is one-complement negation.

val add : 's bitv -> 's bitv -> 's bitv

add x y addition modulo 2^'s

val sub : 's bitv -> 's bitv -> 's bitv

sub x y subtraction modulo 2^'s

val mul : 's bitv -> 's bitv -> 's bitv

mul x y multiplication modulo 2^'s

val div : 's bitv -> 's bitv -> 's bitv

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.

val sdiv : 's bitv -> 's bitv -> 's bitv

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.

val modulo : 's bitv -> 's bitv -> 's bitv

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

val smodulo : 's bitv -> 's bitv -> 's bitv

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.

val logand : 's bitv -> 's bitv -> 's bitv

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

val logor : 's bitv -> 's bitv -> 's bitv

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

val logxor : 's bitv -> 's bitv -> 's bitv

logxor x y is a bitwise logical xor of x and y.

val shiftr : bool -> 's bitv -> 'b bitv -> 's bitv

shiftr s x m shifts x right by m bits filling with s.

val shiftl : bool -> 's bitv -> 'b bitv -> 's bitv

shiftl s x m shifts x left by m bits filling with s.

val sle : 'a bitv -> 'a bitv -> bool

sle x y binary predicate for singed less than or equal

val ule : 'a bitv -> 'a bitv -> bool

ule x y binary predicate for unsigned less than or equal

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 Memory

val load : ('a, 'b) mem -> 'a bitv -> 'b bitv

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

val store : ('a, 'b) mem -> 'a bitv -> 'b bitv -> ('a, 'b) mem

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

include Effect

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

perform s performs a generic effect of sort s.

val set : 'a var -> 'a pure -> data eff

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

val jmp : _ bitv -> ctrl eff

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

val goto : label -> ctrl eff

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

val seq : 'a eff -> 'a eff -> 'a eff

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

val blk : label -> data eff -> ctrl eff -> unit eff

blk lbl data ctrl an optionally labeled sequence of effects.

If lbl is Label.null then the block is unlabeled. If it is not Label.null then the denotations will preserve the label and assume that this blk is referenced from some other blocks.

since 2.4.0 the [blk] operator accepts (and welcomes)

Label.null as the label in cases when the block is not really expected to be called from anywhere else.

val repeat : bool -> data eff -> data eff

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

val branch : bool -> 'a eff -> 'a eff -> 'a eff

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

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

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

val is_zero : 'a bitv -> bool

is_zero x holds if x is a bitvector of all zeros

val non_zero : 'a bitv -> bool

non_zero x holds if x is not a zero bitvector.

val succ : 'a bitv -> 'a bitv

succ x is the successor of x.

val pred : 'a bitv -> 'a bitv

pred x is the predecessor of x.

val nsucc : 'a bitv -> int -> 'a bitv

nsucc x n is the nth successor of x.

val npred : 'a bitv -> int -> 'a bitv

npred x is the nth predecessor of x.

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.

val extract : 'a Bitv.t Value.sort -> 'b bitv -> 'b bitv -> _ bitv -> 'a bitv

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.

val loadw : 'c Bitv.t Value.sort -> bool -> ('a, _) mem -> 'a bitv -> 'c bitv

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.

val storew : bool -> ('a, 'b) mem -> 'a bitv -> 'c bitv -> ('a, 'b) mem

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.

val arshift : 'a bitv -> 'b bitv -> 'a bitv

arshift x m = shiftr (msb x) m arithmetically shifts x right by m bits.

val rshift : 'a bitv -> 'b bitv -> 'a bitv

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

val lshift : 'a bitv -> 'b bitv -> 'a bitv

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

val eq : 'a bitv -> 'a bitv -> bool

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

val neq : 'a bitv -> 'a bitv -> bool

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

val slt : 'a bitv -> 'a bitv -> bool

slt x y signed strict less than.

val ult : 'a bitv -> 'a bitv -> bool

ult x y unsigned strict less than.

val sgt : 'a bitv -> 'a bitv -> bool

sgt x y signed strict greater than.

val ugt : 'a bitv -> 'a bitv -> bool

ugt x y unsigned strict greater than.

val sge : 'a bitv -> 'a bitv -> bool

sge x y signed greater or equal than.

val uge : 'a bitv -> 'a bitv -> bool

sge x y signed greater or equal than.

include Float

include Fbasic

val float : 
  ('r, 's) format Float.t Value.sort ->
  's bitv ->
  ('r, 's) format float

float s x interprets x as a floating-point number.

val fbits : ('r, 's) format float -> 's bitv

fbits x is a bitvector representation of the floating-point number x.

val is_finite : 'f float -> bool

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.

val is_nan : 'f float -> bool

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.

val is_inf : 'f float -> bool

is_inf x holds if x represents an infinite number.

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

val is_fzero : 'f float -> bool

is_fzero x holds if x represents a zero.

val is_fpos : 'f float -> bool

is_fpos x holds if x represents a positive number.

The denotation is not defined if x represents zero.

val is_fneg : 'f float -> bool

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.

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 requal : rmode -> rmode -> bool

requal x y holds if rounding modes are equal.

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.

val fneg : 'f float -> 'f float

fneg x is -x

val fabs : 'f float -> 'f float

fabs x the absolute value of x.

val fadd : rmode -> 'f float -> 'f float -> 'f float

fadd m x y is the floating-point number closest to x+y.

val fsub : rmode -> 'f float -> 'f float -> 'f float

fsub m x y is the floating-point number closest to x-y.

val fmul : rmode -> 'f float -> 'f float -> 'f float

fmul m x y is the floating-point number closest to x*y.

val fdiv : rmode -> 'f float -> 'f float -> 'f float

fdiv m x y is the floating-point number closest to x/y.

val fsqrt : rmode -> 'f float -> 'f float

fsqrt m x returns the closest floating-point number to r, where r is such number that r*r is equal to x.

If x is a negative finite non-zero number, or is nan, or is the negative infinity, then sqrt x is nan. If x is the positive infinity then fsqrt x is the positive infinity.

val fmodulo : rmode -> 'f float -> 'f float -> 'f float

fdiv m x y is the floating-point number closest to the remainder of x/y.

val fmad : rmode -> 'f float -> 'f float -> 'f float -> 'f float

fmad m x y z is the floating-point number closest to x * y + z.

val fround : rmode -> 'f float -> 'f float

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.

val fsucc : 'f float -> 'f float

fsucc m x is the least floating-point number representable in (sort x) that is greater than x.

val fpred : 'f float -> 'f float

fsucc m x is the greatest floating-point number representable in (sort x) that is less than x.

val forder : 'f float -> 'f float -> bool

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.

val pow : rmode -> 'f float -> 'f float -> 'f float

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.

val compound : rmode -> 'f float -> 'a bitv -> 'f float

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.

val rootn : rmode -> 'f float -> 'a bitv -> 'f float

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;

val pown : rmode -> 'f float -> 'a bitv -> 'f float

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.

val rsqrt : rmode -> 'f float -> 'f float

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.

val hypot : rmode -> 'f float -> 'f float -> 'f float

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 Trans

val exp : rmode -> 'f float -> 'f float

exp m x is the floating-point number closest to e^x,

where b^a is b raised to the power of a and e is the base of natural logarithm.

val expm1 : rmode -> 'f float -> 'f float

expm1 m x is the floating-point number closest to e^x - 1,

where b^a is b raised to the power of a and e is the base of natural logarithm.

val exp2 : rmode -> 'f float -> 'f float

exp2 m x is the floating-point number closest to 2^x,

where b^a is b raised to the power of a.

val exp2m1 : rmode -> 'f float -> 'f float

exp2 m x is the floating-point number closest to 2^x - 1,

where b^a is b raised to the power of a.

val exp10 : rmode -> 'f float -> 'f float

exp10 m x is the floating-point number closest to 10^x,

where b^a is b raised to the power of a.

val exp10m1 : rmode -> 'f float -> 'f float

exp10m1 m x is the floating-point number closest to 10^x - 1,

where b^a is b raised to the power of a.

val log : rmode -> 'f float -> 'f float

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

val log2 : rmode -> 'f float -> 'f float

log2 m x is the floating-point number closest to log x / log 2.

val log10 : rmode -> 'f float -> 'f float

log10 m x is the floating-point number closest to log x / log 10.

val logp1 : rmode -> 'f float -> 'f float

logp1 m x is the floating-point number closest to log (1+x).

val log2p1 : rmode -> 'f float -> 'f float

logp1 m x is the floating-point number closest to log (1+x) / log 2.

val log10p1 : rmode -> 'f float -> 'f float

logp1 m x is the floating-point number closest to log (1+x) / log 10.

val sin : rmode -> 'f float -> 'f float

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

val cos : rmode -> 'f float -> 'f float

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

val tan : rmode -> 'f float -> 'f float

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

val sinpi : rmode -> 'f float -> 'f float

sinpi m x is the floating-point number closest to sin (pi*x).

val cospi : rmode -> 'f float -> 'f float

cospi m x is the floating-point number closest to cos (pi*x).

val atanpi : rmode -> 'f float -> 'f float

atanpi m y x is the floating-point number closest to atan(y/x) / pi.

val atan2pi : rmode -> 'f float -> 'f float -> 'f float

atanpi m y x is the floating-point number closest to atan(y/x) / (2*pi).

val asin : rmode -> 'f float -> 'f float

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

val acos : rmode -> 'f float -> 'f float

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

val atan : rmode -> 'f float -> 'f float

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

val atan2 : rmode -> 'f float -> 'f float -> 'f float

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

val sinh : rmode -> 'f float -> 'f float

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

val cosh : rmode -> 'f float -> 'f float

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

val tanh : rmode -> 'f float -> 'f float

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

val asinh : rmode -> 'f float -> 'f float

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

val acosh : rmode -> 'f float -> 'f float

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

val atanh : rmode -> 'f float -> 'f float

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