Module Memory.Make

Make(Machine) lifts the memory interface into the Machine monad.

Parameters

Signature

val switch : memory -> unit Machine.t

switch memory switches the memory module to memory.

All consecutive operations until the next switch will affect only this memory.

val memory : memory Machine.t

memory a descriptor of currently active memory

get a loads a byte from the address a.

raises the Pagefault machine exception if a is not mapped.

val set : Bap.Std.addr -> value -> unit Machine.t

set a x stores x at the address a.

raises the Pagefault machine exception if a is not mapped, or not writable.

Precondition: the size of the address and the size of the datum match with the current memory sizes.

val set_never_fail : Bap.Std.addr -> value -> unit Machine.t

set_never_fail a x stores x at a bypassing any checks.

Forcefully stores x at the address a without any sanity checks, i.e., doesn't check if the memory is mapped or is it writable.

Precondition: the size of the address and the size of the datum match with the current memory sizes.

  • since 2.6.0
val del : Bap.Std.addr -> unit Machine.t

del p removes the value associated with the pointer p.

load a loads a byte from the given address a.

Same as get a >>= Value.to_word

val store : Bap.Std.addr -> Bap.Std.word -> unit Machine.t

store a x stores the byte x at the address a.

Same as Value.of_word x >>= set a.

Precondition: the size of the address and the size of the datum match with the current memory sizes.

val store_never_fail : Bap.Std.addr -> Bap.Std.word -> unit Machine.t

store_never_fail a x stores x at a bypassing any checks.

Forcefully stores x at the address a without any sanity checks, i.e., doesn't check if the memory is mapped or is it writable.

Same as Value.of_word x >>= set_never_fail a.

Precondition: the size of the address and the size of the datum match with the current memory sizes.

  • since 2.6.0
val add_text : Bap.Std.mem -> unit Machine.t

add_text mem maps a memory chunk mem as executable and readonly segment of machine memory.

val add_data : Bap.Std.mem -> unit Machine.t

add_data maps a memory chunk mem as writable and nonexecutable segment of machine memory.

val add_region : ?readonly:bool -> ?executable:bool -> ?init:(Bap.Std.addr -> Bap.Std.word Machine.t) -> ?generator:Generator.t -> lower:Bap.Std.addr -> upper:Bap.Std.addr -> unit -> unit Machine.t

add_region ~lower ~upper allocates a segment of memory denoted by its lower and upper bounds (included). An unitilialized reads from the segment will produce values generated by a generator (defaults to a Generator.Random.Seeded.lcg ~width (), where width is the data size of the currently selected memory bank ).

If init is provided then the region is initialized, it is the responsibility of init to generates words of correct size (matching the data size of the currently selected memory bank).

An attempt to write to a readonly segment, or an attempt to execute non-executable segment will generate a segmentation fault.

  • since 2.1.0
val allocate : ?readonly:bool -> ?executable:bool -> ?init:(Bap.Std.addr -> Bap.Std.word Machine.t) -> ?generator:Generator.t -> Bap.Std.addr -> int -> unit Machine.t

allocate addr size allocates a segment of the specified size. This function uses add_region underneath the hood, please refer to it for more information.

val map : ?readonly:bool -> ?executable:bool -> Bap.Std.mem -> unit Machine.t

map mem maps a memory chunk mem to a segment with the given permissions. See also add_text and add_data.

val is_mapped : Bap.Std.addr -> bool Machine.t

is_mapped addr a computation that evaluates to true, when the value is mapped, i.e., it is readable.

val is_writable : Bap.Std.addr -> bool Machine.t

is_writable addr is a computation that evaluates to true if addr is writable.