Update for single-precision floats. Calls to vararg functions remain

to be updated.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 153 insertions, 32 deletions

diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index c84bd55..9bb2009 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -157,20 +157,29 @@ let string_of_instruction = function
 | Pextsh    (i0, i1)            -> "Pextsh(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")"
 | Pfreeframe(c0, i1)            -> "Pfreeframe(" ^ string_of_coq_Z c0 ^ ", " ^ string_of_iint i1 ^ ")"
 | Pfabs     (f0, f1)            -> "Pfabs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
+| Pfabss    (f0, f1)            -> "Pfabss(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
 | Pfadd     (f0, f1, f2)        -> "Pfadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
+| Pfadds    (f0, f1, f2)        -> "Pfadds(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
 | Pfcmpu    (f0, f1)            -> "Pfcmpu(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
 | Pfcti     (i0, f1)            -> "Pfcti(" ^ string_of_ireg i0 ^ ", " ^ string_of_freg f1 ^ ")"
 | Pfdiv     (f0, f1, f2)        -> "Pfdiv(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
+| Pfdivs    (f0, f1, f2)        -> "Pfdivs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
 | Pfmake    (f0, i1, i2)        -> "Pfmake(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pfmr      (f0, f1)            -> "Pfmr(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
 | Pfmul     (f0, f1, f2)        -> "Pfmul(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
+| Pfmuls    (f0, f1, f2)        -> "Pfmuls(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
 | Pfneg     (f0, f1)            -> "Pfneg(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
+| Pfnegs    (f0, f1)            -> "Pfnegs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
 | Pfrsp     (f0, f1)            -> "Pfrsp(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
+| Pfxdp     (f0, f1)            -> "Pfxdp(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")"
 | Pfsub     (f0, f1, f2)        -> "Pfsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
+| Pfsubs    (f0, f1, f2)        -> "Pfsubs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")"
 | Plbz      (i0, c1, i2)        -> "Plbz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plbzx     (i0, i1, i2)        -> "Plbzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plfd      (f0, c1, i2)        -> "Plfd(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Plfd_a    (f0, c1, i2)        -> "Plfd_a(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plfdx     (f0, i1, i2)        -> "Plfdx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Plfdx_a   (f0, i1, i2)        -> "Plfdx_a(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plfs      (f0, c1, i2)        -> "Plfs(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plfsx     (f0, i1, i2)        -> "Plfsx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plha      (i0, c1, i2)        -> "Plha(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
@@ -178,8 +187,11 @@ let string_of_instruction = function
 | Plhz      (i0, c1, i2)        -> "Plhz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plhzx     (i0, i1, i2)        -> "Plhzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plfi      (f0, f1)            -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat f1 ^ ")"
+| Plfis     (f0, f1)            -> "Plfis(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat32 f1 ^ ")"
 | Plwz      (i0, c1, i2)        -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Plwz_a    (i0, c1, i2)        -> "Plwz_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Plwzx     (i0, i1, i2)        -> "Plwzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Plwzx_a   (i0, i1, i2)        -> "Plwzx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pmfcrbit  (i0, c1)            -> "Pmfcrbit(" ^ string_of_ireg i0 ^ ", " ^ string_of_crbit c1 ^ ")"
 | Pmflr     (i0)                -> "Pmflr(" ^ string_of_ireg i0 ^ ")"
 | Pmr       (i0, i1)            -> "Pmr(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")"
