module Offsetmap_sig:sig
..end
Offsetmap
module, that implement efficient maps from
intervals to arbitrary values.type
v
type
widen_hint
typealarm =
bool
true
indicates that an alarm may have occurredinclude Datatype.S
val pretty_generic : ?typ:Cil_types.typ ->
?pretty_v:(Cil_types.typ option ->
Format.formatter -> v -> unit) ->
?skip_v:(v -> bool) ->
?sep:string -> unit -> Format.formatter -> t -> unit
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
Offsetmap_sig.create
, but for values that are isotropic. In this case,
size_v
is automatically computed.val of_list : ((t -> v -> t) -> t -> 'l -> t) ->
'l -> Abstract_interp.Int.t -> t
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
val size_from_validity : Base.validity -> Integer.t Bottom.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.Invalid
.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, and size
its size; if size
is less than stop-start+1
, v
repeats itself until stop
.offset
is the offset at which v
starts in the interval;
it ranges over 0..size-1
. If offset
is 0
, v
starts
at the beginning of the interval. Otherwise, it starts at offset-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
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
.val iter_on_values : (v -> unit) -> t -> unit
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.val fold_on_values : (v -> 'a -> 'a) -> t -> 'a -> 'a
iter_on_values
but with an accumulatorval map_on_values : (v -> v) -> t -> t
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 |
|||
| |
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 contains v everywhere'. It is always correct to return
Recurse , which will force the recursion until the maps have been fully
decomposed.
Typical usage include functions that verify | *) |
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 buils 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.include Lattice_type.Join_Semi_Lattice
val widen : widen_hint -> t -> t -> t
widen wh m1 m2
performs a widening step on m2
, assuming that
m1
was the previous state. The relation is_included m1 m2
must holdmodule Make_Narrow:
val find : validity:Base.validity ->
?conflate_bottom:bool ->
offsets:Ival.t -> size:Integer.t -> t -> bool * v
validity
.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
.val find_imprecise_everywhere : t -> v
val copy_slice : validity:Base.validity ->
offsets:Ival.t ->
size:Integer.t -> t -> alarm * t Bottom.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.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 Offsetmap_sig.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 -> alarm * t Bottom.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 offsers
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.
The boolean returned indicates a potential alarm.val update_under : validity:Base.validity ->
exact:bool ->
offsets:Ival.t ->
size:Abstract_interp.Int.t ->
v -> t -> alarm * t Bottom.or_bottom
Offsetmap_sig.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 Bottom.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 -> alarm * t Bottom.or_bottom
val cardinal_zero_or_one : t -> bool
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.val single_interval_value : t -> v option
single_interval_value o
returns Some v
if o
contains a single
interval, to which v
is bound, and None
otherwise.val is_same_value : t -> v -> bool
is_same_value o v
is true if the offsetmap o
contains a single
binding to v
, or is the empty offsetmap.val imprecise_write_msg : string Pervasives.ref
val clear_caches : unit -> unit