MR !151 Review: address reviewer's comments

src/plugins/e-acsl/prepare_ast.ml

@@ -50,28 +50,26 @@ let sufficiently_aligned attrs algn =
       should not happen really *)
       assert false
     | _ -> acc
-  ) 0 attrs in
-  if alignment > 0 then true else false
+  ) 0 attrs in alignment > 0
 
 (* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
  * true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
  * of [algn] (i.e., less than [algn] bytes and has no alignment attribute *)
 let require_alignment typ attrs algn =
-  if (Cil.bitsSizeOf typ) < algn*8 && not (sufficiently_aligned attrs algn) then
-    true
-  else
-    false
+  Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
 
 class prepare_visitor prj = object (_)
   inherit Visitor.frama_c_copy prj
 
   (* Add align attributes to local variables (required by temporal analysis) *)
   method !vblock _ =
-    if (Temporal.is_enabled ()) then
+    if Temporal.is_enabled () then
       Cil.DoChildrenPost (fun blk ->
         List.iter (fun vi ->
+        (* 4 bytes alignment is required to allow sufficient space for storage
+           of 32-bit timestamps in a 1:1 shadow. *)
           if require_alignment vi.vtype vi.vattr 4; then begin
-            vi.vattr <- Attr("aligned",[AInt(Integer.four)]) :: vi.vattr
+            vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
           end)
         blk.blocals;
       blk)

src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c

@@ -105,8 +105,8 @@ static void describe_run();
 # error "No E-ACSL memory model defined. Aborting compilation"
 #endif
 
-/* Temporal analysis shared by both models.
- * Uses macros differently defined macros */
+/* This header contains temporal analysis shared by both models.
+   It should be here as it uses differently defined macros */
 #include "e_acsl_temporal.h"
 
 #ifdef E_ACSL_WEAK_VALIDITY

src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h

@@ -51,9 +51,11 @@ static uint32_t temporal_timestamp = 2;
 
 struct temporal_parameter {
   void *ptr;
+  /* Number all members such that there is no `0` which potentially
+     corresponds to an invalid number */
   enum {
     TBlockN = 10,
-    TReferentN = 20,
+    TReferentN  = 20,
     TCopy = 30
   } temporal_flow;
 };

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h

@@ -1234,7 +1234,7 @@ static int heap_initialized(uintptr_t addr, long len) {
 #ifdef E_ACSL_TEMPORAL
 static uint32_t heap_temporal_info(uintptr_t addr, int origin) {
   /* NOTE: No checking for allocated blocks, since an invalid
-     timestamp is zero and ununsed memory is nullified then an invalid
+     timestamp is zero and unused memory is nullified then an invalid
      timestamp is also returned for allocated memory */
   if (origin) {
     uintptr_t *aligned_shadow = (uintptr_t*)ALIGNED_HEAP_SHADOW(addr);

src/plugins/e-acsl/temporal.mli

@@ -20,6 +20,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Transformations to detect temporal memory errors (e.g., derererence of
+    stale pointers). Detailed description of the transformations is presented
+    in Sections 2 and 3 of the RV'17 paper "Runtime Detection of Temporal Memory
+    Errors" by K. Vorobyov, N. Kosmatov, J Signoles and A. Jakobsson.
+*)
+
 val enable: bool -> unit
 (** Enable/disable temporal transformations *)
 
@@ -28,7 +34,10 @@ val is_enabled: unit -> bool
 
 val handle_arguments: Cil_types.kernel_function -> Env.t -> Env.t
 (** Update local environment ([Env.t]) with statements allowing to track
-    referent numbers across function calls *)
+    referent numbers across calls function whose definitions are available.
+    This is such that whenever a function [f] is called (and a new stack
+    frame is created) [handle_arguments] generates statements that transfer
+    referent numbers stored in RTL to the new stack frame. *)
 
 val handle_stmt: Cil_types.stmt -> Env.t -> Env.t
 (** Update local environment ([Env.t]) with statements tracking temporal

src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c

+/* Generated by Frama-C */
+#include "stdint.h"
+#include "stdlib.h"
+int main(int argc, char **argv)
+{
+  int __retres;
+  char *p;
+  int *q;
+  __e_acsl_memory_init(& argc,& argv,(size_t)8);
+  __e_acsl_store_block((void *)(& q),(size_t)8);
+  __e_acsl_store_block((void *)(& p),(size_t)8);
+  uintptr_t addr = (unsigned long)(& argc);
+  __e_acsl_store_block((void *)(& addr),(size_t)8);
+  __e_acsl_full_init((void *)(& addr));
+  __e_acsl_temporal_store_nblock((void *)(& q),(void *)(& argc));
+  __e_acsl_full_init((void *)(& q));
+  q = & argc;
+  __e_acsl_temporal_store_nblock((void *)(& p),(void *)((char *)addr));
+  __e_acsl_full_init((void *)(& p));
+  p = (char *)addr;
+  __e_acsl_temporal_store_nblock((void *)(& p),(void *)0x123456);
+  __e_acsl_full_init((void *)(& p));
+  p = (char *)0x123456;
+  __e_acsl_temporal_store_nreferent((void *)(& p),(void *)(& q));
+  __e_acsl_full_init((void *)(& p));
+  p = (char *)q;
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& argc));
+  __e_acsl_delete_block((void *)(& q));
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_delete_block((void *)(& addr));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/temporal/t_addr-by-val.c

+/* run.config
+  COMMENT: Case when a pointer is taking address by value.
+*/
+
+#include <stdint.h>
+
+int main (int argc, char **argv) {
+  uintptr_t addr = (uintptr_t)&argc;
+  char *p;
+  int *q;
+  q = &argc;
+  /* Here the referent of p should be assigned from the value of addr */
+  p = (char*)addr;
+  p = (char*)0x123456;
+  p = (char*)q;
+}
+
+

src/plugins/e-acsl/visit.ml

@@ -206,6 +206,8 @@ class e_acsl_visitor prj generate = object (self)
                     :: stmts)
                   stmts
               in
+              let return =
+                Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown)) in
               (* Generate init statements for temporal analysis *)
               let tinit_stmts = Varinfo.Hashtbl.fold
                 (fun vi (off, init) acc ->
@@ -215,11 +217,9 @@ class e_acsl_visitor prj generate = object (self)
                       (match stmt with | Some stmt -> stmt :: acc | None -> acc)
                   | None -> acc)
                 global_vars
