diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 4ee29fa9fdc7440f4ed9f783221d95111a001677..1c819cd5e87f17624361fca3bdcccaba756013e9 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -251,32 +251,83 @@ let is_weak = function
| Allocated (_, _, Variable { weak }) -> weak
| _ -> false
-let offset_is_in_validity size validity ival =
- Ival.is_bottom ival ||
- (* Special case. We stretch the truth and say that the address of the
- base itself is valid for a size of 0. A size of 0 appears for:
- - empty structs
- - memory operations on a 0 size (e.g. memcpy (_, _ 0))
- - internally, to emulate the semantics of "past-one" pointers (in
- Cvalue_forward.are_comparable). *)
- Int.(equal zero size) && Ival.(equal ival zero) ||
+(* Does a C type end by an empty struct? *)
+let rec final_empty_struct = function
+ | TArray (typ, _, _, _) -> final_empty_struct typ
+ | TComp (compinfo, _, _) ->
+ begin
+ match compinfo.cfields with
+ | [] -> true
+ | l ->
+ let last_field = List.(hd (rev l)) in
+ try Cil.bitsSizeOf last_field.ftype = 0
+ with Cil.SizeOfError _ -> false
+ end
+ | TNamed (typeinfo, _) -> final_empty_struct typeinfo.ttype
+ | TVoid _ | TInt _ | TFloat _ | TPtr _ | TEnum _
+ | TFun _ | TBuiltin_va_list _ -> false
+
+(* Does a base end by an empty struct? *)
+let final_empty_struct = function
+ | Var (vi, _) | Allocated (vi, _, _) -> final_empty_struct vi.vtype
+ | _ -> false
+
+type access = Read of Integer.t | Write of Integer.t | No_access
+let for_writing = function Write _ -> true | Read _ | No_access -> false
+
+let is_empty = function
+ | Read size | Write size -> Int.(equal zero size)
+ | No_access -> true
+
+(* Computes the last valid offset for an access of the base [base] with [max]
+ valid bits: [max - size + 1] for an access of size [size]. *)
+let last_valid_offset base max = function
+ | Read size | Write size ->
+ if Int.is_zero size
+ (* For an access of size 0, [max] is the last valid offset, unless the base
+ ends by an empty struct, in which case [max+1] is also a valid offset. *)
+ then if final_empty_struct base then Int.succ max else max
+ else Int.sub max (Int.pred size)
+ | No_access -> Int.succ max (* A pointer can point just beyond its object. *)
+
+let offset_for_validity ~bitfield access base =
+ match validity base with
+ | Empty -> if is_empty access then Ival.zero else Ival.bottom
+ | Invalid -> if access = No_access then Ival.zero else Ival.bottom
+ | Known (min, max) | Unknown (min, _, max) ->
+ let max = last_valid_offset base max access in
+ if bitfield
+ then Ival.inject_range (Some min) (Some max)
+ else Ival.inject_interval (Some min) (Some max) Int.zero Int.eight
+ | Variable variable_v ->
+ let maxv = last_valid_offset base variable_v.max_alloc access in
+ Ival.inject_range (Some Int.zero) (Some maxv)
+
+let valid_offset ?(bitfield=true) access base =
+ if for_writing access && is_read_only base
+ then Ival.bottom
+ else offset_for_validity ~bitfield access base
+
+let offset_is_in_validity access base ival =
let is_valid_for_bounds min_bound max_bound =
match Ival.min_and_max ival with
| Some min, Some max ->
- Int.ge min min_bound && Int.le (Int.add max (Int.pred size)) max_bound
+ Int.ge min min_bound &&
+ Int.le max (last_valid_offset base max_bound access)
| _, _ -> false
in
- match validity with
- | Empty | Invalid -> false
+ match validity base with
+ | Empty -> is_empty access && Ival.(equal zero ival)
+ | Invalid -> access = No_access && Ival.(equal zero ival)
| Known (min, max)
| Unknown (min, Some max, _) -> is_valid_for_bounds min max
- | Unknown (_, None, _) -> false (* all accesses are possibly invalid *)
+ | Unknown (_, None, _) -> false (* All accesses are possibly invalid. *)
| Variable v -> is_valid_for_bounds Int.zero v.min_alloc
-let is_valid_offset ~for_writing size base offset =
- Ival.is_bottom offset ||
- not (for_writing && (is_read_only base)) &&
- offset_is_in_validity size (validity base) offset
+let is_valid_offset access base offset =
+ Ival.is_bottom offset
+ || not (for_writing access && (is_read_only base))
+ && offset_is_in_validity access base offset
let is_function base =
match base with
diff --git a/src/kernel_services/abstract_interp/base.mli b/src/kernel_services/abstract_interp/base.mli
index 0c4cefd19495e11fb35129e8649ca2b1e9bd3346..22ccad956fda3ce7c9d234d4df4d54baf93216be 100644
--- a/src/kernel_services/abstract_interp/base.mli
+++ b/src/kernel_services/abstract_interp/base.mli
@@ -177,14 +177,25 @@ val max_valid_absolute_address: unit -> Int.t
val bits_sizeof : t -> Int_Base.t
-val offset_is_in_validity : Int.t -> validity -> Ival.t -> bool
-(** [is_offset_in_validity size validity ival] checks that [ival] is a valid
- offset for an access of size [size] according to [validity]. *)
-
-val is_valid_offset : for_writing:bool -> Int.t -> t -> Ival.t -> bool
-(** [is_valid_offset ~for_writing size b offset] checks that [offset]
- (expressed in bits) plus [size] bits is valid in [b]. *)
-
+(** 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). *)
+type access = Read of Int.t | Write of Int.t | No_access
+
+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). *)
(** {2 Misc} *)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 28caf337006fcec6b57e30107c4995b82d084cc5..825aa7b0b7446d42855c91482a4f1c7d1458fef4 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -183,10 +183,7 @@ struct
Offsetmap.update_imprecise_everywhere ~validity orig v offm
| Int_Base.Value size ->
assert (Int.ge size Int.zero);
- let _, r =
- Offsetmap.update ?origin ~validity ~exact ~offsets ~size v offm
- in
- r
+ Offsetmap.update ?origin ~validity ~exact ~offsets ~size v offm
in
match offm' with
| `Bottom -> ()
@@ -230,7 +227,7 @@ struct
match find_or_default base mem with
| `Bottom -> acc_v
| `Value offsetmap ->
- let _alarm_o, new_v =
+ let new_v =
Offsetmap.find
~conflate_bottom ~validity ~offsets ~size offsetmap
in
@@ -475,7 +472,7 @@ struct
match offsetmap_dst with
| `Bottom -> acc
| `Value offsetmap_dst ->
- let _this_alarm, new_offsetmap =
+ let new_offsetmap =
Offsetmap.paste_slice ~validity ~exact
~from ~size ~offsets:i_dst offsetmap_dst
in
@@ -512,9 +509,8 @@ struct
match find_or_default k_src m with
| `Bottom -> acc
| `Value offsetmap_src ->
- let _alarm_copy, copy =
- Offsetmap.copy_slice ~validity
- ~offsets:i_src ~size offsetmap_src
+ let copy =
+ Offsetmap.copy_slice ~validity~offsets:i_src ~size offsetmap_src
in
Bottom.join Offsetmap.join acc copy
in
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index f508068d2dbd6d7c4ccf4594625a23e2f5ea903d..70ca0060d5d777a9a3e5afc27d693aa004b0b1b2 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -522,40 +522,21 @@ type location =
{ loc : Location_Bits.t;
size : Int_Base.t }
-exception Found_two
+type access = Read | Write | No_access
+
+let project_size = function
+ | Int_Base.Value size -> size
+ | Int_Base.Top -> Int.zero
-(* Reduce [offsets] so that reading [size] from [offsets] fits within
- the validity of [base]. If [aligned] is set to true, make the offset
- congruent to 0 modulo 8.
- Maintain synchronized with Precise_locs.reduce_offset_by_validity. *)
-let reduce_offset_by_validity ~for_writing ?(bitfield=true) base offsets size =
- if for_writing && Base.is_read_only base then
- Ival.bottom
- else
- match Base.validity base, size with
- | Base.Empty, _ ->
- if Int_Base.(compare size zero) > 0 then Ival.bottom else Ival.zero
- | Base.Invalid, _ -> Ival.bottom
- | _, Int_Base.Top -> offsets
- | (Base.Known (minv,maxv) | Base.Unknown (minv,_,maxv)),
- Int_Base.Value size ->
- (* The maximum offset is maxv - (size - 1), except if size = 0,
- in which case the maximum offset is exactly maxv. *)
- let pred_size = Int.max Int.zero (Int.pred size) in
- let maxv = Int.sub maxv pred_size in
- let range =
- if bitfield
- then Ival.inject_range (Some minv) (Some maxv)
- else Ival.inject_interval (Some minv) (Some maxv) Int.zero Int.eight
- in
- Ival.narrow range offsets
- | Base.Variable variable_v, Int_Base.Value size ->
- let pred_size = Int.max Int.zero (Int.pred size) in
- let maxv = Int.sub variable_v.Base.max_alloc pred_size in
- let range =
- Ival.inject_range (Some Int.zero) (Some maxv)
- in
- Ival.narrow range offsets
+(* Conversion into Base.access. A location valid for an access of unknown size
+ must be at least valid for an empty access, so accesses of unknown sizes are
+ converted into empty accesses. *)
+let base_access ~size = function
+ | No_access -> Base.No_access
+ | Read -> Base.Read (project_size size)
+ | Write -> Base.Write (project_size size)
+
+exception Found_two
let valid_cardinal_zero_or_one ~for_writing {loc=loc;size=size} =
Location_Bits.equal Location_Bits.bottom loc ||
@@ -566,16 +547,18 @@ let valid_cardinal_zero_or_one ~for_writing {loc=loc;size=size} =
already := true
in
try
- match loc with
- | Location_Bits.Top _ -> false
- | Location_Bits.Map m ->
- if Int_Base.is_top size then false
- else begin
+ match loc, size with
+ | Location_Bits.Top _, _ -> false
+ | _, Int_Base.Top -> false
+ | Location_Bits.Map m, Int_Base.Value size ->
Location_Bits.M.iter
(fun base offsets ->
if Base.is_weak base then raise Found_two;
+ let access =
+ if for_writing then Base.Write size else Base.Read size
+ in
let valid_offsets =
- reduce_offset_by_validity ~for_writing base offsets size
+ Ival.narrow offsets (Base.valid_offset access base)
in
if Ival.cardinal_zero_or_one valid_offsets
then begin
@@ -585,7 +568,6 @@ let valid_cardinal_zero_or_one ~for_writing {loc=loc;size=size} =
else raise Found_two
) m;
true
- end
with
| Abstract_interp.Error_Top | Found_two -> false
@@ -605,14 +587,13 @@ let loc_size { size = size } = size
let make_loc loc_bits size = { loc = loc_bits; size = size }
-let is_valid ~for_writing {loc; size} =
- match size with
- | Int_Base.Top -> false
- | Int_Base.Value size ->
- let is_valid_offset b o = Base.is_valid_offset ~for_writing size b o in
- match loc with
- | Location_Bits.Top _ -> false
- | Location_Bits.Map m -> Location_Bits.M.for_all is_valid_offset m
+let is_valid access {loc; size} =
+ not (Int_Base.is_top size) &&
+ let access = base_access ~size access in
+ let is_valid_offset = Base.is_valid_offset access in
+ match loc with
+ | Location_Bits.Top _ -> false
+ | Location_Bits.Map m -> Location_Bits.M.for_all is_valid_offset m
let filter_base f loc =
@@ -696,9 +677,10 @@ let pretty_english ~prefix fmt { loc = m ; size = size } =
print_binding fmt off
(* Case [Top (Top, _)] must be handled by caller. *)
-let enumerate_valid_bits_under_over under_over ~for_writing {loc; size} =
+let enumerate_valid_bits_under_over under_over access {loc; size} =
+ let access = base_access ~size access in
let compute_offset base offs acc =
- let valid_offset = reduce_offset_by_validity ~for_writing base offs size in
+ let valid_offset = Ival.narrow offs (Base.valid_offset access base) in
if Ival.is_bottom valid_offset then
acc
else
@@ -716,36 +698,37 @@ let interval_from_ival_under base offset size =
| Base.Variable { Base.weak = true } -> Int_Intervals.bottom
| _ -> Int_Intervals.from_ival_size_under offset size
-let enumerate_valid_bits ~for_writing loc =
+let enumerate_valid_bits access loc =
match loc.loc with
| Location_Bits.Top (Base.SetLattice.Top, _) -> Zone.top
| _ ->
- enumerate_valid_bits_under_over interval_from_ival_over ~for_writing loc
+ enumerate_valid_bits_under_over interval_from_ival_over access loc
;;
-let enumerate_valid_bits_under ~for_writing loc =
+let enumerate_valid_bits_under access loc =
match loc.size with
| Int_Base.Top -> Zone.bottom
| Int_Base.Value _ ->
match loc.loc with
| Location_Bits.Top _ -> Zone.bottom
| Location_Bits.Map _ ->
- enumerate_valid_bits_under_over interval_from_ival_under ~for_writing loc
+ enumerate_valid_bits_under_over interval_from_ival_under access loc
;;
(** [valid_part l] is an over-approximation of the valid part
of the location [l]. *)
-let valid_part ~for_writing ?(bitfield=true) {loc = loc; size = size } =
+let valid_part access ?(bitfield=true) {loc = loc; size = size } =
+ let access = base_access ~size access in
let compute_loc base offs acc =
let valid_offset =
- reduce_offset_by_validity ~for_writing ~bitfield base offs size
+ Ival.narrow offs (Base.valid_offset access ~bitfield base)
in
if Ival.is_bottom valid_offset then
acc
else
Location_Bits.M.add base valid_offset acc
in
- let locbits =
+ let locbits =
match loc with
| Location_Bits.Top (Base.SetLattice.Top, _) -> loc
| Location_Bits.Top (Base.SetLattice.Set _, _) ->
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index f1facdc393237c64a1b8892bf852f36ff05f83d0..654cd6dbc403b113fa9cacd7d0403f2b4809798b 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -326,12 +326,18 @@ val make_loc : Location_Bits.t -> Int_Base.t -> location
val loc_equal : location -> location -> bool
val loc_size : location -> Int_Base.t
-val is_valid : for_writing:bool -> location -> bool
-(** Is the given location entirely valid, as the destination of a write
- operation if [for_writing] is true, as the destination of a read
- otherwise. *)
+(** Kind of memory access. *)
+type access = Read | Write | No_access
-val valid_part : for_writing:bool -> ?bitfield:bool -> location -> location
+(** Conversion into a base access, with the size information.
+ Accesses of unknown sizes are converted into empty accesses. *)
+val base_access: size:Int_Base.t -> access -> Base.access
+
+val is_valid : access -> location -> bool
+(** Is the given location entirely valid, without any access or as a destination
+ for a read or write access. *)
+
+val valid_part : access -> ?bitfield:bool -> location -> location
(** Overapproximation of the valid part of the given location. Beware that
[is_valid (valid_part loc)] does not necessarily hold, as garbled mix
may not be reduced by [valid_part].
@@ -375,10 +381,10 @@ val loc_bits_to_loc_bytes_under : Location_Bits.t -> Location_Bytes.t
val enumerate_bits : location -> Zone.t
val enumerate_bits_under : location -> Zone.t
-val enumerate_valid_bits : for_writing:bool -> location -> Zone.t
+val enumerate_valid_bits : access -> location -> Zone.t
(** @plugin development guide *)
-val enumerate_valid_bits_under : for_writing:bool -> location -> Zone.t
+val enumerate_valid_bits_under : access -> location -> Zone.t
val zone_of_varinfo : varinfo -> Zone.t
(** @since Carbon-20101201 *)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 507f88fe4c81019cefb345cea00c9fa6405093b9..bd89eb563c1519850e970cafdb39ef3b69fcbd07 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -109,7 +109,6 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
type v = V.t
type widen_hint = V.generic_widen_hint
- type alarm = bool
let empty = Empty
(** All high-level functions of this module must handle a size of 0, in which
@@ -1531,7 +1530,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
(* Finds the value associated to some offsets represented as an ival. *)
let find ~validity ?(conflate_bottom=true) ~offsets ~size tree =
- let alarm, offsets = Tr_offset.trim_by_validity offsets size validity in
+ let offsets = Tr_offset.trim_by_validity offsets size validity in
let topify = Origin.K_Misalign_read in
let read_one_node ~offset node ~start ~size acc =
extract_bits_and_stitch ~topify ~conflate_bottom
@@ -1543,8 +1542,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let read_nodes = read_successive_nodes ~read_one_node neutral in
let read_value v _size = v in
let join = V.join in
- let v = read ~offsets ~size tree ~read_value ~read_nodes ~join V.bottom in
- alarm, v
+ read ~offsets ~size tree ~read_value ~read_nodes ~join V.bottom
(* Copies the node [node] at the end of the offsetmap [acc], as part of the
larger copy of the interval [start..start+size-1] from the englobing
@@ -1575,10 +1573,10 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
t
let copy_slice ~validity ~offsets ~size tree =
- let alarm, offsets = Tr_offset.trim_by_validity offsets size validity in
- if Int.(equal size zero) then alarm, `Value Empty
+ let offsets = Tr_offset.trim_by_validity offsets size validity in
+ if Int.(equal size zero) then `Value Empty
else match offsets with
- | Tr_offset.Invalid -> alarm, `Bottom
+ | Tr_offset.Invalid -> `Bottom
| _ ->
let read_one_node = copy_one_node in
let neutral = m_empty in
@@ -1586,7 +1584,7 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let read_value v size = interval_aux (pred size) Rel.zero size v in
let init = isotropic_interval size V.bottom in
let t = read ~offsets ~size tree ~read_value ~read_nodes ~join init in
- alarm, `Value t
+ `Value t
(* Keep the part of the tree strictly under (i.e. strictly on the left) of a
given offset. *)
@@ -1907,37 +1905,34 @@ let update_aux_tr_offsets ~exact ~offsets ~size v curr_off t =
the memory zones written. *)
let update_aux ?origin ~validity ~exact ~offsets ~size v curr_off t =
let v = V.anisotropic_cast ~size v in
- let alarm, reduced =
- Tr_offset.trim_by_validity ?origin offsets size validity
- in
+ let reduced = Tr_offset.trim_by_validity ?origin offsets size validity in
let exact = exact && not (Base.is_weak_validity validity) in
- let r = update_aux_tr_offsets ~exact ~offsets:reduced ~size v curr_off t in
- alarm, r
+ update_aux_tr_offsets ~exact ~offsets:reduced ~size v curr_off t
(* Same as update_aux, but on zero-rooted offsetmaps. *)
let update ?origin ~validity ~exact ~offsets ~size v t =
try
- let alarm, (_curr_off, r) =
+ let _curr_off, r =
update_aux ?origin ~validity ~exact ~offsets ~size v Int.zero t
in
- alarm, `Value r
- with Update_Result_is_bottom -> true, `Bottom
+ `Value r
+ with Update_Result_is_bottom -> `Bottom
(* High-level update function (roughly of type [Ival.t -> v -> offsetmap ->
offsetmap]) that *under*-approximate the set of written locations, when
there are too many of them. *)
let update_under ~validity ~exact ~offsets ~size v t =
let v = V.anisotropic_cast ~size v in
- let alarm, offsets = Tr_offset.trim_by_validity offsets size validity in
+ let offsets = Tr_offset.trim_by_validity offsets size validity in
if Base.is_weak_validity validity ||
update_aux_tr_offsets_approximates offsets size
then
- alarm, `Value t
+ `Value t
else
try
let _, t = update_aux_tr_offsets ~exact ~offsets ~size v Int.zero t in
- alarm, `Value t
- with Update_Result_is_bottom -> true, `Bottom
+ `Value t
+ with Update_Result_is_bottom -> `Bottom
let is_single_interval o =
match o with
@@ -2016,33 +2011,26 @@ let update_under ~validity ~exact ~offsets ~size v t =
let stop_src = Int.pred size in
ignore (Ival.cardinal_less_than offsets plevel);
(* See explanations at the end of [Tr_offset] for what is computed here.*)
- let min_valid, max_sure_valid, max_maybe_valid = match validity with
- | Base.Invalid | Base.Empty (* size > 0 *) ->
- Int.zero, Int.minus_one, Int.minus_one
- | Base.Known (b,e) ->
- b, e, e
- | Base.Unknown (b, k, e) ->
- let max_sure = Extlib.opt_conv Int.minus_one k in
- b, max_sure, e
- | Base.Variable { Base.min_alloc; Base.max_alloc } ->
- Int.zero, min_alloc, max_alloc
+ let min_valid, max_maybe_valid = match validity with
+ | Base.Invalid | Base.Empty (* size > 0 *) -> Int.zero, Int.minus_one
+ | Base.Known (b, e) | Base.Unknown (b, _, e) -> b, e
+ | Base.Variable { Base.max_alloc } -> Int.zero, max_alloc
in
- let aux start_to (acc_offsm, acc_alarm, acc_success) =
+ let aux start_to (acc_offsm, acc_success) =
let stop_to = Int.pred (Int.add start_to size) in
(* check if at least one access is possibly valid *)
if Int.lt start_to min_valid || Int.gt stop_to max_maybe_valid then
(* at least one bit cannot be written => invalid access *)
- acc_offsm, true, acc_success
+ acc_offsm, acc_success
else
let exact = exact && not (Base.is_weak_validity validity) in
- let alarm = acc_alarm || Int.gt stop_to max_sure_valid in
- paste_slice_itv ~exact src stop_src start_to acc_offsm, alarm, true
+ paste_slice_itv ~exact src stop_src start_to acc_offsm, true
in
(* TODO: this should be improved if offsets if of the form [a..b]c%d
with d >= size. In this case, the write do not overlap, and
could be done in one run in the offsetmap itself, using a zipper *)
- let res, alarm, success = Ival.fold_int aux offsets (dst, false, false) in
- if success then alarm, `Value res else true, `Bottom
+ let res, success = Ival.fold_int aux offsets (dst, false) in
+ if success then `Value res else `Bottom
with Not_less_than ->
(* Value to paste, since we cannot be precise *)
let v =
@@ -2050,11 +2038,8 @@ let update_under ~validity ~exact ~offsets ~size v t =
when doing 'find' *)
if size <=~ Integer.of_int 128 then
let validity_src = Base.validity_from_size size in
- let _, v =
- find ~validity:validity_src ~conflate_bottom:false
- ~offsets:Ival.zero ~size src
- in
- v
+ find ~validity:validity_src ~conflate_bottom:false
+ ~offsets:Ival.zero ~size src
else
(* This is a struct or an array. Either the result will be imprecise
because catenating semi-imprecise values through merge_bits
@@ -2074,7 +2059,7 @@ let update_under ~validity ~exact ~offsets ~size v t =
(** pastes [from] (of size [size]) at all [offsets] in [dst] *)
let paste_slice ~validity ~exact ~from:src ~size ~offsets dst =
- if Int.(equal size zero) then (* nothing to do *) false, `Value dst
+ if Int.(equal size zero) then (* nothing to do *) `Value dst
else
match offsets, src with
(*Special case: [from] contains a single (aligned) binding [v], and [size]
@@ -2714,7 +2699,7 @@ module Int_Intervals = struct
let max = pred (start_max +~ size) in
let curr_off, ifalse = aux_create_interval ~min ~max false in
let validity = Base.Known (min, max) in
- let _alarm, (curr_off', i) =
+ let curr_off', i =
try
Int_Intervals_Map.update_aux
~validity ~exact:true ~offsets:ival ~size true curr_off ifalse
@@ -2758,7 +2743,7 @@ module Int_Intervals = struct
(* See if using [from_ival_size] would cause an approximation *)
let max = pred (start_max +~ size) in
let validity = Base.Known (min, max) in
- let _, offsets = Tr_offset.trim_by_validity ival size validity in
+ let offsets = Tr_offset.trim_by_validity ival size validity in
if Int_Intervals_Map.update_aux_tr_offsets_approximates offsets size
then bottom (* imprecise *)
else from_ival_size_over_cached ival size (* precise *)
@@ -2836,7 +2821,7 @@ end) = struct
let add_binding_ival ~validity ~exact offsets ~size v m =
match size with
| Int_Base.Value size ->
- snd (update ~validity ~exact ~offsets ~size v m)
+ update ~validity ~exact ~offsets ~size v m
| Int_Base.Top ->
update_imprecise_everywhere ~validity Origin.top v m
diff --git a/src/kernel_services/abstract_interp/offsetmap_sig.mli b/src/kernel_services/abstract_interp/offsetmap_sig.mli
index 87ee6349e914f8f428991146cde7aeba63c5a113..54f47dbbd530e2f6ac0512b89bc070ab3d18516a 100644
--- a/src/kernel_services/abstract_interp/offsetmap_sig.mli
+++ b/src/kernel_services/abstract_interp/offsetmap_sig.mli
@@ -29,7 +29,6 @@ open Abstract_interp
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 *)
@@ -182,10 +181,9 @@ val find :
validity:Base.validity ->
?conflate_bottom:bool ->
offsets:Ival.t -> size:Integer.t ->
- t -> bool * v
+ t -> 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]. *)
+ given rangemap. *)
val find_imprecise: validity:Base.validity-> t -> v
(** [find_imprecise ~validity m] returns an imprecise join of the values bound
@@ -197,9 +195,9 @@ val find_imprecise_everywhere: t -> v
val copy_slice:
validity:Base.validity ->
offsets:Ival.t -> size:Integer.t ->
- t -> alarm * t Bottom.or_bottom
+ t -> 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
+ [m] starting at offsets [offsets] and of size [size]. Offsets invalid
according to [validity] are removed. [size] must be strictly greater
than zero. *)
@@ -221,15 +219,14 @@ val update :
offsets:Ival.t ->
size:Int.t ->
v ->
- t -> alarm * t Bottom.or_bottom
+ t -> 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. *)
+ the resulting imprecision. Returns [`Bottom] when all offsets are invalid. *)
val update_under :
validity:Base.validity ->
@@ -237,7 +234,7 @@ val update_under :
offsets:Ival.t ->
size:Int.t ->
v ->
- t -> alarm * t Bottom.or_bottom
+ t -> t Bottom.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. *)
@@ -258,7 +255,7 @@ val paste_slice:
from:t ->
size:Int.t ->
offsets:Ival.t ->
- t -> alarm * t Bottom.or_bottom
+ t -> t Bottom.or_bottom
(** {2 Shape} *)
diff --git a/src/kernel_services/abstract_interp/tr_offset.ml b/src/kernel_services/abstract_interp/tr_offset.ml
index 190317dfd3faa1084880a06df2395fe5ecb7b58f..1dff8c7d48b1c8cbcd94653452626b4025e4e7ed 100644
--- a/src/kernel_services/abstract_interp/tr_offset.ml
+++ b/src/kernel_services/abstract_interp/tr_offset.ml
@@ -65,9 +65,7 @@ let reduce_offset_by_validity origin ival size validity =
| Base.Variable v -> reduce_for_bounds Int.zero v.Base.max_alloc
let trim_by_validity ?(origin=Origin.Unknown) ival size validity =
- let alarm = not (Base.offset_is_in_validity size validity ival) in
- let offset = reduce_offset_by_validity origin ival size validity in
- alarm, offset
+ reduce_offset_by_validity origin ival size validity
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/tr_offset.mli b/src/kernel_services/abstract_interp/tr_offset.mli
index d59336ec349c56dce580427d086d84151453dc43..a64e29a1612aed3378cf2573cfa6d3632ee58603 100644
--- a/src/kernel_services/abstract_interp/tr_offset.mli
+++ b/src/kernel_services/abstract_interp/tr_offset.mli
@@ -40,16 +40,11 @@ val pretty: t Pretty_utils.formatter
(** [trim_by_validity ?origin offsets size validity] reduces [offsets] so that
all accesses to [offsets+(0..size-1)] are valid according to [validity].
For a size of 0, consider the offsets up to the validity past-one valid.
- The returned boolean indicates that at least one of the offsets does not
- comply with [validity]. If the valid offsets cannot be represented
- precisely, the [Overlap] constructor is returned. When specified,
- the [origin] argument is used as the source of this imprecision . *)
+ If the valid offsets cannot be represented precisely, the [Overlap]
+ constructor is returned. When specified, the [origin] argument is used as
+ the source of this imprecision . *)
val trim_by_validity :
- ?origin:Origin.t ->
- Ival.t ->
- Integer.t ->
- Base.validity ->
- bool (** alarm *) * t
+ ?origin:Origin.t -> Ival.t -> Integer.t -> Base.validity -> t
(** This is a more complete specification of this function, for a single offset
[o]. We want to write [size>0 bits], on a base possibly valid between
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 6217f6e42a334e014d44f07a1b24e1da0039c2b2..0f49ea6243172b8b95ab56568df92361f2e7723f 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -100,7 +100,7 @@ let compute_using_prototype_for_state state kf assigns =
let acc = Function_Froms.Memory.add_binding_loc ~exact:false
acc output_loc_over input_deps in
let output_loc_under_zone = Locations.enumerate_valid_bits_under
- ~for_writing:true output_loc_under in
+ Write output_loc_under in
(* Now, perform a strong update on the zones that are guaranteed
to be assigned (under-approximation) AND that do not depend
on themselves.
@@ -347,10 +347,10 @@ struct
let deps_of_deps = Function_Froms.Memory.find state.deps_table deps in
let all_indirect = Zone.join state.additional_deps deps_of_deps in
let deps = Function_Froms.Deps.add_indirect_dep deps_right all_indirect in
+ let access = if init then Read else Write in
{ state with deps_table =
Function_Froms.Memory.add_binding_precise_loc
- ~for_writing:(not init)
- ~exact state.deps_table loc deps }
+ ~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
!Db.progress ();
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index 17ef8fb7dd3197553754330618873ec11af6eadb..30200c083f7b4283ec230bb8335927d4d76e63c4 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -47,7 +47,7 @@ class virtual do_it_ = object(self)
let loc = loc_bytes_to_loc_bits r in
let size = Bit_utils.sizeof_lval lv in
self#join
- (enumerate_valid_bits ~for_writing:false (make_loc loc size))
+ (enumerate_valid_bits Read (make_loc loc size))
end;
DoChildren
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index e1e981e872ab69b19755b18d5e5cfe15535600b4..d4d164bb0b37dccd90e04f2e1b947063c557bf93 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -123,8 +123,8 @@ let eval_assigns kf state assigns =
let loc_out_under, loc_out_over, deps =
!Db.Properties.Interp.loc_to_loc_under_over ~result:None state out.it_content
in
- (enumerate_valid_bits_under ~for_writing:true loc_out_under,
- enumerate_valid_bits ~for_writing:true loc_out_over,
+ (enumerate_valid_bits_under Write loc_out_under,
+ enumerate_valid_bits Write loc_out_over,
clean_deps deps)
with Db.Properties.Interp.No_conversion ->
Inout_parameters.warning ~current:true ~once:true
@@ -141,7 +141,7 @@ let eval_assigns kf state assigns =
let _, loc, deps =
!Db.Properties.Interp.loc_to_loc_under_over None state from in
let acc = Zone.join (clean_deps deps) acc in
- let z = enumerate_valid_bits ~for_writing:false loc in
+ let z = enumerate_valid_bits Read loc in
Zone.join z acc
in
List.fold_left aux deps l
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 29d65d3c4ca723ebf4c07abe6c55600d63a4015c..8d0c5ba63a37452d073c75c0ed816cc4c5849a5b 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -471,10 +471,7 @@ let is_variadic kf =
let key_return = Key.stmt_key ret_stmt in
let return_node = add_elem pdg key_return in
let retres_loc = Db.Value.find_return_loc pdg.fct in
- let retres =
- Locations.enumerate_valid_bits ~for_writing:false
- retres_loc
- in
+ let retres = Locations.(enumerate_valid_bits Read retres_loc) in
add_dpds pdg return_node Dpd.Data state retres_loc_dpds;
add_decl_dpds pdg return_node Dpd.Data retres_decls;
let new_state = Pdg_state.add_loc_node state true retres return_node in
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index e413f5d9ac2483cb764c1ee6bcf84d08d4b3f7f4..dac35d94de1cac889b51d9b42b3a004d8b712724 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -167,8 +167,8 @@ let frama_c_memcpy state actuals =
~from:offsetmap ~dst_loc:dst_bits ~size:size_min ~exact:true state
in
let (deps_table, sure_zone) =
- let zone_dst = enumerate_valid_bits ~for_writing:true loc_dst in
- let zone_src = enumerate_valid_bits ~for_writing:false loc_src in
+ let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
+ let zone_src = enumerate_valid_bits Locations.Read loc_src in
let deps =
Function_Froms.(Deps.add_data_dep Deps.bottom zone_src)
in
@@ -211,8 +211,8 @@ let frama_c_memcpy state actuals =
let loc_dst = make_loc (Location_Bits.shift range dst) size_char in
let c_from =
let open Function_Froms in
- let zone_src = enumerate_valid_bits ~for_writing:false loc_src in
- let zone_dst = enumerate_valid_bits ~for_writing:true loc_dst in
+ let zone_src = enumerate_valid_bits Locations.Read loc_src in
+ let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
let deps = Deps.add_data_dep Deps.bottom zone_src in
let deps_table =
Memory.add_binding ~exact:false precise_deps_table zone_dst deps
@@ -345,7 +345,7 @@ let frama_c_memset_imprecise state dst v size =
let loc = loc_bytes_to_loc_bits loc in
let loc = make_loc loc (Int_Base.inject size_char) in
let state = Cvalue.Model.add_binding ~exact:false state loc v in
- (state,enumerate_valid_bits ~for_writing:true loc)
+ (state,enumerate_valid_bits Locations.Write loc)
else (state,Zone.bottom)
in
(* Write "sure" bytes in an exact way: they exist only if there is only
@@ -367,7 +367,7 @@ let frama_c_memset_imprecise state dst v size =
~from ~dst_loc:left' ~size:sure ~exact:true new_state
in
let sure_loc = make_loc left' (Int_Base.inject sure) in
- let sure_zone = enumerate_valid_bits ~for_writing:true sure_loc in
+ let sure_zone = enumerate_valid_bits Locations.Write sure_loc in
(state,sure_zone)
else
(new_state,Zone.bottom)
@@ -444,8 +444,8 @@ let memset_typ_offsm_int full_typ i =
(* Read [full_offsm] between [offset] and [offset+size-1], and return
the value stored there. *)
let find size =
- snd (V_Offsetmap.find ~validity
- ~offsets:(Ival.inject_singleton offset) ~size full_offsm)
+ V_Offsetmap.find ~validity
+ ~offsets:(Ival.inject_singleton offset) ~size full_offsm
in
(* Update [full_offsm] between [offset] and [offset+size-1], and store
exactly [v] there *)
@@ -490,7 +490,7 @@ let memset_typ_offsm_int full_typ i =
if Integer.(gt nb one) then begin
(* Copy the result *)
let src = Ival.inject_singleton offset in
- let _alarm_access, copy =
+ let copy =
V_Offsetmap.copy_slice
~validity ~offsets:src ~size:sizeelt offsm'
in
@@ -505,7 +505,7 @@ let memset_typ_offsm_int full_typ i =
match copy with
| `Bottom -> assert false (* the copy is within bounds *)
| `Value copy ->
- let _alarm_access, r =
+ let r =
V_Offsetmap.paste_slice ~validity
~exact:true ~from:copy ~size:sizeelt ~offsets:dst offsm'
in
@@ -591,8 +591,7 @@ let frama_c_memset_precise state dst v (exp_size, size) =
let open Function_Froms in
let size_bits = Integer.mul size (Bit_utils.sizeofchar ())in
let dst_location = Locations.make_loc dst_loc (Int_Base.Value size_bits) in
- let dst_zone = Locations.enumerate_valid_bits
- ~for_writing:true dst_location in
+ let dst_zone = Locations.(enumerate_valid_bits Write dst_location) in
let deps_table =
Function_Froms.Memory.add_binding ~exact:true
Function_Froms.Memory.empty dst_zone input in
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index 343dffefba4e16a5111823da6bb19630cc4551ef..3298ae3d4d48f3a32c20dcf44b40b49ba881d07c 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -149,7 +149,7 @@ let read_char kind offset cvalue acc =
let rec search_each_index kind ~validity ~index ~max offsetmap acc =
let offsets = Ival.inject_singleton index in
let size = kind.size in
- let _, cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
+ let cvalue = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsetmap in
let acc = read_char kind offsets cvalue acc in
let index = Integer.add index size in
if acc.stop || Integer.gt index max
@@ -344,10 +344,10 @@ let search_char kind ~length state str =
let reduce_by_validity ~size cvalue =
let loc_bits = Locations.loc_bytes_to_loc_bits cvalue in
let loc = Locations.make_loc loc_bits (Int_Base.inject size) in
- if Locations.is_valid ~for_writing:false loc
+ if Locations.(is_valid Read loc)
then loc.Locations.loc, true
else
- let valid_loc = Locations.valid_part ~for_writing:false ~bitfield:true loc in
+ let valid_loc = Locations.(valid_part Read ~bitfield:true loc) in
valid_loc.Locations.loc, false
type char = Char | Wide
diff --git a/src/plugins/value/domains/cvalue/cvalue_specification.ml b/src/plugins/value/domains/cvalue/cvalue_specification.ml
index 69a39589b185ee6e2704837a43b0681356a91340..756a15776b1281c77719192d8be5297a54c820ff 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -36,7 +36,7 @@ let eval_assigns_from pre_state it =
let eval_env = Eval_terms.env_assigns pre_state in
let under, _ =
Eval_terms.eval_tlval_as_zone_under_over
- ~alarm_mode:Eval_terms.Ignore ~for_writing:false eval_env term
+ ~alarm_mode:Eval_terms.Ignore Locations.Read eval_env term
in
under
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 844b890277e5e45e324a1911239fec5037816f51..69f1c355b3a96660e6ca6536cfd66394270db1d8 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -406,9 +406,7 @@ module Make
let assign _stmt left_value right_expr value valuation state =
let open Locations in
let left_loc = Precise_locs.imprecise_location left_value.lloc in
- let direct_left_zone =
- Locations.enumerate_valid_bits ~for_writing:true left_loc
- in
+ let direct_left_zone = Locations.(enumerate_valid_bits Write left_loc) in
let state = kill Hcexprs.Modified direct_left_zone state in
let right_expr = Cil.constFold true right_expr in
try
@@ -515,7 +513,7 @@ module Make
let logic_assign _assigns location ~pre:_ state =
let loc = Precise_locs.imprecise_location location in
- let zone = Locations.enumerate_valid_bits ~for_writing:true loc in
+ let zone = Locations.(enumerate_valid_bits Write loc) in
kill Hcexprs.Modified zone state
let evaluate_predicate _ _ _ = Alarmset.Unknown
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index d6dd5b5afde403c01c75a6bb3e40162e6f017069..bd2e643f14d79c980524840433d49f992389d28d 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -177,7 +177,7 @@ module Transfer = struct
let inputs_lv = Value_util.indirect_zone_of_lval to_z lv.Eval.lval in
let inputs = Zone.join inputs_e inputs_lv in
let outputs =
- Precise_locs.enumerate_valid_bits ~for_writing:true lv.Eval.lloc
+ Precise_locs.enumerate_valid_bits Locations.Write lv.Eval.lloc
in
let exact_outputs = Precise_locs.cardinal_zero_or_one lv.Eval.lloc in
{
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 6bf6163b4fa0a638d1735a23b11ae68bcb8376b9..1d197a22ce9d2aff5f1bef4948b660b9d368ebe9 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -368,7 +368,7 @@ module Memory = struct
List.fold_left aux_vi state l
let kill loc state =
- let z = Locations.enumerate_valid_bits ~for_writing:false loc in
+ let z = Locations.(enumerate_valid_bits Read loc) in
fold_overwritten remove_key state z state
(* Add the the mapping [lv --> v] to [state] when possible.
@@ -378,8 +378,7 @@ module Memory = struct
state
else
let k = K.HCE.of_lval lv in
- let for_writing = false in
- let z_lv = Precise_locs.enumerate_valid_bits ~for_writing (get_z lv) in
+ let z_lv = Precise_locs.enumerate_valid_bits Locations.Read (get_z lv) in
let z_lv_indirect = Value_util.indirect_zone_of_lval get_z lv in
if Locations.Zone.intersects z_lv z_lv_indirect then
(* The location of [lv] intersects with the zones needed to compute
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 4caa148ad2398fe93a5674f80078f0e6e6367b63..dc968ee3006341a02b5b8ba0f5e093a96b2cda78 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -133,7 +133,7 @@ let reduce_to_valid_location out loc =
None
end
else
- let valid = Locations.valid_part ~for_writing:true loc in
+ let valid = Locations.(valid_part Write loc) in
if Locations.is_bottom_loc valid then
begin
if is_assigns out && not (Locations.is_bottom_loc loc) then
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index a2b2f89b7048974510abc4680a7c074a3a0223b9..06607377956dd1dddc23320a6dbfa3dfe8ce662c 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -193,7 +193,7 @@ module Make (X: Analysis.S) = struct
if Cvalue.Model.is_reachable state then
if Int_Base.(equal loc.Locations.size zero) then GO_Empty, true
else
- let loc' = Locations.valid_part ~for_writing:false loc in
+ let loc' = Locations.(valid_part Read loc) in
if Locations.is_bottom_loc loc' then
GO_InvalidLoc, false
else
@@ -202,7 +202,7 @@ module Make (X: Analysis.S) = struct
match Cvalue.Model.copy_offsetmap loc'.Locations.loc size state with
| `Bottom -> GO_Bottom, false
| `Value offsm ->
- let ok = Locations.is_valid ~for_writing:false loc in
+ let ok = Locations.(is_valid Read loc) in
GO_Offsetmap offsm, ok
with Abstract_interp.Error_Top -> GO_Top, false
else (* Bottom state *)
@@ -261,7 +261,7 @@ module Make (X: Analysis.S) = struct
| `Bottom -> Locations.Zone.bottom, false, false
| `Value loc ->
let ploc = get_precise_loc loc in
- let z = Precise_locs.enumerate_valid_bits ~for_writing:false ploc in
+ let z = Precise_locs.enumerate_valid_bits Locations.Read ploc in
z, false, false
in
{eval_and_warn=lv_to_zone;
@@ -439,8 +439,7 @@ module Make (X: Analysis.S) = struct
let tlv_to_zone env tlv =
let alarms = ref false in
let alarm_mode = Eval_terms.Track alarms in
- let for_writing = false in
- let z = Eval_terms.eval_tlval_as_zone ~for_writing env ~alarm_mode tlv in
+ let z = Eval_terms.eval_tlval_as_zone Locations.Read env ~alarm_mode tlv in
z, not !alarms, false
in
{eval_and_warn=tlv_to_zone;
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 7e919716a71686e0ea10fd1043fd25dcfda091a7..207409c22900ce3e4105492ac3a6af47da41b382 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -54,10 +54,7 @@ let v_uninit_of_offsetmap ~typ offsm =
| Int_Base.Value size ->
let validity = Base.validity_from_size size in
let offsets = Ival.zero in
- let _alarm, r =
- V_Offsetmap.find ~validity ~conflate_bottom:false ~offsets ~size offsm
- in
- r
+ V_Offsetmap.find ~validity ~conflate_bottom:false ~offsets ~size offsm
let backward_comp_int_left positive comp l r =
if (Value_parameters.UndefinedPointerComparisonPropagateAll.get())
@@ -133,7 +130,7 @@ let reduce_by_initialized_defined f loc state =
| Ival.Not_Singleton_Int (* from Ival.project_int *) ->
state
-let reduce_by_valid_loc ~positive ~for_writing loc typ state =
+let reduce_by_valid_loc ~positive access loc typ state =
try
let value = Cvalue.Model.find state loc in
if Cvalue.V.is_imprecise value then
@@ -146,7 +143,7 @@ let reduce_by_valid_loc ~positive ~for_writing loc typ state =
let reduced_value =
Locations.loc_to_loc_without_size
(if positive
- then Locations.valid_part ~for_writing value_as_loc
+ then Locations.valid_part access value_as_loc
else Locations.invalid_part value_as_loc )
in
if V.equal value reduced_value
@@ -179,7 +176,7 @@ let apply_on_all_locs f loc state =
| Int_Base.Top -> state
| Int_Base.Value _ as size ->
try
- let loc = Locations.valid_part ~for_writing:false loc in
+ let loc = Locations.valid_part Locations.Read loc in
let loc = loc.Locations.loc in
let plevel = Value_parameters.ArrayPrecisionLevel.get() in
ignore (Locations.Location_Bits.cardinal_less_than loc plevel);
@@ -221,13 +218,13 @@ let add_if_singleton value acc =
else acc
let find_offsm_under validity ival size offsm acc =
- let _alarm, offsets = Tr_offset.trim_by_validity ival size validity in
+ let offsets = Tr_offset.trim_by_validity ival size validity in
match offsets with
| Tr_offset.Invalid | Tr_offset.Overlap _ -> acc
| Tr_offset.Set list ->
let find acc offset =
let offsets = Ival.inject_singleton offset in
- let _, value = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsm in
+ let value = Cvalue.V_Offsetmap.find ~validity ~offsets ~size offsm in
add_if_singleton value acc
in
List.fold_left find acc list
diff --git a/src/plugins/value/legacy/eval_op.mli b/src/plugins/value/legacy/eval_op.mli
index a50dbf5673ea90f5b762553805b77c48e0bbeb5f..d151cccfcca11e7ee5ce913ca2b71d5ff4984dc3 100644
--- a/src/plugins/value/legacy/eval_op.mli
+++ b/src/plugins/value/legacy/eval_op.mli
@@ -60,7 +60,7 @@ val apply_on_all_locs:
val reduce_by_valid_loc:
positive:bool ->
- for_writing:bool ->
+ Locations.access ->
Locations.location -> typ -> Model.t -> Model.t
(* [reduce_by_valid_loc positive ~for_writing loc typ state] reduces
[state] so that [loc] contains a pointer [p] such that [(typ* )p] is
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index bd7d695d4566cc4694907fb0970c6443f2df610a..72aaae64939db4a472ba53182119724d895b22c0 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -123,7 +123,7 @@ let alarm_reduce_mode () =
if Value_parameters.ReduceOnLogicAlarms.get () then Ignore else Fail
let find_or_alarm ~alarm_mode state loc =
- let is_invalid = not (Locations.is_valid ~for_writing:false loc) in
+ let is_invalid = not Locations.(is_valid Read loc) in
track_alarms is_invalid alarm_mode;
let v = Model.find_indeterminate ~conflate_bottom:true state loc in
let is_indeterminate = Cvalue.V_Or_Uninitialized.is_indeterminate v in
@@ -737,7 +737,7 @@ let rec eval_term ~alarm_mode env t =
let deps =
if Cvalue.Model.is_reachable state then
add_deps env.e_cur empty_logic_deps
- (enumerate_valid_bits ~for_writing:false eover_loc)
+ (enumerate_valid_bits Locations.Read eover_loc)
else empty_logic_deps
in
let eunder_loc = make_loc (lval.eunder) size in
@@ -1303,16 +1303,16 @@ let eval_tlval_as_location_with_deps ~alarm_mode env t =
(* Return a pair of (under-approximating, over-approximating) zones. *)
-let eval_tlval_as_zone_under_over ~alarm_mode ~for_writing env t =
+let eval_tlval_as_zone_under_over ~alarm_mode access env t =
let r = eval_tlval ~alarm_mode env t in
let s = Eval_typ.sizeof_lval_typ r.etype in
- let under = enumerate_valid_bits_under ~for_writing (make_loc r.eunder s) in
- let over = enumerate_valid_bits ~for_writing (make_loc r.eover s) in
+ let under = enumerate_valid_bits_under access (make_loc r.eunder s) in
+ let over = enumerate_valid_bits access (make_loc r.eover s) in
(under, over)
-let eval_tlval_as_zone ~alarm_mode ~for_writing env t =
+let eval_tlval_as_zone ~alarm_mode access env t =
let _under, over =
- eval_tlval_as_zone_under_over ~alarm_mode ~for_writing env t
+ eval_tlval_as_zone_under_over ~alarm_mode access env t
in
over
@@ -1487,7 +1487,7 @@ let eval_forall_predicate state r test =
let size_bits = Eval_typ.sizeof_lval_typ r.etype in
let make_loc loc = make_loc loc size_bits in
let over_loc = make_loc r.eover in
- if not (Locations.is_valid ~for_writing:false over_loc) then c_alarm ();
+ if not Locations.(is_valid Read over_loc) then c_alarm ();
match forall_in_over_location state over_loc test with
| Unknown ->
let under_loc = make_loc r.eunder in
@@ -1604,7 +1604,7 @@ let reduce_by_known_papp env positive li _labels args =
can evaluate, but on which we are not able to reduce on (yet ?).*)
env
-let reduce_by_valid env positive ~for_writing (tset: term) =
+let reduce_by_valid env positive access (tset: term) =
(* Auxiliary function that reduces \valid(lv+offs), where lv is atomic
(no more tsets), and offs is a bits-expressed constant offset.
[offs_typ] is supposed to be the type of the pointed location after [offs]
@@ -1625,7 +1625,7 @@ let reduce_by_valid env positive ~for_writing (tset: term) =
let lshifted_p = make_loc shifted_p (Eval_typ.sizeof_lval_typ offs_typ) in
let valid = (* reduce the shifted pointer to the wanted part *)
if positive
- then Locations.valid_part ~for_writing lshifted_p
+ then Locations.valid_part access lshifted_p
else Locations.invalid_part lshifted_p
in
let valid = valid.loc in
@@ -1661,7 +1661,7 @@ let reduce_by_valid env positive ~for_writing (tset: term) =
let aux_one_lval typ loc env =
try
let state =
- Eval_op.reduce_by_valid_loc ~positive ~for_writing
+ Eval_op.reduce_by_valid_loc ~positive access
loc typ (env_current_state env)
in
overwrite_current_state env state
@@ -1876,9 +1876,9 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
| _,Pvalid (_label,tsets) ->
(* TODO: label should not be ignored. Instead, we should clear
variables that are not in scope at the label. *)
- reduce_by_valid env positive ~for_writing:true tsets
+ reduce_by_valid env positive Write tsets
| _,Pvalid_read (_label,tsets) ->
- reduce_by_valid env positive ~for_writing:false tsets
+ reduce_by_valid env positive Read tsets
| _,Pvalid_function _tsets -> env (* TODO *)
@@ -2019,28 +2019,29 @@ and eval_predicate env pred =
| Pvalid (_label, tsets) | Pvalid_read (_label, tsets) -> begin
(* TODO: see same constructor in reduce_by_predicate *)
try
- let for_writing =
- (match p.pred_content with Pvalid_read _ -> false | _ -> true) in
+ let access =
+ match p.pred_content with Pvalid_read _ -> Read | _ -> Write
+ in
let state = env_current_state env in
let typ_pointed = Logic_typing.ctype_of_pointed tsets.term_type in
(* Check if we are trying to write in a const l-value *)
- if for_writing && Value_util.is_const_write_invalid typ_pointed then
+ if access = Write && Value_util.is_const_write_invalid typ_pointed then
raise Stop;
let size = Eval_typ.sizeof_lval_typ typ_pointed in
(* Check that the given location is valid *)
let valid ~over:locbytes_over ~under:locbytes_under =
let loc = loc_bytes_to_loc_bits locbytes_over in
let loc = Locations.make_loc loc size in
- if not (Locations.is_valid ~for_writing loc) then (
+ if not Locations.(is_valid access loc) then (
(* \valid does not hold if the over-approximation is invalid
everywhere, or if a part of the under-approximation is invalid
*)
- let valid = valid_part ~for_writing loc in
+ let valid = valid_part access loc in
if Locations.is_bottom_loc valid then raise Stop;
let loc_under = loc_bytes_to_loc_bits locbytes_under in
let loc_under = Locations.make_loc loc_under size in
let valid_loc_under =
- Locations.valid_part ~for_writing loc_under
+ Locations.valid_part access loc_under
in
if not (Location.equal loc_under valid_loc_under) then
raise Stop;
@@ -2051,7 +2052,7 @@ and eval_predicate env pred =
(* Evaluate the left-value, and check that it is initialized
and not an escaping pointer *)
let loc = eval_tlval_as_location ~alarm_mode env tsets in
- if not (Locations.is_valid ~for_writing:false loc) then
+ if not Locations.(is_valid Read loc) then
c_alarm ();
let v = Model.find_indeterminate state loc in
let v, ok = match v with
@@ -2329,7 +2330,7 @@ let predicate_deps env pred =
| Pinitialized (lbl, tsets) | Pdangling (lbl, tsets) ->
let loc, deploc =
eval_tlval_as_location_with_deps ~alarm_mode env tsets in
- let zone = enumerate_valid_bits ~for_writing:false loc in
+ let zone = enumerate_valid_bits Locations.Read loc in
Logic_label.Map.add lbl zone deploc
| Pnot p -> do_eval env p
diff --git a/src/plugins/value/legacy/eval_terms.mli b/src/plugins/value/legacy/eval_terms.mli
index 6f8c8f5334b54504e3ccafaa95d2f48351c0ad50..9a134a1b1aef75bc9c34cff581fb72490d9959d5 100644
--- a/src/plugins/value/legacy/eval_terms.mli
+++ b/src/plugins/value/legacy/eval_terms.mli
@@ -83,7 +83,7 @@ type alarm_mode =
(** Return a pair of (under-approximating, over-approximating) zones. *)
val eval_tlval_as_zone_under_over:
alarm_mode:alarm_mode ->
- for_writing:bool -> eval_env -> term -> Zone.t * Zone.t
+ Locations.access -> eval_env -> term -> Zone.t * Zone.t
(* ML: Should not be exported. *)
type 'a eval_result = {
@@ -104,7 +104,7 @@ val eval_tlval_as_location :
val eval_tlval_as_zone :
alarm_mode:alarm_mode ->
- for_writing:bool -> eval_env -> term -> Zone.t
+ Locations.access -> eval_env -> term -> Zone.t
val eval_predicate :
eval_env -> predicate -> predicate_status
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 2c7b988317afb6be1d88c75938e1ede69361e660..c3ec4215b3a27fc7e3359de63d965c1d4a964d32 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -59,7 +59,7 @@ let assigns_inputs_to_zone state assigns =
(fun acc t ->
let z =
Eval_terms.eval_tlval_as_zone ~alarm_mode:Eval_terms.Ignore
- ~for_writing:false env t.it_content
+ Read env t.it_content
in
Zone.join acc z)
acc
@@ -96,7 +96,7 @@ let assigns_outputs_aux ~eval ~bot ~top ~join state ~result assigns =
let assigns_outputs_to_zone =
let eval env term =
Eval_terms.eval_tlval_as_zone
- ~alarm_mode:Eval_terms.Ignore ~for_writing:true env term
+ ~alarm_mode:Eval_terms.Ignore Write env term
in
assigns_outputs_aux ~eval
~bot:Locations.Zone.bottom ~top:Locations.Zone.top ~join:Locations.Zone.join
@@ -211,7 +211,7 @@ and eval_deps_lval state lv =
match loc with
| `Bottom -> deps
| `Value loc ->
- let deps_lv = Precise_locs.enumerate_valid_bits ~for_writing loc in
+ let deps_lv = Precise_locs.enumerate_valid_bits Read loc in
Locations.Zone.join deps deps_lv
and eval_deps_addr state (h, o:lval) =
Locations.Zone.join (eval_deps_host state h) (eval_deps_offset state o)
@@ -399,7 +399,7 @@ module Export (Eval : Eval) = struct
let _, r =
lval_to_precise_loc_with_deps_state_alarm ?with_alarms state ~deps:None lv
in
- let zone = Precise_locs.enumerate_valid_bits ~for_writing:false r in
+ let zone = Precise_locs.enumerate_valid_bits Read r in
Locations.Zone.join acc zone
in
Db.Value.fold_state_callstack
@@ -407,7 +407,7 @@ module Export (Eval : Eval) = struct
let lval_to_zone_state state lv =
let _, r = lval_to_precise_loc_with_deps_state state ~deps:None lv in
- Precise_locs.enumerate_valid_bits ~for_writing:false r
+ Precise_locs.enumerate_valid_bits Read r
let lval_to_zone_with_deps_state state ~for_writing ~deps lv =
let deps, r = lval_to_precise_loc_with_deps_state state ~deps lv in
@@ -416,14 +416,15 @@ module Export (Eval : Eval) = struct
then Precise_locs.loc_bottom
else r
in
- let zone = Precise_locs.enumerate_valid_bits ~for_writing r in
+ let access = if for_writing then Write else Read in
+ let zone = Precise_locs.enumerate_valid_bits access r in
let exact = Precise_locs.valid_cardinal_zero_or_one ~for_writing r in
deps, zone, exact
let lval_to_offsetmap_aux ?with_alarms state lv =
let loc =
- Locations.valid_part ~for_writing:false
+ Locations.valid_part Read
(lval_to_loc ?with_alarms state lv)
in
match loc.Locations.size with
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index db6e355de381ed3b50f4901515712679478e4972..99bfd13838fb8991f534a2720753c88bf5b1a6e7 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -271,7 +271,7 @@ let rec zone_of_expr find_loc expr =
and zone_of_lval find_loc lval =
let ploc = find_loc lval in
let loc = Precise_locs.imprecise_location ploc in
- let zone = Locations.enumerate_valid_bits ~for_writing:false loc in
+ let zone = Locations.(enumerate_valid_bits Read loc) in
Locations.Zone.join zone
(indirect_zone_of_lval find_loc lval)
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index 9051330001c931db8f5ab8ba54637a8e4bf402c5..81f7f5347720eb559045328300b58485b67d2e40 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -61,14 +61,12 @@ let are_comparable_string pointer1 pointer2 =
In practice, function pointers are considered possible or one past
when their offset is 0. For object pointers, the offset is checked
against the validity of each base, taking past-one into account. *)
-let possible_pointer ~one_past location =
+let possible_pointer access location =
let location = Locations.loc_bytes_to_loc_bits location in
let is_possible_offset base offs =
- if Base.is_function base then
- Ival.is_zero offs
- else
- let size = if one_past then Integer.zero else Integer.one in
- Base.is_valid_offset ~for_writing:false size base offs
+ if Base.is_function base
+ then Ival.is_zero offs
+ else Base.is_valid_offset access base offs
in
Locations.Location_Bits.for_all is_possible_offset location
@@ -107,8 +105,8 @@ let are_comparable_reason kind ev1 ev2 =
else
(* Both pointers have to be almost valid (they can be pointers to one past
an array object. *)
- if (not (possible_pointer ~one_past:true rest_1)) ||
- (not (possible_pointer ~one_past:true rest_2))
+ if (not (possible_pointer Base.No_access rest_1)) ||
+ (not (possible_pointer Base.No_access rest_2))
then false, `Invalid_pointer
else
(* Equality operators allow the comparison between an almost valid pointer
@@ -133,8 +131,8 @@ let are_comparable_reason kind ev1 ev2 =
then false, `Rel_different_bases
else
(* If both addresses are valid, they can be compared for equality. *)
- if (possible_pointer ~one_past:false rest_1) &&
- (possible_pointer ~one_past:false rest_2)
+ if (possible_pointer (Base.Read Integer.one) rest_1) &&
+ (possible_pointer (Base.Read Integer.one) rest_2)
then
(* But beware of the comparisons of literal strings. *)
if are_comparable_string rest_1 rest_2
diff --git a/src/plugins/value/values/main_locations.ml b/src/plugins/value/values/main_locations.ml
index 3645e0e14d083b08ac4c3f6e9908415602b18d1f..f98119eab16be0479dd44dbd92e7c66bb668296d 100644
--- a/src/plugins/value/values/main_locations.ml
+++ b/src/plugins/value/values/main_locations.ml
@@ -138,13 +138,14 @@ module PLoc = struct
let eval_varinfo varinfo = make (Locations.loc_of_varinfo varinfo)
- let is_valid ~for_writing loc =
- Locations.is_valid ~for_writing (Precise_locs.imprecise_location loc)
+ let is_valid access loc =
+ Locations.is_valid access (Precise_locs.imprecise_location loc)
let assume_valid_location ~for_writing ~bitfield loc =
- if not (is_valid ~for_writing loc)
+ let access = Locations.(if for_writing then Write else Read) in
+ if not (is_valid access loc)
then
- let loc = Precise_locs.valid_part ~for_writing ~bitfield loc in
+ let loc = Precise_locs.valid_part access ~bitfield loc in
if Precise_locs.is_bottom_loc loc then `False else `Unknown loc
else `True
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index ad5cffc13e11f7d514c14e8a0ce508935d8a8d2d..db062fd131da08eab8e7c53b7df3f16bd068c1ff 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -44,8 +44,8 @@ let basic_copy ?(start=Int.zero) ~size o =
let validity = enough_validity ~start ~size in
let offsets = Ival.inject_singleton start in
match V_Offsetmap.copy_slice ~validity ~offsets ~size o with
- | _, `Bottom -> assert false
- | _, `Value r -> r
+ | `Bottom -> assert false
+ | `Value r -> r
(* paste [src] of size [size_src] starting at [start] in [r]. If [r] has size
[size_r], [size+start <= size_r] must hold. *)
@@ -56,14 +56,14 @@ let basic_paste ?(start=Int.zero) ~src ~size_src dst =
let offsets = Ival.inject_singleton start in
let from = src in
match V_Offsetmap.paste_slice ~validity ~exact ~from ~size ~offsets dst with
- | _, `Bottom -> assert false
- | _, `Value r -> r
+ | `Bottom -> assert false
+ | `Value r -> r
(* Reads [size] bits starting at [start] in [o], as a single value *)
let basic_find ?(start=Int.zero) ~size o =
let validity = enough_validity ~start ~size in
let offsets = Ival.inject_singleton start in
- let _, v = V_Offsetmap.find ~validity ~offsets ~size o in
+ let v = V_Offsetmap.find ~validity ~offsets ~size o in
V_Or_Uninitialized.map (fun v -> V.reinterpret_as_int ~signed:false ~size v) v
(* Paste [v] of size [size] at position [start] in [o] *)
@@ -72,8 +72,8 @@ let basic_add ?(start=Int.zero) ~size v o =
let offsets = Ival.inject_singleton start in
let v = V_Or_Uninitialized.initialized v in
match V_Offsetmap.update ~validity ~exact:true ~offsets ~size v o with
- | _, `Value m -> m
- | _ -> assert false
+ | `Value m -> m
+ | `Bottom -> assert false
let inject ~size v =
V_Offsetmap.create ~size ~size_v:size (V_Or_Uninitialized.initialized v)
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 7ee4502377bd972fd87abfb20e44dc853af3e12d..fd1b472fbcca009b6b9a6e26401e81fed87f8346 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -103,7 +103,7 @@ module V = struct
then Ival.contains_zero offset
else
let bits_offset = Ival.scale (Bit_utils.sizeofchar()) offset in
- not (Base.is_valid_offset ~for_writing:false Int.zero base bits_offset)
+ not Base.(is_valid_offset No_access base bits_offset)
in
Location_Bytes.exists offset_contains_zero loc
diff --git a/src/plugins/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index 4fd759f702f1107d6c7c6cd8a7626235e56c6fc7..4de3b0ed250790e2ff4819eb2d686657dd71310e 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -372,9 +372,9 @@ module Memory = struct
let find z m =
Deps.to_zone (find_precise z m)
- let add_binding_precise_loc ~exact ~for_writing m loc v =
+ let add_binding_precise_loc ~exact access m loc v =
let aux_one_loc loc m =
- let loc = Locations.valid_part ~for_writing loc in
+ let loc = Locations.valid_part access loc in
add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
in
Precise_locs.fold aux_one_loc loc m
diff --git a/src/plugins/value_types/function_Froms.mli b/src/plugins/value_types/function_Froms.mli
index 0c385d0254460a1a49b0e71bdef0a6be2dac09fd..b05c9dd733fbf0afb0227472cc9a9731e576681f 100644
--- a/src/plugins/value_types/function_Froms.mli
+++ b/src/plugins/value_types/function_Froms.mli
@@ -103,7 +103,7 @@ module Memory : sig
val add_binding: exact:bool -> t -> Locations.Zone.t -> Deps.t -> t
val add_binding_loc: exact:bool -> t -> Locations.location -> Deps.t -> t
val add_binding_precise_loc:
- exact:bool -> for_writing:bool -> t ->
+ exact:bool -> Locations.access -> t ->
Precise_locs.precise_location -> Deps.t -> t
val bind_var: Cil_types.varinfo -> Deps.t -> t -> t
val unbind_var: Cil_types.varinfo -> t -> t
diff --git a/src/plugins/value_types/precise_locs.ml b/src/plugins/value_types/precise_locs.ml
index 9d0eb8c75c7e121ae1b213838bcc975f50337be0..66689b97a1fc37f523458a69aaa5c68c9d9ac3de 100644
--- a/src/plugins/value_types/precise_locs.ml
+++ b/src/plugins/value_types/precise_locs.ml
@@ -305,8 +305,8 @@ let fold f pl acc =
in
fold_offset aux_po po acc
-let enumerate_valid_bits ~for_writing loc =
- let aux loc z = Zone.join z (enumerate_valid_bits ~for_writing loc) in
+let enumerate_valid_bits access loc =
+ let aux loc z = Zone.join z (enumerate_valid_bits access loc) in
fold aux loc Zone.bottom
@@ -323,7 +323,8 @@ let valid_cardinal_zero_or_one ~for_writing pl =
try
ignore
(fold (fun loc found_one ->
- let valid = Locations.valid_part ~for_writing loc in
+ let access = if for_writing then Write else Read in
+ let valid = Locations.valid_part access loc in
if Locations.is_bottom_loc loc then found_one
else
if Locations.cardinal_zero_or_one valid then
@@ -355,50 +356,20 @@ let rec reduce_offset_by_range range offset = match offset with
let offset = reduce_offset_by_range range offset in
if offset = POBottom then offset else POShift (shift, offset, card)
-(* Maintain synchronized with Locations.reduce_offset_by_validity *)
-let reduce_offset_by_validity ~for_writing ~bitfield base offset size =
- if for_writing && Base.is_read_only base then
- POBottom
- else
- match Base.validity base, size with
- | Base.Empty, _ ->
- if Int_Base.(compare size zero) > 0
- then POBottom
- else reduce_offset_by_range Ival.zero offset
- | Base.Invalid, _ -> POBottom
- | _, Int_Base.Top -> offset
- | (Base.Known (minv, maxv) | Base.Unknown (minv,_,maxv)),
- Int_Base.Value size ->
- (* The maximum offset is maxv - (size - 1), except if size = 0,
- in which case the maximum offset is exactly maxv. *)
- let pred_size = Int.max Int.zero (Int.pred size) in
- let maxv = Int.sub maxv pred_size in
- let range =
- if bitfield
- then Ival.inject_range (Some minv) (Some maxv)
- else Ival.inject_interval (Some minv) (Some maxv) Int.zero Int.eight
- in
- reduce_offset_by_range range offset
- | Base.Variable variable_v, Int_Base.Value size ->
- let pred_size = Int.max Int.zero (Int.pred size) in
- let maxv = Int.sub variable_v.Base.max_alloc pred_size in
- let range =
- if bitfield
- then Ival.inject_range (Some Int.zero) (Some maxv)
- else Ival.inject_interval (Some Int.zero) (Some maxv) Int.zero Int.eight
- in
- reduce_offset_by_range range offset
-
+let reduce_offset_by_validity ~bitfield access size base offset =
+ let access = Locations.base_access ~size access in
+ let range = Base.valid_offset ~bitfield access base in
+ if Ival.is_bottom range then POBottom else reduce_offset_by_range range offset
-let reduce_by_valid_part ~for_writing ~bitfield precise_loc size =
+let reduce_by_valid_part access ~bitfield precise_loc size =
match precise_loc with
| PLBottom -> precise_loc
| PLLoc loc ->
let loc = Locations.make_loc loc size in
- PLLoc Locations.((valid_part ~for_writing ~bitfield loc).Locations.loc)
+ PLLoc Locations.((valid_part access ~bitfield loc).Locations.loc)
| PLVarOffset (base, offset) ->
begin
- match reduce_offset_by_validity ~for_writing ~bitfield base offset size with
+ match reduce_offset_by_validity ~bitfield access size base offset with
| POBottom -> PLBottom
| offset -> PLVarOffset (base, offset)
end
@@ -407,8 +378,8 @@ let reduce_by_valid_part ~for_writing ~bitfield precise_loc size =
simultaneously [loc] and [offset]. We do nothing for the time being. *)
precise_loc
-let valid_part ~for_writing ~bitfield {loc; size} =
- { loc = reduce_by_valid_part ~for_writing ~bitfield loc size;
+let valid_part access ~bitfield {loc; size} =
+ { loc = reduce_by_valid_part ~bitfield access loc size;
size = size }
(*
diff --git a/src/plugins/value_types/precise_locs.mli b/src/plugins/value_types/precise_locs.mli
index 2ed59ce10ab8a729bfc076f87a4c58731256d525..a45c5391d1cbb34c9d8d90929e8736acf916d6ac 100644
--- a/src/plugins/value_types/precise_locs.mli
+++ b/src/plugins/value_types/precise_locs.mli
@@ -88,7 +88,7 @@ val fold:
(Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a
val enumerate_valid_bits:
- for_writing:bool -> precise_location -> Locations.Zone.t
+ Locations.access -> precise_location -> Locations.Zone.t
val valid_cardinal_zero_or_one: for_writing:bool -> precise_location -> bool
(** Is the restriction of the given location to its valid part precise enough
@@ -101,9 +101,9 @@ val cardinal_zero_or_one: precise_location -> bool
val pretty_loc: precise_location Pretty_utils.formatter
val valid_part:
- for_writing:bool -> bitfield:bool -> precise_location -> precise_location
-(** Overapproximation of the valid part of the given location for a read or write
- operation, according to the [for_writing] boolean.
+ Locations.access -> bitfield:bool -> precise_location -> precise_location
+(** Overapproximation of the valid part of the given location (without any
+ access, or for a read or write access).
[bitfield] indicates whether the location may be the one of a bitfield, and
is true by default. If it is set to false, the location is assumed to be
byte aligned, and its offset (expressed in bits) is reduced to be congruent
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index d77f1466122eaff29333291e8a76e978c2c2fbab..e27e83c8af3557509f71e9dee55793438f58b39d 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -39,6 +39,8 @@
[eva] computing for function f <- invalid_assigns_imprecise <- main.
Called from tests/builtins/imprecise.c:11.
[eva] using specification for function f
+[eva] tests/builtins/imprecise.c:11: Warning:
+ Completely invalid destination for assigns clause *p. Ignoring.
[eva] Done for function f
[eva] Recording results for invalid_assigns_imprecise
[from] Computing for function invalid_assigns_imprecise
@@ -285,7 +287,6 @@
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
p_gm_null ∈ [100..197]
[eva:final-states] Values at end of function invalid_assigns_imprecise:
- NULL[rbits 800 to 1607] ∈ [--..--]
p ∈ {0}
[eva:final-states] Values at end of function many_writes:
t_packed1{[0..298]{.i1; .i2#; .[bits 48 to 63]#}; [299].i1} ∈
@@ -490,7 +491,7 @@
Sure outputs:
p_gm_null
[inout] Out (internal) for function invalid_assigns_imprecise:
- NULL[..]; p
+ p
[inout] Inputs for function invalid_assigns_imprecise:
\nothing
[inout] InOut (internal) for function invalid_assigns_imprecise:
@@ -568,7 +569,7 @@
Sure outputs:
i; j; k[0..4]; p
[inout] Out (internal) for function main:
- NULL[..]; v1.[bits 0 to 7]; v2.[bits 32 to 63]; v3.[bits 0 to ..];
+ NULL[100..200]; v1.[bits 0 to 7]; v2.[bits 32 to 63]; v3.[bits 0 to ..];
v5.[bits 0 to ..]; p_gm_null
[inout] Inputs for function main:
NULL[100..200]; v; v1.[bits 0 to 7]; p_gm_null
@@ -836,7 +837,6 @@
NULL[rbits 800 to 1607] ∈ [--..--] or ESCAPINGADDR
p_gm_null ∈ [100..197]
[eva:final-states] Values at end of function invalid_assigns_imprecise:
- NULL[rbits 800 to 1607] ∈ [--..--]
p ∈ {0}
[eva:final-states] Values at end of function many_writes:
t_packed1{[0..298]{.i1; .i2#; .[bits 48 to 63]#}; [299].i1} ∈
@@ -1035,7 +1035,7 @@
Sure outputs:
p_gm_null
[inout] Out (internal) for function invalid_assigns_imprecise:
- NULL[..]; p
+ p
[inout] Inputs for function invalid_assigns_imprecise:
\nothing
[inout] InOut (internal) for function invalid_assigns_imprecise:
@@ -1113,7 +1113,7 @@
Sure outputs:
i; j; k[0..4]; p
[inout] Out (internal) for function main:
- NULL[..]; v1.[bits 0 to 7]; v2.[bits 32 to 63]; v3.[bits 0 to ..];
+ NULL[100..200]; v1.[bits 0 to 7]; v2.[bits 32 to 63]; v3.[bits 0 to ..];
v5.[bits 0 to ..]; p_gm_null
[inout] Inputs for function main:
NULL[100..200]; v; v1.[bits 0 to 7]; p_gm_null
diff --git a/tests/pdg/sets.ml b/tests/pdg/sets.ml
index c0753d1cddd89c081bf2b3015c30ed976b9f1423..5fcdf037acd216631a506f0a396eba8a772d0209 100644
--- a/tests/pdg/sets.ml
+++ b/tests/pdg/sets.ml
@@ -30,11 +30,7 @@ let main _ =
v
in
- let y_zone =
- Locations.enumerate_valid_bits
- ~for_writing:false
- (Locations.loc_of_varinfo y)
- in
+ let y_zone = Locations.(enumerate_valid_bits Read (loc_of_varinfo y)) in
let y_at_11_nodes, undef = (* y=5 *)
!Pdg.find_location_nodes_at_stmt
pdg (fst (Kernel_function.find_from_sid 11)) ~before:false y_zone
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index 39a9a84a8ea49c3c2fff568e972716c60b05ad56..41e55de6abc57f04b210f23b7547f49fa38d0821 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -77,7 +77,7 @@ let get_zones str_data (kinst, kf) =
let lval_term = !Db.Properties.Interp.term_lval kf str_data in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
let loc = !Db.Value.lval_to_loc (Cil_types.Kstmt kinst) lval in
- Locations.enumerate_valid_bits ~for_writing:false loc
+ Locations.(enumerate_valid_bits Read loc)
;;
let select_data_before_stmt str_data kinst kf =
@@ -91,11 +91,7 @@ let select_retres kf =
let ki = Kernel_function.find_return kf in
try
let loc = Db.Value.find_return_loc kf in
- let zone =
- Locations.enumerate_valid_bits
- ~for_writing:false
- loc
- in
+ let zone = Locations.(enumerate_valid_bits Read loc) in
let mark = Slicing.Api.Mark.make ~data:true ~addr:false ~ctrl:false in
let before = false in
Slicing.Api.Select.select_stmt_zone_internal kf ki before zone mark
diff --git a/tests/value/oracle/empty_struct.4.res.oracle b/tests/value/oracle/empty_struct.4.res.oracle
index 4daf49a7923c2705333e45daa163dd3ba05bbfba..62bc2e7b1deaaee1f22521674e50ca8e9812905e 100644
--- a/tests/value/oracle/empty_struct.4.res.oracle
+++ b/tests/value/oracle/empty_struct.4.res.oracle
@@ -6,8 +6,12 @@
NULL[rbits 0 to 15] ∈ [--..--]
s2 ∈ {0}
pgs ∈ {{ &gs }}
+[eva:alarm] tests/value/empty_struct.c:70: Warning:
+ out of bounds read. assert \valid_read(ptr_ret);
[eva] Recording results for main2
[eva] done for function main2
+[eva] tests/value/empty_struct.c:70:
+ assertion 'Eva,mem_access' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main2:
ptr_ret ∈ {2}