diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 654ecfa161c9ec36f57379ff101be547cecbecc1..06322b509861441f6af05e12df251c5162ce0a6d 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -807,6 +807,23 @@ struct
let addrs = C.logic env t in
p_all (L.initialized sigma) (L.region (Ctypes.object_of te) addrs)
+ let call_pred env f ls es =
+ match C.logic_info env f with
+ | Some p ->
+ if ls <> [] || es <> [] then
+ Warning.error "Unexpected parameters for named predicate '%a'"
+ Logic_info.pretty f ; p
+ | None ->
+ let empty ls =
+ if ls <> [] then
+ Warning.error "Unexpected labels for purely logic '%a'"
+ Logic_info.pretty f ;
+ in
+ match LogicBuiltins.logic f with
+ | ACSLDEF -> C.call_pred env f ls es
+ | HACK phi -> empty ls ; F.p_bool (phi es)
+ | LFUN p -> empty ls ; p_call p es
+
let predicate polarity env p =
match p.pred_content with
| Pfalse -> p_false
@@ -833,24 +850,7 @@ struct
| _ -> Warning.error "\\subset requires 2 arguments"
end
| Papp(f,ls,ts) ->
- begin
- match C.logic_info env f with
- | Some p ->
- if ls <> [] || ts <> [] then
- Warning.error "Unexpected parameters for named predicate '%a'"
- Logic_info.pretty f ; p
- | None ->
- let empty ls =
- if ls <> [] then
- Warning.error "Unexpected labels for purely logic '%a'"
- Logic_info.pretty f ;
- in
- let es = List.map (val_of_term env) ts in
- match LogicBuiltins.logic f with
- | ACSLDEF -> C.call_pred env f ls es
- | HACK phi -> empty ls ; F.p_bool (phi es)
- | LFUN p -> empty ls ; p_call p es
- end
+ call_pred env f ls @@ List.map (val_of_term env) ts
| Plet( { l_var_info=v ; l_body=LBterm a } , p ) ->
let va = C.logic env a in
diff --git a/src/plugins/wp/Sigs.mli b/src/plugins/wp/Sigs.mli
index 83335aaf4119b97eb8924ec181f00f201c45c44b..e8a2b331fbb88c39682c3ed6910505d9c12ae2ca 100644
--- a/src/plugins/wp/Sigs.mli
+++ b/src/plugins/wp/Sigs.mli
@@ -796,6 +796,11 @@ sig
underlying memory model. *)
val pred : polarity -> env -> Cil_types.predicate -> pred
+ (** Compile a predicate call. *)
+ val call_pred:
+ env -> Cil_types.logic_info -> Cil_types.logic_label list -> term list ->
+ pred
+
(** Compile a term representing a set of memory locations into an abstract
region. *)
val region : env -> Cil_types.term -> region
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 044184ea98f9c62e27ed682b0f220ed913f5e797..d6bc77f086a4b5a1202344190d8a0425ff607b53 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -250,6 +250,9 @@ let get_decreases_goal kf =
| None -> None
| Some v -> Some (defined v)
+let get_decreases_hyp kf =
+ Annotations.decreases ~populate:false kf
+
(* -------------------------------------------------------------------------- *)
(* --- Contracts --- *)
(* -------------------------------------------------------------------------- *)
@@ -262,6 +265,7 @@ type contract = {
contract_smoke : WpPropId.pred_info list ;
contract_assigns : Cil_types.assigns ;
contract_terminates : bool * Cil_types.predicate ;
+ contract_decreases : Cil_types.variant option ;
}
let assigns_upper_bound behaviors =
@@ -338,6 +342,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| Writes froms -> Writes (normalize_froms Normal froms)
in
let terminates = get_terminates_hyp kf in
+ let decreases = get_decreases_hyp kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
@@ -346,6 +351,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
contract_smoke = [] ;
contract_assigns = assigns ;
contract_terminates = terminates ;
+ contract_decreases = decreases ;
}
end)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 53c1c4659e4eee89d24c38360ef7b054af202a9d..adfbe70680a6c211384c0e3d799a2ac57b478dba 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -118,6 +118,7 @@ type contract = {
contract_smoke : pred_info list ;
contract_assigns : assigns ;
contract_terminates : bool * predicate ; (* boolean: assumed terminates *)
+ contract_decreases : variant option ;
}
val get_call_contract : ?smoking:stmt -> kernel_function -> stmt -> contract
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 4fba7b07405c29adbe274cefd5e4695299d724c2..c7a4a5d656b4f2e1dc93e8e75671ae3035fd1cbe 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -188,7 +188,7 @@ struct
let prove_property env (p : WpPropId.pred_info) w =
if is_selected ~goal:true env p then W.add_goal env.we p w else w
- let prove_subproperty env (p : WpPropId.pred_info) ?deps prop stmt source w =
+ let prove_subproperty env p ?deps prop stmt source w =
if is_selected ~goal:true env p
then W.add_subgoal env.we ?deps p prop stmt source w
else w
@@ -367,15 +367,31 @@ struct
W.call_goal_precond env.we s kf es ~pre w_call
else w_call
in
- match env.terminates with
- | Some p when is_default_bhv env.mode && is_selected ~goal:true env p ->
- let generated, callee_t = c.contract_terminates in
- if generated then
- Wp_parameters.warning ~once:true
- "Missing terminates clause on call to %a, defaults to %a"
- Kernel_function.pretty kf Cil_printer.pp_predicate callee_t ;
- W.call_terminates env.we p s kf es ~callee_t w_pre
- | _ -> w_pre
+ let callee_t =
+ (** TODO when kernel terminates complete: remove this code. *)
+ let generated, callee_t = c.contract_terminates in
+ if generated && env.terminates <> None then
+ Wp_parameters.warning ~once:true
+ "Missing terminates clause on call to %a, defaults to %a"
+ Kernel_function.pretty kf Cil_printer.pp_predicate callee_t ;
+ Some callee_t
+ in
+ let selected t = is_selected ~goal:true env t && is_default_bhv env.mode in
+ let in_cluster = CfgInfos.in_cluster ~caller:env.mode.kf kf in
+ let w_term = match env.terminates with
+ | Some t when selected t ->
+ W.call_terminates env.we s kf es t ?callee_t w_pre
+ | _ -> w_pre
+ in
+ let w_decr = match env.decreases with
+ | Some d when selected d && in_cluster ->
+ W.call_decreases env.we s kf es d
+ ?caller_t:(Option.map snd env.terminates)
+ ?callee_d:c.contract_decreases
+ w_term
+ | _ -> w_term
+ in
+ w_decr
let do_complete_disjoint env w =
if not (is_default_bhv env.mode) then w
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index c38b30c4127d6bf3949afa58487cfdeaaab2c9c4..6b348971f63e6ac6627e1b827337de79d0c9fc12 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -111,13 +111,12 @@ let add_goal env (pid,pred) k =
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
-let add_subgoal env (pid, t_pred) ?deps prop stmt _source k =
+let add_subgoal env (pid, _) ?deps prop stmt _source k =
ignore deps ;
let u = node () in
if Wp_parameters.debug_atleast 1 then
- Format.fprintf !out " %a [ color=red , label=\"Prove %a @@ %a (%a)\" ] ;@."
+ Format.fprintf !out " %a [ color=red , label=\"Prove %a (%a)\" ] ;@."
pretty u
- Printer.pp_predicate t_pred
Cil_printer.pp_stmt stmt
Printer.pp_predicate prop
else
@@ -245,16 +244,49 @@ let call_goal_precond env _stmt kf _es ~pre k =
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
-let call_terminates env (_gpid, prop) _stmt kf _es ~callee_t k =
- let _ = callee_t in
+let call_terminates env _stmt kf _es (_gpid, prop) ?callee_t k =
let u = node () in
- Format.fprintf !out " %a [ color=red , label=\"Prove PreCond %a%t\" ] ;@."
+ let pp_opt_pred = Pretty_utils.pp_opt ~none:"FALSE" Printer.pp_predicate in
+ Format.fprintf !out " %a [ color=red , label=\"Prove Terminates %a%t\" ] ;@."
pretty u Kernel_function.pretty kf
begin fun fmt ->
if Wp_parameters.debug_atleast 1 then
Format.fprintf fmt "\n@[<hov 2>Terminates if %a[%s] ==> %a[%a];@]"
Printer.pp_predicate prop "Caller"
- Printer.pp_predicate callee_t Kernel_function.pretty kf
+ pp_opt_pred callee_t
+ Kernel_function.pretty kf
+ end ;
+ Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
+ merge env u k
+
+let call_decreases env _s kf _es (_id, (caller_d, rel)) ?caller_t ?callee_d k =
+ let u = node () in
+ let pp_opt_pred = Pretty_utils.pp_opt ~none:"TRUE" Printer.pp_predicate in
+ let pp_rel fmt callee_d =
+ match rel with
+ | None ->
+ Format.fprintf fmt "%a ==> %a[%a] < %a[%s] && %a[%a] >= 0"
+ pp_opt_pred caller_t
+ Printer.pp_term callee_d Kernel_function.pretty kf
+ Printer.pp_term caller_d "Caller"
+ Printer.pp_term callee_d Kernel_function.pretty kf
+ | Some rel ->
+ Format.fprintf fmt "%a ==> %a(%a[%s], %a[%a])"
+ pp_opt_pred caller_t
+ Printer.pp_logic_info rel
+ Printer.pp_term caller_d "Caller"
+ Printer.pp_term callee_d Kernel_function.pretty kf
+ in
+ Format.fprintf !out " %a [ color=red , label=\"Prove Decreases %a%t\" ] ;@."
+ pretty u Kernel_function.pretty kf
+ begin fun fmt ->
+ match callee_d with
+ | None ->
+ Format.fprintf fmt "\n@[<hov 2>Decreases if %a ==> FALSE;@]"
+ pp_opt_pred caller_t
+ | Some (callee_d, _) ->
+ if Wp_parameters.debug_atleast 1 then
+ Format.fprintf fmt "\n@[<hov 2>Decreases if %a;@]" pp_rel callee_d
end ;
Format.fprintf !out " %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
merge env u k
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index c3fa404c7e5b3c500ed9b1893c1f0c304c660950..fb4d49fc6e481c6cfbcf41ad6aa1915b6e587180 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -208,7 +208,7 @@ module Callees = WpContext.StaticGenerator(Kernel_function)
module RecursiveClusters : sig
val is_recursive : Kernel_function.t -> bool
- val get_cluster : Kernel_function.t -> Kernel_function.Set.t option
+ val in_cluster : caller:Kernel_function.t -> Kernel_function.t -> bool
end =
struct
(* Tarjan's algorithm, adapted from:
@@ -287,10 +287,15 @@ struct
let is_recursive kf =
(* in a recursive cluster or contains unspecified function pointer call *)
None <> get_cluster kf || [] <> snd @@ Callees.get kf
+
+ let in_cluster ~caller callee =
+ match get_cluster caller with
+ | None -> false
+ | Some cluster -> Fset.mem callee cluster
end
let is_recursive = RecursiveClusters.is_recursive
-let get_cluster = RecursiveClusters.get_cluster
+let in_cluster = RecursiveClusters.in_cluster
(* -------------------------------------------------------------------------- *)
(* --- No variant loops --- *)
@@ -433,11 +438,8 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Option.iter
begin fun (cfg : Cfg.automaton) ->
(* Spec Iteration *)
- if selected_decreases ~prop kf then
- Wp_parameters.warning
- "Unsupported clause @decreases in '%a' (ignored)"
- Kernel_function.pretty kf ;
- if selected_terminates ~prop kf ||
+ if selected_decreases ~prop kf ||
+ selected_terminates ~prop kf ||
selected_disjoint_complete kf ~bhv ~prop ||
(List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
then infos.annots <- true ;
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index ba6256d0099a60679a4f083661cdab56fc8b4761..b3daaf0164e7fc9fc2cb231930df62e82aada1b2 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -41,7 +41,7 @@ val unreachable : t -> Cfg.vertex -> bool
val terminates_deps : t -> Property.Set.t
val is_recursive : Kernel_function.t -> bool
-val get_cluster : Kernel_function.t -> Kernel_function.Set.t option
+val in_cluster : caller:Kernel_function.t -> Kernel_function.t -> bool
val trivial_terminates : int ref
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 97c136c1d4f285c2cc0117b7d9dd115951496e90..52ea8a59bff7868bc16adfb6e3df6d9ad284285f 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1054,47 +1054,137 @@ struct
(* --- WP RULE : call terminates --- *)
(* -------------------------------------------------------------------------- *)
- let call_terminates wenv (gpid, caller_t) stmt kf es ~callee_t wp =
+ let call_terminates wenv stmt kf args (id, caller_t) ?callee_t wp =
in_wenv wenv wp
(fun env wp ->
- let gid = Gsource(gpid, stmt, FromCall) in
let outcome = Warning.catch
- ~severe:true ~effect:"Can not prove call termination"
+ ~severe:true
+ ~effect:"Considering that call must always terminate"
(L.pred `Positive env) caller_t
in
+ let warn, caller_t = match outcome with
+ | Warning.Failed warn -> warn, p_true
+ | Warning.Result (warn, p) -> warn, p
+ in
+ let prove_terminates ~warn p =
+ add_vc (Gsource(id, stmt, FromCall)) ~warn (p_imply caller_t p)
+ in
+ let sigma = L.current env in
+ let outcome = Warning.catch
+ ~severe:true
+ ~effect:"Considering non terminating callee"
+ (List.map (C.exp sigma)) args in
match outcome with
- | Warning.Failed warn ->
- let vcs = add_vc gid ~warn p_false wp.vcs in
+ | Warning.Failed warn2 ->
+ let warn = W.union warn warn2 in
+ let vcs = prove_terminates ~warn p_false wp.vcs in
+ { wp with vcs = vcs }
+ | Warning.Result(warn2, args) ->
+ let warn = W.union warn warn2 in
+ let compile_callee = function
+ | None ->
+ Warning.error "No terminates clause for %a"
+ Kernel_function.pretty kf
+ | Some callee_t ->
+ let init = L.mem_at env Clabels.init in
+ let call = L.call kf args in
+ let call_e = L.mk_env ~here:sigma () in
+ let call_f = L.call_pre init call sigma in
+ L.in_frame call_f (L.pred `Positive call_e) callee_t
+ in
+ let outcome =
+ Warning.catch
+ ~severe:true ~effect:"Considering non terminating callee"
+ compile_callee callee_t
+ in
+ let warn2, callee_t = match outcome with
+ | Warning.Failed warn -> warn, p_false
+ | Warning.Result(warn,callee_t) -> warn, callee_t
+ in
+ let warn = W.union warn warn2 in
+ let vcs = prove_terminates ~warn callee_t wp.vcs in
+ { wp with vcs = vcs })
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- WP RULE : call decreases --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let call_decreases wenv stmt kf args (id, caller_d) ?caller_t ?callee_d wp =
+ in_wenv wenv wp
+ (fun env wp ->
+ let compile_caller_t caller_t =
+ if not @@ Wp_parameters.TerminatesVariantHyp.get () then p_true
+ else match caller_t with
+ | None -> p_true
+ | Some t -> (L.pred `Positive env) t
+ in
+ let outcome = Warning.catch
+ ~severe:true
+ ~effect:"Considering that call must always decrease"
+ compile_caller_t caller_t
+ in
+ let warn, caller_t = match outcome with
+ | Warning.Failed warn -> warn, p_true
+ | Warning.Result (warn, p) -> warn, p
+ in
+ let prove_decreases ~warn p =
+ add_vc (Gsource(id, stmt, FromCall)) ~warn (p_imply caller_t p)
+ in
+ let sigma = L.current env in
+ let outcome = Warning.catch
+ ~severe:true
+ ~effect:"Considering non decreasing call"
+ (List.map (C.exp sigma)) args in
+ match outcome with
+ | Warning.Failed warn2 ->
+ let warn = W.union warn warn2 in
+ let vcs = prove_decreases ~warn p_false wp.vcs in
{ wp with vcs = vcs }
- | Warning.Result(warn, caller_t) ->
- let sigma = L.current env in
- let outcome = Warning.catch
- ~severe:true ~effect:"Can not prove call preconditions"
- (List.map (C.exp sigma)) es in
- match outcome with
- | Warning.Failed warn2 ->
- let warn = W.union warn warn2 in
- let vcs = add_vc gid ~warn p_false wp.vcs in
- { wp with vcs = vcs }
- | Warning.Result(warn2, vs) ->
- let warn = W.union warn warn2 in
- let init = L.mem_at env Clabels.init in
- let call = L.call kf vs in
- let call_e = L.mk_env ~here:sigma () in
- let call_f = L.call_pre init call sigma in
- let outcome = Warning.catch
- ~severe:true ~effect:"Can not prove call precondition"
- (L.in_frame call_f (L.pred `Positive call_e)) callee_t in
- match outcome with
- | Warning.Result(warn3,callee_t) ->
- let warn = W.union warn warn3 in
- let goal = p_imply caller_t callee_t in
- let vcs = add_vc gid ~warn goal wp.vcs in
- { wp with vcs = vcs }
- | Warning.Failed warn3 ->
- let warn = W.union warn warn3 in
- let vcs = add_vc gid ~warn p_false wp.vcs in
- { wp with vcs = vcs })
+ | Warning.Result(warn2, args) ->
+ let warn = W.union warn warn2 in
+ let init = L.mem_at env Clabels.init in
+ let call = L.call kf args in
+ let call_e = L.mk_env ~here:sigma () in
+ let call_f = L.call_pre init call sigma in
+ let compile_decreases (caller_d, callee_d) =
+ match caller_d, callee_d with
+ | _, None ->
+ Warning.error "No decreases clause for %a"
+ Kernel_function.pretty kf
+ | (_, r), Some (_, r')
+ when not @@ Option.equal Logic_utils.is_same_logic_info r r' ->
+ Warning.error
+ "On call to %a, decreases relation (%a) does not match \
+ caller relation (%a)"
+ Kernel_function.pretty kf
+ (Pretty_utils.pp_opt Cil_printer.pp_logic_info) r
+ (Pretty_utils.pp_opt Cil_printer.pp_logic_info) r'
+ | (caller_d, rel), Some (callee_d,_ ) ->
+ let rel caller callee = match rel with
+ | None ->
+ p_and (p_leq e_zero callee) (p_lt callee caller)
+ | Some rel ->
+ (L.in_frame call_f (L.call_pred call_e))
+ rel [] [caller ; callee]
+ in
+ let caller_d = L.term env caller_d in
+ let callee_d =
+ (L.in_frame call_f (L.term call_e)) callee_d in
+ rel caller_d callee_d
+ in
+ let outcome =
+ Warning.catch
+ ~severe:true ~effect:"Considering non decreasing call"
+ compile_decreases (caller_d, callee_d)
+ in
+ let warn2, pred = match outcome with
+ | Warning.Failed warn -> warn, p_false
+ | Warning.Result (warn, p) -> warn, p
+ in
+ let warn = W.union warn warn2 in
+ let vcs = prove_decreases ~warn pred wp.vcs in
+ { wp with vcs = vcs })
+
(* -------------------------------------------------------------------------- *)
(* --- WP RULE : call postcondition --- *)
diff --git a/src/plugins/wp/mcfg.mli b/src/plugins/wp/mcfg.mli
index 3afad69feed2e4d4e6fcd96525a437f27dfd6306..881d303b667a1abad001661a268c50e40fbb6cab 100644
--- a/src/plugins/wp/mcfg.mli
+++ b/src/plugins/wp/mcfg.mli
@@ -68,7 +68,7 @@ module type S = sig
val add_hyp :
?for_pid:WpPropId.prop_id -> t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
- val add_subgoal : t_env -> WpPropId.pred_info -> ?deps:Property.Set.t ->
+ val add_subgoal : t_env -> WpPropId.prop_id * 'a -> ?deps:Property.Set.t ->
predicate -> stmt -> WpPropId.effect_source -> t_prop -> t_prop
val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
@@ -104,9 +104,15 @@ module type S = sig
pre: WpPropId.pred_info list ->
t_prop -> t_prop
- val call_terminates : t_env -> WpPropId.pred_info ->
- stmt -> kernel_function -> exp list ->
- callee_t:predicate -> t_prop -> t_prop
+ val call_terminates : t_env -> stmt ->
+ kernel_function -> exp list ->
+ WpPropId.pred_info -> ?callee_t:predicate -> t_prop -> t_prop
+
+ val call_decreases : t_env -> stmt ->
+ kernel_function -> exp list ->
+ WpPropId.variant_info ->
+ ?caller_t: predicate ->
+ ?callee_d: variant -> t_prop -> t_prop
val call : t_env -> stmt ->
lval option -> kernel_function -> exp list ->
diff --git a/src/plugins/wp/tests/wp_acsl/clusters.i b/src/plugins/wp/tests/wp_acsl/clusters.i
index c1a2e71653c867c4a4cb93eba854d6f5f55f69fa..a1e3eba197178d084f1726464472e84aecb4a340 100644
--- a/src/plugins/wp/tests/wp_acsl/clusters.i
+++ b/src/plugins/wp/tests/wp_acsl/clusters.i
@@ -33,7 +33,7 @@ void mutual_1(unsigned n){
// succeeds termination
//@ decreases n ;
void mutual_2(unsigned n){
- if(n) mutual_1(n-1);
+ if(n) mutual_1(n-1); // fails decreases: no decreases for mutual_1
simpl_rf(n); // this does not prevent termination proof
}
@@ -52,7 +52,7 @@ void fp(void (*)(unsigned), unsigned);
//@ decreases n ;
void function(unsigned n){
- if(n) fp(&function, n-1);
+ if(n) fp(&function, n-1); // fails decreases: no decreases for fp
}
// termination fails : recursion without decreases
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
index 22929c54f81d6ef7379d18ccc6ed9f303796e754..61a3435b5bbc033d1871b398ddf626f180645976 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
@@ -9,18 +9,12 @@
Missing terminates clause for caller_no_cluster, populates 'terminates \true'
[wp] clusters.i:60: Warning:
Missing terminates clause for fp, populates 'terminates \true'
-[wp] clusters.i:60: Warning:
- Unsupported clause @decreases in 'function' (ignored)
[wp] clusters.i:54: Warning:
Missing terminates clause for function, populates 'terminates \true'
[wp] clusters.i:28: Warning:
Missing terminates clause for mutual_1, populates 'terminates \true'
-[wp] clusters.i:60: Warning:
- Unsupported clause @decreases in 'mutual_2' (ignored)
[wp] clusters.i:35: Warning:
Missing terminates clause for mutual_2, populates 'terminates \true'
-[wp] clusters.i:60: Warning:
- Unsupported clause @decreases in 'simpl_r' (ignored)
[wp] clusters.i:11: Warning:
Missing terminates clause for simpl_r, populates 'terminates \true'
[wp] clusters.i:15: Warning:
@@ -29,8 +23,10 @@
No 'decreases' clause on recursive function 'simpl_rf', cannot prove termination
[wp] clusters.i:60: Warning:
No 'decreases' clause on recursive function 'mutual_1', cannot prove termination
+[wp] clusters.i:36: Warning: No decreases clause for mutual_1
[wp] clusters.i:60: Warning:
No 'decreases' clause on recursive function 'fp', cannot prove termination
+[wp] clusters.i:55: Warning: No decreases clause for fp
------------------------------------------------------------
Function caller_no_cluster
------------------------------------------------------------
@@ -67,6 +63,16 @@ Prove: true.
------------------------------------------------------------
+Goal Recursion variant:
+Call Effect at line 55
+clusters.i:55: warning from wp:
+ - Warning: Considering non decreasing call, looking for context inconsistency
+ Reason: No decreases clause for fp
+Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
+Prove: false.
+
+------------------------------------------------------------
+
Goal Instance of 'Pre-condition (file clusters.i, line 59) in 'fp'' in 'function' at call 'fp' (file clusters.i, line 55)
:
Prove: true.
@@ -93,6 +99,16 @@ Prove: false.
Goal Termination-condition (generated) in 'mutual_2':
Prove: true.
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 36
+clusters.i:36: warning from wp:
+ - Warning: Considering non decreasing call, looking for context inconsistency
+ Reason: No decreases clause for mutual_1
+Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
+Prove: false.
+
------------------------------------------------------------
------------------------------------------------------------
Function simpl_r
@@ -101,6 +117,13 @@ Prove: true.
Goal Termination-condition (generated) in 'simpl_r':
Prove: true.
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 12
+Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
+Prove: to_uint32(n - 1) < n.
+
------------------------------------------------------------
------------------------------------------------------------
Function simpl_rf
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index cd339be06cf96cd4225b29340256672b0d64ab3b..08ae66d1fc233090df6da03de3c90f2809b26b87 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -4,6 +4,8 @@
[wp] Warning: Missing RTE guards
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
+[wp] tests/wp_acsl/terminates_formulae.i:90: Warning:
+ No 'decreases' clause on recursive function 'no_decreases', cannot prove termination
------------------------------------------------------------
Function base_call
------------------------------------------------------------
@@ -58,6 +60,36 @@ Goal Termination-condition (file terminates_formulae.i, line 27) in 'call_same':
Call Effect at line 29
Prove: true.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function decreases
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 77) in 'decreases':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 80
+Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
+Prove: to_uint32(n - 1) < n.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function general_decreases
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 83) in 'general_decreases':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 86
+Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
+Prove: P_Rel(n, to_uint32(n - 1)).
+
------------------------------------------------------------
------------------------------------------------------------
Function general_variant
@@ -72,6 +104,20 @@ 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_decreases
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 89) in 'no_decreases' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 89) in 'no_decreases' (2/2):
+Call Result at line 92
+Prove: false.
+
------------------------------------------------------------
------------------------------------------------------------
Function no_variant
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle
index 8e6f2960697c5548bc3cb90393df4ce92cd713b9..b7b48261bc0d1f853f89e289774ccae1298e46bd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/clusters.res.oracle
@@ -9,18 +9,12 @@
Missing terminates clause for caller_no_cluster, populates 'terminates \true'
[wp] clusters.i:60: Warning:
Missing terminates clause for fp, populates 'terminates \true'
-[wp] clusters.i:60: Warning:
- Unsupported clause @decreases in 'function' (ignored)
[wp] clusters.i:54: Warning:
Missing terminates clause for function, populates 'terminates \true'
[wp] clusters.i:28: Warning:
Missing terminates clause for mutual_1, populates 'terminates \true'
-[wp] clusters.i:60: Warning:
- Unsupported clause @decreases in 'mutual_2' (ignored)
[wp] clusters.i:35: Warning:
Missing terminates clause for mutual_2, populates 'terminates \true'
-[wp] clusters.i:60: Warning:
- Unsupported clause @decreases in 'simpl_r' (ignored)
[wp] clusters.i:11: Warning:
Missing terminates clause for simpl_r, populates 'terminates \true'
[wp] clusters.i:15: Warning:
@@ -29,31 +23,36 @@
No 'decreases' clause on recursive function 'simpl_rf', cannot prove termination
[wp] clusters.i:60: Warning:
No 'decreases' clause on recursive function 'mutual_1', cannot prove termination
+[wp] clusters.i:36: Warning: No decreases clause for mutual_1
[wp] clusters.i:60: Warning:
No 'decreases' clause on recursive function 'fp', cannot prove termination
-[wp] 12 goals scheduled
+[wp] clusters.i:55: Warning: No decreases clause for fp
+[wp] 15 goals scheduled
[wp] [Qed] Goal typed_simpl_r_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_simpl_r_variant : Valid
[wp] [Qed] Goal typed_simpl_rf_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_simpl_rf_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_mutual_1_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_mutual_1_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_mutual_2_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_mutual_2_variant : Unsuccess (Degenerated)
[wp] [Qed] Goal typed_caller_no_cluster_terminates : Valid
[wp] [Qed] Goal typed_fp_call_point_function_s41 : Valid
[wp] [Qed] Goal typed_fp_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fp_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_function_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_function_variant : Unsuccess (Degenerated)
[wp] [Qed] Goal typed_function_call_fp_requires : Valid
-[wp] Proved goals: 10 / 13
+[wp] Proved goals: 11 / 16
Qed: 9
- Alt-Ergo: 0 (unsuccess: 3)
+ Alt-Ergo: 1 (unsuccess: 5)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- simpl_r 1 - 1 100%
+ simpl_r 1 1 2 100%
simpl_rf 1 - 2 50.0%
mutual_1 1 - 2 50.0%
- mutual_2 1 - 1 100%
+ mutual_2 1 - 2 50.0%
caller_no_cluster 1 - 1 100%
fp 2 - 3 66.7%
- function 2 - 2 100%
+ function 2 - 3 66.7%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index 2beb6a738f11a1c2da19a7d9151bf108dabc747a..61f36ae2e4f9b9c7838a21b3561a4821e4641d59 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -4,7 +4,9 @@
[wp] Warning: Missing RTE guards
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
-[wp] 12 goals scheduled
+[wp] tests/wp_acsl/terminates_formulae.i:90: Warning:
+ No 'decreases' clause on recursive function 'no_decreases', cannot prove termination
+[wp] 18 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
@@ -17,9 +19,15 @@
[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: 10 / 14
- Qed: 6
- Alt-Ergo: 2 (unsuccess: 4)
+[wp] [Qed] Goal typed_decreases_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_decreases_variant : Valid
+[wp] [Qed] Goal typed_general_decreases_terminates : Valid
+[wp] [Alt-Ergo] Goal typed_general_decreases_variant : Valid
+[wp] [Qed] Goal typed_no_decreases_terminates_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_no_decreases_terminates_part2 : Unsuccess
+[wp] Proved goals: 15 / 20
+ Qed: 9
+ Alt-Ergo: 4 (unsuccess: 5)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
base_call - - 1 0.0%
@@ -30,4 +38,7 @@
variant 2 1 3 100%
general_variant 1 1 2 100%
no_variant 1 - 2 50.0%
+ decreases 1 1 2 100%
+ general_decreases 1 1 2 100%
+ no_decreases 1 - 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_formulae.i b/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
index 9cf88ab44eda973fe845a63f1563ee8f3d62623c..5a3e16c8827f5acab07ea3435f02d328c7c12c3d 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
+++ b/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
@@ -73,3 +73,20 @@ void no_variant(void){
//@ loop assigns i ;
for(unsigned i = 3; i > 0; --i);
}
+
+/*@ terminates Q ;
+ decreases n ; */
+void decreases(unsigned n){
+ if(n != 0) decreases(n-1) ;
+}
+
+/*@ terminates Q ;
+ decreases n for Rel; */
+void general_decreases(unsigned n){
+ if(n != 0) general_decreases(n-1) ;
+}
+
+/*@ terminates Q ; */
+void no_decreases(unsigned n){
+ if(n != 0) no_decreases(n-1) ;
+}
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 9da760aa83318e9b45a3a48faee66efe331cf235..8071f17896070904334e96daeee1a7036b250bc4 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -46,7 +46,8 @@ type prop_kind =
| 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 *)
- | PKSmoke (** expected to fail *)
+ | PKDecreases (** computation related to the decreases clause *)
+ | PKSmoke (** expected to fail *)
| PKPre of kernel_function * stmt * Property.t
(** precondition for function
at stmt, property of the require. Many information that should come
@@ -75,7 +76,6 @@ let tactical ~gid =
(* --- Category --- *)
(* -------------------------------------------------------------------------- *)
-let kind_of_id p = p.p_kind
let parts_of_id p = p.p_part
let property_of_id p = p.p_prop
let doomed_if_valid p = p.p_doomed
@@ -153,7 +153,7 @@ let mk_disj_bhv_id (kf,ki,active,disj) =
let mk_compl_bhv_id (kf,ki,active,comp) =
mk_prop PKProp (Property.ip_of_complete kf ki active comp)
let mk_decrease_id kf s x =
- mk_prop PKProp (Property.ip_of_decreases kf s x)
+ mk_prop PKDecreases (Property.ip_of_decreases kf s x)
let mk_lemma_id l = mk_prop PKProp (LogicUsage.ip_lemma l)
@@ -222,6 +222,7 @@ let kind_order = function
| PKTactic -> 11
| PKSmoke -> 12
| PKTerminates -> 13
+ | PKDecreases -> 14
let compare_kind k1 k2 = match k1, k2 with
PKPre (kf1, ki1, p1), PKPre (kf2, ki2, p2) ->
@@ -336,8 +337,6 @@ end = struct
let basename_of_prop_id p =
match p.p_kind , p.p_prop with
- | (PKTactic | PKCheck | PKProp | PKPropLoop | PKSmoke | PKTerminates) , p ->
- base_id_prop_txt p
| PKEstablished , p -> base_id_prop_txt p ^ "_established"
| PKPreserved , p -> base_id_prop_txt p ^ "_preserved"
| PKVarDecr , p -> base_id_prop_txt p ^ "_decrease"
@@ -350,6 +349,9 @@ end = struct
Kernel_function.get_name
(Kernel_function.find_englobing_kf stmt)
in Printf.sprintf "%s_call_%s" kf_name_of_stmt (base_id_prop_txt pre)
+ | _ , p ->
+ base_id_prop_txt p
+
(** function used to normalize basename *)
let normalize_basename s =
@@ -420,8 +422,6 @@ struct
let get_prop_id_base p =
match p.p_kind , p.p_prop with
- | (PKTactic | PKCheck | PKProp | PKPropLoop | PKSmoke | PKTerminates) , p ->
- get_ip p
| PKEstablished , p -> get_ip p ^ "_established"
| PKPreserved , p -> get_ip p ^ "_preserved"
| PKVarDecr , p -> get_ip p ^ "_decrease"
@@ -443,6 +443,9 @@ struct
ip_string)
in
call_string^"_"^ip_string
+ | _ , p ->
+ get_ip p
+
let get_prop_id_basename p =
let basename = get_prop_id_base p in
@@ -576,6 +579,7 @@ let label_of_kind = function
| PKAFctOut -> "Function assigns"
| PKAFctExit -> "Exit assigns"
| PKTerminates -> "Terminates"
+ | PKDecreases -> "Decreases"
| PKPre(kf,_,_) ->
Printf.sprintf "Precondition for '%s'" (Kernel_function.get_name kf)
@@ -592,7 +596,8 @@ struct
| None -> ()
| Some(k,n) -> fprintf fmt " (%d/%d)" (succ k) n
let pp_subprop fmt p = match p.p_kind with
- | PKProp | PKTactic | PKCheck | PKPropLoop | PKSmoke | PKTerminates -> ()
+ | PKProp | PKTactic | PKCheck | PKPropLoop | PKSmoke
+ | PKTerminates | PKDecreases -> ()
| PKEstablished -> pp_print_string fmt " (established)"
| PKPreserved -> pp_print_string fmt " (preserved)"
| PKVarDecr -> pp_print_string fmt " (decrease)"
@@ -673,6 +678,7 @@ let propid_hints hs p =
| PKAFctOut , _ -> add_required hs "return"
| PKAFctExit , _ -> add_required hs "exit"
| PKTerminates , _ -> add_required hs "terminates"
+ | PKDecreases , _ -> add_required hs "decreases"
| PKPre(kf,st,_) , _ ->
add_required hs ("precond-" ^ Kernel_function.get_name kf) ;
stmt_hints hs st
@@ -747,7 +753,7 @@ let prop_id_keys p =
let pp_goal_kind fmt = function
| PKTactic | PKSmoke | PKCheck
- | PKProp | PKPropLoop | PKAFctOut | PKAFctExit | PKTerminates
+ | PKProp | PKPropLoop | PKAFctOut | PKAFctExit | PKTerminates | PKDecreases
| PKPre _ -> ()
| PKEstablished -> Format.pp_print_string fmt "Establishment of "
| PKPreserved -> Format.pp_print_string fmt "Preservation of "
@@ -1059,7 +1065,7 @@ let split_map f pid gs =
let subproofs id = match id.p_kind with
| PKCheck -> 0
| PKProp | PKSmoke | PKTactic | PKPre _ | PKPropLoop
- | PKTerminates | PKVarRel -> 1
+ | PKTerminates | PKDecreases | PKVarRel -> 1
| PKEstablished | PKPreserved
| PKVarDecr | PKVarPos
| PKAFctExit | PKAFctOut -> 2
@@ -1067,7 +1073,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 | PKVarRel -> 0 (* 1/1 *)
+ | PKTerminates | PKDecreases | PKVarRel -> 0 (* 1/1 *)
| PKPreserved -> 0 (* 1/2 *)
| PKEstablished-> 1 (* 2/2 *)
| PKVarDecr -> 0 (* 1/2 *)
@@ -1117,7 +1123,8 @@ let get_induction p =
| IPAssigns {ias_kf; ias_kinstr=Kstmt stmt} -> Some (ias_kf, stmt)
| _ -> None
in match p.p_kind with
- | PKCheck|PKSmoke |PKAFctOut|PKAFctExit|PKPre _ | PKTactic| PKTerminates ->
+ | PKCheck | PKSmoke | PKAFctOut | PKAFctExit | PKPre _
+ | PKTactic | PKTerminates | PKDecreases ->
None
| PKProp ->
let loop_stmt_opt = match get_stmt (property_of_id p) with
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 559492ad8374b347e8226ecbca02b56a2cd1e674..469a8ee011df1accd813977b937c03d755ac237f 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -89,24 +89,6 @@ val are_selected_names: string list -> string list -> bool
(** [are_selected_names asked names] checks if [names] of a property are
selected according to [asked] names. *)
-type prop_kind =
- | PKTactic (** tactical sub-goal *)
- | PKCheck (** internal check *)
- | PKProp (** normal property *)
- | PKEstablished (** computation related to a loop property before the loop. *)
- | PKPreserved (** computation related to a loop property inside the loop. *)
- | 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 *)
- | PKSmoke (** smoke property *)
- | PKPre of kernel_function * stmt * Property.t (** precondition for function
- at stmt, property of the require. Many information that should come
- from the p_prop part of the prop_id, but in the PKPre case,
- it seems that it is hidden in a IPBlob property ! *)
val pretty : Format.formatter -> prop_id -> unit
val pretty_context : Description.kf -> Format.formatter -> prop_id -> unit
@@ -285,9 +267,6 @@ val split_map : (prop_id -> 'a -> 'b) -> prop_id -> 'a list -> 'b list
(** [mk_part pid (k, n)] build the identification for the [k/n] part of [pid].*)
val mk_part : prop_id -> (int * int) -> prop_id
-(** get the 'kind' information. *)
-val kind_of_id : prop_id -> prop_kind
-
(** get the 'part' information. *)
val parts_of_id : prop_id -> (int * int) option