]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/ERTL/ERTLInterpret.ml
Package description and copyright added.
[pkg-cerco/acc.git] / src / ERTL / ERTLInterpret.ml
1
2 (** This module provides an interpreter for the ERTL language. *)
3
4
5 let error_prefix = "ERTL interpret"
6 let error s = Error.global_error error_prefix s
7
8
9 module Mem = Driver.ERTLMemory
10 module Val = Mem.Value
11 let chunk = Driver.ERTLMemory.int_size
12 module Eval = I8051.Eval (Val)
13
14
15 (* Memory *)
16
17 type 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
22 type local_env = Val.t Register.Map.t
23
24 (* Hardware registers environments. They associate a value to each hardware
25    register. *)
26
27 type 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
33 type stack_frame = local_env
34
35 (* Execution states. *)
36
37 type 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
51 let add_st_frs st frame = { st with st_frs = frame :: st.st_frs }
52 let 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 }
55 let change_pc st pc = { st with pc = pc }
56 let change_isp st isp = { st with isp = isp }
57 let change_exit st exit = { st with exit = exit }
58 let change_lenv st lenv = { st with lenv = lenv }
59 let change_carry st carry = { st with carry = carry }
60 let change_renv st renv = { st with renv = renv }
61 let change_mem st mem = { st with mem = mem }
62 let change_trace st trace = { st with trace = trace }
63 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
64
65 let 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
81 module Labels_Offsets = Bijection.Make (Label) (Val.Offset)
82
83 let 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
91 let 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
97 let 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
101 let 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
112 let 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
116 let 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
122 let 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
126 let 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
132 type register = Hdw of I8051.register | Psd of Register.t
133
134 let 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
142 let 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
150 let 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
155 let 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
161 let get_ra st =
162   let (st, pch) = pop st in
163   let (st, pcl) = pop st in
164   [pcl ; pch]
165
166 let 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
173 let save_frame st = add_st_frs st st.lenv
174
175 let 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
182 let pointer_of_label lbls_offs ptr lbl =
183   Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
184
185 let get_sp st =
186   List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]
187
188 let 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 let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2]
196
197
198 module InterpretExternal = Primitive.Interpret (Mem)
199
200 let interpret_external mem f args = match InterpretExternal.t mem f args with
201   | (mem', InterpretExternal.V vs) -> (mem', vs)
202   | (mem', InterpretExternal.A addr) -> (mem', addr)
203
204 let fetch_external_args f st =
205   let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
206   let params = MiscPottier.prefix size I8051.parameters in
207   List.map (fun r -> get_reg (Hdw r) st) params
208
209 let set_result st vs =
210   let f st (r, v) = add_reg (Hdw r) v st in
211   List.fold_left f st (MiscPottier.combine I8051.rets vs)
212
213 let interpret_external_call st f next_pc =
214   let args = fetch_external_args f 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
220 let interpret_call lbls_offs st ptr 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
232 let 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
242 let 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_opaccsA (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_opaccsB (opaccs, destr, srcr1, srcr2, lbl) ->
327       let (_, v) =
328         Eval.opaccs opaccs
329           (get_reg (Psd srcr1) st)
330           (get_reg (Psd srcr2) st) in
331       let st = add_reg (Psd destr) v st in
332       next_pc st lbl
333
334     | ERTL.St_op1 (op1, destr, srcr, lbl) ->
335       let v = Eval.op1 op1 (get_reg (Psd srcr) st) in
336       let st = add_reg (Psd destr) v st in
337       next_pc st lbl
338
339     | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
340       let (v, carry) =
341         Eval.op2 st.carry op2
342           (get_reg (Psd srcr1) st)
343           (get_reg (Psd srcr2) st) in
344       let st = change_carry st carry in
345       let st = add_reg (Psd destr) v st in
346       next_pc st lbl
347
348     | ERTL.St_clear_carry lbl ->
349       let st = change_carry st Val.zero in
350       next_pc st lbl
351
352     | ERTL.St_set_carry lbl ->
353       let st = change_carry st (Val.of_int 1) in
354       next_pc st lbl
355
356     | ERTL.St_load (destr, addr1, addr2, lbl) ->
357       let addr = make_addr st addr1 addr2 in
358       let v = Mem.load st.mem chunk addr in
359       let st = add_reg (Psd destr) v st in
360       next_pc st lbl
361
362     | ERTL.St_store (addr1, addr2, srcr, lbl) ->
363       let addr = make_addr st addr1 addr2 in
364       let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
365       let st = change_mem st mem in
366       next_pc st lbl
367
368     | ERTL.St_call_id (f, _, lbl) ->
369       interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
370
371     | ERTL.St_call_ptr (f1, f2, _, lbl) ->
372       interpret_call lbls_offs st (make_addr st f1 f2) lbl
373
374     | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
375       let v = get_reg (Psd srcr) st in
376       let lbl =
377         if Val.is_true v then lbl_true
378         else
379           if Val.is_false v then lbl_false
380           else error "Undecidable branchment." in
381       next_pc st lbl
382
383     | ERTL.St_return _ ->
384       interpret_return lbls_offs st
385
386
387 let print_lenv lenv =
388   let f r v =
389     if not (Val.eq v Val.undef) then
390       Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in
391   Register.Map.iter f lenv
392
393 let print_renv renv =
394   let f r v =
395     if not (Val.eq v Val.undef) then
396     Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
397   I8051.RegisterMap.iter f renv
398
399 let current_label lbls_offs st =
400   Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
401
402 let print_state lbls_offs st =
403   Printf.printf "PC: %s (%s)\n%!"
404     (Val.string_of_address st.pc) (current_label lbls_offs st) ;
405   Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
406   Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
407   Printf.printf "Carry: %s%!" (Val.to_string st.carry) ;
408   print_lenv st.lenv ;
409   print_renv st.renv ;
410   Mem.print st.mem ;
411   Printf.printf "\n%!"
412
413 let compute_result st ret_regs =
414   let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
415   let f res v = res && (Val.is_int v) in
416   let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
417   if is_int vs then
418     let chunks =
419       List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
420     IntValue.Int32.merge chunks
421   else IntValue.Int32.zero
422
423 let rec iter_small_step debug lbls_offs st =
424   let print_and_return_result (res, cost_labels) =
425     if debug then Printf.printf "Result = %s\n%!"
426       (IntValue.Int32.to_string res) ;
427     (res, cost_labels) in
428   if debug then print_state lbls_offs st ;
429   match fetch_stmt lbls_offs st with
430     | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
431       print_and_return_result (compute_result st ret_regs, List.rev st.trace)
432     | stmt ->
433       let st' = interpret_stmt lbls_offs st stmt in
434       iter_small_step debug lbls_offs st'
435
436
437 let add_global_vars =
438   List.fold_left
439     (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
440
441 let add_fun_defs =
442   List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
443
444 let init_prog (st : state) (p : ERTL.program) : state =
445   let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in
446   change_mem st mem
447
448 let init_sp st =
449   let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
450   let sp =
451     Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
452   let st = change_mem st mem in
453   (st, sp)
454
455 let init_isp st =
456   let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
457   let st = change_mem (change_isp st isp) mem in
458   let (mem, exit) = Mem.alloc st.mem 1 in
459   let st = change_exit st exit in
460   let st = push st (List.nth exit 0) in
461   let st = push st (List.nth exit 1) in
462   st  
463
464 let init_renv st sp =
465   let f r renv = I8051.RegisterMap.add r Val.undef renv in
466   let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
467   let spl = List.nth sp 0 in
468   let sph = List.nth sp 1 in
469   let renv = I8051.RegisterMap.add I8051.sph sph renv in
470   let renv = I8051.RegisterMap.add I8051.spl spl renv in
471   change_renv st renv
472
473 let init_main_call lbls_offs st main =
474   let ptr = Mem.find_global st.mem main in
475   match Mem.find_fun_def st.mem ptr with
476     | ERTL.F_int def ->
477       init_fun_call lbls_offs st ptr def
478     | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
479
480
481 (* Before interpreting, the environment is initialized:
482    - Build a bijection between the labels in the program and some values (taken
483      amongst the offsets).
484    - Add function definitions to the memory and reserve space for the globals.
485    - Allocate memory to emulate the external stack and initialize the external
486      stack pointer.
487    - Allocate memory to emulate the internal stack and initialize the internal
488      stack pointer.
489    - Initialiaze the physical register environment. All are set to 0, except for
490      the stack pointer registers that take the high and low bits of the external
491      stack pointer.
492    - Initialize a call to the main (set the current program counter to the
493      beginning of the function).
494    - Initialize the carry flag to 0. *)
495
496 let interpret debug p =
497   Printf.printf "*** ERTL interpret ***\n%!" ;
498   match p.ERTL.main with
499     | None -> (IntValue.Int32.zero, [])
500     | Some main ->
501       let lbls_offs = labels_offsets p in
502       let st = empty_state in
503       let st = init_prog st p in
504       let (st, sp) = init_sp st in
505       let st = init_isp st in
506       let st = init_renv st sp in
507       let st = init_main_call lbls_offs st main in
508       let st = change_carry st Val.zero in
509       iter_small_step debug lbls_offs st