open Asm open Asm_printers open AST open BinInt open BinPos open Bitstring_utils open C2C open ELF_parsers open ELF_printers open ELF_types open ELF_utils open Frameworks open Lens open Library open PPC_parsers open PPC_printers open PPC_types open PPC_utils open Sections (** Enables immediate printing of log information to stdout. Warning: will print out everything even when backtracking. *) let debug = ref false (** Whether to print the ELF map *) let print_elfmap = ref false (** Whether to dump the ELF map *) let dump_elfmap = ref false (** Whether to check that all ELF function/data symbols have been matched against CompCert idents *) let exhaustivity = ref true (** CompCert Asm *) type ccode = Asm.instruction list (** Adds a log entry into the framework. *) let add_log (entry: log_entry) (efw: e_framework): e_framework = if !debug then print_endline (string_of_log_entry true entry); {efw with log = entry :: efw.log} (** [flag] should have only one bit set. *) let is_set_flag (flag: int32) (bitset: int32): bool = Int32.logand bitset flag <> 0l (** Checks that [atom]'s binding matches [sym]'s. *) let check_st_bind atom (sym: elf32_sym): s_framework -> s_framework = let static = atom.a_storage = C.Storage_static || atom.a_inline in match static, sym.st_bind with | true, STB_LOCAL -> id | false, STB_GLOBAL -> id | _ -> ( sf_ef ^%= add_log (ERROR( "Symbol: " ^ sym.st_name ^ " has a wrong binding (local vs. global)" )) ) (** Taken 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_const -> ".rodata" | Section_small_const -> ".sdata2" | Section_string -> ".rodata" | Section_literal -> ".rodata.cst8" | Section_jumptable -> ".text" | Section_user(s, wr, ex) -> s (** Taken from CompCert *) let name_of_section_Diab: 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_const -> ".text" | Section_small_const -> ".sdata2" | Section_string -> ".text" | Section_literal -> ".text" | Section_jumptable -> ".text" | Section_user(s, wr, ex) -> s (** Taken from CompCert *) let name_of_section: section_name -> string = begin match Configuration.system with | "macosx" -> failwith "Unsupported CompCert configuration: macosx" | "linux" -> name_of_section_Linux | "diab" -> name_of_section_Diab | _ -> failwith "Unsupported CompCert configuration" end (** Compares a CompCert section name with an ELF section name. *) let match_sections_name (c_section: section_name) (e_name: string) (sfw: s_framework): s_framework = let c_name = name_of_section c_section in try let expected = StringMap.find c_name sfw.ef.section_map in if e_name = expected then sfw else ( sfw >>> sf_ef ^%= add_log (ERROR( Printf.sprintf "CompCert section %s was mapped to both %s and %s" c_name expected e_name )) ) with Not_found -> ( sfw >>> (sf_ef |-- section_map) ^%= StringMap.add c_name e_name ) (** Checks the symbol table entry of the function symbol number [sym_ndx], according to CompCert's [ident]. *) let check_fun_symtab (ident: ident) (sym_ndx: int) (sfw: s_framework): s_framework = let elf = sfw.ef.elf in let symtab_sndx = from_some (section_ndx_by_name elf ".symtab") in let symtab_ent_start = Int32.(add elf.e_shdra.(symtab_sndx).sh_offset (Safe32.of_int (16 * sym_ndx))) in let sym = sfw.ef.elf.e_symtab.(sym_ndx) in let atom = Hashtbl.find sfw.atoms ident in let section = match atom.a_sections with | [t; _; _] -> t | _ -> Section_text in sfw >>> check_st_bind atom sym >>> ( if sym.st_type = STT_FUNC then id else (sf_ef ^%= add_log (ERROR("Symbol should have type STT_FUNC")) ) ) >>> ( if sym.st_other = 0 then id else (sf_ef ^%= add_log (ERROR("Symbol should have st_other set to 0")) ) ) >>> match_sections_name section elf.e_shdra.(sym.st_shndx).sh_name >>> sf_ef ^%= add_range symtab_ent_start 16l 4 (Symtab_function(sym)) (** Checks that the offset [ofs] is well aligned with regards to [al], expressed in bytes. *) let is_well_aligned (ofs: int32) (al: int): bool = al = 0 || Int32.rem ofs (Safe32.of_int al) = 0l (** Adds a function symbol to the set of covered symbols. *) let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework = let elf = ffw.sf.ef.elf in let sym = elf.e_symtab.(ndx) in let sym_sndx = sym.st_shndx in let sym_size = sym.st_size in let sym_shdr = elf.e_shdra.(sym_sndx) in let sym_vaddr = sym.st_value in let sym_ofs_local = Int32.sub sym_vaddr sym_shdr.sh_addr in let sxn_ofs = sym_shdr.sh_offset in let sym_begin = Int32.add sxn_ofs sym_ofs_local in let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in let align = match atom.a_alignment with | Some(a) -> a | None -> 0 in ffw.sf.ef.chkd_fun_syms.(ndx) <- true; ffw >>> (ff_ef ^%= add_range sym_begin sym_size align (Function_symbol(sym))) >>> (ff_sf ^%= if not (is_well_aligned sym_ofs_local align) then ( sf_ef ^%= add_log (ERROR("Symbol not correctly aligned in the ELF file")) ) else id ) >>> (ff_sf ^%= check_fun_symtab ffw.this_ident ndx) (** Taken from CompCert *) let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$" (** Tries to refine the mapping for key [k] in [ident_to_sym_ndx] so that it is mapped to [vaddr]. Fails if no symbol in [k]'s mapping has that virtual address, unless the symbol is a stub from CompCert. Otherwise, it filters out all symbols whose virtual address does not match [vaddr]. *) let idmap_unify (k: positive) (vaddr: int32) (sfw: s_framework): s_framework or_err = try ( let id_ndxes = PosMap.find k sfw.ident_to_sym_ndx in match List.filter (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_value = vaddr) id_ndxes with | [] -> if Str.string_match re_variadic_stub (Hashtbl.find sfw.ident_to_name k) 0 then (* this points to a stub *) try ( let v = PosMap.find k sfw.stub_ident_to_vaddr in if vaddr = v then OK(sfw) else ERR( "Incoherent constraints for stub: " ^ Hashtbl.find sfw.ident_to_name k ) ) with Not_found -> OK( sfw >>> (stub_ident_to_vaddr ^%= PosMap.add k vaddr) ) else (* not a stub, so this is a real error *) ERR( "Incoherent constraints for ident " ^ Hashtbl.find sfw.ident_to_name k ^ " with value " ^ string_of_int32 vaddr ^ " and candidates [" ^ (string_of_list (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value ) ", " id_ndxes ) ^ "]" ) | ndxes -> if id_ndxes = ndxes then OK(sfw) else OK((ident_to_sym_ndx ^%= (PosMap.add k ndxes)) sfw) ) with | Not_found -> ERR( "Missing ident: " ^ Hashtbl.find sfw.ident_to_name k ^ " should be at vaddr: " ^ string_of_int32 vaddr ) (** Checks whether the label [k] points to [v] in [label_to_vaddr]. If it points to another virtual address, this returns an ERR. If it points to nothing, the mapping [k] -> [v] is added. Thus, the first time a label is encountered determines the expected virtual address of its destination. Subsequent references to the label will have to conform. *) let lblmap_unify (k: label) (v: int32) (ffw: f_framework) : f_framework or_err = try ( let v' = PosMap.find k ffw.label_to_vaddr in if v = v' then OK ffw else ( ERR( "Incoherent constraints for label " ^ string_of_positive k ^ " with values " ^ string_of_int32 v ^ " and " ^ string_of_int32 v' ) ) ) with | Not_found -> OK { ffw with label_to_vaddr = PosMap.add k v ffw.label_to_vaddr } let ireg_arr: ireg array = [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7; GPR8; GPR9; GPR10; GPR11; GPR12; GPR13; GPR14; GPR15; GPR16; GPR17; GPR18; GPR19; GPR20; GPR21; GPR22; GPR23; GPR24; GPR25; GPR26; GPR27; GPR28; GPR29; GPR30; GPR31 |] let freg_arr: freg array = [| FPR0; FPR1; FPR2; FPR3; FPR4; FPR5; FPR6; FPR7; FPR8; FPR9; FPR10; FPR11; FPR12; FPR13; FPR14; FPR15; FPR16; FPR17; FPR18; FPR19; FPR20; FPR21; FPR22; FPR23; FPR24; FPR25; FPR26; FPR27; FPR28; FPR29; FPR30; FPR31 |] let crbit_arr: crbit array = [| CRbit_0; CRbit_1; CRbit_2; CRbit_3 |] (** Generic condition checker *) let check (cond: bool) (msg: string) (ffw: f_framework): f_framework = if cond then ffw else ffw >>> ff_ef ^%= add_log (ERROR(msg)) let check_eq (msg: string) (a: 'a) (b: 'a): f_framework -> f_framework = check (a = b) msg let match_bools: bool -> bool -> f_framework -> f_framework = check_eq "match_bools" let match_ints: int -> int -> f_framework -> f_framework = check_eq "match_ints" let match_int32s: int32 -> int32 -> f_framework -> f_framework = check_eq "match_int32s" (** We compare floats by their bit representation, so that 0.0 and -0.0 are different. *) let match_floats (a: float) (b: float): f_framework -> f_framework = check_eq "match_floats" (Int64.bits_of_float a) (Int64.bits_of_float b) let match_crbits cb eb = check_eq "match_crbits" cb (crbit_arr.(eb)) let match_iregs cr er = check_eq "match_iregs" cr (ireg_arr.(er)) let match_fregs cr er = check_eq "match_fregs" cr (freg_arr.(er)) let name_of_ndx (efw: e_framework) (ndx: int): string = let st = efw.elf.e_symtab.(ndx) in st.st_name ^ " at address " ^ (string_of_int32 st.st_value) (** Filters the lower 16 bits of an int32. *) let low: int32 -> int32 = Int32.logand 0x0000ffffl (** high_exts x is equal to: - the 16 high bits of x if its lower 16 bits form a positive 16 bit integer - the 16 high bits of x plus one otherwise This is so that: x == high_exts x + exts (low x) *) let high_exts (x: int32): int32 = Int32.( if logand x 0x00008000l = 0l then logand x 0xffff0000l else add 0x00010000l (logand x 0xffff0000l) ) (** Matches a CompCert constant against an [int32]. *) let match_csts (cc: constant) (ec: int32) (ffw: f_framework): f_framework = let sfw = ffw |. ff_sf in let efw = ffw |. ff_ef in match cc with | Cint (i) -> check_eq "match_csts Cint" ec (z_int32_lax i) ffw | Csymbol_low (ident, i) -> let candidates = try PosMap.find ident sfw.ident_to_sym_ndx with Not_found -> [] in let vaddrs = List.filter (fun ndx -> let ident_vaddr = efw.elf.e_symtab.(ndx).st_value in Int32.(low (add ident_vaddr (z_int32_lax i)) = low ec) ) candidates in begin match vaddrs with | [] -> let sym_names = List.map (name_of_ndx efw) candidates in (ff_ef ^%= (add_log (ERROR("Csymbol_low " ^ string_of_list id ", " sym_names))) ) ffw | _ -> if candidates = vaddrs then ffw else ( ffw >>> ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) ) end | Csymbol_high (ident, i) -> (* In this case, ec is 0x0000XXXX standing for XXXX0000 *) let candidates = try PosMap.find ident sfw.ident_to_sym_ndx with Not_found -> [] in let vaddrs = List.filter (fun ndx -> let ident_vaddr = efw.elf.e_symtab.(ndx).st_value in Int32.(high_exts (add ident_vaddr (z_int32_lax i)) = shift_left ec 16)) candidates in begin match vaddrs with | [] -> let sym_names = List.map (name_of_ndx efw) candidates in (ff_ef ^%= (add_log (ERROR("Csymbol_high " ^ string_of_list id ", " sym_names))) ) ffw | _ -> if candidates = vaddrs then ffw else ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) ffw end | Csymbol_sda (ident, i) -> (* sda should be handled separately in places it occurs *) failwith "Unhandled Csymbol_sda, please report." let match_z_int32 (cz: coq_Z) (ei: int32) = check_eq "match_z_int32" (z_int32 cz) ei let match_z_int (cz: coq_Z) (ei: int) = check_eq "match_z_int" (z_int32 cz) (Safe32.of_int ei) (* [m] is interpreted as a bitmask, and checked against [ei]. *) let match_mask (m: coq_Z) (ei: int32) = check_eq ("match_mask " ^ string_of_int32 (z_int32_lax m) ^ " and " ^ string_of_int32 ei) (z_int32_lax m) ei (** Checks that the special register referred to in [spr] is [r]. *) let match_spr (str: string) (r: int) (spr: bitstring) : f_framework -> f_framework = bitmatch spr with | { v:5; 0:5 } when v = r -> id | { _ } -> ff_ef ^%= (add_log (ERROR(str))) let match_xer = match_spr "match_xer" 1 let match_lr = match_spr "match_lr" 8 let match_ctr = match_spr "match_ctr" 9 (** Read a n-bits bitstring as a signed integer, two's complement representation (n < 32). *) let exts (bs: bitstring): int32 = let signif_bits = Bitstring.bitstring_length bs - 1 in bitmatch bs with | { sign : 1 ; rest : signif_bits : int } -> Int64.( to_int32 ( if sign then logor rest (lognot (sub (shift_left one signif_bits) one)) else rest ) ) (** Creates a bitmask from bits mb to me, according to the specification in "4.2.1.4 Integer Rotate and Shift Instructions" of the PowerPC manual. *) let rec bitmask mb me = assert (0 <= mb); assert (0 <= me); assert (mb < 32); assert (me < 32); if (mb, me) = (0, 31) then -1l (* this case does not compute correctly otherwise *) else if mb <= me (* 0 ... mb ... me ... 31 0 0 0 1 1 1 1 1 0 0 0 *) then Int32.(shift_left (sub (shift_left 1l (me - mb + 1)) 1l) (31 - me) ) (* 0 ... me ... mb ... 31 1 1 1 1 0 0 0 1 1 1 1 == 1 1 1 1 1 1 1 1 1 1 1 -1l - 0 0 0 0 1 1 1 0 0 0 0 bitmask (me + 1) (mb - 1) *) else if mb = me + 1 then (-1l) (* this needs special handling *) else Int32.(sub (-1l) (bitmask (me + 1) (mb - 1))) (** Checks that a label did not occur twice in the same function. *) let check_label_unicity ffw = let rec check_label_unicity_aux l ffw = match l with | [] -> ffw | h::t -> ffw >>> ( if List.mem h t then ( ff_ef ^%= (add_log (ERROR("Duplicate label: " ^ string_of_positive h))) ) else id ) >>> check_label_unicity_aux t in check_label_unicity_aux ffw.label_list ffw (** Checks that all the labels that have been referred to in instructions actually appear in the code. *) let check_label_existence ffw = PosMap.fold (fun k v -> if List.mem k ffw.label_list then id else ( ff_ef ^%= (add_log (ERROR("Missing label: " ^ string_of_positive k))) ) ) ffw.label_to_vaddr ffw (** Matches the segment at virtual address [vaddr] with the jumptable expected from label list [lbllist]. Then checks whether the matched chunk of the code had the expected [size]. *) let rec match_jmptbl lbllist vaddr size ffw = let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in let jmptbl_section = match atom.a_sections with | [_; _; j] -> j | _ -> Section_jumptable in let rec match_jmptbl_aux lbllist bs ffw = match lbllist with | [] -> OK ffw | lbl :: lbls -> ( bitmatch bs with | { vaddr : 32 : int; rest : -1 : bitstring } -> ffw >>> lblmap_unify lbl vaddr >>= match_jmptbl_aux lbls rest | { _ } -> print_endline "Ill-formed jump table"; ERR("Ill-formed jump table") ) in let elf = ffw.sf.ef.elf in begin match section_at_vaddr elf vaddr with | None -> ERR("No section for the jumptable") | Some(sndx) -> begin match bitstring_at_vaddr elf vaddr size with | None -> ERR("") | Some(bs, pofs, psize) -> ffw >>> (ff_sf ^%= match_sections_name jmptbl_section elf.e_shdra.(sndx).sh_name ) >>> match_jmptbl_aux lbllist bs >>? (ff_ef ^%= add_range pofs psize 0 Jumptable) end end (** 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) option = 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 -> fw >>> match_fregs FPR0 frD0 >>> match_iregs src rA0 >>> match_int32s ofs32 (exts d0) >>> match_fregs FPR0 frS1 >>> match_iregs dst rA1 >>> match_int32s ofs32 (exts d1) >>> match_memcpy_small_aux (ofs + 8) (sz - 8) es (Int32.add 8l pc) | _ -> None ) else if sz >= 4 then ( match ecode with | LWZ(rD0, rA0, d0) :: STW(rS1, rA1, d1) :: es -> 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) | _ -> None ) else if sz >= 2 then ( match ecode with | LHZ(rD0, rA0, d0) :: STH(rS1, rA1, d1) :: es -> 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) | _ -> None ) else if sz >= 1 then ( match ecode with | LBZ(rD0, rA0, d0) :: STB(rS1, rA1, d1) :: es -> 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) | _ -> None ) else Some(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) option = 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 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) >>> ( bitmatch bo6 with | { 16:5:int } -> id | { _ } -> ff_ef ^%= add_log (ERROR("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 -> 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 -> Some(fw, es, Int32.add 36l pc)) | _ -> None end | 2 -> begin match es with | LHZ(rD0, rA0, d0) :: STH(rS1, rA1, d1) :: es -> 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 -> Some(fw, es , Int32.add 36l pc)) | _ -> None end | 3 -> begin match es with | LHZ(rD0, rA0, d0) :: STH(rS1, rA1, d1) :: LBZ(rD2, rA2, d2) :: STB(rS3, rA3, d3) :: es -> 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 -> Some(fw, es, Int32.add 44l pc)) | _ -> None end | _ -> Some(fw, es, Int32.add 28l pc) ) | _ -> None let match_bo_bt_bool bo = bitmatch bo with | { false:1; true:1; true:1; false:1; false:1 } -> true | { _ } -> false let match_bo_bf_bool bo = bitmatch bo with | { false:1; false:1; true:1; false:1; false:1 } -> true | { _ } -> false let match_bo_bt bo ffw = ffw >>> (ff_ef ^%= bitmatch bo with | { false:1; true:1; true:1; false:1; false:1 } -> id | { _ } -> add_log (ERROR("match_bo_bt")) ) let match_bo_bf bo ffw = ffw >>> (ff_ef ^%= if match_bo_bf_bool bo then id else add_log (ERROR("match_bo_bf")) ) let match_bo_ctr bo ffw = ffw >>> (ff_ef ^%= bitmatch bo with | { true:1; false:1; true:1; false:1; false:1 } -> id | { _ } -> add_log (ERROR("bitmatch")) ) let check_sda ident ofs r addr ffw: f_framework or_err = let ofs = z_int32 ofs in let check_sda_aux ndx: f_framework or_err = let elf = ffw.sf.ef.elf in let sym = elf.e_symtab.(ndx) in let sxn = elf.e_shdra.(sym.st_shndx) in try let r_addr = IntMap.find r ffw.sf.ef.sda_map in if r_addr < sxn.sh_offset || r_addr >= Safe32.(sxn.sh_offset + sxn.sh_size) then ERR("SDA register out of the address range of its symbol's section") else if Safe32.(r_addr + ofs) = sym.st_value then OK(ffw) else ERR( Printf.sprintf "SDA register %d is expected to point both at 0x%lx and 0x%lx" r r_addr Safe32.(sym.st_value - ofs) ) with Not_found -> OK( ffw >>> (ff_ef |-- sda_map) ^%= IntMap.add r Safe32.(sym.st_value - ofs) ) in let sym_list = PosMap.find ident ffw.sf.ident_to_sym_ndx in let res = List.map check_sda_aux sym_list in match filter_ok res with | [] -> ERR("No satisfying SDA mapping, errors were: " ^ string_of_list id ", " (filter_err res)) | [ffw] -> OK(ffw) | _ -> failwith "Multiple possible SDA mappings, please report." (** Compares a whole CompCert function code against an ELF code, starting at program counter [pc]. *) let rec compare_code ccode ecode pc fw: f_framework or_err = let error = ERR("Non-matching instructions") in match ccode, ecode with | [], [] -> OK(fw) | [], e_rest -> let rest_str = String.concat "\n" (List.map string_of_instr e_rest) in ERR("CompCert code exhausted before the end of ELF code, remaining:\n" ^ rest_str) | c_rest, [] -> let rest_str = String.concat "\n" (List.map string_of_instruction c_rest) in ERR("ELF code exhausted before the end of CompCert code, remaining:\n" ^ rest_str) | c::cs, e::es -> let recur_simpl = compare_code cs es (Int32.add 4l pc) in let fw = if !debug then ( let curr_instr = " [" ^ string_of_int32 pc ^ "] " ^ string_of_instruction c ^ " - " ^ string_of_instr e in (ff_ef ^%= add_log (DEBUG(curr_instr))) fw ) else fw in match c with | Padd(rd, r1, r2) -> begin match ecode with | ADDx(rD, rA, rB, oe, rc) :: es -> 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 -> 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 | Paddi(rd, r1, Csymbol_sda(ident, ofs)) -> begin match ecode with | ADDI(rD, rA, simm) :: es -> fw >>> match_iregs rd rD >>> check_sda ident ofs rA (exts simm) >>= recur_simpl | _ -> error end | Paddi(rd, r1, cst) -> begin match ecode with | ADDI(rD, rA, simm) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_csts cst (exts simm) >>> recur_simpl | _ -> error end | Paddic(rd, r1, cst) -> begin match ecode with | ADDIC(rD, rA, simm) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_csts cst (exts simm) >>> recur_simpl | _ -> error end | Paddis(rd, r1, cst) -> begin match ecode with | ADDIS(rD, rA, simm) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_csts cst (Safe32.of_int simm) >>> recur_simpl | _ -> error end | Paddze(rd, r1) -> begin match ecode with | ADDZEx(rD, rA, oe, rc) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_bools false oe >>> match_bools false rc >>> recur_simpl | _ -> error end | Pallocframe(sz, ofs) -> begin match ecode with | STWU(rS, rA, d) :: es -> 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 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 | Pandc(rd, r1, r2) -> begin match ecode with | ANDCx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pand_(rd, r1, r2) -> begin match ecode with | ANDx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools true rc >>> recur_simpl | _ -> error end | Pandis_(rd, r1, cst) -> begin match ecode with | ANDIS_(rS, rA, uimm) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end | Pandi_(rd, r1, cst) -> begin match ecode with | ANDI_(rS, rA, uimm) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end | Pannot(ef, args) -> fw >>> compare_code cs ecode pc | Pb(lbl) -> begin match ecode with | Bx(li, aa, lk) :: es -> let lblvaddr = Int32.(add pc (mul 4l (exts li))) in fw >>> lblmap_unify lbl lblvaddr >>? match_bools false aa >>? match_bools false lk >>= recur_simpl | _ -> error end | Pbctr -> begin match ecode with | BCCTRx(bo, bi, lk) :: es -> fw >>> match_bo_ctr bo >>> match_ints 0 bi >>> match_bools false lk >>> recur_simpl | _ -> error end | Pbctrl -> begin match ecode with | BCCTRx(bo, bi, lk) :: es -> fw >>> match_bo_ctr bo >>> match_ints 0 bi >>> match_bools true 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 -> let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in fw (* >>> match_bo_bf bo already done in pattern match *) >>> match_crbits bit bi >>> lblmap_unify lbl lblvaddr >>? match_bools false aa >>? match_bools false lk >>= recur_simpl | BCx(bo0, bi0, bd0, aa0, lk0) :: Bx (li1, aa1, lk1) :: es -> let cnext = Int32.add pc 8l in let enext = Int32.(add pc (mul 4l (exts bd0))) in let lblvaddr = Int32.(add pc (mul 4l (exts bd0))) in fw >>> match_bo_bt bo0 >>> match_crbits bit bi0 >>> match_int32s cnext enext >>> match_bools false aa0 >>> match_bools false lk0 >>> lblmap_unify lbl lblvaddr >>? match_bools false aa1 >>? match_bools false lk1 >>= compare_code cs es (Int32.add 8l pc) | _ -> error end | Pbl(ident) -> begin match ecode with | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in fw >>> (ff_sf ^%=? idmap_unify ident dest) >>? match_bools false aa >>? match_bools true lk >>= recur_simpl | _ -> error end | Pblr -> begin match ecode with | BCLRx(bo, bi, lk) :: es -> fw >>> match_bo_ctr bo >>> match_ints 0 bi >>> match_bools false lk >>> recur_simpl | _ -> error end | Pbs(ident) -> begin match ecode with | Bx(li, aa, lk) :: es -> let dest = Int32.(add pc (mul 4l (exts li))) in fw >>> match_bools false aa >>> match_bools false lk >>> (ff_sf ^%=? idmap_unify ident dest) >>= recur_simpl | _ -> error end | Pbt(bit, lbl) -> begin match ecode with | BCx(bo, bi, bd, aa, lk) :: es when match_bo_bt_bool bo -> let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in fw (* >>> match_bo_bt bo already done in pattern match *) >>> match_crbits bit bi >>> lblmap_unify lbl lblvaddr >>? match_bools false aa >>? match_bools false lk >>= recur_simpl | BCx(bo0, bi0, bd0, aa0, lk0) :: Bx (li1, aa1, lk1) :: es -> let cnext = Int32.add pc 8l in let enext = Int32.(add pc (mul 4l (exts bd0))) in let lblvaddr = Int32.(add pc (mul 4l (exts bd0))) in fw >>> match_bo_bf bo0 >>> match_crbits bit bi0 >>> match_int32s cnext enext >>> match_bools false aa0 >>> match_bools false lk0 >>> lblmap_unify lbl lblvaddr >>? match_bools false aa1 >>? match_bools false lk1 >>= compare_code cs es (Int32.add 8l pc) | _ -> error end | Pbtbl(reg, table) -> begin match ecode with | ADDIS (rD0, rA0, simm0) :: LWZ (rD1, rA1, d1) :: MTSPR (rS2, spr2) :: BCCTRx(bo3, bi3, rc3) :: es -> let tblvaddr = Int32.( add (shift_left (Safe32.of_int simm0) 16) (exts d1) ) in let tblsize = Safe32.of_int (32 * List.length table) in fw >>> match_iregs GPR12 rD0 >>> match_iregs reg rA0 >>> match_iregs GPR12 rD1 >>> match_iregs GPR12 rA1 >>> match_iregs GPR12 rS2 >>> match_ctr spr2 >>> match_bo_ctr bo3 >>> match_ints 0 bi3 >>> match_bools false rc3 >>> match_jmptbl table tblvaddr tblsize >>= compare_code cs es (Int32.add 16l pc) | _ -> error 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 -> 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 -> 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 -> fw >>> match_iregs a1 rS >>> match_iregs res rA >>> match_bools false rc >>> recur_simpl | _ -> error end | "__builtin_bswap", [IR a1], IR res -> begin match ecode with | STWU (rS0, rA0, d0) :: LWBRX(rD1, rA1, rB1) :: ADDI (rD2, rA2, simm2) :: es -> 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_fmadd", [FR a1; FR a2; FR a3], FR res -> begin match ecode with | FMADDx(frD, frA, frB, frC, rc) :: es -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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_read16_reversed", [IR a1], IR res -> begin match ecode with | LHBRX(rD, rA, rB):: es -> 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 -> 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 -> 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 -> 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 -> fw >>> recur_simpl | _ -> error end | "__builtin_sync", [], _ -> begin match ecode with | SYNC :: es -> fw >>> recur_simpl | _ -> error end | "__builtin_isync", [], _ -> begin match ecode with | ISYNC :: es -> fw >>> recur_simpl | _ -> error end | "__builtin_trap", [], _ -> begin match ecode with | TW(tO, rA, rB) :: es -> fw >>> (ff_ef ^%= bitmatch tO with | { 31 : 5 : int } -> id | { _ } -> add_log (ERROR("bitmatch")) ) >>> match_iregs GPR0 rA >>> match_iregs GPR0 rB >>> recur_simpl | _ -> error end | _ -> error end | EF_vload(chunk) -> begin match args with | [IR addr] -> fw >>> check_builtin_vload_common cs ecode pc chunk addr (Cint Integers.Int.zero) res | _ -> failwith "Unexpected args in EF_vload, please report." end | EF_vstore(chunk) -> begin match args with | [IR addr; src] -> fw >>> check_builtin_vstore_common cs ecode pc chunk addr (Cint Integers.Int.zero) src | _ -> failwith "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 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 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 | _ -> failwith "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 <= 64 then ( match match_memcpy_small ecode pc sz al src dst fw with | None -> error | Some(fw, es, pc) -> compare_code cs es pc fw ) else ( match match_memcpy_big ecode pc sz al src dst fw with | None -> error | Some(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 -> 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 -> 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(_, _) -> failwith "Unexpected EF_annot, please report." | EF_external(_, _) -> failwith "Unexpected EF_external, please report." | EF_free -> failwith "Unexpected EF_free, please report." | EF_malloc -> failwith "Unexpected EF_malloc, please report." end | Pcmplw(r1, r2) -> begin match ecode with | CMPL(crfD, l, rA, rB) :: es -> fw >>> match_crbits CRbit_0 crfD >>> match_bools false l >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Pcmplwi(r1, cst) -> begin match ecode with | CMPLI(crfD, l, rA, uimm) :: es -> fw >>> match_iregs r1 rA >>> match_csts cst (Safe32.of_int uimm) >>> match_crbits CRbit_0 crfD >>> match_bools false l >>> recur_simpl | _ -> error end | Pcmpw(r1, r2) -> begin match ecode with | CMP(crfD, l, rA, rB) :: es -> fw >>> match_ints crfD 0 >>> match_bools l false >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Pcmpwi(r1, cst) -> begin match ecode with | CMPI(crfD, l, rA, simm) :: es -> fw >>> match_ints crfD 0 >>> match_bools false l >>> match_iregs r1 rA >>> match_csts cst (exts simm) >>> recur_simpl | _ -> error end | Pcror(bd, b1, b2) -> begin match ecode with | CROR(crbD, crbA, crbB) :: es -> 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 -> 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 | Pdivwu(rd, r1, r2) -> begin match ecode with | DIVWUx(rD, rA, rB, oe, rc) :: es -> 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 | Peqv(rd, r1, r2) -> begin match ecode with | EQVx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pextsb(rd, r1) -> begin match ecode with | EXTSBx(rS, rA, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_bools false rc >>> recur_simpl | _ -> error end | Pextsh(rd, r1) -> begin match ecode with | EXTSHx(rS, rA, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfabs(rd, r1) -> begin match ecode with | FABSx(frD, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfadd(rd, r1, r2) -> begin match ecode with | FADDx(frD, frA, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frA >>> match_fregs r2 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfcmpu(r1, r2) -> begin match ecode with | FCMPU(crfD, frA, frB) :: es -> fw >>> match_crbits CRbit_0 crfD >>> match_fregs r1 frA >>> match_fregs r2 frB >>> recur_simpl | _ -> error end | Pfcti(rd, r1) -> begin match ecode with | FCTIWZx(frD0, frB0, rc0) :: STFDU (frS1, rA1, d1) :: LWZ (rD2, rA2, d2) :: ADDI (rD3, rA3, simm3) :: es -> 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 | Pfdiv(rd, r1, r2) -> begin match ecode with | FDIVx(frD, frA, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frA >>> match_fregs r2 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfmake(rd, r1, r2) -> begin match ecode with | STWU (rS0, rA0, d0) :: STW (rS1, rA1, d1) :: LFD (frD2, rA2, d2) :: ADDI (rD3, rA3, simm3) :: es -> 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 | Pfmr(rd, r1) -> begin match ecode with | FMRx(frD, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfmul(rd, r1, r2) -> begin match ecode with | FMULx(frD, frA, frC, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frA >>> match_fregs r2 frC >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfneg (rd, r1) -> begin match ecode with | FNEGx(frD, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfreeframe(sz, ofs) -> begin match ecode with | LWZ(rD, rA, d) :: es -> fw >>> match_iregs GPR1 rD >>> match_iregs GPR1 rA >>> match_z_int32 ofs (Int32.neg (exts d)) >>> recur_simpl | _ -> error end | Pfrsp(rd, r1) -> begin match ecode with | FRSPx(frD, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pfsub(rd, r1, r2) -> begin match ecode with | FSUBx(frD, frA, frB, rc) :: es -> fw >>> match_fregs rd frD >>> match_fregs r1 frA >>> match_fregs r2 frB >>> match_bools false rc >>> recur_simpl | _ -> error end | Plabel(lbl) -> fw >>> lblmap_unify lbl pc >>? (fun fw -> {fw with label_list = lbl :: fw.label_list}) >>= compare_code cs ecode pc | Plbz(rd, Csymbol_sda(ident, ofs), r1) -> begin match ecode with | LBZ(rD, rA, d) :: es -> fw >>> match_iregs rd rD >>> check_sda ident ofs rA (exts d) >>= recur_simpl | _ -> error end | Plbz(rd, cst, r1) -> begin match ecode with | LBZ(rD, rA, d) :: es -> fw >>> match_iregs rd rD >>> match_csts cst (exts d) >>> match_iregs r1 rA >>> recur_simpl | _ -> error end | Plbzx(rd, r1, r2) -> begin match ecode with | LBZX(rD, rA, rB) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Plfd(rd, Csymbol_sda(ident, ofs), r1) -> begin match ecode with | LFD(frD, rA, d) :: es -> fw >>> match_fregs rd frD >>> check_sda ident ofs rA (exts d) >>= recur_simpl | _ -> error end | Plfd(rd, cst, r1) -> begin match ecode with | LFD(frD, rA, d) :: es -> fw >>> match_fregs rd frD >>> match_csts cst (exts d) >>> match_iregs r1 rA >>> recur_simpl | _ -> error end | Plfdx(rd, r1, r2) -> begin match ecode with | LFDX(frD, rA, rB) :: es -> fw >>> match_fregs rd frD >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Plfi(r1, c) -> begin match ecode with | ADDIS(rD0, rA0, simm0) :: LFD (frD1, rA1, d1) :: es -> let vaddr = Int32.( add (shift_left (Safe32.of_int simm0) 16) (exts d1) ) in if Int32.rem vaddr 8l <> 0l then ERR("Float constants should be 8-byte aligned") else let elf = fw.sf.ef.elf in let atom = Hashtbl.find fw.sf.atoms fw.this_ident in let literal_section = begin match atom.a_sections with | [_; l; _] -> l | _ -> Section_literal end in let continue = compare_code cs es (Int32.add 8l pc) in begin match bitstring_at_vaddr elf vaddr 64l with | None -> fw >>> (ff_ef ^%= add_log (ERROR("Floating point constant address is wrong"))) >>> continue | Some(bs, pofs, psize) -> let f = bitmatch bs with | { f : 64 : int } -> Int64.float_of_bits f in fw >>> (ff_sf ^%= begin match section_at_vaddr elf vaddr with | None -> sf_ef ^%= add_log (ERROR("No section at that virtual address")) | Some(sndx) -> match_sections_name literal_section elf.e_shdra.(sndx).sh_name end ) >>> match_iregs GPR12 rD0 >>> match_iregs GPR0 rA0 >>> match_fregs r1 frD1 >>> match_floats c f >>> (ff_ef ^%= add_range pofs psize 8 (Float_literal(f))) >>> match_iregs GPR12 rA1 >>> continue end | _ -> error end | Plfs(rd, Csymbol_sda(ident, ofs), r1) -> begin match ecode with | LFS(frD, rA, d) :: es -> fw >>> match_fregs rd frD >>> check_sda ident ofs rA (exts d) >>= recur_simpl | _ -> error end | Plfs(rd, cst, r1) -> begin match ecode with | LFS(frD, rA, d) :: es -> fw >>> match_fregs rd frD >>> match_csts cst (exts d) >>> match_iregs r1 rA >>> recur_simpl | _ -> error end | Plfsx(rd, r1, r2) -> begin match ecode with | LFSX(frD, rA, rB) :: es -> fw >>> match_fregs rd frD >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Plha(rd, Csymbol_sda(ident, ofs), r1) -> begin match ecode with | LHA(rD, rA, d) :: es -> fw >>> match_iregs rd rD >>> check_sda ident ofs rA (exts d) >>= recur_simpl | _ -> error end | Plha(rd, cst, r1) -> begin match ecode with | LHA(rD, rA, d) :: es -> fw >>> match_iregs rd rD >>> match_csts cst (exts d) >>> match_iregs r1 rA >>> recur_simpl | _ -> error end | Plhax(rd, r1, r2) -> begin match ecode with | LHAX(rD, rA, rB) :: es -> 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 -> fw >>> match_iregs rd rD >>> check_sda ident ofs rA (exts d) >>= recur_simpl | _ -> error end | Plhz(rd, cst, r1) -> begin match ecode with | LHZ(rD, rA, d) :: es -> fw >>> match_iregs rd rD >>> match_csts cst (exts d) >>> match_iregs r1 rA >>> recur_simpl | _ -> error end | Plhzx(rd, r1, r2) -> begin match ecode with | LHZX(rD, rA, rB) :: es -> 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 -> fw >>> match_iregs rd rD >>> check_sda ident ofs rA (exts d) >>= recur_simpl | _ -> error end | Plwz(rd, cst, r1) -> begin match ecode with | LWZ(rD, rA, d) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_csts cst (exts d) >>> recur_simpl | _ -> error end | Plwzx(rd, r1, r2) -> begin match ecode with | LWZX(rD, rA, rB) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Pmfcrbit(rd, bit) -> begin match ecode with | MFCR (rD0) :: RLWINMx(rS1, rA1, sh1, mb1, me1, rc1) :: es -> 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) | _ -> error end | Pmflr(r) -> begin match ecode with | MFSPR(rD, spr) :: es -> fw >>> match_iregs r rD >>> match_lr spr >>> recur_simpl | _ -> error end | Pmr(rd, r1) -> begin match ecode with | ORx(rS, rA, rB, rc) :: es when (rB = rS) -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_bools false rc >>> recur_simpl | _ -> error end | Pmtctr(r1) -> begin match ecode with | MTSPR(rS, spr) :: es -> fw >>> match_iregs r1 rS >>> match_ctr spr >>> recur_simpl | _ -> error end | Pmtlr(r1) -> begin match ecode with | MTSPR(rS, spr) :: es -> fw >>> match_iregs r1 rS >>> match_lr spr >>> recur_simpl | _ -> error end | Pmulli(rd, r1, cst) -> begin match ecode with | MULLI(rD, rA, simm) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_csts cst (exts simm) >>> recur_simpl | _ -> error end | Pmullw(rd, r1, r2) -> begin match ecode with | MULLWx(rD, rA, rB, oe, rc) :: es -> 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 | Pnand(rd, r1, r2) -> begin match ecode with | NANDx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pnor(rd, r1, r2) -> begin match ecode with | NORx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Por(rd, r1, r2) -> begin match ecode with | ORx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Porc(rd, r1, r2) -> begin match ecode with | ORCx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pori(rd, r1, cst) -> begin match ecode with | ORI(rS, rA, uimm) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end | Poris(rd, r1, cst) -> begin match ecode with | ORIS(rS, rA, uimm) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end | Prlwimi(rd, r1, amount, mask) -> begin match ecode with | RLWIMIx(rS, rA, sh, mb, me, rc) :: es -> fw >>> match_iregs r1 rS >>> match_iregs rd rA >>> match_z_int amount sh >>> match_mask mask (bitmask mb me) >>> match_bools false rc >>> recur_simpl | _ -> error end | Prlwinm(rd, r1, amount, mask) -> begin match ecode with | RLWINMx(rS, rA, sh, mb, me, rc) :: es -> fw >>> match_iregs r1 rS >>> match_iregs rd rA >>> match_z_int amount sh >>> match_mask mask (bitmask mb me) >>> match_bools false rc >>> recur_simpl | _ -> error end | Pslw(rd, r1, r2) -> begin match ecode with | SLWx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Psraw(rd, r1, r2) -> begin match ecode with | SRAWx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Psrawi(rd, r1, n) -> begin match ecode with | SRAWIx(rS, rA, sh, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_z_int n sh >>> match_bools false rc >>> recur_simpl | _ -> error end | Psrw(rd, r1, r2) -> begin match ecode with | SRWx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pstb(rd, cst, r1) -> begin match ecode with | STB(rS, rA, d) :: es -> fw >>> match_iregs rd rS >>> match_iregs r1 rA >>> match_csts cst (exts d) >>> recur_simpl | _ -> error end | Pstbx(rd, r1, r2) -> begin match ecode with | STBX(rS, rA, rB) :: es -> fw >>> match_iregs rd rS >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Pstfd(rd, cst, r1) -> begin match ecode with | STFD(frS, rA, d) :: es -> fw >>> match_fregs rd frS >>> match_iregs r1 rA >>> match_csts cst (exts d) >>> recur_simpl | _ -> error end | Pstfdx(rd, r1, r2) -> begin match ecode with | STFDX(frS, rA, rB) :: es -> fw >>> match_fregs rd frS >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Pstfs(rd, cst, r1) -> begin match ecode with | FRSPx(frD0, frB0, rc0) :: STFS (frS1, rA1, d1) :: es -> fw >>> match_fregs FPR13 frD0 >>> match_fregs rd frB0 >>> match_bools false rc0 >>> match_fregs FPR13 frS1 >>> match_iregs r1 rA1 >>> match_csts cst (exts d1) >>> compare_code cs es (Int32.add 8l pc) | _ -> error end | Pstfsx(rd, r1, r2) -> begin match ecode with | FRSPx(frD0, frB0, rc0) :: STFSX(frS1, rA1, rB1) :: es -> fw >>> match_fregs FPR13 frD0 >>> match_fregs rd frB0 >>> match_bools false rc0 >>> match_fregs FPR13 frS1 >>> match_iregs r1 rA1 >>> match_iregs r2 rB1 >>> compare_code cs es (Int32.add 8l pc) | _ -> error end | Psth(rd, cst, r1) -> begin match ecode with | STH(rS, rA, d) :: es -> fw >>> match_iregs rd rS >>> match_iregs r1 rA >>> match_csts cst (exts d) >>> recur_simpl | _ -> error end | Psthx(rd, r1, r2) -> begin match ecode with | STHX(rS, rA, rB) :: es -> fw >>> match_iregs rd rS >>> match_iregs r1 rA >>> match_iregs r2 rB >>> recur_simpl | _ -> error end | Pstw(rd, cst, r1) -> begin match ecode with | STW(rS, rA, d) :: es -> fw >>> match_iregs rd rS >>> match_iregs r1 rA >>> match_csts cst (exts d) >>> recur_simpl | _ -> error end | Pstwx(rd, r1, r2) -> begin match ecode with | STWX(rS, rA, rB) :: es -> 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 -> 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 | Psubfe(rd, r1, r2) -> begin match ecode with | SUBFEx(rD, rA, rB, oe, rc) :: es -> 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 | Psubfic(rd, r1, cst) -> begin match ecode with | SUBFIC(rD, rA, simm) :: es -> fw >>> match_iregs rd rD >>> match_iregs r1 rA >>> match_csts cst (exts simm) >>> recur_simpl | _ -> error end | Pxor(rd, r1, r2) -> begin match ecode with | XORx(rS, rA, rB, rc) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_iregs r2 rB >>> match_bools false rc >>> recur_simpl | _ -> error end | Pxori(rd, r1, cst) -> begin match ecode with | XORI(rS, rA, uimm) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end | Pxoris(rd, r1, cst) -> begin match ecode with | XORIS(rS, rA, uimm) :: es -> fw >>> match_iregs rd rA >>> match_iregs r1 rS >>> match_csts cst (Safe32.of_int uimm) >>> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 -> 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 | FRSPx(frD0, frB0, rc0) :: STFS (frS1, rA1, d1) :: es -> fw >>> match_fregs FPR13 frD0 >>> match_fregs src frB0 >>> match_bools false rc0 >>> match_fregs FPR13 frS1 >>> match_iregs addr rA1 >>> match_csts offset (exts d1) >>> compare_code ccode es (Int32.add pc 8l) | _ -> error end | Mfloat64, FR src -> begin match ecode with | STFD(frS, rA, d) :: es -> 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 to recover one of the three components given the other two. *) type worklist = (ident * string * ccode) list (** Pops a work element from the worklist, ensuring that fully-determined idents (i.e. those for which the possible virtual address have been narrowed to one candidate) are picked first. When the first element is not fully-determined, the whole list is sorted so that hopefully several fully-determined idents are brought at the beginning at the same time. *) let worklist_pop fw wl = match wl with | [] -> None | h::t -> let (i, _, _) = h in let candidates = try PosMap.find i fw.ident_to_sym_ndx with Not_found -> [] in match candidates with | [] | [_] -> Some (h, t, candidates) | _ -> let wl = List.fast_sort (fun (i1, _, _) (i2, _, _) -> compare (List.length (PosMap.find i1 fw.ident_to_sym_ndx)) (List.length (PosMap.find i2 fw.ident_to_sym_ndx))) wl in let winner = List.hd wl in let (i, _, _) = winner in Some (winner, List.tl wl, PosMap.find i fw.ident_to_sym_ndx) (** Processes a worklist, threading in the framework. *) let rec worklist_process (wl: worklist) sfw: s_framework = match worklist_pop sfw wl with | None -> sfw (*done*) | Some ((ident, name, ccode), wl, candidates) -> let process_ndx ndx = ( let elf = (sfw |. sf_ef).elf in let pc = elf.e_symtab.(ndx).st_value in match code_of_sym_ndx elf ndx with | None -> ERR("Could not find symbol data for function symbol " ^ name) | Some ecode -> sfw >>> sf_ef ^%= add_log (DEBUG("Processing function: " ^ name)) >>> (fun sfw -> { sf = sfw; this_sym_ndx = ndx; this_ident = ident; label_to_vaddr = PosMap.empty; label_list = []; } ) >>> compare_code ccode ecode pc >>? mark_covered_fun_sym_ndx ndx ) in begin match candidates with | [] -> sfw >>> sf_ef ^%= add_log (ERROR("Skipping missing symbol " ^ name)) >>> worklist_process wl | [ndx] -> begin match process_ndx ndx with | OK(ffw) -> ffw >>> check_label_existence >>> check_label_unicity >>> (fun ffw -> worklist_process wl ffw.sf ) | ERR(s) -> sfw >>> sf_ef ^%= add_log (ERROR( "Unique candidate did not match: " ^ s )) >>> worklist_process wl end | ndxes -> (* Multiple candidates for one symbol *) let fws = filter_ok (List.map process_ndx ndxes) in begin match fws with | [] -> sfw >>> sf_ef ^%= add_log (ERROR("No matching candidate")) >>> worklist_process wl | [ffw] -> worklist_process wl ffw.sf | fws -> sfw >>> sf_ef ^%= add_log (ERROR( "Multiple matching candidates for symbol: " ^ name )) >>> worklist_process wl end end (** Compares a data symbol with its expected contents. Returns the updated framework as well as the size of the data matched. **) let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework) : (s_framework * int) or_err = let error = ERR("Reached end of data bitstring too soon") in let rec compare_data_aux l bs s (sfw: s_framework): (s_framework * int) or_err = match l with | [] -> OK(sfw, s) | d::l -> let sfw = if !debug then ( (sf_ef ^%= add_log (DEBUG(" " ^ string_of_init_data d))) sfw ) else sfw in begin match d with | Init_int8(i) -> ( bitmatch bs with | { j : 8 : int; bs : -1 : bitstring } -> if (z_int_lax i) land 0xFF = j then compare_data_aux l bs (s + 1) sfw else ERR("Wrong int8") | { _ } -> error ) | Init_int16(i) -> ( bitmatch bs with | { j : 16 : int; bs : -1 : bitstring } -> if (z_int_lax i) land 0xFFFF = j then compare_data_aux l bs (s + 2) sfw else ERR("Wrong int16") | { _ } -> error ) | Init_int32(i) -> ( bitmatch bs with | { j : 32 : int; bs : -1 : bitstring } -> if z_int32_lax i = j then compare_data_aux l bs (s + 4) sfw else ERR("Wrong int32") | { _ } -> error ) | Init_float32(f) -> ( bitmatch bs with | { j : 32 : int; bs : -1 : bitstring } -> if f = Int32.float_of_bits j then compare_data_aux l bs (s + 4) sfw else ERR("Wrong float32") | { _ } -> error ) | Init_float64(f) -> ( bitmatch bs with | { j : 64 : int; bs : -1 : bitstring } -> if f = Int64.float_of_bits j then compare_data_aux l bs (s + 8) sfw else ERR("Wrong float64") | { _ } -> error ) | Init_space(z) -> ( let space_size = z_int z in bitmatch bs with | { space : space_size * 8 : bitstring; bs : -1 : bitstring } -> if is_zeros space (space_size * 8) then compare_data_aux l bs (s + space_size) sfw else ERR("Wrong space " ^ string_of_int (z_int z) ^ " " ^ string_of_bitstring space) | { _ } -> error ) | Init_addrof(ident, ofs) -> ( bitmatch bs with | { vaddr : 32 : int; bs : -1 : bitstring } -> sfw >>> idmap_unify ident (Int32.sub vaddr (z_int32 ofs)) >>= compare_data_aux l bs (s + 4) | { _ } -> error ) end in compare_data_aux l bs 0 sfw (** Checks the data symbol table. *) let check_data_symtab ident sym_ndx size sfw = let elf = sfw.ef.elf in let symtab_ent_start = Int32.( add elf.e_shdra.(elf.e_symtab_sndx).sh_offset (Safe32.of_int (16 * sym_ndx)) ) in let sym = sfw.ef.elf.e_symtab.(sym_ndx) in let atom = Hashtbl.find sfw.atoms ident in let section = match atom.a_sections with | [s] -> s | _ -> Section_data true in sfw >>> ( if sym.st_size = Safe32.of_int size then id else ( sf_ef ^%= add_log (ERROR( "Incorrect symbol size (" ^ sym.st_name ^ "): expected " ^ string_of_int32i sym.st_size ^ ", counted: " ^ string_of_int size )) ) ) >>> check_st_bind atom sym >>> ( match sym.st_type with | STT_OBJECT -> id | STT_NOTYPE -> (sf_ef ^%= add_log (WARNING("Missing type for symbol " ^ sym.st_name)) ) | _ -> (sf_ef ^%= add_log (ERROR("Symbol should have type STT_OBJECT")) ) ) >>> ( if sym.st_other = 0 then id else (sf_ef ^%= add_log (ERROR("Symbol should have st_other set to 0")) ) ) >>> match_sections_name section elf.e_shdra.(sym.st_shndx).sh_name >>> (sf_ef ^%= add_range symtab_ent_start 16l 4 (Symtab_data(sym)) ) (** Checks all the program variables. *) let check_data (pv: (ident * unit globvar) list) (sfw: s_framework) : s_framework = let process_ndx ident ldata sfw ndx = let elf = sfw.ef.elf in let sym = elf.e_symtab.(ndx) in let sym_vaddr = sym.st_value in begin match bitstring_at_vaddr_nosize elf sym_vaddr with | None -> ERR("Could not find symbol data for data symbol " ^ sym.st_name) | Some(sym_bs, pofs, psize) -> let res = sfw >>> (sf_ef ^%= add_log (DEBUG("Processing data: " ^ sym.st_name))) >>> compare_data ldata sym_bs in begin match res with | ERR(s) -> ERR(s) | OK(sfw, size) -> let align = begin match (Hashtbl.find sfw.atoms ident).a_alignment with | None -> 0 | Some(a) -> a end in sfw.ef.chkd_data_syms.(ndx) <- true; sfw >>> ( if size = 0 then id (* These occupy no space, for now we just forget them *) else sf_ef ^%= add_range pofs (Safe32.of_int size) align (Data_symbol(sym)) ) >>> ( if not (is_well_aligned sym_vaddr align) then ( sf_ef ^%= add_log (ERROR( "Symbol not correctly aligned in the ELF file" )) ) else id ) >>> check_data_symtab ident ndx size >>> (fun sfw -> OK(sfw)) end end in let check_data_aux sfw ig = let (ident, gv) = ig in let init_data = gv.gvar_init in let ident_ndxes = PosMap.find ident sfw.ident_to_sym_ndx in (*print_endline ("Candidates: " ^ string_of_list id ", " (List.map (fun ndx -> fw.elf.e_symtab.(ndx).st_name) ident_ndxes));*) let results = List.map (process_ndx ident init_data sfw) ident_ndxes in let successes = filter_ok results in match successes with | [] -> sfw >>> sf_ef ^%= add_log (ERROR( "No matching data segment among candidates [" ^ (string_of_list (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_name) ", " ident_ndxes ) ^ "], Errors: [" ^ string_of_list (function OK(_) -> "" | ERR(s) -> s) ", " (List.filter (function ERR(_) -> true | _ -> false) results) ^ "]" )) | [sfw] -> sfw | fws -> sfw >>> sf_ef ^%= add_log (ERROR("Multiple matching data segments!")) in List.fold_left check_data_aux sfw (* Empty lists mean the symbol is external, no need for check *) (List.filter (fun (_, gv) -> gv.gvar_init <> []) pv) (** Checks that everything that has been assimiled as a stub during checks indeed looks like a stub. *) let check_stubs sfw = let check cond msg sfw = sfw >>> (if cond then id else (sf_ef ^%= add_log (ERROR(msg)))) in let check_eq msg a b = check (a = b) msg in let match_bools = check_eq "match_bools" in let match_ints = check_eq "match_ints" in let check_stub ident vaddr sfw = let fundef = List.find (fun (i, _) -> i = ident) sfw.program.prog_funct in let elf = sfw.ef.elf in let stub_ecode = from_some (code_at_vaddr elf vaddr 2) in let stub_offset = from_some (physical_offset_of_vaddr elf vaddr) in begin match fundef with | (_, External(EF_external(dest_ident, _) as ef)) -> let args = (ef_sig ef).sig_args in if List.mem Tfloat args then begin match stub_ecode with | CREQV(crbD, crbA, crbB) :: (* vaddr *) Bx(li, aa, lk) :: (* vaddr + 4 *) [] -> let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in begin match idmap_unify dest_ident dest_vaddr sfw with | ERR(s) -> sfw >>> (sf_ef ^%= add_log (ERROR( "Couldn't match stub, " ^ s ))) | OK(sfw) -> sfw >>> match_ints 6 crbD >>> match_ints 6 crbA >>> match_ints 6 crbB >>> match_bools false aa >>> match_bools false lk >>> (sf_ef ^%= add_range stub_offset 8l 4 (Stub(Hashtbl.find sfw.ident_to_name ident)) ) end | _ -> sfw >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) end else begin match stub_ecode with | CRXOR(crbD, crbA, crbB) :: (* vaddr *) Bx(li, aa, lk) :: (* vaddr + 4 *) [] -> let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in begin match idmap_unify dest_ident dest_vaddr sfw with | ERR(s) -> sfw >>> (sf_ef ^%= add_log (ERROR( "Couldn't match stub, " ^ s ))) | OK(sfw) -> sfw >>> match_ints 6 crbD >>> match_ints 6 crbA >>> match_ints 6 crbB >>> match_bools false aa >>> match_bools false lk >>> (sf_ef ^%= add_range stub_offset 8l 4 (Stub(Hashtbl.find sfw.ident_to_name ident)) ) end | _ -> sfw >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) end | _ -> failwith "Unexpected fundef in check_stubs, please report." end in PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw (** Read a .sdump file *) let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version let read_sdump file = let ic = open_in_bin file in try let magic = String.create (String.length sdump_magic_number) in really_input ic magic 0 (String.length sdump_magic_number); if magic <> sdump_magic_number then failwith "bad magic number"; let prog = (input_value ic: Asm.program) in let names = (input_value ic: (ident, string) Hashtbl.t) in let atoms = (input_value ic: (ident, C2C.atom_info) Hashtbl.t) in close_in ic; (prog, names, atoms) with | End_of_file -> close_in ic; Printf.eprintf "Truncated file %s\n" file; exit 2 | Failure msg -> close_in ic; Printf.eprintf "Corrupted file %s: %s\n" file msg; exit 2 (** Processes a .sdump file. *) let process_sdump efw sdump: e_framework = if !debug then print_endline ("Beginning reading " ^ sdump); let (prog, names, atoms) = read_sdump sdump in if !debug then print_endline "Constructing mapping from idents to symbol indices"; let ident_to_sym_ndx = Hashtbl.fold (fun ident name m -> match ndxes_of_sym_name efw.elf name with | [] -> m (* skip if missing *) | ndxes -> PosMap.add ident ndxes m ) names PosMap.empty in if !debug then print_endline "Constructing worklist"; let worklist_fundefs = List.filter (fun f -> match snd f with | Internal _ -> true | External _ -> false ) prog.prog_funct in let wl = List.map (fun f -> match f with | ident, Internal ccode -> (ident, Hashtbl.find names ident, ccode) | _, External _ -> failwith "IMPOSSIBRU!" ) worklist_fundefs in if !debug then print_endline "Beginning processing of the worklist"; efw >>> (fun efw -> { ef = efw; program = prog; ident_to_name = names; ident_to_sym_ndx = ident_to_sym_ndx; stub_ident_to_vaddr = PosMap.empty; atoms = atoms; } ) >>> worklist_process wl >>> (fun sfw -> if !debug then print_endline "Checking stubs"; sfw ) >>> check_stubs >>> (fun sfw -> if !debug then print_endline "Checking data"; sfw ) >>> check_data prog.prog_vars >>> (fun sfw -> sfw.ef) (** Returns true if [a, b] intersects [ofs, ofs + size - 1]. *) let intersect (a, b) ofs size: bool = let within (a, b) x = (a <= x) && (x <= b) in (within (a, b) ofs) || (within (ofs, Int32.(sub (add ofs size) 1l)) a) let string_of_range a b = "[0x" ^ Printf.sprintf "%08lx" a ^ " - 0x" ^ Printf.sprintf "%08lx" b ^ "]" (** Checks that the bits from [start] to [stop] in [bs] are zeroed. *) let is_padding bs start stop = let bs_start = start * 8 in let bs_length = (stop - start + 1) * 8 in is_zeros (Bitstring.subbitstring bs bs_start bs_length) bs_length (** This functions goes through the list of checked bytes, and tries to find padding in it. That is, it takes pairs of chunks in order, and adds a padding chunk in between if these conditions are met: - the second chunk needs to be aligned. - the difference between the two chunks is strictly less than the alignment. - the data in this space is zeroed. Otherwise, it fills holes with an Unknown chunk. Returns a framework where [chkd_bytes_list] is sorted and full. *) let check_padding efw = let elf = efw.elf in let sndxes = list_n elf.e_hdr.e_shnum in let matching_sections x y = string_of_list id ", " (List.map (fun ndx -> elf.e_shdra.(ndx).sh_name) (List.filter (fun ndx -> let shdr = elf.e_shdra.(ndx) in intersect (x, y) shdr.sh_offset shdr.sh_size ) sndxes ) ) in let matching_symbols x y = string_of_list id ", " (List.map (fun sym -> sym.st_name) (List.filter (fun sym -> if sym.st_shndx >= Array.length elf.e_shdra then false (* special section *) else match physical_offset_of_vaddr elf sym.st_value with | None -> false | Some(ofs) -> intersect (x, y) ofs sym.st_size ) (Array.to_list elf.e_symtab) ) ) in let unknown x y = Unknown( "\nSections: " ^ matching_sections x y ^ "\nSymbols: " ^ matching_symbols x y ) in (* check_padding_aux assumes a sorted list *) let rec check_padding_aux efw accu l = match l with | [] -> efw (* if there is only one chunk left, we add an unknown space between it and the end. *) | [(_, e, _, _) as h] -> let elf_size = Safe32.of_int ((Bitstring.bitstring_length efw.elf.e_bitstring) / 8) in let elf_end = Int32.sub elf_size 1l in if e = elf_end then { efw with chkd_bytes_list = List.rev (h :: accu); } else ( let start = Int32.add e 1l in { efw with chkd_bytes_list = List.rev ((start, elf_end, 0, unknown start elf_end) :: h :: accu); } ) | ((b1, e1, a1, n1) as h1) :: ((b2, e2, a2, n2) as h2) :: rest -> let pad_start = Int32.add e1 1l in let pad_stop = Int32.sub b2 1l in if pad_start = b2 (* if they are directly consecutive *) || Safe.(of_int32 b2 - of_int32 e1) > a2 (* or if they are too far away *) || not (is_padding efw.elf.e_bitstring (Safe32.to_int pad_start) (Safe32.to_int pad_stop)) then (* not padding *) if pad_start <= pad_stop then check_padding_aux efw ((pad_start, pad_stop, 0, unknown pad_start pad_stop) :: h1 :: accu) (h2 :: rest) else check_padding_aux efw (h1 :: accu) (h2 :: rest) else ( (* this is padding! *) check_padding_aux efw ((pad_start, pad_stop, 0, Padding) :: h1 :: accu) (h2 :: rest) ) in let sorted_chkd_bytes_list = List.fast_sort (fun (a, _, _, _) (b, _, _, _) -> Int32.compare a b) efw.chkd_bytes_list in check_padding_aux efw [] sorted_chkd_bytes_list (** Checks a boolean. *) let ef_checkb b msg = if b then id else add_log(ERROR(msg)) let check_elf_identification efw = let ei = efw.elf.e_hdr.e_ident in efw >>> ef_checkb (ei.ei_class = ELFCLASS32) "ELF class should be ELFCLASS32" >>> ef_checkb (ei.ei_data = ELFDATA2MSB || ei.ei_data = ELFDATA2LSB) "ELF should be MSB or LSB" >>> ef_checkb (ei.ei_version = EV_CURRENT) "ELF identification version should be EV_CURRENT" let check_elf_header efw: e_framework = let eh = efw.elf.e_hdr in efw >>> check_elf_identification >>> ef_checkb (eh.e_type = ET_EXEC) "ELF type should be ET_EXEC" >>> ef_checkb (eh.e_machine = EM_PPC) "ELF machine should be PPC" >>> ef_checkb (eh.e_version = EV_CURRENT) "ELF version should be EV_CURRENT" >>> add_range 0l 52l 0 ELF_header (* Header is always 52-bytes long *) (** Checks the index 0 of the symbol table. This index is reserved to hold special values. *) let check_sym_tab_zero efw = let elf = efw.elf in let sym0 = efw.elf.e_symtab.(0) in efw >>> ( if sym0.st_name = "" then id else add_log (ERROR("Symbol 0 should not have a name")) ) >>> ( if sym0.st_value = 0l then id else add_log (ERROR("Symbol 0 should have st_value = 0")) ) >>> ( if sym0.st_size = 0l then id else add_log (ERROR("Symbol 0 should have st_size = 0")) ) >>> ( if sym0.st_bind = STB_LOCAL then id else add_log (ERROR("Symbol 0 should have STB_LOCAL binding")) ) >>> ( if sym0.st_type = STT_NOTYPE then id else add_log (ERROR("Symbol 0 should have STT_NOTYPE type")) ) >>> ( if sym0.st_other = 0 then id else add_log (ERROR("Symbol 0 should have st_other = 0")) ) >>> ( if sym0.st_shndx = shn_UNDEF then id else add_log (ERROR("Symbol 0 should have st_shndx = SHN_UNDEF")) ) >>> add_range elf.e_shdra.(elf.e_symtab_sndx).sh_offset 16l 4 Zero_symbol (** If CompCert sections have been mapped to an ELF section whose name is not the same, we warn the user. *) let warn_sections_remapping efw = StringMap.fold (fun c_name e_name efw -> if c_name = e_name then efw else ( efw >>> add_log (WARNING( Printf.sprintf "Section %s has been re-mapped to %s by your linker script" c_name e_name )) ) ) efw.section_map efw let warn_sda_mapping efw = if IntMap.is_empty efw.sda_map then efw else ( IntMap.fold (fun r vaddr efw -> efw >>> add_log (WARNING( Printf.sprintf "SDA register %d has been mapped to virtual address 0x%lx by your linker script" r vaddr )) ) efw.sda_map efw ) let (>>=) li f = List.flatten (List.map f li) (** Returns the list of all strictly-ordered pairs of [[0; len - 1]] that don't satisfy f. *) let forall_sym (len: int) (f: 'a -> 'a -> bool): ('a * 'a) list = (list_n len) >>= fun x -> (list_ab (x + 1) (len - 1)) >>= fun y -> (if f x y then [] else [(x, y)]) let check_overlaps efw = let shdra = efw.elf.e_shdra in let intersect a asize b bsize = asize <> 0l && bsize <> 0l && ( let last x xsize = Int32.(sub (add x xsize) 1l) in let alast = last a asize in let blast = last b bsize in let within (a, b) x = (a <= x) && (x <= b) in (within (a, alast) b) || (within (b, blast) a) ) in match forall_sym (Array.length shdra) (fun i j -> let ai = shdra.(i) in let aj = shdra.(j) in (ai.sh_type = SHT_NOBITS) || (aj.sh_type = SHT_NOBITS) || (not (intersect ai.sh_offset ai.sh_size aj.sh_offset aj.sh_size)) ) with | [] -> efw | l -> List.fold_left (fun efw (i, j) -> let msg = Printf.sprintf "Sections %s and %s overlap" shdra.(i).sh_name shdra.(j).sh_name in add_log (ERROR(msg)) efw ) efw l (** Checks a whole ELF file according to a list of .sdump files. This never dumps anything, so it can be safely used when fuzz-testing even if the user accidentally enabled dumping options. *) let check_elf_nodump elf sdumps = let eh = elf.e_hdr in let nb_syms = Array.length elf.e_symtab in let section_strtab = elf.e_shdra.(eh.e_shstrndx) in let symtab_shdr = elf.e_shdra.(elf.e_symtab_sndx) in let symbol_strtab = elf.e_shdra.(Safe32.to_int symtab_shdr.sh_link) in let efw = { elf = elf; log = []; chkd_bytes_list = []; chkd_fun_syms = Array.make nb_syms false; chkd_data_syms = Array.make nb_syms false; section_map = StringMap.empty; sda_map = IntMap.empty; } >>> check_elf_header >>> add_range eh.e_phoff Safe.(to_int32 (eh.e_phnum * eh.e_phentsize)) 4 ELF_progtab >>> add_range eh.e_shoff Safe.(to_int32 (eh.e_shnum * eh.e_shentsize)) 4 ELF_shtab >>> add_range section_strtab.sh_offset section_strtab.sh_size 0 ELF_section_strtab >>> add_range symbol_strtab.sh_offset symbol_strtab.sh_size 0 ELF_symbol_strtab >>> check_sym_tab_zero in if !debug then print_endline "Done checking header, beginning processing of .sdumps"; (* Thread the framework through the processing of all .sdump files *) List.fold_left process_sdump efw sdumps (* check the padding in between identified byte chunks *) >>> check_padding (* warn if some CompCert sections have been remapped by the linker script *) >>> warn_sections_remapping (* warn if there exists non-empty overlapping sections *) >>> check_overlaps >>> warn_sda_mapping (** Checks a whole ELF file according to .sdump files. If requested, dump the calculated bytes mapping, so that it can be reused by the fuzzer. *) let check_elf_dump elffilename sdumps = if !debug then print_endline "Beginning ELF parsing"; let elf = read_elf elffilename in if !debug then print_endline "Beginning ELF checking"; let efw = check_elf_nodump elf sdumps in (* print the elfmap if requested *) if !print_elfmap then begin print_endline ( string_of_list (fun (a, b, align, r) -> string_of_range a b ^ " (" ^ string_of_int align ^ ") " ^ string_of_byte_chunk_desc r) "\n" efw.chkd_bytes_list ) end; (* dump the elfmap if requested *) if !dump_elfmap then begin let oc = open_out (elffilename ^ ".elfmap") in output_value oc efw.chkd_bytes_list; close_out oc end; (* indicate function symbols that have not been checked *) let miss_fun = List.filter (fun ndx -> let symtype = efw.elf.e_symtab.(ndx).st_type in symtype = STT_FUNC || symtype = STT_NOTYPE ) (filter_some (Array.to_list (Array.mapi (fun ndx b -> if b then None else Some(ndx)) efw.chkd_fun_syms ) ) ) in if !exhaustivity then begin match miss_fun with | [] -> () | _ -> print_endline "\nWARNING: the following function symbols do not appear in .sdump files."; print_endline ( string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_fun ); print_newline () end ; (* indicate data symbols that have not been checked *) let miss_data = List.filter (fun ndx -> let symtype = efw.elf.e_symtab.(ndx).st_type in symtype = STT_OBJECT || symtype = STT_NOTYPE ) (filter_some (Array.to_list (Array.mapi (fun ndx b -> if b then None else Some(ndx)) efw.chkd_data_syms ) ) ) in if !exhaustivity then begin match miss_data with | [] -> () | _ -> print_endline "WARNING: the following data symbols do not appear in .sdump files."; print_endline ( string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_data ); print_newline () end ; (* print diagnosis *) let worrysome = List.filter (function | ERROR(_) -> true | WARNING(_) -> true | DEBUG(_) -> false ) efw.log in let exists_unknown_chunk = List.exists (function (_, _, _, Unknown(_)) -> true | _ -> false) efw.chkd_bytes_list in begin match worrysome with | [] -> print_endline "\nEverything seems fine with this ELF."; if exists_unknown_chunk then begin print_endline ( "However, some parts of the ELF could not be identified." ^ if !print_elfmap then "" else " Use -printelfmap to see what was covered." ) end | _ -> if !debug then print_endline ( "DEBUG MODE: The following messages are actual problems." ); List.(iter (fun e -> match string_of_log_entry false e with | "" -> () | s -> print_endline s ) (rev efw.log) ) end