Moved constant expansion into Asmexpand. (#40)

This commit introduces a new pass which is run after the expansion of the
builtin functions which performs the expansion and placement of
constants inside the function code.

5 files changed, 419 insertions, 318 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 613f027b..c05ec3e9 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -130,6 +130,11 @@ Inductive testcond : Type :=
   | TCgt: testcond    (**r signed greater *)
   | TCle: testcond.   (**r signed less than or equal *)
 
+Inductive code_constant: Type :=
+| Float32 : label -> float32 -> code_constant
+| Float64 : label -> float -> code_constant
+| Symbol : label -> ident -> ptrofs -> code_constant.
+
 Inductive instruction : Type :=
   (* Core instructions *)
   | Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *)
@@ -246,8 +251,16 @@ Inductive instruction : Type :=
   | Pfcpy_fii: freg -> ireg -> ireg -> instruction    (**r copy integer register pair to double fp-register  *)
   | Pfcpy_fi: freg -> ireg -> instruction            (**r copy integer register to single fp-register *)
   | Pfcpy_iif: ireg -> ireg -> freg -> instruction    (**r copy double fp-register to integer register pair *)
-  | Pfcpy_if: ireg -> freg -> instruction.           (**r copy single fp-register to integer register *)
+  | Pfcpy_if: ireg -> freg -> instruction            (**r copy single fp-register to integer register *)
 
+  (* Instructions for the emitting of constants *)
+  | Pconstants: list code_constant -> instruction   (**r constants in code*)
+  | Ploadsymbol_imm: ireg -> ident -> ptrofs -> instruction (**r move symbol address in register *)
+  | Pflid_lbl: freg -> label -> float -> instruction (**r load float64 from label *)
+  | Pflis_lbl: freg -> label -> float32 -> instruction (**r load float32 from label *)
+  | Pflid_imm: freg -> float -> instruction          (**r move float64 into register *)
+  | Pflis_imm: freg -> float32 -> instruction        (**r move float32 into register *)
+  | Ploadsymbol_lbl: ireg -> label -> ident -> ptrofs -> instruction. (**r load symbol address from label *)
 
 (** The pseudo-instructions are the following:
 
@@ -807,7 +820,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfcpy_fii _ _ _
   | Pfcpy_fi _ _
   | Pfcpy_iif _ _ _
-  | Pfcpy_if _ _ =>
+  | Pfcpy_if _ _
+  | Pconstants _
+  | Ploadsymbol_imm _ _ _
+  | Pflid_lbl _ _ _
+  | Pflis_lbl _ _ _
+  | Pflid_imm _ _
+  | Pflis_imm _ _
+  | Ploadsymbol_lbl _ _ _ _
+    =>
     Stuck
   end.
 
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 2627f29b..e105ea20 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -20,24 +20,26 @@ open Camlcoq
 open Json
 
 let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic"; "Pblreg";
-                       "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pfcpy_iif";
-                       "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd";
+                       "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pconstants";"Pfcpy_iif";
+                       "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pflid_lbl"; "Pflis_lbl"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd";
                        "Pfabss"; "Pfaddd"; "Pfadds"; "Pfcmpd"; "Pfcmps"; "Pfcmpzd"; "Pfcmpzs";
                        "Pfcpyd"; "Pfcpy_fs"; "Pfcpy_if";"Pfcvtds"; "Pfcvtsd"; "Pfdivd"; "Pfdivs"; "Pfldd";
-                       "Pfldd_a"; "Pflds"; "Pflid"; "Pflis"; "Pfmuld"; "Pfmuls"; "Pfnegd";
+                       "Pfldd_a"; "Pflid"; "Pflds"; "Pflid_imm"; "Pflis_imm"; "Pfmuld"; "Pfmuls"; "Pfnegd";
                        "Pfnegs"; "Pfreeframe"; "Pfsitod"; "Pfsitos"; "Pfsqrt"; "Pfstd"; "Pfstd_a";
                        "Pfsts"; "Pfsubd"; "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd";
                        "Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr";
-                       "Pldr_a"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb";
-                       "Pldrsh"; "Ploadsymbol"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite";
-                       "Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Porr"; "Ppush"; "Prev"; "Prev16"; "Prsb";
-                       "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull"; "Pstr"; "Pstr_a";
-                       "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv";
+                       "Pldr_a"; "Ploadsymbol_lbl"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb";
+                       "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite";
+                       "Pmovt"; "Pmovw"; "Pmul"; "Pmvn";  "Ploadsymbol_imm"; "Porr";
+                       "Ppush"; "Prev"; "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull";
+                       "Pstr"; "Pstr_a"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv";
                        "Pumull" ]
 
 type instruction_arg =
   | ALabel of positive
   | Atom of positive
+  | Data32 of Integers.Int.int
+  | Data64 of Integers.Int64.int
   | DFreg of freg
   | Float32 of Floats.float32
   | Float64 of Floats.float
@@ -51,6 +53,12 @@ type instruction_arg =
   | Symbol of ident * BinNums.coq_Z
   | Condition of string
 
+let makedata (c : code_constant) : instruction_arg =
+ match c with
+ | Asm.Float32(_, f) -> Data32 (Floats.Float32.to_bits f)
+ | Asm.Float64(_, f) -> Data64 (Floats.Float.to_bits f)
+ | Asm.Symbol(_, id, ofs) -> Symbol(id, ofs)
+
 let pp_reg pp reg =
   pp_jsingle_object pp "Register" pp_jstring reg
 
@@ -104,6 +112,8 @@ let pp_symbol pp (id, ofs) =
 let pp_arg pp = function
   | ALabel lbl -> pp_label pp lbl
   | Atom a -> pp_atom_constant pp a
+  | Data32 i -> pp_jsingle_object pp "Data32" pp_int i
+  | Data64 i -> pp_jsingle_object pp "Data64" pp_int64 i
   | DFreg fr -> pp_freg pp fr
   | Float32 f -> pp_float32_constant pp f
   | Float64 f  -> pp_float64_constant pp f
