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/Check.ml | 163 +++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 132 insertions(+), 31 deletions(-) (limited to 'checklink/Check.ml') 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 -> -- cgit v1.2.3