bap-core-theory 2.1.0 · OCaml Package

Booleans.

type t

an abstract type denoting a Core Theory boolean term.

type exp

the type of expressions of the target language

val error : t

an ill-formed term.

val eq : exp -> exp -> t

eq x y is eq (bitv x) (bitv y).

val neq : exp -> exp -> t

neq x y is neq (bitv x) (bitv y).

val lt : exp -> exp -> t

lt x y is lt (bitv x) (bitv y).

val le : exp -> exp -> t

le x y is le (bitv x) (bitv y).

val slt : exp -> exp -> t

slt x y is slt (bitv x) (bitv y).

val sle : exp -> exp -> t

sle x y is sle (bitv x) (bitv y).

val var : string -> t

var s is var Bool.t (ctxt s).

val int : word -> t

int x is b0 is Bitvec.equal x 0 else b1.

val unknown : unit -> t

unknown () is unk Bool.t

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

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

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

let_bit s x y is scoped @@ fun v -> (bool x) (bool [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) (bool [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) (bool [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) (bool [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.

val high : exp -> t

high x is msb (bitv x).

val low : exp -> t

low x is lsb (bitv x).

val extract : int -> exp -> t

extract p x is extract (const p) (const p) (bitv x).

val not : exp -> t

not x is inv (bool x).

val logand : exp -> exp -> t

logand x y is and_ (bool x) (bool y)

val logor : exp -> exp -> t

logor x y is or_ (bool x) (bool y)

val logxor : exp -> exp -> t

logxor x y is xor_ (bool x) (bool y)

val is_inf : exp -> t

is_inf x is is_inf (float x)

val is_nan : exp -> t

is_nan x is is_nan (float x)

val is_fzero : exp -> t

is_fzero x is is_fzero (float x)

val is_fpos : exp -> t

is_fpos x is is_fpos (float x)

val is_fneg : exp -> t

is_fneg x is is_fneg (float x)

val fle : exp -> exp -> t

fle x y is p < q \/ p = q,

where p = float x, and q = float y, and p < q if forder p q, and r \/ s is or_ r s, and p = q if (not (p < q) /\ not (q < p)), and r /\ s is and_ r s, and not r is inv r.

val flt : exp -> exp -> t

flt x y is forder (float x) (float y)

val feq : exp -> exp -> t

feq x y is x = y,

where p = q if (not (p < q) /\ not (q < p)), and p < q if forder p q, and r /\ s is and_ r s, and not r is inv r.

package bap-core-theory