module Base:sig
..end
Abstraction of the base of an addressable memory zone, together with the validity of the zone.
type
cstring =
| |
CSString of |
|||
| |
CSWstring of |
(* | This type abstracts over the two kinds of constant strings present in strings. It is used in a few modules below Base. | *) |
type
variable_validity = private {
|
mutable weak : |
(* | Indicate that the variable is weak, i.e. that it may represent multiple memory locations | *) |
|
mutable min_alloc : |
(* | First bit guaranteed to be valid; can be -1 | *) |
|
mutable max_alloc : |
(* | Last possibly valid bit | *) |
|
max_allocable : |
(* | Maximum valid bit after size increase | *) |
}
Validity for variables that might change size.
type
deallocation =
| |
Malloc |
| |
VLA |
| |
Alloca |
Whether the allocated base has been obtained via calls to
malloc/calloc/realloc (Malloc
), alloca (Alloca
), or is related to a
variable-length array (VLA
).
type
base = private
| |
Var of |
(* | Base for a standard C variable. | *) |
| |
CLogic_Var of |
(* | Base for a logic variable that has a C type. | *) |
| |
Null |
(* | Base for an address like | *) |
| |
String of |
(* | contents of the constant string | *) |
| |
Allocated of |
(* | Base for a variable dynamically allocated via malloc/calloc/realloc/alloca | *) |
type
validity =
| |
Empty |
(* | For 0-sized bases | *) |
| |
Known of |
(* | Valid between those two bits | *) |
| |
Unknown of |
(* | Unknown(b,k,e) indicates:
If k is
| *) |
| |
Variable of |
(* | Variable(min_alloc, max_alloc) means:
| *) |
| |
Invalid |
(* | Valid nowhere. Typically used for the NULL base, or for function pointers. | *) |
module Base:sig
..end
include Datatype.S_with_collections
module Hptshape:Hptmap_sig.Shape
with type key = t and type 'v map = 'v Hptmap.Shape(Base).t
module Hptset:Hptset.S
with type elt = t and type 'v map = 'v Hptshape.map
module SetLattice:Lattice_type.Lattice_Set
with module O = Hptset
module Validity:Datatype.S
with type t = validity
val pretty_addr : Stdlib.Format.formatter -> t -> unit
pretty_addr fmt base
pretty-prints the name of base
on fmt
, with
a leading ampersand if it is a variable
val typeof : t -> Cil_types.typ option
Type of the memory block that starts from the given base. Useful to give to
the function Bit_utils.pretty_bits
, typically.
val pretty_validity : Stdlib.Format.formatter -> validity -> unit
val validity : t -> validity
val validity_from_size : Abstract_interp.Int.t -> validity
validity_from_size size
returns Empty
if size
is zero,
or Known (0, size-1)
if size > 0
.
size
must not be negative.
val validity_from_type : Cil_types.varinfo -> validity
type
range_validity =
| |
Invalid_range |
| |
Valid_range of |
val valid_range : validity -> range_validity
valid_range v
returns Invalid_range
if v
is Invalid
,
Valid_range None
if v
is Empty
, or Valid_range (Some (mn, mx))
otherwise, where mn
and mx
are the minimum and maximum (possibly)
valid bounds of v
.
val is_weak_validity : validity -> bool
is_weak_validity v
returns true iff v
is a Weak
validity.
val create_variable_validity : weak:bool ->
min_alloc:Abstract_interp.Int.t ->
max_alloc:Abstract_interp.Int.t -> variable_validity
val update_variable_validity : variable_validity ->
weak:bool ->
min_alloc:Abstract_interp.Int.t -> max_alloc:Abstract_interp.Int.t -> unit
Update the corresponding fields of the variable validity. Bases already weak cannot be made 'strong' through this function, and the validity bounds can only grow.
val of_varinfo : Cil_types.varinfo -> t
val of_string_exp : Cil_types.exp -> t
val of_c_logic_var : Cil_types.logic_var -> t
Must only be called on logic variables that have a C type
exception Not_a_C_variable
val to_varinfo : t -> Cil_types.varinfo
Not_a_C_variable
otherwise.val is_formal_or_local : t -> Cil_types.fundec -> bool
val is_any_formal_or_local : t -> bool
val is_any_local : t -> bool
val is_global : t -> bool
val is_formal_of_prototype : t -> Cil_types.varinfo -> bool
val is_local : t -> Cil_types.fundec -> bool
val is_formal : t -> Cil_types.fundec -> bool
val is_block_local : t -> Cil_types.block -> bool
val is_function : t -> bool
val null : t
val is_null : t -> bool
val null_set : Hptset.t
Set containing only the base Base.null
.
val min_valid_absolute_address : unit -> Abstract_interp.Int.t
val max_valid_absolute_address : unit -> Abstract_interp.Int.t
Bounds for option absolute-valid-range
val bits_sizeof : t -> Int_Base.t
type
access =
| |
Read of |
| |
Write of |
| |
No_access |
Access kind: read/write of k bits, or no access. Without any access, an offset must point into or just beyond the base ("one past the last element of the array object", non-array object being viewed as array of one element).
val is_valid_offset : access -> t -> Ival.t -> bool
is_valid_offset access b offset
holds iff the ival offset
(expressed in
bits) is completely valid for the access
of base b
(it only represents
valid offsets for such an access). Returns false if offset
may be invalid
for such an access.
val valid_offset : ?bitfield:bool -> access -> t -> Ival.t
Computes all offsets that may be valid for an access
of base t
.
For bases with variable or unknown validity, the result may not satisfy
is_valid_offset
, as some offsets may be valid or invalid.
bitfield
is true by default: the computed offset may be offsets of
bitfields. If it is set to false, the computed offsets are byte aligned
(they are all congruent to 0 modulo 8).
val is_read_only : t -> bool
Is the base valid as a read/write location, or only for reading.
The const
attribute is not currently taken into account.
val is_weak : t -> bool
Is the given base a weak one (in the sens that its validity is Weak
).
Only possible for Allocated
bases.
val id : t -> int
val is_aligned_by : t -> Abstract_interp.Int.t -> bool
This is only useful to create an initial memory state for analysis, and is never needed for normal users.
val register_allocated_var : Cil_types.varinfo -> deallocation -> validity -> t
Allocated variables are variables not present in the source of the
program, but instead created through dynamic allocation. Their field
vsource
is set to false.
val register_memory_var : Cil_types.varinfo -> validity -> t
Memory variables are variables not present in the source of the program.
They are created only to fill the contents of another variable.
Their field vsource
is set to false.
This is used to efficiently replace some bases by others in locations or
in memory states, for instance in Locations
or Lmap_sig
.
typesubstitution =
base Hptshape.map
Type used for the substitution between bases.
val substitution_from_list : (base * base) list -> substitution
Creates a substitution from an association list.