diff options
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Asm_printers.ml | 47 | ||||
| -rw-r--r-- | checklink/Check.ml | 1164 | ||||
| -rw-r--r-- | checklink/Frameworks.ml | 8 | ||||
| -rw-r--r-- | checklink/Fuzz.ml | 19 |
4 files changed, 385 insertions, 853 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 9bb2009..1f737c2 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -88,6 +88,7 @@ let string_of_preg = function | CR0_1 -> "CR0_1" | CR0_2 -> "CR0_2" | CR0_3 -> "CR0_3" +| CR1_2 -> "CR1_2" let string_of_external_function e = match e with @@ -117,8 +118,19 @@ let string_of_crbit = function | CRbit_1 -> "CRbit_1" | CRbit_2 -> "CRbit_2" | CRbit_3 -> "CRbit_3" +| CRbit_6 -> "CRbit_6" -let string_of_memory_chunk mc = "MEMORY_CHUNK" +let string_of_memory_chunk = function + | Mint8signed -> "int8s" + | Mint8unsigned -> "int8u" + | Mint16signed -> "int16s" + | Mint16unsigned -> "int16u" + | Mint32 -> "int32" + | Mint64 -> "int64" + | Mfloat32 -> "float32" + | Mfloat64 -> "float64" + | Many32 -> "any32" + | Many64 -> "any64" let string_of_annot_param = function | APreg (p0)-> "APreg(" ^ string_of_preg p0 ^ ")" @@ -126,6 +138,7 @@ let string_of_annot_param = function let string_of_instruction = function | Padd (i0, i1, i2) -> "Padd(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Paddc (i0, i1, i2) -> "Paddc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Padde (i0, i1, i2) -> "Padde(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Paddi (i0, i1, c2) -> "Paddi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Paddic (i0, i1, c2) -> "Paddic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" @@ -139,6 +152,7 @@ let string_of_instruction = function | Pb (l0) -> "Pb(" ^ string_of_label l0 ^ ")" | Pbctr sg -> "Pbctr" | Pbctrl sg -> "Pbctrl" +| Pbdnz (l1) -> "Pbdnz(" ^ string_of_label l1 ^ ")" | Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" | Pbl (i0, sg) -> "Pbl(" ^ string_of_ident i0 ^ ")" | Pbs (i0, sg) -> "Pbs(" ^ string_of_ident i0 ^ ")" @@ -149,9 +163,13 @@ let string_of_instruction = function | Pcmplwi (i0, c1) -> "Pcmplwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" | Pcmpw (i0, i1) -> "Pcmpw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" | Pcmpwi (i0, c1) -> "Pcmpwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" +| Pcntlz (i0, i1) -> "Pcntlz(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pcreqv (c0, c1, c2) -> "Pcreqv(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" | Pcror (c0, c1, c2) -> "Pcror(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" +| Pcrxor (c0, c1, c2) -> "Pcrxor(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" | Pdivw (i0, i1, i2) -> "Pdivw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pdivwu (i0, i1, i2) -> "Pdivwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Peieio -> "Peieio" | Peqv (i0, i1, i2) -> "Peqv(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pextsb (i0, i1) -> "Pextsb(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" | Pextsh (i0, i1) -> "Pextsh(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" @@ -162,6 +180,8 @@ let string_of_instruction = function | 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 ^ ")" +| Pfctiw (f0, f1) -> "Pfctiw(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfctiwz (f0, f1) -> "Pfctiwz(" ^ string_of_freg f0 ^ ", " ^ 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 ^ ")" @@ -174,6 +194,15 @@ let string_of_instruction = function | 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 ^ ")" +| Pfmadd (f0, f1, f2, f3) -> "Pfmadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" +| Pfmsub (f0, f1, f2, f3) -> "Pfmsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" +| Pfnmadd (f0, f1, f2, f3) -> "Pfnmadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" +| Pfnmsub (f0, f1, f2, f3) -> "Pfnmsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" +| Pfsqrt (f0, f1) -> "Pfsqrt(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfrsqrte (f0, f1) -> "Pfrsqrte(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfres (f0, f1) -> "Pfres(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" +| Pfsel (f0, f1, f2, f3) -> "Pfsel(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" +| Pisync -> "Pisync" | 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 ^ ")" @@ -184,14 +213,18 @@ let string_of_instruction = function | 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 ^ ")" | Plhax (i0, i1, i2) -> "Plhax(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plhbrx (i0, i1, i2) -> "Plhbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | 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 ^ ")" +| Plwbrx (i0, i1, i2) -> "Plwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Plwz (i0, c1, i2) -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Plwzu (i0, c1, i2) -> "Plwzu(" ^ 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 ^ ")" +| Pmfcr (i0) -> "Pmfcr(" ^ string_of_ireg i0 ^ ")" | 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 ^ ")" @@ -217,32 +250,42 @@ let string_of_instruction = function | 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 ^ ")" +| Pstfdu (f0, c1, i2) -> "Pstfdu(" ^ 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 ^ ")" +| Psthbrx (i0, i1, i2) -> "Psthbrx(" ^ 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 ^ ")" +| Pstwu (i0, c1, i2) -> "Pstwu(" ^ 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 ^ ")" +| Pstwxu (i0, i1, i2) -> "Pstwxu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" +| Pstwbrx (i0, i1, i2) -> "Pstwbrx(" ^ 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 ^ ")" +| Psubfze (i0, i1) -> "Psubfze(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" | Psubfic (i0, i1, c2) -> "Psubfic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" +| Psync -> "Psync" +| Ptrap -> "Ptrap" | Pxor (i0, i1, i2) -> "Pxor(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pxori (i0, i1, c2) -> "Pxori(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Pxoris (i0, i1, c2) -> "Pxoris(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" | Plabel (l0) -> "Plabel(" ^ string_of_label l0 ^ ")" | Pbuiltin (e0, p1, p2) -> "Pbuiltin(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_preg ", " p1 ^ ", " ^ string_of_list string_of_preg ", " p2 ^ ")" | Pannot (e0, a1) -> "Pannot(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_annot_param ", " a1 ^ ")" +| Pcfi_adjust n -> "Pcfi_adjust(" ^ string_of_coq_Z n ^ ")" +| Pcfi_rel_offset n -> "Pcfi_rel_offset(" ^ string_of_coq_Z n ^ ")" let string_of_init_data = function | Init_int8(i) -> "Init_int8(" ^ string_of_int (z_int_lax i) ^ ")" | Init_int16(i) -> "Init_int16(" ^ string_of_int (z_int_lax i) ^ ")" | Init_int32(i) -> "Init_int32(" ^ string_of_int32i (z_int32 i) ^ ")" | Init_int64(i) -> "Init_int64(" ^ string_of_int64i (z_int64 i) ^ ")" -| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat f ^ ")" +| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat32 f ^ ")" | Init_float64(f) -> "Init_float64(" ^ string_of_ffloat f ^ ")" | Init_space(z) -> "Init_space(" ^ string_of_int (z_int z) ^ ")" | Init_addrof(ident, ofs) -> diff --git a/checklink/Check.ml b/checklink/Check.ml index 9f842b8..7eb3ea3 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -68,8 +68,8 @@ let check_st_bind atom (sym: elf32_sym): s_framework -> s_framework = (** Adapted from CompCert *) let name_of_section_Linux: section_name -> string = function | Section_text -> ".text" -| Section_data i -> if i then ".data" else ".bss" -| Section_small_data i -> if i then ".sdata" else ".sbss" +| Section_data i -> if i then ".data" else "COMM" +| Section_small_data i -> if i then ".sdata" else "COMM" | Section_const -> ".rodata" | Section_small_const -> ".sdata2" | Section_string -> ".rodata" @@ -277,10 +277,12 @@ let freg_arr: freg array = FPR23; FPR24; FPR25; FPR26; FPR27; FPR28; FPR29; FPR30; FPR31 |] -let crbit_arr: crbit array = - [| - CRbit_0; CRbit_1; CRbit_2; CRbit_3 - |] +let num_crbit = function + | CRbit_0 -> 0 + | CRbit_1 -> 1 + | CRbit_2 -> 2 + | CRbit_3 -> 3 + | CRbit_6 -> 6 type checker = f_framework -> f_framework or_err let check (cond: bool) (msg: string): checker = @@ -301,22 +303,20 @@ let match_int32s a b: checker = ) a b (** We compare floats by their bit representation, so that 0.0 and -0.0 are different. *) -let match_floats (a: Floats.float) (b: float): checker = - let a = Int64.bits_of_float (camlfloat_of_coqfloat a) in - let b = Int64.bits_of_float b in +let match_floats (a: Floats.float) (b: int64): checker = + let a = camlint64_of_coqint (Floats.Float.to_bits a) in 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 +let match_floats32 (a: Floats.float32) (b: int32): checker = + let a = camlint_of_coqint (Floats.Float32.to_bits a) in check_eq ( - Printf.sprintf "match_floats %s %s" (string_of_int64 a) (string_of_int64 b) + Printf.sprintf "match_floats %s %s" (string_of_int32 a) (string_of_int32 b) ) a b let match_crbits cb eb = - let eb = crbit_arr.(eb) in + let cb = num_crbit cb in check_eq ( - Printf.sprintf "match_crbits %s %s" (string_of_crbit cb) (string_of_crbit eb) + Printf.sprintf "match_crbits %d %d" cb eb ) cb eb let match_iregs cr er = let er = ireg_arr.(er) in @@ -575,195 +575,6 @@ let rec match_jmptbl lbllist vaddr size ffw = end end -(** Matches [ecode] against the expected CR6 magic before a function call. -*) -let match_set_cr6 sg ecode = - if sg.sig_cc.cc_vararg then - if List.mem Tfloat sg.sig_args then - match ecode with - | CREQV(6, 6, 6) :: ecode' -> Some ecode' - | _ -> None - else - match ecode with - | CRXOR(6, 6, 6) :: ecode' -> Some ecode' - | _ -> None - else Some ecode - -(** Matches [ecode] agains the expected code for a small memory copy - pseudo-instruction. Returns a triple containing the updated framework, - the remaining ELF code, and the updated program counter. -*) -let match_memcpy_small ecode pc sz al src dst (fw: f_framework) - : (f_framework * ecode * int32) or_err = - let error = ERR("match_memcpy_small") in - let rec match_memcpy_small_aux ofs sz ecode pc (fw: f_framework) = - let ofs32 = Safe32.of_int ofs in - if sz >= 8 && al >= 4 - then ( - match ecode with - | LFD (frD0, rA0, d0) :: - STFD(frS1, rA1, d1) :: es -> - OK(fw) - >>= match_fregs FPR13 frD0 - >>= match_iregs src rA0 - >>= match_int32s ofs32 (exts d0) - >>= match_fregs FPR13 frS1 - >>= match_iregs dst rA1 - >>= match_int32s ofs32 (exts d1) - >>= match_memcpy_small_aux (ofs + 8) (sz - 8) es (Int32.add 8l pc) - | _ -> error - ) - else if sz >= 4 - then ( - match ecode with - | LWZ(rD0, rA0, d0) :: - STW(rS1, rA1, d1) :: es -> - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs src rA0 - >>= match_int32s ofs32 (exts d0) - >>= match_iregs GPR0 rS1 - >>= match_iregs dst rA1 - >>= match_int32s ofs32 (exts d0) - >>= match_memcpy_small_aux (ofs + 4) (sz - 4) es (Int32.add 8l pc) - | _ -> error - ) - else if sz >= 2 - then ( - match ecode with - | LHZ(rD0, rA0, d0) :: - STH(rS1, rA1, d1) :: es -> - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs src rA0 - >>= match_int32s ofs32 (exts d0) - >>= match_iregs GPR0 rS1 - >>= match_iregs dst rA1 - >>= match_int32s ofs32 (exts d0) - >>= match_memcpy_small_aux (ofs + 2) (sz - 2) es (Int32.add 8l pc) - | _ -> error - ) - else if sz >= 1 - then ( - match ecode with - | LBZ(rD0, rA0, d0) :: - STB(rS1, rA1, d1) :: es -> - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs src rA0 - >>= match_int32s ofs32 (exts d0) - >>= match_iregs GPR0 rS1 - >>= match_iregs dst rA1 - >>= match_int32s ofs32 (exts d0) - >>= match_memcpy_small_aux (ofs + 1) (sz - 1) es (Int32.add 8l pc) - | _ -> error - ) - else OK(fw, ecode, pc) - in match_memcpy_small_aux 0 sz ecode pc fw - -(** Matches [ecode] agains the expected code for a big memory copy - pseudo-instruction. Returns a triple containing the updated framework, - the remaining ELF code, and the updated program counter. -*) -let match_memcpy_big ecode pc sz al src dst fw - : (f_framework * ecode * int32) or_err = - let error = ERR("match_memcpy_big") in - match ecode with - | ADDI (rD0, rA0, simm0) :: (* pc *) - MTSPR(rS1, spr1) :: - ADDI (rD2, rA2, simm2) :: - ADDI (rD3, rA3, simm3) :: - LWZU (rD4, rA4, d4) :: (* pc + 16 <- *) - STWU (rS5, rA5, d5) :: (* | *) - BCx (bo6, bi6, bd6, aa6, lk6) :: (* pc + 24 -- *) - es -> - let sz' = Safe32.of_int (sz / 4) in - let (s, d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in - let target_vaddr = Int32.(add 16l pc) in - let dest_vaddr = Int32.(add (add 24l pc) (mul 4l (exts bd6))) in - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs GPR0 rA0 - >>= match_int32s sz' (exts simm0) - >>= match_iregs GPR0 rS1 - >>= match_ctr spr1 - >>= match_iregs s rD2 - >>= match_iregs src rA2 - >>= match_int32s (-4l) (exts simm2) - >>= match_iregs d rD3 - >>= match_iregs dst rA3 - >>= match_int32s (-4l) (exts simm3) - >>= match_iregs GPR0 rD4 - >>= match_iregs s rA4 - >>= match_int32s 4l (exts d4) - >>= match_iregs GPR0 rS5 - >>= match_iregs d rA5 - >>= match_int32s 4l (exts d5) - >>= (fun ffw -> - bitmatch bo6 with - | { 16:5:int } -> OK(ffw) - | { _ } -> ERR("bitmatch bo") - ) - >>= match_ints bi6 0 - >>= match_int32s dest_vaddr target_vaddr - >>= match_bools false aa6 - >>= match_bools false lk6 - >>= (fun fw -> - match sz land 3 with - | 1 -> - begin match es with - | LBZ(rD0, rA0, d0) :: - STB(rS1, rA1, d1) :: es -> - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs s rA0 - >>= match_int32s 4l (exts d0) - >>= match_iregs GPR0 rS1 - >>= match_iregs d rA1 - >>= match_int32s 4l (exts d1) - >>= (fun fw -> OK(fw, es, Int32.add 36l pc)) - | _ -> error - end - | 2 -> - begin match es with - | LHZ(rD0, rA0, d0) :: - STH(rS1, rA1, d1) :: es -> - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs s rA0 - >>= match_int32s 4l (exts d0) - >>= match_iregs GPR0 rS1 - >>= match_iregs d rA1 - >>= match_int32s 4l (exts d1) - >>= (fun fw -> OK(fw, es , Int32.add 36l pc)) - | _ -> error - end - | 3 -> - begin match es with - | LHZ(rD0, rA0, d0) :: - STH(rS1, rA1, d1) :: - LBZ(rD2, rA2, d2) :: - STB(rS3, rA3, d3) :: es -> - OK(fw) - >>= match_iregs GPR0 rD0 - >>= match_iregs s rA0 - >>= match_int32s 4l (exts d0) - >>= match_iregs GPR0 rS1 - >>= match_iregs d rA1 - >>= match_int32s 4l (exts d1) - >>= match_iregs GPR0 rD2 - >>= match_iregs s rA2 - >>= match_int32s 6l (exts d2) - >>= match_iregs GPR0 rS3 - >>= match_iregs d rA3 - >>= match_int32s 6l (exts d3) - >>= (fun fw -> OK(fw, es, Int32.add 44l pc)) - | _ -> error - end - | _ -> OK(fw, es, Int32.add 28l pc) - ) - | _ -> error - let match_bo_bt_bool bo = bitmatch bo with | { false:1; true:1; true:1; false:1; false:1 } -> true @@ -774,6 +585,11 @@ let match_bo_bf_bool bo = | { false:1; false:1; true:1; false:1; false:1 } -> true | { _ } -> false +let match_bo_bdnz_bool bo = + bitmatch bo with + | { true:1; false:1; false:1; false:1; false:1 } -> true + | { _ } -> false + let match_bo_bt bo: checker = fun ffw -> bitmatch bo with | { false:1; true:1; true:1; false:1; false:1 } -> OK(ffw) @@ -869,6 +685,18 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Paddc(rd, r1, r2) -> + begin match ecode with + | ADDCx(rD, rA, rB, oe, rc) :: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= match_bools false oe + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end | Padde(rd, r1, r2) -> begin match ecode with | ADDEx(rD, rA, rB, oe, rc) :: es -> @@ -931,34 +759,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pallocframe(sz, ofs) -> - begin match ecode with - | STWU(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs GPR1 rS - >>= match_iregs GPR1 rA - >>= match_z_int32 sz (Int32.neg (exts d)) - >>= match_z_int32 ofs 0l - >>= recur_simpl - | ADDIS (rD0, rA0, simm0) :: - ORI (rS1, rA1, uimm1) :: - STWUX (rS2, rA2, rB2) :: es -> - let sz32 = Int32.neg (z_int32 sz) in - let sz_hi = Int32.shift_right_logical sz32 16 in - let sz_lo = Int32.logand sz32 0xFFFFl in - OK(fw) - >>= match_iregs GPR12 rD0 - >>= match_iregs GPR0 rA0 - >>= match_int32s sz_hi (Safe32.of_int simm0) - >>= match_iregs GPR12 rS1 - >>= match_iregs GPR12 rA1 - >>= match_int32s sz_lo (Safe32.of_int uimm1) - >>= match_iregs GPR1 rS2 - >>= match_iregs GPR1 rA2 - >>= match_iregs GPR12 rB2 - >>= compare_code cs es (Int32.add 12l pc) - | _ -> error - end + | Pallocframe(sz, ofs) -> error | Pandc(rd, r1, r2) -> begin match ecode with | ANDCx(rS, rA, rB, rc) :: es -> @@ -1016,8 +817,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbctr sg -> - begin match match_set_cr6 sg ecode with - | Some(BCCTRx(bo, bi, lk) :: es) -> + begin match ecode with + | BCCTRx(bo, bi, lk) :: es -> OK(fw) >>= match_bo_ctr bo >>= match_ints 0 bi @@ -1026,8 +827,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbctrl sg -> - begin match match_set_cr6 sg ecode with - | Some(BCCTRx(bo, bi, lk) :: es) -> + begin match ecode with + | BCCTRx(bo, bi, lk) :: es -> OK(fw) >>= match_bo_ctr bo >>= match_ints 0 bi @@ -1035,6 +836,18 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pbdnz(lbl) -> + begin match ecode with + | BCx (bo, bi, bd, aa, lk) :: es when match_bo_bdnz_bool bo -> + let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in + OK(fw) + >>= match_ints 0 bi + >>= lblmap_unify lbl lblvaddr + >>= match_bools false aa + >>= match_bools false lk + >>= recur_simpl + | _ -> error + end | Pbf(bit, lbl) -> begin match ecode with | BCx(bo, bi, bd, aa, lk) :: es when match_bo_bf_bool bo -> @@ -1064,8 +877,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbl(ident, sg) -> - begin match match_set_cr6 sg ecode with - | Some(Bx(li, aa, lk) :: es) -> + begin match ecode with + | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in OK(fw) >>= (ff_sf ^%=? idmap_unify ident dest) @@ -1085,8 +898,8 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pbs(ident, sg) -> - begin match match_set_cr6 sg ecode with - | Some(Bx(li, aa, lk) :: es) -> + begin match ecode with + | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in OK(fw) >>= match_bools false aa @@ -1156,386 +969,12 @@ let rec compare_code ccode ecode pc: checker = fun fw -> end | Pbuiltin(ef, args, res) -> begin match ef with - | EF_builtin(name, sg) -> - begin match Hashtbl.find - (fw |. ff_sf).ident_to_name name, args, res with - | "__builtin_mulhw", [IR a1; IR a2], [IR res] -> - begin match ecode with - | MULHWx(rD, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs a1 rA - >>= match_iregs a2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_mulhwu", [IR a1; IR a2], [IR res] -> - begin match ecode with - | MULHWUx(rD, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs a1 rA - >>= match_iregs a2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_cntlz", [IR a1], [IR res] -> - begin match ecode with - | CNTLZWx(rS, rA, rc) :: es -> - OK(fw) - >>= match_iregs a1 rS - >>= match_iregs res rA - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | ("__builtin_bswap"|"__builtin_bswap32"), [IR a1], [IR res] -> - begin match ecode with - | STWU (rS0, rA0, d0) :: - LWBRX(rD1, rA1, rB1) :: - ADDI (rD2, rA2, simm2) :: es -> - OK(fw) - >>= match_iregs a1 rS0 - >>= match_iregs GPR1 rA0 - >>= match_int32s (-8l) (exts d0) - >>= match_iregs res rD1 - >>= match_iregs GPR0 rA1 - >>= match_iregs GPR1 rB1 - >>= match_iregs GPR1 rD2 - >>= match_iregs GPR1 rA2 - >>= match_int32s 8l (exts simm2) - >>= compare_code cs es (Int32.add 12l pc) - | _ -> error - end - | "__builtin_bswap16", [IR a1], [IR res] -> - begin match ecode with - | RLWINMx(rS1, rA1, sh1, mb1, me1, rc1) :: - RLWINMx(rS2, rA2, sh2, mb2, me2, rc2) :: - ORx(rS3, rA3, rB3, rc3) :: es -> - OK(fw) - >>= match_iregs GPR0 rS1 - >>= match_iregs a1 rA1 - >>= check_eq "bswap16-1" sh1 8 - >>= check_eq "bswap16-2" mb1 16 - >>= check_eq "bswap16-3" me1 23 - >>= match_iregs res rS2 - >>= match_iregs a1 rA2 - >>= check_eq "bswap16-4" sh2 24 - >>= check_eq "bswap16-5" mb2 24 - >>= check_eq "bswap16-6" me2 31 - >>= match_iregs res rS3 - >>= match_iregs GPR0 rA3 - >>= match_iregs res rB3 - >>= compare_code cs es (Int32.add 12l pc) - | _ -> error - end - | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] -> - begin match ecode with - | FMADDx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frA - >>= match_fregs a3 frB - >>= match_fregs a2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] -> - begin match ecode with - | FMSUBx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frA - >>= match_fregs a3 frB - >>= match_fregs a2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] -> - begin match ecode with - | FNMADDx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frA - >>= match_fregs a3 frB - >>= match_fregs a2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] -> - begin match ecode with - | FNMSUBx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frA - >>= match_fregs a3 frB - >>= match_fregs a2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fabs", [FR a1], [FR res] -> - begin match ecode with - | FABSx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fsqrt", [FR a1], [FR res] -> - begin match ecode with - | FSQRTx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_frsqrte", [FR a1], [FR res] -> - begin match ecode with - | FRSQRTEx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fres", [FR a1], [FR res] -> - begin match ecode with - | FRESx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fsel", [FR a1; FR a2; FR a3], [FR res] -> - begin match ecode with - | FSELx(frD, frA, frB, frC, rc) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_fregs a1 frA - >>= match_fregs a3 frB - >>= match_fregs a2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | "__builtin_fcti", [FR r1], [IR rd] -> - begin match ecode with - | FCTIWx(frD0, frB0, rc0) :: - STFDU (frS1, rA1, d1) :: - LWZ (rD2, rA2, d2) :: - ADDI (rD3, rA3, simm3) :: es -> - OK(fw) - >>= match_fregs FPR13 frD0 - >>= match_fregs r1 frB0 - >>= match_bools false rc0 - >>= match_fregs FPR13 frS1 - >>= match_iregs GPR1 rA1 - >>= match_int32s (-8l) (exts d1) - >>= match_iregs rd rD2 - >>= match_iregs GPR1 rA2 - >>= match_int32s 4l (exts d2) - >>= match_iregs GPR1 rD3 - >>= match_iregs GPR1 rA3 - >>= match_int32s 8l (exts simm3) - >>= compare_code cs es (Int32.add 16l pc) - | _ -> error - end - | "__builtin_read16_reversed", [IR a1], [IR res] -> - begin match ecode with - | LHBRX(rD, rA, rB):: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs GPR0 rA - >>= match_iregs a1 rB - >>= recur_simpl - | _ -> error - end - | "__builtin_read32_reversed", [IR a1], [IR res] -> - begin match ecode with - | LWBRX(rD, rA, rB) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs GPR0 rA - >>= match_iregs a1 rB - >>= recur_simpl - | _ -> error - end - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - begin match ecode with - | STHBRX(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs a2 rS - >>= match_iregs GPR0 rA - >>= match_iregs a1 rB - >>= recur_simpl - | _ -> error - end - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - begin match ecode with - | STWBRX(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs a2 rS - >>= match_iregs GPR0 rA - >>= match_iregs a1 rB - >>= recur_simpl - | _ -> error - end - | "__builtin_eieio", [], _ -> - begin match ecode with - | EIEIO :: es -> - OK(fw) - >>= recur_simpl - | _ -> error - end - | "__builtin_sync", [], _ -> - begin match ecode with - | SYNC :: es -> - OK(fw) - >>= recur_simpl - | _ -> error - end - | "__builtin_isync", [], _ -> - begin match ecode with - | ISYNC :: es -> - OK(fw) - >>= recur_simpl - | _ -> error - end - | "__builtin_trap", [], _ -> - begin match ecode with - | TW(tO, rA, rB) :: es -> - OK(fw) - >>= (fun ffw -> - bitmatch tO with - | { 31 : 5 : int } -> OK(ffw) - | { _ } -> ERR("bitmatch") - ) - >>= match_iregs GPR0 rA - >>= match_iregs GPR0 rB - >>= recur_simpl - | _ -> error - end - | _ -> error - end - | EF_vload(chunk) -> - begin match args with - | [IR addr] -> - OK(fw) - >>= check_builtin_vload_common - cs ecode pc chunk addr (Cint Integers.Int.zero) res - | _ -> fatal "Unexpected args in EF_vload, please report." - end - | EF_vstore(chunk) -> - begin match args with - | [IR addr; src] -> - OK(fw) - >>= check_builtin_vstore_common - cs ecode pc chunk addr (Cint Integers.Int.zero) src - | _ -> fatal "Unexpected args in EF_vstore, please report." - end - | EF_vload_global(chunk, ident, ofs) -> - begin match ecode with - | ADDIS(rD, rA, simm) :: es -> - let high = Csymbol_high(ident, ofs) in - OK(fw) - >>= match_iregs GPR11 rD - >>= match_iregs GPR0 rA - >>= match_csts high (Safe32.of_int simm) - >>= check_builtin_vload_common - cs es (Int32.add pc 4l) chunk GPR11 - (Csymbol_low(ident, ofs)) res - | _ -> error - end - | EF_vstore_global(chunk, ident, ofs) -> - begin match args with - | [src] -> - begin match ecode with - | ADDIS(rD, rA, simm) :: es -> - let tmp = - if src = IR GPR11 - then GPR12 - else GPR11 - in - let high = Csymbol_high(ident, ofs) in - OK(fw) - >>= match_iregs tmp rD - >>= match_iregs GPR0 rA - >>= match_csts high (Safe32.of_int simm) - >>= check_builtin_vstore_common - cs es (Int32.add pc 4l) chunk tmp - (Csymbol_low(ident, ofs)) src - | _ -> error - end - | _ -> fatal "Unexpected args in EF_vstore_global, please report." - end - | EF_memcpy(sz, al) -> - let sz = z_int sz in - let al = z_int al in - begin match args with - | [IR dst; IR src] -> - if sz <= 48 - then ( - match match_memcpy_small ecode pc sz al src dst fw with - | ERR(s) -> ERR(s) - | OK(fw, es, pc) -> compare_code cs es pc fw - ) - else ( - match match_memcpy_big ecode pc sz al src dst fw with - | ERR(s) -> ERR(s) - | OK(fw, es, pc) -> compare_code cs es pc fw - ) - | _ -> error - end - | EF_annot_val(text, targ) -> - begin match args, res with - | IR src :: _, [IR dst] -> - if dst <> src - then ( - match ecode with - | ORx(rS, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs src rS - >>= match_iregs dst rA - >>= match_iregs src rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - ) - else compare_code cs ecode pc fw - | FR src :: _, [FR dst] -> - if dst <> src - then ( - match ecode with - | FMRx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs dst frD - >>= match_fregs src frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - ) - else compare_code cs ecode pc fw - | _ -> error - end - | EF_annot(_, _) -> fatal "Unexpected EF_annot, please report." - | EF_external(_, _) -> fatal "Unexpected EF_external, please report." - | EF_free -> fatal "Unexpected EF_free, please report." - | EF_malloc -> fatal "Unexpected EF_malloc, please report." | EF_inline_asm(_) -> fatal "Unsupported: inline asm statement." + | _ -> fatal "Unexpected Pbuiltin, please report." end + | Pcfi_adjust _ | Pcfi_rel_offset _ -> + OK(fw) + >>= compare_code cs ecode pc | Pcmplw(r1, r2) -> begin match ecode with | CMPL(crfD, l, rA, rB) :: es -> @@ -1580,6 +1019,26 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pcntlz(r1, r2) -> + begin match ecode with + | CNTLZWx(rS, rA, rc) :: es -> + OK(fw) + >>= match_iregs r2 rS + >>= match_iregs r1 rA + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pcreqv(bd, b1, b2) -> + begin match ecode with + | CREQV(crbD, crbA, crbB) :: es -> + OK(fw) + >>= match_crbits bd crbD + >>= match_crbits b1 crbA + >>= match_crbits b2 crbB + >>= recur_simpl + | _ -> error + end | Pcror(bd, b1, b2) -> begin match ecode with | CROR(crbD, crbA, crbB) :: es -> @@ -1590,6 +1049,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pcrxor(bd, b1, b2) -> + begin match ecode with + | CRXOR(crbD, crbA, crbB) :: es -> + OK(fw) + >>= match_crbits bd crbD + >>= match_crbits b1 crbA + >>= match_crbits b2 crbB + >>= recur_simpl + | _ -> error + end | Pdivw(rd, r1, r2) -> begin match ecode with | DIVWx(rD, rA, rB, oe, rc) :: es -> @@ -1614,6 +1083,13 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Peieio -> + begin match ecode with + | EIEIO :: es -> + OK(fw) + >>= recur_simpl + | _ -> error + end | Peqv(rd, r1, r2) -> begin match ecode with | EQVx(rS, rA, rB, rc) :: es -> @@ -1688,25 +1164,25 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pfcti(rd, r1) -> + error + | Pfctiw(rd, r1) -> begin match ecode with - | FCTIWZx(frD0, frB0, rc0) :: - STFDU (frS1, rA1, d1) :: - LWZ (rD2, rA2, d2) :: - ADDI (rD3, rA3, simm3) :: es -> + | FCTIWx(frD0, frB0, rc0) :: es -> OK(fw) - >>= match_fregs FPR13 frD0 + >>= match_fregs rd frD0 >>= match_fregs r1 frB0 >>= match_bools false rc0 - >>= match_fregs FPR13 frS1 - >>= match_iregs GPR1 rA1 - >>= match_int32s (-8l) (exts d1) - >>= match_iregs rd rD2 - >>= match_iregs GPR1 rA2 - >>= match_int32s 4l (exts d2) - >>= match_iregs GPR1 rD3 - >>= match_iregs GPR1 rA3 - >>= match_int32s 8l (exts simm3) - >>= compare_code cs es (Int32.add 16l pc) + >>= recur_simpl + | _ -> error + end + | Pfctiwz(rd, r1) -> + begin match ecode with + | FCTIWZx(frD0, frB0, rc0) :: es -> + OK(fw) + >>= match_fregs rd frD0 + >>= match_fregs r1 frB0 + >>= match_bools false rc0 + >>= recur_simpl | _ -> error end | Pfdiv(rd, r1, r2) -> @@ -1732,27 +1208,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pfmake(rd, r1, r2) -> - begin match ecode with - | STWU (rS0, rA0, d0) :: - STW (rS1, rA1, d1) :: - LFD (frD2, rA2, d2) :: - ADDI (rD3, rA3, simm3) :: es -> - OK(fw) - >>= match_iregs r1 rS0 - >>= match_iregs GPR1 rA0 - >>= match_int32s (-8l) (exts d0) - >>= match_iregs r2 rS1 - >>= match_iregs GPR1 rA1 - >>= match_int32s 4l (exts d1) - >>= match_fregs rd frD2 - >>= match_iregs GPR1 rA2 - >>= match_int32s 0l (exts d2) - >>= match_iregs GPR1 rD3 - >>= match_iregs GPR1 rA3 - >>= match_int32s 8l (exts simm3) - >>= compare_code cs es (Int32.add 16l pc) - | _ -> error - end + error | Pfmr(rd, r1) -> begin match ecode with | FMRx(frD, frB, rc) :: es -> @@ -1796,21 +1252,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> error end | Pfreeframe(sz, ofs) -> - begin match ecode with - | ADDI(rD, rA, simm) :: es -> - OK(fw) - >>= match_iregs GPR1 rD - >>= match_iregs GPR1 rA - >>= match_z_int32 sz (exts simm) - >>= recur_simpl - | LWZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs GPR1 rD - >>= match_iregs GPR1 rA - >>= match_z_int32 ofs (exts d) - >>= recur_simpl - | _ -> error - end + error | Pfrsp(rd, r1) -> begin match ecode with | FRSPx(frD, frB, rc) :: es -> @@ -1822,16 +1264,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | _ -> 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 + error | Pfsub(rd, r1, r2) -> begin match ecode with | FSUBx(frD, frA, frB, rc) :: es -> @@ -1854,6 +1287,103 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pfmadd(rd, r1, r2, r3) -> + begin match ecode with + | FMADDx(frD, frA, frB, frC, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frA + >>= match_fregs r3 frB + >>= match_fregs r2 frC + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfmsub(rd, r1, r2, r3) -> + begin match ecode with + | FMSUBx(frD, frA, frB, frC, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frA + >>= match_fregs r3 frB + >>= match_fregs r2 frC + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfnmadd(rd, r1, r2, r3) -> + begin match ecode with + | FNMADDx(frD, frA, frB, frC, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frA + >>= match_fregs r3 frB + >>= match_fregs r2 frC + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfnmsub(rd, r1, r2, r3) -> + begin match ecode with + | FNMSUBx(frD, frA, frB, frC, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frA + >>= match_fregs r3 frB + >>= match_fregs r2 frC + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfsqrt(rd, r1) -> + begin match ecode with + | FSQRTx(frD, frB, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frB + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfrsqrte(rd, r1) -> + begin match ecode with + | FRSQRTEx(frD, frB, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frB + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfres(rd, r1) -> + begin match ecode with + | FRESx(frD, frB, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frB + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pfsel(rd, r1, r2, r3) -> + begin match ecode with + | FSELx(frD, frA, frB, frC, rc) :: es -> + OK(fw) + >>= match_fregs rd frD + >>= match_fregs r1 frA + >>= match_fregs r3 frB + >>= match_fregs r2 frC + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end + | Pisync -> + begin match ecode with + | ISYNC :: es -> + OK(fw) + >>= recur_simpl + | _ -> error + end | Plabel(lbl) -> OK(fw) >>= lblmap_unify lbl pc @@ -1942,7 +1472,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | Some(bs, pofs, psize) -> let f = bitmatch bs with - | { f : 64 : int } -> Int64.float_of_bits f + | { f : 64 : int } -> f in OK(fw) >>= (fun ffw -> @@ -1994,7 +1524,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> | Some(bs, pofs, psize) -> let f = bitmatch bs with - | { f : 32 : int } -> Int32.float_of_bits f + | { f : 32 : int } -> f in OK(fw) >>= (fun ffw -> @@ -2014,7 +1544,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= match_iregs GPR12 rD0 >>= match_iregs GPR0 rA0 >>= match_fregs r1 frD1 - >>= match_floats32 c f + >>= match_floats32 c f >>^ (ff_ef ^%= add_range pofs psize 4 (Float32_literal(f))) >>= match_iregs GPR12 rA1 >>= continue @@ -2079,6 +1609,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Plhbrx(rd, r1, r2) -> + begin match ecode with + | LHBRX(rD, rA, rB):: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end | Plhz(rd, Csymbol_sda(ident, ofs), r1) -> begin match ecode with | LHZ(rD, rA, d) :: es -> @@ -2108,6 +1648,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Plwbrx(rd, r1, r2) -> + begin match ecode with + | LWBRX(rD, rA, rB):: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end | Plwz(rd, Csymbol_sda(ident, ofs), r1) -> begin match ecode with | LWZ(rD, rA, d) :: es -> @@ -2127,6 +1677,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Plwzu(rd, cst, r1) -> + begin match ecode with + | LWZU(rD, rA, d) :: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1 rA + >>= match_csts cst (exts d) + >>= recur_simpl + | _ -> error + end | Plwzx(rd, r1, r2) | Plwzx_a(rd, r1, r2) -> begin match ecode with | LWZX(rD, rA, rB) :: es -> @@ -2137,21 +1697,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pmfcrbit(rd, bit) -> + | Pmfcr rd -> begin match ecode with - | MFCR (rD0) :: - RLWINMx(rS1, rA1, sh1, mb1, me1, rc1) :: es -> + | MFCR (rD0) :: es -> OK(fw) >>= match_iregs rd rD0 - >>= match_iregs rd rS1 - >>= match_iregs rd rA1 - >>= match_crbits bit (sh1 - 1) - >>= match_ints 31 mb1 - >>= match_ints 31 me1 - >>= match_bools false rc1 - >>= compare_code cs es (Int32.add 8l pc) + >>= recur_simpl | _ -> error - end + end + | Pmfcrbit(rd, bit) -> + error | Pmflr(r) -> begin match ecode with | MFSPR(rD, spr) :: es -> @@ -2395,6 +1950,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstfdu(rd, cst, r1) -> + begin match ecode with + | STFDU(frS, rA, d) :: es -> + OK(fw) + >>= match_fregs rd frS + >>= match_iregs r1 rA + >>= match_csts cst (exts d) + >>= recur_simpl + | _ -> error + end | Pstfdx(rd, r1, r2) | Pstfdx_a(rd, r1, r2) -> begin match ecode with | STFDX(frS, rA, rB) :: es -> @@ -2445,6 +2010,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Psthbrx(rd, r1, r2) -> + begin match ecode with + | STHBRX(rS, rA, rB) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end | Pstw(rd, cst, r1) | Pstw_a(rd, cst, r1) -> begin match ecode with | STW(rS, rA, d) :: es -> @@ -2455,6 +2030,16 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstwu(rd, cst, r1) -> + begin match ecode with + | STWU(rS, rA, d) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= match_iregs r1 rA + >>= match_csts cst (exts d) + >>= recur_simpl + | _ -> error + end | Pstwx(rd, r1, r2) | Pstwx_a(rd, r1, r2) -> begin match ecode with | STWX(rS, rA, rB) :: es -> @@ -2465,6 +2050,26 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Pstwbrx(rd, r1, r2) -> + begin match ecode with + | STWBRX(rS, rA, rB) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end + | Pstwxu(rd, r1, r2) -> + begin match ecode with + | STWUX(rS, rA, rB) :: es -> + OK(fw) + >>= match_iregs rd rS + >>= match_iregs r1 rA + >>= match_iregs r2 rB + >>= recur_simpl + | _ -> error + end | Psubfc(rd, r1, r2) -> begin match ecode with | SUBFCx(rD, rA, rB, oe, rc) :: es -> @@ -2489,6 +2094,17 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Psubfze(rd, r1) -> + begin match ecode with + | SUBFZEx(rD, rA, oe, rc) :: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1 rA + >>= match_bools false oe + >>= match_bools false rc + >>= recur_simpl + | _ -> error + end | Psubfic(rd, r1, cst) -> begin match ecode with | SUBFIC(rD, rA, simm) :: es -> @@ -2499,6 +2115,27 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Psync -> + begin match ecode with + | SYNC :: es -> + OK(fw) + >>= recur_simpl + | _ -> error + end + | Ptrap -> + begin match ecode with + | TW(tO, rA, rB) :: es -> + OK(fw) + >>= (fun ffw -> + bitmatch tO with + | { 31 : 5 : int } -> OK(ffw) + | { _ } -> ERR("bitmatch") + ) + >>= match_iregs GPR0 rA + >>= match_iregs GPR0 rB + >>= recur_simpl + | _ -> error + end | Pxor(rd, r1, r2) -> begin match ecode with | XORx(rS, rA, rB, rc) :: es -> @@ -2530,142 +2167,6 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end -and check_builtin_vload_common ccode ecode pc chunk addr offset res fw = - let error = ERR("Non-matching instructions") in - let recur_simpl = compare_code ccode (List.tl ecode) (Int32.add pc 4l) in - begin match chunk, res with - | Mint8unsigned, [IR res] -> - begin match ecode with - | LBZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mint8signed, [IR res] -> - begin match ecode with - | LBZ (rD0, rA0, d0) :: - EXTSBx(rS1, rA1, rc1) :: es -> - OK(fw) - >>= match_iregs res rD0 - >>= match_iregs addr rA0 - >>= match_csts offset (exts d0) - >>= match_iregs res rS1 - >>= match_iregs res rA1 - >>= match_bools false rc1 - >>= compare_code ccode es (Int32.add 8l pc) - | _ -> error - end - | Mint16unsigned, [IR res] -> - begin match ecode with - | LHZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mint16signed, [IR res] -> - begin match ecode with - | LHA(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mint32, [IR res] -> - begin match ecode with - | LWZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs res rD - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mfloat32, [FR res] -> - begin match ecode with - | LFS(frD, rA, d) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mfloat64, [FR res] -> - begin match ecode with - | LFD(frD, rA, d) :: es -> - OK(fw) - >>= match_fregs res frD - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | _ -> error - end -and check_builtin_vstore_common ccode ecode pc chunk addr offset src fw = - let recur_simpl = compare_code ccode (List.tl ecode) (Int32.add pc 4l) in - let error = ERR("Non-matching instructions") in - begin match chunk, src with - | (Mint8signed | Mint8unsigned), IR src -> - begin match ecode with - | STB(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs src rS - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | (Mint16signed | Mint16unsigned), IR src -> - begin match ecode with - | STH(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs src rS - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mint32, IR src -> - begin match ecode with - | STW(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs src rS - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mfloat32, FR src -> - begin match ecode with - | STFS(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs src frS - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | Mfloat64, FR src -> - begin match ecode with - | STFD(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs src frS - >>= match_iregs addr rA - >>= match_csts offset (exts d) - >>= recur_simpl - | _ -> error - end - | _ -> error - end (** A work element is a triple giving a CompCert ident for the function to analyze, its name as a string, and the actual code. It is not obvious how @@ -2822,7 +2323,7 @@ let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework) | Init_float32(f) -> ( bitmatch bs with | { j : 32 : int; bs : -1 : bitstring } -> - if camlfloat_of_coqfloat f = Int32.float_of_bits j + if camlint_of_coqint (Floats.Float32.to_bits f) = j then compare_data_aux l bs (s + 4) sfw else ERR("Wrong float32") | { _ } -> error @@ -2830,7 +2331,7 @@ let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework) | Init_float64(f) -> ( bitmatch bs with | { j : 64 : int; bs : -1 : bitstring } -> - if camlfloat_of_coqfloat f = Int64.float_of_bits j + if camlint64_of_coqint (Floats.Float.to_bits f) = j then compare_data_aux l bs (s + 8) sfw else ERR("Wrong float64") | { _ } -> error @@ -3276,6 +2777,7 @@ let warn_sections_remapping efw = print_debug "Checking remapped sections"; StringMap.fold (fun c_name (e_name, conflicts) efw -> + if c_name = "COMM" then efw else if StringSet.is_empty conflicts then match e_name with diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 0f7ec44..30c0b38 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -24,8 +24,8 @@ type byte_chunk_desc = | Zero_symbol | Stub of string | Jumptable - | Float_literal of float - | Float32_literal of float + | Float_literal of int64 + | Float32_literal of int32 | Padding | Unknown of string @@ -208,7 +208,7 @@ let string_of_byte_chunk_desc = function | Zero_symbol -> "Symbol 0" | 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 +| Float_literal(f) -> "Float literal: " ^ string_of_int64 f +| Float32_literal(f) -> "Float32 literal: " ^ string_of_int32 f | Padding -> "Padding" | Unknown(s) -> "???" ^ (if !verbose_elfmap then s else "") diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml index d7947ee..dc98493 100644 --- a/checklink/Fuzz.ml +++ b/checklink/Fuzz.ml @@ -75,7 +75,6 @@ let fuzz_check elfmap bs byte old sdumps = let ok_fuzz elfmap str byte fuzz = let (a, b, _, r) = full_range_of_byte elfmap byte in let a = Safe32.to_int a in - let b = Safe32.to_int b in let old = Char.code str.[byte] in let fuz = Char.code fuzz in match r with @@ -98,13 +97,7 @@ let ok_fuzz elfmap str byte fuzz = && ((old land 0xf = 0) || (fuz land 0xf = 0)) ) | Symtab_function(_) -> true - | Data_symbol(_) -> - (* False positive: 0. becomes -0. *) - not ( - (byte + 7 <= b) - && (fuz = 0x80) (* sign bit *) - && String.sub str byte 8 = "\000\000\000\000\000\000\000\000" - ) + | Data_symbol(_) -> true | Function_symbol(_) -> let opcode = Char.code str.[byte - 3] in (* False positive: rlwinm with bitmask 0 31 = bitmask n (n - 1) *) @@ -113,14 +106,8 @@ let ok_fuzz elfmap str byte fuzz = | Zero_symbol -> false | Stub(_) -> true | Jumptable -> true - | 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 + | Float_literal(_) -> true + | 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 |