diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 0f49ea6243172b8b95ab56568df92361f2e7723f..ea103a92baa5bd002f4c8377783de31e6a8dcf48 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -463,7 +463,6 @@ struct
let init = Cil.is_mutable_or_initialized lv in
transfer_assign stmt ~init lv comp_vars state
| Local_init(v, AssignInit i, _) ->
- let implicit = true in
let rec aux lv i acc =
let doinit o i _ state = aux (Cil.addOffsetLval o lv) i state in
match i with
@@ -471,7 +470,21 @@ struct
let comp_vars = find stmt acc.deps_table e in
transfer_assign stmt ~init:true lv comp_vars acc
| CompoundInit (ct, initl) ->
- Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc
+ (* To avoid a performance issue, do not fold implicit initializers
+ of scalar or large arrays. We still use implicit initializers
+ for small struct arrays, as this may be more precise in case of
+ padding bits. The 100 limit is arbitrary. *)
+ let implicit =
+ not (Cil.isArrayType ct &&
+ (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem ct)
+ || Ast_info.array_size ct > (Integer.of_int 100)))
+ in
+ let r = Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc in
+ if implicit then r else
+ (* If implicit zero-initializers have been skipped, also mark
+ the entire array as initialized from no dependency (nothing
+ is read by the implicit zero-initializers). *)
+ transfer_assign stmt ~init:true lv Function_Froms.Deps.bottom r
in
aux (Cil.var v) i state
| Call (lvaloption,funcexp,argl,loc) ->
diff --git a/src/plugins/inout/cumulative_analysis.ml b/src/plugins/inout/cumulative_analysis.ml
index ca86a013946ae195cc20b412acad4dbb69ecfe87..9bdb2f6624b8bea5f4e4408dd01a1932040ddf66 100644
--- a/src/plugins/inout/cumulative_analysis.ml
+++ b/src/plugins/inout/cumulative_analysis.ml
@@ -23,6 +23,18 @@
open Cil_types
open Visitor
+(* To avoid a performance issue, do not fold implicit zero-initializers of large
+ arrays. For arrays of scalar elements, the outputs of an initializer is
+ exactly the zone covered by the array. For arrays containing structs with
+ padding bits, this is an over-approximation, so we prefer folding the
+ initializer if the array is not too big (the 100 cells limit is arbitrary).
+ We still need to fold the explicit initializers to collect the inputs. *)
+let fold_implicit_initializer typ =
+ not
+ (Cil.isArrayType typ &&
+ (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem typ)
+ || Ast_info.array_size typ > (Integer.of_int 100)))
+
let specialize_state_on_call ?stmt kf =
match stmt with
| Some ({ skind = Instr (Call (_, _, l, _)) } as stmt) ->
diff --git a/src/plugins/inout/cumulative_analysis.mli b/src/plugins/inout/cumulative_analysis.mli
index 7844837205097c48d1c9ee32e21a0776190d9f29..e5af1ddfa41fab99734f0049b4530e6d15506ab5 100644
--- a/src/plugins/inout/cumulative_analysis.mli
+++ b/src/plugins/inout/cumulative_analysis.mli
@@ -32,6 +32,10 @@ open Cil_types
can be gathered using a Cil visitor).
*)
+(** Should implicit zero-initializers for [typ] be folded? False for big arrays
+ to avoid a performance issue. *)
+val fold_implicit_initializer: typ -> bool
+
val specialize_state_on_call: ?stmt:stmt -> kernel_function -> Db.Value.state
(** If the given statement is a call to the given function,
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index 2819a6864d3f9c3bc155efdc1e2cdad6f51cc583..96edd8a1f3d90ca3a1f58fa736851f62936a3c00 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -96,7 +96,9 @@ class virtual do_it_ = object(self)
self#do_assign lv;
ignore (visitFramacExpr (self:>frama_c_visitor) e)
| CompoundInit (ct,initl) ->
- let implicit = true in
+ (* No need to consider implicit zero-initializers, for which
+ nothing is read. *)
+ let implicit = false in
let doinit o i _ () =
ignore (visitFramacOffset (self:>frama_c_visitor) o);
aux (Cil.addOffsetLval o lv) i
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d4d164bb0b37dccd90e04f2e1b947063c557bf93..1c070d2ddf96a72f356d251e2394de36da5f4ced 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -283,7 +283,6 @@ end) = struct
let new_inputs = Zone.diff inputs data.under_outputs_d in
store_non_terminating_inputs new_inputs;
{data with over_inputs_d = Zone.join data.over_inputs_d new_inputs}
- ;;
(* Initialized const variables should be included as outputs of the function,
so [for_writing] must be false for local initializations. It should be
@@ -302,8 +301,8 @@ end) = struct
Add it into the under-approximated outputs. *)
Zone.link data.under_outputs_d new_outs
else data.under_outputs_d
- in {
- under_outputs_d = new_sure_outs;
+ in
+ { under_outputs_d = new_sure_outs;
over_inputs_d = Zone.join data.over_inputs_d new_inputs;
over_outputs_d = Zone.join data.over_outputs_d new_outs }
@@ -372,9 +371,16 @@ end) = struct
let e_inputs = !Db.From.find_deps_no_transitivity_state state e in
add_out ~for_writing:false state lv e_inputs acc
| CompoundInit(ct, initl) ->
- let implicit = true in
+ (* Avoid folding implicit zero-initializer of large arrays. *)
+ let implicit = Cumulative_analysis.fold_implicit_initializer ct in
let doinit o i _ data = aux (Cil.addOffsetLval o lv) i data in
- Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc
+ let data = Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc in
+ if implicit then data else
+ (* If the implicit zero-initializers hade been skipped, add the
+ zone of the array as outputs. It is exactly the written zone for
+ arrays of scalar elements. Nothing is read by zero-initializers,
+ so the inputs are empty. *)
+ add_out ~for_writing:false state lv Zone.bottom acc
in
aux (Cil.var v) i data
| Call (lvaloption,funcexp,argl,loc) ->
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 35e15968f181dfbce0c2683dd9af346f27e776a0..67ff63012dcd01968c5414adaac3dd6e63d0c47b 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -89,10 +89,19 @@ class virtual do_it_ = object(self)
let rec aux lv = function
| SingleInit _ -> self#do_assign ~for_writing:false lv
| CompoundInit (ct, initl) ->
- let implicit = true in
- let doinit o i _ () = aux (Cil.addOffsetLval o lv) i in
- Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc:()
- in aux (Cil.var v) i
+ (* Avoid folding the implicit zero-initializers of large arrays. *)
+ if Cumulative_analysis.fold_implicit_initializer ct
+ then
+ let implicit = true in
+ let doinit o i _ () = aux (Cil.addOffsetLval o lv) i in
+ Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc:()
+ else
+ (* For arrays of scalar elements, all the zone covered by the
+ array is written. For arrays of structs containing padding
+ bits, this is a sound over-approximation. *)
+ self#do_assign ~for_writing:false lv
+ in
+ aux (Cil.var v) i
| Local_init (v, ConsInit(f, _, _),_) ->
let state = Db.Value.get_state self#current_kinstr in
if Cvalue.Model.is_top state then self#join Zone.top