diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/PrintAsm.ml | 95 | ||||
-rw-r--r-- | ia32/ValueAOp.v | 13 |
2 files changed, 68 insertions, 40 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 5c84af6b..b0ef0180 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -57,7 +57,7 @@ let preg oc = function (* System dependend printer functions *) -module type SYSTEM= +module type SYSTEM = sig val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit @@ -69,6 +69,8 @@ module type SYSTEM= val print_fun_info: out_channel -> P.t -> unit val print_var_info: out_channel -> P.t -> unit val print_epilogue: out_channel -> unit + val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit + val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit end (* Printer functions for cygwin *) @@ -86,8 +88,10 @@ module Cygwin_System = let name_of_section = function | Section_text -> ".text" - | Section_data _ | Section_small_data _ -> ".data" - | Section_const | Section_small_const -> ".section .rdata,\"dr\"" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rdata,\"dr\"" else "COMM" | Section_string -> ".section .rdata,\"dr\"" | Section_literal -> ".section .rdata,\"dr\"" | Section_jumptable -> ".text" @@ -108,6 +112,14 @@ module Cygwin_System = let print_var_info _ _ = () let print_epilogue _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + end:SYSTEM) (* Printer functions for ELF *) @@ -125,8 +137,10 @@ module ELF_System = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> if i then ".data" else "COMM" - | Section_const | Section_small_const -> ".section .rodata" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rodata" else "COMM" | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" | Section_jumptable -> ".text" @@ -151,6 +165,14 @@ module ELF_System = fprintf oc " .size %a, . - %a\n" symbol name symbol name let print_epilogue _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + end:SYSTEM) (* Printer functions for MacOS *) @@ -161,15 +183,17 @@ module MacOS_System = fprintf oc "_%s" s let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + fprintf oc "_%s" (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl let name_of_section = function | Section_text -> ".text" - | Section_data _ | Section_small_data _ -> ".data" - | Section_const | Section_small_const -> ".const" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".const" else "COMM" | Section_string -> ".const" | Section_literal -> ".literal8" | Section_jumptable -> ".const" @@ -206,7 +230,16 @@ module MacOS_System = fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; fprintf oc " .indirect_symbol %a\n" raw_symbol s; fprintf oc " .long 0\n") - !indirect_symbols + !indirect_symbols; + indirect_symbols := StringSet.empty + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + let print_lcomm_decl oc name sz al = + fprintf oc " .lcomm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) end:SYSTEM) @@ -231,8 +264,7 @@ let transl_label lbl = Hashtbl.add current_function_labels lbl lbl'; lbl' - -(* basic printing functions *) +(* Basic printing functions *) let comment = "#" @@ -275,6 +307,7 @@ let name_of_neg_condition = function (* Names of sections *) + let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -305,24 +338,11 @@ let need_masks = ref false (* Emit .file / .loc debugging directives *) -let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7 - let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - let filenum = - try - Hashtbl.find filename_num file - with Not_found -> - let n = Hashtbl.length filename_num + 1 in - Hashtbl.add filename_num file n; - fprintf oc " .file %d %S\n" n file; - n - in fprintf oc " .loc %d %s\n" filenum line - end + PrintAnnot.print_file_line oc comment file line let print_location oc loc = - if loc <> Cutil.no_loc then - print_file_line oc (fst loc) (string_of_int (snd loc)) + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) (* Emit .cfi directives *) @@ -350,7 +370,8 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" let print_annot_stmt oc txt targs args = if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt) + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args @@ -638,7 +659,6 @@ let print_builtin_inline oc name args res = let float64_literals : (int * int64) list ref = ref [] let float32_literals : (int * int32) list ref = ref [] let jumptables : (int * label list) list ref = ref [] -let indirect_symbols : StringSet.t ref = ref StringSet.empty (* Reminder on AT&T syntax: op source, dest *) @@ -996,12 +1016,9 @@ let print_var oc name v = end else begin let sz = match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - if C2C.atom_is_static name then - fprintf oc " .local %a\n" symbol name; - fprintf oc " .comm %a, %s, %d\n" - symbol name - (Z.to_string sz) - align + if C2C.atom_is_static name + then Target.print_lcomm_decl oc name sz align + else Target.print_comm_decl oc name sz align end let print_globdef oc (name, gdef) = @@ -1013,7 +1030,6 @@ end) type target = ELF | MacOS | Cygwin - let print_program oc p = let target = match Configuration.system with @@ -1028,11 +1044,12 @@ let print_program oc p = | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in let module Printer = AsmPrinter(Target) in PrintAnnot.print_version_and_options oc Printer.comment; + PrintAnnot.reset_filenames(); Printer.need_masks := false; - Hashtbl.clear Printer.filename_num; List.iter (Printer.print_globdef oc) p.prog_defs; if !Printer.need_masks then begin - Printer.section oc Section_const; (* not Section_literal because not 8-bytes *) + Printer.section oc (Section_const true); + (* not Section_literal because not 8-bytes *) Target.print_align oc 16; fprintf oc "%a: .quad 0x8000000000000000, 0\n" Target.raw_symbol "__negd_mask"; @@ -1042,4 +1059,6 @@ let print_program oc p = Target.raw_symbol "__negs_mask"; fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" Target.raw_symbol "__abss_mask" - end + end; + Target.print_epilogue oc; + PrintAnnot.close_filenames() diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 874c2be3..53013337 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop - | Oindirectsymbol id, nil => Ptr (Gl id Int.zero) + | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast8unsigned, v1 :: nil => zero_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 @@ -145,7 +145,16 @@ Proof. intros; apply symbol_address_sound; apply GENV. Qed. -Hint Resolve symbol_address_sound: va. +Lemma symbol_address_sound_2: + forall id ofs, + vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + constructor. constructor. apply GENV; auto. + constructor. +Qed. + +Hint Resolve symbol_address_sound symbol_address_sound_2: va. Ltac InvHyps := match goal with |