source: Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml @ 818

Last change on this file since 818 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

File size: 15.6 KB
Line 
1
2(** This module provides an interpreter for the ERTL language. *)
3
4
5let error_prefix = "ERTL interpret"
6let error s = Error.global_error error_prefix s
7
8
9module Mem = Driver.ERTLMemory
10module Val = Mem.Value
11let chunk = Driver.ERTLMemory.int_size
12module Eval = I8051.Eval (Val)
13
14
15(* Memory *)
16
17type memory = ERTL.function_def Mem.memory
18
19(* Local environments. They associate a value to the pseudo-registers of the
20   function being executed. *)
21
22type local_env = Val.t Register.Map.t
23
24(* Hardware registers environments. They associate a value to each hardware
25   register. *)
26
27type hdw_reg_env = Val.t I8051.RegisterMap.t
28
29(* Call frames. The execution state has a call stack, each element of the stack
30   being composed of the local environment to resume the execution of the
31   caller. *)
32
33type stack_frame = local_env
34
35(* Execution states. *)
36
37type state =
38    { st_frs : stack_frame list ;
39      pc     : Val.address ;
40      isp    : Val.address ;
41      exit   : Val.address ;
42      lenv   : local_env ;
43      carry  : Val.t ;
44      renv   : hdw_reg_env ;
45      mem    : memory ;
46      trace  : CostLabel.t list }
47
48
49(* Helpers *)
50
51let add_st_frs st frame = { st with st_frs = frame :: st.st_frs }
52let pop_st_frs st = match st.st_frs with
53  | [] -> error "Empty stack frames."
54  | lenv :: st_frs -> { st with st_frs = st_frs ; lenv = lenv }
55let change_pc st pc = { st with pc = pc }
56let change_isp st isp = { st with isp = isp }
57let change_exit st exit = { st with exit = exit }
58let change_lenv st lenv = { st with lenv = lenv }
59let change_carry st carry = { st with carry = carry }
60let change_renv st renv = { st with renv = renv }
61let change_mem st mem = { st with mem = mem }
62let change_trace st trace = { st with trace = trace }
63let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
64
65let empty_state =
66  { st_frs = [] ;
67    pc     = Val.null ;
68    isp    = Val.null ;
69    exit   = Val.null ;
70    lenv   = Register.Map.empty ;
71    carry  = Val.undef ;
72    renv   = I8051.RegisterMap.empty ;
73    mem    = Mem.empty ;
74    trace  = [] }
75
76
77(* Each label of each function is associated an address. The base of this
78   address is the base of the function in memory. Inside a function, offsets are
79   bijectively associated to labels. *)
80
81module Labels_Offsets = Bijection.Make (Label) (Val.Offset)
82
83let labels_offsets_internal int_fun =
84  let f lbl _ (lbls_offs, i) =
85    (Labels_Offsets.add1 lbl i lbls_offs, Val.Offset.succ i) in
86  Label.Map.fold f int_fun.ERTL.f_graph
87
88(* [labels_offsets p] builds a bijection between the labels found in the
89   functions of [p] and some memory addresses. *)
90
91let labels_offsets p =
92  let f (lbls_offs, i) (_, def) = match def with
93    | ERTL.F_int int_fun -> labels_offsets_internal int_fun (lbls_offs, i)
94    | _ -> (lbls_offs, i) in
95  fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.ERTL.functs)
96
97let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
98  | ERTL.F_int def -> def
99  | _ -> error "Trying to fetch the definition of an external function."
100
101let fetch_stmt lbls_offs st =
102  let msg =
103    Printf.sprintf "%s does not point to a statement."
104      (Val.string_of_address st.pc) in
105  if Val.is_mem_address st.pc then
106    let off = Val.offset_of_address st.pc in
107    let def = fun_def_of_ptr st.mem st.pc in
108    let lbl = Labels_Offsets.find2 off lbls_offs in
109    Label.Map.find lbl def.ERTL.f_graph
110  else error msg
111
112let entry_pc lbls_offs ptr def =
113  let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in
114  Val.change_address_offset ptr off
115
116let init_fun_call lbls_offs st ptr def =
117  let f r lenv = Register.Map.add r Val.undef lenv in
118  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
119  let pc = entry_pc lbls_offs ptr def in
120  change_lenv (change_pc st pc) lenv
121
122let next_pc lbls_offs st lbl =
123  let off = Labels_Offsets.find1 lbl lbls_offs in
124  change_pc st (Val.change_address_offset st.pc off)
125
126let framesize st =
127  if Val.is_mem_address st.pc then
128    let def = fun_def_of_ptr st.mem st.pc in
129    def.ERTL.f_stacksize
130  else error "No function at the given address."
131
132type register = Hdw of I8051.register | Psd of Register.t
133
134let add_reg r v st = match r with
135  | Hdw r ->
136    let renv = I8051.RegisterMap.add r v st.renv in
137    change_renv st renv
138  | Psd r ->
139    let lenv = Register.Map.add r v st.lenv in
140    change_lenv st lenv
141
142let get_reg r st = match r with
143  | Hdw r ->
144    if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
145    else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
146  | Psd r ->
147    if Register.Map.mem r st.lenv then Register.Map.find r st.lenv
148    else error ("Unknown local register " ^ (Register.print r) ^ ".")
149
150let push st v =
151  let mem = Mem.store st.mem chunk st.isp v in
152  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
153  change_mem (change_isp st isp) mem
154
155let pop st =
156  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
157  let st = change_isp st isp in
158  let v = Mem.load st.mem chunk st.isp in
159  (st, v)
160
161let get_ra st =
162  let (st, pch) = pop st in
163  let (st, pcl) = pop st in
164  [pcl ; pch]
165
166let save_ra lbls_offs st lbl =
167  let ra =
168    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
169  let st = push st (List.nth ra 0) in
170  let st = push st (List.nth ra 1) in
171  st
172
173let save_frame st = add_st_frs st st.lenv
174
175let label_of_pointer lbls_offs ptr =
176(*
177  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
178*)
179  let off = Val.offset_of_address ptr in
180  Labels_Offsets.find2 off lbls_offs
181
182let pointer_of_label lbls_offs ptr lbl =
183  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
184
185let get_sp st =
186  List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]
187
188let set_sp vs st =
189  let spl = List.nth vs 0 in
190  let sph = List.nth vs 1 in
191  let st = add_reg (Hdw I8051.spl) spl st in
192  let st = add_reg (Hdw I8051.sph) sph st in
193  st
194
195
196module InterpretExternal = Primitive.Interpret (Mem)
197
198let interpret_external mem f args = match InterpretExternal.t mem f args with
199  | (mem', InterpretExternal.V vs) -> (mem', vs)
200  | (mem', InterpretExternal.A addr) -> (mem', addr)
201
202let fetch_external_args f st =
203  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
204  let params = MiscPottier.prefix size I8051.parameters in
205  List.map (fun r -> get_reg (Hdw r) st) params
206
207let set_result st vs =
208  let f st (r, v) = add_reg (Hdw r) v st in
209  List.fold_left f st (MiscPottier.combine I8051.rets vs)
210
211let interpret_external_call st f next_pc =
212  let args = fetch_external_args f st in
213  let (mem, vs) = interpret_external st.mem f args in
214  let st = change_mem st mem in
215  let st = set_result st vs in
216  change_pc st next_pc
217
218let interpret_call lbls_offs st f ra =
219  let ptr = Mem.find_global st.mem f in
220  match Mem.find_fun_def st.mem ptr with
221    | ERTL.F_int def ->
222      let st = save_ra lbls_offs st ra in
223      let st = save_frame st in
224      init_fun_call lbls_offs st ptr def
225    | ERTL.F_ext def ->
226      let next_pc = 
227        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
228      interpret_external_call st def.AST.ef_tag next_pc
229
230let interpret_return lbls_offs st =
231  let st = pop_st_frs st in
232  let (st, pch) = pop st in
233  let (st, pcl) = pop st in
234  let pc = [pcl ; pch] in
235  change_pc st pc
236
237
238(* Interpret statements. *)
239
240let interpret_stmt lbls_offs st stmt =
241  let next_pc = next_pc lbls_offs in
242  match stmt with
243
244    | ERTL.St_skip lbl ->
245      next_pc st lbl
246
247    | ERTL.St_comment (s, lbl) ->
248(*
249      Printf.printf "*** %s ***\n\n%!" s ;
250*)
251      next_pc st lbl
252
253    | ERTL.St_cost (cost_lbl, lbl) ->
254      let st = add_trace st cost_lbl in
255      next_pc st lbl
256
257    | ERTL.St_get_hdw (destr, srcr, lbl) ->
258      let st = add_reg (Psd destr) (get_reg (Hdw srcr) st) st in
259      next_pc st lbl
260
261    | ERTL.St_set_hdw (destr, srcr, lbl) ->
262      let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
263      next_pc st lbl
264
265    | ERTL.St_hdw_to_hdw (destr, srcr, lbl) ->
266      let st = add_reg (Hdw destr) (get_reg (Hdw srcr) st) st in
267      next_pc st lbl
268
269    | ERTL.St_newframe lbl ->
270      let size = framesize st in
271      let sp = get_sp st in
272      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
273      let st = set_sp new_sp st in
274      next_pc st lbl
275
276    | ERTL.St_delframe lbl ->
277      let size = framesize st in
278      let sp = get_sp st in
279      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
280      let st = set_sp new_sp st in
281      next_pc st lbl
282
283    | ERTL.St_framesize (destr, lbl) ->
284      let size = framesize st in
285      let st = add_reg (Psd destr) (Val.of_int size) st in
286      next_pc st lbl
287
288    | ERTL.St_pop (destr, lbl) ->
289      let (st, v) = pop st in
290      let st = add_reg (Psd destr) v st in
291      next_pc st lbl
292
293    | ERTL.St_push (srcr, lbl) ->
294      let v = get_reg (Psd srcr) st in
295      let st = push st v in
296      next_pc st lbl
297
298    | ERTL.St_addrH (r, x, lbl) ->
299      let vs = Mem.find_global st.mem x in
300      let st = add_reg (Psd r) (List.nth vs 1) st in
301      next_pc st lbl
302
303    | ERTL.St_addrL (r, x, lbl) ->
304      let vs = Mem.find_global st.mem x in
305      let st = add_reg (Psd r) (List.nth vs 0) st in
306      next_pc st lbl
307
308    | ERTL.St_int (r, i, lbl) ->
309      let st = add_reg (Psd r) (Val.of_int i) st in
310      next_pc st lbl
311
312    | ERTL.St_move (destr, srcr, lbl) ->
313      let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
314      next_pc st lbl
315
316    | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) ->
317      let (v, _) =
318        Eval.opaccs opaccs
319          (get_reg (Psd srcr1) st)
320          (get_reg (Psd srcr2) st) in
321      let st = add_reg (Psd destr) v st in
322      next_pc st lbl
323
324    | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) ->
325      let (_, v) =
326        Eval.opaccs opaccs
327          (get_reg (Psd srcr1) st)
328          (get_reg (Psd srcr2) st) in
329      let st = add_reg (Psd destr) v st in
330      next_pc st lbl
331
332    | ERTL.St_op1 (op1, destr, srcr, lbl) ->
333      let v = Eval.op1 op1 (get_reg (Psd srcr) st) in
334      let st = add_reg (Psd destr) v st in
335      next_pc st lbl
336
337    | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
338      let (v, carry) =
339        Eval.op2 st.carry op2
340          (get_reg (Psd srcr1) st)
341          (get_reg (Psd srcr2) st) in
342      let st = change_carry st carry in
343      let st = add_reg (Psd destr) v st in
344      next_pc st lbl
345
346    | ERTL.St_clear_carry lbl ->
347      let st = change_carry st Val.zero in
348      next_pc st lbl
349
350    | ERTL.St_set_carry lbl ->
351      let st = change_carry st (Val.of_int 1) in
352      next_pc st lbl
353
354    | ERTL.St_load (destr, addr1, addr2, lbl) ->
355      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
356      let v = Mem.load st.mem chunk addr in
357      let st = add_reg (Psd destr) v st in
358      next_pc st lbl
359
360    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
361      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
362      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
363      let st = change_mem st mem in
364      next_pc st lbl
365
366    | ERTL.St_call_id (f, _, lbl) ->
367      interpret_call lbls_offs st f lbl
368
369    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
370      let v = get_reg (Psd srcr) st in
371      let lbl =
372        if Val.is_true v then lbl_true
373        else
374          if Val.is_false v then lbl_false
375          else error "Undecidable branchment." in
376      next_pc st lbl
377
378    | ERTL.St_return _ ->
379      interpret_return lbls_offs st
380
381
382let print_lenv lenv =
383  let f r v =
384    if not (Val.eq v Val.undef) then
385      Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in
386  Register.Map.iter f lenv
387
388let print_renv renv =
389  let f r v =
390    if not (Val.eq v Val.undef) then
391    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
392  I8051.RegisterMap.iter f renv
393
394let current_label lbls_offs st =
395  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
396
397let print_state lbls_offs st =
398  Printf.printf "PC: %s (%s)\n%!"
399    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
400  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
401  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
402  Printf.printf "Carry: %s%!" (Val.to_string st.carry) ;
403  print_lenv st.lenv ;
404  print_renv st.renv ;
405  Mem.print st.mem ;
406  Printf.printf "\n%!"
407
408let compute_result st ret_regs =
409  let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
410  let f res v = res && (Val.is_int v) in
411  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
412  if is_int vs then
413    let chunks =
414      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
415    IntValue.Int32.merge chunks
416  else IntValue.Int32.zero
417
418let rec iter_small_step debug lbls_offs st =
419  let print_and_return_result (res, cost_labels) =
420    if debug then Printf.printf "Result = %s\n%!"
421      (IntValue.Int32.to_string res) ;
422    (res, cost_labels) in
423  if debug then print_state lbls_offs st ;
424  match fetch_stmt lbls_offs st with
425    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
426      print_and_return_result (compute_result st ret_regs, List.rev st.trace)
427    | stmt ->
428      let st' = interpret_stmt lbls_offs st stmt in
429      iter_small_step debug lbls_offs st'
430
431
432let add_global_vars =
433  List.fold_left
434    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
435
436let add_fun_defs =
437  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
438
439let init_prog (st : state) (p : ERTL.program) : state =
440  let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in
441  change_mem st mem
442
443let init_sp st =
444  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
445  let sp =
446    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
447  let st = change_mem st mem in
448  (st, sp)
449
450let init_isp st =
451  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
452  let st = change_mem (change_isp st isp) mem in
453  let (mem, exit) = Mem.alloc st.mem 1 in
454  let st = change_exit st exit in
455  let st = push st (List.nth exit 0) in
456  let st = push st (List.nth exit 1) in
457  st 
458
459let init_renv st sp =
460  let f r renv = I8051.RegisterMap.add r Val.undef renv in
461  let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
462  let spl = List.nth sp 0 in
463  let sph = List.nth sp 1 in
464  let renv = I8051.RegisterMap.add I8051.sph sph renv in
465  let renv = I8051.RegisterMap.add I8051.spl spl renv in
466  change_renv st renv
467
468let init_main_call lbls_offs st main =
469  let ptr = Mem.find_global st.mem main in
470  match Mem.find_fun_def st.mem ptr with
471    | ERTL.F_int def ->
472      init_fun_call lbls_offs st ptr def
473    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
474
475
476(* Before interpreting, the environment is initialized:
477   - Build a bijection between the labels in the program and some values (taken
478     amongst the offsets).
479   - Add function definitions to the memory and reserve space for the globals.
480   - Allocate memory to emulate the external stack and initialize the external
481     stack pointer.
482   - Allocate memory to emulate the internal stack and initialize the internal
483     stack pointer.
484   - Initialiaze the physical register environment. All are set to 0, except for
485     the stack pointer registers that take the high and low bits of the external
486     stack pointer.
487   - Initialize a call to the main (set the current program counter to the
488     beginning of the function).
489   - Initialize the carry flag to 0. *)
490
491let interpret debug p =
492  Printf.printf "*** ERTL interpret ***\n%!" ;
493  match p.ERTL.main with
494    | None -> (IntValue.Int32.zero, [])
495    | Some main ->
496      let lbls_offs = labels_offsets p in
497      let st = empty_state in
498      let st = init_prog st p in
499      let (st, sp) = init_sp st in
500      let st = init_isp st in
501      let st = init_renv st sp in
502      let st = init_main_call lbls_offs st main in
503      let st = change_carry st Val.zero in
504      iter_small_step debug lbls_offs st
Note: See TracBrowser for help on using the repository browser.