Merge pull request #48 from AbsInt/json_export

Json export

arm/AsmToJSON.ml

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Simple functions to serialize powerpc Asm to JSON *)
+
+(* Dummy function *)
+
+let p_program oc prog =
+  ()

cparser/Parse.ml

@@ -29,7 +29,7 @@ let transform_program t p name =
       Some (CtoDwarf.program_to_dwarf p p1 name)
     else
       None in
-  (Rename.program p1),debug
+  (Rename.program p1 (Filename.chop_suffix name ".c")),debug
 
 let parse_transformations s =
   let t = ref CharSet.empty in

cparser/Rename.ml

@@ -42,6 +42,16 @@ let enter_public env id =
     { re_id = IdentMap.add id id env.re_id;
       re_public = StringMap.add id.name id env.re_public;
       re_used = StringSet.add id.name env.re_used }
+      
+let enter_static env id file =
+  try
+    let id' = StringMap.find id.name env.re_public in
+    { env with re_id = IdentMap.add id id' env.re_id }
+  with Not_found ->
+    let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in 
+    { re_id = IdentMap.add id id' env.re_id;
+      re_public = env.re_public;
+      re_used = StringSet.add id'.name env.re_used }
 
 (* For static or local identifiers, we make up a new name if needed *)
 (* If the same identifier has already been declared, 
@@ -249,7 +259,7 @@ let reserve_builtins () =
 
 (* Reserve global declarations with public visibility *)
 
-let rec reserve_public env = function
+let rec reserve_public env file = function
   | [] -> env
   | dcl :: rem ->
       let env' =
@@ -257,22 +267,28 @@ let rec reserve_public env = function
         | Gdecl(sto, id, _, _) ->
             begin match sto with
             | Storage_default | Storage_extern -> enter_public env id
-            | Storage_static -> env
+            | Storage_static -> if !Clflags.option_rename_static then
+                enter_static env id file 
+                  else
+                env
             | _ -> assert false
             end
         | Gfundef f ->
             begin match f.fd_storage with
             | Storage_default | Storage_extern -> enter_public env f.fd_name
-            | Storage_static -> env
+            | Storage_static -> if !Clflags.option_rename_static then
+                enter_static env f.fd_name file
+            else
+                env
             | _ -> assert false
             end
         | _ -> env in
-      reserve_public env' rem
+      reserve_public env' file rem
 
 (* Rename the program *)
 
-let program p =
+let program p file =
   globdecls
-    (reserve_public (reserve_builtins()) p)
+    (reserve_public (reserve_builtins()) file p)
     [] p
   

cparser/Rename.mli

@@ -13,4 +13,4 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-val program : C.program -> C.program
+val program : C.program -> string -> C.program

driver/Clflags.ml

@@ -59,3 +59,4 @@ let option_small_data =
        then 8 else 0)
 let option_small_const = ref (!option_small_data)
 let option_timings = ref false
+let option_rename_static = ref false

driver/Driver.ml

@@ -155,6 +155,15 @@ let dump_asm asm destfile =
   output_value oc C2C.decl_atom;
   close_out oc
 
+let jdump_magic_number = "CompCertJDUMP" ^ Version.version
+
+let dump_jasm asm destfile =
+  let oc = open_out_bin destfile in
+  fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a}"
+    jdump_magic_number AsmToJSON.p_program asm;
+  close_out oc
+
+
 (* From CompCert C AST to asm *)
 
 let compile_c_ast sourcename csyntax ofile debug =
@@ -176,9 +185,12 @@ let compile_c_ast sourcename csyntax ofile debug =
     | Errors.Error msg ->
         print_error stderr msg;
         exit 2 in
-  (* Dump Asm in binary format *)
+  (* Dump Asm in binary and JSON format *)  
   if !option_sdump then
-    dump_asm asm (output_filename sourcename ".c" ".sdump");
+    begin
+      dump_asm asm (output_filename sourcename ".c" ".sdump");
+      dump_jasm asm (output_filename sourcename ".c" ".json")
+    end;
   (* Print Asm in text form *)
   let oc = open_out ofile in
   PrintAsm.print_program oc asm debug;
@@ -429,6 +441,7 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fnone         Turn off all language support options above
 Debugging options:
   -g             Generate debugging information
+  -frename-static Rename static functions and declarations
 Optimization options: (use -fno-<opt> to turn off -f<opt>)
   -O             Optimize the compiled code [on by default]
   -O0            Do not optimize the compiled code
@@ -531,6 +544,7 @@ let cmdline_actions =
   Exact "-fnone", Self (fun _ -> unset_all language_support_options);
 (* Debugging options *)
   Exact "-g", Self (fun s -> option_g := true);
+  Exact "-frename-static", Self (fun s -> option_rename_static:= true);
 (* Code generation options -- more below *)
   Exact "-O0", Self (fun _ -> unset_all optimization_options);
   Exact "-O", Self (fun _ -> set_all optimization_options);

ia32/AsmToJSON.ml

+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Simple functions to serialize powerpc Asm to JSON *)
+
+(* Dummy function *)
+let p_program oc prog =
+  ()