From 02f323979c95a168bcc5889bc69449f9087271df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 10 Jun 2024 22:17:21 +0200
Subject: [PATCH] [Eva] Improves precision of memset builtin.
---
.../eva/domains/cvalue/builtins_memory.ml | 88 ++++++++------
tests/builtins/oracle/memset.res.oracle | 109 ++++++++++++------
2 files changed, 129 insertions(+), 68 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index f0c86e9e19d..30e1e753191 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -174,14 +174,14 @@ let imprecise_copy ~name ~src_loc ~dst_loc ~dst_expr state =
return [bottom]. In this case, return the previously computed state *)
if Model.is_reachable new_state then new_state else state
-(* Creates the location {loc + [0..max_size-1]} of size char. *)
-let char_location loc max_size =
+(* Creates the location {loc + [min_size..max_size-1]} of size char. *)
+let char_location loc ?(min_size=Int.zero) max_size =
let size_char = Bit_utils.sizeofchar () in
let max = Int.sub max_size size_char in
(* Use ranges modulo char_bits to read and write byte-by-byte, which can
preserve some precision.*)
let shift =
- Ival.inject_interval ~min:(Some Int.zero) ~max:(Some max)
+ Ival.inject_interval ~min:(Some min_size) ~max:(Some max)
~rem:Int.zero ~modu:size_char
in
let loc = Location_Bits.shift shift loc in
@@ -271,45 +271,65 @@ let () =
(* Implementation of [memset] that accepts imprecise arguments. *)
let frama_c_memset_imprecise state dst_expr dst v size =
let size_min, size_max = min_max_size size in
+ let exact = Location_Bits.cardinal_zero_or_one dst in
+ (* Write [v] everywhere that is written, between [dst] and [dst+size_min]. *)
+ let state, min_zone =
+ if Int.gt size_min Int.zero then
+ let size = size_min in
+ let value = Cvalue.V_Or_Uninitialized.initialized v in
+ let from = Cvalue.V_Offsetmap.create ~size ~size_v:Integer.eight value in
+ warn_imprecise_offsm_write ~name:"memset" dst_expr from;
+ let state =
+ Cvalue.Model.paste_offsetmap ~from ~size ~exact ~dst_loc:dst state
+ in
+ let loc = make_loc dst (Int_Base.Value size_min) in
+ let written_zone = enumerate_valid_bits Locations.Write loc in
+ state, written_zone
+ else state, Zone.bottom
+ in
(* Write [v] everywhere that might be written, ie between
- [dst] and [dst+size-1]. *)
- let state, over_zone =
- if Int.gt size_max Int.zero then
- let loc = char_location dst size_max in
+ [dst+size_min] and [dst+size_max-1]. *)
+ let state, extra_zone =
+ if Int.gt size_max size_min then
+ let loc = char_location dst ~min_size:size_min size_max in
warn_imprecise_write ~name:"memset" dst_expr loc v;
let state = Cvalue.Model.add_binding ~exact:false state loc v in
let written_zone = enumerate_valid_bits Locations.Write loc in
state, written_zone
else state, Zone.bottom
in
- (* Write "sure" bytes in an exact way: they exist only if there is only
- one base, and within it, size_min+leftmost_loc > rightmost_loc *)
- let state, sure_zone =
- try
- let base, offset = Location_Bits.find_lonely_key dst in
- let minb, maxb = match Ival.min_and_max offset with
- | Some minb, Some maxb -> minb, maxb
- | _ -> raise Not_found
- in
- let sure = Int.sub (Int.add minb size_min) maxb in
- if Int.gt sure Int.zero then
- let dst_loc = Location_Bits.inject base (Ival.inject_singleton maxb) in
- let vuninit = V_Or_Uninitialized.initialized v in
- let size_v = Bit_utils.sizeofchar () in
- let from = V_Offsetmap.create ~size:sure vuninit ~size_v in
- warn_imprecise_offsm_write ~name:"memset" dst_expr from;
- let state =
- Cvalue.Model.paste_offsetmap
- ~from ~dst_loc ~size:sure ~exact:true state
+ let over_zone = Zone.join min_zone extra_zone in
+ if exact
+ then state, min_zone, over_zone
+ else
+ (* Write "sure" bytes in an exact way: they exist only if there is only
+ one base, and within it, size_min+leftmost_loc > rightmost_loc *)
+ let state, sure_zone =
+ try
+ let base, offset = Location_Bits.find_lonely_key dst in
+ let minb, maxb = match Ival.min_and_max offset with
+ | Some minb, Some maxb -> minb, maxb
+ | _ -> raise Not_found
in
- let sure_loc = make_loc dst_loc (Int_Base.inject sure) in
- let sure_zone = enumerate_valid_bits Locations.Write sure_loc in
- state, sure_zone
- else
- state, Zone.bottom
- with Not_found -> state, Zone.bottom (* from find_lonely_key + explicit raise *)
- in
- state, sure_zone, over_zone
+ let sure = Int.sub (Int.add minb size_min) maxb in
+ if Int.gt sure Int.zero then
+ let dst_loc = Location_Bits.inject base (Ival.inject_singleton maxb) in
+ let vuninit = V_Or_Uninitialized.initialized v in
+ let size_v = Bit_utils.sizeofchar () in
+ let from = V_Offsetmap.create ~size:sure vuninit ~size_v in
+ warn_imprecise_offsm_write ~name:"memset" dst_expr from;
+ let state =
+ Cvalue.Model.paste_offsetmap
+ ~from ~dst_loc ~size:sure ~exact:true state
+ in
+ let sure_loc = make_loc dst_loc (Int_Base.inject sure) in
+ let sure_zone = enumerate_valid_bits Locations.Write sure_loc in
+ state, sure_zone
+ else
+ state, Zone.bottom
+ with Not_found -> state, Zone.bottom (* from find_lonely_key + explicit raise *)
+ in
+ state, sure_zone, over_zone
(* Type that describes why the 'precise memset' builtin may fail. *)
type imprecise_memset_reason =
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index 61a577a188d..ce26d8999c1 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -129,9 +129,6 @@
{0},{12})) failed; destination is not exact
[eva:alarm] memset.c:107: Warning:
accessing uninitialized left-value. assert \initialized(&s->ptr);
-[eva:alarm] memset.c:109: Warning:
- pointer comparison. assert \pointer_comparable((void *)q, (void *)0);
-[eva:alarm] memset.c:109: Warning: out of bounds write. assert \valid(q);
[eva] Recording results for memset_weak_base
[from] Computing for function memset_weak_base
[from] Done for function memset_weak_base
@@ -142,26 +139,19 @@
[from] Computing for function main
[from] Done for function main
[eva] Done for function main
-[eva:garbled-mix:summary]
- Origins of garbled mix generated during analysis:
- memset.c:106: imprecise merge of addresses
- (read in 3 statements, propagated through 1 statement)
- garbled mix of &{x}
[eva] memset.c:85: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function memset_weak_base:
- NULL[rbits 128 to 1927] ∈ [--..--]
__fc_heap_status ∈ [--..--]
x ∈ {42} or UNINITIALIZED
s ∈ {{ &__malloc_w_memset_weak_base_l101[0] }}
- q ∈ {{ NULL + [0..237] ; &x }}
- __malloc_w_memset_weak_base_l101[0].i ∈ [--..--] or UNINITIALIZED
+ q ∈ {{ NULL ; &x }}
+ __malloc_w_memset_weak_base_l101[0].i ∈ {0; 421} or UNINITIALIZED
[0].c ∈ {0; 1} or UNINITIALIZED
[0].[bits 40 to 63] ∈
{0} or UNINITIALIZED
[0].ptr ∈
- {{ garbled mix of &{x}
- (origin: Merge {memset.c:106}) }} or UNINITIALIZED
+ {{ NULL ; &x }} or UNINITIALIZED
[eva:final-states] Values at end of function test:
NULL[rbits 128 to 143] ∈ {66} repeated %8
[rbits 144 to 1927] ∈ [--..--]
@@ -190,7 +180,31 @@
[3]# ∈ {153} repeated %8
[4..6]# ∈ {0; 153} repeated %8
[7..99] ∈ {0}
- t12[0..96]# ∈ {0; 1} repeated %8
+ t12[0]# ∈ {0; 1} repeated %8
+ [1..7] ∈ {0}
+ [8]# ∈ {0; 1} repeated %8
+ [9..15] ∈ {0}
+ [16]# ∈ {0; 1} repeated %8
+ [17..23] ∈ {0}
+ [24]# ∈ {0; 1} repeated %8
+ [25..31] ∈ {0}
+ [32]# ∈ {0; 1} repeated %8
+ [33..39] ∈ {0}
+ [40]# ∈ {0; 1} repeated %8
+ [41..47] ∈ {0}
+ [48]# ∈ {0; 1} repeated %8
+ [49..55] ∈ {0}
+ [56]# ∈ {0; 1} repeated %8
+ [57..63] ∈ {0}
+ [64]# ∈ {0; 1} repeated %8
+ [65..71] ∈ {0}
+ [72]# ∈ {0; 1} repeated %8
+ [73..79] ∈ {0}
+ [80]# ∈ {0; 1} repeated %8
+ [81..87] ∈ {0}
+ [88]# ∈ {0; 1} repeated %8
+ [89..95] ∈ {0}
+ [96]# ∈ {0; 1} repeated %8
[97..99] ∈ {0}
ts[0].f1 ∈ {-2; 0}
[0].[bits 8 to 15] ∈ {0; 254}
@@ -224,7 +238,8 @@
x ∈ {{ (void *)&a }}
a ∈ {0}
[eva:final-states] Values at end of function main:
- NULL[rbits 128 to 1927] ∈ [--..--]
+ NULL[rbits 128 to 143] ∈ {66} repeated %8
+ [rbits 144 to 1927] ∈ [--..--]
__fc_heap_status ∈ [--..--]
t1[0..99] ∈ {286331153}
t2[0..99] ∈ {303174162}
@@ -251,7 +266,31 @@
[3]# ∈ {153} repeated %8
[4..6]# ∈ {0; 153} repeated %8
[7..99] ∈ {0}
- t12[0..96]# ∈ {0; 1} repeated %8
+ t12[0]# ∈ {0; 1} repeated %8
+ [1..7] ∈ {0}
+ [8]# ∈ {0; 1} repeated %8
+ [9..15] ∈ {0}
+ [16]# ∈ {0; 1} repeated %8
+ [17..23] ∈ {0}
+ [24]# ∈ {0; 1} repeated %8
+ [25..31] ∈ {0}
+ [32]# ∈ {0; 1} repeated %8
+ [33..39] ∈ {0}
+ [40]# ∈ {0; 1} repeated %8
+ [41..47] ∈ {0}
+ [48]# ∈ {0; 1} repeated %8
+ [49..55] ∈ {0}
+ [56]# ∈ {0; 1} repeated %8
+ [57..63] ∈ {0}
+ [64]# ∈ {0; 1} repeated %8
+ [65..71] ∈ {0}
+ [72]# ∈ {0; 1} repeated %8
+ [73..79] ∈ {0}
+ [80]# ∈ {0; 1} repeated %8
+ [81..87] ∈ {0}
+ [88]# ∈ {0; 1} repeated %8
+ [89..95] ∈ {0}
+ [96]# ∈ {0; 1} repeated %8
[97..99] ∈ {0}
ts[0].f1 ∈ {-2; 0}
[0].[bits 8 to 15] ∈ {0; 254}
@@ -275,12 +314,12 @@
[4]{.f3; .f4[0..2]} ∈ {-16843010; 0}
S_incomplete_type[bits 0 to 7] ∈ {65}
[bits 8 to ..] ∈ [--..--] or UNINITIALIZED
- __malloc_w_memset_weak_base_l101[0].i ∈ [--..--] or UNINITIALIZED
+ __malloc_w_memset_weak_base_l101[0].i ∈ {0; 421} or UNINITIALIZED
[0].c ∈ {0; 1} or UNINITIALIZED
[0].[bits 40 to 63] ∈
{0} or UNINITIALIZED
[0].ptr ∈
- [--..--] or UNINITIALIZED or ESCAPINGADDR
+ {0} or UNINITIALIZED or ESCAPINGADDR
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to malloc at memset.c:101 (by memset_weak_base):
__fc_heap_status FROM __fc_heap_status; size (and SELF)
@@ -325,7 +364,9 @@
ts[0..4] FROM c
\result FROM s
[from] call to memset at memset.c:72 (by test):
- t12[0..96] FROM c (and SELF)
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}
+ FROM c (and SELF)
\result FROM s
[from] call to memset at memset.c:74 (by test):
\result FROM s
@@ -353,22 +394,18 @@
[7..12] FROM \nothing (and SELF)
t11{[2]; [4..6]} FROM \nothing (and SELF)
[3] FROM \nothing
- t12[0..96] FROM \nothing (and SELF)
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}
+ FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
S_incomplete_type[bits 0 to 7] FROM \nothing
[from] call to uninit at memset.c:114 (by main):
NO EFFECTS
[from] call to memset_weak_base at memset.c:115 (by main):
- NULL[16..240]
- FROM __fc_heap_status;
- __malloc_w_memset_weak_base_l101[0].ptr (and SELF)
__fc_heap_status FROM __fc_heap_status (and SELF)
__malloc_w_memset_weak_base_l101[0] FROM __fc_heap_status (and SELF)
[from] entry point:
- NULL[16..17] FROM __fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
- [18..240]
- FROM __fc_heap_status;
- __malloc_w_memset_weak_base_l101[0].ptr (and SELF)
+ NULL[16..17] FROM \nothing
__fc_heap_status FROM __fc_heap_status (and SELF)
t1[0..99] FROM \nothing
t2[0..99] FROM \nothing
@@ -383,14 +420,15 @@
[7..12] FROM \nothing (and SELF)
t11{[2]; [4..6]} FROM \nothing (and SELF)
[3] FROM \nothing
- t12[0..96] FROM \nothing (and SELF)
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}
+ FROM \nothing (and SELF)
ts[0..4] FROM vol (and SELF)
S_incomplete_type[bits 0 to 7] FROM \nothing
__malloc_w_memset_weak_base_l101[0] FROM __fc_heap_status (and SELF)
[from] ====== END OF CALLWISE DEPENDENCIES ======
[inout] Out (internal) for function memset_weak_base:
- NULL[16..240]; __fc_heap_status; x; s; q;
- __malloc_w_memset_weak_base_l101[0]
+ __fc_heap_status; x; s; q; __malloc_w_memset_weak_base_l101[0]
[inout] Inputs for function memset_weak_base:
__fc_heap_status; __malloc_w_memset_weak_base_l101[0].ptr
[inout] InOut (internal) for function memset_weak_base:
@@ -403,7 +441,8 @@
[inout] Out (internal) for function test:
NULL[16..17]; t1[0..99]; t2[0..99]; t3[10..99]; t4[1..99]; t5[0..99];
t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99]; t10[4..12]; t11[2..6];
- t12[0..96]; ts[0..4]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}; ts[0..4]; dst; p; tmp_0; s; s1; k; absolute_valid_range;
S_incomplete_type[bits 0 to 7]
[inout] Inputs for function test:
incomplete_type; vol
@@ -428,10 +467,12 @@
Sure outputs:
a
[inout] Out (internal) for function main:
- NULL[16..240]; __fc_heap_status; t1[0..99]; t2[0..99]; t3[10..99];
+ NULL[16..17]; __fc_heap_status; t1[0..99]; t2[0..99]; t3[10..99];
t4[1..99]; t5[0..99]; t6[10..13]; t7[0..3]; t8[0..3]; t9[20..99];
- t10[4..12]; t11[2..6]; t12[0..96]; ts[0..4];
- S_incomplete_type[bits 0 to 7]; __malloc_w_memset_weak_base_l101[0]
+ t10[4..12]; t11[2..6];
+ t12{[0]; [8]; [16]; [24]; [32]; [40]; [48]; [56]; [64]; [72]; [80]; [88];
+ [96]}; ts[0..4]; S_incomplete_type[bits 0 to 7];
+ __malloc_w_memset_weak_base_l101[0]
[inout] Inputs for function main:
__fc_heap_status; incomplete_type; vol;
__malloc_w_memset_weak_base_l101[0].ptr
--
GitLab