[options] refactor unmangling options and allow unmangling even on C files

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

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

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.
        *)

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

tests/basic/oracle/printer.res.c

+/* 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;
+}
+
+

tests/basic/oracle/printer.res2.c

+/* 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;
+}
+
+

tests/basic/printer.cpp

 /* 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 {