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

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

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