From 268dec55a9b0d0ba1f5917d339ff35cec4a2ff5c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 11 Feb 2022 18:26:44 +0100
Subject: [PATCH] [options] refactor unmangling options and allow unmangling
even on C files
---
frama_Clang_option.ml | 104 ++++++++++++++++++------------
frama_Clang_option.mli | 20 +++---
frama_Clang_register.ml | 14 ++--
mangling.ml | 7 +-
tests/basic/oracle/printer.res.c | 50 ++++++++++++++
tests/basic/oracle/printer.res2.c | 50 ++++++++++++++
tests/basic/printer.cpp | 4 +-
7 files changed, 190 insertions(+), 59 deletions(-)
create mode 100644 tests/basic/oracle/printer.res.c
create mode 100644 tests/basic/oracle/printer.res2.c
diff --git a/frama_Clang_option.ml b/frama_Clang_option.ml
index ee81e6e5..2e806ff3 100644
--- a/frama_Clang_option.ml
+++ b/frama_Clang_option.ml
@@ -42,48 +42,69 @@ module Clang_command =
let () = Parameter_customize.no_category ()
module Clang_extra_args =
String_list(
- struct
- let option_name = "-fclang-cpp-extra-args"
- let help =
- "pass additional options to clang. If not set, the content of \
- -cpp-extra-args (if any) is used instead"
- let arg_name = "opt"
- end)
-
-module Unmangling:
-sig
- val add_hook_on_update: (unit -> unit) -> unit
- val set: string -> unit
- val get: unit -> string
- val clear: unit -> unit
- val get_val: unit -> (string -> string)
- val register_mangling_func: string -> (string->string) -> unit
-end
-=
struct
- module Rep =
- State_builder.Ref(Datatype.String)
- (struct let dependencies = []
- let name = "Unmangling"
- let default () = "short"
- end)
- let add_hook_on_update f = Rep.add_hook_on_update (fun _ -> f ())
- let available_opt = Hashtbl.create 7
- let set s = if Hashtbl.mem available_opt s then Rep.set s
- let clear () = Rep.clear ()
- let get () = Rep.get ()
- let get_val () = Hashtbl.find available_opt (Rep.get ())
- let register_mangling_func s f = Hashtbl.add available_opt s f
- let () =
- register_mangling_func "id" (fun s -> s);
- set "short"
+ let option_name = "-fclang-cpp-extra-args"
+ let help =
+ "pass additional options to clang. If not set, the content of \
+ -cpp-extra-args (if any) is used instead"
+ let arg_name = "opt"
+ end)
+
+let unmangling_functions: (string*(string->string)) Datatype.String.Hashtbl.t =
+ Datatype.String.Hashtbl.create 7
+
+let pp_unmangling_functions fmt =
+ Datatype.String.Hashtbl.iter
+ (fun key (help, _) -> Format.fprintf fmt "%s: %s@\n" key help)
+ unmangling_functions
+
+let () =
+ Datatype.String.Hashtbl.add
+ unmangling_functions "none" ("keep mangled names", fun id -> id)
+
+module Unmangling =
+ String(
+ struct
+ let option_name = "-cxx-unmangling"
+ let help =
+ "how to pretty-print mangled symbols. Use -unmangling help to list \
+ available options"
+ let arg_name = "s"
+ let default = "none"
end
+)
+
+let unmangling_help () =
+ feedback "Possible unmangling functions are:@\n%t" pp_unmangling_functions;
+ Cmdline.nop
+
+let unmangling_hook _ v =
+ if Datatype.String.equal v "help" then
+ Cmdline.run_after_exiting_stage unmangling_help
+
+let () = Unmangling.add_set_hook unmangling_hook
+
+let () = Unmangling.set_possible_values [ "none"; "help" ]
+let add_unmangling_function key descr f =
+ let l = Unmangling.get_possible_values () in
+ Unmangling.set_possible_values (key :: l);
+ Datatype.String.Hashtbl.add unmangling_functions key (descr,f)
+
+let get_unmangling_function () =
+ let v = Unmangling.get () in
+ if v <> "help" then
+ snd (Datatype.String.Hashtbl.find unmangling_functions v)
+ else
+ fatal
+ "cannot get current unmangling function: \
+ Frama-C is not supposed to run analyses if `-unmangling help' is set "
module UnmanglingFull =
Bool(struct
let default = false
let option_name = "-cxx-demangling-full"
- let help= "displays identifiers with their full C++ name"
+ let help= "displays identifiers with their full C++ name. \
+ OBSOLETE: use -unmangling fully-qualified instead)"
end)
let () = Parameter_customize.set_negative_option_name ""
@@ -94,7 +115,8 @@ module UnmanglingShort =
let option_name = "-cxx-demangling-short"
let help=
"displays identifiers with their C++ short name \
- (without qualifiers)"
+ (without qualifiers). \
+ OBSOLETE: use -unmangling without-qualifier instead"
end)
let () = Parameter_customize.set_negative_option_name ""
@@ -103,17 +125,17 @@ module UnmanglingNo =
Bool(struct
let default = false
let option_name= "-cxx-keep-mangling"
- let help= "displays identifiers with their mangled name"
+ let help= "displays identifiers with their mangled name \
+ OBSOLETE: use -unmangling none instead"
end)
let add_unmangling_option s _ new_flag =
if new_flag then Unmangling.set s
- else if Unmangling.get () = s then Unmangling.clear ()
let () =
- UnmanglingFull.add_set_hook (add_unmangling_option "full");
- UnmanglingShort.add_set_hook (add_unmangling_option "short");
- UnmanglingNo.add_set_hook (add_unmangling_option "id");
+ UnmanglingFull.add_set_hook (add_unmangling_option "fully-qualified");
+ UnmanglingShort.add_set_hook (add_unmangling_option "without-qualifier");
+ UnmanglingNo.add_set_hook (add_unmangling_option "none")
module ParseableOutput =
False(struct
diff --git a/frama_Clang_option.mli b/frama_Clang_option.mli
index 1310d797..16f00806 100644
--- a/frama_Clang_option.mli
+++ b/frama_Clang_option.mli
@@ -27,14 +27,18 @@ module Clang_command: Parameter_sig.String
module Clang_extra_args: Parameter_sig.String_list
-(** state of the demangling options. *)
-module Unmangling:
-sig
- val add_hook_on_update: (unit -> unit) -> unit
- val set: string -> unit
- val get_val: unit -> (string -> string)
- val register_mangling_func: string -> (string->string) -> unit
-end
+(** state of the -unmangling option. *)
+module Unmangling: Parameter_sig.String
+
+(** [add_unmangling_function key descr f] registers [f] as an unmangling
+ function, activated by [-unmangling key]. [descr] will be displayed
+ along with [key] in the [-unmangling help] output.
+ *)
+val add_unmangling_function: string -> string -> (string -> string) -> unit
+
+(** gets the unmangling function corresponding
+ to the current value of [Unmangling] *)
+val get_unmangling_function: unit -> (string -> string)
(** -cxx-parseable-output *)
module ParseableOutput: Parameter_sig.Bool
diff --git a/frama_Clang_register.ml b/frama_Clang_register.ml
index 1c753b84..5c7dcfcb 100644
--- a/frama_Clang_register.ml
+++ b/frama_Clang_register.ml
@@ -120,7 +120,8 @@ struct
class printer = object
inherit M.printer
method! varname fmt name =
- Format.pp_print_string fmt (Frama_Clang_option.Unmangling.get_val() name)
+ Format.pp_print_string fmt
+ (Frama_Clang_option.get_unmangling_function () name)
end
end
@@ -129,8 +130,9 @@ end
let is_cxx_printer_initialized = ref false
-let init_cxx_printer () =
- if not !is_cxx_printer_initialized then begin
+let init_cxx_printer _ v =
+ if v <> "help" && not !is_cxx_printer_initialized then
+ begin
is_cxx_printer_initialized := true;
Cil_printer.register_shallow_attribute Convert.fc_implicit_attr;
Cil_printer.register_shallow_attribute Convert.fc_pure_template_decl_attr;
@@ -138,14 +140,16 @@ let init_cxx_printer () =
end
let () =
- Frama_Clang_option.Unmangling.add_hook_on_update init_cxx_printer
+ Frama_Clang_option.Unmangling.add_set_hook init_cxx_printer
let is_initialized = ref false
let init_cxx_normalization () =
if not !is_initialized then begin
is_initialized:=true;
- init_cxx_printer ();
+ (* If unmangling has not been set, default to short. *)
+ if not (Frama_Clang_option.Unmangling.is_set ()) then
+ Frama_Clang_option.Unmangling.set "without-qualifier";
(* enable exception removal unless it has explicitely been set to false
on the command line.
*)
diff --git a/mangling.ml b/mangling.ml
index cee5981b..51b84c99 100644
--- a/mangling.ml
+++ b/mangling.ml
@@ -801,6 +801,7 @@ let short_name name =
let is_constructor_name name = basename name = "Ctor"
let () =
- Frama_Clang_option.Unmangling.register_mangling_func "short" short_name;
- Frama_Clang_option.Unmangling.register_mangling_func "full" unmangle;
- Frama_Clang_option.Unmangling.set "short"
+ Frama_Clang_option.add_unmangling_function
+ "without-qualifier" "short version of the symbol" short_name;
+ Frama_Clang_option.add_unmangling_function
+ "fully-qualified" "fully qualified symbol" unmangle
diff --git a/tests/basic/oracle/printer.res.c b/tests/basic/oracle/printer.res.c
new file mode 100644
index 00000000..8a05f771
--- /dev/null
+++ b/tests/basic/oracle/printer.res.c
@@ -0,0 +1,50 @@
+/* Generated by Frama-C */
+struct _Z20_frama_c_vmt_content {
+ void (*method_ptr)() ;
+ int shift_this ;
+};
+struct _Z28_frama_c_rtti_name_info_node;
+struct _Z12_frama_c_vmt {
+ struct _Z20_frama_c_vmt_content *table ;
+ int table_size ;
+ struct _Z28_frama_c_rtti_name_info_node *rtti_info ;
+};
+struct _Z31_frama_c_rtti_name_info_content {
+ struct _Z28_frama_c_rtti_name_info_node *value ;
+ int shift_object ;
+ int shift_vmt ;
+};
+struct _Z28_frama_c_rtti_name_info_node {
+ char const *name ;
+ struct _Z31_frama_c_rtti_name_info_content *base_classes ;
+ int number_of_base_classes ;
+ struct _Z12_frama_c_vmt *pvmt ;
+};
+struct _ZN1AE1B;
+struct _ZN1AE1B {
+ int x ;
+};
+struct _Z28_frama_c_rtti_name_info_node _ZN1A1BE23_frama_c_rtti_name_info;
+
+/*@ requires \valid_read(this); */
+void _ZN1A1BEC1(struct _ZN1AE1B const *this __attribute__((____fc_initialized_object__)))
+{
+ this->x = 42;
+ return;
+}
+
+struct _Z28_frama_c_rtti_name_info_node _ZN1A1BE23_frama_c_rtti_name_info =
+ {.name = "B",
+ .base_classes = (struct _Z31_frama_c_rtti_name_info_content *)0,
+ .number_of_base_classes = 0,
+ .pvmt = (struct _Z12_frama_c_vmt *)0};
+int main(void)
+{
+ int __retres;
+ struct _ZN1AE1B b;
+ _ZN1A1BEC1(& b);
+ __retres = b.x;
+ return __retres;
+}
+
+
diff --git a/tests/basic/oracle/printer.res2.c b/tests/basic/oracle/printer.res2.c
new file mode 100644
index 00000000..7429be90
--- /dev/null
+++ b/tests/basic/oracle/printer.res2.c
@@ -0,0 +1,50 @@
+/* Generated by Frama-C */
+struct _frama_c_vmt_content {
+ void (*method_ptr)() ;
+ int shift_this ;
+};
+struct _frama_c_rtti_name_info_node;
+struct _frama_c_vmt {
+ struct _frama_c_vmt_content *table ;
+ int table_size ;
+ struct _frama_c_rtti_name_info_node *rtti_info ;
+};
+struct _frama_c_rtti_name_info_content {
+ struct _frama_c_rtti_name_info_node *value ;
+ int shift_object ;
+ int shift_vmt ;
+};
+struct _frama_c_rtti_name_info_node {
+ char const *name ;
+ struct _frama_c_rtti_name_info_content *base_classes ;
+ int number_of_base_classes ;
+ struct _frama_c_vmt *pvmt ;
+};
+struct B;
+struct B {
+ int x ;
+};
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
+
+/*@ requires \valid_read(this); */
+void B::Ctor(struct B const *this)
+{
+ this->x = 42;
+ return;
+}
+
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+ {.name = "B",
+ .base_classes = (struct _frama_c_rtti_name_info_content *)0,
+ .number_of_base_classes = 0,
+ .pvmt = (struct _frama_c_vmt *)0};
+int main(void)
+{
+ int __retres;
+ struct B b;
+ B::Ctor((struct B const *)(& b));
+ __retres = b.x;
+ return __retres;
+}
+
+
diff --git a/tests/basic/printer.cpp b/tests/basic/printer.cpp
index b442d7f8..88e4eea8 100644
--- a/tests/basic/printer.cpp
+++ b/tests/basic/printer.cpp
@@ -1,7 +1,7 @@
/* run.config
NOFRAMAC:
-EXECNOW: LOG printer.res.c @frama-c@ @PTEST_FILE@ @CXX@ @MACHDEP@ -cxx-keep-mangling -print-as-is -ocode printer.res.c -print
-EXECNOW: @frama-c@ @CXX@ @MACHDEP@ -cxx-demangling-short printer.res.c -print
+EXECNOW: LOG printer.res.c @frama-c@ @PTEST_FILE@ @CXX@ @MACHDEP@ -cxx-unmangling none -kernel-msg-key printer:attrs -ocode @PTEST_RESULT@/printer.res.c -print
+EXECNOW: LOG printer.res2.c @frama-c@ @CXX@ @MACHDEP@ -cxx-unmangling without-qualifier @PTEST_RESULT@/printer.res.c -ocode @PTEST_RESULT@/printer.res2.c -print
*/
namespace A {
--
GitLab