diff options
| -rw-r--r-- | Changelog | 26 | ||||
| -rw-r--r-- | README | 5 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 23 | ||||
| -rw-r--r-- | backend/CleanupLabelsproof.v | 10 | ||||
| -rw-r--r-- | backend/PrintLTLin.ml | 2 | ||||
| -rw-r--r-- | backend/PrintMach.ml | 126 | ||||
| -rw-r--r-- | cparser/Elab.ml | 2 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Compiler.v | 7 | ||||
| -rw-r--r-- | driver/Driver.ml | 49 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 19 |
12 files changed, 218 insertions, 53 deletions
@@ -1,3 +1,29 @@ +- Support for "aligned" attributes on global variables, e.g. + __attribute__((aligned(16))) int x; + +- Pointer comparisons now treated as unsigned comparisons (previously: signed). + This fixes an issue with arrays straddling the 0x8000_0000 boundary. + Consequently, the "ofs" part of pointer values "Vptr b ofs" is + now treated as unsigned (previously: signed). + +- Elimination of unreferenced labels now performed by a separate pass + (backend/CleanupLabels.v) and proved correct. + +- Stacking pass revised: supports more flexible layout of the stack + frame; two-step proof (Stackingproof + Machabstr2concr) merged + into one single proof (Stackingproof). + +- The requirement that pointers be valid in pointer comparisons + was pushed through all intermediate languages of the back-end + (previously: requirement present only in up to Csharpminor). + +- Improvements to the compiler driver: + . -E option now prints preprocessed result to standard output + instead of saving it in a .i file + . support for .s (assembly) and .S (assembly to be preprocessed) + input files + + Release 1.8.1, 2011-03-14 ========================= @@ -154,13 +154,15 @@ a C construct that it cannot process. The "ccomp" command recognizes the following classes of input files: .c C source file .cm Cminor source file + .s Assembly file + .S Assembly file, to be run through the C preprocessor .o Object code file .a Library file The "ccomp" command recognizes the following options: Processing options: - -E Preprocess only, save result in <file>.i + -E Preprocess only, send result to standard output -S Compile to assembler only, save result in <file>.s -c Compile to object file only (no linking), result in <file>.o Preprocessing options: @@ -188,6 +190,7 @@ Tracing options: -dconstprop Save RTL after constant propagation in <file>.constprop.rtl -dcse Save RTL after CSE optimization in <file>.cse.rtl -dalloc Save LTL after register allocation in <file>.alloc.ltl + -dmach Save generated Mach in <file>.mach -dasm Save generated assembly in <file>.s Linking options: -l<lib> Link library <lib> diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 66ee772..8be92fd 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -363,9 +363,7 @@ let shift_addr oc = function | SAasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n | SAror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n -module Labelset = Set.Make(struct type t = label let compare = compare end) - -let print_instruction oc labels = function +let print_instruction oc = function (* Core instructions *) | Padd(r1, r2, so) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 @@ -492,8 +490,7 @@ let print_instruction oc labels = function else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 | Plabel lbl -> - if Labelset.mem lbl labels then - fprintf oc "%a:\n" print_label lbl; 0 + fprintf oc "%a:\n" print_label lbl; 0 | Ploadsymbol(r1, id, ofs) -> let lbl = label_symbol id ofs in fprintf oc " ldr %a, .L%d @ %a\n" @@ -517,7 +514,7 @@ let no_fallthrough = function | Pbreg _ -> true | _ -> false -let rec print_instructions oc labels instrs = +let rec print_instructions oc instrs = match instrs with | [] -> () | i :: il -> @@ -532,17 +529,7 @@ let rec print_instructions oc labels instrs = emit_constants oc; fprintf oc ".L%d:\n" lbl end; - print_instructions oc labels il - -let rec labels_of_code accu = function - | [] -> - accu - | (Pb lbl | Pbc(_, lbl)) :: c -> - labels_of_code (Labelset.add lbl accu) c - | Pbtbl(_, tbl) :: c -> - labels_of_code (List.fold_right Labelset.add tbl accu) c - | _ :: c -> - labels_of_code accu c + print_instructions oc il let print_function oc name code = Hashtbl.clear current_function_labels; @@ -554,7 +541,7 @@ let print_function oc name code = if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; - print_instructions oc (labels_of_code Labelset.empty code) code; + print_instructions oc code; emit_constants oc; fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index 6201306..abd2581 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -231,14 +231,16 @@ Proof. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto with coqlib. (* Lload *) + assert (eval_addressing tge sp addr (map rs args) = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. left; econstructor; split. - econstructor; eauto. rewrite <- H. - apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto. econstructor; eauto with coqlib. (* Lstore *) + assert (eval_addressing tge sp addr (map rs args) = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. left; econstructor; split. - econstructor; eauto. rewrite <- H. - apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto. econstructor; eauto with coqlib. (* Lcall *) left; econstructor; split. diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml index 0f38a3f..e0a3204 100644 --- a/backend/PrintLTLin.ml +++ b/backend/PrintLTLin.ml @@ -83,7 +83,7 @@ let print_instruction pp i = fprintf pp "%a = builtin \"%s\"(%a)@ " reg res (extern_atom ef.ef_id) regs args | Llabel lbl -> - fprintf pp "%5ld: " (camlint_of_positive lbl) + fprintf pp "%ld:@ " (camlint_of_positive lbl) | Lgoto lbl -> fprintf pp "goto %ld@ " (camlint_of_positive lbl) | Lcond(cond, args, lbl) -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml new file mode 100644 index 0000000..5b4887e --- /dev/null +++ b/backend/PrintMach.ml @@ -0,0 +1,126 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printer for Mach code *) + +open Format +open Camlcoq +open Datatypes +open Maps +open AST +open Integers +open Locations +open Machregsaux +open Mach +open PrintOp + +let name_of_chunk = function + | Mint8signed -> "int8signed" + | Mint8unsigned -> "int8unsigned" + | Mint16signed -> "int16signed" + | Mint16unsigned -> "int16unsigned" + | Mint32 -> "int32" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + +let reg pp r = + match name_of_register r with + | Some s -> fprintf pp "%s" s + | None -> fprintf pp "<unknown reg>" + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_instruction pp i = + match i with + | Mgetstack(ofs, ty, res) -> + fprintf pp "%a = stack(%ld, %s)@ " + reg res (camlint_of_coqint ofs) (name_of_type ty) + | Msetstack(arg, ofs, ty) -> + fprintf pp "stack(%ld, %s) = %a@ " + (camlint_of_coqint ofs) (name_of_type ty) reg arg + | Mgetparam(ofs, ty, res) -> + fprintf pp "%a = param(%ld, %s)@ " + reg res (camlint_of_coqint ofs) (name_of_type ty) + | Mop(op, args, res) -> + fprintf pp "%a = %a@ " + reg res (PrintOp.print_operation reg) (op, args) + | Mload(chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]@ " + reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | Mstore(chunk, addr, args, src) -> + fprintf pp "%s[%a] = %a@ " + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + | Mcall(sg, fn) -> + fprintf pp "call %a@ " ros fn + | Mtailcall(sg, fn) -> + fprintf pp "tailcall %a@ " ros fn + | Mbuiltin(ef, args, res) -> + fprintf pp "%a = builtin \"%s\"(%a)@ " + reg res (extern_atom ef.ef_id) regs args + | Mlabel lbl -> + fprintf pp "%ld:@ " (camlint_of_positive lbl) + | Mgoto lbl -> + fprintf pp "goto %ld@ " (camlint_of_positive lbl) + | Mcond(cond, args, lbl) -> + fprintf pp "if (%a) goto %ld@ " + (PrintOp.print_condition reg) (cond, args) + (camlint_of_positive lbl) + | Mjumptable(arg, tbl) -> + let tbl = Array.of_list tbl in + fprintf pp "@[<v 2>jumptable (%a)" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "@ case %d: goto %ld" i (camlint_of_positive tbl.(i)) + done; + fprintf pp "@]@ " + | Mreturn -> + fprintf pp "return@ " + +let print_function pp f = + fprintf pp "@[<v 2>f() {@ "; + List.iter (print_instruction pp) f.fn_code; + fprintf pp "@;<0 -2>}@]@." + +let print_fundef pp fd = + match fd with + | Internal f -> print_function pp f + | External _ -> () + +let destination : string option ref = ref None +let currpp : formatter option ref = ref None + +let print_if fd = + match !destination with + | None -> () + | Some f -> + let pp = + match !currpp with + | Some pp -> pp + | None -> + let oc = open_out f in + let pp = formatter_of_out_channel oc in + currpp := Some pp; + pp + in print_fundef pp fd diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2b31009..bbb049e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1263,8 +1263,6 @@ let elab_for_expr loc env = function (* Elaboration of initializers *) -(* Initializers are first elaborated to the following type: *) - let project_init loc il = List.map (fun (what, i) -> diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b34b10a..c47d0f3 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -31,6 +31,7 @@ let option_dcastopt = ref false let option_dconstprop = ref false let option_dcse = ref false let option_dalloc = ref false +let option_dmach = ref false let option_dasm = ref false let option_E = ref false let option_S = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index bde6308..d8810a4 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -92,6 +92,7 @@ Parameter print_RTL_castopt: RTL.fundef -> unit. Parameter print_RTL_constprop: RTL.fundef -> unit. Parameter print_RTL_cse: RTL.fundef -> unit. Parameter print_LTLin: LTLin.fundef -> unit. +Parameter print_Mach: Mach.fundef -> unit. Open Local Scope string_scope. @@ -113,7 +114,7 @@ Notation "a @@ b" := (apply_total _ _ a b) (at level 50, left associativity). Definition print {A: Type} (printer: A -> unit) (prog: A) : A := - match printer prog with tt => prog end. + let unused := printer prog in prog. (** We define three translation functions for whole programs: one starting with a C program, one with a Cminor program, one with an @@ -149,6 +150,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@ print print_LTLin @@ Reload.transf_fundef @@@ Stacking.transf_fundef + @@ print print_Mach @@@ Asmgen.transf_fundef. (* Here is the translation of a CminorSel function to an Asm function. *) @@ -316,7 +318,7 @@ Proof. Reloadtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. - eapply Asmgenproof.transf_program_correct; eauto 6. + eapply Asmgenproof.transf_program_correct; eauto 8. eapply Stackingproof.transf_program_correct; eauto 6. eapply Reloadproof.transf_program_correct; eauto. eapply CleanupLabelsproof.transf_program_correct; eauto. @@ -341,7 +343,6 @@ Proof. eapply transf_rtl_program_correct; eauto. eapply RTLgenproof.transf_program_correct; eauto. eapply Selectionproof.transf_program_correct; eauto. - rewrite print_identity. auto. Qed. Theorem transf_c_program_correct: diff --git a/driver/Driver.ml b/driver/Driver.ml index ee48ffc..87b1569 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -46,16 +46,18 @@ let print_error oc msg = (* From C to preprocessed C *) let preprocess ifile ofile = + let output = + if ofile = "-" then "" else sprintf "> %s" ofile in let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s > %s" + sprintf "%s -D__COMPCERT__ %s %s %s %s" Configuration.prepro (if Configuration.need_stdlib_wrapper then sprintf "-I%s" !stdlib_path else "") (quote_options !prepro_options) - ifile ofile in + ifile output in if command cmd <> 0 then begin - safe_remove ofile; + if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 end @@ -103,6 +105,7 @@ let compile_c_file sourcename ifile ofile = set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl"; set_dest PrintRTL.destination_cse option_dcse ".cse.rtl"; set_dest PrintLTLin.destination option_dalloc ".alloc.ltl"; + set_dest PrintMach.destination option_dmach ".mach"; (* Convert to Asm *) let asm = match Compiler.transf_c_program csyntax with @@ -152,7 +155,6 @@ let assemble ifile ofile = sprintf "%s -o %s %s" Configuration.asm ofile ifile in let retcode = command cmd in - if not !option_dasm then safe_remove ifile; if retcode <> 0 then begin safe_remove ofile; eprintf "Error during assembling.\n"; @@ -177,7 +179,7 @@ let linker exe_name files = let process_c_file sourcename = let prefixname = Filename.chop_suffix sourcename ".c" in if !option_E then begin - preprocess sourcename (prefixname ^ ".i") + preprocess sourcename "-" end else begin let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; @@ -189,7 +191,8 @@ let process_c_file sourcename = then prefixname ^ ".s" else Filename.temp_file "compcert" ".s" in compile_c_file sourcename preproname asmname; - assemble asmname (prefixname ^ ".o") + assemble asmname (prefixname ^ ".o"); + if not !option_dasm then safe_remove asmname end end; prefixname ^ ".o" @@ -206,7 +209,27 @@ let process_cminor_file sourcename = then prefixname ^ ".s" else Filename.temp_file "compcert" ".s" in compile_cminor_file sourcename asmname; - assemble asmname (prefixname ^ ".o") + assemble asmname (prefixname ^ ".o"); + if not !option_dasm then safe_remove asmname + end; + prefixname ^ ".o" + +(* Processing of .S and .s files *) + +let process_s_file sourcename = + let prefixname = Filename.chop_suffix sourcename ".s" in + assemble sourcename (prefixname ^ ".o"); + prefixname ^ ".o" + +let process_S_file sourcename = + let prefixname = Filename.chop_suffix sourcename ".s" in + if !option_E then begin + preprocess sourcename "-" + end else begin + let preproname = Filename.temp_file "compcert" ".s" in + preprocess sourcename preproname; + assemble preproname (prefixname ^ ".o"); + safe_remove preproname end; prefixname ^ ".o" @@ -217,10 +240,12 @@ let usage_string = Recognized source files: .c C source file .cm Cminor source file + .s Assembly file + .S Assembly file, to be run through the preprocessor .o Object file .a Library file Processing options: - -E Preprocess only, save result in <file>.i + -E Preprocess only, send result to standard output -S Compile to assembler only, save result in <file>.s -c Compile to object file only (no linking), result in <file>.o Preprocessing options: @@ -248,6 +273,7 @@ Tracing options: -dconstprop Save RTL after constant propagation in <file>.constprop.rtl -dcse Save RTL after CSE optimization in <file>.cse.rtl -dalloc Save LTL after register allocation in <file>.alloc.ltl + -dmach Save generated Mach code in <file>.mach -dasm Save generated assembly in <file>.s Linking options: -l<lib> Link library <lib> @@ -332,6 +358,7 @@ let cmdline_actions = "-dconstprop$", Set option_dconstprop; "-dcse$", Set option_dcse; "-dalloc$", Set option_dalloc; + "-dmach$", Set option_dmach; "-dasm$", Set option_dasm; "-E$", Set option_E; "-S$", Set option_S; @@ -343,6 +370,12 @@ let cmdline_actions = ".*\\.cm$", Self (fun s -> let objfile = process_cminor_file s in linker_options := objfile :: !linker_options); + ".*\\.s$", Self (fun s -> + let objfile = process_s_file s in + linker_options := objfile :: !linker_options); + ".*\\.S$", Self (fun s -> + let objfile = process_S_file s in + linker_options := objfile :: !linker_options); ".*\\.[oa]$", Self (fun s -> linker_options := s :: !linker_options); "-fsmall-data$", Integer(fun n -> option_small_data := n); diff --git a/extraction/extraction.v b/extraction/extraction.v index 5fc6795..765bebd 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -91,6 +91,7 @@ Extract Constant Compiler.print_RTL_castopt => "PrintRTL.print_castopt". Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop". Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse". Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if". +Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 2264498..daa7f90 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -422,12 +422,10 @@ let print_annotation oc txt args res = (* Printing of instructions *) -module Labelset = Set.Make(struct type t = label let compare = compare end) - let float_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] -let print_instruction oc labels = function +let print_instruction oc = function | Padd(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Paddi(r1, r2, c) -> @@ -654,8 +652,7 @@ let print_instruction oc labels = function | Pxoris(r1, r2, c) -> fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c | Plabel lbl -> - if Labelset.mem lbl labels then - fprintf oc "%a:\n" label (transl_label lbl) + fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> let name = extern_atom ef.ef_id in if Str.string_match re_builtin_annotation name 0 @@ -673,16 +670,6 @@ let print_jumptable oc (lbl, tbl) = (fun l -> fprintf oc " .long %a\n" label (transl_label l)) tbl -let rec labels_of_code accu = function - | [] -> - accu - | (Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)) :: c -> - labels_of_code (Labelset.add lbl accu) c - | Pbtbl(_, tbl) :: c -> - labels_of_code (List.fold_right Labelset.add tbl accu) c - | _ :: c -> - labels_of_code accu c - let print_function oc name code = Hashtbl.clear current_function_labels; float_literals := []; @@ -693,7 +680,7 @@ let print_function oc name code = if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; - List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code; + List.iter (print_instruction oc) code; if target <> MacOS then begin fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name |