IntelHex.ml

   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
   9 let size_lookup = function `Eight -> 8 | `Sixteen -> 16
  10
  11 let zero size =
  12  let size = size_lookup size in
  13  Extracted.BitVector.zero (Extracted.Glue.matitanat_of_int size)
  14
  15 let int_of_vect v =
  16  Extracted.Glue.int_of_matitanat (Extracted.Arithmetic.nat_of_bitvector (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);;
  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
  22 let complement v = Extracted.BitVector.negation_bv (Extracted.Glue.matitanat_of_int 8) v
  23
  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
  35 let vect_of_int k n =
  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)
  39
  40 let from_word v =
  41  let {Extracted.Types.fst = fst ; snd = snd} =
  42   Extracted.Vector.vsplit (Extracted.Glue.matitanat_of_int 8)
  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
 286 (*prerr_string ("M(" ^ string_of_int address ^ "=" ^ string_of_int (int_of_vect (vect_of_int address `Sixteen)) ^ ")" ^ hex_string_of_vect code ^ " ");*)
 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 *)