From 2dabda2cf918343fa5152008c0be9de3d45e346c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Sep 2023 15:05:44 +0200
Subject: [PATCH] [Eva] Reworks garbled mix origins.
Origins no longer have a lattice structure.
A unique id is associated to each created origin. When multiple origins can
be associated to a value, we keep the oldest origin (according to their ids).
---
src/kernel_services/abstract_interp/cvalue.ml | 8 +-
src/kernel_services/abstract_interp/lmap.ml | 2 +-
.../abstract_interp/locations.ml | 8 +-
.../abstract_interp/map_lattice.ml | 6 +-
.../abstract_interp/offsetmap.ml | 14 +-
src/kernel_services/abstract_interp/origin.ml | 308 ++++--------------
.../abstract_interp/origin.mli | 35 +-
.../eva/domains/cvalue/builtins_memory.ml | 2 +-
.../tests/known/oracle/printf.res.oracle | 2 +-
.../oracle/printf_garbled_mix.res.oracle | 2 +-
tests/builtins/oracle/memcpy.res.oracle | 2 +-
tests/float/oracle/nonlin.0.res.oracle | 4 +-
tests/float/oracle/nonlin.1.res.oracle | 4 +-
tests/float/oracle/nonlin.2.res.oracle | 4 +-
tests/float/oracle/nonlin.3.res.oracle | 4 +-
tests/float/oracle/nonlin.4.res.oracle | 4 +-
tests/float/oracle/nonlin.5.res.oracle | 4 +-
tests/libc/oracle/signal_h.res.oracle | 4 +-
tests/value/oracle/arith_pointer.res.oracle | 6 +-
tests/value/oracle/shift.0.res.oracle | 2 +-
tests/value/oracle/shift.1.res.oracle | 2 +-
.../value/oracle_bitwise/addition.res.oracle | 16 +-
.../bitwise_pointer.0.res.oracle | 12 -
.../bitwise_pointer.1.res.oracle | 12 -
.../oracle_bitwise/logic_ptr_cast.res.oracle | 6 -
.../value/oracle_equality/addition.res.oracle | 12 +
.../backward_add_ptr.res.oracle | 46 +--
27 files changed, 148 insertions(+), 383 deletions(-)
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index cd0302182f0..aa3c9b484b3 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -510,7 +510,7 @@ module V = struct
(topify_with_origin_kind topify e2)
end
- let arithmetic_function = import_function ~topify:Origin.K_Arith
+ let arithmetic_function = import_function ~topify:Origin.Arith
(* Compute the pointwise difference between two Locations_Bytes.t. *)
let sub_untyped_pointwise = sub_pointwise
@@ -600,13 +600,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.K_Arith Ival.bitwise_or v1 v2
+ import_function ~topify:Origin.Arith 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.K_Arith f v1 v2
+ import_function ~topify:Origin.Arith f v1 v2
let shift_right e1 e2 =
arithmetic_function Ival.shift_right e1 e2
@@ -706,7 +706,7 @@ module V = struct
Int.min card (Int.two_power size)
let add_untyped ~factor v1 v2 =
- add_untyped ~topify:Origin.K_Arith ~factor v1 v2
+ add_untyped ~topify:Origin.Arith ~factor v1 v2
end
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index c289a18af63..8d37feb2514 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -187,7 +187,7 @@ struct
let offm' =
match size with
| Int_Base.Top ->
- let orig = Origin.current Origin.K_Arith in
+ let orig = Origin.current Origin.Arith in
Offsetmap.update_imprecise_everywhere ~validity orig v offm
| Int_Base.Value size ->
assert (Int.ge size Int.zero);
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 616bf360823..a30181b5f0a 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -287,16 +287,16 @@ module Location_Bytes = struct
with Not_found -> false
let topify_merge_origin v =
- topify_with_origin_kind Origin.K_Merge v
+ topify_with_origin_kind Origin.Merge v
let topify_misaligned_read_origin v =
- topify_with_origin_kind Origin.K_Misalign_read v
+ topify_with_origin_kind Origin.Misalign_read v
let topify_arith_origin v =
- topify_with_origin_kind Origin.K_Arith v
+ topify_with_origin_kind Origin.Arith v
let topify_leaf_origin v =
- topify_with_origin_kind Origin.K_Leaf v
+ topify_with_origin_kind Origin.Leaf v
let may_reach base loc =
if Base.is_null base then true
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 7a64bce7a05..62bb89ef6cd 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -366,12 +366,12 @@ module Make_MapSet_Lattice
match t1, t2 with
| Top _ as x, Map _
| Map _, (Top _ as x) -> x (* arbitrary, may be approximated *)
- | Top (s1, o1), Top (s2, o2) -> Top (KSet.link s1 s2, Origin.link o1 o2)
+ | Top (s1, o1), Top (s2, o2) -> Top (KSet.link s1 s2, Origin.join o1 o2)
| Map m1, Map m2 -> Map (KVMap.link m1 m2)
let meet t1 t2 =
match t1, t2 with
- | Top (s1, o1), Top (s2, o2) -> Top (KSet.meet s1 s2, Origin.meet o1 o2)
+ | Top (s1, o1), Top (s2, o2) -> Top (KSet.meet s1 s2, Origin.join o1 o2)
| Top (KSet.Top, _), (Map _ as m)
| (Map _ as m), Top (KSet.Top, _) -> m
| Top (KSet.Set s, _), (Map m)
@@ -382,7 +382,7 @@ module Make_MapSet_Lattice
let narrow t1 t2 =
match t1, t2 with
| Top (s1, o1), Top (s2, o2) ->
- Top (KSet.narrow s1 s2, Origin.narrow o1 o2)
+ Top (KSet.narrow s1 s2, Origin.join o1 o2)
| Top (KSet.Top, _), (Map _ as m)
| (Map _ as m), Top (KSet.Top, _) -> m
| Top (KSet.Set set, _), (Map m)
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index d13cf425dbb..0b88644948d 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1144,7 +1144,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
pretty_int abs_min pretty_int abs_max pretty_int rem1 pretty_int
modu1 V.pretty v1 pretty_int rem2 pretty_int modu2 V.pretty v2 ; *)
else
- let topify = Origin.K_Merge in
+ let topify = Origin.Merge in
let offset = abs_min in
let size = Integer.length abs_min abs_max in
let v1_fit = modu1 =~ size && Rel.is_zero rem1
@@ -1174,7 +1174,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
(* similar to [f_aux_merge_generic], but we perform a reinterpretation in
all cases. This is to ensure that [V.narrow] can be applied soundly. *)
let f_aux_merge_narrow merge_v abs_min abs_max rem1 modu1 v1 rem2 modu2 v2 =
- let topify = Origin.K_Merge in
+ let topify = Origin.Merge in
let offset = abs_min in
let size = Integer.length abs_min abs_max in
let v1' =
@@ -1380,7 +1380,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
if V.is_isotropic v
then v
else
- let origin = Origin.(current K_Misalign_read) in
+ let origin = Origin.(current Misalign_read) in
V.topify_with_origin origin v
in
V.join subl_value (V.join subr_value current_node_value)
@@ -1523,7 +1523,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
(* Finds the value associated to some offsets represented as an ival. *)
let find ~validity ?(conflate_bottom=true) ~offsets ~size tree =
let offsets = Tr_offset.trim_by_validity offsets size validity in
- let topify = Origin.K_Misalign_read in
+ let topify = Origin.Misalign_read in
let read_one_node ~offset node ~start ~size acc =
extract_bits_and_stitch ~topify ~conflate_bottom
~offset:start ~size
@@ -1666,7 +1666,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
else if V.is_isotropic v_node
then rem, size, V.anisotropic_cast ~size joined_value
else
- let origin = Origin.(current K_Merge) in
+ let origin = Origin.(current Merge) in
let new_value = V.topify_with_origin origin joined_value in
let new_rem = Rel.zero and new_modu = Integer.one in
new_rem, new_modu, new_value
@@ -1849,7 +1849,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let origin =
match origin with
| Some origin -> origin
- | None -> Origin.(current K_Misalign_read)
+ | None -> Origin.(current Misalign_read)
in
let v = V.topify_with_origin origin v in
(* TODO: check *)
@@ -1872,7 +1872,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let v =
if Int.is_zero (period %~ size) then v
else
- let origin = Origin.(current K_Misalign_read) in
+ let origin = Origin.(current Misalign_read) in
let v' = V.topify_with_origin origin v in
if not (V.equal v v') then
Lattice_messages.emit_approximation msg_emitter
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 4f2c87688de..c3c4b4e1ac4 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -21,258 +21,94 @@
(**************************************************************************)
type kind =
- | K_Misalign_read
- | K_Leaf
- | K_Merge
- | K_Arith
-
-module Location = Cil_datatype.Location
-
-module LocationLattice = struct
-
- type t = Top | Bottom | Value of Location.t
-
- module Datatype_Input = struct
- include Datatype.Serializable_undefined
-
- type nonrec t = t
- let name = "Origin.LocationLattice"
- let reprs = [ Top ]
- let structural_descr =
- Structural_descr.t_sum [| [| Location.packed_descr |] |]
-
- let compare l1 l2 =
- match l1, l2 with
- | Top, Top | Bottom, Bottom -> 0
- | Value loc1, Value loc2 -> Location.compare loc1 loc2
- | Top, _ -> 1
- | _, Top -> -1
- | Bottom, _ -> -1
- | _, Bottom -> 1
-
- let equal l1 l2 =
- match l1, l2 with
- | Top, Top | Bottom, Bottom -> true
- | Value loc1, Value loc2 -> Location.equal loc1 loc2
- | _ -> false
-
- let hash = function
- | Top -> 3
- | Bottom -> 5
- | Value loc -> Location.hash loc * 7
-
- let pretty fmt = function
- | Top -> Format.fprintf fmt "Top"
- | Bottom -> Format.fprintf fmt "Bottom"
- | Value loc -> Format.fprintf fmt "{%a}" Location.pretty loc
- end
-
- include (Datatype.Make (Datatype_Input) : Datatype.S with type t := t)
-
- let current_loc () = Value (Cil.CurrentLoc.get ())
-
- let join l1 l2 =
- if l1 == l2 then l1 else
- match l1, l2 with
- | Top, _ | _, Top -> Top
- | Bottom , l | l, Bottom -> l
- | Value loc1, Value loc2 ->
- if Location.equal loc1 loc2 then l1 else Top
-
- let narrow l1 l2 =
- if l1 == l2 then l1 else
- match l1, l2 with
- | Bottom, _ | _, Bottom -> Bottom
- | Top , l | l, Top -> l
- | Value loc1, Value loc2 ->
- if Location.equal loc1 loc2 then l1 else Bottom
-
- let meet = narrow
-end
-
-type origin =
- | Misalign_read of LocationLattice.t
- | Leaf of LocationLattice.t
- | Merge of LocationLattice.t
- | Arith of LocationLattice.t
+ | Misalign_read
+ | Leaf
+ | Merge
+ | Arith
+
+let kind_rank = function
+ | Misalign_read -> 0
+ | Leaf -> 1
+ | Merge -> 2
+ | Arith -> 3
+
+let kind_label = function
+ | Misalign_read -> "Misaligned"
+ | Leaf -> "Library function"
+ | Merge -> "Merge"
+ | Arith -> "Arithmetic"
+
+type location = Cil_datatype.Location.t
+
+type tt =
+ | Origin of { kind: kind; loc: location; id: int; }
| Well
| Unknown
-let well = Well
-
-let current = function
- | K_Misalign_read -> Misalign_read (LocationLattice.current_loc ())
- | K_Leaf -> Leaf (LocationLattice.current_loc ())
- | K_Merge -> Merge (LocationLattice.current_loc ())
- | K_Arith -> Arith (LocationLattice.current_loc ())
+module Id = State_builder.Counter (struct let name = "Origin.Id" end)
-let equal o1 o2 = match o1, o2 with
- | Well, Well | Unknown, Unknown -> true
- | Leaf o1, Leaf o2 | Arith o1, Arith o2 | Merge o1, Merge o2
- | Misalign_read o1, Misalign_read o2 ->
- LocationLattice.equal o1 o2
- | Misalign_read _, _ -> false
- | _, Misalign_read _ -> false
- | Leaf _, _ -> false
- | _, Leaf _ -> false
- | Merge _, _ -> false
- | _, Merge _ -> false
- | Arith _, _ -> false
- | _, Arith _ -> false
- | _, Well | Well, _ -> false
-
-let compare o1 o2 = match o1, o2 with
- | Misalign_read s1, Misalign_read s2
- | Leaf s1, Leaf s2
- | Merge s1, Merge s2
- | Arith s1, Arith s2 ->
- LocationLattice.compare s1 s2
-
- | Well, Well | Unknown, Unknown -> 0
-
- | Misalign_read _, (Leaf _ | Merge _ | Arith _ | Well | Unknown)
- | Leaf _, (Merge _ | Arith _ | Well | Unknown)
- | Merge _, (Arith _ | Well | Unknown)
- | Arith _, (Well | Unknown)
- | Well, Unknown ->
- -1
-
- | Unknown, (Well | Arith _ | Merge _ | Leaf _ | Misalign_read _)
- | Well, (Arith _ | Merge _ | Leaf _ | Misalign_read _)
- | Arith _, (Merge _ | Leaf _ | Misalign_read _)
- | Merge _, (Leaf _ | Misalign_read _)
- | Leaf _, Misalign_read _
- -> 1
+let current kind =
+ let id = Id.next () in
+ let loc = Cil.CurrentLoc.get () in
+ Origin { kind; loc; id; }
+let well = Well
let top = Unknown
-let is_top x = equal top x
-
-
-let pretty_source fmt = function
- | LocationLattice.Top -> () (* Hide unhelpful 'TopSet' *)
- | LocationLattice.Value _ | LocationLattice.Bottom as s ->
- Format.fprintf fmt "@ %a" LocationLattice.pretty s
+let is_top t = t = Unknown
+
+module Prototype = struct
+ include Datatype.Serializable_undefined
+ type t = tt
+ let name = "Origin"
+ let reprs = [ Unknown ]
+
+ let compare t1 t2 =
+ match t1, t2 with
+ | Origin o1, Origin o2 ->
+ if o1.kind = o2.kind
+ then Cil_datatype.Location.compare o1.loc o2.loc
+ else kind_rank o2.kind - kind_rank o1.kind
+ | Well, Well | Unknown, Unknown -> 0
+ | Origin _, _ | Well, Unknown -> 1
+ | _, Origin _ | Unknown, Well -> -1
+
+ let equal = Datatype.from_compare
+
+ let hash = function
+ | Well -> 0
+ | Unknown -> 1
+ | Origin { kind; loc; } ->
+ Hashtbl.hash (kind_rank kind, Cil_datatype.Location.hash loc) + 2
+
+ let pretty fmt = function
+ | Well -> Format.fprintf fmt "Well"
+ | Unknown -> Format.fprintf fmt "Unknown"
+ | Origin { kind; loc; } ->
+ let pretty_loc = Cil_datatype.Location.pretty in
+ Format.fprintf fmt "%s@ {%a}" (kind_label kind) pretty_loc loc
+end
-let pretty fmt o = match o with
- | Unknown ->
- Format.fprintf fmt "Unknown"
- | Misalign_read o ->
- Format.fprintf fmt "Misaligned%a" pretty_source o
- | Leaf o ->
- Format.fprintf fmt "Library function%a" pretty_source o
- | Merge o ->
- Format.fprintf fmt "Merge%a" pretty_source o
- | Arith o ->
- Format.fprintf fmt "Arithmetic%a" pretty_source o
- | Well -> Format.fprintf fmt "Well"
+include Datatype.Make (Prototype)
let pretty_as_reason fmt org =
- if not (is_top org) then
- Format.fprintf fmt " because of %a" pretty org
-
+ if not (is_top org)
+ then Format.fprintf fmt " because of %a" pretty org
-let hash o = match o with
- | Misalign_read o ->
- 2001 + (LocationLattice.hash o)
- | Leaf o ->
- 2501 + (LocationLattice.hash o)
- | Merge o ->
- 3001 + (LocationLattice.hash o)
- | Arith o ->
- 3557 + (LocationLattice.hash o)
- | Well -> 17
- | Unknown -> 97
-
-include Datatype.Make
- (struct
- type t = origin
- let name = "Origin"
- let structural_descr = Structural_descr.t_unknown
- let reprs = [ Well; Unknown ]
- let compare = compare
- let equal = equal
- let hash = hash
- let rehash = Datatype.undefined
- let copy = Datatype.undefined
- let pretty = pretty
- let mem_project = Datatype.never_any_project
- end)
-
-let bottom = Arith LocationLattice.Bottom
-
-let join o1 o2 =
- let result =
- if o1 == o2
- then o1
- else
- match o1, o2 with
- | Unknown,_ | _, Unknown -> Unknown
- | Well,_ | _ , Well -> Well
- | Misalign_read o1, Misalign_read o2 ->
- Misalign_read(LocationLattice.join o1 o2)
- | _, (Misalign_read _ as m) | (Misalign_read _ as m), _ -> m
- | Leaf o1, Leaf o2 ->
- Leaf(LocationLattice.join o1 o2)
- | (Leaf _ as m), _ | _, (Leaf _ as m) -> m
- | Merge o1, Merge o2 ->
- Merge(LocationLattice.join o1 o2)
- | (Merge _ as m), _ | _, (Merge _ as m) -> m
- | Arith o1, Arith o2 ->
- Arith(LocationLattice.join o1 o2)
- (* | (Arith _ as m), _ | _, (Arith _ as m) -> m *)
- in
- (* Format.printf "Origin.join %a %a -> %a@." pretty o1 pretty o2 pretty result;
- *)
- result
-
-let link = join
-
-let meet o1 o2 =
- if o1 == o2
- then o1
- else
- match o1, o2 with
- | Arith o1, Arith o2 ->
- Arith(LocationLattice.meet o1 o2)
- | (Arith _ as m), _ | _, (Arith _ as m) -> m
- | Merge o1, Merge o2 ->
- Merge(LocationLattice.meet o1 o2)
- | (Merge _ as m), _ | _, (Merge _ as m) -> m
- | Leaf o1, Leaf o2 ->
- Leaf(LocationLattice.meet o1 o2)
- | (Leaf _ as m), _ | _, (Leaf _ as m) -> m
- | Misalign_read o1, Misalign_read o2 ->
- Misalign_read(LocationLattice.meet o1 o2)
- | _, (Misalign_read _ as m) | (Misalign_read _ as m), _ -> m
- | Well, Well -> Well
- | Well,m | m, Well -> m
- | Unknown, Unknown -> Unknown
-
-let narrow o1 o2 =
- if o1 == o2
- then o1
- else
- match o1, o2 with
- | Arith o1, Arith o2 -> Arith (LocationLattice.narrow o1 o2)
- | Merge o1, Merge o2 -> Merge (LocationLattice.narrow o1 o2)
- | Leaf o1, Leaf o2 -> Leaf (LocationLattice.narrow o1 o2)
- | Misalign_read o1, Misalign_read o2 ->
- Misalign_read (LocationLattice.narrow o1 o2)
- | Well, Well -> Well
- | Unknown, m | m, Unknown -> m
- | _, _ -> Unknown
-
-let is_included o1 o2 =
- (equal o1 (meet o1 o2))
+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 is_included = equal
(* Well and Unknown origins have no location information.
Leaf origins are also imprecise, because we may create tons of those,
that get reduced to precise values by the specifications of the function. *)
let is_precise = function
- | Well | Unknown | Leaf _ -> false
- | Misalign_read _ | Merge _ | Arith _ -> true
-
+ | Unknown | Well -> false
+ | Origin { kind } -> kind <> Leaf
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 13af0bf55aa..572f9d58694 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -28,43 +28,26 @@
ie. a numeric value that contains bits extracted from at least one
pointer, and that are not the result of a translation *)
-
-(** Lattice of source locations. *)
-module LocationLattice : Datatype.S
-
-(** List of possible origins. Most of them also include the set of
- source locations where the operation took place. *)
-type origin
-
-include Datatype.S with type t = origin
-
+include Datatype.S
type kind =
- | K_Misalign_read
- | K_Leaf
- | K_Merge
- | K_Arith
+ | Misalign_read
+ | Leaf
+ | Merge
+ | Arith
-val current: kind -> origin
+val current: kind -> t
(** This is automatically extracted from [Cil.CurrentLoc] *)
-val well: origin
-(** Creates a well origin. *)
+val well: t
+val top: t
+val is_top: t -> bool
val pretty_as_reason: Format.formatter -> t -> unit
(** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or
nothing otherwise *)
-val top: t
-val is_top: t -> bool
-
-val bottom: t
-
val join: t -> t -> t
-val link: t -> t -> t
-val meet: t -> t -> t
-val narrow: t -> t -> t
-
val is_included: t -> t -> bool
val is_precise: t -> bool
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 9cfa63a0dc9..fc5a2d67965 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -596,7 +596,7 @@ let frama_c_memset state actuals =
let dst = V.filter_base (fun b -> not (Base.is_read_only b)) dst in
(* Keep only the first byte of the value argument *)
let _, v = Cvalue.V.extract_bits
- ~topify:Origin.K_Misalign_read
+ ~topify:Origin.Misalign_read
~start:Int.zero ~stop:(Int.pred (Bit_utils.sizeofchar ()))
~size:(Int.of_int (Cil.bitsSizeOfInt IInt))
v
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 96c9680ea4b..efb382209eb 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -129,7 +129,7 @@
__fc_initial_stdout.__fc_FILE_id ∈ {1}
.__fc_FILE_data ∈
{{ garbled mix of &{"Hello world !\n"}
- (origin: Library function) }}
+ (origin: Library function {printf.c:68}) }}
string ∈ {{ "Hello world !\n" }}
wstring ∈ {{ L"Hello world !\n" }}
c ∈ {52}
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 88fba0600f5..c669384d558 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -36,7 +36,7 @@
S___fc_stdout[0].__fc_FILE_id ∈ [--..--]
[0].__fc_FILE_data ∈
{{ garbled mix of &{a}
- (origin: Library function {printf_garbled_mix.c:7}) }}
+ (origin: Arithmetic {printf_garbled_mix.c:6}) }}
[1] ∈ [--..--]
/* Generated by Frama-C */
#include "errno.h"
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 9354818cac3..33c2b065e84 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -568,7 +568,7 @@
v4.x ∈ [--..--]
.y ∈ {{ (int)&t }}
{.p; .padding[0..23]} ∈ [--..--]
- v5 ∈ {{ garbled mix of &{t} (origin: Misaligned {memcpy.c:91}) }}
+ v5 ∈ {{ garbled mix of &{t} (origin: Arithmetic {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/float/oracle/nonlin.0.res.oracle b/tests/float/oracle/nonlin.0.res.oracle
index 3c25cbe9a7e..3ba20ecccb3 100644
--- a/tests/float/oracle/nonlin.0.res.oracle
+++ b/tests/float/oracle/nonlin.0.res.oracle
@@ -244,7 +244,7 @@
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva:garbled-mix:write] nonlin.c:99:
Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -299,7 +299,7 @@
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.1.res.oracle b/tests/float/oracle/nonlin.1.res.oracle
index 5efd17ffac7..abf87dfd56f 100644
--- a/tests/float/oracle/nonlin.1.res.oracle
+++ b/tests/float/oracle/nonlin.1.res.oracle
@@ -263,7 +263,7 @@
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva:garbled-mix:write] nonlin.c:99:
Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -326,7 +326,7 @@
res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 861a2facbf8..be3781ef63b 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -246,7 +246,7 @@
The imprecision originates from Arithmetic {nonlin.c:98}
[eva:garbled-mix:write] nonlin.c:99:
Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -300,7 +300,7 @@
res ∈ [-0x1.0000000000000p0 .. inf]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.3.res.oracle b/tests/float/oracle/nonlin.3.res.oracle
index e59972c716f..9dc49e265e7 100644
--- a/tests/float/oracle/nonlin.3.res.oracle
+++ b/tests/float/oracle/nonlin.3.res.oracle
@@ -244,7 +244,7 @@
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva:garbled-mix:write] nonlin.c:99:
Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -299,7 +299,7 @@
res ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.4.res.oracle b/tests/float/oracle/nonlin.4.res.oracle
index a9cb1e55da7..84cee1a2044 100644
--- a/tests/float/oracle/nonlin.4.res.oracle
+++ b/tests/float/oracle/nonlin.4.res.oracle
@@ -263,7 +263,7 @@
non-finite float value. assert \is_finite(\add_float(a_0, a_0));
[eva:garbled-mix:write] nonlin.c:99:
Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -326,7 +326,7 @@
res ∈ {-0x1.0000000000000p0}
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index a41360104ac..00141d61ead 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -246,7 +246,7 @@
The imprecision originates from Arithmetic {nonlin.c:98}
[eva:garbled-mix:write] nonlin.c:99:
Assigning imprecise value to f.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {nonlin.c:98}
[eva] Recording results for garbled
[eva] Done for function garbled
[eva] computing for function around_zeros <- main.
@@ -300,7 +300,7 @@
res ∈ [-0x1.0000000000000p0 .. inf]
[eva:final-states] Values at end of function garbled:
a_0 ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
- f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic) }}
+ f ∈ {{ garbled mix of &{x_0} (origin: Arithmetic {nonlin.c:98}) }}
[eva:final-states] Values at end of function nonlin_f:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 59925bcb9eb..1b2258ac3dd 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -178,7 +178,7 @@
[9]{.sa_mask; .sa_flags} ∈ [--..--]
[10] ∈
{{ garbled mix of &{__fc_sigaction}
- (origin: Library function) }}
+ (origin: Library function {signal_h.c:48}) }}
[11]{.sa_handler; .sa_sigaction} ∈ {0}
[11]{.sa_mask; .sa_flags} ∈ [--..--]
[12]{.sa_handler; .sa_sigaction} ∈ {0}
@@ -193,7 +193,7 @@
{[16]{.sa_mask; .sa_flags}; [17]} ∈ [--..--]
[18] ∈
{{ garbled mix of &{__fc_sigaction}
- (origin: Library function) }}
+ (origin: Library function {signal_h.c:45}) }}
[19]{.sa_handler; .sa_sigaction} ∈ {0}
[19]{.sa_mask; .sa_flags} ∈ [--..--]
[20]{.sa_handler; .sa_sigaction} ∈ {0}
diff --git a/tests/value/oracle/arith_pointer.res.oracle b/tests/value/oracle/arith_pointer.res.oracle
index 2397783f775..c2b913baa6d 100644
--- a/tests/value/oracle/arith_pointer.res.oracle
+++ b/tests/value/oracle/arith_pointer.res.oracle
@@ -150,11 +150,9 @@
signed overflow. assert -2147483648 ≤ p2 - p1;
[eva:alarm] arith_pointer.c:56: Warning:
signed overflow. assert p2 - p1 ≤ 2147483647;
-[eva:garbled-mix:write] arith_pointer.c:56:
- Assigning imprecise value to d.
- The imprecision originates from Arithmetic
[eva] arith_pointer.c:57:
- Frama_C_show_each: {{ garbled mix of &{x} (origin: Arithmetic) }}
+ Frama_C_show_each:
+ {{ garbled mix of &{x} (origin: Arithmetic {arith_pointer.c:54}) }}
[eva] arith_pointer.c:64: Frama_C_show_each: [-3..5]
[eva] Recording results for main2
[eva] Done for function main2
diff --git a/tests/value/oracle/shift.0.res.oracle b/tests/value/oracle/shift.0.res.oracle
index bb1cdf05531..562d983b174 100644
--- a/tests/value/oracle/shift.0.res.oracle
+++ b/tests/value/oracle/shift.0.res.oracle
@@ -60,7 +60,7 @@
assert (long)r + (long)((long)((char *)t) << 8) ≤ 2147483647;
[eva:garbled-mix:write] shift.i:53:
Assigning imprecise value to r.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {shift.i:52}
[eva:alarm] shift.i:58: Warning:
unsigned overflow. assert 2U << 31 ≤ 4294967295;
[eva] Recording results for main
diff --git a/tests/value/oracle/shift.1.res.oracle b/tests/value/oracle/shift.1.res.oracle
index 601488698eb..72a6309593a 100644
--- a/tests/value/oracle/shift.1.res.oracle
+++ b/tests/value/oracle/shift.1.res.oracle
@@ -52,7 +52,7 @@
assert (long)r + (long)((long)((char *)t) << 8) ≤ 2147483647;
[eva:garbled-mix:write] shift.i:53:
Assigning imprecise value to r.
- The imprecision originates from Arithmetic
+ The imprecision originates from Arithmetic {shift.i:52}
[eva] Recording results for main
[eva] Done for function main
[eva] shift.i:35: assertion 'Eva,shift' got final status invalid.
diff --git a/tests/value/oracle_bitwise/addition.res.oracle b/tests/value/oracle_bitwise/addition.res.oracle
index f65148d676c..b130cd926c7 100644
--- a/tests/value/oracle_bitwise/addition.res.oracle
+++ b/tests/value/oracle_bitwise/addition.res.oracle
@@ -1,16 +1,6 @@
-123d122
-< The imprecision originates from Arithmetic {addition.i:52}
-162a162
+162a163
> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
-163a164
+163a165
> {{ garbled mix of &{p2} (origin: Misaligned {addition.i:56}) }}
-186c187
-< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
----
-> p10 ∈ {{ garbled mix of &{p1} }}
-405a407
+405a408
> {{ garbled mix of &{p1} (origin: Misaligned {addition.i:52}) }}
-429c431
-< p10 ∈ {{ garbled mix of &{p1} (origin: Arithmetic {addition.i:52}) }}
----
-> p10 ∈ {{ garbled mix of &{p1} }}
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
index 370739039c6..e69de29bb2d 100644
--- a/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
+++ b/tests/value/oracle_bitwise/bitwise_pointer.0.res.oracle
@@ -1,12 +0,0 @@
-34,36c34
-< [eva:garbled-mix:write] bitwise_pointer.i:18:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:18}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:18: Assigning imprecise value to p.
-41,43c39
-< [eva:garbled-mix:write] bitwise_pointer.i:22:
-< Assigning imprecise value to p1.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:22}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:22: Assigning imprecise value to p1.
diff --git a/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle b/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
index 370739039c6..e69de29bb2d 100644
--- a/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
+++ b/tests/value/oracle_bitwise/bitwise_pointer.1.res.oracle
@@ -1,12 +0,0 @@
-34,36c34
-< [eva:garbled-mix:write] bitwise_pointer.i:18:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:18}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:18: Assigning imprecise value to p.
-41,43c39
-< [eva:garbled-mix:write] bitwise_pointer.i:22:
-< Assigning imprecise value to p1.
-< The imprecision originates from Arithmetic {bitwise_pointer.i:22}
----
-> [eva:garbled-mix:write] bitwise_pointer.i:22: Assigning imprecise value to p1.
diff --git a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
index 60fe515050a..e69de29bb2d 100644
--- a/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
+++ b/tests/value/oracle_bitwise/logic_ptr_cast.res.oracle
@@ -1,6 +0,0 @@
-8,10c8
-< [eva:garbled-mix:write] logic_ptr_cast.i:8:
-< Assigning imprecise value to p.
-< The imprecision originates from Arithmetic {logic_ptr_cast.i:8}
----
-> [eva:garbled-mix:write] logic_ptr_cast.i:8: Assigning imprecise value to p.
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index 05493bd86ca..e379631a78c 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -3,10 +3,18 @@
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
+144c140
+< The imprecision originates from Misaligned {addition.i:61}
+---
+> The imprecision originates from Misaligned {addition.i:59}
168c164
< [scope:rm_asserts] removing 9 assertion(s)
---
> [scope:rm_asserts] removing 7 assertion(s)
+190c186
+< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+---
+> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
384,387d379
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
@@ -16,3 +24,7 @@
< [scope:rm_asserts] removing 9 assertion(s)
---
> [scope:rm_asserts] removing 7 assertion(s)
+433c425
+< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
+---
+> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
diff --git a/tests/value/oracle_equality/backward_add_ptr.res.oracle b/tests/value/oracle_equality/backward_add_ptr.res.oracle
index 3a6305e610f..0e1d24af5ce 100644
--- a/tests/value/oracle_equality/backward_add_ptr.res.oracle
+++ b/tests/value/oracle_equality/backward_add_ptr.res.oracle
@@ -16,65 +16,41 @@
> Called from backward_add_ptr.c:125.
> [eva] Recording results for gm
> [eva] Done for function gm
-107c113
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-142,145c148,152
-< {{ garbled mix of &{b}
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
-< [0..4294967295]
+145c151,154
< [eva] backward_add_ptr.c:160: Reusing old results for call to gm
---
-> {{ garbled mix of &{b} (origin: Arithmetic Bottom) }}, [0..4294967295]
> [eva] computing for function gm <- main4 <- main.
> Called from backward_add_ptr.c:160.
> [eva] Recording results for gm
> [eva] Done for function gm
-161c168
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-163c170
-< (origin: Arithmetic {backward_add_ptr.c:68}) }}
----
-> (origin: Arithmetic Bottom) }}
-171c178
-< (origin: Arithmetic {backward_add_ptr.c:68}) }}
----
-> (origin: Arithmetic Bottom) }}
-177c184
-< (origin: Arithmetic {backward_add_ptr.c:68}) }},
----
-> (origin: Arithmetic Bottom) }},
-189a197,198
+189a199,200
> {{ garbled mix of &{b} (origin: Arithmetic {backward_add_ptr.c:33}) }}
> {{ garbled mix of &{a} (origin: Arithmetic {backward_add_ptr.c:33}) }}
-200a210
+200a212
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:106}) }}
-202c212
+202c214
< {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
---
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:107}) }}
-203a214,216
+203a216,218
> {{ garbled mix of &{c} (origin: Arithmetic {backward_add_ptr.c:115}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:116}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:121}) }}
-204a218,219
+204a220,221
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:122}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:130}) }}
-205a221
+205a223
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:136}) }}
-206a223
+206a225
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:137}) }}
-207a225
+207a227
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:145}) }}
-208a227,230
+208a229,232
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:150}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:151}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:156}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:157}) }}
-209a232,243
+209a234,245
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:165}) }}
> {{ garbled mix of &{b; c} (origin: Arithmetic {backward_add_ptr.c:165}) }}
> {{ garbled mix of &{a; b} (origin: Arithmetic {backward_add_ptr.c:166}) }}
--
GitLab