From 04ff02a9f4bc4f766a450e5463729102ee26882e Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 24 Jul 2014 08:05:35 +0000 Subject: 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 --- checklink/Asm_printers.ml | 16 +++++ checklink/Check.ml | 163 +++++++++++++++++++++++++++++++++++++--------- checklink/Frameworks.ml | 2 + checklink/Fuzz.ml | 3 +- checklink/Library.ml | 1 + 5 files changed, 153 insertions(+), 32 deletions(-) (limited to 'checklink') 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 -- cgit v1.2.3