@@ -204,13 +216,17 @@ let string_of_instruction = function
 | Pstb      (i0, c1, i2)        -> "Pstb(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstbx     (i0, i1, i2)        -> "Pstbx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstfd     (f0, c1, i2)        -> "Pstfd(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Pstfd_a   (f0, c1, i2)        -> "Pstfd_a(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstfdx    (f0, i1, i2)        -> "Pstfdx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Pstfdx_a  (f0, i1, i2)        -> "Pstfdx_a(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstfs     (f0, c1, i2)        -> "Pstfs(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstfsx    (f0, i1, i2)        -> "Pstfsx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Psth      (i0, c1, i2)        -> "Psth(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Psthx     (i0, i1, i2)        -> "Psthx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstw      (i0, c1, i2)        -> "Pstw(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Pstw_a    (i0, c1, i2)        -> "Pstw_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Pstwx     (i0, i1, i2)        -> "Pstwx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
+| Pstwx_a   (i0, i1, i2)        -> "Pstwx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Psubfc    (i0, i1, i2)        -> "Psubfc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Psubfe    (i0, i1, i2)        -> "Psubfe(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
 | Psubfic   (i0, i1, c2)        -> "Psubfic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 6f48b23..9f842b8 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -307,6 +307,12 @@ let match_floats (a: Floats.float) (b: float): checker =
   check_eq (
     Printf.sprintf "match_floats %s %s" (string_of_int64 a) (string_of_int64 b)
   ) a b
+let match_floats32 (a: Floats.float32) (b: float): checker =
+  let a = Int64.bits_of_float (camlfloat_of_coqfloat32 a) in
+  let b = Int64.bits_of_float b in
+  check_eq (
+    Printf.sprintf "match_floats %s %s" (string_of_int64 a) (string_of_int64 b)
+  ) a b
 let match_crbits cb eb =
   let eb = crbit_arr.(eb) in
   check_eq (
@@ -1639,7 +1645,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
-      | Pfabs(rd, r1) ->
+      | Pfabs(rd, r1) | Pfabss(rd, r1) ->
           begin match ecode with
           | FABSx(frD, frB, rc) :: es ->
               OK(fw)
@@ -1660,6 +1666,17 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pfadds(rd, r1, r2) ->
+          begin match ecode with
+          | FADDSx(frD, frA, frB, rc) :: es ->
+              OK(fw)
+              >>= match_fregs rd    frD
+              >>= match_fregs r1    frA
+              >>= match_fregs r2    frB
+              >>= match_bools false rc
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pfcmpu(r1, r2) ->
           begin match ecode with
           | FCMPU(crfD, frA, frB) :: es ->
@@ -1703,6 +1720,17 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pfdivs(rd, r1, r2) ->
+          begin match ecode with
+          | FDIVSx(frD, frA, frB, rc) :: es ->
+              OK(fw)
+              >>= match_fregs rd    frD
+              >>= match_fregs r1    frA
+              >>= match_fregs r2    frB
+              >>= match_bools false rc
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pfmake(rd, r1, r2) ->
           begin match ecode with
           |   STWU  (rS0, rA0, d0)    ::
@@ -1746,7 +1774,18 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
-      | Pfneg (rd, r1) ->
+      | Pfmuls(rd, r1, r2) ->
+          begin match ecode with
+          | FMULSx(frD, frA, frC, rc) :: es ->
+              OK(fw)
+              >>= match_fregs rd    frD
+              >>= match_fregs r1    frA
+              >>= match_fregs r2    frC
+              >>= match_bools false rc
+              >>= recur_simpl
+          | _ -> error
+          end
+      | Pfneg(rd, r1) | Pfnegs(rd, r1) ->
           begin match ecode with
           | FNEGx(frD, frB, rc) :: es ->
               OK(fw)
@@ -1782,6 +1821,17 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pfxdp(rd, r1) ->
+          if rd = r1 then OK(fw) >>= compare_code cs ecode pc else 
+          begin match ecode with
+          | FMRx(frD, frB, rc) :: es ->
+              OK(fw)
+              >>= match_fregs rd    frD
+              >>= match_fregs r1    frB
+              >>= match_bools false rc
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pfsub(rd, r1, r2) ->
           begin match ecode with
           | FSUBx(frD, frA, frB, rc) :: es ->
@@ -1793,6 +1843,17 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pfsubs(rd, r1, r2) ->
+          begin match ecode with
+          | FSUBSx(frD, frA, frB, rc) :: es ->
+              OK(fw)
+              >>= match_fregs rd    frD
+              >>= match_fregs r1    frA
+              >>= match_fregs r2    frB
+              >>= match_bools false rc
+              >>= recur_simpl
+          | _ -> error
+          end
       | Plabel(lbl) ->
           OK(fw)
           >>= lblmap_unify lbl pc
@@ -1908,6 +1969,58 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
                 end
           | _ -> error
           end
+      | Plfis(r1, c) ->
+          begin match ecode with
+          |   ADDIS(rD0, rA0, simm0) ::
+              LFS  (frD1, rA1, d1)   :: es ->
+              let vaddr = Int32.(
+                add (shift_left (Safe32.of_int simm0) 16) (exts d1)
+              ) in
+              if Int32.rem vaddr 4l <> 0l
+              then ERR("Float32 constants should be 4-byte aligned")
+              else
+                let elf = fw.sf.ef.elf in
+                let atom = Hashtbl.find fw.sf.atoms fw.this_ident in
+                let literal_section =
+                  begin match atom.a_sections with
+                  | [_; l; _] -> l
+                  | _ -> Section_literal
+                  end
+                in
+                let continue = compare_code cs es (Int32.add 8l pc) in
+                begin match bitstring_at_vaddr elf vaddr 4l with
+                | None ->
+                    ERR("Floating point constant address is wrong")
+                | Some(bs, pofs, psize) ->
+                    let f =
+                      bitmatch bs with
+                      | { f : 32 : int } -> Int32.float_of_bits f
+                    in
+                    OK(fw)
+                    >>= (fun ffw ->
+                      begin match section_at_vaddr elf vaddr with
+                      | None -> ERR("No section at that virtual address")
+                      | Some(sndx) ->
+                          let section_name = elf.e_shdra.(sndx).sh_name in
+                          OK(
+                            ffw
+                            >>> (
+                              ff_sf ^%=
+                                match_sections_name literal_section section_name
+                            )
+                          )
+                      end
+                    )
+                    >>= match_iregs  GPR12 rD0
+                    >>= match_iregs  GPR0  rA0
+                    >>= match_fregs  r1    frD1
+                    >>= match_floats32 c     f
+                    >>^ (ff_ef ^%= add_range pofs psize 4 (Float32_literal(f)))
+                    >>= match_iregs  GPR12 rA1
+                    >>= continue
+                end
+          | _ -> error
+          end
       | Plfs(rd, Csymbol_sda(ident, ofs), r1) ->
           begin match ecode with
           | LFS(frD, rA, d) :: es ->
@@ -2294,30 +2407,22 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
           end
       | Pstfs(rd, cst, r1) ->
           begin match ecode with
-          |   FRSPx(frD0, frB0, rc0) ::
-              STFS (frS1, rA1,  d1)  :: es ->
+          | STFS(frS, rA, d) :: es ->
               OK(fw)
-              >>= match_fregs FPR13 frD0
-              >>= match_fregs rd    frB0
-              >>= match_bools false rc0
-              >>= match_fregs FPR13 frS1
-              >>= match_iregs r1    rA1
-              >>= match_csts  cst (exts d1)
-              >>= compare_code cs es (Int32.add 8l pc)
+              >>= match_fregs rd  frS
+              >>= match_iregs r1  rA
+              >>= match_csts  cst (exts d)
+              >>= recur_simpl
           | _ -> error
           end
       | Pstfsx(rd, r1, r2) ->
           begin match ecode with
-          |   FRSPx(frD0, frB0, rc0) ::
-              STFSX(frS1, rA1,  rB1) :: es ->
+          | STFSX(frS, rA, rB) :: es ->
               OK(fw)
-              >>= match_fregs FPR13 frD0
-              >>= match_fregs rd    frB0
-              >>= match_bools false rc0
-              >>= match_fregs FPR13 frS1
-              >>= match_iregs r1    rA1
-              >>= match_iregs r2    rB1
-              >>= compare_code cs es (Int32.add 8l pc)
+              >>= match_fregs rd frS
+              >>= match_iregs r1 rA
+              >>= match_iregs r2 rB
+              >>= recur_simpl
           | _ -> error
           end
       | Psth(rd, cst, r1) ->
@@ -2340,7 +2445,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
-      | Pstw(rd, cst, r1) ->
+      | Pstw(rd, cst, r1) | Pstw_a(rd, cst, r1) ->
           begin match ecode with
           | STW(rS, rA, d) :: es ->
               OK(fw)
@@ -2350,7 +2455,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
-      | Pstwx(rd, r1, r2) ->
+      | Pstwx(rd, r1, r2) | Pstwx_a(rd, r1, r2) ->
           begin match ecode with
           | STWX(rS, rA, rB) :: es ->
               OK(fw)
@@ -2541,16 +2646,12 @@ and check_builtin_vstore_common ccode ecode pc chunk addr offset src fw =
       end
   | Mfloat32, FR src ->
       begin match ecode with
-      |   FRSPx(frD0, frB0, rc0) ::
-          STFS (frS1, rA1,  d1)  :: es ->
+      | STFS(frS, rA, d) :: es ->
           OK(fw)
-          >>= match_fregs  FPR13  frD0
-          >>= match_fregs  src    frB0
-          >>= match_bools  false  rc0
-          >>= match_fregs  FPR13  frS1
-          >>= match_iregs  addr   rA1
-          >>= match_csts   offset (exts d1)
-          >>= compare_code ccode es (Int32.add pc 8l)
+          >>= match_fregs  src    frS
+          >>= match_iregs  addr   rA
+          >>= match_csts   offset (exts d)
+          >>= recur_simpl
       | _ -> error
       end
   | Mfloat64, FR src ->
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index ec11412..0f7ec44 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -25,6 +25,7 @@ type byte_chunk_desc =
   | Stub               of string
   | Jumptable
   | Float_literal      of float
+  | Float32_literal    of float
   | Padding
   | Unknown            of string
 
@@ -208,5 +209,6 @@ let string_of_byte_chunk_desc = function
 | Stub(s) -> "Stub for: " ^ s
 | Jumptable -> "Jump table"
 | Float_literal(f) -> "Float literal: " ^ string_of_float f
+| Float32_literal(f) -> "Float32 literal: " ^ string_of_float f
 | Padding -> "Padding"
 | Unknown(s) -> "???" ^ (if !verbose_elfmap then s else "")
diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml
index fb7bee7..d7947ee 100644
--- a/checklink/Fuzz.ml
+++ b/checklink/Fuzz.ml
@@ -113,13 +113,14 @@ let ok_fuzz elfmap str byte fuzz =
   | Zero_symbol        -> false
   | Stub(_)            -> true
   | Jumptable          -> true
-  | Float_literal(_)   ->
+  | Float_literal(_)   -> (* FIXME: this shouldn't be a false positive! *)
       (* False positive: 0. becomes -0. *)
       not (
         (byte = a)
         && (fuz = 0x80) (* sign bit *)
         && String.sub str byte 8 = "\000\000\000\000\000\000\000\000"
       )
+  | Float32_literal(_)  -> true
   (* padding is allowed to be non-null, but won't be recognized as padding, but
      as unknown, which is not an ERROR *)
   | Padding            -> false
diff --git a/checklink/Library.ml b/checklink/Library.ml
index 69a0d6e..54bca41 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -115,6 +115,7 @@ let z_int64 = Camlcoq.Z.to_int64
 (* Some more printers *)
 
 let string_of_ffloat f = string_of_float (camlfloat_of_coqfloat f)
+let string_of_ffloat32 f = string_of_float (camlfloat_of_coqfloat32 f)
 
 let string_of_array string_of_elt sep a =
   let b = Buffer.create 1024 in