summaryrefslogtreecommitdiff
path: root/checklink
diff options
context:
space:
mode:
Diffstat (limited to 'checklink')
-rw-r--r--checklink/Asm_printers.ml47
-rw-r--r--checklink/Check.ml1164
-rw-r--r--checklink/Frameworks.ml8
-rw-r--r--checklink/Fuzz.ml19
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