Source file `byte_pattern_extra.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
(*Generated by Lem from byte_pattern_extra.lem.*)
open Lem_basic_classes
open Lem_string
open Lem_maybe
open Lem_num
open Lem_bool

open Byte_pattern
open Missing_pervasives
open Show

type byte_pattern_compare_result =
  | BytePatternMatch
  | BytePatternMismatch of (Nat_big_num.num * string)

let rec compare_byte_pattern' dict_Basic_classes_Eq_a dict_Show_Show_a offset core_bp binary_bp:byte_pattern_compare_result=
   ((match (core_bp, binary_bp) with
    | (_, []) ->
      BytePatternMatch
    | ((Some core_b)::core_bp, (Some binary_b)::binary_bp) ->
      if  dict_Basic_classes_Eq_a.isInequal_method core_b binary_b then
        let err_msg = ("compare_byte_pattern: mismatch at offset 0x" ^ ((hex_string_of_natural offset) ^ (": byte " ^ ((
  dict_Show_Show_a.show_method core_b) ^ (" vs. " ^ (
  dict_Show_Show_a.show_method binary_b)))))) in
        BytePatternMismatch (offset, err_msg)
      else
        compare_byte_pattern' 
  dict_Basic_classes_Eq_a dict_Show_Show_a ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) core_bp binary_bp
    | (_::core_bp, None::binary_bp) ->
      compare_byte_pattern' 
  dict_Basic_classes_Eq_a dict_Show_Show_a ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) core_bp binary_bp
    | (maybe_core_b::_, maybe_binary_b::_) ->
      let err_msg = ("compare_byte_pattern: mismatch at offset 0x" ^ ((hex_string_of_natural offset) ^ (": " ^ ((string_of_maybe 
  dict_Show_Show_a maybe_core_b) ^ (" vs. " ^ (string_of_maybe 
  dict_Show_Show_a maybe_binary_b)))))) in
      BytePatternMismatch (offset, err_msg)
    | (_, _) ->
      let err_msg = ("compare_byte_pattern: mismatch at offset 0x" ^ ((hex_string_of_natural offset) ^ ": length mismatch")) in
      BytePatternMismatch (offset, err_msg)
  ))

(*val compare_byte_pattern : byte_pattern -> byte_pattern -> byte_pattern_compare_result*)
let compare_byte_pattern:((char)option)list ->((char)option)list ->byte_pattern_compare_result=  (compare_byte_pattern' 
  instance_Basic_classes_Eq_var_dict instance_Show_Show_Missing_pervasives_byte_dict( (Nat_big_num.of_int 0)))

(*val print_byte_pattern_line' : natural -> natural -> byte_pattern -> unit*)
let rec print_byte_pattern_line' offset len bp:unit=
   (if Nat_big_num.equal len( (Nat_big_num.of_int 0)) then () else
  let (s, bp) = ((match bp with
    | [] -> ("  ", [])
    | maybe_b::bp ->
      let s = ((match maybe_b with
        | None -> "--"
        | Some b -> hex_string_of_byte b
      )) in
      (s, bp)
  )) in
  let s = (if Nat_big_num.equal (Nat_big_num.modulus offset( (Nat_big_num.of_int 2)))( (Nat_big_num.of_int 1)) && Nat_big_num.greater ( Nat_big_num.sub_nat len( (Nat_big_num.of_int 1)))( (Nat_big_num.of_int 0)) then s ^ " " else s) in
  let _ = (prerr_string s) in
  print_byte_pattern_line' ( Nat_big_num.add offset( (Nat_big_num.of_int 1))) ( Nat_big_num.sub_nat len( (Nat_big_num.of_int 1))) bp)

(*val print_byte_pattern_line : natural -> byte_pattern -> unit*)
let print_byte_pattern_line:Nat_big_num.num ->byte_pattern ->unit=  (print_byte_pattern_line'( (Nat_big_num.of_int 0)))

(*val fixed_hex_string_of_natural : natural -> natural -> string*)
let rec fixed_hex_string_of_natural len n:string=
     (if Nat_big_num.equal len( (Nat_big_num.of_int 0)) then ""
    else (fixed_hex_string_of_natural ( Nat_big_num.sub_nat len( (Nat_big_num.of_int 1))) ( Nat_big_num.div n( (Nat_big_num.of_int 16)))) ^ (Xstring.implode [Missing_pervasives.hex_char_of_nibble ( Nat_big_num.modulus n( (Nat_big_num.of_int 16)))]))

let print_byte_pattern_addr_size : Nat_big_num.num= ( (Nat_big_num.of_int 12))
let print_byte_pattern_line_size : Nat_big_num.num= ( (Nat_big_num.of_int 16))

(*val print_byte_pattern : natural -> byte_pattern -> unit*)
let rec print_byte_pattern start bp:unit=
   (if (Lem_list.listEqualBy (Lem.option_equal (=)) bp []) then () else
  let _ = (prerr_string ((fixed_hex_string_of_natural print_byte_pattern_addr_size start) ^ " ")) in
  let (line, bp) = (Lem_list.split_at (Nat_big_num.to_int print_byte_pattern_line_size) bp) in
  let _ = (print_byte_pattern_line print_byte_pattern_line_size line) in
  let _ = (prerr_string "\n") in
  print_byte_pattern ( Nat_big_num.add start print_byte_pattern_line_size) bp)

(*val print_two_byte_patterns : natural -> byte_pattern -> byte_pattern -> unit*)
let rec print_two_byte_patterns start bp1 bp2:unit=
   (if (Lem_list.listEqualBy (Lem.option_equal (=)) bp1 []) && (Lem_list.listEqualBy (Lem.option_equal (=)) bp2 []) then () else
  let was_bp1_empty = (Lem_list.listEqualBy (Lem.option_equal (=)) bp1 []) in (* If only bp1 is empty, print one extra line *)
  let _ = (prerr_string ((fixed_hex_string_of_natural print_byte_pattern_addr_size start) ^ " | ")) in
  let (line1, bp1) = (Lem_list.split_at (Nat_big_num.to_int print_byte_pattern_line_size) bp1) in
  let (line2, bp2) = (Lem_list.split_at (Nat_big_num.to_int print_byte_pattern_line_size) bp2) in
  let _ = (print_byte_pattern_line print_byte_pattern_line_size line1) in
  let _ = (prerr_string " | ") in
  let _ = (print_byte_pattern_line print_byte_pattern_line_size line2) in
  let _ = ((match compare_byte_pattern line2 line1 with
    | BytePatternMatch -> ()
    | BytePatternMismatch (_, err_msg) -> prerr_string " X" (* Missing_pervasives.errs (" " ^ err_msg) *)
  )) in
  let _ = (prerr_string "\n") in
  if was_bp1_empty then
    prerr_endline "             |                                         |                   […]                  "
  else
    print_two_byte_patterns ( Nat_big_num.add start print_byte_pattern_line_size) bp1 bp2)