open Camlcoq
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 -> ".rodata"
| Section_small_const -> ".sdata2"
| Section_string -> ".rodata"
| Section_literal -> ".rodata.cst8"
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) -> s

(** Adapted 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" -> fatal "Unsupported CompCert configuration: macosx"
  | "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 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
      | { _ } ->
          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

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 (32 * 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
      | Pcntlz(r1, r2) ->
          begin match ecode with
          | CNTLZWx(rS, rA, rc) :: es ->
              OK(fw)
              >>= match_iregs r2    rS
              >>= match_iregs r1    rA
              >>= match_bools false rc
              >>= recur_simpl
          | _ -> error
          end
      | Pcreqv(bd, b1, b2) ->
          begin match ecode with
          | CREQV(crbD, crbA, crbB) :: es ->
              OK(fw)
              >>= match_crbits bd crbD
              >>= match_crbits b1 crbA
              >>= match_crbits b2 crbB
              >>= recur_simpl
          | _ -> error
          end
      | Pcror(bd, b1, b2) ->
          begin match ecode with
          | CROR(crbD, crbA, crbB) :: es ->
              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
      | Pstwxu(rd, r1, r2) ->
          begin match ecode with
          | STWUX(rS, rA, rB) :: es ->
              OK(fw)
              >>= match_iregs rd rS
              >>= match_iregs r1 rA
              >>= match_iregs r2 rB
              >>= recur_simpl
          | _ -> error
          end
      | Psubfc(rd, r1, r2) ->
          begin match ecode with
          | SUBFCx(rD, rA, rB, oe, rc) :: es ->
              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" ^ 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 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