[wp] fix use/verify predicate kinds

src/kernel_services/ast_queries/logic_utils.ml

@@ -2229,6 +2229,9 @@ let lhost_c_type thost =
      | _ -> assert false)
   | TResult ty -> ty
 
+let use_predicate = function Assert | Admit -> true | Check -> false
+let verify_predicate = function Assert | Check -> true | Admit -> false
+
 let is_assert ca =
   match ca.annot_content with AAssert (_, p) -> p.tp_kind = Assert | _ -> false
 

src/kernel_services/ast_queries/logic_utils.mli

@@ -444,6 +444,15 @@ val merge_funspec :
 val clear_funspec: funspec -> unit
 
 (** {2 Discriminating code_annotations} *)
+
+(** Checks if a predicate kind can be used as an hypothesis or requirement.
+    It is true for `Admit` and `Assert`, and false for `Check`. *)
+val use_predicate : predicate_kind -> bool
+
+(** Checks if a predicate kind shall be put under verification.
+    It is true for `Assert` and `Check`, and false for `Admit`. *)
+val verify_predicate : predicate_kind -> bool
+
 (** Functions below allows to test a special kind of code_annotation.
     Use them in conjunction with {!Annotations.get_filter} to retrieve
     a particular kind of annotations associated to a statement. *)

src/plugins/wp/wpAnnot.ml

@@ -28,6 +28,7 @@ let debug fmt = Wp_parameters.debug ~dkey fmt
 
 open Cil_types
 open Cil_datatype
+open Logic_utils
 
 (* -------------------------------------------------------------------------- *)
 (* --- Selection of relevant assigns and postconditions                   --- *)
@@ -761,7 +762,7 @@ let add_called_post called_kf termination_kind acc =
     let kind = WpStrategy.AcallHyp called_kf in
     let assumes = (Ast_info.behavior_assumes b) in
     let add_post acc (tk, p) =
-      if tk = termination_kind && p.ip_content.tp_kind <> Check
+      if tk = termination_kind && use_predicate p.ip_content.tp_kind
       then WpStrategy.add_prop_call_post acc kind called_kf b tk ~assumes p
       else acc
     in List.fold_left add_post acc b.b_post_cond
@@ -838,7 +839,8 @@ let add_variant_annot config s ca var_exp loop_entry loop_back =
   in loop_entry, loop_back
 
 let add_loop_invariant_annot config vloop s ca b_list inv acc =
