Module type `Memory_sig.VALUE`

A scalar value stored inside a memory region. Should be a subset of Sig.MINIMAL + Sig.WITH_BINARY.

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

type binary

Generally different from Scalar.binary!

val binary_pretty : 
  size:Units.In_bits.t ->
  Context.t ->
  Stdlib.Format.formatter ->
  binary ->
  unit

val binary_empty : size:Units.In_bits.t -> Context.t -> binary

val binary_unknown : size:Units.In_bits.t -> Context.t -> binary

val binary_unknown_typed : 
  size:Units.In_bits.t ->
  Context.t ->
  Types.TypedC.typ ->
  binary

Returns an unknown value with a given type.

val check_type : 
  size:Units.In_bits.t ->
  Context.t ->
  Types.TypedC.typ ->
  binary ->
  binary Types.Type_check_tree.t

Type check a binary value

val serialize : 
  widens:bool ->
  size:Units.In_bits.t ->
  Context.t ->
  binary ->
  Context.t ->
  binary ->
  'a Context.in_acc ->
  (binary, 'a) Context.result

Serialize functions also return their de-serializer.

val union : 
  Operator.Condition.t ->
  Context.t ->
  'a Context.in_tuple ->
  'a Context.out_tuple

Here we consider that all values are sets with a given cardinality, and most operations operate on values of cardinality 1, except union and choose which change the cardinality.

Or, we could have a separate value_set type, wich functions empty, singleton, union and choose (this would prevent some errors and avoid the need to store cardinals for singleton values), between value sets and values. This requires to add set operations for most types, but it seems feasible.

But there are many questions then: e.g. should division by zero return a set with one element, or assume that the divisor is non-zero and ignore divisions by zero? Probably the latter is fine, but then we need to throw an exception, like for memory, when an operation does not return any value,etc. Maybe we should differentiate sets with 0 and 1 elements from sets with more than 1 element, etc.

So for now, we do not differenciate values and sets using types.

val addresses_in_binary : 
  size:Units.In_bits.t ->
  Context.t ->
  binary ->
  Context.t ->
  binary ->
  (binary * binary) list

addresses_in_binary ~size ctxa a ctxb b should return a list of addresses corresponding to on both sides in values a and b of size size

module Binary_Forward : sig ... end

Module type Memory_sig.VALUE

Module type `Memory_sig.VALUE`