[122] | 1 | open BitVectors;; |
---|
| 2 | open ASM;; |
---|
[128] | 3 | open Util;; |
---|
[130] | 4 | open Parser;; |
---|
[122] | 5 | |
---|
| 6 | type intel_hex_entry_type = |
---|
| 7 | Data |
---|
| 8 | | End |
---|
| 9 | | ExtendedSeg |
---|
| 10 | | ExtendedLinear |
---|
[130] | 11 | ;; |
---|
[122] | 12 | |
---|
| 13 | type intel_hex_entry = |
---|
| 14 | { |
---|
[133] | 15 | record_length: nibble * nibble; |
---|
| 16 | record_addr: nibble * nibble * nibble * nibble; |
---|
[122] | 17 | record_type: intel_hex_entry_type; |
---|
[133] | 18 | data_field: nibble list; |
---|
| 19 | data_checksum: nibble * nibble |
---|
[130] | 20 | } |
---|
| 21 | ;; |
---|
[122] | 22 | |
---|
[130] | 23 | type intel_hex_format = intel_hex_entry list;; |
---|
[123] | 24 | |
---|
[130] | 25 | let hex_digit_of_char = |
---|
[128] | 26 | function |
---|
| 27 | '0' -> 0 | '1' -> 1 | '2' -> 2 |
---|
| 28 | | '3' -> 3 | '4' -> 4 | '5' -> 5 |
---|
| 29 | | '6' -> 6 | '7' -> 7 | '8' -> 8 |
---|
| 30 | | '9' -> 9 | 'A' -> 10 | 'B' -> 11 |
---|
| 31 | | 'C' -> 12 | 'D' -> 13 | 'E' -> 14 |
---|
[130] | 32 | | 'F' -> 15 | _ -> assert false |
---|
[128] | 33 | |
---|
[130] | 34 | let vect_of_hex_string s size = |
---|
| 35 | let int_of_hex_string h = |
---|
| 36 | let rec aux l p = |
---|
| 37 | match l with |
---|
| 38 | [] -> 0 |
---|
| 39 | | hd::tl -> |
---|
| 40 | hex_digit_of_char hd * p + aux tl (p * 16) |
---|
| 41 | in |
---|
| 42 | aux (List.rev $ char_list_of_string h) 1 |
---|
[128] | 43 | in |
---|
[130] | 44 | let i_str = int_of_hex_string s in |
---|
| 45 | vect_of_int i_str size |
---|
| 46 | ;; |
---|
[128] | 47 | |
---|
| 48 | let hex_string_of_vect v = |
---|
[130] | 49 | let hex_string_of_int i = |
---|
| 50 | let digit_lookup = |
---|
| 51 | function |
---|
| 52 | 0 -> "0" | 1 -> "1" | 2 -> "2" |
---|
| 53 | | 3 -> "3" | 4 -> "4" | 5 -> "5" |
---|
| 54 | | 6 -> "6" | 7 -> "7" | 8 -> "8" |
---|
| 55 | | 9 -> "9" | 10 -> "A" | 11 -> "B" |
---|
| 56 | | 12 -> "C" | 13 -> "D" | 14 -> "E" |
---|
| 57 | | 15 -> "F" | _ -> assert false in |
---|
[128] | 58 | |
---|
[130] | 59 | let rec aux i = |
---|
| 60 | if i < 16 then |
---|
| 61 | digit_lookup i |
---|
| 62 | else |
---|
| 63 | let div = i / 16 in |
---|
| 64 | let rem = i mod 16 in |
---|
| 65 | aux div ^ digit_lookup rem |
---|
| 66 | in |
---|
| 67 | aux i |
---|
| 68 | in |
---|
| 69 | let vect_int = int_of_vect v in |
---|
| 70 | hex_string_of_int vect_int |
---|
| 71 | ;; |
---|
| 72 | |
---|
| 73 | let intel_hex_entry_type_of_int = |
---|
| 74 | function |
---|
| 75 | 0 -> Data |
---|
| 76 | | 1 -> End |
---|
| 77 | | 2 -> ExtendedSeg |
---|
| 78 | | 4 -> ExtendedLinear |
---|
| 79 | | _ -> assert false |
---|
| 80 | ;; |
---|
| 81 | |
---|
[131] | 82 | let int_of_intel_hex_type = |
---|
| 83 | function |
---|
| 84 | Data -> 0 |
---|
| 85 | | End -> 1 |
---|
| 86 | | ExtendedSeg -> 2 |
---|
| 87 | | ExtendedLinear -> 4 |
---|
| 88 | ;; |
---|
| 89 | |
---|
[130] | 90 | let prs_length = |
---|
| 91 | prs_hex_digit >>= |
---|
| 92 | fun a -> prs_hex_digit >>= |
---|
[133] | 93 | fun b -> return (vect_of_hex_string (String.make 1 a) `Four, |
---|
| 94 | vect_of_hex_string (String.make 1 b) `Four) |
---|
[130] | 95 | ;; |
---|
| 96 | |
---|
| 97 | let prs_addr = |
---|
| 98 | prs_hex_digit >>= |
---|
| 99 | fun a -> prs_hex_digit >>= |
---|
| 100 | fun b -> prs_hex_digit >>= |
---|
| 101 | fun c -> prs_hex_digit >>= |
---|
[133] | 102 | fun d -> return $ (vect_of_hex_string (String.make 1 a) `Four, |
---|
| 103 | vect_of_hex_string (String.make 1 b) `Four, |
---|
| 104 | vect_of_hex_string (String.make 1 c) `Four, |
---|
| 105 | vect_of_hex_string (String.make 1 d) `Four) |
---|
[130] | 106 | ;; |
---|
| 107 | |
---|
| 108 | let prs_type = |
---|
| 109 | prs_hex_digit >>= |
---|
| 110 | fun a -> prs_hex_digit >>= |
---|
| 111 | fun b -> |
---|
| 112 | let a_as_hex = hex_digit_of_char a in |
---|
| 113 | let b_as_hex = hex_digit_of_char b in |
---|
| 114 | let total = a_as_hex + b_as_hex in |
---|
| 115 | return $ intel_hex_entry_type_of_int total |
---|
| 116 | |
---|
| 117 | let prs_data len = |
---|
| 118 | prs_exact len $ prs_hex_digit >>= |
---|
| 119 | fun a -> |
---|
| 120 | let a_as_strs = List.map (String.make 1) a in |
---|
[133] | 121 | let byte_data = List.map (fun x -> vect_of_hex_string x `Four) a_as_strs in |
---|
[130] | 122 | return $ byte_data |
---|
| 123 | ;; |
---|
| 124 | |
---|
| 125 | let prs_checksum = |
---|
| 126 | prs_hex_digit >>= |
---|
| 127 | fun a -> prs_hex_digit >>= |
---|
[133] | 128 | fun b -> return (vect_of_hex_string (String.make 1 a) `Four, |
---|
| 129 | vect_of_hex_string (String.make 1 b) `Four) |
---|
[130] | 130 | ;; |
---|
| 131 | |
---|
| 132 | let prs_intel_hex_record = |
---|
| 133 | prs_char ':' >>= |
---|
| 134 | fun a -> prs_length >>= |
---|
| 135 | fun b -> prs_addr >>= |
---|
| 136 | fun c -> prs_type >>= |
---|
| 137 | fun d -> |
---|
| 138 | let (l_u_b, l_l_b) = b in |
---|
[133] | 139 | let len = int_of_vect (mk_byte l_u_b l_l_b) in |
---|
[132] | 140 | prs_data (2 * len) >>= |
---|
[130] | 141 | fun e -> prs_checksum >>= |
---|
| 142 | fun f -> |
---|
| 143 | return $ { |
---|
| 144 | record_length = b; |
---|
| 145 | record_addr = c; |
---|
| 146 | record_type = d; |
---|
| 147 | data_field = e; |
---|
| 148 | data_checksum = f |
---|
| 149 | } |
---|
| 150 | ;; |
---|
| 151 | |
---|
| 152 | let prs_intel_hex_format = |
---|
| 153 | prs_sep_by prs_intel_hex_record (prs_char '\n') |
---|
| 154 | ;; |
---|
| 155 | |
---|
| 156 | let intel_hex_format_of_string s = |
---|
| 157 | let chars = char_list_of_string s in |
---|
| 158 | match prs_intel_hex_format chars with |
---|
| 159 | [] -> None |
---|
| 160 | | (prs,_)::_ -> Some prs |
---|
| 161 | |
---|
[123] | 162 | let string_of_intel_hex_entry entry = |
---|
| 163 | let record_length_l, record_length_r = entry.record_length in |
---|
[130] | 164 | let record_addr_1, record_addr_2, record_addr_3, record_addr_4 = entry.record_addr in |
---|
[123] | 165 | let data_checksum_l, data_checksum_r = entry.data_checksum in |
---|
| 166 | let length_string = hex_string_of_vect record_length_l ^ |
---|
| 167 | hex_string_of_vect record_length_l in |
---|
[130] | 168 | let addr_string = hex_string_of_vect record_addr_1 ^ |
---|
| 169 | hex_string_of_vect record_addr_2 ^ |
---|
| 170 | hex_string_of_vect record_addr_3 ^ |
---|
| 171 | hex_string_of_vect record_addr_4 in |
---|
[123] | 172 | let checksum_string = hex_string_of_vect data_checksum_l ^ |
---|
| 173 | hex_string_of_vect data_checksum_r in |
---|
| 174 | let type_string = |
---|
| 175 | match entry.record_type with |
---|
| 176 | Data -> "00" |
---|
| 177 | | End -> "01" |
---|
| 178 | | ExtendedSeg -> "02" |
---|
| 179 | | ExtendedLinear -> "04" in |
---|
| 180 | let data_string = String.concat "" (List.map hex_string_of_vect entry.data_field) in |
---|
[130] | 181 | ":" ^ length_string ^ addr_string ^ type_string ^ data_string ^ checksum_string |
---|
| 182 | ;; |
---|
| 183 | |
---|
| 184 | let string_of_intel_hex_format f = |
---|
| 185 | let strs = List.map string_of_intel_hex_entry f in |
---|
| 186 | let rec aux = |
---|
| 187 | function |
---|
| 188 | [] -> "" |
---|
| 189 | | [e] -> e |
---|
| 190 | | hd::tl -> hd ^ "\n" ^ aux tl |
---|
| 191 | in |
---|
| 192 | aux strs |
---|
[131] | 193 | |
---|
| 194 | let add_bytes v = |
---|
| 195 | let r = List.rev v in |
---|
| 196 | let rec aux (cry, bs) = |
---|
| 197 | function |
---|
| 198 | [] -> (cry, bs) |
---|
| 199 | | hd::tl -> |
---|
[135] | 200 | aux (half_add hd bs) tl |
---|
[131] | 201 | in |
---|
[134] | 202 | aux (false, (vect_of_int 0 `Eight)) r |
---|
[131] | 203 | |
---|
[134] | 204 | (* DPM: Non exhaustive pattern as we always check list length is even! *) |
---|
| 205 | let rec lift_to_bytes = |
---|
| 206 | function |
---|
| 207 | [] -> [] |
---|
| 208 | | hd::hd'::tl -> |
---|
| 209 | (mk_byte hd hd')::(lift_to_bytes tl) |
---|
| 210 | |
---|
[131] | 211 | let checksum_valid hex_entry = |
---|
| 212 | if List.length hex_entry.data_field mod 2 <> 0 then |
---|
| 213 | false |
---|
| 214 | else |
---|
| 215 | let chk_1, chk_2 = hex_entry.data_checksum in |
---|
[134] | 216 | let checksum = mk_byte chk_1 chk_2 in |
---|
| 217 | let len_1, len_2 = hex_entry.record_length in |
---|
| 218 | let ln_total = mk_byte len_1 len_2 in |
---|
| 219 | let ty_total = (flip vect_of_int $ `Eight) $ int_of_intel_hex_type hex_entry.record_type in |
---|
[131] | 220 | let adr_1, adr_2, adr_3, adr_4 = hex_entry.record_addr in |
---|
[134] | 221 | let ad_total1 = mk_byte adr_1 adr_2 in |
---|
| 222 | let ad_total2 = mk_byte adr_3 adr_4 in |
---|
| 223 | let _, dt_total = add_bytes <*> lift_to_bytes $ hex_entry.data_field in |
---|
| 224 | let _, total = add_bytes [ln_total; ad_total1; ad_total2; ty_total; dt_total] in |
---|
| 225 | let _,total = half_add (vect_of_int 1 `Eight) $ complement total in |
---|
| 226 | checksum = total |
---|
[133] | 227 | |
---|
| 228 | (* DPM: Debug |
---|
[135] | 229 | let tot = complement <*> snd $ add_bytes [vect_of_int 2 `Eight; vect_of_int 0 `Eight; vect_of_int 0 `Eight; vect_of_int 4 `Eight; vect_of_int 255 `Eight; vect_of_int 255 `Eight];; |
---|
| 230 | let Some entry = intel_hex_format_of_string ":02000004FFFFFC";; |
---|
[133] | 231 | checksum_valid $ List.hd entry;; |
---|
| 232 | *) |
---|