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

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