diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:20:11 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-20 16:20:11 +0200 |
commit | 71cec9c9126ee4385ce12fd29dec557995d5a903 (patch) | |
tree | 26e86fc9b15680721baea86d5294ee9faaf2508c /cfrontend | |
parent | 1801685f8352b7a120d87d5b529d290728129529 (diff) | |
parent | e1725209b2b4401adc63ce5238fa5db7c134609c (diff) | |
download | compcert-kvx-71cec9c9126ee4385ce12fd29dec557995d5a903.tar.gz compcert-kvx-71cec9c9126ee4385ce12fd29dec557995d5a903.zip |
Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/PrintClight.ml | 54 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 |
2 files changed, 45 insertions, 17 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ca378c11..0e735d2d 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -23,9 +23,18 @@ open Cop open PrintCsyntax open Clight -(* Naming temporaries *) +(* Naming temporaries. + Some temporaries are obtained by lifting variables in SimplLocals. + For these we use a meaningful name "$var", as found in the table of + atoms. Other temporaries are generated during SimplExpr, and are + not in the table of atoms. We print them as "$NNN" (a unique + integer). *) -let temp_name (id: AST.ident) = "$" ^ Z.to_string (Z.Zpos id) +let temp_name (id: AST.ident) = + try + "$" ^ Hashtbl.find string_of_atom id + with Not_found -> + Printf.sprintf "$%d" (P.to_int id) (* Declarator (identifier + type) -- reuse from PrintCsyntax *) @@ -236,10 +245,20 @@ and print_stmt_for p s = | _ -> fprintf p "({ %a })" print_stmt s -let print_function p id f = +(* There are two versions of Clight, Clight1 and Clight2, that differ + only in the meaning of function parameters: + - in Clight1, function parameters are variables + - in Clight2, function parameters are temporaries. +*) + +type clight_version = Clight1 | Clight2 + +let name_param = function Clight1 -> extern_atom | Clight2 -> temp_name + +let print_function ver p id f = fprintf p "%s@ " - (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params f.fn_callconv) + (name_cdecl (name_function_parameters (name_param ver) + (extern_atom id) f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[<v 2>{@ "; List.iter @@ -253,12 +272,12 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p id fd = +let print_fundef ver p id fd = match fd with | Ctypes.External(_, _, _, _) -> () | Internal f -> - print_function p id f + print_function ver p id f let print_fundecl p id fd = match fd with @@ -271,9 +290,9 @@ let print_fundecl p id fd = fprintf p "%s;@ " (name_cdecl (extern_atom id) (Clight.type_of_function f)) -let print_globdef p (id, gd) = +let print_globdef var p (id, gd) = match gd with - | AST.Gfun f -> print_fundef p id f + | AST.Gfun f -> print_fundef var p id f | AST.Gvar v -> print_globvar p id v (* from PrintCsyntax *) let print_globdecl p (id, gd) = @@ -281,20 +300,29 @@ let print_globdecl p (id, gd) = | AST.Gfun f -> print_fundecl p id f | AST.Gvar v -> () -let print_program p prog = +let print_program ver p prog = fprintf p "@[<v 0>"; List.iter (declare_composite p) prog.prog_types; List.iter (define_composite p) prog.prog_types; List.iter (print_globdecl p) prog.prog_defs; - List.iter (print_globdef p) prog.prog_defs; + List.iter (print_globdef ver p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None -let print_if prog = +let print_if_gen ver prog = match !destination with | None -> () | Some f -> let oc = open_out f in - print_program (formatter_of_out_channel oc) prog; + print_program ver (formatter_of_out_channel oc) prog; close_out oc + +(* print_if is called from driver/Compiler.v between the SimplExpr + and SimplLocals passes. It receives Clight1 syntax. *) +let print_if prog = print_if_gen Clight1 prog + +(* print_if_2 is called from clightgen/Clightgen.ml, after the + SimplLocals pass. It receives Clight2 syntax. *) +let print_if_2 prog = print_if_gen Clight2 prog + diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 3a44796c..1c9729c5 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -391,7 +391,7 @@ and print_stmt_for p s = | _ -> fprintf p "({ %a })" print_stmt s -let name_function_parameters fun_name params cconv = +let name_function_parameters name_param fun_name params cconv = let b = Buffer.create 20 in Buffer.add_string b fun_name; Buffer.add_char b '('; @@ -404,7 +404,7 @@ let name_function_parameters fun_name params cconv = if cconv.cc_vararg then Buffer.add_string b ",..." | (id, ty) :: rem -> if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl (extern_atom id) ty); + Buffer.add_string b (name_cdecl (name_param id) ty); add_params false rem in add_params true params end; @@ -413,8 +413,8 @@ let name_function_parameters fun_name params cconv = let print_function p id f = fprintf p "%s@ " - (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params f.fn_callconv) + (name_cdecl (name_function_parameters extern_atom + (extern_atom id) f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[<v 2>{@ "; List.iter |