module Location_Bytes:sig
..end
Association between bases and offsets in byte.
module M:sig
..end
type
t = private
| |
Top of |
(* | Garbled mix of the addresses in the set | *) |
| |
Map of |
(* | Precise set of addresses+offsets | *) |
typesize_widen_hint =
Ival.size_widen_hint
typegeneric_widen_hint =
Base.t -> Ival.generic_widen_hint
typewiden_hint =
size_widen_hint *
generic_widen_hint
include Lattice_type.AI_Lattice_with_cardinal_one
Those locations have a lattice structure, including standard operations
such as join
, narrow
, etc.
include Datatype.S_with_collections
val singleton_zero : t
the set containing only the value for to the C expression 0
val singleton_one : t
the set containing only the value 1
val zero_or_one : t
val is_zero : t -> bool
val is_bottom : t -> bool
val top_int : t
val top_float : t
val top_single_precision_float : t
val inject : Base.t -> Ival.t -> t
val inject_ival : Ival.t -> t
val inject_float : Fval.F.t -> t
val add : Base.t -> Ival.t -> t -> t
add b i loc
binds b
to i
in loc
when i
is not Ival.bottom
,
and returns bottom
otherwise.
val diff : t ->
t -> t
Over-approximation of difference. arg2
needs to be exact or an
under_approximation.
val diff_if_one : t ->
t -> t
Over-approximation of difference. arg2
can be an
over-approximation.
val shift : Ival.t -> t -> t
val shift_under : Ival.t -> t -> t
Over- and under-approximation of shifting the value by the given Ival.
val sub_pointwise : ?factor:Int_Base.t ->
t -> t -> Ival.t
Subtracts the offsets of two locations loc1
and loc2
.
Returns the pointwise subtraction of their offsets
off1 - factor * off2
. factor
defaults to 1
.
val topify_arith_origin : t -> t
Topifying of values, in case of imprecise accesses
val topify_misaligned_read_origin : t -> t
val topify_merge_origin : t -> t
val topify_leaf_origin : t -> t
val topify_with_origin : Origin.t -> t -> t
val topify_with_origin_kind : Origin.kind -> t -> t
val inject_top_origin : Origin.t -> Base.Hptset.t -> t
inject_top_origin origin p
creates a top with origin origin
and additional information param
val top_with_origin : Origin.t -> t
Completely imprecise value. Use only as last resort.
val fold_bases : (Base.t -> 'a -> 'a) -> t -> 'a -> 'a
Fold on all the bases of the location, including Top bases
.
Error_Top
in the case Top Top
.val fold_i : (Base.t -> Ival.t -> 'a -> 'a) -> t -> 'a -> 'a
Fold with offsets.
Error_Top
in the cases Top Top
, Top bases
.val fold_topset_ok : (Base.t -> Ival.t -> 'a -> 'a) -> t -> 'a -> 'a
Fold with offsets, including in the case Top bases
. In this case,
Ival.top
is supplied to the iterator.
Error_Top
in the case Top Top
.val fold_enum : (t -> 'a -> 'a) ->
t -> 'a -> 'a
fold_enum f loc acc
enumerates the locations in acc
, and passes
them to f
. Make sure to call Locations.Location_Bytes.cardinal_less_than
before calling
this function, as all possible combinations of bases/offsets are
presented to f
. Raises Error_Top
if loc
is Top _
or if
one offset cannot be enumerated.
val cached_fold : cache_name:string ->
temporary:bool ->
f:(Base.t -> Ival.t -> 'a) ->
projection:(Base.t -> Ival.t) ->
joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
Cached version of fold_i
, for advanced users
val for_all : (Base.t -> Ival.t -> bool) -> t -> bool
val exists : (Base.t -> Ival.t -> bool) -> t -> bool
val filter_base : (Base.t -> bool) -> t -> t
val cardinal_zero_or_one : t -> bool
val cardinal_less_than : t -> int -> int
cardinal_less_than v card
returns the cardinal of v
if it is less
than card
, or raises Not_less_than
.
val cardinal : t -> Integer.t option
None if the cardinal is unbounded
val find_lonely_key : t -> Base.t * Ival.t
if there is only one base b
in the location, then returns the
pair b,o
where o
are the offsets associated to b
.
Not_found
otherwise.val find_lonely_binding : t -> Base.t * Ival.t
if there is only one binding b -> o
in the location (that is, only
one base b
with cardinal_zero_or_one o
), returns the pair b,o
.
Not_found
otherwiseval find : Base.t -> t -> Ival.t
val find_or_bottom : Base.t -> M.t -> Ival.t
val split : Base.t -> t -> Ival.t * t
val get_bases : t -> Base.SetLattice.t
Returns the bases the location may point to. Never fails, but
may return Base.SetLattice.Top
.
val contains_addresses_of_locals : (M.key -> bool) ->
t -> bool
contains_addresses_of_locals is_local loc
returns true
if loc
contains the address of a variable for which
is_local
returns true
val remove_escaping_locals : (M.key -> bool) ->
t -> bool * t
remove_escaping_locals is_local v
removes from v
the information
associated with bases for which is_local
returns true
. The
returned boolean indicates that v
contained some locals.
val contains_addresses_of_any_locals : t -> bool
contains_addresses_of_any_locals loc
returns true
iff loc
contains
the address of a local variable or of a formal variable.
val iter_on_strings : skip:Base.t option ->
(Base.t -> string -> int -> int -> unit) ->
t -> unit
val partially_overlaps : size:Abstract_interp.Int.t ->
t -> t -> bool
Is there a possibly-non empty intersection between the two supplied
locations, assuming they have size size
val is_relationable : t -> bool
is_relationable loc
returns true
iff loc
represents a single
memory location.
val may_reach : Base.t -> t -> bool
may_reach base loc
is true if base
might be accessed from loc
.
val get_garbled_mix : unit -> t list
All the garbled mix that have been created so far, sorted by "temporal" order of emission.
val clear_garbled_mix : unit -> unit
Clear the information on created garbled mix.
val do_track_garbled_mix : bool -> unit