From ff4cd3b7e2525a1dcf552f44c74dac10304e7357 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 8 Jan 2019 10:49:55 +0100
Subject: [PATCH] [Inout] Avoids folding implicit zero-initializers of large
arrays.
Fixes a performance issue.
---
src/plugins/inout/cumulative_analysis.ml | 12 ++++++++++++
src/plugins/inout/cumulative_analysis.mli | 4 ++++
src/plugins/inout/inputs.ml | 4 +++-
src/plugins/inout/operational_inputs.ml | 16 +++++++++++-----
src/plugins/inout/outputs.ml | 17 +++++++++++++----
5 files changed, 43 insertions(+), 10 deletions(-)
diff --git a/src/plugins/inout/cumulative_analysis.ml b/src/plugins/inout/cumulative_analysis.ml
index ca86a013946..9bdb2f6624b 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 78448372050..e5af1ddfa41 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 2819a6864d3..96edd8a1f3d 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 d4d164bb0b3..1c070d2ddf9 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 35e15968f18..67ff63012dc 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
--
GitLab