From 3be325cbad15488e91d218cd27cb2ac0cc021ac3 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 21 Feb 2019 15:30:22 +0100
Subject: [PATCH] [Kernel] add more debug pretty-printers
---
.../ast_printing/cil_types_debug.ml | 268 ++++++++++--------
.../ast_printing/cil_types_debug.mli | 10 +-
2 files changed, 159 insertions(+), 119 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index c1c21886248..55d7253b1f9 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -40,6 +40,8 @@ let print_full_fieldinfo = false
let print_full_enuminfo = false
let print_full_typeinfo = false
let print_full_varinfo = false
+let print_full_fundec = false
+let print_full_spec = false
let pp_list fmt = Pretty_utils.pp_list fmt ~sep:", " ~pre:"[" ~last:"]" ~suf:"" ~empty:"[]"
let pp_option fmt = Pretty_utils.pp_opt ~none:"None" ~pre:"Some(" ~suf:")" fmt
@@ -412,10 +414,9 @@ and pp_exp_node fmt = function
| StartOf(lval) -> Format.fprintf fmt "StartOf(%a)" pp_lval lval
| Info(exp,exp_info) -> Format.fprintf fmt "Info(%a,%a)" pp_exp exp pp_exp_info exp_info
-and pp_exp_info fmt _exp_info = Format.fprintf fmt "pp_exp_info_TODO" (*{
- exp_type : logic_type;
- exp_name: string_list;
- }*)
+and pp_exp_info fmt exp_info = Format.fprintf fmt "{exp_type=%a;exp_name=%a}"
+ pp_logic_type exp_info.exp_type
+ (pp_list pp_string) exp_info.exp_name
and pp_constant fmt = function
| CInt64(integer,ikind,string_option) ->
@@ -473,27 +474,42 @@ and pp_init fmt = function
Format.fprintf fmt "CompoundInit(%a,%a)" pp_typ typ
(pp_list (pp_pair pp_offset pp_init)) offset_init_pair_list
-and pp_initinfo fmt _initinfo = Format.fprintf fmt "pp_initinfo_TODO" (*{ mutable init : init_option }*)
-
-and pp_fundec fmt _fundec = Format.fprintf fmt "pp_fundec_TODO" (*{
- mutable svar: varinfo;
- mutable sformals: varinfo_list;
- mutable slocals: varinfo_list;
- mutable smaxid: int;
- mutable sbody: block;
- mutable smaxstmtid: int_option;
- mutable sallstmts: stmt_list;
- mutable sspec: funspec;
- }*)
-
-and pp_block fmt _block = Format.fprintf fmt "pp_block_TODO" (*{
- mutable battrs: attributes;
- mutable blocals: varinfo_list;
- mutable bstmts: stmt_list;
- }*)
+and pp_initinfo fmt initinfo = Format.fprintf fmt "{%a}" (pp_option pp_init) initinfo.init
+
+and pp_fundec fmt fundec =
+ if print_full_fundec then
+ Format.fprintf fmt
+ "{svar=%a;sformals=%a;slocals=%a;smaxid=%a;sbody=%a;smaxstmtid=%a;sallstmts=%a;sspec=%a}"
+ pp_varinfo fundec.svar
+ (pp_list pp_varinfo) fundec.sformals
+ (pp_list pp_varinfo) fundec.slocals
+ pp_int fundec.smaxid
+ pp_block fundec.sbody
+ (pp_option pp_int) fundec.smaxstmtid
+ (pp_list pp_stmt) fundec.sallstmts
+ pp_funspec fundec.sspec
+ else
+ Format.fprintf fmt
+ "{svar=%a;sformals=%a;slocals=%a;smaxid=%a;sbody=<...>;smaxstmtid=%a;sallstmts=<...>;sspec=%a}"
+ pp_varinfo fundec.svar
+ (pp_list pp_varinfo) fundec.sformals
+ (pp_list pp_varinfo) fundec.slocals
+ pp_int fundec.smaxid
+ (*pp_block fundec.sbody*)
+ (pp_option pp_int) fundec.smaxstmtid
+ (*(pp_list pp_stmt) fundec.sallstmts*)
+ pp_funspec fundec.sspec
+
+and pp_block fmt block =
+ Format.fprintf fmt "{battrs=%a;bscoping=%a;blocals=%a;bstatics=%a;bstmts=%a}"
+ pp_attributes block.battrs
+ pp_bool block.bscoping
+ (pp_list pp_varinfo) block.blocals
+ (pp_list pp_varinfo) block.bstatics
+ (pp_list pp_stmt) block.bstmts
and pp_stmt fmt stmt = Format.fprintf fmt
- "{sid=%a;labels=%a;skind=%a;ghost=%a;TODO}"
+ "{sid=%a;labels=%a;skind=%a;ghost=%a;succs=<...>;preds=<...>}"
pp_int stmt.sid
(pp_list pp_label) stmt.labels
pp_stmtkind stmt.skind
@@ -569,13 +585,12 @@ and pp_instr fmt = function
| Local_init(vi,i,location) ->
Format.fprintf fmt "Local_init(%a,%a,%a)" pp_varinfo vi pp_local_init i pp_location location
-and pp_extended_asm fmt _extended_asm = Format.fprintf fmt "pp_extended_asm_TODO" (*{
- {
- asm_outputs: (string_option * string * lval)_list;
- asm_inputs: (string_option * string * exp)_list;
- asm_clobbers: string_list;
- asm_gotos: (stmt ref)_list;
- }*)
+and pp_extended_asm fmt extended_asm =
+ Format.fprintf fmt "{asm_outputs=%a;asm_inputs=%a;asm_clobbers=%a;asm_gotos=%a}"
+ (pp_list (pp_tuple3 (pp_option pp_string) pp_string pp_lval)) extended_asm.asm_outputs
+ (pp_list (pp_tuple3 (pp_option pp_string) pp_string pp_exp)) extended_asm.asm_inputs
+ (pp_list pp_string) extended_asm.asm_clobbers
+ (pp_list (pp_ref pp_stmt)) extended_asm.asm_gotos
and pp_filepath_position fmt filepath_position =
Format.fprintf fmt "{pos_path=%s;pos_lnum=%d;pos_bol=%d;pos_cnum=%d}"
@@ -605,12 +620,12 @@ and pp_logic_constant fmt = function
| LReal(logic_real) -> Format.fprintf fmt "LReal(%a)" pp_logic_real logic_real
| LEnum(enumitem) -> Format.fprintf fmt "LEnum(%a)" pp_enumitem enumitem
-and pp_logic_real fmt _logic_real = Format.fprintf fmt "pp_logic_real_TODO" (*{
- r_literal : string ;
- r_nearest : float ;
- r_upper : float ;
- r_lower : float ;
- }*)
+and pp_logic_real fmt logic_real =
+ Format.fprintf fmt "{r_literal=%a;r_nearest=%a;r_upper=%a;r_lower=%a}"
+ pp_string logic_real.r_literal
+ pp_float logic_real.r_nearest
+ pp_float logic_real.r_upper
+ pp_float logic_real.r_lower
and pp_logic_type fmt = function
| Ctype(typ) -> Format.fprintf fmt "Ctype(%a)" pp_typ typ
@@ -709,14 +724,13 @@ and pp_term_lhost fmt = function
| TResult(typ) -> Format.fprintf fmt "TResult(%a)" pp_typ typ
| TMem(term) -> Format.fprintf fmt "TMem(%a)" pp_term term
-and pp_model_info fmt _model_info = Format.fprintf fmt "pp_model_info_TODO" (*{
- mi_name: string;
- mi_field_type: logic_type;
- mi_base_type: typ;
- mi_decl: location;
- mutable mi_attr: attributes;
-
- }*)
+and pp_model_info fmt model_info = Format.fprintf fmt
+ "{mi_name=%a;mi_field_type=%a;mi_base_type=%a;mi_decl=%a;mi_attr=%a}"
+ pp_string model_info.mi_name
+ pp_logic_type model_info.mi_field_type
+ pp_typ model_info.mi_base_type
+ pp_location model_info.mi_decl
+ pp_attributes model_info.mi_attr
and pp_term_offset fmt = function
| TNoOffset -> Format.fprintf fmt "TNoOffset"
@@ -728,11 +742,12 @@ and pp_term_offset fmt = function
Format.fprintf fmt "TIndex(%a,%a)" pp_term term pp_term_offset term_offset
and pp_logic_info fmt logic_info =
- Format.fprintf fmt "{l_var_info=%a;%al_tparams=%a;logic_type=%a;TODO}"
+ Format.fprintf fmt "{l_var_info=%a;%al_tparams=%a;logic_type=%a;l_profile=%a;l_body=<...>}"
pp_logic_var logic_info.l_var_info
(pp_if_list_not_empty "l_labels=" ";" (pp_list pp_logic_label)) logic_info.l_labels
(pp_list pp_string) logic_info.l_tparams
(pp_option pp_logic_type) logic_info.l_type
+ (pp_list pp_logic_var) logic_info.l_profile
(*{
mutable l_var_info : logic_var;
mutable l_labels : logic_label_list;
@@ -742,13 +757,14 @@ and pp_logic_info fmt logic_info =
mutable l_body : logic_body;
}*)
-and pp_builtin_logic_info fmt _builtin_logic_info = Format.fprintf fmt "pp_builtin_logic_info_TODO" (*{
- mutable bl_name: string;
- mutable bl_labels: logic_label_list;
- mutable bl_params: string_list;
- mutable bl_type: logic_type_option;
- mutable bl_profile: (string * logic_type)_list;
- }*)
+and pp_builtin_logic_info fmt builtin_logic_info =
+ Format.fprintf fmt
+ "{bl_name=%a;bl_labels=%a;bl_params=%a;bl_type=%a;bl_profile=%a}"
+ pp_string builtin_logic_info.bl_name
+ (pp_list pp_logic_label) builtin_logic_info.bl_labels
+ (pp_list pp_string) builtin_logic_info.bl_params
+ (pp_option pp_logic_type) builtin_logic_info.bl_type
+ (pp_list (pp_pair pp_string pp_logic_type)) builtin_logic_info.bl_profile
and pp_logic_body fmt = function
| LBnone -> Format.fprintf fmt "LBnone"
@@ -780,8 +796,12 @@ and pp_logic_var_kind fmt = function
| LVLocal -> Format.fprintf fmt "LVLocal"
and pp_logic_var fmt logic_var =
- Format.fprintf fmt "{lv_name=%a;lv_id=%a;TODO}"
+ Format.fprintf fmt "{lv_name=%a;lv_id=%a;lv_type=%a;lv_kind=%a;lv_origin=%a;lv_attr=%a}"
pp_string logic_var.lv_name pp_int logic_var.lv_id
+ pp_logic_type logic_var.lv_type
+ pp_logic_var_kind logic_var.lv_kind
+ (pp_option pp_varinfo) logic_var.lv_origin
+ pp_attributes logic_var.lv_attr
(*{
mutable lv_name : string;
mutable lv_id : int;
@@ -792,7 +812,7 @@ and pp_logic_var fmt logic_var =
}*)
and pp_logic_ctor_info fmt logic_ctor_info =
- Format.fprintf fmt "{ctor_name=%a;ctor_type=TODO;ctor_params=%a}"
+ Format.fprintf fmt "{ctor_name=%a;ctor_type=<...>;ctor_params=%a}"
pp_string logic_ctor_info.ctor_name
(*note: printing ctor_type type may lead to infinite recursion*)
(*pp_logic_type_info logic_ctor_info.ctor_type*)
@@ -871,13 +891,22 @@ and pp_predicate fmt predicate = Format.fprintf fmt "{%a%apred_content=%a}"
(pp_if_loc_known "pred_loc=" ";") predicate.pred_loc
pp_predicate_node predicate.pred_content
-and pp_spec fmt _spec = Format.fprintf fmt "pp_spec_TODO" (*{
- mutable spec_behavior : behavior_list;
- mutable spec_variant : term variant_option;
- mutable spec_terminates: identified_predicate_option;
- mutable spec_complete_behaviors: string_list_list;
- mutable spec_disjoint_behaviors: string_list_list;
- }*)
+and pp_spec fmt spec =
+ if print_full_spec then
+ Format.fprintf fmt
+ "{spec_behavior=%a;spec_variant=%a;spec_terminates=%a;\
+ spec_complete_behaviors=%a;spec_disjoint_behaviors=%a}"
+ (pp_list pp_behavior) spec.spec_behavior
+ (pp_option pp_variant) spec.spec_variant
+ (pp_option pp_identified_predicate) spec.spec_terminates
+ (pp_list (pp_list pp_string)) spec.spec_complete_behaviors
+ (pp_list (pp_list pp_string)) spec.spec_disjoint_behaviors
+ else
+ Format.fprintf fmt "{spec_behavior=%a;spec_complete_behaviors=%a;\
+ spec_disjoint_behaviors=%a}"
+ (pp_list pp_string) (List.map (fun b -> b.b_name) spec.spec_behavior)
+ (pp_list (pp_list pp_string)) spec.spec_complete_behaviors
+ (pp_list (pp_list pp_string)) spec.spec_disjoint_behaviors
and pp_acsl_extension fmt = pp_tuple5 pp_int pp_string pp_location pp_bool pp_acsl_extension_kind fmt
@@ -886,15 +915,17 @@ and pp_acsl_extension_kind fmt = function
| Ext_terms(term_list) -> Format.fprintf fmt "Ext_terms(%a)" (pp_list pp_term) term_list
| Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)" (pp_list pp_predicate) predicate_list
-and pp_behavior fmt _behavior = Format.fprintf fmt "pp_behavior_TODO" (*{
- mutable b_name : string;
- mutable b_requires : identified_predicate_list;
- mutable b_assumes : identified_predicate_list;
- mutable b_post_cond : (termination_kind * identified_predicate)_list;
- mutable b_assigns : assigns;
- mutable b_allocation : allocation;
- mutable b_extended : acsl_extension_list
- }*)
+and pp_behavior fmt behavior =
+ Format.fprintf fmt
+ "{b_name=%a;b_requires=%a;b_assumes=%a;b_post_cond=%a;b_assigns=%a;\
+ b_allocation=%a;b_extended=%a}"
+ pp_string behavior.b_name
+ (pp_list pp_identified_predicate) behavior.b_requires
+ (pp_list pp_identified_predicate) behavior.b_assumes
+ (pp_list (pp_pair pp_termination_kind pp_identified_predicate)) behavior.b_post_cond
+ (pp_assigns pp_from) behavior.b_assigns
+ pp_allocation behavior.b_allocation
+ (pp_list pp_acsl_extension) behavior.b_extended
and pp_termination_kind fmt = function
| Normal -> Format.fprintf fmt "Normal"
@@ -947,12 +978,12 @@ and pp_code_annotation_node fmt = function
Format.fprintf fmt "AExtended(%a,%B,%a)"
(pp_list pp_string) string_list is_loop pp_acsl_extension acsl_extension
-and pp_funspec fmt _funspec = Format.fprintf fmt "pp_funspec_TODO"
+and pp_funspec fmt funspec = pp_spec fmt funspec
-and pp_code_annotation fmt _code_annotation = Format.fprintf fmt "pp_code_annotation_TODO" (*{
- annot_id: int;
- annot_content : code_annotation_node;
- }*)
+and pp_code_annotation fmt code_annotation =
+ Format.fprintf fmt "{annot_id=%a;annot_content=%a}"
+ pp_int code_annotation.annot_id
+ pp_code_annotation_node code_annotation.annot_content
and pp_funbehavior fmt = pp_behavior fmt
@@ -1001,48 +1032,57 @@ let pp_cil_function fmt = function
Format.fprintf fmt "Declaration(%a,%a,%a,%a)" pp_funspec funspec pp_varinfo varinfo
(pp_option (pp_list pp_varinfo)) varinfo_list_option pp_location location
-let pp_kernel_function fmt _kernel_function = Format.fprintf fmt "pp_kernel_function_TODO" (*{
- mutable fundec : cil_function;
- mutable spec : funspec;
- }*)
+let pp_kernel_function fmt kernel_function =
+ Format.fprintf fmt "{fundec=%a;spec=%a}"
+ pp_cil_function kernel_function.fundec
+ pp_funspec kernel_function.spec
let pp_localisation fmt = function
| VGlobal -> Format.fprintf fmt "VGlobal"
| VLocal(kernel_function) -> Format.fprintf fmt "VLocal(%a)" pp_kernel_function kernel_function
| VFormal(kernel_function) -> Format.fprintf fmt "VFormal(%a)" pp_kernel_function kernel_function
-let pp_mach fmt _mach = Format.fprintf fmt "pp_mach_TODO" (*{
- sizeof_short: int;
- sizeof_int: int;
- sizeof_long: int ;
- sizeof_longlong: int;
- sizeof_ptr: int;
- sizeof_float: int;
- sizeof_double: int;
- sizeof_longdouble: int;
- sizeof_void: int;
- sizeof_fun: int;
- size_t: string;
- wchar_t: string;
- ptrdiff_t: string;
- alignof_short: int;
- alignof_int: int;
- alignof_long: int;
- alignof_longlong: int;
- alignof_ptr: int;
- alignof_float: int;
- alignof_double: int;
- alignof_longdouble: int;
- alignof_str: int;
- alignof_fun: int;
- char_is_unsigned: bool;
- underscore_name: bool;
- const_string_literals: bool;
- little_endian: bool;
- alignof_aligned: int;
- has__builtin_va_list: bool;
- __thread_is_keyword: bool;
- compiler: string;
- cpp_arch_flags: string_list;
- version: string;
- }*)
+let pp_mach fmt mach =
+ Format.fprintf fmt
+ "{sizeof_short=%a;sizeof_int=%a;sizeof_long=%a;sizeof_longlong=%a;\
+ sizeof_ptr=%a;sizeof_float=%a;sizeof_double=%a;sizeof_longdouble=%a;\
+ sizeof_void=%a;sizeof_fun=%a;size_t=%a;wchar_t=%a;ptrdiff_t=%a;\
+ alignof_short=%a;alignof_int=%a;alignof_long=%a;alignof_longlong=%a;\
+ alignof_ptr=%a;alignof_float=%a;alignof_double=%a;alignof_longdouble=%a;\
+ alignof_str=%a;alignof_fun=%a;char_is_unsigned=%a;underscore_name=%a;\
+ const_string_literals=%a;little_endian=%a;alignof_aligned=%a;\
+ has__builtin_va_list=%a;__thread_is_keyword=%a;compiler=%a;\
+ cpp_arch_flags=%a;version=%a}"
+ pp_int mach.sizeof_short
+ pp_int mach.sizeof_int
+ pp_int mach.sizeof_long
+ pp_int mach.sizeof_longlong
+ pp_int mach.sizeof_ptr
+ pp_int mach.sizeof_float
+ pp_int mach.sizeof_double
+ pp_int mach.sizeof_longdouble
+ pp_int mach.sizeof_void
+ pp_int mach.sizeof_fun
+ pp_string mach.size_t
+ pp_string mach.wchar_t
+ pp_string mach.ptrdiff_t
+ pp_int mach.alignof_short
+ pp_int mach.alignof_int
+ pp_int mach.alignof_long
+ pp_int mach.alignof_longlong
+ pp_int mach.alignof_ptr
+ pp_int mach.alignof_float
+ pp_int mach.alignof_double
+ pp_int mach.alignof_longdouble
+ pp_int mach.alignof_str
+ pp_int mach.alignof_fun
+ pp_bool mach.char_is_unsigned
+ pp_bool mach.underscore_name
+ pp_bool mach.const_string_literals
+ pp_bool mach.little_endian
+ pp_int mach.alignof_aligned
+ pp_bool mach.has__builtin_va_list
+ pp_bool mach.__thread_is_keyword
+ pp_string mach.compiler
+ (pp_list pp_string) mach.cpp_arch_flags
+ pp_string mach.version
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index e6cca0530b1..29eb14f20cc 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -141,8 +141,8 @@ val pp_predicate : Cil_types.predicate Pretty_utils.formatter
val pp_spec : Format.formatter -> Cil_types.spec -> unit
val pp_acsl_extension : Format.formatter -> Cil_types.acsl_extension -> unit
val pp_acsl_extension_kind :
- Cil_types.acsl_extension_kind Pretty_utils.formatter
-val pp_behavior : Format.formatter -> 'a -> unit
+ Format.formatter -> Cil_types.acsl_extension_kind -> unit
+val pp_behavior : Format.formatter -> Cil_types.behavior -> unit
val pp_termination_kind :
Format.formatter -> Cil_types.termination_kind -> unit
val pp_loop_pragma :
@@ -161,11 +161,11 @@ val pp_code_annotation_node :
Format.formatter -> Cil_types.code_annotation_node -> unit
val pp_funspec : Format.formatter -> Cil_types.funspec -> unit
val pp_code_annotation : Cil_types.code_annotation Pretty_utils.formatter
-val pp_funbehavior : Format.formatter -> 'a -> unit
+val pp_funbehavior : Format.formatter -> Cil_types.funbehavior -> unit
val pp_global_annotation : Cil_types.global_annotation Pretty_utils.formatter
val pp_custom_tree : Format.formatter -> Cil_types.custom_tree -> unit
val pp_kinstr : Format.formatter -> Cil_types.kinstr -> unit
val pp_cil_function : Format.formatter -> Cil_types.cil_function -> unit
-val pp_kernel_function : Format.formatter -> 'a -> unit
+val pp_kernel_function : Format.formatter -> Cil_types.kernel_function -> unit
val pp_localisation : Format.formatter -> Cil_types.localisation -> unit
-val pp_mach : Format.formatter -> 'a -> unit
+val pp_mach : Format.formatter -> Cil_types.mach -> unit
--
GitLab