bap-core-theory 2.1.0 · OCaml Package

Floating point expressions.

type t

an abstract type denoting a Core Theory floating point term.

type exp

the type of expressions of the target language.

type rmode

the type for representing rounding modes in the target language.

val error : t

an ill-formed term.

val ieee754 : ieee754 -> exp -> t

ieee754 p x is |float| s (bitv x),

where s = IEEE754.Sort.define p, and |float| is the float operation from the Core Theory.

val ieee754_var : ieee754 -> string -> t

ieee754_var p x is var v x,

where v = Var.define v s, and s = IEEE754.Sort.define p.

val ieee754_unk : ieee754 -> t

ieee754 p x is unk s,

where s = IEEE754.Sort.define p.

val ieee754_cast : ieee754 -> rmode -> exp -> t

ieee754_cast p m x is cast_float s (rmode m) (bitv x),

where s = IEEE754.Sort.define p.

val ieee754_cast_signed : ieee754 -> rmode -> exp -> t

ieee754_cast_signed p m x is cast_sfloat s (rmode m) (bitv x),

where s = IEEE754.Sort.define p.

val ieee754_convert : ieee754 -> rmode -> exp -> t

ieee754_convert p m x is fconvert s (rmode m) (float x),

where s = IEEE754.Sort.define p.

val ite : exp -> exp -> exp -> t

ite c x y is ite (bool c) (float x) (float y)

val fadd : rmode -> exp -> exp -> t

fadd m x y is fadd (rmode m) (float x) (float y).

val fsub : rmode -> exp -> exp -> t

fsub m x y is fsub (rmode m) (float x) (float y).

val fmul : rmode -> exp -> exp -> t

fmul m x y is fmul (rmode m) (float x) (float y).

val fdiv : rmode -> exp -> exp -> t

fdiv m x y is fdiv (rmode m) (float x) (float y).

val frem : rmode -> exp -> exp -> t

frem m x y is fmodulo (rmode m) (float x) (float y).

val fmin : exp -> exp -> t

fmin m x y is ite c p q,

where p = float x, and q = float y, and c = forder p q.

val fmax : exp -> exp -> t

fmax m x y is ite c q p,

where p = float x, and q = float y, and c = forder p q.

val fabs : exp -> t

fabs x is fabs (float x).

val fneg : exp -> t

fneg x is fneg (float x).

val fsqrt : rmode -> exp -> t

fsqrt x is fsqrt (float x).

val fround : rmode -> exp -> t

fround x is fround (float x).

val let_bit : string -> exp -> exp -> t

let_bit s x y is scoped @@ fun v -> (bool x) (float [y|s->v]).

Note, the let_bit rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

val let_reg : string -> exp -> exp -> t

let_reg s x y is scoped @@ fun v -> (bitv x) (float [y|s->v]).

Note, the let_reg rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

val let_mem : string -> exp -> exp -> t

let_mem s x y is scoped @@ fun v -> (mem x) (float [y|s->v]).

Note, the let_mem rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

val let_float : string -> exp -> exp -> t

let_float s x y is scoped @@ fun v -> (float x) (float [y|s->v]).

Note, the let_float rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

package bap-core-theory