@@ -177,6 +187,9 @@ let pp_instructions pp ic =
     (* Call Frame Information, only debug relevant and not exported *)
     | Pcfi_adjust _ -> assert false
     | Pcfi_rel_offset _ -> assert false
+    (* Should be eliminated in constant expansion step *)
+    | Pflis(r1, f) -> assert false
+    | Ploadsymbol(r1, id, ofs) -> assert false
     (* ARM instructions *)
     | Padc(r1, r2, so) -> instruction pp "Padc" [Ireg r1; Ireg r2; Shift so]
     | Padd(r1, r2, so) -> instruction pp "Padd" [Ireg r1; Ireg r2; Shift so]
@@ -213,7 +226,6 @@ let pp_instructions pp ic =
     | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> instruction pp "Pfldd" [DFreg r1; Ireg r2; Long n]
     | Pflds(r1, r2, n) -> instruction pp "Pflds" [SFreg r1; Ireg r2; Long n]
     | Pflid(r1, f) -> instruction pp "Pflid" [DFreg r1; Float64 f]
-    | Pflis(r1, f) -> instruction pp "Pflis" [SFreg r1; Float32 f]
     | Pfmuld(r1, r2, r3) -> instruction pp "Pfmuld" [DFreg r1; DFreg r2; DFreg r3]
     | Pfmuls(r1, r2, r3) -> instruction pp "Pfmuls" [SFreg r1; SFreg r2; SFreg r3]
     | Pfnegd(r1, r2) -> instruction pp "Pfnegd" [DFreg r1; DFreg r2]
@@ -241,7 +253,6 @@ let pp_instructions pp ic =
     | Pldrh_p(r1, r2, so) -> instruction pp "Pldrh_p" [Ireg r1; Ireg r2; Shift so]
     | Pldrsb(r1, r2, so) -> instruction pp "Pldrsb" [Ireg r1; Ireg r2; Shift so]
     | Pldrsh(r1, r2, so) -> instruction pp "Pldrsh" [Ireg r1; Ireg r2; Shift so]
-    | Ploadsymbol(r1, id, ofs) -> instruction pp "Ploadsymbol" [Ireg r1; Symbol (id, ofs)]
     | Plsl(r1, r2, r3) -> instruction pp "Plsl" [Ireg r1; Ireg r2; Ireg r3]
     | Plsr(r1, r2, r3) -> instruction pp "Plsr" [Ireg r1; Ireg r2; Ireg r3]
     | Pmla(r1, r2, r3, r4) -> instruction pp "Pmla" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
@@ -279,6 +290,14 @@ let pp_instructions pp ic =
     | Pfcpy_fi(r1, r2) -> instruction pp "Pfcpy_fi" [SFreg r1; Ireg r2]
     | Pfcpy_iif(r1, r2, r3) -> instruction pp "Pfcpy_iif" [Ireg r1; Ireg r2; DFreg r3]
     | Pfcpy_if (r1,r2) -> instruction pp "Pfcpy_if" [Ireg r1; SFreg r2]
+    (* Pseudo instructions from constant expansion step *)
+    | Pconstants consts -> instruction pp "Pconstants" (List.map makedata consts)
+    | Ploadsymbol_imm (r1,id,ofs) -> instruction pp "Ploadsymbol_imm" [Ireg r1; Symbol (id,ofs)]
+    | Pflid_lbl (r1,lbl,f) -> instruction pp "Pflid_lbl" [DFreg r1; ALabel lbl; Float64 f]
+    | Pflis_lbl (r1,lbl,f) -> instruction pp "Pflis_lbl" [SFreg r1; ALabel lbl; Float32 f]
+    | Pflid_imm (r1,f) -> instruction pp "Pflid_imm" [DFreg r1; Float64 f]
+    | Pflis_imm (r1,f) -> instruction pp "Pflis_imm" [SFreg r1; Float32 f]
+    | Ploadsymbol_lbl (r1,lbl,id,ofs) -> instruction pp "Ploadsymbol_lbl" [Ireg r1; ALabel lbl; Symbol (id,ofs)]
   in
     pp_jarray instruction pp ic
 
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 6c6b4a11..7c18be6b 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -669,7 +669,9 @@ let expand_function id fn =
       expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code
     else
       List.iter expand_instruction fn.fn_code;
-    Errors.OK (get_current_function ())
+    let fn = get_current_function () in
+    let fn = Constantexpand.expand_constants fn in
+    Errors.OK fn
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
 
