diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 85181c1a4218956a3ac6f9d36fa17d21cb6108dd..9f0caf109ce2a5d48016d9c8066bf10c30d40fbf 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -74,25 +74,8 @@ let frama_c_offset _state = function
let () = register_builtin "Frama_C_offset" frama_c_offset
-exception Memcpy_result of (Cvalue.Model.t * Assigns.t * Zone.t)
-exception Indeterminate of V_Or_Uninitialized.t
-
-(* Called by the [memcpy] builtin. Warns when the offsetmap contains
- an indeterminate value, when the imprecision category is enabled *)
-let memcpy_check_indeterminate_offsetmap offsm =
- if Self.is_debug_key_enabled dkey then
- try
- let aux_offset _ (v, _, _) =
- match v with
- | V_Or_Uninitialized.C_init_noesc _ -> ()
- | _ -> raise (Indeterminate v)
- in
- V_Offsetmap.iter aux_offset offsm
- with Indeterminate v ->
- Self.debug ~current:true ~dkey ~once:true
- "@[In memcpy@ builtin:@ precise@ copy of@ indeterminate@ values %a@]%t"
- V_Or_Uninitialized.pretty v Eva_utils.pp_callstack
+let plevel = Parameters.ArrayPrecisionLevel.get
(* Create a dependency [\from arg_n] where n is the nth argument of the
currently called function. *)
@@ -103,206 +86,209 @@ let deps_nth_arg n =
Deps.add_data Deps.bottom (Locations.zone_of_varinfo vi)
with Failure _ -> Kernel.fatal "%d arguments expected" n
+(* -------------------------------------------------------------------------- *)
+(* Memcpy & Memmove *)
+(* -------------------------------------------------------------------------- *)
+
+(* Warns when the value is indeterminate. *)
+let warn_indeterminate_value ?(precise = false) = function
+ | V_Or_Uninitialized.C_init_noesc _ -> ()
+ | _ ->
+ Self.result ~dkey ~current:true ~once:true
+ "@[In memcpy builtin:@ %sprecise copy@ of indeterminate values.@]%t"
+ (if precise then "" else "im") Eva_utils.pp_callstack
+
+(* Warns when the offsetmap contains an indeterminate value. *)
+let check_indeterminate_offsetmap offsm =
+ if Self.is_debug_key_enabled dkey then
+ let warn _ (v, _, _) = warn_indeterminate_value ~precise:true v in
+ V_Offsetmap.iter warn offsm
+
+(* Adds \from dependency from [src_loc] to [dst_loc]. *)
+let add_deps_loc ~exact ~src_loc ~dst_loc deps_table =
+ let src_zone = Locations.(enumerate_valid_bits Read src_loc) in
+ let dst_zone = Locations.(enumerate_valid_bits Write dst_loc) in
+ let deps = Deps.(add_data bottom src_zone) in
+ Assigns.Memory.add_binding ~exact deps_table dst_zone deps
+
+(* Adds a sure \from dependency of size [size] from [src] to [dst].
+ Also returns the written zone if it is a singleton. *)
+let add_sure_deps ~size ~src ~dst (deps_table, sure_output) =
+ let size = Int_Base.inject size in
+ let src_loc = Locations.make_loc src size in
+ let dst_loc = Locations.make_loc dst size in
+ let exact = Location_Bits.cardinal_zero_or_one dst in
+ let deps_table = add_deps_loc ~exact ~src_loc ~dst_loc deps_table in
+ let dst_zone = Locations.(enumerate_valid_bits Write dst_loc) in
+ let sure_zone = if exact then dst_zone else Zone.bottom in
+ deps_table, Zone.join sure_zone sure_output
+
+(* Copy the offsetmap of size [size] from [src] to [dst] in [state]. *)
+let copy_offsetmap ~exact ~size ~src ~dst ~dst_lval state =
+ match Cvalue.Model.copy_offsetmap src size state with
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value offsetmap ->
+ check_indeterminate_offsetmap offsetmap;
+ let prefix = "Builtin memcpy" in
+ Cvalue_transfer.warn_imprecise_offsm_write ~prefix dst_lval offsetmap;
+ Cvalue.Model.paste_offsetmap ~from:offsetmap ~dst_loc:dst ~size ~exact state
+
+(* Returns the min and max size of a copy from an Ival.t. *)
+let min_max_size size =
+ let min, max = Ival.min_and_max size in
+ let min = Option.fold min ~none:Int.zero ~some:Int.(max zero) in
+ let max_max = Bit_utils.max_bit_size () in
+ let max = Option.fold max ~none:max_max ~some:Int.(max zero) in
+ min, max
+
+(* Computes the remaining [src], [dst] and [size] to be copied after [factor]
+ bits have already been copied. *)
+let shift ~factor:i src dst size =
+ let new_size = Int.sub size i in
+ let ival = Ival.inject_singleton i in
+ let new_src = Location_Bits.shift ival src in
+ let new_dst = Location_Bits.shift ival dst in
+ new_src, new_dst, new_size
+
+(* Performs the remaining copy from [src] to [dst] for all other possible [size],
+ after the copy for the minimum size has already been done.
+ Iterates on all possible values of [size] (after the first), and does the
+ copy for [previous_size..size]. *)
+let copy_remaining_size_by_size ~src ~dst ~dst_lval ~size state =
+ let exception Result of Cvalue.Model.t in
+ let do_size size (state, previous_size) =
+ (* First iteration: this copy has already been performed, skip. *)
+ if Int.(equal previous_size minus_one)
+ then state, size
+ else
+ (* Copy data between [previous_size] and [size]. *)
+ let src, dst, size = shift ~factor:previous_size src dst size in
+ (* [exact] is false as all these copies may not happen according to the
+ concrete value of [size]. *)
+ let exact = false in
+ let new_state = copy_offsetmap ~exact ~size ~src ~dst ~dst_lval state in
+ (* If this copy failed, the current size is completely invalid, and so
+ will be the following ones. Stop now with the previous state. *)
+ if not (Cvalue.Model.is_reachable new_state) then raise (Result state);
+ new_state, size
+ in
+ try fst (Ival.fold_int do_size size (state, Int.minus_one))
+ with Result state -> state
+
+(* Copy the value at location [src_loc] to location [dst_loc] in [state]. *)
+let imprecise_copy ~src_loc ~dst_loc ~dst_lval state =
+ Self.debug ~dkey ~once:true
+ ~current:true "In memcpy builtin: too many sizes to enumerate, \
+ possible loss of precision";
+ (* conflate_bottom:false as we want to copy padding bits *)
+ let v = Model.find_indeterminate ~conflate_bottom:false state src_loc in
+ warn_indeterminate_value v;
+ let value = Cvalue.V_Or_Uninitialized.get_v v in
+ let prefix = "Builtin memcpy" in
+ Cvalue_transfer.warn_imprecise_write ~prefix dst_lval dst_loc value;
+ let new_state =
+ Cvalue.Model.add_indeterminate_binding ~exact:false state dst_loc v
+ in
+ (* Beware that all sizes may be invalid, in which case [add_binding] will
+ 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..size]} of size char. *)
+let char_location loc 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)
+ ~rem:Int.zero ~modu:size_char
+ in
+ let loc = Location_Bits.shift shift loc in
+ make_loc loc (Int_Base.inject size_char)
+
+let compute_memcpy ~dst_lval ~dst ~src ~size state =
+ let size_min, size_max = min_max_size size in
+ (* Empty \from dependencies and sure output *)
+ let empty_deps = Assigns.Memory.empty, Zone.bottom in
+ (* First step: copy the bits we are sure to copy, i.e. for the minimum size
+ [size_min] if it is not zero. *)
+ let state, (deps_table, written_zone) =
+ if Int.gt size_min Int.zero
+ then
+ let state =
+ copy_offsetmap ~exact:true ~size:size_min ~src ~dst ~dst_lval state
+ in
+ (* If the copy succeeded, update \from dependencies and sure output. *)
+ if Cvalue.Model.is_reachable state
+ then state, add_sure_deps ~size:size_min ~src ~dst empty_deps
+ else state, empty_deps
+ else state, empty_deps
+ in
+ (* Stop here if the first copy failed or if there is nothing more to copy. *)
+ if not (Cvalue.Model.is_reachable state) || Int.equal size_min size_max
+ then state, deps_table, written_zone
+ else
+ (* Second step: size is imprecise, we will now copy some bits that we are
+ not sure to copy, for all possible sizes greater than [size_min]. *)
+ (* [size_min] bits have already been copied. *)
+ let src_shift, dst_shift, size_diff = shift ~factor:size_min src dst size_max in
+ (* Remaining locations to be read/written, as locations of char size. *)
+ let src_loc = char_location src_shift size_diff
+ and dst_loc = char_location dst_shift size_diff in
+ let deps_table = add_deps_loc ~exact:false ~src_loc ~dst_loc deps_table in
+ (* If there is sufficiently few possible sizes, iter on each possible size
+ via [copy_remaining_size_by_size]. Otherwise, use [imprecise_copy] in one
+ step to read the entire range src+(size_min..size_max-1) as one byte, and
+ write the result as one byte in dst+(size_min..size_max-1). *)
+ let state =
+ if Ival.cardinal_is_less_than size (plevel () / 10)
+ then copy_remaining_size_by_size ~src ~dst ~dst_lval ~size state
+ else imprecise_copy ~src_loc ~dst_loc ~dst_lval state
+ in
+ state, deps_table, written_zone
-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 frama_c_memcpy _name state actuals =
+ match actuals with
+ | [(dst_exp, dst_cvalue); (_src_exp, src_cvalue); (_size_exp, size_cvalue)] ->
+ let dst_lval = lval_of_address dst_exp in
let size =
- try Cvalue.V.project_ival size
+ try Cvalue.V.project_ival size_cvalue
with Cvalue.V.Not_based_on_null -> Ival.top (* TODO: use size_t *)
in
- let min,max = Ival.min_and_max size in
- let min = match min with None -> Int.zero | Some m -> Int.max m Int.zero in
- let char_bits = Bit_utils.sizeofchar() in
- let size_min = Int.mul char_bits min in
- let src = loc_bytes_to_loc_bits src_bytes in
- let dst = loc_bytes_to_loc_bits dst_bytes in
- (* Remove read-only destinations *)
- let dst_bits =
+ (* Convert locations and size into bits. *)
+ let size = Ival.scale (Bit_utils.sizeofchar ()) size in
+ let src = loc_bytes_to_loc_bits src_cvalue in
+ let dst = loc_bytes_to_loc_bits dst_cvalue in
+ (* Remove read-only destinations. *)
+ let dst =
Location_Bits.filter_base (fun b -> not (Base.is_read_only b)) dst
in
- let deps_return = deps_nth_arg 0 in
- let empty_cfrom =
- Assigns.{ memory = Memory.empty; return = deps_return }
+ (* Do the copy. *)
+ let state, memory, sure_output =
+ compute_memcpy ~dst_lval ~dst ~src ~size state
in
- let precise_copy state =
- (* First step: copy the bytes we are sure to copy *)
- if Int.gt size_min Int.zero then begin
- match Cvalue.Model.copy_offsetmap src size_min state with
- | `Bottom -> (* Read failed. Source was invalid, but must be read, we
- stop the analysis *)
- raise (Memcpy_result (Cvalue.Model.bottom,empty_cfrom,Zone.bottom))
- | `Value offsetmap ->
- let loc_dst = make_loc dst_bits (Int_Base.inject size_min) in
- 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
- in
- let (deps_table, sure_zone) =
- let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
- let zone_src = enumerate_valid_bits Locations.Read loc_src in
- let deps = Deps.data zone_src in
- (* Note: actually a part may be written for sure (if the
- difference between the offsets in loc_dst is smaller
- than size), but keeping it imprecise reflects more the
- imprecision of the value analysis here. *)
- let exact = Location_Bits.cardinal_zero_or_one dst_bits in
- let deps_table =
- Assigns.Memory.add_binding ~exact
- Assigns.Memory.empty zone_dst deps
- in
- let sure_zone = if exact then zone_dst else Zone.bottom in
- (deps_table, sure_zone)
- in
- new_state, deps_table, sure_zone
- end
- else (* Nothing certain can be copied *)
- (state, Assigns.Memory.empty, Zone.bottom)
- in
- let imprecise_copy new_state precise_assigns sure_zone =
- (* Second step. Size is imprecise, we will now copy some bits
- that we are not sure to copy *)
- let size_min_ival = Ival.inject_singleton size_min in
- let dst = Location_Bits.shift size_min_ival dst_bits in
- let src = Location_Bits.shift size_min_ival src in
- (* Size remaining to copy imprecisely *)
- let diff = match max with
- | Some max -> Some (Int.mul char_bits (Int.pred (Int.sub max min)))
- | None -> None
- in
- (* Imprecise locations remaining to be read/written. By using ranges
- modulo char_bits, we read and write byte-by-byte, which can preserve
- some precision in the fallback. If sufficiently few sizes need
- to be copied, we use a more precise method (see do_size below).
- However, in all cases, those locations are used to compute the
- read and written bits. *)
- let range =
- Ival.inject_interval ~min:(Some Int.zero) ~max:diff
- ~rem:Int.zero ~modu:char_bits
- in
- let size_char = Int_Base.inject char_bits in
- let loc_src = make_loc (Location_Bits.shift range src) size_char in
- let loc_dst = make_loc (Location_Bits.shift range dst) size_char in
- let c_from =
- let zone_src = enumerate_valid_bits Locations.Read loc_src in
- let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
- let deps = Deps.data zone_src in
- let memory =
- Assigns.Memory.add_binding ~exact:false precise_assigns zone_dst deps
- in
- Assigns.{ memory; return = deps_return }
- in
- try
- (* We try to iter on all the slices inside the value of slice.
- If there are more too many of them, we use a backup solution *)
- ignore (Ival.cardinal_less_than size (plevel / 10));
- let do_size s (dst, src, prev_size, state) =
- let s = Int.mul char_bits s in
- let diff = Int.sub s prev_size in
- if Int.equal s size_min then
- (* occurs the very first time. This copy has already been
- performed at the beginning, skip *)
- (dst, src, s, state)
- else begin
- (* Copy data between prev_size and s *)
- match Cvalue.Model.copy_offsetmap src diff state with
- | `Bottom ->
- (* This size is completely invalid. The following ones
- will also be invalid, stop now with current result *)
- 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
- in
- if Cvalue.Model.is_reachable new_state then
- let diffi = Ival.inject_singleton diff in
- let dst = Location_Bits.shift diffi dst in
- let src = Location_Bits.shift diffi src in
- (dst, src, s, new_state)
- else (* As above, invalid size, this time for the destination.
- We stop there *)
- raise (Memcpy_result (state,c_from,sure_zone))
- end
- in
- let _, _, _, state =
- Ival.fold_int do_size size (dst, src, Int.zero, new_state)
- in
- raise (Memcpy_result (state,c_from,sure_zone))
- with
- | Abstract_interp.Not_less_than ->
- Self.debug ~dkey ~once:true
- ~current:true "In memcpy builtin: too many sizes to enumerate, \
- possible loss of precision";
- (* Too many slices in the size. We read the entire range
- src+(size_min..size_max-1) in one step, as one byte, and write the
- result as one byte in dst+(size_min..size_max-1) *)
- let v = (* conflate_bottom=false: we want to copy padding bits *)
- Model.find_indeterminate ~conflate_bottom:false state loc_src
- in
- begin match v with
- | V_Or_Uninitialized.C_init_noesc _ -> ()
- | _ -> Self.result ~dkey ~current:true ~once:true
- "@[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
- in
- (* Beware that all the imprecise sizes may be invalid, in which case
- [add_binding] will return [Bottom]. In this case, return the
- previously computed state *)
- if Model.is_reachable updated_state then
- raise (Memcpy_result (updated_state,c_from,sure_zone))
- else
- raise (Memcpy_result (new_state,c_from,sure_zone))
- in
- try
- if Ival.is_zero size then
- raise (Memcpy_result (state, empty_cfrom, Zone.bottom));
- let (precise_state,precise_assigns,sure_zone) = precise_copy state in
- if Option.fold ~none:false ~some:(Int.equal min) max then
- begin
- let c_assigns =
- Assigns.{ memory = precise_assigns; return = deps_return }
- in
- raise (Memcpy_result (precise_state, c_assigns, sure_zone))
- end;
- imprecise_copy precise_state precise_assigns sure_zone
- with
- | Memcpy_result (new_state,c_assigns,sure_zone) ->
- if Model.is_reachable new_state then
- (* Copy at least partially succeeded (with perhaps an
- alarm for some of the sizes *)
- Builtins.Full
- { Builtins.c_values = [Some dst_bytes, new_state];
- c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
- c_assigns = Some (c_assigns, sure_zone); }
+ (* Build the builtin results. *)
+ let return = deps_nth_arg 0 in
+ let froms = Assigns.{ memory; return } in
+ let c_assigns = Some (froms, sure_output) in
+ let return, c_clobbered =
+ if Model.is_reachable state then
+ (* Copy at least partially succeeded *)
+ Some dst_cvalue, Builtins.clobbered_set_from_ret state dst_cvalue
else
- Builtins.Full
- { Builtins.c_values = [ None, Cvalue.Model.bottom];
- c_clobbered = Base.SetLattice.bottom;
- c_assigns = Some (c_assigns, sure_zone); }
- in
- match actuals with
- | [dst; src; size] -> compute dst src size
+ None, Base.SetLattice.bottom
+ in
+ Builtins.Full { c_values = [ return, state ]; c_clobbered; c_assigns }
| _ -> raise (Builtins.Invalid_nb_of_args 3)
let () =
register_builtin ~replace:"memcpy" "Frama_C_memcpy" (frama_c_memcpy "memcpy");
register_builtin ~replace:"memmove" "Frama_C_memmove" (frama_c_memcpy "memmove")
+(* -------------------------------------------------------------------------- *)
+(* Memset *)
+(* -------------------------------------------------------------------------- *)
+
(* Implementation of [memset] that accepts imprecise arguments. *)
let frama_c_memset_imprecise state dst_lval dst v size =
let prefix = "Builtin memset" in
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 1559794a477915a5ad20d5b9232252094712ec3f..8672dfccee497d309e2305e7817f1c99ff5c318a 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -220,7 +220,7 @@
[eva] memcpy.c:172: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:172: function memcpy: precondition 'separation' got status valid.
[eva:imprecision] memcpy.c:172:
- In memcpy builtin: precise copy of indeterminate values UNINITIALIZED
+ In memcpy builtin: precise copy of indeterminate values.
[eva] memcpy.c:173: assertion got status valid.
[eva] computing for function itv <- main_uninit <- main_all.
Called from memcpy.c:174.
@@ -233,7 +233,7 @@
[eva:imprecision] memcpy.c:174:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:174:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva] memcpy.c:175: assertion got status valid.
[eva] computing for function make_unknown <- main_uninit <- main_all.
Called from memcpy.c:178.
@@ -255,7 +255,7 @@
[eva:imprecision] memcpy.c:181:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:181:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva:alarm] memcpy.c:182: Warning:
accessing uninitialized left-value. assert \initialized(&b[11]);
[eva] computing for function make_unknown <- main_uninit <- main_all.
@@ -267,7 +267,7 @@
[eva] memcpy.c:187: function memcpy: precondition 'valid_src' got status valid.
[eva] memcpy.c:187: function memcpy: precondition 'separation' got status valid.
[eva:imprecision] memcpy.c:187:
- In memcpy builtin: precise copy of indeterminate values UNINITIALIZED
+ In memcpy builtin: precise copy of indeterminate values.
[eva] memcpy.c:188: assertion got status valid.
[eva] computing for function itv <- main_uninit <- main_all.
Called from memcpy.c:190.
@@ -279,7 +279,7 @@
[eva:imprecision] memcpy.c:190:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:190:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva] memcpy.c:191: assertion got status valid.
[eva:alarm] memcpy.c:192: Warning:
accessing uninitialized left-value. assert \initialized(&b[8]);
@@ -306,7 +306,7 @@
[eva:imprecision] memcpy.c:200:
In memcpy builtin: too many sizes to enumerate, possible loss of precision
[eva:imprecision] memcpy.c:200:
- In memcpy builtin: imprecise copy of indeterminate values
+ In memcpy builtin: imprecise copy of indeterminate values.
[eva:alarm] memcpy.c:201: Warning:
accessing uninitialized left-value. assert \initialized(&b[11]);
[eva] Recording results for main_uninit