bap-core-theory 2.0.0 · OCaml Package

Bitvectors.

type t

an abstract type denoting a Core Theory bitvector term.

type exp

the type of expressions of the target language.

type rmode

an abstract type denoting a Core Theory rounding mode term,

val error : t

the error term.

Denotes an ill-typed term. The parsing is immediately stopped.

val unsigned : int -> exp -> t

unsigned m x is unsinged (bits m) (bitv x).

val signed : int -> exp -> t

signed m x is signed (bits m) (bitv x).

val high : int -> exp -> t

high m x is high (bits m) (bitv x).

val low : int -> exp -> t

low m x is low (bits m) (bitv x).

val cast : int -> exp -> exp -> t

cast m x y is cast (bits m) (bool b) (bitv y).

val extract : int -> exp -> exp -> exp -> t

extract m hi lo x is extract (bits m) (bitv hi) (bitv lo) (bitv x).

val add : exp -> exp -> t

add x y is add (bitv x) (bitv y)

val sub : exp -> exp -> t

sub x y is sub (bitv x) (bitv y)

val mul : exp -> exp -> t

mul x y is mul (bitv x) (bitv y)

val div : exp -> exp -> t

div x y is div (bitv x) (bitv y)

val sdiv : exp -> exp -> t

sdiv x y is sdiv (bitv x) (bitv y)

val modulo : exp -> exp -> t

modulo x y is modulo (bitv x) (bitv y)

val smodulo : exp -> exp -> t

smodulo x y is smodulo (bitv x) (bitv y)

val lshift : exp -> exp -> t

lshift x y is lshift (bitv x) (bitv y)

val rshift : exp -> exp -> t

rshift x y is rshift (bitv x) (bitv y)

val arshift : exp -> exp -> t

arshift x y is arshift (bitv x) (bitv y)

val logand : exp -> exp -> t

logand x y is logand (bitv x) (bitv y)

val logor : exp -> exp -> t

logor x y is logor (bitv x) (bitv y)

val logxor : exp -> exp -> t

logxor x y is logxor (bitv x) (bitv y)

val neg : exp -> t

neg x is neg (bitv x)

val not : exp -> t

not x is not (bitv x)

val load_word : int -> exp -> exp -> exp -> t

load_word m d s a is loadw (bits m) (bool d) (mem s) (bitv a).

val load : exp -> exp -> t

load s k is load (mem s) (bitv k)

val var : string -> int -> t

var s m is var (ctxt s) (bits m)

val int : word -> int -> t

int x m is int (bits m) x

val unknown : int -> t

unknown m is unk (bits m)

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

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

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

let_bit s x y is scoped @@ fun v -> (bool x) (bitv [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) (bitv [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) (bitv [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) (bitv [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 append : exp -> exp -> t

append x y is append s (bitv x) (bitv y), where

s is bits (size (sort (bitv x)) + size (sort (bitv x))).

val concat : exp list -> t

concat xs is concat (bits (size s * n)) xs,

where s is the sort of the xs element, and n is the total number of elements in xs.

val cast_int : int -> rmode -> exp -> t

cast_int m r x is cast_int (bits m) (rmode r) (float x).

val cast_sint : int -> rmode -> exp -> t

cast_sint m r x is cast_sint (bits m) (rmode r) (float x).

val fbits : exp -> t

fbits x is fbits (float x).

package bap-core-theory