Merge branch 'feature/wp/post-assigns' into 'master'

[wp] fix assigns with Post labels

See merge request frama-c/frama-c!2931

src/plugins/wp/cfgWP.ml

@@ -90,7 +90,7 @@ struct
   (* Authorized written region from an assigns specification *)
   type effect = {
     e_pid : P.t ; (* Assign Property *)
-    e_kind : a_kind ; (* Requires post effects (in case of loop-assigns) *)
+    e_post : bool ; (* Requires post effects (loop-assigns or post-assigns) *)
     e_label : c_label ; (* scope for collection *)
     e_valid : L.sigma ; (* sigma where locations are filtered for validity *)
     e_region : L.region ; (* expected from spec *)
@@ -444,21 +444,23 @@ struct
         ainfo.a_assigns
     in match authorized_region with
     | None -> None
-    | Some region -> Some {
-        e_pid = pid ;
-        e_kind = ainfo.a_kind ;
-        e_label = from ;
-        e_valid = sigma ;
-        e_region = region ;
-        e_warn = Warning.Set.empty ;
-      }
+    | Some region ->
+        let post = match ainfo.a_kind with
+          | LoopAssigns -> true
+          | StmtAssigns -> NormAtLabels.has_postassigns ainfo.a_assigns
+        in Some {
+          e_pid = pid ;
+          e_post = post ;
+          e_label = from ;
+          e_valid = sigma ;
+          e_region = region ;
+          e_warn = Warning.Set.empty ;
+        }
 
   let cc_posteffect e vcs =
-    match e.e_kind with
-    | StmtAssigns -> vcs
-    | LoopAssigns ->
-        let vc = { empty_vc with vars = L.vars e.e_region } in
-        Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
+    if not e.e_post then vcs else
+      let vc = { empty_vc with vars = L.vars e.e_region } in
+      Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
 
   (* -------------------------------------------------------------------------- *)
   (* --- WP RULES : adding axioms, hypotheses and goals                     --- *)
@@ -549,14 +551,13 @@ struct
              vars = xs }
          in
          let group =
-           match e.e_kind with
-           | StmtAssigns ->
-               Splitter.singleton (setup empty_vc)
-           | LoopAssigns ->
-               try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
-               with Not_found ->
-                 Wp_parameters.fatal "Missing post-effect for %a"
-                   WpPropId.pretty e.e_pid
+           if not e.e_post then
+             Splitter.singleton (setup empty_vc)
+           else
+             try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
+             with Not_found ->
+               Wp_parameters.fatal "Missing post-effect for %a"
+                 WpPropId.pretty e.e_pid
          in
          let target = match sloc with
            | None -> Gprop e.e_pid

src/plugins/wp/clabels.ml

@@ -74,6 +74,11 @@ let of_logic = function
   | BuiltinLabel LoopEntry -> loopentry
   | StmtLabel s -> stmt !s
 
+let is_post = function
+  | BuiltinLabel Post -> true
+  | FormalLabel a -> a = post
+  | _ -> false
+
 let name = function FormalLabel a -> a | _ -> ""
 
 let lookup labels a =

src/plugins/wp/clabels.mli

@@ -65,6 +65,9 @@ val of_logic : Cil_types.logic_label -> c_label
     labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since
     they points to different program points dependending on the context. *)
 
+val is_post : Cil_types.logic_label -> bool
+(** Checks whether the logic-label is [Post] or [to_logic post] *)
+
 val pretty : Format.formatter -> c_label -> unit
 
 open Cil_types

src/plugins/wp/normAtLabels.ml

@@ -210,9 +210,27 @@ let preproc_assigns labels asgns =
   let visitor = new norm_at labels in
   List.map (Visitor.visitFramacFrom visitor) asgns
 
+let has_postassigns = function
+  | WritesAny -> false
+  | Writes froms ->
+      let exception HAS_POST in
+      let visitor = new norm_at (fun l ->
+          if Clabels.is_post l then raise HAS_POST
+          else Clabels.of_logic l
+        ) in
+      try
+        List.iter
+          (fun fr -> ignore @@ Visitor.visitFramacFrom visitor fr)
+          froms ;
+        false
+      with HAS_POST ->
+        true
+
 let catch_label_error ex txt1 txt2 = match ex with
   | LabelError lab ->
       Wp_parameters.warning
         "Unexpected label %a in %s : ignored %s"
         Wp_error.pp_logic_label lab txt1 txt2
   | _ -> raise ex
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/normAtLabels.mli

@@ -42,5 +42,5 @@ val labels_predicate : (logic_label * logic_label) list -> label_mapping
 val labels_axiom : label_mapping
 
 val preproc_annot : label_mapping -> predicate -> predicate
-
 val preproc_assigns : label_mapping -> from list -> from list
+val has_postassigns : assigns -> bool

