[wp] Support relation based variant

src/plugins/wp/cfgAnnot.ml

@@ -468,6 +468,14 @@ let mk_variant_properties kf s ca v =
   let vdecr = Logic_const.prel ~loc (Rlt, v, vcurr) in
   (vpos_id, vpos), (vdecr_id, vdecr)
 
+let mk_variant_relation_property kf s ca v li =
+  let vid = WpPropId.mk_var_id kf s ca in
+  let loc = v.term_loc in
+  let lcurr = Clabels.to_logic (Clabels.loop_current s) in
+  let vcurr = Logic_const.tat ~loc (v, lcurr) in
+  let variant = Logic_const.papp ~loc (li,[],[vcurr ; v]) in
+  (vid, variant)
+
 type loop_hypothesis =
   | NoHyp
   | Check of WpPropId.prop_id
@@ -505,6 +513,23 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
         let normalize_pred p = NormAtLabels.preproc_annot labels p in
         let normalize_annot (i,p) = i, normalize_pred p in
         let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
+        let intro_terminates_variant ~loc (pid, v) =
+          pid,
+          let t = snd @@ get_terminates_hyp kf in
+          if Wp_parameters.TerminatesVariantHyp.get () then begin
+            if Logic_utils.is_same_predicate t Logic_const.pfalse then
+              Wp_parameters.warning
+                ~source:(fst loc) ~once:true
+                "Loop variant is always trivially verified \
+                 (terminates \\false)" ;
+            Logic_const.pimplies (t, v)
+          end else v
+        in
+        let variant_as_inv ~loc (i, p) =
+          let i, p = intro_terminates_variant ~loc @@ normalize_annot (i, p) in
+          { loop_pred = p ;
+            loop_hyp = NoHyp ; loop_est = None ; loop_ind = Some i }
+        in
         default_assigns stmt @@
         Annotations.fold_code_annot
           begin fun _emitter ca l ->
@@ -525,28 +550,15 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
                 { l with
                   loop_invariants  = inv :: l.loop_invariants ; }
             | AVariant(term, None) ->
-                let vpos , vdec =
-                  mk_variant_properties kf stmt ca term in
-                let intro_terminates (pid, v) =
-                  pid,
-                  let t = snd @@ get_terminates_hyp kf in
-                  if Wp_parameters.TerminatesVariantHyp.get () then begin
-                    if Logic_utils.is_same_predicate t Logic_const.pfalse then
-                      Wp_parameters.warning
-                        ~source:(fst term.term_loc) ~once:true
-                        "Loop variant is always trivially verified \
-                         (terminates \\false)" ;
-                    Logic_const.pimplies (t, v)
-                  end else v
-                in
-                let mk_inv (i, p) =
-                  let i, p = intro_terminates @@ normalize_annot (i, p) in
-                  { loop_pred = p ;
-                    loop_hyp = NoHyp ; loop_est = None ; loop_ind = Some i }
-                in
+                let vpos , vdec = mk_variant_properties kf stmt ca term in
+                let vpos = variant_as_inv ~loc:term.term_loc vpos in
+                let vdec = variant_as_inv ~loc:term.term_loc vdec in
                 { l with loop_terminates = None ;
-                         loop_invariants =
-                           mk_inv vdec :: mk_inv vpos :: l.loop_invariants }
+                         loop_invariants = vdec :: vpos :: l.loop_invariants }
+            | AVariant(term, Some rel) ->
+                let vrel = mk_variant_relation_property kf stmt ca term rel in
+                let vrel = variant_as_inv ~loc:term.term_loc vrel in
+                { l with loop_invariants = vrel :: l.loop_invariants }
             | AAssigns(_,WritesAny) ->
                 let asgn = WpPropId.mk_loop_any_assigns_info stmt in
                 { l with loop_assigns = asgn :: l.loop_assigns }

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

@@ -2,6 +2,7 @@
 [kernel] Parsing terminates_formulae.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
 [wp] [CFG] Goal variant_terminates : Valid (Trivial)
 ------------------------------------------------------------
   Function base_call
@@ -57,18 +58,32 @@ Goal Termination-condition (file terminates_formulae.i, line 27) in 'call_same':
 Call Effect at line 29
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function general_variant
+------------------------------------------------------------
+
+Goal Loop assigns (file terminates_formulae.i, line 66):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Follows relation Loop variant at loop (file terminates_formulae.i, line 68):
+Assume { Type: is_uint32(x). (* Goal *) When: P_Q. (* Then *) Have: 0 < x. }
+Prove: P_Rel(x, to_uint32(x - 1)).
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function no_variant
 ------------------------------------------------------------
 
-Goal Termination-condition (file terminates_formulae.i, line 62) in 'no_variant':
-Effect at line 65
+Goal Termination-condition (file terminates_formulae.i, line 71) in 'no_variant':
+Effect at line 74
 Prove: !P_Q.
 
 ------------------------------------------------------------
 
-Goal Loop assigns (file terminates_formulae.i, line 64):
+Goal Loop assigns (file terminates_formulae.i, line 73):
 Prove: true.
 
 ------------------------------------------------------------

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

