package bap-core-theory

  1. Overview
  2. Docs

Statements.

type t

an abstract type denoting effects of the Core Theory.

type exp

the type of expressions of the target language.

type rmode

the type for representing rounding modes in the target language.

type stmt

the type of statements in the target language.

val error : t

an ill-formed term.

val set_mem : string -> int -> int -> exp -> t

set_mem s m n x is set v (mem x),

where v = Var.create (mems (bits m) (bits n) s.

val set_reg : string -> int -> exp -> t

set_reg s m x is set v (bitv x),

where v = Var.create (bits m) s.

val set_bit : string -> exp -> t

set_bit s x is set v (bool x),

where v = Var.create Bool.t s.

val set_ieee754 : string -> ieee754 -> exp -> t

set_ieee754 s p x is set v (float x),

where v = Var.create (IEEE754.Sort.define p) s.

val set_rmode : string -> rmode -> t

set_rmode s x is set v (rmode x),

where v = Var.create Rmode.t x.

val tmp_mem : string -> exp -> t

tmp_mem s x is set v (mem x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_reg : string -> exp -> t

tmp_reg s x is set v (bitv x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_bit : string -> exp -> t

tmp_bit s x is set v (bool x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_float : string -> exp -> t

tmp_float s x is set v (float x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_rmode : string -> rmode -> t

tmp_rmode s x is set v (rmode x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

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

let_mem s x p is seq (set v (mem x)) (stmt p),

where v is freshly created variable, and all occurrences of s will be substituted with the identifier of v in the statement p.

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

let_reg s x p is seq (set v (bitv x)) (stmt p),

where v is freshly created variable, and all occurrences of s will be substituted with the identifier of v in the statement p.

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

let_bit s x p is seq (set v (bool x)) (stmt p),

where v is freshly created variable, and all occurrences of s will be substituted with the identifier of v in the statement p.

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

let_float s x p is seq (set v (float x)) (stmt p),

where v is freshly created variable, and all occurrences of s will be substituted with the identifier of v in the statement p.

val let_rmode : string -> rmode -> stmt -> t

let_rmode s x p is seq (set v (rmode x)) (stmt p),

where v is freshly created variable, and all occurrences of s will be substituted with the identifier of v in the statement p.

val jmp : exp -> t

jmp x is jmp (bitv x),

where x is a non-constant expression.

If x is a constant use goto.

val goto : word -> t

goto x is goto lbl,

where lbl = Label.for_addr x.

val call : string -> t

call x is goto lbl,

where lbl = Label.for_name x

val special : string -> t

special s is pass.

val cpuexn : int -> t

cpuexn x is goto lbl,

where lbl = Label.for_ivec x.

val while_ : exp -> stmt list -> t

while_ c ps is repet (bool c) (map stmt ps).

val if_ : exp -> stmt list -> stmt list -> t

if_ c xs ys is branch (bool c) (map stmt xs) (map stmt ys).

val seq : stmt list -> t

seq xs is map stmt xs