[e-acsl:archi] addressing Michele's comments

src/kernel_services/ast_data/kernel_function.ml

@@ -570,7 +570,8 @@ let is_return_stmt kf stmt =
   try
     let return = find_return kf in
     Stmt.equal stmt return
-  with No_Statement -> false
+  with No_Statement ->
+    false
 
 let is_entry_point kf =
   let main, _ = Globals.entry_point () in

src/plugins/e-acsl/src/code_generator/at_with_lscope.ml

@@ -263,7 +263,7 @@ let to_exp ~loc kf env pot label =
           Constructor.mk_lib_call ~loc
             ~result:(Cil.var vi)
             "malloc"
-            [e_size]
+            [ e_size ]
         in
         malloc_stmt
       | Typing.(C_integer _ | C_float _ | Gmpz) ->

src/plugins/e-acsl/src/code_generator/constructor.ml

@@ -82,7 +82,7 @@ let mk_lib_call ~loc ?result fname args =
       ty_params
       args
   in
-  let args = match vi.vtype with
+  let args = match Cil.unrollType vi.vtype with
     | TFun(_, Some params, _, _) -> make_args args params
     | TFun(_, None, _, _) -> []
     | _ -> assert false
@@ -122,12 +122,18 @@ let mk_named_store_stmt name ?str_size vi =
   | TPtr(TInt(IChar, _), _), Some size ->
     store [ Cil.evar ~loc vi ; size ]
   | TPtr _, Some size ->
-    (* a VLA that has been converted to a pointer by the kernel *)
+    (* a VLA that has been converted into a pointer by the kernel *)
     store [ Cil.evar ~loc vi; size ]
   | _, None ->
     store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
-  | _, Some _ ->
-    assert false
+  | _, Some size ->
+    Options.fatal
+      "unexpected types for arguments of function '%s': \
+      %s got type %a, while representing a memory block of %a bytes"
+      name
+      vi.vname
+      Printer.pp_typ ty
+      Printer.pp_exp size
 
 let mk_store_stmt ?str_size vi =
   mk_named_store_stmt "store_block" ?str_size vi
@@ -154,7 +160,9 @@ let mk_runtime_check ?(reverse=false) kind kf e p =
   in
   let line = (fst loc).Filepath.pos_lnum in
   let e =
-    if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
+    if reverse
+    then e
+    else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
   in
   mk_rtl_call ~loc
     "assert"

src/plugins/e-acsl/src/code_generator/env.ml

@@ -318,7 +318,8 @@ let emitter =
     ~correctness:[ Options.Gmp_only.parameter ]
     ~tuning:[]
 
-let add_assert kf stmt annot = Annotations.add_assert emitter ~kf stmt annot
+let add_assert kf stmt annot =
+  Annotations.add_assert emitter ~kf stmt annot
 
 let add_stmt ?(post=false) ?before env kf stmt =
   if not post then

src/plugins/e-acsl/src/code_generator/global_observer.ml

@@ -54,7 +54,8 @@ let add_initializer vi offset init =
       Options.fatal "variable %a is not monitored" Printer.pp_varinfo vi
 
 let rec literal_in_initializer env kf = function
-  | SingleInit exp -> snd (Literal_observer.exp_in_depth env kf exp)
+  | SingleInit exp ->
+    snd (Literal_observer.subst_all_literals_in_exp env kf exp)
   | CompoundInit (_, l) ->
     List.fold_left (fun env (_, i) -> literal_in_initializer env kf i) env l
 
@@ -69,7 +70,7 @@ let mk_init_function () =
   vi.vdefined <- true;
   (* There is no contract associated with the function *)
   let spec = Cil.empty_funspec () in
-  (* Create function definition which no stmt yet: they will be added
+  (* Create function definition with no stmt yet: they will be added
      afterwards *)
   let blk = Cil.mkBlock [] in
   let fundec =
@@ -134,7 +135,7 @@ let mk_init_function () =
          :: stmts)
       stmts
   in
-  (* Create a new code block with generated statements *)
+  (* create a new code block with generated statements *)
   let b, stmts = match stmts with
     | [] -> assert false
     | stmt :: stmts ->
@@ -142,7 +143,7 @@ let mk_init_function () =
       b, stmts
   in
   let stmts = Cil.mkStmt ~valid_sid:true (Block b) :: stmts in