diff --git a/arm/Constantexpand.ml b/arm/Constantexpand.ml
new file mode 100644
index 00000000..408b291e
--- /dev/null
+++ b/arm/Constantexpand.ml
@@ -0,0 +1,197 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  AbsInt Angewandte Informatik GmbH. All rights reserved. This file  *)
+(*  is distributed under the terms of the INRIA Non-Commercial         *)
+(*  License Agreement.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Asm
+open Asmexpandaux
+open AST
+ open Camlcoq
+(* open Integers *)
+
+let _0 = Integers.Int.zero
+
+(* Options controlling the output of the constants *)
+
+let literals_in_code = ref true     (* to be turned into a proper option *)
+
+let vfpv3 = Configuration.model >= "armv7"
+
+
+(* Record current code position and latest position at which to
+   emit float and symbol constants. *)
+
+let currpos = ref 0
+let size_constants = ref 0
+let max_pos_constants = ref max_int
+
+let distance_to_emit_constants () =
+  if !literals_in_code
+  then !max_pos_constants - (!currpos + !size_constants)
+  else max_int
+
+
+(* Associate labels to floating-point constants and to symbols *)
+
+let float_labels = (Hashtbl.create 39 : (Floats.float, label) Hashtbl.t)
+let float32_labels = (Hashtbl.create 39 : (Floats.float32, label) Hashtbl.t)
+let symbol_labels =
+  (Hashtbl.create 39 : (ident * Integers.Int.int, label) Hashtbl.t)
+
+let get_label tbl sz pinc bf =
+  try
+    Hashtbl.find tbl bf
+  with Not_found ->
+    let lbl' = new_label () in
+    Hashtbl.add tbl bf lbl';
+    size_constants := !size_constants + sz;
+    max_pos_constants := min !max_pos_constants (!currpos + pinc);
+    lbl'
+
+let label_float = get_label float_labels 8 1024
+let label_float32 = get_label float32_labels 4 1024
+let label_symbol id ofs = get_label symbol_labels 4 4096 (id,ofs)
+
+let reset_constants () =
+  Hashtbl.clear float_labels;
+  Hashtbl.clear float32_labels;
+  Hashtbl.clear symbol_labels;
+  size_constants := 0;
+  max_pos_constants := max_int
+
+
+(* Recognition of float constants appropriate for VMOV.
+   a normalized binary floating point encoding with 1 sign bit, 4
+   bits of fraction and a 3-bit exponent *)
+
+let is_immediate_float64 bits =
+  let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
+  let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
+  exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
+
+let is_immediate_float32 bits =
+  let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
+  let mant = Int32.logand bits 0x7F_FFFFl in
+  exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
+
+let no_fallthrough = function
+  | Pb _ -> true
+  | Pbsymb _ -> true
+  | Pbreg _ -> true
+  | _ -> false
+
+let estimate_size = function
+  | Pflid _
+  | Pflis _ -> 3
+  | Pfcmpd _
+  | Pfcmpzd _
+  | Pfsitod _
+  | Pfuitod _
+  | Pftosizd _
+  | Pftouizd _
+  | Pfcmps _
+  | Pfcmpzs _
+  | Pfsitos _
+  | Pfuitos _
+  | Pftosizs _
+  | Pftouizs _
+  | Pmovite _ -> 2
+  | Pbuiltin (ef,_,_) ->
+    begin match ef with
+    | EF_inline_asm _ -> 256
+    | _ -> 0 end
+  | Pcfi_adjust _
+  | Pcfi_rel_offset _
+  | Plabel _ -> 0
+  | Pbtbl (r,tbl) ->  2 + List.length tbl
+  | _ -> 1
+
+let expand_constants () =
+  let consts = Hashtbl.fold (fun bf lbl c ->
+      Float64 (lbl, bf)::c)
+      float_labels [] in
+  let consts = Hashtbl.fold (fun bf lbl c ->
+      Float32 (lbl, bf)::c)
+      float32_labels consts in
+  let consts = Hashtbl.fold (fun (id,ofs) lbl c ->
+      Symbol (lbl,id,ofs)::c)
+      symbol_labels consts in
+  if consts <> [] then
+    emit (Pconstants consts);
+  reset_constants ()
+
+let expand_instruction = function
+  | Pflid (r1,f) ->
+    let f' = camlint64_of_coqint(Floats.Float.to_bits f) in
+    if vfpv3 && is_immediate_float64 f' then begin
+      emit (Pflid_imm (r1,f));
+      1
+    end else if !literals_in_code then begin
+      let lbl = label_float f in
+      emit (Pflid_lbl (r1,lbl,f));
+      1
+    end else begin
+      emit (Pflid (r1,f));
+      3
+    end
+  | Pflis (r1,f) ->
+    let f' = camlint_of_coqint(Floats.Float32.to_bits f) in
+    if vfpv3 && is_immediate_float32 f' then begin
+      emit (Pflis_imm (r1,f));
+      1
+    end else if !literals_in_code then begin
+      let lbl = label_float32 f in
+      emit (Pflis_lbl (r1,lbl,f));
+      1
+    end else begin
+      let lo =  coqint_of_camlint (Int32.logand f' 0xFFFFl)
+      and hi = coqint_of_camlint (Int32.shift_right_logical f' 16) in
+      emit (Pmovw (IR14,lo));
+      emit (Pmovt (IR14,hi));
+      emit (Pfcpy_fi (r1,IR14));
+      3
+    end
+  | Ploadsymbol(r1, id, ofs) ->
+    let o = camlint_of_coqint ofs in
+    if o >= -32768l && o <= 32767l && !Clflags.option_mthumb then begin
+      emit (Ploadsymbol_imm (r1,id,ofs));
+      2
+    end else begin
+      let lbl = label_symbol id ofs in
+      emit (Ploadsymbol_lbl (r1,lbl,id,ofs));
+      1
+    end
+  | inst ->
+    emit inst;
+    estimate_size inst
+
+let rec expand_instructions no_fall = function
+  | [] -> ()
+  | i :: il ->
+    let estimate = estimate_size i * 4 in
+    let d = distance_to_emit_constants() - estimate in
+    if d < 256 && no_fall then
+      expand_constants ()
+    else if d < 16 then begin
+      let lbl = new_label () in
+      emit (Pb lbl);
+      expand_constants ();
+      emit (Plabel lbl)
+    end;
+    let n = expand_instruction i in
+    currpos := !currpos + n * 4;
+    expand_instructions (no_fallthrough i) il
+
+let expand_constants fn =
+  reset_constants ();
+  set_current_function fn;
+  expand_instructions false fn.fn_code;
+  expand_constants ();
+  get_current_function ()
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index ebaaf50e..93733f56 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -95,9 +95,6 @@ let neg_condition_name = function
 
 module Target (Opt: PRINTER_OPTIONS) : TARGET =
 struct
-  (* Code generation options. *)
-
-  let literals_in_code = ref true     (* to be turned into a proper option *)
 
   (* Basic printing functions *)
 
@@ -171,115 +168,6 @@ struct
   let section oc sec =
     fprintf oc "	%s\n" (name_of_section sec)
 
-  (* Record current code position and latest position at which to
-     emit float and symbol constants. *)
-
-  let currpos = ref 0
-  let size_constants = ref 0
-  let max_pos_constants = ref max_int
-
-  let distance_to_emit_constants () =
-    if !literals_in_code
-    then !max_pos_constants - (!currpos + !size_constants)
-    else max_int
-
-  (* Associate labels to floating-point constants and to symbols *)
-
-  let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t)
-  let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t)
-
-  let label_float bf =
-    try
-      Hashtbl.find float_labels bf
-    with Not_found ->
-      let lbl' = new_label() in
-      Hashtbl.add float_labels bf lbl';
-      size_constants := !size_constants + 8;
-      max_pos_constants := min !max_pos_constants (!currpos + 1024);
-      lbl'
-
-  let label_float32 bf =
-    try
-      Hashtbl.find float32_labels bf
-    with Not_found ->
-      let lbl' = new_label() in
-      Hashtbl.add float32_labels bf lbl';
-      size_constants := !size_constants + 4;
-      max_pos_constants := min !max_pos_constants (!currpos + 1024);
-      lbl'
-
-  let symbol_labels =
-    (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t)
-
-  let label_symbol id ofs =
-    try
-      Hashtbl.find symbol_labels (id, ofs)
-    with Not_found ->
-      let lbl' = new_label() in
-      Hashtbl.add symbol_labels (id, ofs) lbl';
-      size_constants := !size_constants + 4;
-      max_pos_constants := min !max_pos_constants (!currpos + 4096);
-      lbl'
-
-  let reset_constants () =
-    Hashtbl.clear float_labels;
-    Hashtbl.clear float32_labels;
-    Hashtbl.clear symbol_labels;
-    size_constants := 0;
-    max_pos_constants := max_int
-
-  let emit_constants oc =
-    fprintf oc "	.balign	4\n";
-    Hashtbl.iter
-      (fun bf lbl ->
-         (* Big or little-endian floats *)
-         let bfhi = Int64.shift_right_logical bf 32
-         and bflo = Int64.logand bf 0xFFFF_FFFFL in
-         if Archi.big_endian
-         then fprintf oc ".L%d:	.word	0x%Lx, 0x%Lx\n" lbl bfhi bflo
-         else fprintf oc ".L%d:	.word	0x%Lx, 0x%Lx\n" lbl bflo bfhi)
-      float_labels;
-    Hashtbl.iter
-      (fun bf lbl ->
-         fprintf oc ".L%d:	.word	0x%lx\n" lbl bf)
-      float32_labels;
-    Hashtbl.iter
-      (fun (id, ofs) lbl ->
-         fprintf oc ".L%d:	.word	%a\n"
-           lbl symbol_offset (id, ofs))
-      symbol_labels;
-    reset_constants ()
-
-  (* Generate code to load the address of id + ofs in register r *)
-
-  let loadsymbol oc r id ofs =
-    let o = camlint_of_coqint ofs in
-    if o >= -32768l && o <= 32767l && !Clflags.option_mthumb then begin
-      fprintf oc "	movw	%a, #:lower16:%a\n"
-        ireg r symbol_offset (id, ofs);
-      fprintf oc "	movt	%a, #:upper16:%a\n"
-        ireg r symbol_offset (id, ofs); 2
-    end else begin
-      let lbl = label_symbol id ofs in
-      fprintf oc "	ldr	%a, .L%d @ %a\n"
-        ireg r lbl symbol_offset (id, ofs); 1
-    end
-
-  (* Recognition of float constants appropriate for VMOV.
-     a normalized binary floating point encoding with 1 sign bit, 4
-     bits of fraction and a 3-bit exponent *)
-
-  let is_immediate_float64 bits =
-    let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
-    let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
-    exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
-
-  let is_immediate_float32 bits =
-    let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
-    let mant = Int32.logand bits 0x7F_FFFFl in
-    exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
-
-
   (* Emit .file / .loc debugging directives *)
 
   let print_file_line oc file line =
@@ -288,6 +176,24 @@ struct
 
   (* Printing of instructions *)
 
+  let print_literal64 oc n lbl =
+    let bfhi = Int64.shift_right_logical n 32
+    and bflo = Int64.logand n 0xFFFF_FFFFL in
+    if Archi.big_endian
+    then fprintf oc ".L%d:	.word	0x%Lx, 0x%Lx\n" lbl bfhi bflo
+    else fprintf oc ".L%d:	.word	0x%Lx, 0x%Lx\n" lbl bflo bfhi
+
+  let print_constants oc = function
+    | Float32 (lbl,c) ->
+      let c = camlint_of_coqint (Floats.Float32.to_bits c) in
+      fprintf oc "%a:	.word	0x%lx\n"  print_label lbl c
+    | Float64 (lbl,bf) ->
+      let bf = camlint64_of_coqint (Floats.Float.to_bits  bf)
+      and lbl = transl_label lbl in
+      print_literal64 oc bf lbl
+    | Symbol (lbl,id,ofs) ->
+      fprintf oc "%a:	.word	%a\n" print_label lbl symbol_offset (id, ofs)
+
   let shift_op oc = function
     | SOimm n -> fprintf oc "#%a" coqint n
     | SOreg r -> ireg oc r
@@ -299,286 +205,254 @@ struct
   let print_instruction oc = function
     (* Core instructions *)
     | Padc (r1,r2,so) ->
-      fprintf oc "	adc	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
+      fprintf oc "	adc	%a, %a, %a\n" ireg r1 ireg r2 shift_op so
     | Padd(r1, r2, so) ->
       fprintf oc "	add%s	%a, %a, %a\n"
         (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "")
-        ireg r1 ireg r2 shift_op so; 1
+        ireg r1 ireg r2 shift_op so
     | Padds (r1,r2,so) ->
-      fprintf oc "	adds	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
+      fprintf oc "	adds	%a, %a, %a\n" ireg r1 ireg r2 shift_op so
     | Pand(r1, r2, so) ->
       fprintf oc "	and%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 shift_op so; 1
+        thumbS ireg r1 ireg r2 shift_op so
     | Pasr(r1, r2, r3) ->
       fprintf oc "	asr%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 ireg r3; 1
+        thumbS ireg r1 ireg r2 ireg r3
     | Pb lbl ->
-      fprintf oc "	b	%a\n" print_label lbl; 1
+      fprintf oc "	b	%a\n" print_label lbl
     | Pbc(bit, lbl) ->
-      fprintf oc "	b%s	%a\n" (condition_name bit) print_label lbl; 1
+      fprintf oc "	b%s	%a\n" (condition_name bit) print_label lbl
     | Pbne lbl ->
-      fprintf oc "	bne	%a\n" print_label lbl; 1
+      fprintf oc "	bne	%a\n" print_label lbl
     | Pbsymb(id, sg) ->
-      fprintf oc "	b	%a\n" symbol id; 1
+      fprintf oc "	b	%a\n" symbol id
     | Pbreg(r, sg) ->
-      fprintf oc "	bx	%a\n" ireg r; 1
+      fprintf oc "	bx	%a\n" ireg r
     | Pblsymb(id, sg) ->
-      fprintf oc "	bl	%a\n" symbol id; 1
+      fprintf oc "	bl	%a\n" symbol id
     | Pblreg(r, sg) ->
-      fprintf oc "	blx	%a\n" ireg r; 1
+      fprintf oc "	blx	%a\n" ireg r
     | Pbic(r1, r2, so) ->
       fprintf oc "	bic%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 shift_op so; 1
+        thumbS ireg r1 ireg r2 shift_op so
     | Pclz (r1,r2) ->
-      fprintf oc "	clz	%a, %a\n" ireg r1 ireg r2; 1
+      fprintf oc "	clz	%a, %a\n" ireg r1 ireg r2
     | Pcmp(r1, so) ->
-      fprintf oc "	cmp	%a, %a\n" ireg r1 shift_op so; 1
+      fprintf oc "	cmp	%a, %a\n" ireg r1 shift_op so
     | Pdmb ->
-      fprintf oc "	dmb\n"; 1
+      fprintf oc "	dmb\n"
     | Pdsb ->
-      fprintf oc "	dsb\n"; 1
+      fprintf oc "	dsb\n"
     |  Peor(r1, r2, so) ->
       fprintf oc "	eor%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 shift_op so; 1
+        thumbS ireg r1 ireg r2 shift_op so
     | Pisb ->
-      fprintf oc "	isb\n"; 1
+      fprintf oc "	isb\n"
     | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) ->
