[wp] Fix induction tactic typing

src/plugins/wp/Conditions.mli

@@ -177,6 +177,8 @@ val lemma : pred -> sequent
 val head : step -> pred (** Predicate for Have and such, Condition for Branch, True for Either *)
 val have : step -> pred (** Predicate for Have and such, True for any other *)
 
+val pred_cond : condition -> pred
+
 val condition : sequence -> pred (** With free variables kept. *)
 val close : sequent -> pred (** With free variables {i quantified}. *)
 

src/plugins/wp/TacInduction.ml

@@ -22,22 +22,40 @@
 
 open Lang
 
-type env = {
-  n : F.var ;
-  sigma : F.sigma ;
-  mutable hind : F.pred list ;
-}
-
-let rec strip env p =
-  match F.p_expr p with
-  | And ps -> F.p_all (strip env) ps
-  | _ ->
-      let p = F.p_subst env.sigma p in
-      if F.occursp env.n p then
-        ( env.hind <- p :: env.hind ; F.p_true )
-      else p
-
-let process value n0 seq =
+let filter n sequence =
+  let sequence = Conditions.list sequence in
+  let partition p =
+    match F.p_expr p with
+    | And ps -> List.partition (F.occursp n) ps
+    | _ -> if F.occursp n p then [ p ], [] else [], [ p ]
+  in
+  let add make (removed, steps) (rem, kept) =
+    List.rev_append (List.rev rem) removed, make (F.p_conj kept) :: steps
+  in
+  let partition_add acc make p = add make acc @@ partition p in
+  let filter_condition ((removed, steps) as acc) s =
+    let update = Conditions.update_cond s in
+    match s.condition with
+    | Type p -> partition_add acc (fun x -> update (Type x)) p
+    | Have p -> partition_add acc (fun x -> update (Have x)) p
+    | When p -> partition_add acc (fun x -> update (When x)) p
+    | Core p -> partition_add acc (fun x -> update (Core x)) p
+    | Init p -> partition_add acc (fun x -> update (Init x)) p
+    | State _ -> removed, update (Have F.p_true) :: steps
+    | Either _ | Branch _ as c ->
+        (* Note: it is not really expected that Conditions.pred_cond can
+           generate a property that, once partitioned, results in both kept and
+           removed parts. Anyway if it is the case, it means that it was able to
+           reduce the original property to a single conjunction, so let us
+           handle it like a Have. *)
+        match partition @@ Conditions.pred_cond c with
+        | [], _ -> removed, s :: steps
+        | res -> add (fun x -> update (Have x)) acc res
+  in
+  let removed, steps = List.fold_left filter_condition ([], []) sequence in
+  List.rev removed, Conditions.sequence @@ List.rev steps
+
+let process value n0 sequent =
 
   (* Transfrom seq into: hyps => (forall n, goal) *)
   let n = Lang.freshvar ~basename:"n" Qed.Logic.Int in
@@ -46,9 +64,9 @@ let process value n0 seq =
   let vi = F.e_var i in
   let sigma = Lang.sigma () in
   F.Subst.add sigma value vn ;
-  let env = { n ; sigma ; hind = [] } in
-  let hyps = Conditions.map_sequence (strip env) (fst seq) in
-  let goal_n = F.p_hyps env.hind @@ F.p_subst sigma (snd seq) in
+  let seq, goal = Conditions.map_sequent (F.p_subst sigma) sequent in
+  let hind, seq = filter n seq in
+  let goal_n = F.p_hyps hind @@ F.p_subst sigma goal in
   let goal_i = F.p_subst_var n vi goal_n in
 
   (* Base: n = n0 *)
@@ -67,7 +85,7 @@ let process value n0 seq =
     F.p_hyps [F.p_lt vn n0; hind] goal_n in
 
   (* All Cases *)
