From 93637166d5a2b551891ed70de19e43eaba1545dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 17 Feb 2021 19:11:58 +0100
Subject: [PATCH] [logic] pretty-printing predicate kinds
---
Makefile | 2 +-
src/kernel_services/ast_data/property.ml | 36 +++-----
.../ast_printing/cil_printer.ml | 85 ++++++++++++++-----
.../ast_printing/cil_printer.mli | 28 ++++++
.../ast_printing/description.ml | 9 +-
.../ast_printing/logic_print.ml | 28 ++----
src/plugins/gui/design.ml | 7 +-
src/plugins/obfuscator/obfuscate.ml | 5 +-
src/plugins/value/engine/transfer_logic.ml | 4 +-
src/plugins/value/legacy/eval_annots.ml | 4 +-
src/plugins/wp/LogicUsage.ml | 10 +--
11 files changed, 127 insertions(+), 91 deletions(-)
diff --git a/Makefile b/Makefile
index 73227de03b3..177271d48bc 100644
--- a/Makefile
+++ b/Makefile
@@ -526,8 +526,8 @@ KERNEL_CMO=\
src/kernel_services/ast_printing/cil_descriptive_printer.cmo \
src/kernel_services/parsetree/cabs.cmo \
src/kernel_services/parsetree/cabshelper.cmo \
- src/kernel_services/ast_printing/logic_print.cmo \
src/kernel_services/ast_queries/logic_utils.cmo \
+ src/kernel_services/ast_printing/logic_print.cmo \
src/kernel_internals/parsing/logic_parser.cmo \
src/kernel_internals/parsing/logic_lexer.cmo \
src/kernel_services/ast_queries/logic_typing.cmo \
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 26db9e82553..c4b3ce48fa4 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -420,10 +420,8 @@ let rec pretty_ip fmt = function
| IPExtended {ie_ext} -> Cil_printer.pp_extended fmt ie_ext
| IPAxiomatic {iax_name} -> Format.fprintf fmt "axiomatic@ %s" iax_name
| IPLemma {il_name; il_pred} ->
- (match il_pred.tp_kind with
- | Admit -> Format.fprintf fmt "axiom@ %s" il_name
- | Assert -> Format.fprintf fmt "lemma@ %s" il_name
- | Check -> Format.fprintf fmt "check lemma@ %s" il_name)
+ Format.fprintf fmt "%a@ %s"
+ Cil_printer.pp_lemma_kind il_pred.tp_kind il_name
| IPTypeInvariant {iti_name; iti_type} ->
Format.fprintf fmt "invariant@ %s for type %a" iti_name
Cil_printer.pp_typ iti_type
@@ -1135,11 +1133,10 @@ struct
Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [ext_name]
| IPCodeAnnot {ica_kf=kf; ica_ca=ca} ->
let name = match ca.annot_content with
- | AAssert (_, {tp_kind = Assert }) -> "assert"
- | AAssert (_, {tp_kind = Check }) -> "check"
- | AAssert (_, {tp_kind = Admit }) -> "admit"
- | AInvariant (_,true,_) -> "loop_inv"
- | AInvariant _ -> "inv"
+ | AAssert (_, {tp_kind}) -> Cil_printer.string_of_assert tp_kind
+ | AInvariant (_,loop,{tp_kind}) ->
+ let kw = if loop then "invariant" else "loop_invariant" in
+ Cil_printer.ident_of_predicate ~kw tp_kind
| APragma _ -> "pragma"
| AStmtSpec _ -> "contract"
| AAssigns _ -> "assigns"
@@ -1161,7 +1158,9 @@ struct
(kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
| IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
| IPLemma {il_name=name; il_pred} ->
- Format.asprintf "lemma_%s%a" name pp_names il_pred.tp_statement.pred_name
+ Format.asprintf "%s_%s%a"
+ (Cil_printer.ident_of_lemma il_pred.tp_kind)
+ name pp_names il_pred.tp_statement.pred_name
| IPTypeInvariant {iti_name; iti_pred} ->
Format.asprintf "type_invariant_%s%a"
iti_name pp_names iti_pred.pred_name
@@ -1169,10 +1168,10 @@ struct
Format.asprintf "global_invariant_%s%a"
igi_name pp_names igi_pred.pred_name
| IPAllocation {ial_kf=kf; ial_kinstr=ki; ial_bhv=Id_contract (a,b)} ->
- Format.asprintf "%s%s%a%salloc"
+ Format.asprintf "%s%s%a%sallocates"
(kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
| IPAllocation {ial_kf=kf; ial_kinstr=Kstmt _; ial_bhv=Id_loop ca} ->
- Format.asprintf "%sloop_alloc%a"
+ Format.asprintf "%sloop_allocates%a"
(kf_prefix kf) pp_code_annot_names ca
| IPAllocation _ -> assert false
| IPAssigns {ias_kf=kf; ias_kinstr=ki; ias_bhv=Id_contract (a,b)} ->
@@ -1271,10 +1270,7 @@ struct
add_part buffer p ; add_sep buffer ; add_parts buffer ps
let prefix_with_kind tp name =
- match tp.tp_kind with
- | Assert -> name
- | Check -> "check_" ^ name
- | Admit -> "admit_" ^ name
+ Cil_printer.ident_of_predicate ~kw:name tp.tp_kind
let rec parts_of_property ip : part list =
match ip with
@@ -1334,11 +1330,7 @@ struct
ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
[ K kf ; A ext_name ; S stmt ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_,p)}} ->
- let a = match p.tp_kind with
- | Assert -> "assert"
- | Check -> "check"
- | Admit -> "admit"
- in
+ let a = Cil_printer.string_of_assert p.tp_kind in
[K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, true, p)}} ->
let a = prefix_with_kind p "loop_invariant" in
@@ -1372,7 +1364,7 @@ struct
| IPAxiomatic _ -> []
| IPLemma {il_name=name; il_pred=p} ->
- let a = prefix_with_kind p "lemma" in
+ let a = Cil_printer.ident_of_lemma p.tp_kind in
[ A a ; A name ; P p.tp_statement ]
| IPTypeInvariant {iti_name=name}
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c7e35880edb..583f8298fc1 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -27,6 +27,53 @@ open Cil_datatype
open Printer_api
open Format
+let string_of_assert = function
+ | Assert -> "assert"
+ | Check -> "check"
+ | Admit -> "admit"
+
+let name_of_assert = function
+ | Assert -> "assertion"
+ | Check -> "check"
+ | Admit -> "admit"
+
+let string_of_lemma = function
+ | Assert -> "lemma"
+ | Check -> "check lemma"
+ | Admit -> "axiom"
+
+let ident_of_lemma = function
+ | Assert -> "lemma"
+ | Check -> "check_lemma"
+ | Admit -> "axiom"
+
+let string_of_predicate ~kw = function
+ | Assert -> kw
+ | Check -> "check " ^ kw
+ | Admit -> "admit " ^ kw
+
+let ident_of_predicate ~kw = function
+ | Assert -> kw
+ | Check -> "check_" ^ kw
+ | Admit -> "admit_" ^ kw
+
+let pp_assert_kind fmt kd = Format.pp_print_string fmt (string_of_assert kd)
+let pp_lemma_kind fmt kd = Format.pp_print_string fmt (string_of_lemma kd)
+let pp_predicate_kind ~kw fmt kd =
+ match kd with
+ | Assert -> Format.pp_print_string fmt kw
+ | Check ->
+ begin
+ Format.pp_print_string fmt "check " ;
+ Format.pp_print_string fmt kw ;
+ end
+ | Admit ->
+ begin
+ Format.pp_print_string fmt "admit " ;
+ Format.pp_print_string fmt kw ;
+ end
+
+
module Extensions = struct
let initialized = ref false
let ref_print = ref (fun _ _ _ _ -> assert false)
@@ -2847,11 +2894,20 @@ class cil_printer () = object (self)
method decreases fmt v = self#decrement "decreases" fmt v
method variant fmt v = self#decrement "loop variant" fmt v
- method private pp_predicate_kind fmt p =
- match p.tp_kind with
+ method private pp_predicate_kind fmt = function
| Assert -> ()
- | Check -> fprintf fmt "%a " self#pp_acsl_keyword "check"
- | Admit -> fprintf fmt "%a " self#pp_acsl_keyword "admit"
+ | Check -> self#pp_acsl_keyword fmt "check" ; pp_print_char fmt ' '
+ | Admit -> self#pp_acsl_keyword fmt "admit" ; pp_print_char fmt ' '
+
+ method private pp_lemma_kind fmt = function
+ | Assert -> self#pp_acsl_keyword fmt "lemma"
+ | Admit -> self#pp_acsl_keyword fmt "axiom"
+ | Check ->
+ begin
+ self#pp_acsl_keyword fmt "check" ;
+ pp_print_char fmt ' ' ;
+ self#pp_acsl_keyword fmt "lemma" ;
+ end
method assumes fmt p =
fprintf fmt "@[<hov 2>%a@ %a;@]"
@@ -2860,7 +2916,7 @@ class cil_printer () = object (self)
method requires fmt p =
fprintf fmt "@[<hov 2>%a%a@ %a;@]"
- self#pp_predicate_kind p.ip_content
+ self#pp_predicate_kind p.ip_content.tp_kind
self#pp_acsl_keyword "requires"
self#identified_predicate p
@@ -2873,7 +2929,7 @@ class cil_printer () = object (self)
method post_cond fmt (k,p) =
let kw = get_termination_kind_name k in
fprintf fmt "@[<hov 2>%a%a@ %a;@]"
- self#pp_predicate_kind p.ip_content
+ self#pp_predicate_kind p.ip_content.tp_kind
self#pp_acsl_keyword kw
self#identified_predicate p
@@ -3086,14 +3142,9 @@ class cil_printer () = object (self)
in
match ca.annot_content with
| AAssert (behav,p) ->
- let kw = match p.tp_kind with
- | Assert -> "assert"
- | Check -> "check"
- | Admit -> "admit"
- in
fprintf fmt "@[%a%a@ %a;@]"
pp_for_behavs behav
- self#pp_acsl_keyword kw
+ self#pp_acsl_keyword (string_of_assert p.tp_kind)
self#predicate p.tp_statement
| APragma (Slice_pragma sp) ->
fprintf fmt "@[%a@ %a;@]"
@@ -3122,13 +3173,13 @@ class cil_printer () = object (self)
| AInvariant(behav,true, i) ->
fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
- self#pp_predicate_kind i
+ self#pp_predicate_kind i.tp_kind
self#pp_acsl_keyword "loop invariant"
self#predicate i.tp_statement
| AInvariant(behav,false,i) ->
fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
- self#pp_predicate_kind i
+ self#pp_predicate_kind i.tp_kind
self#pp_acsl_keyword "invariant"
self#predicate i.tp_statement
| AVariant v ->
@@ -3221,11 +3272,7 @@ class cil_printer () = object (self)
(* attributes are meant to be purely internal for now. *)
let old_lab = current_label in
fprintf fmt "@[<hv 2>@[<hov 1>%a %a%a%a:@]@ %t%a;@]@\n"
- self#pp_acsl_keyword
- (match pred.tp_kind with
- | Admit -> "axiom"
- | Assert -> "lemma"
- | Check -> "check lemma")
+ self#pp_lemma_kind pred.tp_kind
self#varname name
self#labels labels
self#polyTypePrms tvars
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 40eeaa1b3e0..820154ac10b 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -30,6 +30,34 @@
include Printer_api.S
+(** ["assert"], ["check"] or ["admit"]. *)
+val string_of_assert : Cil_types.predicate_kind -> string
+
+(** ["assertion"], ["check"] or ["admit"]. *)
+val name_of_assert : Cil_types.predicate_kind -> string
+
+(** ["lemma"], ["check lemma"] or ["axiom"]. *)
+val string_of_lemma : Cil_types.predicate_kind -> string
+
+(** clause, prefixed by ["check"] or ["admit"]. *)
+val string_of_predicate : kw:string -> Cil_types.predicate_kind -> string
+
+(** same as [string_of_lemma] with ["_"] for separator. *)
+val ident_of_lemma : Cil_types.predicate_kind -> string
+
+(** same as [string_of_predicate] with ["_"] for separator. *)
+val ident_of_predicate : kw:string -> Cil_types.predicate_kind -> string
+
+(** pretty prints [string_of_assert]. *)
+val pp_assert_kind : Format.formatter -> Cil_types.predicate_kind -> unit
+
+(** pretty prints [string_of_lemma]. *)
+val pp_lemma_kind : Format.formatter -> Cil_types.predicate_kind -> unit
+
+(** pretty prints [string_of_predicate]. *)
+val pp_predicate_kind :
+ kw:string -> Format.formatter -> Cil_types.predicate_kind -> unit
+
val get_termination_kind_name: Cil_types.termination_kind -> string
val register_shallow_attribute: string -> unit
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 000cedcd25f..a545e1b1f63 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -120,13 +120,8 @@ let pp_top fmt tp = pp_named fmt tp.tp_statement
let pp_code_annot fmt ca =
match ca.annot_content with
| AAssert(bs,tp) ->
- let kind =
- match tp.tp_kind with
- | Assert -> "assertion"
- | Check -> "check"
- | Admit -> "admit"
- in
- Format.fprintf fmt "%s%a%a" kind pp_for bs pp_top tp
+ Format.fprintf fmt "%a%a%a"
+ Cil_printer.pp_assert_kind tp.tp_kind pp_for bs pp_top tp
| AInvariant(bs,_,tp) ->
Format.fprintf fmt "invariant%a%a" pp_for bs pp_top tp
| AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 7f41c46efb2..b11531eaefb 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -365,11 +365,8 @@ let rec print_decl fmt d =
(pp_list ~sep:",@ " print_typed_ident) prms
(pp_list ~sep:"@\n" print_case) cases
| LDlemma(name,labels,tvar,body) ->
- fprintf fmt "@[<2>%s@ %s%a%a:@ %a;@]"
- (match body.tp_kind with
- | Admit -> "axiom"
- | Assert -> "lemma"
- | Check -> "check lemma") name
+ fprintf fmt "@[<2>%a@ %s%a%a:@ %a;@]"
+ Cil_printer.pp_lemma_kind body.tp_kind name
(pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
(pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
print_lexpr body.tp_statement
@@ -421,12 +418,7 @@ let print_allocation ~isloop fmt fa =
let print_clause name fmt e = fprintf fmt "@\n%s@ %a;" name print_lexpr e
let print_tp_clause name fmt e =
- let name =
- match e.tp_kind with
- | Assert -> name
- | Check -> "check " ^ name
- | Admit -> "admit " ^ name
- in
+ let name = Cil_printer.string_of_predicate ~kw:name e.tp_kind in
print_clause name fmt e.tp_statement
let print_post fmt (k,e) =
@@ -492,23 +484,19 @@ let print_code_annot fmt ca =
in
match ca with
AAssert(bhvs,e) ->
- fprintf fmt "%a%s@ %a;"
+ fprintf fmt "%a%a@ %a;"
print_behaviors bhvs
- (match e.tp_kind with
- | Assert -> ""
- | Check -> "check "
- | Admit -> "admit")
+ Cil_printer.pp_assert_kind e.tp_kind
print_lexpr e.tp_statement
| AStmtSpec (bhvs,s) ->
fprintf fmt "%a%a"
print_behaviors bhvs
print_spec s
| AInvariant (bhvs,loop,e) ->
- fprintf fmt "%a%a%a%ainvariant@ %a;"
+ let kw = if loop then "loop invariant" else "invariant" in
+ fprintf fmt "%a%a@ %a;"
print_behaviors bhvs
- (pp_cond (e.tp_kind = Check)) "check @"
- (pp_cond (e.tp_kind = Admit)) "admit @"
- (pp_cond loop) "loop@ "
+ (Cil_printer.pp_predicate_kind ~kw) e.tp_kind
print_lexpr e.tp_statement
| AVariant e -> fprintf fmt "loop@ variant@ %a;" print_variant e
| AAssigns (bhvs,a) ->
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index dffb3997bbd..5d267bd8926 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -503,11 +503,8 @@ let to_do_on_select
main_ui#pretty_information "This is an axiomatic.@.";
main_ui#view_original (location ip)
| PIP(IPLemma { il_pred } as ip) ->
- let kind = match il_pred.tp_kind with
- | Admit -> "axiom"
- | Assert -> "lemma"
- | Check -> "check lemma" in
- main_ui#pretty_information "This is a %s.@." kind;
+ main_ui#pretty_information "This is a %a.@."
+ Cil_printer.pp_lemma_kind il_pred.tp_kind;
main_ui#view_original (location ip)
| PIP(IPTypeInvariant _ as ip) ->
main_ui#pretty_information "This is a type invariant.@.";
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index ee3739a068f..27c3e8b23d1 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -170,10 +170,7 @@ class visitor = object
warn "axiomatic" str;
Cil.DoChildren
| Dlemma(str, _, _, { tp_kind }, _, _) ->
- warn (match tp_kind with
- | Admit -> "axiom"
- | Assert -> "lemma"
- | Check -> "check lemma") str;
+ warn (Cil_printer.string_of_lemma tp_kind) str;
Cil.DoChildren
| _ ->
Cil.DoChildren
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 2293ed64aef..d5a663cdc06 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -588,9 +588,7 @@ module Make
let code_annotation_text ca =
match ca.annot_content with
- | AAssert (_,{tp_kind = Assert}) -> "assertion"
- | AAssert (_,{tp_kind = Check}) -> "check"
- | AAssert (_,{tp_kind = Admit}) -> "admit"
+ | AAssert (_,{tp_kind}) -> Cil_printer.name_of_assert tp_kind
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index f9c730b433d..4547fb1f139 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -29,9 +29,7 @@ let has_requires spec =
let code_annotation_text ca =
match ca.annot_content with
- | AAssert (_, {tp_kind=Assert}) -> "assertion"
- | AAssert (_, {tp_kind=Check}) -> "check"
- | AAssert (_, {tp_kind=Admit}) -> "admit"
+ | AAssert (_, {tp_kind}) -> Cil_printer.name_of_assert tp_kind
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 28bb84f9b84..e37f7b0903f 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -543,13 +543,9 @@ let pp_decl fmt d l =
pp_sig fmt kind l ;
end
-let pp_kind fmt = function
- | Admit -> Format.pp_print_string fmt "axiom"
- | Assert -> Format.pp_print_string fmt "lemma"
- | Check -> Format.pp_print_string fmt "check lemma"
-
let pp_lemma fmt l =
- Format.fprintf fmt " * %a '%s'@\n" pp_kind l.lem_predicate.tp_kind l.lem_name
+ Format.fprintf fmt " * %a '%s'@\n"
+ Cil_printer.pp_lemma_kind l.lem_predicate.tp_kind l.lem_name
let get_name l = compute () ; compute_logicname l
@@ -584,7 +580,7 @@ let dump () =
SMap.iter
(fun l (lem,s) ->
Format.fprintf fmt " * %a '%s' in %a@\n"
- pp_kind lem.lem_predicate.tp_kind
+ Cil_printer.pp_lemma_kind lem.lem_predicate.tp_kind
l pp_section s)
d.lemmas ;
Format.fprintf fmt "-------------------------------------------------@." ;
--
GitLab