-      fprintf oc "	ldr	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldr	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pldrb(r1, r2, sa) ->
-      fprintf oc "	ldrb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldrb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pldrh(r1, r2, sa) ->
-      fprintf oc "	ldrh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldrh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pldr_p(r1, r2, sa)  ->
-      fprintf oc "	ldr	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldr	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Pldrb_p(r1, r2, sa) ->
-      fprintf oc "	ldrb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldrb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Pldrh_p(r1, r2, sa) ->
-      fprintf oc "	ldrh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldrh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Pldrsb(r1, r2, sa) ->
-      fprintf oc "	ldrsb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldrsb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pldrsh(r1, r2, sa) ->
-      fprintf oc "	ldrsh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	ldrsh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Plsl(r1, r2, r3) ->
       fprintf oc "	lsl%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 ireg r3; 1
+        thumbS ireg r1 ireg r2 ireg r3
     | Plsr(r1, r2, r3) ->
       fprintf oc "	lsr%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 ireg r3; 1
+        thumbS ireg r1 ireg r2 ireg r3
     | Pmla(r1, r2, r3, r4) ->
-      fprintf oc "	mla	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
+      fprintf oc "	mla	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4
     | Pmov(r1, (SOimm _ | SOreg _ as so)) ->
       (* No S flag even in Thumb2 mode *)
