Module Theory.Value

The denotation of expression.

Values are used to express the semantics of terms that evaluate to a value, aka expressions. Values are sorted and value sorts hold static information about the value representation, like the number of bits in a bitvector or the representation format in a floating-point value.

All values belong to the same Knowledge class and thus share the same set of properties, with each property being a specific denotation provided by one or more theories. For example, the bap.std:exp slot holds the denotation of a value in terms of BIL expressions.

type +'a sort

a type for the value sort

type cls

the class of the values.

type 'a t = (cls, 'a sort) KB.cls KB.value

the value type is an instance of Knowledge.value

type 'a value = 'a t
val cls : (cls, unit) KB.cls

the class of all values.

val empty : 'a sort -> 'a t

empty s creates an empty value of sort s.

The empty value doesn't hold any denotations and represents an absence of information about the value.

val sort : 'a t -> 'a sort

sort v is the value sort.

The value sort holds static information about values of that sort.

val resort : ('a sort -> 'b sort option) -> 'a t -> 'b t option

resort refine x applies refine to the sort of x.

Returns the value x with the refined sort, if applicable, otherwise returns the original value.

  • since 2.3.0
val forget : 'a t -> unit t

forget v erases the type index of the value.

The returned value has the monomorphized Top.t type and can be stored in containers, serialized, etc.

To restore the type index use the refine function.

  • since 2.3.0

Note: this is a convenient function that just does Knowledge.Value.refine v @@ Sort.forget @@ sort v

module Top : sig ... end

A value with an erased sort type index.

module Match : sig ... end

A eDSL for dispatching on multiple types.

module Sort : sig ... end

Value Sorts.