source: driver/IntelHex.ml @ 2779

Last change on this file since 2779 was 2779, checked in by sacerdot, 8 years ago
  1. bug fixed in the use of vsplit
  2. major speed up (avoid detour via base-1 natural numbers)

Now the IntelHex? file is output.

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