1414
1515open Printf
1616open Fileinfo
17- open Maps
1817open Camlcoq
1918open Sections
2019open AST
@@ -381,17 +380,9 @@ module Target (System : SYSTEM):TARGET =
381380 assert false
382381 in leftmost_one 0 0x8000_0000_0000_0000L
383382
384- (* Determine if the displacement of a conditional branch fits the short form *)
385-
386- let short_cond_branch tbl pc lbl_dest =
387- match PTree. get lbl_dest tbl with
388- | None -> assert false
389- | Some pc_dest ->
390- let disp = pc_dest - pc in - 0x2000 < = disp && disp < 0x2000
391-
392383 (* Printing of instructions *)
393384
394- let print_instruction oc tbl pc fallthrough = function
385+ let print_instruction oc fallthrough = function
395386 | Padd (r1 , r2 , r3 ) | Padd64 (r1 , r2 , r3 ) ->
396387 fprintf oc " add %a, %a, %a\n " ireg r1 ireg r2 ireg r3
397388 | Paddc (r1 , r2 , r3 ) ->
@@ -435,14 +426,7 @@ module Target (System : SYSTEM):TARGET =
435426 | Pbf (bit , lbl ) ->
436427 if ! Clflags. option_faligncondbranchs > 0 then
437428 fprintf oc " .balign %d\n " ! Clflags. option_faligncondbranchs;
438- if short_cond_branch tbl pc lbl then
439- fprintf oc " bf %a, %a\n " crbit bit label (transl_label lbl)
440- else begin
441- let next = new_label() in
442- fprintf oc " bt %a, %a\n " crbit bit label next;
443- fprintf oc " b %a\n " label (transl_label lbl);
444- fprintf oc " %a:\n " label next
445- end
429+ fprintf oc " bf %a, %a\n " crbit bit label (transl_label lbl)
446430 | Pbl (s , sg ) ->
447431 fprintf oc " bl %a\n " symbol s
448432 | Pbs (s , sg ) ->
@@ -452,14 +436,7 @@ module Target (System : SYSTEM):TARGET =
452436 | Pbt (bit , lbl ) ->
453437 if ! Clflags. option_faligncondbranchs > 0 then
454438 fprintf oc " .balign %d\n " ! Clflags. option_faligncondbranchs;
455- if short_cond_branch tbl pc lbl then
456- fprintf oc " bt %a, %a\n " crbit bit label (transl_label lbl)
457- else begin
458- let next = new_label() in
459- fprintf oc " bf %a, %a\n " crbit bit label next;
460- fprintf oc " b %a\n " label (transl_label lbl);
461- fprintf oc " %a:\n " label next
462- end
439+ fprintf oc " bt %a, %a\n " crbit bit label (transl_label lbl)
463440 | Pbtbl (r , tbl ) ->
464441 let lbl = new_label() in
465442 fprintf oc " %s begin pseudoinstr btbl(%a)\n " comment ireg r;
@@ -866,39 +843,15 @@ module Target (System : SYSTEM):TARGET =
866843 | Pblr -> false
867844 | _ -> true
868845
869- (* Estimate the size of an Asm instruction encoding, in number of actual
870- PowerPC instructions. We can over-approximate. *)
871-
872- let instr_size = function
873- | Pbf (bit , lbl ) -> 2
874- | Pbt (bit , lbl ) -> 2
875- | Pbtbl (r , tbl ) -> 5
876- | Pldi (r1 ,c ) -> 2
877- | Plfi (r1 , c ) -> 2
878- | Plfis (r1 , c ) -> 2
879- | Plabel lbl -> 0
880- | Pbuiltin ((EF_annot _ | EF_debug _ ), args , res ) -> 0
881- | Pbuiltin (ef , args , res ) -> 3
882- | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
883- | _ -> 1
884-
885- (* Build a table label -> estimated position in generated code.
886- Used to predict if relative conditional branches can use the short form. *)
887-
888- let rec label_positions tbl pc = function
889- | [] -> tbl
890- | Plabel lbl :: c -> label_positions (PTree. set lbl pc tbl) pc c
891- | i :: c -> label_positions tbl (pc + instr_size i) c
892-
893846 (* Emit a sequence of instructions *)
894847
895848 let print_instructions oc fn =
896- let rec aux oc tbl pc fallthrough = function
849+ let rec aux oc fallthrough = function
897850 | [] -> ()
898851 | i :: c ->
899- print_instruction oc tbl pc fallthrough i;
900- aux oc tbl (pc + instr_size i) (instr_fall_through i) c in
901- aux oc (label_positions PTree. empty 0 fn.fn_code) 0 true fn.fn_code
852+ print_instruction oc fallthrough i;
853+ aux oc (instr_fall_through i) c in
854+ aux oc true fn.fn_code
902855
903856 (* Print the code for a function *)
904857
0 commit comments