-  let only_check = inv.tp_kind = Check in
+  let hyp = use_predicate inv.tp_kind in
+  let goal = verify_predicate inv.tp_kind in
   let inv = inv.tp_statement in
   let assigns, loop_entry, loop_back , loop_core = acc in
   (* we have to prove that inv is true for each edge that goes
@@ -849,22 +851,29 @@ let add_loop_invariant_annot config vloop s ca b_list inv acc =
   | TBRpart (* TODO: PKPartial *)
     ->
       begin
-        let loop_entry = add_prop_loop_inv ~established:true config loop_entry
-            WpStrategy.Agoal s ca inv in
-        let loop_back = add_prop_loop_inv ~established:false config loop_back
-            WpStrategy.Agoal s ca inv in
+        let loop_entry =
+          if goal then
+            add_prop_loop_inv ~established:true config loop_entry
+              WpStrategy.Agoal s ca inv
+          else loop_entry in
+        let loop_back =
+          if goal then
+            add_prop_loop_inv ~established:false config loop_back
+              WpStrategy.Agoal s ca inv
+          else loop_back in
         let loop_core =
-          if only_check then loop_core
-          else
+          if hyp then
             add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
-        in
+          else loop_core in
         assigns, loop_entry , loop_back , loop_core
       end
-  | TBRhyp when not only_check ->
-      let kind = WpStrategy.Ahyp in
-      let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
-      in assigns, loop_entry , loop_back , loop_core
-  | TBRhyp | TBRno -> acc
+  | TBRhyp ->
+      if hyp then
+        let kind = WpStrategy.Ahyp in
+        let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
+        in assigns, loop_entry , loop_back , loop_core
+      else acc
+  | TBRno -> acc
 
 (** Returns the annotations for the three edges of the loop node:
  * - loop_entry : goals for the edge entering in the loop
@@ -952,24 +961,25 @@ let get_stmt_annots config v s =
         let acc = match is_annot_for_config config v s b_list with
           | TBRno -> acc
           | TBRhyp ->
-              if p.tp_kind = Check then acc
-              else
+              if use_predicate p.tp_kind then
                 let b_acc =
                   WpStrategy.add_prop_assert
                     b_acc WpStrategy.Ahyp kf s a p.tp_statement
                 in (b_acc, (a_acc, e_acc))
+              else acc
           | TBRok | TBRpart ->
               let id = WpPropId.mk_assert_id config.kf s a in
               let goal = goal_to_select config id in
-              if p.tp_kind = Check && not goal then acc
-              else
-                let kind =
-                  WpStrategy.(if p.tp_kind = Check then Agoal else Aboth goal)
-                in
+              let add, kind =
+                match p.tp_kind with
+                | Admit -> true, WpStrategy.Ahyp
+                | Assert -> true, Aboth goal
+                | Check -> goal, Agoal
+              in if add then
                 let b_acc =
                   WpStrategy.add_prop_assert b_acc kind kf s a p.tp_statement
-                in
-                (b_acc, (a_acc, e_acc))
+                in (b_acc, (a_acc, e_acc))
+              else acc
         in acc
     | AAllocation (_b_list, _frees_allocates) ->
         (* [PB] TODO *) acc
@@ -1136,7 +1146,7 @@ let add_global_annotations annots =
           linfo.l_var_info.lv_name;
         ()
     | Dlemma (name,_,_,_,p,_,_) ->
-        if p.tp_kind <> Check then
+        if use_predicate p.tp_kind then
           WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
 
   and do_globals gs = List.iter do_global gs in

src/plugins/wp/wpReached.ml

@@ -92,7 +92,7 @@ let is_dead_annot ca =
       is_unrolled_completely spec
   | AAssert([],p)
   | AInvariant([],_,p) ->
-      p.tp_kind <> Check && is_predicate false p.tp_statement
+      Logic_utils.use_predicate p.tp_kind && is_predicate false p.tp_statement
   | _ -> false
 
 let is_dead_code stmt =

src/plugins/wp/wpStrategy.ml

@@ -24,6 +24,7 @@ let dkey = Wp_parameters.register_category "strategy" (* debugging key *)
 let debug fmt = Wp_parameters.debug ~dkey fmt
 
 open Cil_types
+open Logic_utils
 open LogicUsage
 
 (* -------------------------------------------------------------------------- *)
@@ -171,7 +172,7 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
     Logic_const.(pat (p,pre_label))
   in
   let requires =
-    List.filter (fun x -> x.ip_content.tp_kind <> Check) bhv.b_requires
+    List.filter (fun x -> use_predicate x.ip_content.tp_kind) bhv.b_requires
   in
   let requires = Logic_const.pands (List.map norm_pred requires) in
   let assumes = Logic_const.pands (List.map norm_pred bhv.b_assumes) in
@@ -183,21 +184,23 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
   add_prop acc kind id p
 
 let add_prop_fct_pre acc kind kf bhv ~assumes pre =
-  if pre.ip_content.tp_kind = Check then acc else begin
+  if use_predicate pre.ip_content.tp_kind then begin
     let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
     let labels = NormAtLabels.labels_fct_pre in
     let p = Logic_const.pred_of_id_pred pre in
     let p = Logic_const.(pat (p,pre_label)) in
     let p = normalize id ?assumes labels p in
     add_prop acc kind id p
-  end
+  end else acc
 
 let add_prop_fct_post acc kind kf  bhv tkind post =
-  let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
-  let labels = NormAtLabels.labels_fct_post in
-  let p = Logic_const.pred_of_id_pred post in
-  let p = normalize id labels p in
-  add_prop acc kind id p
+  if verify_predicate post.ip_content.tp_kind then begin
+    let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
+    let labels = NormAtLabels.labels_fct_post in
+    let p = Logic_const.pred_of_id_pred post in
+    let p = normalize id labels p in
+    add_prop acc kind id p
+  end else acc
 
 let add_prop_fct_bhv_pre acc kind kf bhv =
   let assumes = None in
@@ -206,11 +209,13 @@ let add_prop_fct_bhv_pre acc kind kf bhv =
   List.fold_left add acc bhv.b_assumes
 
 let add_prop_stmt_pre acc kind kf s bhv ~assumes pre =
-  let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
-  let labels = NormAtLabels.labels_stmt_pre ~kf s in
-  let p = Logic_const.pred_of_id_pred pre in
-  let p = normalize id labels ?assumes p in
-  add_prop acc kind id p
+  if use_predicate pre.ip_content.tp_kind then begin
+    let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
+    let labels = NormAtLabels.labels_stmt_pre ~kf s in
+    let p = Logic_const.pred_of_id_pred pre in
+    let p = normalize id labels ?assumes p in
+    add_prop acc kind id p
+  end else acc
 
 let add_prop_stmt_bhv_requires acc kind kf s bhv ~with_assumes =
   let assumes =
@@ -227,11 +232,13 @@ let add_prop_stmt_spec_pre acc kind kf s spec =
   in List.fold_left add_bhv_pre acc spec.spec_behavior
 
 let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
-  let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
-  let labels = NormAtLabels.labels_stmt_post ~kf s l_post in
-  let p = Logic_const.pred_of_id_pred post in
-  let p = normalize id labels ?assumes p in
-  add_prop acc kind id p
+  if verify_predicate post.ip_content.tp_kind then begin
+    let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
+    let labels = NormAtLabels.labels_stmt_post ~kf s l_post in
+    let p = Logic_const.pred_of_id_pred post in
+    let p = normalize id labels ?assumes p in
+    add_prop acc kind id p
+  end else acc
 
 let update_kind kind pre =
   if pre.ip_content.tp_kind = Check then begin