[wp] Do not copy volatile lvalues

src/plugins/wp/cfgWP.ml

@@ -709,15 +709,22 @@ struct
     obj , domain , seq , loc
 
   let cc_stored lv seq loc obj expr =
-    if Cil.isVolatileLval lv &&
-       Cvalues.volatile ~warn:"unsafe write-access to volatile l-value" ()
-    then None
+    let intercept_volatile kind lv =
+      let warn = "unsafe " ^ kind ^ "-access to volatile l-value" in
+      Cil.isVolatileLval lv && Cvalues.volatile ~warn ()
+    in
+    if intercept_volatile "write" lv then None
     else
       let value = match expr.enode with
-        | Lval lv -> M.copied seq obj loc (C.lval seq.pre lv)
-        | _ -> M.stored seq obj loc (C.val_of_exp seq.pre expr)
+        | Lval lv when not @@ intercept_volatile "read" lv ->
+            M.copied seq obj loc (C.lval seq.pre lv)
+        | _ ->
+            (* Note: a volatile lval will be compiled to an unknown value *)
+            M.stored seq obj loc (C.val_of_exp seq.pre expr)
       in
       let init = match expr.enode with
+        | Lval lv when intercept_volatile "read" lv ->
+            M.stored_init seq obj loc (Cvalues.initialized_obj obj)
         | Lval lv when Cil.(isStructOrUnionType @@ typeOfLval lv) ->
             M.copied_init seq obj loc (C.lval seq.pre lv)
         | _ ->

src/plugins/wp/tests/wp_plugin/oracle/volatile.0.res.oracle

@@ -2,11 +2,24 @@
 [kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function default_init
+------------------------------------------------------------
+
+Goal Check 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 46):
+Assume {
+  Type: is_sint8(ClientId_0) /\ is_sint32(R1_0).
+  (* Pre-condition *)
+  Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: R1_0 = 0.
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Function job_assigns
 ------------------------------------------------------------
 
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 15):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 16):
 Prove: w = 0.
 
 ------------------------------------------------------------
@@ -14,7 +27,7 @@ Prove: w = 0.
   Function job_read
 ------------------------------------------------------------
 
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 21):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 22):
 Assume { Type: is_sint32(x). }
 Prove: x = w.
 
@@ -23,7 +36,7 @@ Prove: x = w.
   Function job_struct
 ------------------------------------------------------------
 
-Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 29):
+Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 30):
 Prove: true.
 
 ------------------------------------------------------------
@@ -31,11 +44,11 @@ Prove: true.
   Function job_struct_assigns
 ------------------------------------------------------------
 
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 36):
 Prove: EqS1_st_v(w, w_1).
 
 ------------------------------------------------------------
-[wp] tests/wp_plugin/volatile.i:32: Warning: 
+[wp] tests/wp_plugin/volatile.i:33: Warning: 
   Memory model hypotheses for function 'job_struct_assigns':
   /*@ behavior wp_typed:
         requires \separated(p, &sv); */

src/plugins/wp/tests/wp_plugin/oracle/volatile.1.res.oracle

@@ -2,29 +2,54 @@
 [kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/volatile.i:15: Warning: 
+[wp] tests/wp_plugin/volatile.i:16: Warning: 
   unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:14: Warning: 
+[wp] tests/wp_plugin/volatile.i:15: Warning: 
   unsafe write-access to volatile l-value
-[wp] tests/wp_plugin/volatile.i:21: Warning: 
+[wp] tests/wp_plugin/volatile.i:22: Warning: 
   unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:20: Warning: 
+[wp] tests/wp_plugin/volatile.i:21: Warning: 
   unsafe read-access to volatile l-value
-[wp] tests/wp_plugin/volatile.i:35: Warning: 
+[wp] tests/wp_plugin/volatile.i:36: Warning: 
   unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:35: Warning: 
+[wp] tests/wp_plugin/volatile.i:36: Warning: 
   unsafe volatile access to (term) l-value
-[wp] tests/wp_plugin/volatile.i:34: Warning: 
+[wp] tests/wp_plugin/volatile.i:35: Warning: 
   unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning: 
+  unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:45: Warning: 
+  unsafe read-access to volatile l-value
+------------------------------------------------------------
+  Function default_init
+------------------------------------------------------------
+
+Goal Check 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 46):
+tests/wp_plugin/volatile.i:45: warning from wp:
+ - Warning: ignore volatile attribute
+   Reason: unsafe read-access to volatile l-value
+Let x = GlobalConst_0[ClientId_0].
+Assume {
+  Type: is_sint8(ClientId_0) /\ is_sint32(x).
+  (* Heap *)
+  Type: IsArray_sint32(GlobalConst_0).
+  (* Initializer *)
+  Init: forall i : Z. ((0 <= i) -> ((i <= 15) -> (GlobalConst_0[i] = 0))).
+  (* Pre-condition *)
+  Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Function job_assigns
 ------------------------------------------------------------
 
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 15):
-tests/wp_plugin/volatile.i:14: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 16):
+tests/wp_plugin/volatile.i:15: warning from wp:
  - Warning: ignore volatile attribute
    Reason: unsafe write-access to volatile l-value
-tests/wp_plugin/volatile.i:15: warning from wp:
+tests/wp_plugin/volatile.i:16: warning from wp:
  - Warning: ignore volatile attribute
    Reason: unsafe volatile access to (term) l-value
 Prove: true.
