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

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

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 14.9 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 v) -> (mem', [v])
200  | (mem', InterpretExternal.A addr) -> (mem', addr)
201
202let fetch_external_args st =
203  (* TODO: this is bad when parameters are the empty list. *)
204  [get_reg (Hdw (List.hd I8051.parameters)) st]
205
206let set_result st = function
207  | [] -> assert false (* should be impossible: at least one value returned *)
208  | [v] -> add_reg (Hdw I8051.dpl) v st
209  | v1 :: v2 :: _ ->
210    let st = add_reg (Hdw I8051.dpl) v1 st in
211    add_reg (Hdw I8051.dph) v2 st
212
213let interpret_external_call st f next_pc =
214  let args = fetch_external_args st in
215  let (mem, vs) = interpret_external st.mem f args in
216  let st = change_mem st mem in
217  let st = set_result st vs in
218  change_pc st next_pc
219
220let interpret_call lbls_offs st f ra =
221  let ptr = Mem.find_global st.mem f in
222  match Mem.find_fun_def st.mem ptr with
223    | ERTL.F_int def ->
224      let st = save_ra lbls_offs st ra in
225      let st = save_frame st in
226      init_fun_call lbls_offs st ptr def
227    | ERTL.F_ext def ->
228      let next_pc = 
229        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
230      interpret_external_call st def.AST.ef_tag next_pc
231
232let interpret_return lbls_offs st =
233  let st = pop_st_frs st in
234  let (st, pch) = pop st in
235  let (st, pcl) = pop st in
236  let pc = [pcl ; pch] in
237  change_pc st pc
238
239
240(* Interpret statements. *)
241
242let interpret_stmt lbls_offs st stmt =
243  let next_pc = next_pc lbls_offs in
244  match stmt with
245
246    | ERTL.St_skip lbl ->
247      next_pc st lbl
248
249    | ERTL.St_comment (s, lbl) ->
250(*
251      Printf.printf "*** %s ***\n\n%!" s ;
252*)
253      next_pc st lbl
254
255    | ERTL.St_cost (cost_lbl, lbl) ->
256      let st = add_trace st cost_lbl in
257      next_pc st lbl
258
259    | ERTL.St_get_hdw (destr, srcr, lbl) ->
260      let st = add_reg (Psd destr) (get_reg (Hdw srcr) st) st in
261      next_pc st lbl
262
263    | ERTL.St_set_hdw (destr, srcr, lbl) ->
264      let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
265      next_pc st lbl
266
267    | ERTL.St_hdw_to_hdw (destr, srcr, lbl) ->
268      let st = add_reg (Hdw destr) (get_reg (Hdw srcr) st) st in
269      next_pc st lbl
270
271    | ERTL.St_newframe lbl ->
272      let size = framesize st in
273      let sp = get_sp st in
274      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
275      let st = set_sp new_sp st in
276      next_pc st lbl
277
278    | ERTL.St_delframe lbl ->
279      let size = framesize st in
280      let sp = get_sp st in
281      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
282      let st = set_sp new_sp st in
283      next_pc st lbl
284
285    | ERTL.St_framesize (destr, lbl) ->
286      let size = framesize st in
287      let st = add_reg (Psd destr) (Val.of_int size) st in
288      next_pc st lbl
289
290    | ERTL.St_pop (destr, lbl) ->
291      let (st, v) = pop st in
292      let st = add_reg (Psd destr) v st in
293      next_pc st lbl
294
295    | ERTL.St_push (srcr, lbl) ->
296      let v = get_reg (Psd srcr) st in
297      let st = push st v in
298      next_pc st lbl
299
300    | ERTL.St_addrH (r, x, lbl) ->
301      let vs = Mem.find_global st.mem x in
302      let st = add_reg (Psd r) (List.nth vs 1) st in
303      next_pc st lbl
304
305    | ERTL.St_addrL (r, x, lbl) ->
306      let vs = Mem.find_global st.mem x in
307      let st = add_reg (Psd r) (List.nth vs 0) st in
308      next_pc st lbl
309
310    | ERTL.St_int (r, i, lbl) ->
311      let st = add_reg (Psd r) (Val.of_int i) st in
312      next_pc st lbl
313
314    | ERTL.St_move (destr, srcr, lbl) ->
315      let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
316      next_pc st lbl
317
318    | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) ->
319      let v =
320        Eval.opaccs opaccs
321          (get_reg (Psd srcr1) st)
322          (get_reg (Psd srcr2) st) in
323      let st = add_reg (Psd destr) v st in
324      next_pc st lbl
325
326    | ERTL.St_op1 (op1, destr, srcr, lbl) ->
327      let v = Eval.op1 op1 (get_reg (Psd srcr) st) in
328      let st = add_reg (Psd destr) v st in
329      next_pc st lbl
330
331    | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
332      let (v, carry) =
333        Eval.op2 st.carry op2
334          (get_reg (Psd srcr1) st)
335          (get_reg (Psd srcr2) st) in
336      let st = change_carry st carry in
337      let st = add_reg (Psd destr) v st in
338      next_pc st lbl
339
340    | ERTL.St_clear_carry lbl ->
341      let st = change_carry st Val.zero in
342      next_pc st lbl
343
344    | ERTL.St_load (destr, addr1, addr2, lbl) ->
345      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
346      let v = Mem.load st.mem chunk addr in
347      let st = add_reg (Psd destr) v st in
348      next_pc st lbl
349
350    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
351      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
352      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
353      let st = change_mem st mem in
354      next_pc st lbl
355
356    | ERTL.St_call_id (f, _, lbl) ->
357      interpret_call lbls_offs st f lbl
358
359    | ERTL.St_condacc (srcr, lbl_true, lbl_false) ->
360      let v = get_reg (Psd srcr) st in
361      let lbl =
362        if Val.is_true v then lbl_true
363        else
364          if Val.is_false v then lbl_false
365          else error "Undecidable branchment." in
366      next_pc st lbl
367
368    | ERTL.St_return _ ->
369      interpret_return lbls_offs st
370
371
372let print_lenv lenv =
373  let f r v =
374    if not (Val.eq v Val.undef) then
375      Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in
376  Register.Map.iter f lenv
377
378let print_renv renv =
379  let f r v =
380    if not (Val.eq v Val.undef) then
381    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
382  I8051.RegisterMap.iter f renv
383
384let current_label lbls_offs st =
385  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
386
387let print_state lbls_offs st =
388  Printf.printf "PC: %s (%s)\n%!"
389    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
390  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
391  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
392  print_lenv st.lenv ;
393  print_renv st.renv ;
394  Mem.print st.mem ;
395  Printf.printf "\n%!"
396
397let compute_result st ret_regs =
398  try
399    let v = get_reg (Psd (List.hd ret_regs)) st in
400    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
401    else IntValue.Int8.zero
402  with Not_found -> IntValue.Int8.zero
403
404let rec iter_small_step debug lbls_offs st =
405  if debug then print_state lbls_offs st ;
406  match fetch_stmt lbls_offs st with
407    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
408      (compute_result st ret_regs, List.rev st.trace)
409    | stmt ->
410      let st' = interpret_stmt lbls_offs st stmt in
411      iter_small_step debug lbls_offs st'
412
413
414let add_global_vars =
415  List.fold_left
416    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
417
418let add_fun_defs =
419  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
420
421let init_prog (st : state) (p : ERTL.program) : state =
422  let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in
423  change_mem st mem
424
425let init_sp st =
426  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
427  let sp =
428    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
429  let st = change_mem st mem in
430  (st, sp)
431
432let init_isp st =
433  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
434  let st = change_mem (change_isp st isp) mem in
435  let (mem, exit) = Mem.alloc st.mem 1 in
436  let st = change_exit st exit in
437  let st = push st (List.nth exit 0) in
438  let st = push st (List.nth exit 1) in
439  st 
440
441let init_renv st sp =
442  let f r renv = I8051.RegisterMap.add r Val.undef renv in
443  let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
444  let spl = List.nth sp 0 in
445  let sph = List.nth sp 1 in
446  let renv = I8051.RegisterMap.add I8051.sph sph renv in
447  let renv = I8051.RegisterMap.add I8051.spl spl renv in
448  change_renv st renv
449
450let init_main_call lbls_offs st main =
451  let ptr = Mem.find_global st.mem main in
452  match Mem.find_fun_def st.mem ptr with
453    | ERTL.F_int def ->
454      init_fun_call lbls_offs st ptr def
455    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
456
457
458(* Before interpreting, the environment is initialized:
459   - Build a bijection between the labels in the program and some values (taken
460     amongst the offsets).
461   - Add function definitions to the memory and reserve space for the globals.
462   - Allocate memory to emulate the external stack and initialize the external
463     stack pointer.
464   - Allocate memory to emulate the internal stack and initialize the internal
465     stack pointer.
466   - Initialiaze the physical register environment. All are set to 0, except for
467     the stack pointer registers that take the high and low bits of the external
468     stack pointer.
469   - Initialize a call to the main (set the current program counter to the
470     beginning of the function).
471   - Initialize the carry flag to 0. *)
472
473let interpret debug p =
474  if debug then Printf.printf "*** ERTL ***\n\n%!" ;
475  match p.ERTL.main with
476    | None -> (IntValue.Int8.zero, [])
477    | Some main ->
478      let lbls_offs = labels_offsets p in
479      let st = empty_state in
480      let st = init_prog st p in
481      let (st, sp) = init_sp st in
482      let st = init_isp st in
483      let st = init_renv st sp in
484      let st = init_main_call lbls_offs st main in
485      let st = change_carry st Val.zero in
486      iter_small_step debug lbls_offs st
Note: See TracBrowser for help on using the repository browser.