Source file byte_pattern.ml

(*Generated by Lem from byte_pattern.lem.*)
open Lem_assert_extra
open Lem_basic_classes
open Lem_bool
open Lem_list
open Lem_maybe
open Lem_num
open Lem_string

open Byte_sequence
open Missing_pervasives
open Show

(** A byte pattern element can be undefined if it doesn't have a known fixed
    value. *)
type byte_pattern_element =  char option

(* TODO: replace with two byte sequences (one used as a mask) *)
type byte_pattern = byte_pattern_element list

(*val string_of_byte_pattern : byte_pattern -> string*)
let rec string_of_byte_pattern bp:string=
   (let parts = (Lem_list.map (fun maybe_b ->
    (match maybe_b with
      | None -> "--"
      | Some b -> hex_string_of_byte b
    )
  ) bp) in
  let (_, s) = (List.fold_left (fun (n, s) part ->
    let s =
      (if Nat_big_num.equal (Nat_big_num.modulus n( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 0)) && not (s = "") then
        s ^ (" " ^ part)
      else
        s ^ part)
    in
    ( Nat_big_num.add n( (Nat_big_num.of_int 1)), s)
  ) (( (Nat_big_num.of_int 0) : Nat_big_num.num), "") parts) in
  s)

(*val make_byte_pattern_revacc : byte_pattern -> list byte -> list bool -> byte_pattern*)
let rec make_byte_pattern_revacc revacc bytes cares:((char)option)list=
     ((match bytes with
          [] -> List.rev revacc
        | b :: bs -> (match cares with
                care :: more -> make_byte_pattern_revacc ((if not care then None else Some b) :: revacc) bs more
              | _ -> failwith "make_byte_pattern: unequal length"
              )
    ))

(*val make_byte_pattern : list byte -> list bool -> byte_pattern*)
let rec make_byte_pattern bytes cares:(byte_pattern_element)list=
     (make_byte_pattern_revacc [] bytes cares)

(*val byte_list_to_byte_pattern : list byte -> byte_pattern*)
let byte_list_to_byte_pattern bl:((char)option)list=
   (Lem_list.map (fun b -> Some b) bl)

(*val init_byte_pattern : natural -> byte_pattern*)
let init_byte_pattern len:((char)option)list=
   (Lem_list.replicate (Nat_big_num.to_int len) None)

(*val byte_pattern_length : byte_pattern -> natural*)
let byte_pattern_length bp:Nat_big_num.num=
   (Nat_big_num.of_int (List.length bp))

(*val relax_byte_pattern_revacc : byte_pattern -> byte_pattern -> list bool -> byte_pattern*)
let rec relax_byte_pattern_revacc revacc bytes cares:((char)option)list=
     ((match bytes with
          [] -> List.rev revacc
        | b :: bs -> (match cares with
                care :: more -> relax_byte_pattern_revacc ((if not care then None else b) :: revacc) bs more
              | _ -> failwith ("relax_byte_pattern: unequal length")
              )
    ))

(*val relax_byte_pattern : byte_pattern -> list bool -> byte_pattern*)
let rec relax_byte_pattern bytes cares:(byte_pattern_element)list=
     (relax_byte_pattern_revacc [] bytes cares)

type pad_fn = Nat_big_num.num -> char list

