summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-24 08:05:35 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-24 08:05:35 +0000
commit04ff02a9f4bc4f766a450e5463729102ee26882e (patch)
tree8aa397a531c75a3f634f068ff08293718c7f9fe6
parenta19eb81876d9739b569b946ccdbf2778d2e9aca7 (diff)
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
-rw-r--r--checklink/Asm_printers.ml16
-rw-r--r--checklink/Check.ml163
-rw-r--r--checklink/Frameworks.ml2
-rw-r--r--checklink/Fuzz.ml3
-rw-r--r--checklink/Library.ml1
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