@@ -2,8 +2,9 @@
 [kernel] Parsing terminates_formulae.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
+[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
 [wp] [CFG] Goal variant_terminates : Valid (Trivial)
-[wp] 10 goals scheduled
+[wp] 12 goals scheduled
 [wp] [Alt-Ergo] Goal typed_base_call_terminates : Unsuccess
 [wp] [Qed] Goal typed_call_same_terminates : Valid
 [wp] [Alt-Ergo] Goal typed_call_change_terminates : Unsuccess
@@ -12,11 +13,13 @@
 [wp] [Qed] Goal typed_variant_loop_assigns : Valid
 [wp] [Alt-Ergo] Goal typed_variant_loop_variant_decrease : Valid
 [wp] [Qed] Goal typed_variant_loop_variant_positive : Valid
+[wp] [Qed] Goal typed_general_variant_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_general_variant_loop_variant_relation : Valid
 [wp] [Alt-Ergo] Goal typed_no_variant_terminates : Unsuccess
 [wp] [Qed] Goal typed_no_variant_loop_assigns : Valid
-[wp] Proved goals:    7 / 11
-  Qed:             5 
-  Alt-Ergo:        1  (unsuccess: 4)
+[wp] Proved goals:   10 / 14
+  Qed:             6 
+  Alt-Ergo:        2  (unsuccess: 4)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   base_call                 -        -        1       0.0%
@@ -25,5 +28,6 @@
   call_param_same           1        -        1       100%
   call_param_change         -        -        1       0.0%
   variant                   2        1        3       100%
+  general_variant           1        1        2       100%
   no_variant                1        -        2      50.0%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/terminates_formulae.i

@@ -59,6 +59,15 @@ void variant(void){
   for(unsigned i = 3; i > 0; --i);
 }
 
+/*@ predicate Rel (integer old, integer new) = old > new && 0 <= old; */
+
+//@ terminates Q ;
+void general_variant(unsigned x) {
+  /*@ loop assigns x ;
+      loop variant x for Rel; */
+  while (x > 0) x --;
+}
+
 //@ terminates Q ;
 void no_variant(void){
   //@ loop assigns i ;

src/plugins/wp/wpPropId.ml

@@ -42,6 +42,7 @@ type prop_kind =
   | PKPropLoop    (** loop property used as hypothesis inside a loop. *)
   | PKVarDecr     (** computation related to the decreasing of a variant in a loop *)
   | PKVarPos      (** computation related to a loop variant being positive *)
+  | PKVarRel      (** computation related to a generalized loop variant *)
   | PKAFctOut     (** computation related to the function assigns on normal termination *)
   | PKAFctExit    (** computation related to the function assigns on exit termination *)
   | PKTerminates  (** computation related to the termination *)
@@ -124,6 +125,7 @@ let mk_loop_inv kf s ca =
 let mk_inv_hyp_id    kf s ca = mk_prop PKPropLoop  (mk_annot_id kf s ca)
 let mk_var_decr_id   kf s ca = mk_prop PKVarDecr (mk_annot_id kf s ca)
 let mk_var_pos_id    kf s ca = mk_prop PKVarPos  (mk_annot_id kf s ca)
+let mk_var_id kf s ca = mk_prop PKVarRel (mk_annot_id kf s ca)
 
 let mk_loop_from_id kf s ca from =
   let id = Property.ip_of_from kf (Kstmt s) (Property.Id_loop ca) from in
@@ -212,13 +214,14 @@ let kind_order = function
   | PKPreserved -> 3
   | PKVarPos -> 4
   | PKVarDecr -> 5
-  | PKPropLoop -> 6
-  | PKAFctOut -> 7
-  | PKAFctExit -> 8
-  | PKCheck -> 9
-  | PKTactic -> 10
-  | PKSmoke -> 11
-  | PKTerminates -> 12
+  | PKVarRel -> 6
+  | PKPropLoop -> 7
+  | PKAFctOut -> 8
+  | PKAFctExit -> 9
+  | PKCheck -> 10
+  | PKTactic -> 11
+  | PKSmoke -> 12
+  | PKTerminates -> 13
 
 let compare_kind k1 k2 = match k1, k2 with
     PKPre (kf1, ki1, p1), PKPre (kf2, ki2, p2) ->
@@ -339,6 +342,7 @@ end = struct
     | PKPreserved , p -> base_id_prop_txt p ^ "_preserved"
     | PKVarDecr , p -> base_id_prop_txt p ^ "_decrease"
     | PKVarPos , p -> base_id_prop_txt p ^ "_positive"
+    | PKVarRel , p -> base_id_prop_txt p ^ "_relation"
     | PKAFctOut , p -> base_id_prop_txt p ^ "_normal"
     | PKAFctExit , p -> base_id_prop_txt p ^ "_exit"
     | PKPre(_kf,stmt,pre) , _ ->
@@ -422,6 +426,7 @@ struct
     | PKPreserved , p -> get_ip p ^ "_preserved"
     | PKVarDecr , p -> get_ip p ^ "_decrease"
     | PKVarPos , p -> get_ip p ^ "_positive"
+    | PKVarRel , p -> get_ip p ^ "_relation"
     | PKAFctOut , p -> get_ip p ^ "_normal"
     | PKAFctExit , p -> get_ip p ^ "_exit"
     | PKPre(callee_kf,stmt,pre) , _ ->
@@ -567,6 +572,7 @@ let label_of_kind = function
   | PKPreserved -> "Preservation"
   | PKVarDecr -> "Decreasing"
   | PKVarPos -> "Positive"
+  | PKVarRel -> "Relation"
   | PKAFctOut -> "Function assigns"
   | PKAFctExit -> "Exit assigns"
   | PKTerminates -> "Terminates"
@@ -591,6 +597,7 @@ struct
     | PKPreserved -> pp_print_string fmt " (preserved)"
     | PKVarDecr -> pp_print_string fmt " (decrease)"
     | PKVarPos -> pp_print_string fmt " (positive)"
+    | PKVarRel -> pp_print_string fmt " (relation)"
     | PKAFctOut -> pp_print_string fmt " (return)"
     | PKAFctExit -> pp_print_string fmt " (exit)"
     | PKPre(kf,_,_) -> fprintf fmt " (call '%s')" (Kernel_function.get_name kf)
@@ -662,6 +669,7 @@ let propid_hints hs p =
   | PKPreserved , _ -> add_required hs "preserved"
   | PKVarDecr , _ -> add_required hs "decrease"
   | PKVarPos , _ -> add_required hs "positive"
+  | PKVarRel , _ -> add_required hs "relation"
   | PKAFctOut , _ -> add_required hs "return"
   | PKAFctExit , _ -> add_required hs "exit"
   | PKTerminates , _ -> add_required hs "terminates"
@@ -745,6 +753,7 @@ let pp_goal_kind fmt = function
   | PKPreserved -> Format.pp_print_string fmt "Preservation of "
   | PKVarDecr -> Format.pp_print_string fmt "Decreasing of "
   | PKVarPos -> Format.pp_print_string fmt "Positivity of "
+  | PKVarRel -> Format.pp_print_string fmt "Follows relation "
 
 let pp_goal_part fmt = function
   | None -> ()
@@ -1049,7 +1058,8 @@ let split_map f pid gs =
 
 let subproofs id = match id.p_kind with
   | PKCheck -> 0
-  | PKProp | PKSmoke | PKTactic | PKPre _ | PKPropLoop | PKTerminates -> 1
+  | PKProp | PKSmoke | PKTactic | PKPre _ | PKPropLoop
+  | PKTerminates | PKVarRel -> 1
   | PKEstablished | PKPreserved
   | PKVarDecr | PKVarPos
   | PKAFctExit | PKAFctOut -> 2
@@ -1057,7 +1067,7 @@ let subproofs id = match id.p_kind with
 let subproof_idx id = match id.p_kind with
   | PKCheck -> (-1) (* 0/0 *)
   | PKProp | PKTactic | PKPre _ | PKSmoke | PKPropLoop
-  | PKTerminates -> 0 (* 1/1 *)
+  | PKTerminates | PKVarRel -> 0 (* 1/1 *)
   | PKPreserved  -> 0 (* 1/2 *)
   | PKEstablished-> 1 (* 2/2 *)
   | PKVarDecr    -> 0 (* 1/2 *)
@@ -1125,7 +1135,7 @@ let get_induction p =
             (* loop assigns *) Some stmt
         | _ -> None (* assert false ??? *)
       in loop_stmt_opt
-  | PKEstablished|PKVarDecr|PKVarPos|PKPreserved ->
+  | PKEstablished|PKVarDecr|PKVarPos|PKVarRel|PKPreserved ->
       (match get_stmt (property_of_id p) with
        | None -> None | Some (_, s) -> Some s)
 

src/plugins/wp/wpPropId.mli

@@ -98,6 +98,7 @@ type prop_kind =
   | PKPropLoop    (** loop property used as hypothesis inside a loop. *)
   | PKVarDecr     (** computation related to the decreasing of a variant in a loop *)
   | PKVarPos      (** computation related to a loop variant being positive *)
+  | PKVarRel      (** computation related to a generalized loop variant *)
   | PKAFctOut     (** computation related to the function assigns on normal termination *)
   | PKAFctExit    (** computation related to the function assigns on exit termination *)
   | PKTerminates  (** computation related to the termination *)
@@ -145,6 +146,9 @@ val mk_var_decr_id : kernel_function -> stmt -> code_annotation -> prop_id
 (** Variant positive *)
 val mk_var_pos_id : kernel_function -> stmt -> code_annotation -> prop_id
 
+(** Variant for *)
+val mk_var_id : kernel_function -> stmt -> code_annotation -> prop_id
+
 (** \from property of loop assigns. Must not be [FromAny] *)
 val mk_loop_from_id : kernel_function -> stmt -> code_annotation ->
   from -> prop_id