Source file byte_pattern.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
(*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))