-      fprintf oc "	mov	%a, %a\n" ireg r1 shift_op so; 1
+      fprintf oc "	mov	%a, %a\n" ireg r1 shift_op so
     | Pmov(r1, so) ->
-      fprintf oc "	mov%t	%a, %a\n" thumbS ireg r1 shift_op so; 1
+      fprintf oc "	mov%t	%a, %a\n" thumbS ireg r1 shift_op so
     | Pmovw(r1, n) ->
-      fprintf oc "	movw	%a, #%a\n" ireg r1 coqint n; 1
+      fprintf oc "	movw	%a, #%a\n" ireg r1 coqint n
     | Pmovt(r1, n) ->
-      fprintf oc "	movt	%a, #%a\n" ireg r1 coqint n; 1
+      fprintf oc "	movt	%a, #%a\n" ireg r1 coqint n
     | Pmul(r1, r2, r3) ->
-      fprintf oc "	mul	%a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1
+      fprintf oc "	mul	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
     | Pmvn(r1, so) ->
-      fprintf oc "	mvn%t	%a, %a\n" thumbS ireg r1 shift_op so; 1
+      fprintf oc "	mvn%t	%a, %a\n" thumbS ireg r1 shift_op so
     | Porr(r1, r2, so) ->
       fprintf oc "	orr%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 shift_op so; 1
+        thumbS ireg r1 ireg r2 shift_op so
     | Prev (r1,r2) ->
-      fprintf oc "	rev	%a, %a\n" ireg r1 ireg r2; 1
+      fprintf oc "	rev	%a, %a\n" ireg r1 ireg r2
     | Prev16 (r1,r2) ->
-      fprintf oc "	rev16	%a, %a\n" ireg r1 ireg r2; 1
+      fprintf oc "	rev16	%a, %a\n" ireg r1 ireg r2
     | Prsb(r1, r2, so) ->
       fprintf oc "	rsb%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 shift_op so; 1
+        thumbS ireg r1 ireg r2 shift_op so
     | Prsbs(r1, r2, so) ->
       fprintf oc "	rsbs	%a, %a, %a\n"
-        ireg r1 ireg r2 shift_op so; 1
+        ireg r1 ireg r2 shift_op so
     | Prsc (r1,r2,so) ->
-      fprintf oc "	rsc	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
+      fprintf oc "	rsc	%a, %a, %a\n" ireg r1 ireg r2 shift_op so
     | Pfsqrt (f1,f2) ->
