From e5046410c8cf55b61597b647b1389e090df87685 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 20 Feb 2024 11:55:30 +0100
Subject: [PATCH] [Eva] Emits a warning when some builtins propagate some
garbled mix value.
---
src/plugins/eva/domains/cvalue/builtins.ml | 2 +
.../eva/domains/cvalue/builtins_memory.ml | 37 +++++++++++++-----
.../eva/domains/cvalue/cvalue_domain.ml | 9 +++++
.../eva/domains/cvalue/cvalue_transfer.ml | 39 ++++++++-----------
.../eva/domains/cvalue/cvalue_transfer.mli | 12 ++++++
tests/builtins/oracle/memcpy.res.oracle | 3 ++
tests/builtins/oracle/memset.res.oracle | 3 ++
.../builtins/oracle_gauges/memcpy.res.oracle | 4 +-
.../value/oracle_equality/addition.res.oracle | 16 +++-----
.../value/oracle_equality/assigns.res.oracle | 4 +-
tests/value/oracle_octagon/assigns.res.oracle | 4 +-
.../value/oracle_symblocs/assigns.res.oracle | 4 +-
12 files changed, 87 insertions(+), 50 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index 4dc7cb838a7..b128b35eed8 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -252,6 +252,8 @@ let process_result call state call_result =
| Some value, Some vi_ret ->
let b_ret = Base.of_varinfo vi_ret in
let offsm = Eval_op.offsetmap_of_v ~typ:vi_ret.vtype value in
+ let prefix = "Builtin " ^ Kernel_function.get_name call.kf in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix (Cil.var vi_ret) offsm;
Cvalue.Model.add_base b_ret offsm state, clob
| _, _ -> state, clob (* TODO: error? *)
in
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index fc5a2d67965..073fc79acf0 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -30,6 +30,12 @@ let register_builtin name ?replace builtin =
let dkey = Self.register_category "imprecision"
+let rec lval_of_address exp =
+ match exp.enode with
+ | AddrOf lval -> lval
+ | CastE (_typ, exp) -> lval_of_address exp
+ | _ -> Cil.mkMem ~addr:exp ~off:Cil_types.NoOffset
+
let frama_C_is_base_aligned _state = function
| [_, x; _, y] ->
let result =
@@ -99,8 +105,10 @@ let deps_nth_arg n =
with Failure _ -> Kernel.fatal "%d arguments expected" n
-let frama_c_memcpy state actuals =
- let compute (_exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
+let frama_c_memcpy name state actuals =
+ let prefix = "Builtin " ^ name in
+ let compute (exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
+ let dst_lval = lval_of_address exp_dst in
let plevel = Parameters.ArrayPrecisionLevel.get() in
let size =
try Cvalue.V.project_ival size
@@ -132,6 +140,7 @@ let frama_c_memcpy state actuals =
memcpy_check_indeterminate_offsetmap offsetmap;
(* Read succeeded. We write the result *)
let loc_src = make_loc src (Int_Base.inject size_min) in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
let new_state =
Cvalue.Model.paste_offsetmap
~from:offsetmap ~dst_loc:dst_bits ~size:size_min ~exact:true state
@@ -212,6 +221,7 @@ let frama_c_memcpy state actuals =
raise (Memcpy_result (state,c_from,sure_zone))
| `Value offsetmap ->
memcpy_check_indeterminate_offsetmap offsetmap;
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
let new_state =
Cvalue.Model.paste_offsetmap
~from:offsetmap ~dst_loc:dst ~size:diff ~exact:false state
@@ -247,6 +257,8 @@ let frama_c_memcpy state actuals =
"@[In memcpy@ builtin:@ imprecise@ copy of@ indeterminate@ values@]%t"
Eva_utils.pp_callstack
end;
+ let value = Cvalue.V_Or_Uninitialized.get_v v in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc_dst value;
let updated_state =
Cvalue.Model.add_indeterminate_binding
~exact:false new_state loc_dst v
@@ -287,11 +299,13 @@ let frama_c_memcpy state actuals =
| [dst; src; size] -> compute dst src size
| _ -> raise (Builtins.Invalid_nb_of_args 3)
-let () = register_builtin ~replace:"memcpy" "Frama_C_memcpy" frama_c_memcpy
-let () = register_builtin ~replace:"memmove" "Frama_C_memmove" frama_c_memcpy
+let () =
+ register_builtin ~replace:"memcpy" "Frama_C_memcpy" (frama_c_memcpy "memcpy");
+ register_builtin ~replace:"memmove" "Frama_C_memmove" (frama_c_memcpy "memmove")
(* Implementation of [memset] that accepts imprecise arguments. *)
-let frama_c_memset_imprecise state dst v size =
+let frama_c_memset_imprecise state dst_lval dst v size =
+ let prefix = "Builtin memset" in
let size_char = Bit_utils.sizeofchar () in
let size_min, size_max_bytes =
try
@@ -317,6 +331,7 @@ let frama_c_memset_imprecise state dst v size =
let loc = Location_Bytes.shift shift dst in
let loc = loc_bytes_to_loc_bits loc in
let loc = make_loc loc (Int_Base.inject size_char) in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval loc v;
let state = Cvalue.Model.add_binding ~exact:false state loc v in
(state,enumerate_valid_bits Locations.Write loc)
else (state,Zone.bottom)
@@ -335,6 +350,7 @@ let frama_c_memset_imprecise state dst v size =
let left' = Location_Bits.inject base (Ival.inject_singleton maxb) in
let vuninit = V_Or_Uninitialized.initialized v in
let from = V_Offsetmap.create ~size:sure vuninit ~size_v:size_char in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval from;
let state =
Cvalue.Model.paste_offsetmap
~from ~dst_loc:left' ~size:sure ~exact:true new_state
@@ -521,7 +537,7 @@ let memset_typ_offsm typ v =
(* Precise memset builtin, that requires its arguments to be sufficiently
precise abstract values. *)
-let frama_c_memset_precise state dst v (exp_size, size) =
+let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
try
let size_char = Bit_utils.sizeofchar () in
(* We want an exact size, Otherwise, we can use the imprecise memset as a
@@ -571,6 +587,8 @@ let frama_c_memset_precise state dst v (exp_size, size) =
c_from,dst_zone
in
let _ = c_from in
+ let prefix = "Builtin memset" in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsm;
let state' =
Cvalue.Model.paste_offsetmap
~from:offsm ~dst_loc ~size:size_bits ~exact:true state
@@ -590,8 +608,9 @@ let frama_c_memset_precise state dst v (exp_size, size) =
let frama_c_memset state actuals =
match actuals with
- | [(_exp_dst, dst); (_, v); (exp_size, size)] ->
+ | [(exp_dst, dst); (_, v); (exp_size, size)] ->
begin
+ let dst_lval = lval_of_address exp_dst in
(* Remove read-only destinations *)
let dst = V.filter_base (fun b -> not (Base.is_read_only b)) dst in
(* Keep only the first byte of the value argument *)
@@ -601,13 +620,13 @@ let frama_c_memset state actuals =
~size:(Int.of_int (Cil.bitsSizeOfInt IInt))
v
in
- try frama_c_memset_precise state dst v (exp_size, size)
+ try frama_c_memset_precise state dst_lval dst v (exp_size, size)
with ImpreciseMemset reason ->
Self.debug ~dkey ~current:true
"Call to builtin precise_memset(%a) failed; %a%t"
Eva_utils.pretty_actuals actuals pretty_imprecise_memset_reason reason
Eva_utils.pp_callstack;
- frama_c_memset_imprecise state dst v size
+ frama_c_memset_imprecise state dst_lval dst v size
end
| _ -> raise (Builtins.Invalid_nb_of_args 3)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 28d8274aa83..43b19bd4258 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -148,6 +148,15 @@ module State = struct
finalize_recursive_call stmt call ~pre:(pre, clob) a post
in
let post = Option.fold ~some:finalize ~none:post recursion in
+ (* Deallocate memory allocated via alloca().
+ To minimize computations, only do it for function definitions. *)
+ let post =
+ if Kernel_function.is_definition call.kf then
+ let callstack = Eva_utils.current_call_stack () in
+ let callstack = Callstack.push call.kf stmt callstack in
+ Builtins_malloc.free_automatic_bases callstack post
+ else post
+ in
Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
>>-: fun state ->
state, clob
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 08f2e3d48be..4688f52c9b4 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -36,30 +36,34 @@ let unbottomize = function
(* Garbled mix warnings *)
(* ---------------------------------------------------------------------- *)
-let warn_imprecise_value lval value =
+let warn_imprecise_value ?prefix lval value =
match value with
| Locations.Location_Bytes.Top (bases, origin) ->
if Origin.register_write bases origin then
+ let prefix = Option.fold ~none:"A" ~some:(fun s -> s ^ ": a") prefix in
Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
- "@[Assigning imprecise value to %a@ because of %s.@]%t"
- Printer.pp_lval lval (Origin.descr origin)
+ "@[%sssigning imprecise value to %a@ because of %s.@]%t"
+ prefix Printer.pp_lval lval (Origin.descr origin)
Eva_utils.pp_callstack
| _ -> ()
-let warn_imprecise_location loc =
+let warn_imprecise_location ?prefix loc =
match loc.Locations.loc with
| Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
+ let prefix = Option.fold ~none:"" ~some:(fun s -> s ^ ": ") prefix in
Self.fatal ~current:true
- "@[writing at a completely unknown address@ because of %s.@]@\nAborting."
- (Origin.descr orig)
+ "@[%swriting at a completely unknown address@ because of %s.@]@\nAborting."
+ prefix (Origin.descr orig)
| _ -> ()
-let warn_imprecise_write lval loc value =
- warn_imprecise_location loc;
- warn_imprecise_value lval value
+let warn_imprecise_write ?prefix lval loc value =
+ warn_imprecise_location ?prefix loc;
+ warn_imprecise_value ?prefix lval value
-let warn_imprecise_offsm_write lval offsm =
- let warn v = warn_imprecise_value lval (Cvalue.V_Or_Uninitialized.get_v v) in
+let warn_imprecise_offsm_write ?prefix lval offsm =
+ let warn value =
+ warn_imprecise_value ?prefix lval (Cvalue.V_Or_Uninitialized.get_v value)
+ in
Cvalue.V_Offsetmap.iter_on_values warn offsm
(* ---------------------------------------------------------------------- *)
@@ -224,17 +228,8 @@ let actualize_formals state arguments =
let start_call _stmt call _recursion _valuation state =
`Value (actualize_formals state call.arguments)
-let finalize_call stmt call _recursion ~pre:_ ~post:state =
- (* Deallocate memory allocated via alloca().
- To minimize computations, only do it for function definitions. *)
- let state' =
- if Kernel_function.is_definition call.kf then
- let callstack = Eva_utils.current_call_stack () in
- let callstack = Callstack.push call.kf stmt callstack in
- Builtins_malloc.free_automatic_bases callstack state
- else state
- in
- `Value state'
+let finalize_call _stmt _call _recursion ~pre:_ ~post:state =
+ `Value state
let show_expr valuation state fmt expr =
match expr.enode with
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
index 5b01daee42d..0b16f6a3034 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.mli
@@ -32,6 +32,18 @@ include Abstract_domain.Transfer
and type location := location
and type origin := origin
+(** [warn_imprecise_write lval loc v] emits a warning about the assignment of
+ value [v] into location [loc] if one of them is overly imprecise. [lval] is
+ the assigned lvalue, and [prefix] is an optional prefix to the warning. *)
+val warn_imprecise_write:
+ ?prefix:string -> Cil_types.lval -> Locations.location -> Cvalue.V.t -> unit
+
+(** [warn_imprecise_offsm_write lval offsm] emits a warning about the assignment
+ of offsetmap [offsm] if it contains an overly imprecise value. [lval] is the
+ assigned lvalue, and [prefix] is an optional prefix to the warning. *)
+val warn_imprecise_offsm_write:
+ ?prefix:string -> Cil_types.lval -> Cvalue.V_Offsetmap.t -> unit
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index eada478d348..47fb30443a6 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -108,6 +108,9 @@
[eva:alarm] memcpy.c:87: Warning:
function memcpy: precondition 'valid_src' got status unknown.
[eva] memcpy.c:87: function memcpy: precondition 'separation' got status valid.
+[eva:garbled-mix:write] memcpy.c:87:
+ Builtin memcpy: assigning imprecise value to v3
+ because of misaligned read of addresses.
[eva:alarm] memcpy.c:89: Warning:
pointer downcast. assert (unsigned int)(&v4) ≤ 2147483647;
[eva:garbled-mix:write] memcpy.c:89:
diff --git a/tests/builtins/oracle/memset.res.oracle b/tests/builtins/oracle/memset.res.oracle
index 5777e0557a9..d5217c400ff 100644
--- a/tests/builtins/oracle/memset.res.oracle
+++ b/tests/builtins/oracle/memset.res.oracle
@@ -51,6 +51,9 @@
[eva] memset.c:41: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:41:
Call to builtin precise_memset(({{ (void *)&t5 }},{{ (int)&t1 }},{400})) failed; value to write is imprecise
+[eva:garbled-mix:write] memset.c:41:
+ Builtin memset: assigning imprecise value to t5[0]
+ because of misaligned read of addresses.
[eva] memset.c:44: Call to builtin memset
[eva] memset.c:44: function memset: precondition 'valid_s' got status valid.
[eva:imprecision] memset.c:44:
diff --git a/tests/builtins/oracle_gauges/memcpy.res.oracle b/tests/builtins/oracle_gauges/memcpy.res.oracle
index d2986d41912..78ce5790f07 100644
--- a/tests/builtins/oracle_gauges/memcpy.res.oracle
+++ b/tests/builtins/oracle_gauges/memcpy.res.oracle
@@ -1,5 +1,5 @@
-138a139,140
+150a151,152
> [eva] memcpy.c:96: Call to builtin memcpy
> [eva] memcpy.c:96: Call to builtin memcpy
-364a367
+376a379
> [eva] memcpy.c:230: starting to merge loop iterations
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index fe592057b7b..1f9878419ed 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -5,38 +5,32 @@
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
< [eva:garbled-mix:write] addition.i:61: Warning:
< Assigning imprecise value to p14 because of misaligned read of addresses.
-144,146c138
+144,147c138,139
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
< addition.i:61: misaligned read of addresses
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
----
-> (propagated 2 times, read 2 times) garbled mix of bases {p1}
-167c159,161
< [scope:rm_asserts] removing 9 assertion(s)
---
> (propagated 2 times, read 2 times) garbled mix of bases {p1}
> [scope:rm_asserts] removing 7 assertion(s)
-189c183
+169c161
< p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:61}) }}
---
> p14 ∈ {{ garbled mix of &{p1} (origin: Misaligned {addition.i:59}) }}
-383,386d376
+363,366d354
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
< [eva:alarm] addition.i:61: Warning:
< signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-395,397c385
+375,378c363,364
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
< addition.i:61: misaligned read of addresses
< (propagated 1 times, read 1 times) garbled mix of bases {p1}
----
-> (propagated 2 times, read 2 times) garbled mix of bases {p1}
-418c406,408
< [scope:rm_asserts] removing 9 assertion(s)
---
> (propagated 2 times, read 2 times) garbled mix of bases {p1}
> [scope:rm_asserts] removing 7 assertion(s)
-441c431
+401c387
< 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/assigns.res.oracle b/tests/value/oracle_equality/assigns.res.oracle
index 0f5f7cdfe8d..f423e4eb8cc 100644
--- a/tests/value/oracle_equality/assigns.res.oracle
+++ b/tests/value/oracle_equality/assigns.res.oracle
@@ -1,6 +1,6 @@
-149,150d148
+154,155d153
< more than 200(1000) locations to update in array. Approximating.
< [kernel] assigns.i:104:
-151a150,151
+156a155,156
> [kernel] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_octagon/assigns.res.oracle b/tests/value/oracle_octagon/assigns.res.oracle
index 0f5f7cdfe8d..f423e4eb8cc 100644
--- a/tests/value/oracle_octagon/assigns.res.oracle
+++ b/tests/value/oracle_octagon/assigns.res.oracle
@@ -1,6 +1,6 @@
-149,150d148
+154,155d153
< more than 200(1000) locations to update in array. Approximating.
< [kernel] assigns.i:104:
-151a150,151
+156a155,156
> [kernel] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
diff --git a/tests/value/oracle_symblocs/assigns.res.oracle b/tests/value/oracle_symblocs/assigns.res.oracle
index 0f5f7cdfe8d..f423e4eb8cc 100644
--- a/tests/value/oracle_symblocs/assigns.res.oracle
+++ b/tests/value/oracle_symblocs/assigns.res.oracle
@@ -1,6 +1,6 @@
-149,150d148
+154,155d153
< more than 200(1000) locations to update in array. Approximating.
< [kernel] assigns.i:104:
-151a150,151
+156a155,156
> [kernel] assigns.i:104:
> more than 200(1000) locations to update in array. Approximating.
--
GitLab