1 (************* Glue code ******************************)
6 type byte = Extracted.BitVector.byte
7 type word = Extracted.BitVector.word
9 let size_lookup = function `Eight -> 8 | `Sixteen -> 16
12 let size = size_lookup size in
13 Extracted.BitVector.zero (Extracted.Glue.matitanat_of_int size)
16 Extracted.Glue.int_of_matitanat (Extracted.Arithmetic.nat_of_bitvector (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);;
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);;
22 let complement v = Extracted.BitVector.negation_bv (Extracted.Glue.matitanat_of_int 8) v
24 let divide_with_remainder x y = (x / y, x mod y)
26 let rec nat_to_bv n k =
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),
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)
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
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
53 val find : word -> Extracted.BitVector.byte Extracted.BitVectorTrie.bitVectorTrie -> byte
56 let find k m = Extracted.BitVectorTrie.lookup (Extracted.Glue.matitanat_of_int 16) k m (zero `Eight)
59 (************* Untrusted code ******************************)
67 exception WrongFormat of string
70 type intel_hex_entry_type =
77 type intel_hex_entry =
81 record_type: intel_hex_entry_type;
82 data_field: byte list;
87 type intel_hex_format = intel_hex_entry list;;
90 let hex_digit_of_char =
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
101 let intel_hex_entry_type_of_int =
106 | 4 -> ExtendedLinear
111 let int_of_intel_hex_entry_type =
116 | ExtendedLinear -> 4
122 fun a -> return $ vect_of_int (hex_digit_of_char a) `Four
127 fun a -> prs_nibble >>=
128 fun b -> return $ mk_byte a b
133 fun a -> prs_byte >>=
134 fun b -> return $ mk_word a b
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;;
144 fun a -> prs_hex_digit >>=
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
154 let r = List.rev v in
155 let rec aux (cry, bs) =
159 aux (half_add hd bs) tl
161 aux (false, (vect_of_int 0 `Eight)) r
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
171 let checksum_valid hex_entry =
172 let total = calculate_checksum hex_entry in
173 hex_entry.data_checksum = total
175 let prs_intel_hex_record =
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 >>=
191 if checksum_valid entry then
197 let prs_intel_hex_format =
198 prs_sep_by prs_intel_hex_record (prs_char '\n')
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
205 | (prs,_)::_ -> Some prs
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)
216 ":"; length_string; addr_string; type_string
218 List.iter (fun e -> Buffer.add_string b (hex_string_of_vect e)) entry.data_field;
219 Buffer.add_string b checksum_string;
223 let string_of_intel_hex_format f =
224 let strs = List.map string_of_intel_hex_entry f in
229 | hd::tl -> hd ^ "\n" ^ aux tl
234 let intel_hex_of_file path =
235 let fd = open_in path in
237 match try Some (input_line fd) with End_of_file -> None with
240 let read = prs_intel_hex_record (Parser.chars_of_string txt) in
244 | _ -> raise (WrongFormat txt)
251 let rec load_from mem addr =
255 load_from (Physical.WordMap.add addr he mem) (snd (BitVectors.half_add addr (BitVectors.vect_of_int 1 `Sixteen))) tl
258 let process_intel_hex =
263 match he.record_type with
264 End -> assert (tl = []); mem
265 | Data -> aux (load_from mem he.record_addr he.data_field) tl
268 aux Physical.WordMap.empty
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.
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)
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
289 List.rev (aux chunk_size 0 0 [] [])
292 let clean_exported_code_memory = List.filter (fun x -> snd x <> [])
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
305 let process_exported_code_memory =
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
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
318 { temp_record with data_checksum = calculate_checksum temp_record })
325 vect_of_int 0 `Eight :: zeros (len - 1)
327 let post_process_exported_code_memory intel_hex =
328 let reversed = List.rev intel_hex in
333 if he.record_type = End then
335 else if he.record_type = Data then
336 if he.data_field = zeros (int_of_vect he.record_length) then
343 List.rev (aux reversed)
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
351 [{ record_length = zero `Eight;
352 record_addr = zero `Sixteen;
355 data_checksum = vect_of_int 255 `Eight
357 postprocessed @ end_buffer
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;