[2778] | 1 | (************* Glue code ******************************) |
---|
| 2 | |
---|
| 3 | let ($) f x = f x |
---|
| 4 | let flip f a b = f b a |
---|
| 5 | |
---|
| 6 | type byte = Extracted.BitVector.byte |
---|
| 7 | type word = Extracted.BitVector.word |
---|
| 8 | |
---|
[2779] | 9 | let size_lookup = function `Eight -> 8 | `Sixteen -> 16 |
---|
[2778] | 10 | |
---|
| 11 | let zero size = |
---|
[2779] | 12 | let size = size_lookup size in |
---|
[2778] | 13 | Extracted.BitVector.zero (Extracted.Glue.matitanat_of_int size) |
---|
| 14 | |
---|
| 15 | let int_of_vect v = |
---|
[2780] | 16 | Extracted.Glue.int_of_matitanat (Extracted.Arithmetic.nat_of_bitvector (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);; |
---|
[2778] | 17 | |
---|
| 18 | (* CSC: can overflow!!! *) |
---|
| 19 | (* CSC: only works properly with bytes!!! *) |
---|
| 20 | let hex_string_of_vect v = Printf.sprintf "%0 2X" (int_of_vect v);; |
---|
| 21 | |
---|
[2780] | 22 | let complement v = Extracted.BitVector.negation_bv (Extracted.Glue.matitanat_of_int 8) v |
---|
[2778] | 23 | |
---|
[2779] | 24 | let divide_with_remainder x y = (x / y, x mod y) |
---|
| 25 | |
---|
| 26 | let rec nat_to_bv n k = |
---|
| 27 | match n with |
---|
| 28 | | Extracted.Nat.O -> Extracted.Vector.VEmpty |
---|
| 29 | | Extracted.Nat.S n' -> |
---|
| 30 | let res,modu = divide_with_remainder k 2 in |
---|
| 31 | Extracted.Vector.VCons (n', |
---|
| 32 | (if modu = 1 then Extracted.Bool.True else Extracted.Bool.False), |
---|
| 33 | nat_to_bv n' res) |
---|
| 34 | |
---|
[2778] | 35 | let vect_of_int k n = |
---|
[2780] | 36 | Extracted.Vector.reverse |
---|
| 37 | (Extracted.Glue.matitanat_of_int (size_lookup n)) |
---|
| 38 | (nat_to_bv (Extracted.Glue.matitanat_of_int (size_lookup n)) k) |
---|
[2778] | 39 | |
---|
| 40 | let from_word v = |
---|
| 41 | let {Extracted.Types.fst = fst ; snd = snd} = |
---|
[2779] | 42 | Extracted.Vector.vsplit (Extracted.Glue.matitanat_of_int 8) |
---|
[2778] | 43 | (Extracted.Glue.matitanat_of_int 8) v in |
---|
| 44 | fst,snd |
---|
| 45 | |
---|
| 46 | let half_add b1 b2 = |
---|
| 47 | let {Extracted.Types.fst = fst ; snd = snd} = |
---|
| 48 | Extracted.Arithmetic.half_add (Extracted.Glue.matitanat_of_int 8) b1 b2 in |
---|
| 49 | fst = Extracted.Bool.True, snd |
---|
| 50 | |
---|
| 51 | module WordMap : |
---|
| 52 | sig |
---|
| 53 | val find : word -> Extracted.BitVector.byte Extracted.BitVectorTrie.bitVectorTrie -> byte |
---|
| 54 | end = |
---|
| 55 | struct |
---|
| 56 | let find k m = Extracted.BitVectorTrie.lookup (Extracted.Glue.matitanat_of_int 16) k m (zero `Eight) |
---|
| 57 | end;; |
---|
| 58 | |
---|
| 59 | (************* Untrusted code ******************************) |
---|
| 60 | (* |
---|
| 61 | open BitVectors;; |
---|
| 62 | open ASM;; |
---|
| 63 | open Util;; |
---|
| 64 | open Parser;; |
---|
| 65 | open Printf;; |
---|
| 66 | |
---|
| 67 | exception WrongFormat of string |
---|
| 68 | *) |
---|
| 69 | |
---|
| 70 | type intel_hex_entry_type = |
---|
| 71 | Data |
---|
| 72 | | End |
---|
| 73 | | ExtendedSeg |
---|
| 74 | | ExtendedLinear |
---|
| 75 | ;; |
---|
| 76 | |
---|
| 77 | type intel_hex_entry = |
---|
| 78 | { |
---|
| 79 | record_length: byte; |
---|
| 80 | record_addr: word; |
---|
| 81 | record_type: intel_hex_entry_type; |
---|
| 82 | data_field: byte list; |
---|
| 83 | data_checksum: byte |
---|
| 84 | } |
---|
| 85 | ;; |
---|
| 86 | |
---|
| 87 | type intel_hex_format = intel_hex_entry list;; |
---|
| 88 | |
---|
| 89 | (* |
---|
| 90 | let hex_digit_of_char = |
---|
| 91 | function |
---|
| 92 | '0' -> 0 | '1' -> 1 | '2' -> 2 |
---|
| 93 | | '3' -> 3 | '4' -> 4 | '5' -> 5 |
---|
| 94 | | '6' -> 6 | '7' -> 7 | '8' -> 8 |
---|
| 95 | | '9' -> 9 | 'A' -> 10 | 'B' -> 11 |
---|
| 96 | | 'C' -> 12 | 'D' -> 13 | 'E' -> 14 |
---|
| 97 | | 'F' -> 15 | 'a' -> 10 | 'b' -> 11 |
---|
| 98 | | 'c' -> 12 | 'd' -> 13 | 'e' -> 14 |
---|
| 99 | | 'f' -> 15 | _ -> assert false |
---|
| 100 | |
---|
| 101 | let intel_hex_entry_type_of_int = |
---|
| 102 | function |
---|
| 103 | 0 -> Data |
---|
| 104 | | 1 -> End |
---|
| 105 | | 2 -> ExtendedSeg |
---|
| 106 | | 4 -> ExtendedLinear |
---|
| 107 | | _ -> assert false |
---|
| 108 | ;; |
---|
| 109 | *) |
---|
| 110 | |
---|
| 111 | let int_of_intel_hex_entry_type = |
---|
| 112 | function |
---|
| 113 | Data -> 0 |
---|
| 114 | | End -> 1 |
---|
| 115 | | ExtendedSeg -> 2 |
---|
| 116 | | ExtendedLinear -> 4 |
---|
| 117 | ;; |
---|
| 118 | |
---|
| 119 | (* |
---|
| 120 | let prs_nibble = |
---|
| 121 | prs_hex_digit >>= |
---|
| 122 | fun a -> return $ vect_of_int (hex_digit_of_char a) `Four |
---|
| 123 | ;; |
---|
| 124 | |
---|
| 125 | let prs_byte = |
---|
| 126 | prs_nibble >>= |
---|
| 127 | fun a -> prs_nibble >>= |
---|
| 128 | fun b -> return $ mk_byte a b |
---|
| 129 | ;; |
---|
| 130 | |
---|
| 131 | let prs_word = |
---|
| 132 | prs_byte >>= |
---|
| 133 | fun a -> prs_byte >>= |
---|
| 134 | fun b -> return $ mk_word a b |
---|
| 135 | ;; |
---|
| 136 | |
---|
| 137 | let prs_length = prs_byte;; |
---|
| 138 | let prs_data len = prs_exact len prs_byte |
---|
| 139 | let prs_checksum = prs_byte;; |
---|
| 140 | let prs_addr = prs_word;; |
---|
| 141 | |
---|
| 142 | let prs_type = |
---|
| 143 | prs_hex_digit >>= |
---|
| 144 | fun a -> prs_hex_digit >>= |
---|
| 145 | fun b -> |
---|
| 146 | let a_as_hex = hex_digit_of_char a in |
---|
| 147 | let b_as_hex = hex_digit_of_char b in |
---|
| 148 | (*CSC: is next line correct??? *) |
---|
| 149 | let total = a_as_hex + b_as_hex in |
---|
| 150 | return $ intel_hex_entry_type_of_int total |
---|
| 151 | *) |
---|
| 152 | |
---|
| 153 | let add_bytes v = |
---|
| 154 | let r = List.rev v in |
---|
| 155 | let rec aux (cry, bs) = |
---|
| 156 | function |
---|
| 157 | [] -> (cry, bs) |
---|
| 158 | | hd::tl -> |
---|
| 159 | aux (half_add hd bs) tl |
---|
| 160 | in |
---|
| 161 | aux (false, (vect_of_int 0 `Eight)) r |
---|
| 162 | |
---|
| 163 | let calculate_checksum hex_entry = |
---|
| 164 | let ty = (flip vect_of_int $ `Eight) $ int_of_intel_hex_entry_type hex_entry.record_type in |
---|
| 165 | let addr1,addr2 = from_word hex_entry.record_addr in |
---|
| 166 | let _, total = add_bytes (hex_entry.record_length :: addr1 :: addr2 :: ty :: hex_entry.data_field) in |
---|
| 167 | let _,total = half_add (vect_of_int 1 `Eight) $ complement total in |
---|
| 168 | total |
---|
| 169 | |
---|
| 170 | (* |
---|
| 171 | let checksum_valid hex_entry = |
---|
| 172 | let total = calculate_checksum hex_entry in |
---|
| 173 | hex_entry.data_checksum = total |
---|
| 174 | |
---|
| 175 | let prs_intel_hex_record = |
---|
| 176 | prs_char ':' >>= |
---|
| 177 | fun _ -> prs_length >>= |
---|
| 178 | fun b -> prs_addr >>= |
---|
| 179 | fun c -> prs_type >>= |
---|
| 180 | fun d -> prs_data (int_of_vect b) >>= |
---|
| 181 | fun e -> prs_checksum >>= |
---|
| 182 | fun f -> prs_eof >>= |
---|
| 183 | fun _ -> |
---|
| 184 | let entry = |
---|
| 185 | { record_length = b; |
---|
| 186 | record_addr = c; |
---|
| 187 | record_type = d; |
---|
| 188 | data_field = e; |
---|
| 189 | data_checksum = f } |
---|
| 190 | in |
---|
| 191 | if checksum_valid entry then |
---|
| 192 | return entry |
---|
| 193 | else |
---|
| 194 | prs_zero |
---|
| 195 | ;; |
---|
| 196 | |
---|
| 197 | let prs_intel_hex_format = |
---|
| 198 | prs_sep_by prs_intel_hex_record (prs_char '\n') |
---|
| 199 | ;; |
---|
| 200 | |
---|
| 201 | let intel_hex_format_of_string s = |
---|
| 202 | let chars = char_list_of_string s in |
---|
| 203 | match prs_intel_hex_format chars with |
---|
| 204 | [] -> None |
---|
| 205 | | (prs,_)::_ -> Some prs |
---|
| 206 | *) |
---|
| 207 | |
---|
| 208 | let string_of_intel_hex_entry entry = |
---|
| 209 | let b = Buffer.create 655536 in |
---|
| 210 | let length_string = hex_string_of_vect entry.record_length in |
---|
| 211 | let addr_string = Printf.sprintf "%04X" (int_of_vect entry.record_addr) in |
---|
| 212 | let checksum_string = Printf.sprintf "%02X" (int_of_vect entry.data_checksum) in |
---|
| 213 | let type_string = Printf.sprintf "%02d" (int_of_intel_hex_entry_type entry.record_type) in |
---|
| 214 | List.iter (Buffer.add_string b) |
---|
| 215 | [ |
---|
| 216 | ":"; length_string; addr_string; type_string |
---|
| 217 | ]; |
---|
| 218 | List.iter (fun e -> Buffer.add_string b (hex_string_of_vect e)) entry.data_field; |
---|
| 219 | Buffer.add_string b checksum_string; |
---|
| 220 | Buffer.contents b |
---|
| 221 | ;; |
---|
| 222 | |
---|
| 223 | let string_of_intel_hex_format f = |
---|
| 224 | let strs = List.map string_of_intel_hex_entry f in |
---|
| 225 | let rec aux = |
---|
| 226 | function |
---|
| 227 | [] -> "" |
---|
| 228 | | [e] -> e |
---|
| 229 | | hd::tl -> hd ^ "\n" ^ aux tl |
---|
| 230 | in |
---|
| 231 | aux strs |
---|
| 232 | |
---|
| 233 | (* |
---|
| 234 | let intel_hex_of_file path = |
---|
| 235 | let fd = open_in path in |
---|
| 236 | let rec aux () = |
---|
| 237 | match try Some (input_line fd) with End_of_file -> None with |
---|
| 238 | None -> [] |
---|
| 239 | | Some txt -> |
---|
| 240 | let read = prs_intel_hex_record (Parser.chars_of_string txt) in |
---|
| 241 | let read = |
---|
| 242 | match read with |
---|
| 243 | [x,[]] -> x |
---|
| 244 | | _ -> raise (WrongFormat txt) |
---|
| 245 | in |
---|
| 246 | read::aux () |
---|
| 247 | in |
---|
| 248 | aux () |
---|
| 249 | ;; |
---|
| 250 | |
---|
| 251 | let rec load_from mem addr = |
---|
| 252 | function |
---|
| 253 | [] -> mem |
---|
| 254 | | he::tl -> |
---|
| 255 | load_from (Physical.WordMap.add addr he mem) (snd (BitVectors.half_add addr (BitVectors.vect_of_int 1 `Sixteen))) tl |
---|
| 256 | ;; |
---|
| 257 | |
---|
| 258 | let process_intel_hex = |
---|
| 259 | let rec aux mem = |
---|
| 260 | function |
---|
| 261 | [] -> assert false |
---|
| 262 | | he::tl -> |
---|
| 263 | match he.record_type with |
---|
| 264 | End -> assert (tl = []); mem |
---|
| 265 | | Data -> aux (load_from mem he.record_addr he.data_field) tl |
---|
| 266 | | _ -> assert false |
---|
| 267 | in |
---|
| 268 | aux Physical.WordMap.empty |
---|
| 269 | ;; |
---|
| 270 | *) |
---|
| 271 | |
---|
| 272 | (* DPM: this needs some comment: |
---|
| 273 | We aim to extract code memory into segmented lists of bytes, with a maximum |
---|
| 274 | length (chunk_size). The code memory map has a fixed size (max_addressable) |
---|
| 275 | on the 8051. Further, the chunks we extract get segmented when we find an |
---|
| 276 | unitialized zone in the code memory. |
---|
| 277 | *) |
---|
| 278 | let export_code_memory chunk_size max_addressable code_mem = |
---|
| 279 | let rec aux chunk address start_address rbuff lbuff = |
---|
| 280 | if address = max_addressable then |
---|
| 281 | (start_address, List.rev rbuff)::lbuff |
---|
| 282 | else if chunk = 0 then |
---|
| 283 | aux chunk_size address address [] ((start_address, List.rev rbuff)::lbuff) |
---|
| 284 | else |
---|
| 285 | let code = WordMap.find (vect_of_int address `Sixteen) code_mem in |
---|
[2780] | 286 | (*prerr_string ("M(" ^ string_of_int address ^ "=" ^ string_of_int (int_of_vect (vect_of_int address `Sixteen)) ^ ")" ^ hex_string_of_vect code ^ " ");*) |
---|
[2778] | 287 | aux (chunk - 1) (address + 1) start_address (code::rbuff) lbuff |
---|
| 288 | in |
---|
| 289 | List.rev (aux chunk_size 0 0 [] []) |
---|
| 290 | ;; |
---|
| 291 | |
---|
| 292 | let clean_exported_code_memory = List.filter (fun x -> snd x <> []) |
---|
| 293 | ;; |
---|
| 294 | |
---|
| 295 | (* |
---|
| 296 | let calculate_data_checksum (record_length, record_addr, record_type, data_field) = |
---|
| 297 | let ty = (flip vect_of_int $ `Eight) $ int_of_intel_hex_entry_type record_type in |
---|
| 298 | let addr1,addr2 = from_word record_addr in |
---|
| 299 | let _, total = add_bytes (record_length :: addr1 :: addr2 :: ty :: data_field) in |
---|
| 300 | let _,total = half_add (vect_of_int 0 `Eight) $ complement total in |
---|
| 301 | total |
---|
| 302 | ;; |
---|
| 303 | *) |
---|
| 304 | |
---|
| 305 | let process_exported_code_memory = |
---|
| 306 | List.map (fun x -> |
---|
| 307 | let record_length = vect_of_int (List.length (snd x)) `Eight in |
---|
| 308 | let record_addr = vect_of_int (fst x) `Sixteen in |
---|
| 309 | let record_type = Data in |
---|
| 310 | let data_field = snd x in |
---|
| 311 | let temp_record = |
---|
| 312 | { record_length = record_length; |
---|
| 313 | record_addr = record_addr; |
---|
| 314 | record_type = record_type; |
---|
| 315 | data_field = data_field; |
---|
| 316 | data_checksum = zero `Eight |
---|
| 317 | } in |
---|
| 318 | { temp_record with data_checksum = calculate_checksum temp_record }) |
---|
| 319 | ;; |
---|
| 320 | |
---|
| 321 | let rec zeros len = |
---|
| 322 | if len = 0 then |
---|
| 323 | [] |
---|
| 324 | else |
---|
| 325 | vect_of_int 0 `Eight :: zeros (len - 1) |
---|
| 326 | |
---|
| 327 | let post_process_exported_code_memory intel_hex = |
---|
| 328 | let reversed = List.rev intel_hex in |
---|
| 329 | let rec aux hex = |
---|
| 330 | match hex with |
---|
| 331 | [] -> [] |
---|
| 332 | | he::tl -> |
---|
| 333 | if he.record_type = End then |
---|
| 334 | aux tl |
---|
| 335 | else if he.record_type = Data then |
---|
| 336 | if he.data_field = zeros (int_of_vect he.record_length) then |
---|
| 337 | aux tl |
---|
| 338 | else |
---|
| 339 | he::(aux tl) |
---|
| 340 | else |
---|
| 341 | tl |
---|
| 342 | in |
---|
| 343 | List.rev (aux reversed) |
---|
| 344 | |
---|
| 345 | let pack_exported_code_memory chunk_size max_addressable code_mem = |
---|
| 346 | let export = export_code_memory chunk_size max_addressable code_mem in |
---|
| 347 | let cleaned = clean_exported_code_memory export in |
---|
| 348 | let processed = process_exported_code_memory cleaned in |
---|
| 349 | let postprocessed = post_process_exported_code_memory processed in |
---|
| 350 | let end_buffer = |
---|
| 351 | [{ record_length = zero `Eight; |
---|
| 352 | record_addr = zero `Sixteen; |
---|
| 353 | record_type = End; |
---|
| 354 | data_field = []; |
---|
| 355 | data_checksum = vect_of_int 255 `Eight |
---|
| 356 | }] in |
---|
| 357 | postprocessed @ end_buffer |
---|
| 358 | ;; |
---|
| 359 | |
---|
| 360 | (* |
---|
| 361 | let file_of_intel_hex path fmt = |
---|
| 362 | let str_fmt = string_of_intel_hex_format fmt in |
---|
| 363 | let channel = open_out path in |
---|
| 364 | fprintf channel "%s\n" str_fmt; |
---|
| 365 | close_out channel |
---|
| 366 | ;; |
---|
| 367 | *) |
---|