diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-08-24 19:06:46 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-03 10:38:50 +0200 |
| commit | ad6467099ac7147040c59c022635e61370168568 (patch) | |
| tree | ec78577bf5c8bb8c3f96c05f82648d439f52ceaf /backend | |
| parent | 6f26a95f2debe76e1350eea97c2162e5bcd8cfad (diff) | |
| download | compcert-ad6467099ac7147040c59c022635e61370168568.tar.gz compcert-ad6467099ac7147040c59c022635e61370168568.zip | |
Refactor emitting of constants.
The function was the same for nearly all backends and also the way 32 bit
literals are printed so we moved it to PrintAsm. The 64 bit literals
however are still target specific.
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/PrintAsm.ml | 15 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 2 |
2 files changed, 15 insertions, 2 deletions
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 6d1fafd6..b267dfd8 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -37,6 +37,19 @@ module Printer(Target:TARGET) = let print_location oc loc = if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc) + let emit_constants oc lit = + if Hashtbl.length literal64_labels > 0 then begin + Target.section oc (Sections.with_size 8 lit); + Target.print_align oc 8; + iter_literal64 (Target.print_literal64 oc) + end; + if Hashtbl.length literal32_labels > 0 then begin + Target.section oc (Sections.with_size 4 lit); + Target.print_align oc 4; + iter_literal32 (fun n lbl -> fprintf oc "%a: .long 0x%lx\n" Target.label lbl n); + end; + reset_literals () + let get_section_names name = match C2C.atom_sections name with | [t;l;j] -> (t, l, j) @@ -65,7 +78,7 @@ module Printer(Target:TARGET) = Target.cfi_endproc oc; print_debug_label oc e; Target.print_fun_info oc name; - Target.emit_constants oc lit; + emit_constants oc lit; Target.print_jumptable oc jmptbl; if !Clflags.option_g then Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index df2f72f2..2241edfd 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -33,7 +33,7 @@ module type TARGET = val cfi_startproc: out_channel -> unit val print_instructions: out_channel -> coq_function -> unit val cfi_endproc: out_channel -> unit - val emit_constants: out_channel -> section_name -> unit + val print_literal64 : out_channel -> int64 -> int -> unit val print_jumptable: out_channel -> section_name -> unit val section: out_channel -> section_name -> unit val name_of_section: section_name -> string |