(*val concretise_byte_pattern' : list byte -> natural -> byte_pattern -> pad_fn -> list byte*)
let rec concretise_byte_pattern' rev_acc acc_pad bs pad:(char)list=
     ((match bs with
        [] ->
            let padding_bytes = (if Nat_big_num.greater acc_pad( (Nat_big_num.of_int 0)) then pad acc_pad else [])
            in List.rev ( List.rev_append (List.rev (List.rev padding_bytes)) rev_acc)
        | Some(b) :: more ->
            (* flush accumulated padding *)
            let padding_bytes = (if Nat_big_num.greater acc_pad( (Nat_big_num.of_int 0)) then pad acc_pad else [])
            in
            concretise_byte_pattern' (b :: ( List.rev_append (List.rev (List.rev padding_bytes)) rev_acc))( (Nat_big_num.of_int 0)) more pad
        | None :: more ->
            concretise_byte_pattern' rev_acc (Nat_big_num.add acc_pad( (Nat_big_num.of_int 1))) more pad
    ))

(*val concretise_byte_pattern : byte_pattern -> pad_fn -> byte_sequence*)
let rec concretise_byte_pattern pb pad:Byte_sequence_wrapper.byte_sequence=
     (
    (* TODO: don't use lists of bytes *)byte_sequence_of_byte_list (concretise_byte_pattern' []( (Nat_big_num.of_int 0)) pb pad))

(*val byte_option_matches_byte : maybe byte -> byte -> bool*)
let byte_option_matches_byte optb b:bool=
     ((match optb with
            None -> true
        |   Some some -> some = b
    ))

(*val byte_list_matches_pattern : byte_pattern -> list byte -> bool*)
let rec byte_list_matches_pattern pattern bytes:bool=
     ((match pattern with
        [] -> true
        | optbyte :: more -> (match bytes with
                [] -> false
                | abyte :: morebytes ->
                    byte_option_matches_byte optbyte abyte
                 && byte_list_matches_pattern more morebytes
            )
    ))

(*val append_to_byte_pattern_at_offset : natural -> byte_pattern -> byte_pattern -> byte_pattern*)
let append_to_byte_pattern_at_offset offset pat1 pat2:((char)option)list=
     (let pad_length = (Nat_big_num.sub_nat offset (Missing_pervasives.length pat1))
    in
    if Nat_big_num.less pad_length( (Nat_big_num.of_int 0)) then failwith "can't append at offset already used"
    else  List.rev_append (List.rev (List.rev_append (List.rev pat1) (Lem_list.replicate (Nat_big_num.to_int pad_length) None))) pat2)

(*val accum_pattern_possible_starts_in_one_byte_sequence : byte_pattern -> nat -> list byte -> nat -> natural -> list natural -> list natural*)
let rec accum_pattern_possible_starts_in_one_byte_sequence pattern pattern_len seq seq_len offset accum:(Nat_big_num.num)list=
     (
    (* let _ = Missing_pervasives.errs ("At offset " ^ (show offset) ^ "... ")
    in *)(match pattern with
        [] -> (* let _ = Missing_pervasives.errs ("terminating with hit (empty pattern)\n") in *)
            offset :: accum
        | bpe :: more_bpes -> (* nonempty, so check for nonempty seq *)
            (match seq with
                [] -> (*let _ = Missing_pervasives.errs ("terminating with miss (empty pattern)\n")
                    in *) accum (* ran out of bytes in the sequence, so no match *)
                | byte1 :: more_bytes -> let matched_this_byte =
                            (byte_option_matches_byte bpe byte1)
                       in
                       (* let _ = Missing_pervasives.errs ("Byte " ^ (show byte) ^ " matched " ^ (show byte_pattern) ^ "? " ^ (show matched_this_byte) ^ "; ")
                       in *)
                       let sequence_long_enough = (seq_len >= pattern_len)
                       in
                       (* let _ = Missing_pervasives.errs ("enough bytes remaining (" ^ (show seq_len) ^ ") to match rest of pattern (" ^ (show pattern_len) ^ ")? " ^ (show sequence_long_enough) ^ "; ")
                       in *)
                       let matched_here = (matched_this_byte && (sequence_long_enough &&
                        byte_list_matches_pattern more_bpes more_bytes))
                       in
                       (* let _ = Missing_pervasives.errs ("matched pattern anchored here? " ^ (show matched_this_byte) ^ "\n")
                       in *)
                       accum_pattern_possible_starts_in_one_byte_sequence
                           pattern pattern_len
                           more_bytes ( Nat_num.nat_monus seq_len 1)
                           ( Nat_big_num.add offset( (Nat_big_num.of_int 1)))
                           (if matched_here then offset :: accum else accum)
            )
    ))

(*val byte_pattern_of_byte_sequence : byte_sequence -> byte_pattern*)
let byte_pattern_of_byte_sequence seq:((char)option)list=
     (let l = (byte_list_of_byte_sequence seq) in
    Lem_list.map (fun b -> Some b) l)

(* Prefer using byte sequences when possible *)
(*val byte_pattern_to_byte_list : byte_pattern -> list byte*)
let byte_pattern_to_byte_list bp:(char)list=
   (Lem_list.map (fun maybe_b ->
    (match maybe_b with
      | Some b -> b
      | None -> failwith "byte_pattern_to_byte_sequence: attempt to read a masked byte"
    )
  ) bp)

(*val byte_pattern_to_byte_sequence : byte_pattern -> byte_sequence*)
let byte_pattern_to_byte_sequence bp:Byte_sequence_wrapper.byte_sequence=
   (let l = (byte_pattern_to_byte_list bp) in
  byte_sequence_of_byte_list l)

(*val byte_pattern_skip : natural -> byte_pattern -> byte_pattern*)
let rec byte_pattern_skip offset bp:((char)option)list=
   (if Nat_big_num.less offset( (Nat_big_num.of_int 0)) then
    failwith "byte_pattern_skip: cannot skip a negative number of bytes"
  else if Nat_big_num.equal offset( (Nat_big_num.of_int 0)) then
    bp
  else
    (match bp with
      | _ :: bp -> byte_pattern_skip ( Nat_big_num.sub_nat offset( (Nat_big_num.of_int 1))) bp
      | [] -> failwith "byte_pattern_skip: skipped past end"
    ))

(*val write_byte_pattern : byte_pattern -> natural -> byte_pattern -> byte_pattern*)
let write_byte_pattern bp offset sub_bp:((char)option)list=
   (if (listEqualBy (Lem.option_equal (=)) sub_bp []) then bp else
  let len = (List.length sub_bp) in
  let (prefix, bp) = (Lem_list.split_at (Nat_big_num.to_int offset) bp) in
  let (old, suffix) = (Lem_list.split_at len bp) in
  (* We don't want to change the byte pattern length *)
  let _ = (if (listEqualBy (Lem.option_equal (=)) suffix []) && not ((List.length old) = len) then failwith "write_byte_pattern: write past end" else ()) in 
  List.rev_append (List.rev (List.rev_append (List.rev prefix) sub_bp)) suffix)

(*val read_byte_pattern : byte_pattern -> natural -> natural -> byte_pattern*)
let read_byte_pattern bp offset len:((char)option)list=
   (Lem_list.take (Nat_big_num.to_int len) (Lem_list.drop (Nat_big_num.to_int offset) bp))