src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function job1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/postassigns.c, line 4) in 'job1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (2/9):
+Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (3/9):
+Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (4/9):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (5/9):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (6/9):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (7/9):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (8/9):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (9/9):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function job2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/postassigns.c, line 19) in 'job2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (2/9):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (3/9):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (4/9):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (5/9):
+Effect at line 26
+Let x = A[1].
+Assume {
+  Type: is_sint32(x).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ IsArray_sint32(A) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_sint32(p, x), 1).
+}
+Prove: exists i : Z. (A[i] = x) /\ (0 <= i) /\ (i <= 3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (6/9):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (7/9):
+Effect at line 27
+Let x = A[2].
+Assume {
+  Type: is_sint32(x).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ IsArray_sint32(A) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_sint32(p, x), 1).
+}
+Prove: exists i : Z. (A[i] = x) /\ (0 <= i) /\ (i <= 3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (8/9):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (9/9):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function job3
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/postassigns.c, line 38):
+Assume {
+  Type: is_sint32(N) /\ is_sint32(i) /\ is_sint32(1 + i).
+  (* Pre-condition *)
+  Have: 0 <= N.
+  (* Invariant *)
+  Have: (i <= N) /\ (0 <= i).
+  (* Then *)
+  Have: i < N.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/postassigns.c, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (2/3):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (3/3):
+Effect at line 42
+Let a = shift_sint32(p, i).
+Assume {
+  Type: is_sint32(N) /\ is_sint32(i).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, a, 1).
+  (* Pre-condition *)
+  Have: 0 <= N.
+  (* Invariant *)
+  Have: (i <= N) /\ (0 <= i).
+  (* Then *)
+  Have: i < N.
+}
+Prove: included(a, 1, shift_sint32(p, 0), N).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 33) in 'job3' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 33) in 'job3' (2/2):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_acsl/postassigns.c:7: Warning: 
+  Memory model hypotheses for function 'job1':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), &N);
+       ensures \separated(p + (0 .. \at(N,Post) - 1), &N);
+     */
+  void job1(int *p);
+[wp] tests/wp_acsl/postassigns.c:22: Warning: 
+  Memory model hypotheses for function 'job2':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), (int *)A + (..), &N);
+       ensures \separated(p + A[0 .. \at(N,Post) - 1], (int *)A + (..), &N);
+     */
+  void job2(int *p);
+[wp] tests/wp_acsl/postassigns.c:35: Warning: 
+  Memory model hypotheses for function 'job3':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), &N);
+       ensures \separated(p + (0 .. \at(N,Post)), &N);
+     */
+  void job3(int *p);

src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 27 goals scheduled
+[wp] [Qed] Goal typed_job1_ensures : Valid
+[wp] [Qed] Goal typed_job1_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part4 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part5 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part6 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part7 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part8 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part9 : Valid
+[wp] [Qed] Goal typed_job2_ensures : Valid
+[wp] [Qed] Goal typed_job2_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part4 : Valid
+[wp] [Alt-Ergo] Goal typed_job2_assigns_part5 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_job2_assigns_part7 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part8 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part9 : Valid
+[wp] [Alt-Ergo] Goal typed_job3_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job3_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_job3_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job3_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_job3_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job3_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job3_assigns_part2 : Valid
+[wp] Proved goals:   27 / 27
+  Qed:            23 
+  Alt-Ergo:        4
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job1                     10        -       10       100%
+  job2                      8        2       10       100%
+  job3                      5        2        7       100%
+------------------------------------------------------------
+[wp] tests/wp_acsl/postassigns.c:7: Warning: 
+  Memory model hypotheses for function 'job1':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), &N);
+       ensures \separated(p + (0 .. \at(N,Post) - 1), &N);
+     */
+  void job1(int *p);
+[wp] tests/wp_acsl/postassigns.c:22: Warning: 
+  Memory model hypotheses for function 'job2':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), (int *)A + (..), &N);
+       ensures \separated(p + A[0 .. \at(N,Post) - 1], (int *)A + (..), &N);
+     */
+  void job2(int *p);
+[wp] tests/wp_acsl/postassigns.c:35: Warning: 
+  Memory model hypotheses for function 'job3':
+  /*@
+     behavior wp_typed:
+       requires \separated(p + (..), &N);
+       ensures \separated(p + (0 .. \at(N,Post)), &N);
+     */
+  void job3(int *p);

src/plugins/wp/tests/wp_acsl/postassigns.c

+int N;
+
+/*@
+  ensures N == 4;
+  assigns N, p[0..\at(N,Post)-1];
+*/
+void job1(int *p)
+{
+  N = 0;
+  p[N++] = 0;
+  p[N++] = 0;
+  p[N++] = 0;
+  p[N++] = 0;
+}
+
+int A[4];
+
+/*@
+  ensures N == 4;
+  assigns N, *(p + A[0..\at(N,Post)-1]);
+*/
+void job2(int *p)
+{
+  N = 0;
+  p[A[N++]] = 0;
+  p[A[N++]] = 0;
+  p[A[N++]] = 0;
+  p[A[N++]] = 0;
+}
+
+/*@
+  requires 0 <= N;
+  assigns N, p[0..\at(N,Post)];
+*/
+void job3(int *p)
+{
+  /*@
+    loop invariant 0 <= i <= N;
+    loop assigns i, p[0..N-1];
+   */
+  for (int i = 0; i < N; i++)
+    p[i] = 0;
+  N++;
+}