diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index dc9123908981c12063b1e803d5ed09ccea31fbf2..e6eae23d70bc2188c05864ec06ac01ad72a44682 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -338,19 +338,57 @@ let merge_distinct_emitted x y = match x, y with
| False_if_reachable, True | True, False_if_reachable ->
raise Unmergeable
+type property_kind =
+ | Hypothesis (* Admitted property with a [Considered_valid] status. *)
+ | Unverifiable (* Postconditions and assigns of functions without code. *)
+ | Consequence of Property.identified_property list (* Logical consequence. *)
+ | Tautology (* Always valid. *)
+ | Ignored (* Property with no logical status. *)
+ | Other
+
let is_admitted_code_annot = function
| Cil_types.AAssert (_, tp)
| Cil_types.AInvariant (_, _, tp) -> tp.tp_kind = Admit
| _ -> false
let rec is_admitted = function
+ | Property.IPAxiom _ -> true
| Property.IPPredicate ip -> ip.ip_pred.ip_content.tp_kind = Admit
- | IPAxiom _ -> true
| IPLemma lemma -> lemma.il_pred.tp_kind = Admit
| IPCodeAnnot ca -> is_admitted_code_annot ca.ica_ca.annot_content
| IPPropertyInstance instance -> is_admitted instance.ii_ip
| _ -> false
+let is_verifiable = function
+ | Property.IPPredicate {ip_kind = PKEnsures _ | PKTerminates; ip_kf = kf }
+ | IPAssigns {ias_kf = kf}
+ | IPFrom {if_kf = kf}
+ | IPAllocation {ial_kf = kf} -> Kernel_function.has_definition kf
+ | _ -> true
+
+let property_kind = function
+ | Property.IPAxiomatic {iax_props} -> Consequence iax_props
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
+ (* logical consequence of its postconditions *)
+ let active = Datatype.String.Set.elements ib_active in
+ let post = Property.ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv in
+ Consequence post
+ | IPReachable {ir_kf; ir_kinstr; ir_program_point} ->
+ begin
+ match ir_kf, ir_kinstr, ir_program_point with
+ | None, Kglobal, Before -> Tautology
+ | None, Kglobal, After -> assert false
+ | None, Kstmt _, _ ->
+ Kernel.fatal "reachability of a stmt without function"
+ | Some kf, Kglobal, Before when Kernel_function.is_main kf -> Tautology
+ | _ -> Other
+ end
+ | p ->
+ if Property.has_status p then
+ if is_admitted p then Hypothesis else
+ if is_verifiable p then Other else Unverifiable
+ else Ignored
+
module Register_hook = Hook.Build (struct type t = Property.t end)
let register_property_add_hook = Register_hook.extend
@@ -369,71 +407,11 @@ let rec register ppt =
Register_hook.apply ppt;
register_as_kernel_logical_consequence ppt
-(* the functions below and this one MUST be synchronized *)
and register_as_kernel_logical_consequence ppt =
- let open Property in match ppt with
- | IPAxiom _
- | IPPredicate {ip_kind = PKAssumes _} ->
- (* always valid, but must be verifiable by the end-user,
- see [is_not_verifiable_but_valid] *)
- ()
- | IPAxiomatic {iax_props} -> logical_consequence Emitter.kernel ppt iax_props
- | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
- let active = Datatype.String.Set.elements ib_active in
- (* logical consequence of its postconditions *)
- logical_consequence
- Emitter.kernel ppt (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv)
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- (* valid: global properties are always reachable *)
- emit_valid ppt
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = After} ->
- assert false
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kstmt _} ->
- Kernel.fatal "reachability of a stmt without function"
- | IPReachable {ir_kf = Some kf; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- let f = kf.Cil_types.fundec in
- if Ast_info.Function.get_name f = Kernel.MainFunction.get_plain_string ()
- (* main is always reachable *)
- then emit_valid ppt
- | IPOther _ | IPReachable _
- | IPExtended _
- | IPPredicate _ | IPCodeAnnot _ | IPComplete _
- | IPDisjoint _ | IPAssigns _ | IPFrom _
- | IPAllocation _ | IPDecrease _ | IPLemma _
- | IPPropertyInstance _
- | IPTypeInvariant _ | IPGlobalInvariant _ ->
- ()
-
-(* the functions above and below MUST be synchronized *)
-and is_kernel_logical_consequence ppt =
- let open Property in match ppt with
- | IPPredicate {ip_kind = PKAssumes _}
- | IPBehavior _
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- true
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = After} ->
- assert false
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kstmt _} ->
- Kernel.fatal "reachability of a stmt without function"
- | IPReachable {ir_kf = Some kf; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- let f = kf.Cil_types.fundec in (* main is always reachable *)
- Ast_info.Function.get_name f = Kernel.MainFunction.get_plain_string ()
- | IPAxiom _
- | IPExtended _
- | IPAxiomatic _
- | IPOther _ | IPReachable _
- | IPPredicate _ | IPCodeAnnot _ | IPComplete _
- | IPDisjoint _ | IPAssigns _ | IPFrom _
- | IPAllocation _ | IPDecrease _ | IPLemma _
- | IPPropertyInstance _
- | IPTypeInvariant _ | IPGlobalInvariant _ ->
- false
+ match property_kind ppt with
+ | Consequence ips -> logical_consequence Emitter.kernel ppt ips
+ | Tautology -> emit_valid ppt
+ | Hypothesis | Unverifiable | Ignored | Other -> ()
and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
Kernel.feedback ~dkey:Kernel.dkey_prop_status_emit
@@ -505,7 +483,7 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
(match hyps with
| [] ->
let reach_ppt = Property.ip_reachable_ppt ppt in
- if is_kernel_logical_consequence reach_ppt then emit_valid reach_ppt;
+ if property_kind reach_ppt = Tautology then emit_valid reach_ppt;
add { emitter with properties = [ reach_ppt ] } s
| _ :: _ -> Kernel.fatal "Emitter %a proves invalidity of %a under \
hypotheses: unsound!" Emitter.pretty e Property.pretty ppt));
@@ -555,24 +533,13 @@ let () =
register_as_kernel_logical_consequence
let emit_and_get e ~hyps ppt ?distinct s =
- let open Property in begin match ppt with
- | IPBehavior _ | IPAxiom _ | IPAxiomatic _
- | IPPredicate {ip_kind = PKAssumes _} ->
- Kernel.fatal
- "only the kernel should set the status of property %a"
- pretty
- ppt
- | IPPredicate _ | IPCodeAnnot _ | IPComplete _
- | IPDisjoint _ | IPAssigns _ | IPFrom _
- | IPDecrease _ | IPLemma _ | IPReachable _
- | IPAllocation _ | IPOther _
- | IPPropertyInstance _
- | IPExtended _
- | IPTypeInvariant _ | IPGlobalInvariant _ -> ()
- end;
- if is_admitted ppt
- then True (* TODO: fail here? *)
- else unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
+ match property_kind ppt with
+ | Hypothesis | Consequence _ | Ignored ->
+ Kernel.fatal
+ "Only the kernel should set the status of property %a (%a, %a)"
+ Property.pretty ppt Emitter.pretty e Emitted_status.pretty s
+ | Other | Tautology | Unverifiable ->
+ unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
let emit e ~hyps ppt ?distinct s = ignore (emit_and_get e ~hyps ppt ?distinct s)
@@ -660,33 +627,10 @@ let conjunction s1 s2 = match s1, s2 with
| True, True -> True
let is_not_verifiable_but_valid ppt status =
- is_admitted ppt ||
- match status with
- | Never_tried ->
- (match ppt with
- | Property.IPOther _ ->
- (* Non-ACSL properties are not verifiable *)
- false
- | Property.IPReachable _ -> false
- | Property.IPAxiom _ | Property.IPAxiomatic _ -> true
- | _ ->
- match Property.get_kf ppt with
- | None -> false
- | Some kf ->
- (* cannot use module [Kernel_function] nor [Globals] here *)
- let f = kf.Cil_types.fundec in
- if Ast_info.Function.is_definition f then
- false
- else
- (* postconditions of functions without code are not verifiable *)
- let open Property in match ppt with
- | IPPredicate {ip_kind = PKEnsures _ | PKTerminates}
- | IPAssigns _ | IPAllocation _
- | IPFrom _ -> true
- | _ -> false)
- | Best((True | False_if_reachable | False_and_reachable | Dont_know), _)
- | Inconsistent _ ->
- false
+ match property_kind ppt with
+ | Hypothesis -> true
+ | Unverifiable -> status = Never_tried
+ | Other | Consequence _ | Tautology | Ignored -> false
let rec compute_automatic_status _e properties =
let local_get p =
@@ -734,12 +678,8 @@ and get_status ?(must_register=true) ppt =
match ppt with
| Property.IPOther _ | Property.IPReachable _
| Property.IPPropertyInstance _ ->
- if must_register then begin
- register ppt;
- if is_kernel_logical_consequence ppt then get_status ppt
- else Never_tried
- end else
- Never_tried
+ if must_register then register ppt;
+ Never_tried
| Property.IPBehavior _
| Property.IPExtended _
| Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
@@ -755,24 +695,25 @@ and get_status ?(must_register=true) ppt =
let get ppt = get_status ppt
let automatically_proven ppt =
- is_kernel_logical_consequence ppt
- &&
- (* nobody else tried to prove it *)
- try
- let by_emitter = Status.find ppt in
+ match property_kind ppt with
+ | Hypothesis | Unverifiable | Ignored | Other -> false
+ | Consequence _ | Tautology ->
+ (* nobody else tried to prove it *)
try
- Emitter_with_properties.Hashtbl.iter
- (fun e _ ->
- if not (Emitter.equal
- (Emitter.Usable_emitter.get e.emitter)
- Emitter.kernel)
- then raise Exit)
- by_emitter;
+ let by_emitter = Status.find ppt in
+ try
+ Emitter_with_properties.Hashtbl.iter
+ (fun e _ ->
+ if not (Emitter.equal
+ (Emitter.Usable_emitter.get e.emitter)
+ Emitter.kernel)
+ then raise Exit)
+ by_emitter;
+ true
+ with Exit ->
+ false
+ with Not_found ->
true
- with Exit ->
- false
- with Not_found ->
- true
(**************************************************************************)