@@ -34,11 +59,11 @@ Prove: true.
   Function job_read
 ------------------------------------------------------------
 
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 21):
-tests/wp_plugin/volatile.i:20: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 22):
+tests/wp_plugin/volatile.i:21: warning from wp:
  - Warning: ignore volatile attribute
    Reason: unsafe read-access to volatile l-value
-tests/wp_plugin/volatile.i:21: warning from wp:
+tests/wp_plugin/volatile.i:22: warning from wp:
  - Warning: ignore volatile attribute
    Reason: unsafe volatile access to (term) l-value
 Prove: true.
@@ -48,7 +73,7 @@ Prove: true.
   Function job_struct
 ------------------------------------------------------------
 
-Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 29):
+Goal Assertion 'ok,dead_code' (file tests/wp_plugin/volatile.i, line 30):
 Prove: true.
 
 ------------------------------------------------------------
@@ -56,20 +81,23 @@ Prove: true.
   Function job_struct_assigns
 ------------------------------------------------------------
 
-Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 35):
-tests/wp_plugin/volatile.i:34: warning from wp:
+Goal Assertion 'KO_WHEN_VOLATILE' (file tests/wp_plugin/volatile.i, line 36):
+tests/wp_plugin/volatile.i:35: warning from wp:
  - Warning: ignore volatile attribute
-   Reason: unsafe write-access to volatile l-value
+   Reason: unsafe read-access to volatile l-value
 tests/wp_plugin/volatile.i:35: warning from wp:
+ - Warning: ignore volatile attribute
+   Reason: unsafe write-access to volatile l-value
+tests/wp_plugin/volatile.i:36: warning from wp:
  - Warning: ignore volatile attribute
    Reason: unsafe volatile access to (term) l-value
-tests/wp_plugin/volatile.i:35: warning from wp:
+tests/wp_plugin/volatile.i:36: warning from wp:
  - Warning: ignore volatile attribute
    Reason: unsafe volatile access to (term) l-value
 Prove: true.
 
 ------------------------------------------------------------
-[wp] tests/wp_plugin/volatile.i:32: Warning: 
+[wp] tests/wp_plugin/volatile.i:33: Warning: 
   Memory model hypotheses for function 'job_struct_assigns':
   /*@ behavior wp_typed:
         requires \separated(p, &sv); */

src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.0.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_assigns_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_read_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Qed] Goal typed_job_struct_assert_ok_dead_code : Valid
+[wp] [Alt-Ergo] Goal typed_job_struct_assigns_assert_KO_WHEN_VOLATILE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_default_init_check_KO_WHEN_VOLATILE : Unsuccess
+[wp] Proved goals:    1 / 5
+  Qed:             1 
+  Alt-Ergo:        0  (unsuccess: 4)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job_assigns               -        -        1       0.0%
+  job_read                  -        -        1       0.0%
+  job_struct                1        -        1       100%
+  job_struct_assigns        -        -        1       0.0%
+  default_init              -        -        1       0.0%
+------------------------------------------------------------
+[wp] tests/wp_plugin/volatile.i:33: Warning: 
+  Memory model hypotheses for function 'job_struct_assigns':
+  /*@ behavior wp_typed:
+        requires \separated(p, &sv); */
+  void job_struct_assigns(struct st_v *p);

src/plugins/wp/tests/wp_plugin/oracle_qualif/volatile.1.res.oracle

+# frama-c -wp -wp-no-volatile [...]
+[kernel] Parsing tests/wp_plugin/volatile.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/volatile.i:16: Warning: 
+  unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:15: Warning: 
+  unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:22: Warning: 
+  unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:21: Warning: 
+  unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:36: Warning: 
+  unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:36: Warning: 
+  unsafe volatile access to (term) l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning: 
+  unsafe write-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:35: Warning: 
+  unsafe read-access to volatile l-value
+[wp] tests/wp_plugin/volatile.i:45: Warning: 
+  unsafe read-access to volatile l-value
+[wp] 5 goals scheduled
+[wp] [Qed] Goal typed_job_assigns_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Qed] Goal typed_job_read_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Qed] Goal typed_job_struct_assert_ok_dead_code : Valid
+[wp] [Qed] Goal typed_job_struct_assigns_assert_KO_WHEN_VOLATILE : Valid
+[wp] [Alt-Ergo] Goal typed_default_init_check_KO_WHEN_VOLATILE : Valid
+[wp] Proved goals:    5 / 5
+  Qed:             4 
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job_assigns               1        -        1       100%
+  job_read                  1        -        1       100%
+  job_struct                1        -        1       100%
+  job_struct_assigns        1        -        1       100%
+  default_init              -        1        1       100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/volatile.i:33: Warning: 
+  Memory model hypotheses for function 'job_struct_assigns':
+  /*@ behavior wp_typed:
+        requires \separated(p, &sv); */
+  void job_struct_assigns(struct st_v *p);

src/plugins/wp/tests/wp_plugin/volatile.i

@@ -2,11 +2,12 @@
    OPT:
    OPT: -wp-no-volatile
 */
-
 /* run.config_qualif
-   DONTRUN:
+   OPT:
+   OPT: -wp-no-volatile
 */
 
+
 volatile int v ;
 
 void job_assigns(void)
@@ -34,3 +35,13 @@ void job_struct_assigns(struct st_v *p)
   *p = sv;
   /*@ assert KO_WHEN_VOLATILE: *p == sv ;  */ ;
 }
+
+int const volatile GlobalConst[16];
+
+/*@ requires 0 ≤ ClientId < 16; */
+void default_init(char const ClientId)
+{
+  int R1;
+  R1 = GlobalConst[ClientId];
+	//@ check KO_WHEN_VOLATILE: R1 == 0 ;
+}