source: Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLInterpret.ml @ 1345

Last change on this file since 1345 was 1345, checked in by tranquil, 9 years ago

work on ERTL and LTL completed

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