Merge branch 'fix/inout/array-init' into 'master'

[Inout] Avoids folding implicit zero-initializers of large arrays.

See merge request frama-c/frama-c!2105

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) ->

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) ->

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,

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

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) ->

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