source: driver/IntelHex.ml @ 2778

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

Code to pretty-print the IntelHex? output.
At the moment the glue code between the trusted and untrusted code
pass through Matita's base 1 integers. Thus the computation is just too
slow.

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