From 9630563eb251c72d194b8f92abb64d8b95a01d34 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 24 Feb 2021 15:15:44 +0100
Subject: [PATCH] [wp] Provide nullable as an ACSL extension
---
src/plugins/wp/RefUsage.ml | 63 +++++++++++++----
src/plugins/wp/tests/wp_plugin/nullable_ext.i | 33 +++++++++
.../wp_plugin/oracle/nullable_ext.res.oracle | 68 +++++++++++++++++++
.../oracle_qualif/nullable_ext.res.oracle | 49 +++++++++++++
4 files changed, 199 insertions(+), 14 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/nullable_ext.i
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 17a4c1015ae..0bf6762b319 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/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
diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.i b/src/plugins/wp/tests/wp_plugin/nullable_ext.i
new file mode 100644
index 00000000000..dbb1ba79414
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nullable_ext.i
@@ -0,0 +1,33 @@
+/* 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;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
new file mode 100644
index 00000000000..07f85e2ff88
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
@@ -0,0 +1,68 @@
+# 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);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
new file mode 100644
index 00000000000..792224aa370
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
@@ -0,0 +1,49 @@
+# 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);
--
GitLab