-  (* Prevent multiple calls to globals_init *)
+  (* prevent multiple calls to [__e_acsl_globals_init] *)
   let loc = Location.unknown in
   let vi_already_run =
     Cil.makeLocalVar

src/plugins/e-acsl/src/code_generator/global_observer.mli

@@ -25,23 +25,24 @@
 open Cil_types
 
 val function_name: string
-(** name of the function in which [mk_init] generates the code *)
+(** Name of the function in which [mk_init_function] (see below) generates the
+ ** code. *)
 
 val reset: unit -> unit
 val is_empty: unit -> bool
 
 val add: varinfo -> unit
-(** observes the given variable if necessary *)
+(** Observes the given variable if necessary. *)
 
 val add_initializer: varinfo -> offset -> init -> unit
-(** add the initializer for the given observed variable *)
+(** Add the initializer for the given observed variable. *)
 
 val mk_init_function: unit -> varinfo * fundec
-(** generates a new C function containing the observers for global variable
-     declaration and initialization *)
+(** Generates a new C function containing the observers for global variable
+    declarations and initializations. *)
 
 val mk_delete_stmts: stmt list -> stmt list
-(** generates the observers for global variable de-allocation *)
+(** Generates the observers for global variable de-allocations. *)
 
 (*
 Local Variables:

src/plugins/e-acsl/src/code_generator/gmp.ml

@@ -94,14 +94,14 @@ let init_set ~loc lv ev e =
       assert (Gmp_types.Z.is_t (Cil.typeOf ev));
       let call =
         Constructor.mk_lib_call ~loc
-        "__gmpz_import"
-        [ ev;
-          Cil.one ~loc;
-          Cil.one ~loc;
-          Cil.sizeOf ~loc (TInt(IULongLong, []));
-          Cil.zero ~loc;
-          Cil.zero ~loc;
-          Cil.mkAddrOf ~loc elv ]
+          "__gmpz_import"
+          [ ev;
+            Cil.one ~loc;
+            Cil.one ~loc;
+            Cil.sizeOf ~loc (TInt(IULongLong, []));
+            Cil.zero ~loc;
+            Cil.zero ~loc;
+            Cil.mkAddrOf ~loc elv ]
       in
       Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ init ~loc ev; call ]))
     | _ ->

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -35,7 +35,7 @@ let replace_literal_string_in_exp env kf_opt (* None for globals *) e =
      replace literal strings elsewhere *)
   match kf_opt with
   | None -> e, env
-  | Some kf -> Literal_observer.exp_in_depth env kf e
+  | Some kf -> Literal_observer.subst_all_literals_in_exp env kf e
 
 let rec inject_in_init env kf_opt vi off = function
   | SingleInit e as init ->
@@ -466,11 +466,16 @@ and inject_in_block (env: Env.t) kf blk =
       blk.bstmts
   in
   blk.bstmts <- List.rev stmts;
+  (* now inject code that de-allocate the necessary observation variables and
+     blocks of the runtime memory that have been previously allocated *)
+  (* calls to [free] for de-allocating variables observing \at(_,_) *)
   let free_stmts = At_with_lscope.Free.find_all kf in
   match blk.blocals, free_stmts with
   | [], [] ->
     env
   | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
+    (* [TODO] this piece of code could be improved *)
+    (* de-allocate the memory blocks observing locals *)
     let add_locals stmts =
       if Functions.instrument kf then
         List.fold_left
@@ -483,6 +488,7 @@ and inject_in_block (env: Env.t) kf blk =
       else
         stmts
     in
+    (* select the precise location to inject these pieces of code *)
     let rec insert_in_innermost_last_block blk = function
       | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
         (* keep the return (enclosed in a generated block) at the end;
@@ -657,21 +663,21 @@ let inject_global_initializer file main =
          [main] *)
       main.sbody.bstmts <- stmt :: main.sbody.bstmts;
       let new_globals =
