Module Offsetmap_sig

module Offsetmap_sig: sig .. end

Signature for Offsetmap module, that implement efficient maps from intervals to arbitrary values.


type v 

Type of the values stored in the offsetmap

type widen_hint 
type alarm = bool 

true indicates that an alarm may have occurred

include Datatype.S

Datatype for the offsetmaps

Pretty-printing

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

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 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

offsetmap containing no interval.

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.

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:

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

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

Same as iter_on_values but with an accumulator

val 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 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 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 f v v = v, maps m such that f 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
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 hold

Narrowing

module Make_Narrow: 
functor (X : sig
include Lattice_type.With_Top
include Lattice_type.With_Narrow
end-> sig .. end

Searching values

val find : validity:Base.validity ->
?conflate_bottom:bool ->
offsets:Ival.t -> size:Integer.t -> t -> bool * v

Find the value bound to a set of intervals, expressed as an ival, in the given rangemap. The returned boolean (alarm) indicates that at least one of the offsets does not comply with 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

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 -> 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.

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 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 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. 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

Same as 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

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.

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.

Misc

val imprecise_write_msg : string Pervasives.ref

The message "more than N <imprecise_msg_write>. Approximating." is displayed when the offsetmap must update too many locations in one operation.

val clear_caches : unit -> unit

Clear the caches local to this module. Beware that they are not project-aware, and that you must call them at every project switch.