-  List.map (fun (name,goal) -> name , (hyps,goal)) [
+  List.map (fun (name,goal) -> name , (seq,goal)) [
     "Base" , goal_base ;
     "Induction (sup)" , goal_sup ;
     "Induction (inf)" , goal_inf ;

src/plugins/wp/tests/wp_tip/induction_typing.i

+/* run.config
+   OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/* This test is meant to check that we do not generate a ill-formed VC with the
+   induction tactic. Here, the bug happened when triggering an induction on i
+   (i was replaced with true) when proving that X is preserved . The example is
+   complex because we need to have some State variable for i. */
+
+extern int LIST;
+extern unsigned int cpt;
+extern unsigned int A[];
+
+/*@
+	axiomatic call {
+    logic \list<integer> list{L2} reads LIST;
+  }
+*/
+
+/*@
+	ensures cpt == \old(cpt) + 1;
+	ensures A[\old(cpt)] == \old(i);
+	ensures list == (\old(list) ^ [| 1 |]);
+	assigns cpt, LIST;
+*/
+void f(unsigned int i);
+
+
+/*@
+  requires list == [| |];
+	requires cpt == 0;
+*/
+void function(unsigned int Max)
+{
+	unsigned int i = 0;
+	/*@
+    loop invariant 0 <= cpt == i <= 42;
+		loop invariant X: list == (\at(list,LoopEntry) ^ ([| 1 |]  *^ i));
+		loop assigns i, cpt, LIST;
+	*/
+	while (i < Max) {
+		f(i);
+		i ++;
+	}
+
+  return;
+}

src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing induction_typing.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp:script:allgoals] 
+  Goal Preservation of Invariant 'X' (file induction_typing.i, line 41):
+  Let a = L_list(LIST_0).
+  Let a_1 = a ^ [ 1 ].
+  Let x = 1 + i.
+  Assume {
+    Type: is_uint32(Max_0) /\ is_uint32(i).
+    (* Heap *)
+    Type: IsArray_uint32(A) /\ is_sint32(LIST_1).
+    (* Pre-condition *)
+    Have: L_list(LIST_1) = nil.
+    (* Invariant *)
+    Have: (x = to_uint32(x)) /\ (0 <= i) /\ (i <= 42).
+    (* Invariant 'X' *)
+    Have: ([ 1 ] *^ i) = a.
+    (* Then *)
+    Have: i < Max_0.
+    (* Call 'f' *)
+    Have: (A[i] = i) /\ (L_list(LIST_2) = a_1).
+    (* Invariant *)
+    Have: i <= 41.
+  }
+  Prove: ([ 1 ] *^ x) = a_1.
+  
+  ------------------------------------------------------------
+[wp] [Qed] Goal typed_function_loop_invariant_X_established : Valid
+[wp:script:allgoals] 
+  typed_function_loop_invariant_X_preserved subgoal:
+  
+  Goal Wp.Tactical.typed_function_loop_invariant_X_preserved-0 (generated):
+  Let a = L_list(LIST_1).
+  Assume {
+    Type: is_uint32(Max_0) /\ is_uint32(i).
+    (* Heap *)
+    Type: IsArray_uint32(A) /\ is_sint32(LIST_0).
+    (* Pre-condition *)
+    Have: L_list(LIST_0) = nil.
+    (* Invariant *)
+    Have: (0 <= i) /\ (i <= 42).
+    (* Invariant 'X' *)
+    Have: ([ 1 ] *^ i) = a.
+    (* Then *)
+    Have: i < Max_0.
+    (* Call 'f' *)
+    Have: (A[i] = i) /\ (L_list(LIST_2) = a ^ [ 1 ]).
+    (* Invariant *)
+    Have: i <= 41.
+  }
+  Prove: false.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_function_loop_invariant_X_preserved : Unsuccess
+[wp:script:allgoals] 
+  typed_function_loop_invariant_X_preserved subgoal:
+  
+  Goal Wp.Tactical.typed_function_loop_invariant_X_preserved-1 (generated):
+  Let a = L_list(LIST_0).
+  Let a_1 = a ^ [ 1 ].
+  Assume {
+    Have: to_uint32(n) = n.
+    Have: 0 < n.
+    Have: forall i_1 : Z. ((to_uint32(i_1) = i_1) -> ((0 <= i_1) ->
+        ((i_1 < n) -> (([ 1 ] *^ i_1) = a_1)))).
+    Type: is_uint32(Max_0) /\ is_uint32(i).
+    (* Heap *)
+    Type: IsArray_uint32(A) /\ is_sint32(LIST_1).
+    (* Pre-condition *)
+    Have: L_list(LIST_1) = nil.
+    (* Invariant *)
+    Have: (0 <= i) /\ (i <= 42).
+    (* Invariant 'X' *)
+    Have: ([ 1 ] *^ i) = a.
+    (* Then *)
+    Have: i < Max_0.
+    (* Call 'f' *)
+    Have: (A[i] = i) /\ (L_list(LIST_2) = a_1).
+    (* Invariant *)
+    Have: i <= 41.
+  }
+  Prove: ([ 1 ] *^ n) = a_1.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_function_loop_invariant_X_preserved subgoal:
+  
+  Goal Wp.Tactical.typed_function_loop_invariant_X_preserved-2 (generated):
+  Let a = L_list(LIST_0).
+  Let a_1 = a ^ [ 1 ].
+  Assume {
+    Have: to_uint32(n) = n.
+    Have: n < 0.
+    Have: forall i_1 : Z. ((to_uint32(i_1) = i_1) -> ((i_1 <= 0) ->
+        ((n < i_1) -> (([ 1 ] *^ i_1) = a_1)))).
+    Type: is_uint32(Max_0) /\ is_uint32(i).
+    (* Heap *)
+    Type: IsArray_uint32(A) /\ is_sint32(LIST_1).
+    (* Pre-condition *)
+    Have: L_list(LIST_1) = nil.
+    (* Invariant *)
+    Have: (0 <= i) /\ (i <= 42).
+    (* Invariant 'X' *)
+    Have: ([ 1 ] *^ i) = a.
+    (* Then *)
+    Have: i < Max_0.
+    (* Call 'f' *)
+    Have: (A[i] = i) /\ (L_list(LIST_2) = a_1).
+    (* Invariant *)
+    Have: i <= 41.
+  }
+  Prove: ([ 1 ] *^ n) = a_1.
+  
+  ------------------------------------------------------------
+[wp] Proved goals:    1 / 2
+  Qed:             1
+[wp] No updated script.

src/plugins/wp/tests/wp_tip/oracle/induction_typing.session/script/function_loop_invariant_X_preserved.json

+[ { "header": "Induction", "tactic": "Wp.induction",
+    "params": { "base": { "select": "kint", "val": "0" } },
+    "select": { "select": "inside-goal", "occur": 0, "target": "1+i_1",
+                "pattern": "+1$i" },
+    "children": { "Base": [], "Induction (sup)": [], "Induction (inf)": [] } } ]