[wp] Provide nullable as an ACSL extension

src/plugins/wp/RefUsage.ml

@@ -831,22 +831,56 @@ let is_computed () = S.is_computed ()
 (* --- Nullable variables                                             --- *)
 (* ---------------------------------------------------------------------- *)
 
-module HasNullable =
-  State_builder.Option_ref(Datatype.Bool)
-    (struct
-      let name = "Wp.RefUsage.HasNullable"
-      let dependencies = [Ast.self]
-    end)
+module Nullable =
+struct
+  let attribute_name = "wp_nullable"
+
+  let is_nullable vi =
+    vi.vformal && Cil.hasAttribute attribute_name vi.vattr
+
+  let make_nullable vi =
+    vi.vattr <- Cil.addAttribute (AttrAnnot attribute_name) vi.vattr
+
+  module Nullable_extension =
+  struct
+    let type_term typing_context loc e =
+      match e.Logic_ptree.lexpr_node with
+      | Logic_ptree.PLvar s ->
+          let lv = typing_context.Logic_typing.find_var s in
+          begin match lv.lv_origin with
+            | Some vi when Cil.isPointerType vi.vtype ->
+                make_nullable vi ;
+                Logic_const.tvar ~loc lv
+            | _ ->
+                typing_context.error loc "No pointer: %s" s
+          end
+      | _  ->
+          typing_context.error loc "Illegal expression %a"
+            Logic_print.print_lexpr e
+
+    let typer typing_context loc l =
+      Ext_terms (List.map (type_term typing_context loc) l)
+  end
 
-let is_nullable vi = vi.vformal && Cil.hasAttribute "wp_nullable" vi.vattr
+  let () =
+    Acsl_extension.register_behavior
+      "wp_nullable_pointers" Nullable_extension.typer false
 
-let compute_nullable () =
-  let module F = Globals.Functions in
-  F.fold (fun f b ->
-      b || List.fold_left (fun b v -> b || is_nullable v) b (F.get_params f)
-    ) false
+  module HasNullable =
+    State_builder.Option_ref(Datatype.Bool)
+      (struct
+        let name = "Wp.RefUsage.HasNullable"
+        let dependencies = [Ast.self]
+      end)
 
-let has_nullable () = HasNullable.memo compute_nullable
+  let compute_nullable () =
+    let module F = Globals.Functions in
+    F.fold (fun f b ->
+        b || List.fold_left (fun b v -> b || is_nullable v) b (F.get_params f)
+      ) false
+
+  let has_nullable () = HasNullable.memo compute_nullable
+end
 
 (* ---------------------------------------------------------------------- *)
 (* --- API                                                            --- *)
@@ -875,7 +909,8 @@ let get ?kf ?(init=false) vi =
 
 let compute () = ignore (usage ())
 
-
+let is_nullable = Nullable.is_nullable
+let has_nullable = Nullable.has_nullable
 
 let print x m fmt = Access.pretty x fmt m
 

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

+/* run.config
+   OPT: -wp-model Caveat
+*/
+/* run.config_qualif
+   OPT: -wp-model Caveat
+*/
+
+int x ;
+int *g ;
+
+/*@ assigns *g, *p, x ;
+    wp_nullable_pointers p ;
+*/
+void nullable_coherence(int* p){
+  if(p == (void*)0){
+    //@ check must_fail: \false ;
+    return;
+  }
+  //@ check \valid(p);
+  *p = 42;
+  *g = 24;
+  x = 1;
+}
+
+/*@ assigns *p, *q, *r, *s, *t ;
+    wp_nullable_pointers p, q, r ;
+*/
+void nullable_in_context(int* p, int* q, int* r, int* s, int* t){
+  *p = 42;
+  *q = 42;
+  *r = 42;
+  *s = *t = 0;
+}

src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle

+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In Caveat mode, with nullable variables,-wp-rte should be explicitly positioned
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function nullable_coherence
+------------------------------------------------------------
+
+Goal Check 'must_fail' (file tests/wp_plugin/nullable_ext.i, line 16):
+Assume { (* Then *) Have: null = pointer_p. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_plugin/nullable_ext.i, line 19):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.i, line 11) in 'nullable_coherence':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function nullable_in_context
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.i, line 25) in 'nullable_in_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.i, line 25) in 'nullable_in_context' (2/2):
+Effect at line 32
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable_ext.i:14: Warning: 
+  Memory model hypotheses for function 'nullable_coherence':
+  /*@
+     behavior wp_typed_caveat:
+       requires \separated(g, &x);
+       requires \separated(p, &x);
+       requires \valid(g);
+       requires p ≢ \null ⇒ \separated(g, p, &x);
+       requires \valid(p) ∨ p ≡ \null;
+     */
+  void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable_ext.i:28: Warning: 
+  Memory model hypotheses for function 'nullable_in_context':
+  /*@
+     behavior wp_typed_caveat:
+       requires \valid(s);
+       requires \valid(t);
+       requires p ≢ \null ⇒ \separated(p, s, t);
+       requires q ≢ \null ⇒ \separated(q, s, t);
+       requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+       requires r ≢ \null ⇒ \separated(r, s, t);
+       requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+       requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+       requires \valid(p) ∨ p ≡ \null;
+       requires \valid(q) ∨ q ≡ \null;
+       requires \valid(r) ∨ r ≡ \null;
+     */
+  void nullable_in_context(int *p /*@ wp_nullable */,
+                           int *q /*@ wp_nullable */,
+                           int *r /*@ wp_nullable */, int *s, int *t);

src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle

+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In Caveat mode, with nullable variables,-wp-rte should be explicitly positioned
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_caveat_nullable_coherence_check_must_fail : Unsuccess
+[wp] [Qed] Goal typed_caveat_nullable_coherence_check : Valid
+[wp] [Qed] Goal typed_caveat_nullable_coherence_assigns : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part1 : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part2 : Valid
+[wp] Proved goals:    4 / 5
+  Qed:             4 
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  nullable_coherence        2        -        3      66.7%
+  nullable_in_context       2        -        2       100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable_ext.i:14: Warning: 
+  Memory model hypotheses for function 'nullable_coherence':
+  /*@
+     behavior wp_typed_caveat:
+       requires \separated(g, &x);
+       requires \separated(p, &x);
+       requires \valid(g);
+       requires p ≢ \null ⇒ \separated(g, p, &x);
+       requires \valid(p) ∨ p ≡ \null;
+     */
+  void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable_ext.i:28: Warning: 
+  Memory model hypotheses for function 'nullable_in_context':
+  /*@
+     behavior wp_typed_caveat:
+       requires \valid(s);
+       requires \valid(t);
+       requires p ≢ \null ⇒ \separated(p, s, t);
+       requires q ≢ \null ⇒ \separated(q, s, t);
+       requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+       requires r ≢ \null ⇒ \separated(r, s, t);
+       requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+       requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+       requires \valid(p) ∨ p ≡ \null;
+       requires \valid(q) ∨ q ≡ \null;
+       requires \valid(r) ∨ r ≡ \null;
+     */
+  void nullable_in_context(int *p /*@ wp_nullable */,
+                           int *q /*@ wp_nullable */,
+                           int *r /*@ wp_nullable */, int *s, int *t);