diff options
Diffstat (limited to 'checklink/Check.ml')
| -rw-r--r-- | checklink/Check.ml | 3216 |
1 files changed, 0 insertions, 3216 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml deleted file mode 100644 index 0e69ab72..00000000 --- a/checklink/Check.ml +++ /dev/null @@ -1,3216 +0,0 @@ -open Asm -open Asm_printers -open AST -open Bitstring_utils -open C2C -open Camlcoq -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 - -(** Whether to print the list of all symbols (function and data) that were not - found in .sdump files. *) -let list_missing = ref false - -(** CompCert Asm *) -type ccode = Asm.coq_function - -let print_debug s = - if !debug then print_endline (string_of_log_entry true (DEBUG(s))) - -(** Adds a log entry into the framework. *) -let add_log (entry: log_entry) (efw: e_framework): e_framework = - if !debug then print_endline ("--DEBUG-- " ^ 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)" - )) - ) - -(** Adapted from CompCert *) -let name_of_section_Linux: section_name -> string = function -| Section_text -> ".text" -| Section_data i -> if i then ".data" else "COMM" -| Section_small_data i -> if i then ".sdata" else ".sbss" -| Section_const i -> if i then ".rodata" else "COMM" -| Section_small_const i -> if i then ".sdata2" else "COMM" -| Section_string -> ".rodata" -| Section_literal -> ".rodata.cst8" -| Section_jumptable -> ".text" -| Section_user(s, wr, ex) -> s -| Section_debug_info -> ".debug_info" -| Section_debug_abbrev -> ".debug_abbrev" - -(** Adapted from CompCert *) -let name_of_section_Diab: section_name -> string = function -| Section_text -> ".text" -| Section_data i -> if i then ".data" else "COMM" -| 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 -| Section_debug_info -> ".debug_info" -| Section_debug_abbrev -> ".debug_abbrev" - -(** Taken from CompCert *) -let name_of_section: section_name -> string = - begin match Configuration.system with - | "linux" -> name_of_section_Linux - | "diab" -> name_of_section_Diab - | _ -> fatal "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 (value, conflicts) = StringMap.find c_name sfw.ef.section_map in - let expected = from_inferrable value in - if e_name = expected - then sfw - else ( - sfw - >>> (sf_ef |-- section_map) ^%= - StringMap.add c_name (value, StringSet.add e_name conflicts) - ) - with Not_found -> ( - sfw - >>> (sf_ef |-- section_map) ^%= - StringMap.add c_name (Inferred(e_name), StringSet.empty) - ) - -(** 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) - -(** 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. Otherwise, it filters out all symbols whose virtual - address does not match [vaddr]. -*) -let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework) - : s_framework or_err = - try ( - (* get the list of possible symbols for ident [k] *) - let id_ndxes = PosMap.find k sfw.ident_to_sym_ndx in - (* consider only the ones at the correct virtual address *) - match List.filter - (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_value = vaddr) - id_ndxes - with - | [] -> - (* no symbol has that virtual address *) - ERR( - Printf.sprintf - "Incoherent constraints for ident %s with value %s and candidates [%s]" - (Hashtbl.find sfw.ident_to_name k) - (string_of_int32 vaddr) - (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( - Printf.sprintf - "Missing ident: %s should be at vaddr: %s" - (Hashtbl.find sfw.ident_to_name k) - (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 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 = - fun ffw -> if cond then OK(ffw) else ERR(msg) -let check_eq (msg: string) (a: 'a) (b: 'a): checker = - check (a = b) msg -let match_bools a b = - check_eq ( - Printf.sprintf "match_bools %s %s" (string_of_bool a) (string_of_bool b) - ) a b -let match_ints a b = - check_eq ( - Printf.sprintf "match_ints %s %s" (string_of_int a) (string_of_int b) - ) a b -let match_int32s a b: checker = - check_eq ( - Printf.sprintf "match_int32s %s %s" (string_of_int32 a) (string_of_int32 b) - ) 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: 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: int32): checker = - let a = camlint_of_coqint (Floats.Float32.to_bits a) in - check_eq ( - Printf.sprintf "match_floats %s %s" (string_of_int32 a) (string_of_int32 b) - ) a b -let match_crbits cb eb = - let cb = num_crbit cb in - check_eq ( - Printf.sprintf "match_crbits %d %d" cb eb - ) cb eb -let match_iregs cr er = - let er = ireg_arr.(er) in - check_eq ( - Printf.sprintf "match_iregs %s %s" (string_of_ireg cr) (string_of_ireg er) - ) cr er -let match_fregs cr er = - let er = freg_arr.(er) in - check_eq ( - Printf.sprintf "match_fregs %s %s" (string_of_freg cr) (string_of_freg er) - ) cr 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): checker = fun ffw -> - let sfw = ffw |. ff_sf in - let efw = ffw |. ff_ef in - match cc with - | Cint (i) -> - let i = z_int32_lax i in - let msg = - Printf.sprintf "match_csts Cint %s %s" - (string_of_int32 i) - (string_of_int32 ec) - in - check_eq msg ec 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 - ERR("Csymbol_low " ^ string_of_list id ", " sym_names) - | _ -> - if candidates = vaddrs - then OK(ffw) - else OK( - 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 - ERR("Csymbol_high " ^ string_of_list id ", " sym_names) - | _ -> - if candidates = vaddrs - then OK(ffw) - else OK( - ffw - >>> ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) - ) - end - | Csymbol_sda (ident, i) -> - (* sda should be handled separately in places it occurs *) - ERR("Incorrect reference to near-data symbol " - ^ Hashtbl.find ffw.sf.ident_to_name ident) - | Csymbol_rel_low (ident, i) | Csymbol_rel_high (ident, i) -> - (* should be handled separately in places it occurs *) - ERR("Incorrect reference to far-data symbol " - ^ Hashtbl.find ffw.sf.ident_to_name ident) - -let match_z_int32 (cz: Z.t) (ei: int32) = - let cz = z_int32 cz in - check_eq ( - Printf.sprintf "match_z_int32 %s %s" (string_of_int32 cz) (string_of_int32 ei) - ) cz ei - -let match_z_int (cz: Z.t) (ei: int) = - let cz = z_int32 cz in - let ei = Safe32.of_int ei in - check_eq ( - Printf.sprintf "match_z_int %s %s" (string_of_int32i cz) (string_of_int32i ei) - ) cz ei - -(* [m] is interpreted as a bitmask, and checked against [ei]. *) -let match_mask (m: Z.t) (ei: int32) = - let m = z_int32_lax m in - check_eq ( - Printf.sprintf "match_mask %s %s" - (string_of_int32 m) - (string_of_int32 ei) - ) m ei - -(** Checks that the special register referred to in [spr] is [r]. *) -let match_spr (str: string) (r: int) (spr: bitstring): checker = fun ffw -> - bitmatch spr with - | { v:5; 0:5 } when v = r -> OK(ffw) - | { _ } -> ERR(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 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 - | { _ } -> - ERR("Ill-formed jump table") - ) - in - let elf = ffw.sf.ef.elf in - begin match bitstring_at_vaddr elf vaddr size with - | None -> ERR("No section for the jumptable") - | Some(bs, pofs, psize) -> - ffw - >>> match_jmptbl_aux lbllist bs - >>^ (ff_ef ^%= - add_range pofs psize 0 Jumptable - ) - end - -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_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) - | { _ } -> ERR("match_bo_bt") - -let match_bo_bf bo: checker = fun ffw -> - if match_bo_bf_bool bo - then OK(ffw) - else ERR("match_bo_bf") - -let match_bo_ctr bo: checker = fun ffw -> - bitmatch bo with - | { true:1; false:1; true:1; false:1; false:1 } -> OK(ffw) - | { _ } -> ERR("match_bo_ctr") - -(** Checks whether it is feasible that the position at offset [ofs] from the - CompCert symbol [ident] is situated at a relative address [addr] from - the SDA register [r]. This means that the following equation must hold: - [r] + addr = @ident + ofs - This allows us to determine what address [r] has to contain. If it is the - first such guess or if it matches previous expectations, it's fine. - Otherwise, there is a conflict that is reported in sda_map. -*) -let check_sda ident ofs r addr ffw: f_framework or_err = - let ofs = z_int32 ofs in - let check_sda_aux ndx: (int * f_framework) or_err = - let elf = ffw.sf.ef.elf in - let sym = elf.e_symtab.(ndx) in - let expected_addr = Safe32.(sym.st_value + ofs - addr) in - try - let r_addr = from_inferrable (IntMap.find r ffw.sf.ef.sda_map) in - if r_addr = expected_addr - then OK(ndx, ffw) - else ERR( - Printf.sprintf - "SDA register %d is expected to point both at 0x%lx and 0x%lx" - r r_addr expected_addr - ) - with Not_found -> - OK(ndx, - ffw >>> (ff_ef |-- sda_map) ^%= IntMap.add r (Inferred(expected_addr)) - ) - in - (* We might not know yet what symbols is the one for that ident *) - let sym_list = PosMap.find ident ffw.sf.ident_to_sym_ndx in - (* So we test all the candidates *) - let res = List.map check_sda_aux sym_list in - (* For now, we hope at most one matches *) - match filter_ok res with - | [] -> ERR("No satisfying SDA mapping, errors were: " ^ - string_of_list id ", " (filter_err res)) - | [(ndx, ffw)] -> OK( - ffw - (* We instantiate the relationship for that ident to the matching symbol *) - >>> (ff_sf |-- ident_to_sym_ndx) ^%= PosMap.add ident [ndx] - ) - | _ -> fatal "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: checker = fun fw -> - 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 current_instr = - "[" ^ string_of_int32 pc ^ "] " ^ string_of_instruction c ^ " - " ^ string_of_instr e in - let error = ERR("Non-matching instructions: " ^ current_instr) in - let fw = - if !debug - then (ff_ef ^%= add_log (DEBUG(current_instr))) fw - else fw - in - match c with - | Padd(rd, r1, r2) -> - begin match ecode with - | ADDx(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 - | 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 -> - 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 - | Paddi(rd, r1, Csymbol_sda(ident, ofs)) -> - begin match ecode with - | ADDI(rD, rA, simm) :: es -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts simm) - >>= recur_simpl - | _ -> error - end - | Paddis(rd, r1, Csymbol_rel_high(id, ofs)) -> - begin match cs with - | Paddi(rd', r1', Csymbol_rel_low(id', ofs')) :: cs - when id' = id && ofs' = ofs -> - begin match ecode with - | ADDIS(rD, rA, simm) :: ADDI(rD', rA', simm') :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1' rA' - >>= match_iregs rd' rD' - >>= check_sda id ofs rA - Int32.(add (shift_left (of_int simm) 16) (exts simm')) - >>= compare_code cs es (Int32.add 8l pc) - | _ -> error - end - | _ -> error - end - | Paddis(rd, r1, cst) -> - begin match ecode with - | ADDIS(rD, rA, simm) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_bools false oe - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pallocframe(sz, ofs) -> error - | Pandc(rd, r1, r2) -> - begin match ecode with - | ANDCx(rS, rA, rB, rc) :: es -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> error - end - | Pannot(ef, args) -> - OK(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 - OK(fw) - >>= lblmap_unify lbl lblvaddr - >>= match_bools false aa - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbctr sg -> - begin match ecode with - | BCCTRx(bo, bi, lk) :: es -> - OK(fw) - >>= match_bo_ctr bo - >>= match_ints 0 bi - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbctrl sg -> - begin match ecode with - | BCCTRx(bo, bi, lk) :: es -> - OK(fw) - >>= match_bo_ctr bo - >>= match_ints 0 bi - >>= match_bools true lk - >>= 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 -> - let lblvaddr = Int32.(add pc (mul 4l (exts bd))) in - OK(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 - OK(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, sg) -> - 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) - >>= match_bools false aa - >>= match_bools true lk - >>= recur_simpl - | _ -> error - end - | Pblr -> - begin match ecode with - | BCLRx(bo, bi, lk) :: es -> - OK(fw) - >>= match_bo_ctr bo - >>= match_ints 0 bi - >>= match_bools false lk - >>= recur_simpl - | _ -> error - end - | Pbs(ident, sg) -> - 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 - >>= 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 - OK(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 - OK(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 - | RLWINMx(rS0, rA0, sh, mb, me, rc0) :: - ADDIS (rD1, rA1, simm1) :: - LWZ (rD2, rA2, d2) :: - MTSPR (rS3, spr3) :: - BCCTRx(bo4, bi4, rc4) :: es -> - let tblvaddr = Int32.( - add (shift_left (Safe32.of_int simm1) 16) (exts d2) - ) in - let tblsize = Safe32.of_int (4 * List.length table) in - OK(fw) - >>= match_iregs GPR12 rA0 - >>= match_iregs reg rS0 - >>= match_ints sh 2 - >>= match_ints mb 0 - >>= match_ints me 29 - >>= match_bools false rc0 - >>= match_iregs GPR12 rA1 - >>= match_iregs GPR12 rD1 - >>= match_iregs GPR12 rA2 - >>= match_iregs GPR12 rD2 - >>= match_iregs GPR12 rS3 - >>= match_ctr spr3 - >>= match_bo_ctr bo4 - >>= match_ints 0 bi4 - >>= match_bools false rc4 - >>= match_jmptbl table tblvaddr tblsize - >>= compare_code cs es (Int32.add 20l pc) - | _ -> error - end - | Pbuiltin(ef, args, res) -> - begin match ef with - | 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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_ints crfD 0 - >>= match_bools false l - >>= match_iregs r1 rA - >>= match_csts cst (exts simm) - >>= recur_simpl - | _ -> error - end - | Pcntlzw(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 -> - OK(fw) - >>= match_crbits bd crbD - >>= match_crbits b1 crbA - >>= match_crbits b2 crbB - >>= 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 -> - 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 - | Pdivwu(rd, r1, r2) -> - begin match ecode with - | DIVWUx(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 - | 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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfabs(rd, r1) | Pfabss(rd, r1) -> - begin match ecode with - | FABSx(frD, frB, rc) :: es -> - OK(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 -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfadds(rd, r1, r2) -> - begin match ecode with - | FADDSx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfcmpu(r1, r2) -> - begin match ecode with - | FCMPU(crfD, frA, frB) :: es -> - OK(fw) - >>= match_crbits CRbit_0 crfD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= recur_simpl - | _ -> error - end - | Pfcti(rd, r1) -> - error - | Pfctiw(rd, r1) -> - begin match ecode with - | FCTIWx(frD0, frB0, rc0) :: es -> - OK(fw) - >>= match_fregs rd frD0 - >>= match_fregs r1 frB0 - >>= match_bools false rc0 - >>= 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) -> - begin match ecode with - | FDIVx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfdivs(rd, r1, r2) -> - begin match ecode with - | FDIVSx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfmake(rd, r1, r2) -> - error - | Pfmr(rd, r1) -> - 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 - | Pfmul(rd, r1, r2) -> - begin match ecode with - | FMULx(frD, frA, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfmuls(rd, r1, r2) -> - begin match ecode with - | FMULSx(frD, frA, frC, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frC - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfneg(rd, r1) | Pfnegs(rd, r1) -> - begin match ecode with - | FNEGx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfreeframe(sz, ofs) -> - error - | Pfrsp(rd, r1) -> - begin match ecode with - | FRSPx(frD, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfxdp(rd, r1) -> - error - | Pfsub(rd, r1, r2) -> - begin match ecode with - | FSUBx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pfsubs(rd, r1, r2) -> - begin match ecode with - | FSUBSx(frD, frA, frB, rc) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_fregs r1 frA - >>= match_fregs r2 frB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | 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 - >>^ (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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_fregs rd frD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plfd(rd, cst, r1) | Plfd_a(rd, cst, r1) -> - begin match ecode with - | LFD(frD, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frD - >>= match_csts cst (exts d) - >>= match_iregs r1 rA - >>= recur_simpl - | _ -> error - end - | Plfdx(rd, r1, r2) | Plfdx_a(rd, r1, r2) -> - begin match ecode with - | LFDX(frD, rA, rB) :: es -> - OK(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 8l with - | None -> - ERR("Floating point constant address is wrong") - | Some(bs, pofs, psize) -> - let f = - bitmatch bs with - | { f : 64 : int } -> f - in - OK(fw) - >>= (fun ffw -> - begin match section_at_vaddr elf vaddr with - | None -> ERR("No section at that virtual address") - | Some(sndx) -> - let section_name = elf.e_shdra.(sndx).sh_name in - OK( - ffw - >>> ( - ff_sf ^%= - match_sections_name literal_section section_name - ) - ) - end - ) - >>= match_iregs GPR12 rD0 - >>= match_iregs GPR0 rA0 - >>= match_fregs r1 frD1 - >>= match_floats c f - >>^ (ff_ef ^%= add_range pofs psize 8 (Float_literal(f))) - >>= match_iregs GPR12 rA1 - >>= continue - end - | _ -> error - end - | Plfis(r1, c) -> - begin match ecode with - | ADDIS(rD0, rA0, simm0) :: - LFS (frD1, rA1, d1) :: es -> - let vaddr = Int32.( - add (shift_left (Safe32.of_int simm0) 16) (exts d1) - ) in - if Int32.rem vaddr 4l <> 0l - then ERR("Float32 constants should be 4-byte aligned") - else - let elf = fw.sf.ef.elf in - let atom = Hashtbl.find fw.sf.atoms fw.this_ident in - let literal_section = - begin match atom.a_sections with - | [_; l; _] -> l - | _ -> Section_literal - end - in - let continue = compare_code cs es (Int32.add 8l pc) in - begin match bitstring_at_vaddr elf vaddr 4l with - | None -> - ERR("Floating point constant address is wrong") - | Some(bs, pofs, psize) -> - let f = - bitmatch bs with - | { f : 32 : int } -> f - in - OK(fw) - >>= (fun ffw -> - begin match section_at_vaddr elf vaddr with - | None -> ERR("No section at that virtual address") - | Some(sndx) -> - let section_name = elf.e_shdra.(sndx).sh_name in - OK( - ffw - >>> ( - ff_sf ^%= - match_sections_name literal_section section_name - ) - ) - end - ) - >>= match_iregs GPR12 rD0 - >>= match_iregs GPR0 rA0 - >>= match_fregs r1 frD1 - >>= match_floats32 c f - >>^ (ff_ef ^%= add_range pofs psize 4 (Float32_literal(f))) - >>= match_iregs GPR12 rA1 - >>= continue - end - | _ -> error - end - | Plfs(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | LFS(frD, rA, d) :: es -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= 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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Plwarx(rd, r1, r2) -> - begin match ecode with - | LWARX(rD, rA, rB):: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= 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 -> - OK(fw) - >>= match_iregs rd rD - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Plwz(rd, cst, r1) | Plwz_a(rd, cst, r1) -> - begin match ecode with - | LWZ(rD, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= 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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pmfcr rd -> - begin match ecode with - | MFCR (rD0) :: es -> - OK(fw) - >>= match_iregs rd rD0 - >>= recur_simpl - | _ -> error - end - | Pmfcrbit(rd, bit) -> - error - | Pmflr(r) -> - begin match ecode with - | MFSPR(rD, spr) :: es -> - OK(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) -> - OK(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 -> - OK(fw) - >>= match_iregs r1 rS - >>= match_ctr spr - >>= recur_simpl - | _ -> error - end - | Pmtlr(r1) -> - begin match ecode with - | MTSPR(rS, spr) :: es -> - OK(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 -> - OK(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 -> - 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 - | Pmulhw(rd, r1, r2) -> - begin match ecode with - | MULHWx(rD, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pmulhwu(rd, r1, r2) -> - begin match ecode with - | MULHWUx(rD, rA, rB, rc) :: es -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pnand(rd, r1, r2) -> - begin match ecode with - | NANDx(rS, rA, rB, rc) :: es -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_iregs r2 rB - >>= match_bools false rc - >>= recur_simpl - | _ -> error - end - | Pstb(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STB(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstb(rd, cst, r1) -> - begin match ecode with - | STB(rS, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstfd(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STFD(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfd(rd, cst, r1) | Pstfd_a(rd, cst, r1) -> - begin match ecode with - | STFD(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= 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 -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstfs(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STFS(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfs(rd, cst, r1) -> - begin match ecode with - | STFS(frS, rA, d) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= recur_simpl - | _ -> error - end - | Pstfsx(rd, r1, r2) -> - begin match ecode with - | STFSX(frS, rA, rB) :: es -> - OK(fw) - >>= match_fregs rd frS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Psth(rd, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STH(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Psth(rd, cst, r1) -> - begin match ecode with - | STH(rS, rA, d) :: es -> - OK(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 -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= 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, Csymbol_sda(ident, ofs), r1) -> - begin match ecode with - | STW(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= check_sda ident ofs rA (exts d) - >>= recur_simpl - | _ -> error - end - | Pstw(rd, cst, r1) | Pstw_a(rd, cst, r1) -> - begin match ecode with - | STW(rS, rA, d) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_csts cst (exts d) - >>= 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 -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= 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 - | Pstwcx_(rd, r1, r2) -> - begin match ecode with - | STWCX_(rS, rA, rB) :: es -> - OK(fw) - >>= match_iregs rd rS - >>= match_iregs r1 rA - >>= match_iregs r2 rB - >>= recur_simpl - | _ -> error - end - | Pstwux(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 -> - 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 - | Psubfe(rd, r1, r2) -> - begin match ecode with - | SUBFEx(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 - | 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 -> - OK(fw) - >>= match_iregs rd rD - >>= match_iregs r1 rA - >>= match_csts cst (exts simm) - >>= 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 -> - OK(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 -> - OK(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 -> - OK(fw) - >>= match_iregs rd rA - >>= match_iregs r1 rS - >>= match_csts cst (Safe32.of_int uimm) - >>= recur_simpl - | _ -> 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.fn_code 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( - Printf.sprintf - "Unique candidate for %s did not match: %s" - name - 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 for: " ^ name)) - >>> worklist_process wl - | [ffw] -> - worklist_process wl ffw.sf - | fws -> - sfw - >>> sf_ef ^%= - add_log (ERROR( - "Multiple matching candidates for: " ^ 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 camlint_of_coqint (Floats.Float32.to_bits f) = 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 camlint64_of_coqint (Floats.Float.to_bits f) = j - then compare_data_aux l bs (s + 8) sfw - else ERR("Wrong float64") - | { _ } -> error - ) - | Init_int64(i) -> ( - bitmatch bs with - | { j : 64 : int; bs : -1 : bitstring } -> - if z_int64 i = j - then compare_data_aux l bs (s + 8) sfw - else ERR("Wrong int64") - | { _ } -> 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; - OK(sfw) - >>= (fun sfw -> - if size = 0 - then OK(sfw) (* These occupy no space, for now we just forget them *) - else OK( - sfw - >>> sf_ef ^%= - add_range pofs (Safe32.of_int size) align (Data_symbol(sym)) - ) - ) - >>= (fun sfw -> - if not (is_well_aligned sym_vaddr align) - then ERR("Symbol not correctly aligned in the ELF file") - else OK(sfw) - ) - >>^ check_data_symtab ident ndx size - 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) - -(** Read a .sdump file *) - -let sdump_magic_number = "CompCertSDUMP" ^ Version.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 fatal "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 - -(** Split program definitions into functions and variables *) - -let split_prog_defs p = - let rec split fns vars = function - | [] -> (List.rev fns, List.rev vars) - | (id, Gfun fd) :: defs -> split ((id, fd) :: fns) vars defs - | (id, Gvar vd) :: defs -> split fns ((id, vd) :: vars) defs - in split [] [] p.prog_defs - -(** Processes a .sdump file. -*) -let process_sdump efw sdump: e_framework = - print_debug ("Beginning reading " ^ sdump); - let (prog, names, atoms) = read_sdump sdump in - let (prog_funct, prog_vars) = split_prog_defs prog in - print_debug ("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 - print_debug("Constructing worklist"); - let worklist_fundefs = - List.filter - (fun f -> - match snd f with - | Internal _ -> true - | External _ -> false - ) - prog_funct - in - let wl = - List.map - (fun f -> - match f with - | ident, Internal ccode -> (ident, Hashtbl.find names ident, ccode) - | _, External _ -> fatal "IMPOSSIBRU!" - ) - worklist_fundefs - in - print_debug("Beginning processing of the worklist"); - efw - >>> (fun efw -> - { ef = efw - ; program = prog - ; ident_to_name = names - ; ident_to_sym_ndx = ident_to_sym_ndx - ; atoms = atoms - } - ) - >>> worklist_process wl - >>> (fun sfw -> - print_debug "Checking data"; - sfw - ) - >>> check_data 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 - start <= stop && - 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 = - print_debug "Checking padding"; - 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 - (* First, let's mark it checked as a data symbol, to avoid warnings *) - efw.chkd_data_syms.(0) <- true; - 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 = - 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 - | Provided(e_name) -> - efw - | Inferred(e_name) -> - if c_name = e_name - then efw - else - begin - efw - >>> add_log (WARNING( - Printf.sprintf - "Detected linker script remapping: section %S -> %S" - c_name e_name - )) - end - else (* conflicts not empty *) - match e_name with - | Provided(e_name) -> - efw - >>> add_log (ERROR( - Printf.sprintf " - Conflicting remappings for section %s: - Specified: %s - Expected: %s" - c_name e_name (string_of_list id ", " (StringSet.elements conflicts)) - )) - | Inferred(e_name) -> - efw - >>> add_log (ERROR( - Printf.sprintf " - Conflicting remappings for section %s: - %s" - c_name (string_of_list id ", " (e_name :: (StringSet.elements conflicts))) - )) - ) - efw.section_map - efw - -let warn_sda_mapping efw = - print_debug "Checking SDA mappings"; - if IntMap.is_empty efw.sda_map - then efw - else ( - IntMap.fold - (fun r vaddr efw -> - match vaddr with - | Provided(_) -> efw - | Inferred(vaddr) -> - efw >>> add_log (WARNING( - Printf.sprintf - "This SDA register mapping was inferred: register r%u = 0x%lX" - 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 - -let check_unknown_chunks efw = - if - List.exists - (function (_, _, _, Unknown(_)) -> true | _ -> false) - efw.chkd_bytes_list - then add_log (WARNING( - "Some parts of the ELF file are unknown." ^ - (if !print_elfmap then "" else " Use -print-elfmap to see what was covered.") - )) efw - else efw - -let check_missed_symbols efw = - if not !exhaustivity - then efw - else - let chkd_syms_a = - Array.init - (Array.length efw.elf.e_symtab) - ( - fun ndx -> - match efw.elf.e_symtab.(ndx).st_type with - (* we only care about function and data symbols *) - | STT_SECTION | STT_FILE -> true - | STT_OBJECT | STT_FUNC | STT_NOTYPE | STT_UNKNOWN -> - (* checked as either a function or a data symbol *) - efw.chkd_fun_syms.(ndx) - || efw.chkd_data_syms.(ndx) - (* or part of the symbols we know are mising *) - || StringSet.mem efw.elf.e_symtab.(ndx).st_name efw.missing_syms - ) - in - let missed_syms_l = list_false_indices chkd_syms_a in - match missed_syms_l with - | [] -> efw - | _ -> - let symtab = efw.elf.e_symtab in - let symlist_names = string_of_list (fun ndx -> symtab.(ndx).st_name) " " in - let missed_funs = - List.filter (fun ndx -> symtab.(ndx).st_type = STT_FUNC) missed_syms_l in - let missed_data = - List.filter (fun ndx -> symtab.(ndx).st_type = STT_OBJECT) missed_syms_l in - let missed_unknown = - List.filter (fun ndx -> - match symtab.(ndx).st_type with - | STT_NOTYPE | STT_UNKNOWN -> true - | _ -> false - ) missed_syms_l in - if !list_missing - then - efw - >>> add_log (WARNING( - Printf.sprintf - " - The following function symbol(s) do not appear in .sdump files: - %s - The following data symbols do not appear in .sdump files: - %s - The following unknown type symbols do not appear in .sdump files: - %s" - (symlist_names missed_funs) - (symlist_names missed_data) - (symlist_names missed_unknown) - )) - else - efw - >>> add_log (WARNING( - Printf.sprintf - "%u function symbol(s), %u data symbol(s) and %u unknown type symbol(s) do not appear in .sdump files. Add -list-missing to list them." - (List.length missed_funs) - (List.length missed_data) - (List.length missed_unknown) - )) - -let print_diagnosis efw = - let (nb_err, nb_warn) = List.fold_left - (fun (e, w) -> function - | DEBUG(_) -> (e, w) - | ERROR(_) -> (e + 1, w) - | INFO(_) -> (e, w) - | WARNING(_) -> (e, w + 1) - ) - (0, 0) - efw.log - in - if !debug - then Printf.printf "\n\nFINAL LOG:\n\n"; - List.(iter - (fun e -> - match string_of_log_entry false e with - | "" -> () - | s -> print_endline s - ) - (rev efw.log) - ); - let plural n = if n > 1 then "s" else "" in - Printf.printf " SUMMARY: %d error%s, %d warning%s\n" - nb_err (plural nb_err) nb_warn (plural nb_warn); - efw - -let conf_file = ref (None: string option) - -let parse_conf filename = - let section_map = ref StringMap.empty in - let sda_map = ref IntMap.empty in - let missing_syms = ref StringSet.empty in - let ic = open_in filename in - try - while true - do - let line = input_line ic in - (* Test different patterns one by one, until one of them works *) - let rec match_line = function - | [] -> failwith (Printf.sprintf "Couldn't read configuration line: %s" line) - | try_match::rest -> - try try_match () - with Scanf.Scan_failure(_) -> match_line rest - in - (* an empty line is ignored *) - if line <> "" - then - match_line - (* a comment *) - [ (fun () -> - Scanf.sscanf line - "#%s" - (fun _ -> ()) - ) - (* a section remapping *) - ; (fun () -> - Scanf.sscanf line - "section %S -> %S" - (fun sfrom sto -> - if StringMap.mem sfrom !section_map - then failwith ( - Printf.sprintf - "Your configuration file contains multiple mappings for section %s" - sfrom - ) - else - section_map := - StringMap.add sfrom (Provided(sto), StringSet.empty) !section_map - ) - ) - (* a SDA mapping *) - ; (fun () -> - Scanf.sscanf line - "register r%u = %li" - (fun r addr -> - if IntMap.mem r !sda_map - then failwith ( - Printf.sprintf - "Your configuration file contains multiple SDA mappings for register %u" - r - ) - else - sda_map := IntMap.add r (Provided(addr)) !sda_map) - ) - (* a list of symbols supposed to be missing from the .sdump files *) - ; (fun () -> - Scanf.sscanf line - "external %s@\n" - (fun sym_list_s -> - let sym_list = Str.split (Str.regexp "[ \t]+") sym_list_s in - List.iter - (fun sym -> missing_syms := StringSet.add sym !missing_syms) - sym_list - ) - ) - ] - done; raise End_of_file (* unreachable, just to please the typer *) - with - | End_of_file -> (!section_map, !sda_map, !missing_syms) - -(** 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 (section_map, sda_map, missing_syms) = - match !conf_file with - | None -> (StringMap.empty, IntMap.empty, StringSet.empty) - | Some(filename) -> parse_conf filename - 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 = section_map - ; sda_map = sda_map - ; missing_syms = missing_syms - } - >>> 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 - print_debug "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 about inferred SDA registers *) - >>> warn_sda_mapping - (* warn about regions of the ELF file that could not be identified *) - >>> check_unknown_chunks - >>> check_missed_symbols - >>> print_diagnosis - -(** 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 = - print_debug "Beginning ELF parsing"; - let elf = read_elf elffilename in - print_debug "Beginning ELF checking"; - let efw = check_elf_nodump elf sdumps in - (* print the elfmap if requested *) - if !print_elfmap - then - begin - Printf.printf "\n\n%s\n\n\n" - (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 |