Frama-C API - V_Offsetmap
Memory slices. They are maps from intervals to values with flags. All sizes and intervals are in bits.
include Offsetmap_sig.S with type v = V_Or_Uninitialized.t and type widen_hint = V_Or_Uninitialized.widen_hint
type v = V_Or_Uninitialized.t
Type of the values stored in the offsetmap
type widen_hint = V_Or_Uninitialized.widen_hint
Datatype for the offsetmaps
include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
Pretty-printing
val pretty_generic : ?typ:Cil_types.typ -> ?pretty_v:(Cil_types.typ option -> Stdlib.Format.formatter -> v -> unit) -> ?skip_v:(v -> bool) -> ?sep:string -> unit -> Stdlib.Format.formatter -> t -> unit
Creating basic offsetmaps
val create : size:Abstract_interp.Int.t -> v -> size_v:Abstract_interp.Int.t -> t
create ~size v ~size_v
creates an offsetmap of size size
in which the intervals k*size_v .. (k+1)*size_v-1
with 0<= k <= size/size_v
are all mapped to v
.
val create_isotropic : size:Abstract_interp.Int.t -> v -> t
Same as create
, but for values that are isotropic. In this case, size_v
is automatically computed.
from_list fold c size
creates an offsetmap by applying the iterator fold
to the container c
, the elements of c
being supposed to be of size size
. c
must be such that fold
is called at least once.
val empty : t
offsetmap containing no interval.
val size_from_validity : Base.validity -> Integer.t Lattice_bounds.or_bottom
size_from_validity v
returns the size to be used when creating a new offsetmap for a base with validity v
. This is a convention that must be shared by all modules that create offsetmaps, because operations such as join
or is_included
require offsetmaps of the same . Returns `Bottom
iff v
is Base.validity.Invalid
.
Iterators
val iter : ((Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> unit) -> t -> unit
iter f m
calls f
on all the intervals bound in m
, in increasing order. The arguments of f (min, max) (v, size, offset)
are as follows:
(start, stop)
are the bounds of the interval, inclusive.v
is the value bound to the interval, andsize
its size; ifsize
is less thanstop-start+1
,v
repeats itself untilstop
.offset
is the offset at whichv
starts in the interval; it ranges over0..size-1
. Ifoffset
is0
,v
starts at the beginning of the interval. Otherwise, it starts atoffset-size
.
val fold : ((Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> 'a -> 'a) -> t -> 'a -> 'a
Same as iter
, but with an accumulator.
val fold_between : ?direction:[ `LTR | `RTL ] -> entire:bool -> (Abstract_interp.Int.t * Abstract_interp.Int.t) -> ((Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> 'a -> 'a) -> t -> 'a -> 'a
fold_between ~direction:`LTR ~entire (start, stop) m acc
is similar to fold f m acc
, except that only the intervals that intersect start..stop
(inclusive) are presented. If entire
is true, intersecting intervals are presented whole (ie. they may be bigger than start..stop
). If entire
is false
, only the intersection with ib..ie
is presented. fold_between ~direction:`RTL
reverses the iteration order: interval are passed in decreasing order. Default is `LTR
.
Interval-unaware iterators
iter_on_values f m
iterates on the entire contents of m
, but f
receives only the value bound to each interval. Interval bounds, the alignment of the value and its size are not computed.
map_on_values f m
creates the map derived from m
by applying f
to each interval. For each interval, the size of the new value and its offset relative to the beginning of the interval is kept unchanged.
type map2_decide =
| ReturnLeft
| ReturnRight
| ReturnConstant of v
| Recurse
(*This type describes different possibilities to accelerate a simultaneous iteration on two offsetmaps.
ReturnLeft
(resp.ReturnRight
) means 'return the left (resp. right) operand unchanged, and stop the recursive descent'.ReturnConstant v
means 'return a constant offsetmap of the good size and that containsv
everywhere'. It is always correct to returnRecurse
, which will force the recursion until the maps have been fully decomposed.Typical usage include functions that verify
*)f v v = v
, mapsm
such thatf m m' = m'
, etc.
val map2_on_values : Hptmap_sig.cache_type -> (t -> t -> map2_decide) -> (v -> v -> v) -> t -> t -> t
map2_on_values cache decide join m1 m2
applies join
pointwise to all the elements of m1
and m2
and builds the resulting map. This function can only be called if m1
and m2
contain isotropic values. decide
is called during the iteration, and can be used to return early; it is always correct to return Recurse
. Depending on cache
, the results of the partially applied function map2_on_values cache decide join
will be cached between different calls.
Join and inclusion testing
include Lattice_type.Join_Semi_Lattice with type t := t
datatype of element of the lattice
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
val hash : t -> int
Hash function: same spec than Hashtbl.hash
.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
mem_project f x
must return true
iff there is a value p
of type Project.t
in x
such that f p
returns true
.
val widen : ?hint:widen_hint -> t -> t -> t
widen m1 m2
performs a widening step on m2
, assuming that m1
was the previous state. The relation is_included m1 m2
must hold
Narrowing
module Make_Narrow (_ : sig ... end) : sig ... end
Searching values
val find : validity:Base.validity -> ?conflate_bottom:bool -> offsets:Ival.t -> size:Integer.t -> t -> v
Find the value bound to a set of intervals, expressed as an ival, in the given rangemap.
val find_imprecise : validity:Base.validity -> t -> v
find_imprecise ~validity m
returns an imprecise join of the values bound in m
, in the range described by validity
.
Returns an imprecise join of all the values bound in the offsetmap.
val copy_slice : validity:Base.validity -> offsets:Ival.t -> size:Integer.t -> t -> t Lattice_bounds.or_bottom
copy_slice ~validity ~offsets ~size m
copies and merges the slices of m
starting at offsets offsets
and of size size
. Offsets invalid according to validity
are removed. size
must be strictly greater than zero.
Adding values
val add : ?exact:bool -> (Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> t -> t
add (min, max) (v, size, offset) m
maps the interval min..max
(inclusive) to the value v
in m
. v
is assumed as having size size
. If stop-start+1
is greater than size
, v
repeats itself until the entire interval is filled. offset
is the offset at which v
starts in the interval, interpreted as for iter
. Offsetmaps cannot contain holes, so m
must already bind at least the intervals 0..start-1
.
val update : ?origin:Origin.t -> validity:Base.validity -> exact:bool -> offsets:Ival.t -> size:Abstract_interp.Int.t -> v -> t -> t Lattice_bounds.or_bottom
update ?origin ~validity ~exact ~offsets ~size v m
writes v
, of size size
, each offsets
in m
; m
must be of the size implied by validity
. ~exact=true
results in a strong update, while ~exact=false
performs a weak update. If offsets
contains too many offsets, or if offsets
and size
are not compatible, offsets
and/or v
are over-approximated. In this case, origin
is used as the source of the resulting imprecision. Returns `Bottom
when all offsets are invalid.
val update_under : validity:Base.validity -> exact:bool -> offsets:Ival.t -> size:Abstract_interp.Int.t -> v -> t -> t Lattice_bounds.or_bottom
Same as update
, except that no over-approximation on the set of offsets or on the value written occurs. In case of imprecision, m
is not updated.
val update_imprecise_everywhere : validity:Base.validity -> Origin.t -> v -> t -> t Lattice_bounds.or_bottom
update_everywhere ~validity o v m
computes the offsetmap resulting from imprecisely writing v
potentially anywhere where m
is valid according to validity
. If a value becomes too imprecise, o
is used as origin.
val paste_slice : validity:Base.validity -> exact:bool -> from:t -> size:Abstract_interp.Int.t -> offsets:Ival.t -> t -> t Lattice_bounds.or_bottom
Shape
val cardinal_zero_or_one : t -> bool
Returns true
if and only if all the interval bound in the offsetmap are mapped to values with cardinal at most 1.
val is_single_interval : t -> bool
is_single_interval o
is true if the offsetmap o
contains a single binding.
single_interval_value o
returns Some v
if o
contains a single interval, to which v
is bound, and None
otherwise.
is_same_value o v
is true if the offsetmap o
contains a single binding to v
, or is the empty offsetmap.
Misc
val narrow : t -> t -> t Lattice_bounds.or_bottom
val narrow_reinterpret : t -> t -> t Lattice_bounds.or_bottom
See the corresponding functions in Offsetmap_sig
.