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

Last change on this file since 1542 was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

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
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 push st v =
161  let mem = Mem.store st.mem chunk st.isp v in
162  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
163  change_mem (change_isp st isp) mem
164
165let pop st =
166  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
167  let st = change_isp st isp in
168  let v = Mem.load st.mem chunk st.isp in
169  (st, v)
170
171let get_ra st =
172  let (st, pch) = pop st in
173  let (st, pcl) = pop st in
174  [pcl ; pch]
175
176let save_ra lbls_offs st lbl =
177  let ra =
178    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
179  let st = push st (List.nth ra 0) in
180  let st = push st (List.nth ra 1) in
181  st
182
183let save_frame st = add_st_frs st st.lenv
184
185let label_of_pointer lbls_offs ptr =
186(*
187  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
188*)
189  let off = Val.offset_of_address ptr in
190  Labels_Offsets.find2 off lbls_offs
191
192let pointer_of_label lbls_offs ptr lbl =
193  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
194
195let get_sp st =
196  List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]
197
198let set_sp vs st =
199  let spl = List.nth vs 0 in
200  let sph = List.nth vs 1 in
201  let st = add_reg (Hdw I8051.spl) spl st in
202  let st = add_reg (Hdw I8051.sph) sph st in
203  st
204
205let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2]
206
207
208module InterpretExternal = Primitive.Interpret (Mem)
209
210let interpret_external mem f args = match InterpretExternal.t mem f args with
211  | (mem', InterpretExternal.V vs) -> (mem', vs)
212  | (mem', InterpretExternal.A addr) -> (mem', addr)
213
214let fetch_external_args f st =
215  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
216  let params = MiscPottier.prefix size I8051.parameters in
217  List.map (fun r -> get_reg (Hdw r) st) params
218
219let set_result st vs =
220  let f st (r, v) = add_reg (Hdw r) v st in
221  List.fold_left f st (MiscPottier.combine I8051.rets vs)
222
223let interpret_external_call st f next_pc =
224  let args = fetch_external_args f st in
225  let (mem, vs) = interpret_external st.mem f args in
226  let st = change_mem st mem in
227  let st = set_result st vs in
228  change_pc st next_pc
229
230let interpret_call lbls_offs st ptr ra =
231  (* let ptr = Mem.find_global st.mem f in *)
232  match Mem.find_fun_def st.mem ptr with
233    | ERTL.F_int def ->
234      let st = save_ra lbls_offs st ra in
235      let st = save_frame st in
236      init_fun_call lbls_offs st ptr def
237    | ERTL.F_ext def ->
238      let next_pc = 
239        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
240      interpret_external_call st def.AST.ef_tag next_pc
241
242let interpret_return lbls_offs st =
243  let st = forget_ind st in
244  let st = pop_st_frs st in
245  let (st, pch) = pop st in
246  let (st, pcl) = pop st in
247  let pc = [pcl ; pch] in
248  change_pc st pc
249
250
251(* Interpret statements. *)
252
253let interpret_stmt lbls_offs st stmt =
254  let next_pc = next_pc lbls_offs in
255  match stmt with
256
257    | ERTL.St_skip lbl ->
258      next_pc st lbl
259
260    | ERTL.St_comment (s, lbl) ->
261(*
262      Printf.printf "*** %s ***\n\n%!" s ;
263*)
264      next_pc st lbl
265
266    | ERTL.St_cost (cost_lbl, lbl) ->
267      let cost_lbl = ev_label st cost_lbl in 
268      let st = add_trace st cost_lbl in
269      next_pc st lbl
270
271    | ERTL.St_ind_0 (i, lbl) ->
272      enter_loop st i;
273      next_pc st lbl
274
275    | ERTL.St_ind_inc (i, lbl) ->
276      continue_loop st i; 
277      next_pc st lbl
278
279    | ERTL.St_get_hdw (destr, srcr, lbl) ->
280      let st = add_reg (Psd destr) (get_reg (Hdw srcr) st) st in
281      next_pc st lbl
282
283    | ERTL.St_set_hdw (destr, srcr, lbl) ->
284      let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
285      next_pc st lbl
286
287    | ERTL.St_hdw_to_hdw (destr, srcr, lbl) ->
288      let st = add_reg (Hdw destr) (get_reg (Hdw srcr) st) st in
289      next_pc st lbl
290
291    | ERTL.St_newframe lbl ->
292      let size = framesize st in
293      let sp = get_sp st in
294      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
295      let st = set_sp new_sp st in
296      next_pc st lbl
297
298    | ERTL.St_delframe lbl ->
299      let size = framesize st in
300      let sp = get_sp st in
301      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
302      let st = set_sp new_sp st in
303      next_pc st lbl
304
305    | ERTL.St_framesize (destr, lbl) ->
306      let size = framesize st in
307      let st = add_reg (Psd destr) (Val.of_int size) st in
308      next_pc st lbl
309
310    | ERTL.St_pop (destr, lbl) ->
311      let (st, v) = pop st in
312      let st = add_reg (Psd destr) v st in
313      next_pc st lbl
314
315    | ERTL.St_push (srcr, lbl) ->
316      let v = get_reg (Psd srcr) st in
317      let st = push st v in
318      next_pc st lbl
319
320    | ERTL.St_addrH (r, x, lbl) ->
321      let vs = Mem.find_global st.mem x in
322      let st = add_reg (Psd r) (List.nth vs 1) st in
323      next_pc st lbl
324
325    | ERTL.St_addrL (r, x, lbl) ->
326      let vs = Mem.find_global st.mem x in
327      let st = add_reg (Psd r) (List.nth vs 0) st in
328      next_pc st lbl
329
330    | ERTL.St_int (r, i, lbl) ->
331      let st = add_reg (Psd r) (Val.of_int i) st in
332      next_pc st lbl
333
334    | ERTL.St_move (destr, srcr, lbl) ->
335      let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
336      next_pc st lbl
337
338    | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) ->
339      let (v, _) =
340        Eval.opaccs opaccs
341          (get_reg (Psd srcr1) st)
342          (get_reg (Psd srcr2) st) in
343      let st = add_reg (Psd destr) v st in
344      next_pc st lbl
345
346    | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) ->
347      let (_, v) =
348        Eval.opaccs opaccs
349          (get_reg (Psd srcr1) st)
350          (get_reg (Psd srcr2) st) in
351      let st = add_reg (Psd destr) v st in
352      next_pc st lbl
353
354    | ERTL.St_op1 (op1, destr, srcr, lbl) ->
355      let v = Eval.op1 op1 (get_reg (Psd srcr) st) in
356      let st = add_reg (Psd destr) v st in
357      next_pc st lbl
358
359    | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
360      let (v, carry) =
361        Eval.op2 st.carry op2
362          (get_reg (Psd srcr1) st)
363          (get_reg (Psd srcr2) st) in
364      let st = change_carry st carry in
365      let st = add_reg (Psd destr) v st in
366      next_pc st lbl
367
368    | ERTL.St_clear_carry lbl ->
369      let st = change_carry st Val.zero in
370      next_pc st lbl
371
372    | ERTL.St_set_carry lbl ->
373      let st = change_carry st (Val.of_int 1) in
374      next_pc st lbl
375
376    | ERTL.St_load (destr, addr1, addr2, lbl) ->
377      let addr = make_addr st addr1 addr2 in
378      let v = Mem.load st.mem chunk addr in
379      let st = add_reg (Psd destr) v st in
380      next_pc st lbl
381
382    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
383      let addr = make_addr st addr1 addr2 in
384      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
385      let st = change_mem st mem in
386      next_pc st lbl
387
388    | ERTL.St_call_id (f, _, lbl) ->
389      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
390
391    | ERTL.St_call_ptr (f1, f2, _, lbl) ->
392      interpret_call lbls_offs st (make_addr st f1 f2) lbl
393
394    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
395      let v = get_reg (Psd srcr) st in
396      let lbl =
397        if Val.is_true v then lbl_true
398        else
399          if Val.is_false v then lbl_false
400          else error "Undecidable branchment." in
401      next_pc st lbl
402
403    | ERTL.St_return _ ->
404      interpret_return lbls_offs st
405
406
407let print_lenv lenv =
408  let f r v =
409    if not (Val.eq v Val.undef) then
410      Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in
411  Register.Map.iter f lenv
412
413let print_renv renv =
414  let f r v =
415    if not (Val.eq v Val.undef) then
416    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
417  I8051.RegisterMap.iter f renv
418
419let current_label lbls_offs st =
420  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
421
422let print_state lbls_offs st =
423  Printf.printf "PC: %s (%s)\n%!"
424    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
425  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
426  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
427  Printf.printf "Carry: %s%!" (Val.to_string st.carry) ;
428  print_lenv st.lenv ;
429  print_renv st.renv ;
430  Mem.print st.mem ;
431  Printf.printf "\n%!"
432
433let compute_result st ret_regs =
434  let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
435  let f res v = res && (Val.is_int v) in
436  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
437  if is_int vs then
438    let chunks =
439      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
440    IntValue.Int32.merge chunks
441  else IntValue.Int32.zero
442
443let rec iter_small_step debug lbls_offs st =
444  let print_and_return_result (res, cost_labels) =
445    if debug then Printf.printf "Result = %s\n%!"
446      (IntValue.Int32.to_string res) ;
447    (res, cost_labels) in
448  if debug then print_state lbls_offs st ;
449  match fetch_stmt lbls_offs st with
450    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
451      print_and_return_result (compute_result st ret_regs, List.rev st.trace)
452    | stmt ->
453      let st' = interpret_stmt lbls_offs st stmt in
454      iter_small_step debug lbls_offs st'
455
456
457let add_global_vars =
458  List.fold_left
459    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
460
461let add_fun_defs =
462  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
463
464let init_prog (st : state) (p : ERTL.program) : state =
465  let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in
466  change_mem st mem
467
468let init_sp st =
469  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
470  let sp =
471    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
472  let st = change_mem st mem in
473  (st, sp)
474
475let init_isp st =
476  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
477  let st = change_mem (change_isp st isp) mem in
478  let (mem, exit) = Mem.alloc st.mem 1 in
479  let st = change_exit st exit in
480  let st = push st (List.nth exit 0) in
481  let st = push st (List.nth exit 1) in
482  st 
483
484let init_renv st sp =
485  let f r renv = I8051.RegisterMap.add r Val.undef renv in
486  let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
487  let spl = List.nth sp 0 in
488  let sph = List.nth sp 1 in
489  let renv = I8051.RegisterMap.add I8051.sph sph renv in
490  let renv = I8051.RegisterMap.add I8051.spl spl renv in
491  change_renv st renv
492
493let init_main_call lbls_offs st main =
494  let ptr = Mem.find_global st.mem main in
495  match Mem.find_fun_def st.mem ptr with
496    | ERTL.F_int def ->
497      init_fun_call lbls_offs st ptr def
498    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
499
500
501(* Before interpreting, the environment is initialized:
502   - Build a bijection between the labels in the program and some values (taken
503     amongst the offsets).
504   - Add function definitions to the memory and reserve space for the globals.
505   - Allocate memory to emulate the external stack and initialize the external
506     stack pointer.
507   - Allocate memory to emulate the internal stack and initialize the internal
508     stack pointer.
509   - Initialiaze the physical register environment. All are set to 0, except for
510     the stack pointer registers that take the high and low bits of the external
511     stack pointer.
512   - Initialize a call to the main (set the current program counter to the
513     beginning of the function).
514   - Initialize the carry flag to 0. *)
515
516let interpret debug p =
517  Printf.printf "*** ERTL interpret ***\n%!" ;
518  match p.ERTL.main with
519    | None -> (IntValue.Int32.zero, [])
520    | Some main ->
521      let lbls_offs = labels_offsets p in
522      let st = empty_state in
523      let st = init_prog st p in
524      let (st, sp) = init_sp st in
525      let st = init_isp st in
526      let st = init_renv st sp in
527      let st = init_main_call lbls_offs st main in
528      let st = change_carry st Val.zero in
529      iter_small_step debug lbls_offs st
Note: See TracBrowser for help on using the repository browser.