diff options
| -rw-r--r-- | cfrontend/PrintClight.ml | 41 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 | ||||
| -rw-r--r-- | exportclight/Clightgen.ml | 2 |
3 files changed, 35 insertions, 16 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ca378c11..e63067a9 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -236,10 +236,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 +263,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 +281,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 +291,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 diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index 4209975a..f7279a5e 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -45,7 +45,7 @@ let compile_c_ast sourcename csyntax ofile = | Errors.Error msg -> fatal_error loc "%a" print_error msg in (* Dump Clight in C syntax if requested *) - PrintClight.print_if clight; + PrintClight.print_if_2 clight; (* Print Clight in Coq syntax *) let oc = open_out ofile in ExportClight.print_program (Format.formatter_of_out_channel oc) |