Module type `Memory_sig.MEMORY`

Memory map adresses to values. These types may differ (for instance, an array functor can takes integer as adresses, but can contain any value).

include AADT_WITH_BOOLEAN

include AADT

module Scalar : Sig.BASE

include WITH_BOOLEAN_REDEFINITION with module Context = Scalar.Context

include Sig.With_Boolean_Forward

type boolean

include Sig.With_Boolean
  with type boolean := boolean
  with module Context = Scalar.Context

module Context = Scalar.Context

module Boolean : Datatype_sig.S with type t = boolean

val boolean_pretty : Context.t -> Stdlib.Format.formatter -> boolean -> unit

val serialize_boolean : 
  Context.t ->
  boolean ->
  Context.t ->
  boolean ->
  'a Context.in_acc ->
  (boolean, 'a) Context.result

val boolean_empty : Context.t -> boolean

Empty denotes that the concretization has no value (or it is the concrete value representing the absence of value). Note that this does not necessarily imply that some error occured; for instance the offset of an uninitialized pointer can be represented with empty. Emptyness testing is a simple way of communicating between domains.

val boolean_unknown : Context.t -> boolean

module Boolean_Forward : 
  Operator.BOOLEAN_FORWARD
    with module Arity := Sig.Context_Arity_Forward(Context)
     and type boolean := boolean

val query_boolean : Context.t -> boolean -> Lattices.Quadrivalent.t

val assume : Context.t -> boolean -> Context.t option

module Address : ADDRESS with module Scalar = Scalar

module Block : BLOCK with module Scalar = Scalar

type address = Address.binary

type memory

val pretty : Scalar.Context.t -> Stdlib.Format.formatter -> memory -> unit

val load : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  memory ->
  address ->
  Block.Value.binary

val store : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  memory ->
  address ->
  Block.Value.binary ->
  memory

val load_block : Scalar.Context.t -> memory -> address -> Block.block

val store_block : 
  Scalar.Context.t ->
  memory ->
  address ->
  Block.block ->
  memory

val serialize : 
  widens:bool ->
  Scalar.Context.t ->
  memory ->
  Scalar.Context.t ->
  memory ->
  'a Scalar.Context.in_acc ->
  (memory, 'a) Scalar.Context.result

val malloc : 
  id:Operator.Malloc_id.t ->
  malloc_size:Units.In_bytes.t ->
  Scalar.Context.t ->
  memory ->
  address * memory

Allocates a separated block of memory, identified by id. The values initially contained is empty.

val free : Scalar.Context.t -> memory -> address -> memory

Free a memory region.

val unknown : level:int -> Scalar.Context.t -> memory

An initial, unknown region.

val memory_empty : Scalar.Context.t -> memory

An empty region, with no bound address.

val addresses_in_memory : 
  Scalar.Context.t ->
  memory ->
  Scalar.Context.t ->
  memory ->
  (Block.Value.binary * Block.Value.binary) list

include WITH_MEMORY_QUERIES
  with module Context := Scalar.Context
   and type memory := memory
   and type address := address
   and type offset := Block.Offset.offset

val should_focus : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  memory ->
  address ->
  (address * Block.Offset.offset) option

should_focus ~size ctx mem addr asks the domain whether it is useful to "focus" (or "unfold", i.e. try to represent precisely the memory region pointed to by addr, as long as aliasing info ensures that it is sound) a loaded value. size should be the size of addr. If the answer is yes, then the returned value should contain three things about the region to focus: its base, the offset of the end and the offset of addr in it (in bits).

val may_alias : 
  ptr_size:Units.In_bits.t ->
  Scalar.Context.t ->
  size1:Block.Offset.offset ->
  size2:Block.Offset.offset ->
  address ->
  address ->
  bool

may_alias ~ptr_size ~size1 ~size2 ctx addr1 addr2 should return whether the region starting at addr1 of size size1 bytes and the region starting at addr2 of size size2 bytes may have a non-empty intersection. This function is used by focusing abstractions to discard a focused region when writing in a possibly aliased address. ptr_size is the size in bits of both addr1 and addr2.

val is_weak : size:Units.In_bits.t -> Scalar.Context.t -> address -> bool

is_weak ~size ctx addr asks the domain whether the address addr points to a weak type which indicates that the address will not alias with any other

Module type Memory_sig.MEMORY

Module type `Memory_sig.MEMORY`