-                []
+                [return]
               in
-              let return =
-                Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown)) in
-              let stmts = stmts @ tinit_stmts @ [return] in
+              let stmts = stmts @ tinit_stmts in
               (* Create a new code block with generated statements *)
               let (b, env), stmts = match stmts with
                 | [] -> assert false
@@ -601,7 +601,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
           let env = Temporal.handle_stmt stmt env in
           (* Add initialization statements and store_block statements stemming
              from Local_init *)
-            self#add_initializers stmt env kf
+            self#handle_instructions stmt env kf
         else
           env
       in
@@ -727,47 +727,40 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     in
     Cil.ChangeDoChildrenPost(stmt, mk_block)
 
-  method private add_initializer loc ?vi lv ?(post=false) stmt env kf =
-    assert generate;
-    let may_safely_ignore = function
-      | Var vi, NoOffset -> vi.vglob || vi.vformal
-      | _ -> false
-    in
-    if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~kf lv then
-      let before = Cil.memo_stmt self#behavior stmt in
-      let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
-      let new_stmt = Cil.memo_stmt self#behavior new_stmt in
-      let env = Env.add_stmt ~post ~before env new_stmt in
-      let env = match vi with
-        | None -> env
-        | Some vi ->
-          let new_stmt = Project.on prj Misc.mk_store_stmt vi in
-          let new_stmt = Cil.memo_stmt self#behavior new_stmt in
-          Env.add_stmt ~post ~before env new_stmt
+  method private handle_instructions stmt env kf =
+    let add_initializer loc ?vi lv ?(post=false) stmt env kf =
+      assert generate;
+      let may_safely_ignore = function
+        | Var vi, NoOffset -> vi.vglob || vi.vformal
+        | _ -> false
       in
-      env
-    else
-      env
-
-  method private add_initializers stmt env kf =
-    let do_instr instr =
-      match instr with
-      | Set(lv, _, loc) ->
-        self#add_initializer loc lv stmt env kf
-      | Local_init(vi, _, loc) ->
-        let lv = (Var(vi), NoOffset) in
-        self#add_initializer loc ~vi lv ~post:true stmt env kf
-      | Call (Some lv, _, _, loc) ->
-        if not (Misc.is_generated_kf kf) then
-          self#add_initializer loc lv ~post:false stmt env kf
-        else env
-      | _ -> env
+      if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~stmt ~kf lv then
+        let before = Cil.memo_stmt self#behavior stmt in
+        let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
+        let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+        let env = Env.add_stmt ~post ~before env new_stmt in
+        let env = match vi with
+          | None -> env
+          | Some vi ->
+            let new_stmt = Project.on prj Misc.mk_store_stmt vi in
+            let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+            Env.add_stmt ~post ~before env new_stmt
+        in
+        env
+      else
+        env
     in
     match stmt.skind with
-    | Instr(i) -> do_instr i
+    | Instr(Set(lv, _, loc)) -> add_initializer loc lv stmt env kf
+    | Instr(Local_init(vi, _, loc)) ->
+      let lv = (Var(vi), NoOffset) in
+      add_initializer loc ~vi lv ~post:true stmt env kf
+    | Instr(Call (Some lv, _, _, loc)) ->
+      if not (Misc.is_generated_kf kf) then
+        add_initializer loc lv ~post:false stmt env kf
+      else env
     | _ -> env
 
-
   method !vblock blk =
     let handle_memory new_blk =
       match new_blk.blocals with