-        List.fold_right
-          (fun g acc -> match g with
+        List.fold_left
+          (fun acc g -> match g with
              | GFun({ svar = vi }, _)
                when Varinfo.equal vi main.svar ->
                acc
              | _ -> g :: acc)
-          file.globals
           [ cil_fct; GFun(main, Location.unknown) ]
+          file.globals
       in
+      let new_globals = List.rev new_globals in
       (* add the literal string varinfos as the very first
          globals *)
       let new_globals =
         Literal_strings.fold
-          (fun _ vi l ->
-             GVar(vi, { init = None }, Location.unknown) :: l)
+          (fun _ vi l -> GVar(vi, { init = None }, Location.unknown) :: l)
           new_globals
       in
       file.globals <- new_globals
@@ -691,7 +697,7 @@ let inject_mmodel_initializer main =
   let nulls = [ Cil.zero loc ; Cil.zero loc ] in
   let handle_main main =
     let args =
-      (* record arguments only if the second has a pointer type, so a argument
+      (* record arguments only if the second has a pointer type, so argument
          strings can be recorded. This is sufficient to capture C99 compliant
          arguments and GCC extensions with environ. *)
       match main.sformals with
@@ -725,14 +731,20 @@ let inject_in_file file =
   inject_mmodel_initializer main
 
 let reset_all ast =
+  (* by default, do not run E-ACSL on the generated code *)
   Options.Run.off ();
+  (* reset all the E-ACSL environments to their original states *)
   Misc.reset ();
   Logic_functions.reset ();
   Literal_strings.reset ();
   Global_observer.reset ();
   Typing.clear ();
+  (* reset some kernel states: *)
+  (* reset the CFG that has been heavily modified by the code generation step *)
   Cfg.clearFileCFG ~clear_id:false ast;
   Cfg.computeFileCFG ast;
+  (* notify the kernel that new code has been generated (but we have kept the
+     old one) *)
   Ast.mark_as_grown ()
 
 let inject () =

src/plugins/e-acsl/src/code_generator/literal_observer.ml

@@ -43,7 +43,7 @@ let literal loc env kf s =
     Literal_strings.add s vi;
     exp, env
 
-let exp_in_depth env kf e =
+let subst_all_literals_in_exp env kf e =
   let env_ref = ref env in
   let o = object
     inherit Cil.genericCilVisitor (Visitor_behavior.copy (Project.current ()))
@@ -64,6 +64,6 @@ let exp_in_depth env kf e =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/code_generator/literal_observer.mli

@@ -24,12 +24,12 @@
 
 open Cil_types
 
-val exp_in_depth: Env.t -> kernel_function -> exp -> exp * Env.t
-(** replace any sub-expression of the given exp that is a literal string by an
-     observed variable   *)
+val subst_all_literals_in_exp: Env.t -> kernel_function -> exp -> exp * Env.t
+(** Replace any sub-expression of the given exp that is a literal string by an
+    observed variable. *)
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/code_generator/loops.mli

@@ -30,8 +30,8 @@ open Cil_types
 
 val preserve_invariant:
   Env.t -> Kernel_function.t -> stmt -> stmt * Env.t
-(** modify the given stmt loop to insert the code which preserves its loop
-    invariants. Also return the modify environment. *)
+(** Modify the given stmt loop to insert the code which preserves its loop
+    invariants. Also return the modified environment. *)
 
 (**************************************************************************)
 (**************************** Nested loops ********************************)

src/plugins/e-acsl/src/libraries/misc.ml

@@ -49,7 +49,7 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
 let is_fc_or_compiler_builtin vi =
   Cil.is_builtin vi
   ||
-  (String.length vi.vname >= 10
+  (String.length vi.vname > 10 (* number of characters in "__builtin_" *)
    &&
    let prefix = String.sub vi.vname 0 10 in
    Datatype.String.equal prefix "__builtin_")

src/plugins/e-acsl/src/main.ml

@@ -61,8 +61,8 @@ let unmemoized_extend_ast () =
   if Ast.is_computed () then begin
     (* do not modify the existing project: work on a copy.
        Must also extend the current AST with the E-ACSL's library files. *)
-    Options.feedback ~level:2 "AST already computed: \
-E-ACSL is going to work on a copy.";
+    Options.feedback ~level:2
+      "AST already computed: E-ACSL is going to work on a copy.";
     let name = Project.get_name (Project.current ()) in
     let tmpfile =
       Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
@@ -139,7 +139,8 @@ let generate_code =
             Temporal.enable (Options.Temporal_validity.get ());
             let prepared_prj = Prepare_ast.prepare () in
             let res =
-              Project.on prepared_prj
+              Project.on
+                prepared_prj
                 (fun () ->
                    let dup_prj = Dup_functions.dup () in
                    let copied_prj =