source: driver/IntelHex.ml @ 2834

Last change on this file since 2834 was 2780, checked in by sacerdot, 7 years ago

Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were
using the wrong indianess. They were also redundant with the good
(but inefficient) ones in Arithmetic.ma.

On a simple test the compiled code runs (I have not checked the
result).

File size: 9.7 KB
Line 
1(************* Glue code ******************************)
2
3let ($) f x = f x
4let flip f a b = f b a
5
6type byte = Extracted.BitVector.byte
7type word = Extracted.BitVector.word
8
9let size_lookup = function `Eight -> 8 | `Sixteen -> 16
10
11let zero size =
12 let size = size_lookup size in
13 Extracted.BitVector.zero (Extracted.Glue.matitanat_of_int size)
14
15let 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!!! *)
20let hex_string_of_vect v = Printf.sprintf "%0 2X" (int_of_vect v);;
21
22let complement v = Extracted.BitVector.negation_bv (Extracted.Glue.matitanat_of_int 8) v
23
24let divide_with_remainder x y = (x / y, x mod y)
25
26let 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
35let 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
40let 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
46let 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
51module WordMap :
52 sig
53   val find : word -> Extracted.BitVector.byte Extracted.BitVectorTrie.bitVectorTrie -> byte
54 end =
55struct
56  let find k m = Extracted.BitVectorTrie.lookup (Extracted.Glue.matitanat_of_int 16) k m (zero `Eight)
57end;;
58
59(************* Untrusted code ******************************)
60(*
61open BitVectors;;
62open ASM;;
63open Util;;
64open Parser;;
65open Printf;;
66
67exception WrongFormat of string
68*)
69
70type intel_hex_entry_type =
71    Data
72  | End
73  | ExtendedSeg
74  | ExtendedLinear
75;;
76
77type 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
87type intel_hex_format = intel_hex_entry list;;
88
89(*
90let 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
101let 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
111let int_of_intel_hex_entry_type =
112 function
113    Data -> 0
114  | End -> 1
115  | ExtendedSeg -> 2
116  | ExtendedLinear -> 4
117;;
118
119(*
120let prs_nibble =
121         prs_hex_digit >>=
122fun a -> return $ vect_of_int (hex_digit_of_char a) `Four
123;;
124
125let prs_byte =
126         prs_nibble >>=
127fun a -> prs_nibble >>=
128fun b -> return $ mk_byte a b
129;;
130
131let prs_word =
132         prs_byte >>=
133fun a -> prs_byte >>=
134fun b -> return $ mk_word a b
135;;
136
137let prs_length = prs_byte;;
138let prs_data len = prs_exact len prs_byte
139let prs_checksum = prs_byte;;
140let prs_addr = prs_word;;
141
142let prs_type =
143         prs_hex_digit >>=
144fun a -> prs_hex_digit >>=
145fun 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
153let 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
163let 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(*
171let checksum_valid hex_entry =
172  let total = calculate_checksum hex_entry in
173    hex_entry.data_checksum = total
174
175let prs_intel_hex_record =
176         prs_char ':'  >>=
177fun _ -> prs_length    >>=
178fun b -> prs_addr      >>=
179fun c -> prs_type      >>=
180fun d -> prs_data (int_of_vect b) >>=
181fun e -> prs_checksum  >>=
182fun f -> prs_eof       >>=
183fun _ ->
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
197let prs_intel_hex_format =
198  prs_sep_by prs_intel_hex_record (prs_char '\n')
199;;
200
201let 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
208let 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
223let 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(*
234let 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
251let 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
258let 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*)
278let 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
292let clean_exported_code_memory = List.filter (fun x -> snd x <> [])
293;;
294
295(*
296let 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
305let 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
321let rec zeros len =
322  if len = 0 then
323    []
324  else
325    vect_of_int 0 `Eight :: zeros (len - 1)
326
327let 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
345let 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(*
361let 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*)
Note: See TracBrowser for help on using the repository browser.