diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index f401f1594ad1c808bca9fa2c2909eaba6f127dd5..14176234ddcf0ae9b427423b9b9cce1535085240 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -422,37 +422,30 @@ module V = struct
let i = project_ival v in
let i = Ival.reinterpret_as_float fkind i in
inject_ival i
- with Not_based_on_null ->
- if is_bottom v
- then bottom
- else topify_arith_origin v
+ with Not_based_on_null -> topify Origin.Arith v
let cast_float_to_float fkind v =
try
let i = project_ival v in
let i = Ival.cast_float_to_float fkind i in
inject_ival i
- with Not_based_on_null ->
- if is_bottom v
- then bottom
- else topify_arith_origin v
+ with Not_based_on_null -> topify Origin.Arith v
(* Auxiliary functions for cast and reinterpration to an integer type.
[on_null] is the function to apply on the numerical part. *)
let to_int on_null ~size ~signed v =
let integer_part, pointer_part = split Base.null v in
let integer_part'= on_null ~size ~signed integer_part in
- (* ok_garbled indicates that we do _not_ create a (new) garbled mix *)
- let pointer_part', ok_garbled =
- if Int.ge size (Int.of_int (Bit_utils.sizeofpointer ())) ||
- is_bottom pointer_part || is_imprecise pointer_part
- then pointer_part, true
- else topify_arith_origin pointer_part, false
+ (* no_garble indicates that we do _not_ create a (new) garbled mix *)
+ let no_garble =
+ Int.ge size (Int.of_int (Bit_utils.sizeofpointer ())) ||
+ is_bottom pointer_part || is_imprecise pointer_part
in
- if ok_garbled && integer_part' == integer_part then
+ if no_garble && integer_part' == integer_part then
v (* both pointer and integer part are unchanged *)
else
- join (inject_ival integer_part') pointer_part'
+ let v = join (inject_ival integer_part') pointer_part in
+ if no_garble then v else topify Origin.Arith v
let cast_int_to_int ~size ~signed v =
to_int Ival.cast_int_to_int ~size ~signed v
@@ -465,10 +458,7 @@ module V = struct
let v1 = project_ival v in
let r = Ival.cast_float_to_int ~signed ~size v1 in
inject_ival r
- with Not_based_on_null ->
- if is_bottom v
- then v
- else topify_arith_origin v
+ with Not_based_on_null -> topify Origin.Arith v
let cast_float_to_int_inverse ~single_precision i =
try
@@ -482,10 +472,7 @@ module V = struct
let i = project_ival v in
let r = Ival.cast_int_to_float kind i in
inject_ival r
- with Not_based_on_null ->
- if is_bottom v
- then bottom
- else topify_arith_origin v
+ with Not_based_on_null -> topify Origin.Arith v
let cast_int_to_float_inverse ~single_precision vf =
try
@@ -496,7 +483,7 @@ module V = struct
(** Binary functions *)
- let import_function ~topify f e1 e2 =
+ let arithmetic_function f e1 e2 =
try
let v1 = project_ival e1 in
let v2 = project_ival e2 in
@@ -504,13 +491,7 @@ module V = struct
with Not_based_on_null ->
if is_bottom e1 || is_bottom e2
then bottom
- else begin
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
- end
-
- let arithmetic_function = import_function ~topify:Origin.Arith
+ else topify Origin.Arith (join e1 e2)
(* Compute the pointwise difference between two Locations_Bytes.t. *)
let sub_untyped_pointwise = sub_pointwise
@@ -521,7 +502,7 @@ module V = struct
MinusPP, by setting [factor] accordingly. This is more precise than
having multiple functions, as computations such as
[(int)&t[1] - (int)&t[2]] would not be treated precisely otherwise. *)
- let add_untyped ~topify ~factor e1 e2 =
+ let add_untyped ~origin ~factor e1 e2 =
try
if Int_Base.equal factor (Int_Base.minus_one)
then
@@ -540,9 +521,7 @@ module V = struct
try (* On the off chance that someone writes [i+(int)&p]... *)
Location_Bytes.shift (project_ival_bottom e1) e2
with Not_based_on_null ->
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ topify origin (join e1 e2)
end
with Not_found ->
(* we end up here if the only way left to make this
@@ -551,9 +530,7 @@ module V = struct
let right = Ival.scale_int_base factor (project_ival_bottom e2)
in Location_Bytes.shift right e1
with Not_based_on_null -> (* from [project_ival] *)
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ topify origin (join e1 e2)
(* Under-approximating variant of add_untyped. Takes two
under-approximation, and returns an under-approximation.*)
@@ -600,13 +577,13 @@ module V = struct
else if equal singleton_zero v2 then v1
else if equal v1 v2 && cardinal_zero_or_one v1 then v1
else
- import_function ~topify:Origin.Arith Ival.bitwise_or v1 v2
+ arithmetic_function Ival.bitwise_or v1 v2
let bitwise_and v1 v2 =
if equal v1 v2 && cardinal_zero_or_one v1 then v1
else
let f i1 i2 = Ival.bitwise_and i1 i2 in
- import_function ~topify:Origin.Arith f v1 v2
+ arithmetic_function f v1 v2
let shift_right e1 e2 =
arithmetic_function Ival.shift_right e1 e2
@@ -615,15 +592,14 @@ module V = struct
try
let i = project_ival v in
inject_ival (Ival.bitwise_signed_not i)
- with Not_based_on_null -> topify_arith_origin v
-
+ with Not_based_on_null -> topify Origin.Arith v
let bitwise_not ~size ~signed v =
try
let i = project_ival v in
inject_ival (Ival.bitwise_not ~size ~signed i)
- with Not_based_on_null -> topify_arith_origin v
+ with Not_based_on_null -> topify Origin.Arith v
- let extract_bits ~topify ~start ~stop ~size v =
+ let extract_bits ~topify:origin ~start ~stop ~size v =
try
let i = project_ival_bottom v in
false, inject_ival (Ival.extract_bits ~start ~stop ~size i)
@@ -639,10 +615,10 @@ module V = struct
Int.equal (Int.succ stop) ptr_size &&
Int.equal size ptr_size
then false, v
- else true, topify_with_origin_kind topify v
+ else true, topify origin v
(* Computes [e * 2^factor]. Auxiliary function for foo_endian_merge_bits *)
- let shift_left_by_integer ~topify factor v =
+ let shift_left_by_integer ~topify:origin factor v =
try
let i = project_ival_bottom v in
inject_ival (Ival.scale (Int.two_power factor) i)
@@ -650,7 +626,7 @@ module V = struct
| Not_based_on_null ->
if Integer.is_zero factor
then v
- else topify_with_origin_kind topify v
+ else topify origin v
| Z.Overflow -> top_int
let restrict_topint_to_size value size =
@@ -662,19 +638,14 @@ module V = struct
let v = restrict_topint_to_size v (Integer.to_int_exn size) in
shift_left_by_integer ~topify offset v
- let merge_distinct_bits ~topify ~conflate_bottom value acc =
+ let merge_distinct_bits ~topify:origin ~conflate_bottom value acc =
if is_bottom acc || is_bottom value
- then begin
+ then
if conflate_bottom
- then
- bottom
- else
- join
- (topify_with_origin_kind topify acc)
- (topify_with_origin_kind topify value)
- end
+ then bottom
+ else topify origin (join acc value)
else
- add_untyped ~topify ~factor:Int_Base.one value acc
+ add_untyped ~origin ~factor:Int_Base.one value acc
(* neutral value for foo_endian_merge_bits *)
let merge_neutral_element = singleton_zero
@@ -706,7 +677,7 @@ module V = struct
Int.min card (Int.two_power size)
let add_untyped ~factor v1 v2 =
- add_untyped ~topify:Origin.Arith ~factor v1 v2
+ add_untyped ~origin:Origin.Arith ~factor v1 v2
end
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 4e951a71e40ac0261ed1587cde7b900bb860f053..34594c75acf5a866b7e9a746f8abc9cf9296b1ab 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -196,10 +196,9 @@ module Location_Bytes = struct
if Base.Hptset.(equal b empty || equal b Base.null_set) then
top_int
else begin
- if Base.Hptset.mem Base.null b then
- Top (Base.SetLattice.inject b, o)
- else
- Top (Base.(SetLattice.inject (Hptset.add null b)), o)
+ let bases = Base.SetLattice.inject Base.(Hptset.add null b) in
+ Origin.register bases o;
+ Top (bases, o)
end
(** some functions can reduce a garbled mix, make sure to normalize
@@ -212,21 +211,18 @@ module Location_Bytes = struct
let narrow m1 m2 = normalize_top (narrow m1 m2)
let meet m1 m2 = normalize_top (meet m1 m2)
+ let is_top = function
+ | Top _ -> true
+ | Map _ -> false
+
let topify_with_origin o v =
- match v with
- | Top (s,a) ->
- Top (s, Origin.join a o)
- | v when is_zero v -> v
- | Map _ ->
- if equal v bottom then v
- else
- match get_keys v with
- | Base.SetLattice.Top -> top_with_origin o
- | Base.SetLattice.Set b -> inject_top_origin o b
+ if is_top v || is_zero v || is_bottom v then v
+ else
+ match get_keys v with
+ | Base.SetLattice.Top -> top_with_origin o
+ | Base.SetLattice.Set b -> inject_top_origin o b
- let topify_with_origin_kind ok v =
- let o = Origin.current ok in
- topify_with_origin o v
+ let topify kind = topify_with_origin (Origin.current kind)
let get_bases = get_keys
@@ -238,18 +234,6 @@ module Location_Bytes = struct
| Base.Variable { Base.weak } -> not weak
with Not_found -> false
- let topify_merge_origin v =
- topify_with_origin_kind Origin.Merge v
-
- let topify_misaligned_read_origin v =
- topify_with_origin_kind Origin.Misalign_read v
-
- let topify_arith_origin v =
- topify_with_origin_kind Origin.Arith v
-
- let topify_leaf_origin v =
- topify_with_origin_kind Origin.Leaf v
-
let may_reach base loc =
if Base.is_null base then true
else
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index c00226fda5c88eb32e638f77ccfe6857cb1b8a60..3fb04fd17907faa4702db578477c097b10880e04 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -106,16 +106,17 @@ module Location_Bytes : sig
(** Subtracts the offsets of two locations. Same as [sub_pointwise factor:1],
except that garbled mixes from operands are propagated into the result. *)
- (** Topifying of values, in case of imprecise accesses *)
- val topify_arith_origin : t -> t
- val topify_misaligned_read_origin : t -> t
- val topify_merge_origin : t -> t
- val topify_leaf_origin : t -> t
+ val topify: Origin.kind -> t -> t
+ (** [topify kind v] converts [v] to a garbled mix of the addresses pointed to
+ by [v], with origin [kind]. Returns [v] unchanged if it is bottom,
+ the singleton zero or already a garbled mix. *)
+
val topify_with_origin: Origin.t -> t -> t
- val topify_with_origin_kind: Origin.kind -> t -> t
+ (** Same as [topify] above with the given origin. *)
+
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] *)
+ (** [inject_top_origin origin bases] creates a garbled mix of bases [bases]
+ with origin [origin]. *)
val top_with_origin: Origin.t -> t
(** Completely imprecise value. Use only as last resort. *)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 08fa4d98a93a955bd17f37776e332b8e9bca9a84..3359a012d02299a38bfd84124b21d0696b67ce0b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1721,7 +1721,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let clip = clip_by_validity validity in
let r = fold
(fun (min, max as itv) (bound_v, _, _) acc ->
- let new_v = V.join (V.topify_with_origin o bound_v) v in
+ let new_v = V.topify_with_origin o (V.join bound_v v) in
let new_min, new_max = clip itv in
if new_min <=~ new_max then (* [min..max] and validity intersect *)
let acc =
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index eb11a9658de4bed9ccd8704920547c42902d6a2e..fd87a5148a45852f89a9bf5092f2785b3128701c 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -48,23 +48,10 @@ let kind_label = function
type location = Cil_datatype.Location.t
type tt =
- | Origin of { kind: kind; loc: location; id: int; }
+ | Origin of { kind: kind; loc: location; }
| Well
| Unknown
-(* Unique id for each origin. Used to keep the oldest origin when a garbled
- mix may have several origins. *)
-module Id = State_builder.Counter (struct let name = "Origin.Id" end)
-
-let current kind =
- let id = Id.next () in
- let loc = Current_loc.get () in
- Origin { kind; loc; id; }
-
-let well = Well
-let unknown = Unknown
-let is_unknown t = t = Unknown
-
module Prototype = struct
include Datatype.Serializable_undefined
type t = tt
@@ -99,9 +86,9 @@ end
include Datatype.Make_with_collections (Prototype)
-let pretty_as_reason fmt org =
- if not (is_unknown org)
- then Format.fprintf fmt " because of %a" pretty org
+let pretty_as_reason fmt origin =
+ if origin <> Unknown
+ then Format.fprintf fmt " because of %a" pretty origin
let descr = function
| Unknown -> "unknown origin"
@@ -114,17 +101,16 @@ let descr = function
| Merge -> "imprecise merge of addresses"
| Arith -> "arithmetic operation on addresses"
-(* Keep the oldest known origin: it is probably the most relevant origin, as
- subsequent ones may have been created because of the first. *)
-let join t1 t2 =
- if t1 == t2 then t1 else
- match t1, t2 with
- | Unknown, x | x, Unknown -> x
- | Well, _ | _, Well -> Well
- | Origin o1, Origin o2 -> if o1.id <= o2.id then t1 else t2
+
+let current kind = Origin { kind; loc = Current_loc.get (); }
+
+let well = Well
+let unknown = Unknown
+let is_unknown t = t = Unknown
(* For each garbled mix origin, keep track of:
+ - a unique id used to keep the oldest origin when merging two garbled mix.
- the number of writes (according to [register_write] below), i.e. the number
of times a garbled mix with this origin has been written in a state during
the analysis.
@@ -137,35 +123,90 @@ let join t1 t2 =
These info are printed at the end of an Eva analysis. *)
-module History_Info = struct
- let name = "Origin.History"
- let dependencies = []
- let size = 32
-end
-
module LocSet = Cil_datatype.Location.Set
-(* Locations of writes, locations of reads, related bases. *)
-module History_Data = Datatype.Triple (LocSet) (LocSet) (Base.SetLattice)
-module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)
+module History = struct
+
+ module Counter = State_builder.Counter (struct let name = "Origin.Id.Counter" end)
-let clear () = Id.reset (); History.clear ()
+ (* Locations of writes, locations of reads, related bases. *)
+ module Data = Datatype.Triple (LocSet) (LocSet) (Base.SetLattice)
+ module IdData = Datatype.Pair (Datatype.Int) (Data)
+
+ module History_Info = struct
+ let name = "Origin.History"
+ let dependencies = []
+ let size = 10
+ end
+
+ module Table = State_builder.Hashtbl (Hashtbl) (IdData) (History_Info)
+
+ let create () =
+ let id = Counter.next () in
+ id, (LocSet.empty, LocSet.empty, Base.SetLattice.bottom)
+
+ let register origin =
+ if not (Table.mem origin)
+ then Table.replace origin (create ())
+
+ let apply ~change origin =
+ let id, data = try Table.find origin with Not_found -> create () in
+ Table.replace origin (id, change data)
+
+ let cardinal_writes origin =
+ try let (_, (w, _r, _b)) = Table.find origin in LocSet.cardinal w
+ with Not_found -> 0
+
+ let id origin =
+ try fst (Table.find origin)
+ with Not_found -> Stdlib.max_int
+
+ let to_list () = List.of_seq (Table.to_seq ())
+
+ let clear () = Counter.reset (); Table.clear ()
+end
+
+let clear () = History.clear ()
+
+(* Keep the oldest known origin: it is probably the most relevant origin, as
+ subsequent ones may have been created because of the first. *)
+let join t1 t2 =
+ if equal t1 t2 then t1 else
+ match t1, t2 with
+ | Unknown, x | x, Unknown -> x
+ | Well, _ | _, Well -> Well
+ | Origin _, Origin _ -> if History.id t1 < History.id t2 then t1 else t2
let is_current = function
| Unknown | Well -> false
| Origin { loc } -> Cil_datatype.Location.equal loc (Current_loc.get ())
-(* Returns true if the origin has never been registered and is related to the
- current location. *)
+(* Registers the creation of the garbled mix of some origins: Misalign_write and
+ Merge, which are directly written in the cvalue states, and Arith which can
+ be created by many cvalue operations.
+ Does not register:
+ - Leaf origins, as garbled mix are often created by assigns clause and then
+ reduced to precise values by postconditions. Garbled mix with leaf origin
+ are thus registered by [register_write] called at the end of the
+ interpretation of a function specification.
+ - Misalign_read, which should be registered as a read by the cvalue domain.
+ This avoids prioritizing garbled mix created by the bitwise domain.
+ - Unknown and Well origins, which are processed separately by the [join]. *)
+let register _bases t =
+ match t with
+ | Origin { kind = Misalign_write | Merge | Arith } -> History.register t
+ | Origin { kind = Leaf | Misalign_read } | Unknown | Well -> ()
+
+(* Registers a write of a garbled mix of known origin.
+ Returns true if it is related to the current location. *)
let register_write bases t =
if is_unknown t then false else
let current_loc = Current_loc.get () in
- let is_new = not (History.mem t) in
+ let is_new = History.cardinal_writes t = 0 in
let change (w, r, b) =
LocSet.add current_loc w, r, Base.SetLattice.join b bases
in
- let create _ = LocSet.singleton current_loc, LocSet.empty, bases in
- ignore (History.memo ~change create t);
+ History.apply ~change t;
is_new && is_current t
(* Registers a read only if the current location is not that of the origin. *)
@@ -175,14 +216,13 @@ let register_read bases t =
let change (w, r, b) =
w, LocSet.add current_loc r, Base.SetLattice.join b bases
in
- let create _ = LocSet.empty, LocSet.singleton current_loc, bases in
- ignore (History.memo ~change create t)
+ History.apply ~change t
(* Returns the list of recorded origins, sorted by number of reads.
Origins with no reads are filtered. *)
let get_history () =
- let list = List.of_seq (History.to_seq ()) in
- let count (origin, (w, r, bases)) =
+ let list = History.to_list () in
+ let count (origin, (_id, (w, r, bases))) =
if LocSet.is_empty r
then None
else Some (origin, (LocSet.cardinal w, LocSet.cardinal r, bases))
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 44f23b221892e0c605b5edfa640ab0d283fa2858..35d51309cd87b5399935ac3328d2aef244e9f791 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -54,6 +54,9 @@ val descr: t -> string
val join: t -> t -> t
+(** Records the creation of an imprecise value of the given bases. *)
+val register: Base.SetLattice.t -> t -> unit
+
(** Records the write of an imprecise value of the given bases,
with the given origin.
Returns [true] if the given origin has never been written before,
diff --git a/src/plugins/eva/domains/cvalue/builtins_float.ml b/src/plugins/eva/domains/cvalue/builtins_float.ml
index 9ddf6daa5498b43242fabf375dd84d56114b5c97..8e963d49efa48398a7e7d7912a7b41177d4c3f2e 100644
--- a/src/plugins/eva/domains/cvalue/builtins_float.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_float.ml
@@ -51,7 +51,7 @@ let arity2 fk caml_fun _state actuals =
let f' = Cvalue.V.inject_float (caml_fun (Fval.kind fk) f1 f2) in
remove_special_float fk f'
with Cvalue.V.Not_based_on_null ->
- Cvalue.V.topify_arith_origin (V.join arg1 arg2)
+ Cvalue.V.topify Origin.Arith (V.join arg1 arg2)
in
let result = if V.is_bottom r then [] else [r] in
Builtins.Result result
@@ -89,7 +89,7 @@ let arity1 name fk caml_fun _state actuals =
end else begin
Self.result ~once:true ~current:true
"function %s applied to address" name;
- Cvalue.V.topify_arith_origin arg
+ Cvalue.V.topify Origin.Arith arg
end
in
let result = if V.is_bottom r then [] else [r] in
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 43b19bd42586c0c09577be32dd4c1aefe5958e90..2256c9652b170ad1159a604bd20ccb7c9ee87f3a 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -212,7 +212,7 @@ module State = struct
| Some location ->
let location = Precise_locs.imprecise_location location in
let v = Cvalue.Model.find ~conflate_bottom:false state location in
- Cvalue.V.join acc (Cvalue.V.topify_leaf_origin v)
+ Cvalue.V.topify Origin.Leaf (Cvalue.V.join acc v)
else acc
in
List.fold_left one_from_contents Cvalue.V.top_int deps
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index ab2f98468fb829b093a001c480cbc0803effebb4..62175dd1c14d5b0327f30c305b5519206b0134d7 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -1544,7 +1544,7 @@ and eval_float_builtin_arity2 ~alarm_mode env name arg1 arg2 =
let f2 = Ival.project_float i2 in
Cvalue.V.inject_float (fcaml f1 f2)
with Cvalue.V.Not_based_on_null ->
- Cvalue.V.topify_arith_origin (V.join r1.eover r2.eover)
+ Cvalue.V.topify Origin.Arith (V.join r1.eover r2.eover)
in
let eunder = under_from_over v in
let ldeps = join_logic_deps r1.ldeps r2.ldeps in
@@ -1564,7 +1564,7 @@ and eval_float_builtin_arity1 ~alarm_mode env name arg =
let f = Ival.project_float i in
Cvalue.V.inject_float (fcaml f)
with Cvalue.V.Not_based_on_null ->
- Cvalue.V.topify_arith_origin r.eover
+ Cvalue.V.topify Origin.Arith r.eover
in
let eunder = under_from_over v in
{ etype = r.etype; eunder; eover = v; ldeps=r.ldeps; empty = r.empty; }
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index 3f8b7a6bf342b97743c197ee9512490b8e823415..8015fb3dd1544b778205539b6ef921345fd397be 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -364,7 +364,7 @@ let forward_minus_pp ~typ ev1 ev2 =
try
V.inject_ival (conv (Cvalue.V.project_ival minus_val))
with Cvalue.V.Not_based_on_null ->
- V.join (V.topify_arith_origin ev1) (V.topify_arith_origin ev2)
+ V.topify Origin.Arith (V.join ev1 ev2)
else
(* Pointwise arithmetics.*)
let v = V.sub_pointer ev1 ev2 in
@@ -410,7 +410,7 @@ let forward_binop_int ~typ ev1 op ev2 =
let forward_binop_float fkind ev1 op ev2 =
match V.project_float ev1, V.project_float ev2 with
| exception V.Not_based_on_null ->
- V.join (V.topify_arith_origin ev1) (V.topify_arith_origin ev2)
+ V.topify Origin.Arith (V.join ev1 ev2)
| f1, f2 ->
let binary_float_floats (_name: string) f =
V.inject_float (f fkind f1 f2)
@@ -444,7 +444,7 @@ let forward_uneg v t =
with V.Not_based_on_null ->
if Cvalue.V.is_bottom v
then v
- else V.topify_arith_origin v
+ else V.topify Origin.Arith v
let forward_unop typ op value =
match op with
diff --git a/src/plugins/eva/values/main_locations.ml b/src/plugins/eva/values/main_locations.ml
index 7f5404f77806cdf22a94ca10c036c481260ad58e..9a8a1eab3637fc7f3e8af0cf373afb50709c1bf5 100644
--- a/src/plugins/eva/values/main_locations.ml
+++ b/src/plugins/eva/values/main_locations.ml
@@ -81,7 +81,7 @@ module PLoc = struct
let forward_index typ_pointed index remaining =
match remaining with
| Imprecise offset ->
- let bases = Cvalue.V.topify_arith_origin index in
+ let bases = Cvalue.V.topify Origin.Arith index in
Imprecise (Cvalue.V.join bases offset)
| Precise offset ->
try
@@ -94,7 +94,7 @@ module PLoc = struct
with Cvalue.V.Not_based_on_null ->
(* result will be a garbled mix: collect all the bases involved in
the evaluation of [offset], and raise an exception *)
- Imprecise (Cvalue.V.topify_arith_origin index)
+ Imprecise (Cvalue.V.topify Origin.Arith index)
(* ------------------------------------------------------------------------ *)
(* Locations *)
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 6fe4eedb72486a27ebdc2582a036bea66c8573cd..1559794a477915a5ad20d5b9232252094712ec3f 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -580,7 +580,7 @@
v4.x ∈ [--..--]
.y ∈ {{ (int)&t }}
{.p; .padding[0..23]} ∈ [--..--]
- v5 ∈ {{ garbled mix of &{t} (origin: Arithmetic {memcpy.c:91}) }}
+ v5 ∈ {{ garbled mix of &{t} (origin: Misaligned read {memcpy.c:91}) }}
t{[0]; [1]{.x; .y}} ∈ {0}
[1].p ∈ {{ &v1.y }}
{[1].padding[0..23]; [2]; [3]{.x; .y}} ∈ {0}
diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle
index cd237bf6d63ad8d97d880ab1c2dcf0e24f33da60..b1030ddaf977af058e338597fcfcfe3a21784347 100644
--- a/tests/value/oracle/multidim-relations.res.oracle
+++ b/tests/value/oracle/multidim-relations.res.oracle
@@ -53,9 +53,6 @@
multidim-relations.c:19: imprecise merge of addresses
(read in 2 statements, propagated through 0 statements)
garbled mix of &{g; h}
- multidim-relations.c:18: imprecise merge of addresses
- (read in 1 statement, propagated through 0 statements)
- garbled mix of &{g; h}
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function init_array:
t[0]{.kind; .[bits 8 to 31]#} ∈ {0; 1} repeated %8