-      fprintf oc "	vsqrt.f64 %a, %a\n" freg f1 freg f2; 1
+      fprintf oc "	vsqrt.f64 %a, %a\n" freg f1 freg f2
     | Psbc (r1,r2,sa) ->
-      fprintf oc "	sbc	%a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	sbc	%a, %a, %a\n" ireg r1 ireg r2 shift_op sa
     | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) ->
-      fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pstrb(r1, r2, sa) ->
-      fprintf oc "	strb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	strb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pstrh(r1, r2, sa) ->
-      fprintf oc "	strh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	strh	%a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa
     | Pstr_p(r1, r2, sa) ->
-      fprintf oc "	str	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	str	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Pstrb_p(r1, r2, sa) ->
-      fprintf oc "	strb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	strb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Pstrh_p(r1, r2, sa) ->
-      fprintf oc "	strh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1
+      fprintf oc "	strh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Psdiv ->
-      if Opt.hardware_idiv then begin
-        fprintf oc "	sdiv	r0, r0, r1\n"; 1
-      end else begin
-        fprintf oc "	bl	__aeabi_idiv\n"; 1
-      end
+      if Opt.hardware_idiv then
+        fprintf oc "	sdiv	r0, r0, r1\n"
+      else
+        fprintf oc "	bl	__aeabi_idiv\n"
     | Psbfx(r1, r2, lsb, sz) ->
-      fprintf oc "	sbfx	%a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1
+      fprintf oc "	sbfx	%a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz
     | Psmull(r1, r2, r3, r4) ->
-      fprintf oc "	smull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
+      fprintf oc "	smull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4
     | Psub(r1, r2, so) ->
       fprintf oc "	sub%t	%a, %a, %a\n"
-        thumbS ireg r1 ireg r2 shift_op so; 1
+        thumbS ireg r1 ireg r2 shift_op so
     | Psubs(r1, r2, so) ->
       fprintf oc "	subs	%a, %a, %a\n"
-        ireg r1 ireg r2 shift_op so; 1
+        ireg r1 ireg r2 shift_op so
     | Pudiv ->
-      if Opt.hardware_idiv then begin
-        fprintf oc "	udiv	r0, r0, r1\n"; 1
-      end else begin
-        fprintf oc "	bl	__aeabi_uidiv\n"; 1
-      end
+      if Opt.hardware_idiv then
+        fprintf oc "	udiv	r0, r0, r1\n"
+      else
+         fprintf oc "	bl	__aeabi_uidiv\n"
     | Pumull(r1, r2, r3, r4) ->
-      fprintf oc "	umull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
+      fprintf oc "	umull	%a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4
     (* Floating-point VFD instructions *)
     | Pfcpyd(r1, r2) ->
-      fprintf oc "	vmov.f64 %a, %a\n" freg r1 freg r2; 1
+      fprintf oc "	vmov.f64 %a, %a\n" freg r1 freg r2
     | Pfabsd(r1, r2) ->
-      fprintf oc "	vabs.f64 %a, %a\n" freg r1 freg r2; 1
+      fprintf oc "	vabs.f64 %a, %a\n" freg r1 freg r2
     | Pfnegd(r1, r2) ->
-      fprintf oc "	vneg.f64 %a, %a\n" freg r1 freg r2; 1
+      fprintf oc "	vneg.f64 %a, %a\n" freg r1 freg r2
     | Pfaddd(r1, r2, r3) ->
-      fprintf oc "	vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
+      fprintf oc "	vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3
     | Pfdivd(r1, r2, r3) ->
-      fprintf oc "	vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
+      fprintf oc "	vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3
     | Pfmuld(r1, r2, r3) ->
-      fprintf oc "	vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
+      fprintf oc "	vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3
     | Pfsubd(r1, r2, r3) ->
-      fprintf oc "	vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
+      fprintf oc "	vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3
     | Pflid(r1, f) ->
       let f = camlint64_of_coqint(Floats.Float.to_bits f) in
-      if Opt.vfpv3 && is_immediate_float64 f then begin
-        fprintf oc "	vmov.f64 %a, #%.15F\n"
-          freg r1 (Int64.float_of_bits f); 1
-          (* immediate floats have at most 4 bits of fraction, so they
-             should print exactly with OCaml's F decimal format. *)
-      end else if !literals_in_code then begin
-        let lbl = label_float f in
-        fprintf oc "	vldr	%a, .L%d @ %.12g\n"
-          freg r1 lbl (Int64.float_of_bits f); 1
-      end else begin
-        let lbl = label_float f in
-        fprintf oc "	movw	r14, #:lower16:.L%d\n" lbl;
-        fprintf oc "	movt	r14, #:upper16:.L%d\n" lbl;
-        fprintf oc "	vldr	%a, [r14, #0] @ %.12g\n"
-          freg r1 (Int64.float_of_bits f); 3
-      end
+      let lbl = label_literal64 f in
+      fprintf oc "	movw	r14, #:lower16:.L%d\n" lbl;
+      fprintf oc "	movt	r14, #:upper16:.L%d\n" lbl;
+      fprintf oc "	vldr	%a, [r14, #0] @ %.12g\n"
+        freg r1 (Int64.float_of_bits f)
     | Pfcmpd(r1, r2) ->
       fprintf oc "	vcmp.f64 %a, %a\n" freg r1 freg r2;
-      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
+      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"
     | Pfcmpzd(r1) ->
       fprintf oc "	vcmp.f64 %a, #0\n" freg r1;
-      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
+      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"
     | Pfsitod(r1, r2) ->
       fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
-      fprintf oc "	vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1; 2
+      fprintf oc "	vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1
     | Pfuitod(r1, r2) ->
       fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
-      fprintf oc "	vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1; 2
+      fprintf oc "	vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1
     | Pftosizd(r1, r2) ->
       fprintf oc "	vcvt.s32.f64 %a, %a\n" freg_single FR6 freg r2;
-      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
+      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6
     | Pftouizd(r1, r2) ->
       fprintf oc "	vcvt.u32.f64 %a, %a\n" freg_single FR6 freg r2;
-      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
+      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6
     | Pfabss(r1, r2) ->
-      fprintf oc "	vabs.f32 %a, %a\n" freg_single r1 freg_single r2; 1
+      fprintf oc "	vabs.f32 %a, %a\n" freg_single r1 freg_single r2
     | Pfnegs(r1, r2) ->
-      fprintf oc "	vneg.f32 %a, %a\n" freg_single r1 freg_single r2; 1
+      fprintf oc "	vneg.f32 %a, %a\n" freg_single r1 freg_single r2
     | Pfadds(r1, r2, r3) ->
-      fprintf oc "	vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
+      fprintf oc "	vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3
     | Pfdivs(r1, r2, r3) ->
-      fprintf oc "	vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
+      fprintf oc "	vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3
     | Pfmuls(r1, r2, r3) ->
-      fprintf oc "	vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
+      fprintf oc "	vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3
     | Ppush rl ->
       let first = ref true in
       let sep () = if !first then first := false else output_string oc ", " in
-      fprintf oc "	push	{%a}\n"  (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl; ;1
+      fprintf oc "	push	{%a}\n"  (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl
     | Pfsubs(r1, r2, r3) ->
-      fprintf oc "	vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
-    | Pflis(r1, f) ->
-      let f = camlint_of_coqint(Floats.Float32.to_bits f) in
-      if Opt.vfpv3 && is_immediate_float32 f then begin
-        fprintf oc "	vmov.f32 %a, #%.15F\n"
-          freg_single r1 (Int32.float_of_bits f); 1
-          (* immediate floats have at most 4 bits of fraction, so they
-             should print exactly with OCaml's F decimal format. *)
-      end else if !literals_in_code then begin
-        let lbl = label_float32 f in
-        fprintf oc "	vldr	%a, .L%d @ %.12g\n"
-          freg_single r1 lbl (Int32.float_of_bits f); 1
-      end else begin
-        fprintf oc "	movw	r14, #%ld\n" (Int32.logand f 0xFFFFl);
-        fprintf oc "	movt	r14, #%ld\n" (Int32.shift_right_logical f 16);
-        fprintf oc "	vmov	%a, r14 @ %.12g\n"
-          freg_single r1 (Int32.float_of_bits f); 3
-      end
+      fprintf oc "	vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3
+    | Pflis(r1, f) -> assert false (* Should be eliminated in expand constants *)
     | Pfcmps(r1, r2) ->
       fprintf oc "	vcmp.f32 %a, %a\n" freg_single r1 freg_single r2;
-      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
+      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"
     | Pfcmpzs(r1) ->
       fprintf oc "	vcmp.f32 %a, #0\n" freg_single r1;
-      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"; 2
+      fprintf oc "	vmrs APSR_nzcv, FPSCR\n"
     | Pfsitos(r1, r2) ->
       fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
-      fprintf oc "	vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1; 2
+      fprintf oc "	vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1
     | Pfuitos(r1, r2) ->
       fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2;
-      fprintf oc "	vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1; 2
+      fprintf oc "	vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1
     | Pftosizs(r1, r2) ->
       fprintf oc "	vcvt.s32.f32 %a, %a\n" freg_single FR6 freg_single r2;
-      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
+      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6
     | Pftouizs(r1, r2) ->
       fprintf oc "	vcvt.u32.f32 %a, %a\n" freg_single FR6 freg_single r2;
-      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6; 2
+      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single FR6
     | Pfcvtsd(r1, r2) ->
-      fprintf oc "	vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2; 1
+      fprintf oc "	vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2
     | Pfcvtds(r1, r2) ->
-      fprintf oc "	vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2; 1
+      fprintf oc "	vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2
     | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) ->
-      fprintf oc "	vldr	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
+      fprintf oc "	vldr	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n
     | Pflds(r1, r2, n) ->
-      fprintf oc "	vldr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
+      fprintf oc "	vldr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n
     | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) ->
-      fprintf oc "	vstr	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
+      fprintf oc "	vstr	%a, [%a, #%a]\n" freg r1 ireg r2 coqint n
     | Pfsts(r1, r2, n) ->
-      fprintf oc "	vstr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
+      fprintf oc "	vstr	%a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n
     (* Pseudo-instructions *)
     | Pallocframe(sz, ofs) ->
       assert false
     | Pfreeframe(sz, ofs) ->
       assert false
     | Plabel lbl ->
-      fprintf oc "%a:\n" print_label lbl; 0
-    | Ploadsymbol(r1, id, ofs) ->
-      loadsymbol oc r1 id ofs
+      fprintf oc "%a:\n" print_label lbl
+    | Ploadsymbol(r1, id, ofs) -> assert false (* Should be eliminated in expand constants *)
     | Pmovite(cond, r1, ifso, ifnot) ->
       fprintf oc "	ite	%s\n" (condition_name cond);
       fprintf oc "	mov%s	%a, %a\n"
         (condition_name cond) ireg r1 shift_op ifso;
       fprintf oc "	mov%s	%a, %a\n"
-        (neg_condition_name cond) ireg r1 shift_op ifnot; 2
+        (neg_condition_name cond) ireg r1 shift_op ifnot
     | Pbtbl(r, tbl) ->
       if !Clflags.option_mthumb then begin
         fprintf oc "	lsl	r14, %a, #2\n" ireg r;
         fprintf oc "	add	pc, r14\n";   (* 16-bit encoding *)
-        fprintf oc "	nop\n";               (* 16-bit encoding *)
+        fprintf oc "	nop\n";            (* 16-bit encoding *)
         List.iter
           (fun l -> fprintf oc "	b.w	%a\n" print_label l)
-          tbl;
-        2 + List.length tbl
+          tbl
       end else begin
         fprintf oc "	add	pc, pc, %a, lsl #2\n" ireg r;
         fprintf oc "	nop\n";
         List.iter
           (fun l -> fprintf oc "	b	%a\n" print_label l)
-          tbl;
-        2 + List.length tbl
+          tbl
       end
     | Pbuiltin(ef, args, res) ->
       begin match ef with
@@ -591,71 +465,57 @@ struct
                 ais_annot_text lbl preg_annot "sp" (camlstring_of_coqstring txt) args
               | _ -> assert false
             end in
-          fprintf oc "%s annotation: %S\n" comment annot;
-          0
+          fprintf oc "%s annotation: %S\n" comment annot
         | EF_debug(kind, txt, targs) ->
           print_debug_info comment print_file_line preg_annot "sp" oc
-            (P.to_int kind) (extern_atom txt) args;
-          0
+            (P.to_int kind) (extern_atom txt) args
         | EF_inline_asm(txt, sg, clob) ->
           fprintf oc "%s begin inline assembly\n\t" comment;
           print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
-          fprintf oc "%s end inline assembly\n" comment;
-          256 (* Better be safe than sorry  *)
+          fprintf oc "%s end inline assembly\n" comment
         | _ ->
           assert false
       end
-    | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0
-    | Pcfi_rel_offset ofs -> cfi_rel_offset oc "lr" (camlint_of_coqint ofs); 0
+    | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz)
+    | Pcfi_rel_offset ofs -> cfi_rel_offset oc "lr" (camlint_of_coqint ofs)
     (* Fixup instructions for calling conventions *)
     | Pfcpy_fs(r1, r2) ->
-      fprintf oc "	vmov.f32	%a, %a\n" freg_single r1 freg_param_single r2; 1
+      fprintf oc "	vmov.f32	%a, %a\n" freg_single r1 freg_param_single r2
     | Pfcpy_sf(r1, r2) ->
-      fprintf oc "	vmov.f32	%a, %a\n" freg_param_single r1 freg_single r2; 1
+      fprintf oc "	vmov.f32	%a, %a\n" freg_param_single r1 freg_single r2
     | Pfcpy_fii (r1, r2, r3) ->
-      fprintf oc "	vmov	%a, %a, %a\n" freg r1 ireg r2 ireg r3; 1
+      fprintf oc "	vmov	%a, %a, %a\n" freg r1 ireg r2 ireg r3
     | Pfcpy_fi (r1, r2) ->
-      fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2; 1
+      fprintf oc "	vmov	%a, %a\n" freg_single r1 ireg r2
     | Pfcpy_iif (r1, r2, r3) ->
-      fprintf oc "	vmov	%a, %a, %a\n" ireg r1 ireg r2 freg r3; 1
+      fprintf oc "	vmov	%a, %a, %a\n" ireg r1 ireg r2 freg r3
     |  Pfcpy_if (r1, r2) ->
-      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single r2; 1
-
-
-  let no_fallthrough = function
-    | Pb _ -> true
-    | Pbsymb _ -> true
-    | Pbreg _ -> true
-    | _ -> false
+      fprintf oc "	vmov	%a, %a\n" ireg r1 freg_single r2
+    | Pconstants consts ->
+      fprintf oc "	.balign	4\n";
+      List.iter (print_constants oc) consts
+    | Ploadsymbol_imm (r1,id,ofs) ->
+        fprintf oc "	movw	%a, #:lower16:%a\n"
+        ireg r1 symbol_offset (id, ofs);
+        fprintf oc "	movt	%a, #:upper16:%a\n"
+          ireg r1 symbol_offset (id, ofs)
+    | Pflid_lbl (r1,lbl,f) ->
+      fprintf oc "	vldr	%a, %a\n" freg r1 print_label lbl
+    | Pflis_lbl (r1,lbl,f) ->
+      fprintf oc "	vldr	%a, %a\n"
+        freg_single r1 print_label lbl
+    | Pflid_imm (r1,f) ->
+      let f = camlint64_of_coqint(Floats.Float.to_bits f) in
+      fprintf oc "	vmov.f64 %a, #%.15F\n"
+        freg r1 (Int64.float_of_bits f)
+    | Pflis_imm (r1,f) ->
+      let f = camlint_of_coqint(Floats.Float32.to_bits f) in
+       fprintf oc "	vmov.f32 %a, #%.15F\n"
+         freg_single r1 (Int32.float_of_bits f)
+    | Ploadsymbol_lbl (r1,lbl,id,ofs) ->
+      fprintf oc "	ldr	%a, %a\n"
+        ireg r1 print_label lbl
 
-  let estimate_size = function
-    | Pbtbl (_,tbl) ->
-      let len = List.length tbl in
-      let add =if !Clflags.option_mthumb then
-        3
-      else
-        2 in
-      (len + add) * 4
-    | Pbuiltin (EF_inline_asm _,_,_) -> 1024 (* Better be safe than sorry *)
-    | _ -> 12
-
-
-  let rec print_instructions oc no_fall instrs =
-    match instrs with
-    | [] -> ()
-    | i :: il ->
-      let d = distance_to_emit_constants() - estimate_size i in
-      if d < 256 && no_fall then
-        emit_constants oc
-      else if d < 16 then begin
-        let lbl = new_label() in
-        fprintf oc "	b	.L%d\n" lbl;
-        emit_constants oc;
-        fprintf oc ".L%d:\n" lbl
-      end;
-      let n = print_instruction oc i in
-      currpos := !currpos + n * 4;
-      print_instructions oc (no_fallthrough i) il
 
   let get_section_names name =
     let (text, lit) =
@@ -695,14 +555,16 @@ struct
 
   let print_instructions oc fn =
     current_function_sig := fn.fn_sig;
-    print_instructions oc false fn.fn_code;
-    if !literals_in_code then emit_constants oc
+    List.iter (print_instruction oc) fn.fn_code
+
 
   let emit_constants oc lit =
-    if not !literals_in_code && !size_constants > 0 then begin
+    if not !Constantexpand.literals_in_code && exists_constants () then begin
       section oc lit;
-      emit_constants oc
-    end
+      fprintf oc "	.balign 4\n";
+      Hashtbl.iter (print_literal64 oc) literal64_labels;
+    end;
+    reset_constants ()
 
   (* Data *)