]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/RTL/RTLInterpret.ml
Package description and copyright added.
[pkg-cerco/acc.git] / src / RTL / RTLInterpret.ml
1
2 (** This module provides an interpreter for the RTL language. *)
3
4
5 let error_prefix = "RTL interpret"
6 let error s = Error.global_error error_prefix s
7
8
9 module Mem = Driver.RTLMemory
10 module Val = Mem.Value
11 let chunk = Driver.RTLMemory.int_size
12 module Eval = I8051.Eval (Val)
13
14
15 type memory = RTL.function_def Mem.memory
16
17
18 (* Local environments. They associate a value to the registers of the function
19    being executed. *)
20
21 type local_env = Val.t Register.Map.t
22
23 (* Call frames. The execution state has a call stack, each element of the stack
24    being composed of the return registers to store the result of the callee, the
25    graph, the node, the local environment and the value of the carry to resume
26    the execution of the caller. *)
27
28 type stack_frame =
29     { ret_regs : Register.t list ;
30       graph    : RTL.graph ;
31       pc       : Label.t ;
32       sp       : Val.address ;
33       lenv     : local_env ;
34       carry    : Val.t }
35
36 (* Execution states. There are three possible states :
37    - The constructor [State] represents a state when executing a function
38    - The constructor [CallState] represents a state when calling a function
39    - The constructor [ReturnState] represents a state when leaving a function *)
40
41 type state =
42   | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
43              local_env * Val.t (* carry *) * memory * CostLabel.t list
44   | CallState of stack_frame list * RTL.function_def *
45                  Val.t list (* args *) * memory * CostLabel.t list
46   | ReturnState of stack_frame list * Val.t list (* return values *) *
47                    memory * CostLabel.t list
48
49 let string_of_local_env lenv =
50   let f x v s =
51     s ^
52       (if Val.eq v Val.undef then ""
53        else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
54   Register.Map.fold f lenv ""
55
56 let string_of_args args =
57   let f s v = s ^ " " ^ (Val.to_string v) in
58   List.fold_left f "" args
59
60 let print_state = function
61   | State (_, _, lbl, sp, lenv, carry, mem, _) ->
62     Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
63       (Val.string_of_address sp)
64       (Val.to_string carry)
65       (string_of_local_env lenv)
66       (Mem.to_string mem)
67       lbl
68   | CallState (_, _, args, mem, _) ->
69     Printf.printf "Memory:%s\nCall state: %s\n\n%!"
70       (Mem.to_string mem)
71       (string_of_args args)
72   | ReturnState (_, vs, mem, _) ->
73     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
74       (Mem.to_string mem)
75       (string_of_args vs)
76
77
78 let find_function mem f =
79   let addr = Mem.find_global mem f in
80   Mem.find_fun_def mem addr
81
82 let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
83   if Register.Map.mem r lenv then Register.Map.find r lenv
84   else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
85 let get_arg_values lenv args = List.map (get_local_value lenv) args
86
87 let get_local_addr lenv f1 f2 =
88   List.map (get_local_value lenv) [f1 ; f2]
89
90
91 let adds rs vs lenv =
92   let f lenv r v = Register.Map.add r v lenv in
93   List.fold_left2 f lenv rs vs
94
95
96 (* Assign a value to some destinations registers. *)
97
98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
99   let lenv = adds destrs vs lenv in
100   State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
101
102 (* Branch on a value. *)
103
104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
105   let next_lbl =
106     if Val.is_true v then lbl_true
107     else
108       if Val.is_false v then lbl_false
109       else error "Undefined conditional value." in
110   State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
111
112
113 (* Interpret statements. *)
114
115 let interpret_statement
116     (sfrs  : stack_frame list)
117     (graph : RTL.graph)
118     (sp    : Val.address)
119     (lenv  : local_env)
120     (carry : Val.t)
121     (mem   : memory)
122     (stmt  : RTL.statement)
123     (trace : CostLabel.t list) :
124     state = match stmt with
125
126       | RTL.St_skip lbl ->
127         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
128
129       | RTL.St_cost (cost_lbl, lbl) ->
130         State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
131
132       | RTL.St_addr (r1, r2, x, lbl) ->
133         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
134           (Mem.find_global mem x)
135
136       | RTL.St_stackaddr (r1, r2, lbl) ->
137         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
138
139       | RTL.St_int (r, i, lbl) ->
140         assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
141
142       | RTL.St_move (destr, srcr, lbl) ->
143         assign_state sfrs graph lbl sp lenv carry mem trace [destr]
144           [get_local_value lenv srcr]
145
146       | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
147         let (v1, v2) =
148           Eval.opaccs opaccs
149             (get_local_value lenv srcr1)
150             (get_local_value lenv srcr2) in
151         assign_state sfrs graph lbl sp lenv carry mem trace
152           [destr1 ; destr2] [v1 ; v2]
153
154       | RTL.St_op1 (op1, destr, srcr, lbl) ->
155         let v = Eval.op1 op1 (get_local_value lenv srcr) in
156         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
157
158       | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
159         let (v, carry) =
160           Eval.op2 carry op2
161             (get_local_value lenv srcr1)
162             (get_local_value lenv srcr2) in
163         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
164
165       | RTL.St_clear_carry lbl ->
166         State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
167
168       | RTL.St_set_carry lbl ->
169         State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
170
171       | RTL.St_load (destr, addr1, addr2, lbl) ->
172         let addr = get_local_addr lenv addr1 addr2 in
173         let v = Mem.load mem chunk addr in
174         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
175
176       | RTL.St_store (addr1, addr2, srcr, lbl) ->
177         let addr = get_local_addr lenv addr1 addr2 in
178         let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
179         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
180
181       | RTL.St_call_id (f, args, ret_regs, lbl) ->
182         let f_def = find_function mem f in
183         let args = get_arg_values lenv args in
184         let sf =
185           { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
186             sp = sp ; lenv = lenv ; carry = carry }
187         in
188         CallState (sf :: sfrs, f_def, args, mem, trace)
189
190       | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
191         let addr = get_local_addr lenv f1 f2 in
192         let f_def = Mem.find_fun_def mem addr in
193         let args = get_arg_values lenv args in
194         let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
195                    sp = sp ; lenv = lenv ; carry = carry } in
196         CallState (sf :: sfrs, f_def, args, mem, trace)
197
198       | RTL.St_tailcall_id (f, args) ->
199         let f_def = find_function mem f in
200         let args = get_arg_values lenv args in
201         let mem = Mem.free mem sp in
202         CallState (sfrs, f_def, args, mem, trace)
203
204       | RTL.St_tailcall_ptr (f1, f2, args) ->
205         let addr = get_local_addr lenv f1 f2 in
206         let f_def = Mem.find_fun_def mem addr in
207         let args = get_arg_values lenv args in
208         let mem = Mem.free mem sp in
209         CallState (sfrs, f_def, args, mem, trace)
210
211       | RTL.St_cond (srcr, lbl_true, lbl_false) ->
212         let v = get_local_value lenv srcr in
213         branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
214
215       | RTL.St_return rl ->
216         let vl = List.map (get_local_value lenv) rl in
217         let mem = Mem.free mem sp in
218         ReturnState (sfrs, vl, mem, trace)
219
220
221 module InterpretExternal = Primitive.Interpret (Mem)
222
223 let interpret_external mem f args = match InterpretExternal.t mem f args with
224   | (mem', InterpretExternal.V vs) -> (mem', vs)
225   | (mem', InterpretExternal.A addr) -> (mem', addr)
226
227 let init_locals
228     (locals : Register.Set.t)
229     (params : Register.t list)
230     (args   : Val.t list) :
231     local_env =
232   let f r lenv = Register.Map.add r Val.undef lenv in
233   let lenv = Register.Set.fold f locals Register.Map.empty in
234   let f lenv r v = Register.Map.add r v lenv in
235   List.fold_left2 f lenv params args
236
237 let state_after_call
238     (sfrs  : stack_frame list)
239     (f_def : RTL.function_def)
240     (args  : Val.t list)
241     (mem   : memory)
242     (trace : CostLabel.t list) :
243     state =
244   match f_def with
245     | RTL.F_int def ->
246       let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
247       State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
248              init_locals def.RTL.f_locals def.RTL.f_params args,
249              Val.undef, mem', trace)
250     | RTL.F_ext def ->
251       let (mem', vs) = interpret_external mem def.AST.ef_tag args in
252       ReturnState (sfrs, vs, mem', trace)
253
254 let state_after_return
255     (sf       : stack_frame)
256     (sfrs     : stack_frame list)
257     (ret_vals : Val.t list)
258     (mem      : memory)
259     (trace    : CostLabel.t list) :
260     state =
261   let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
262   let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
263   State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
264
265
266 let small_step (st : state) : state = match st with
267   | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
268     let stmt = Label.Map.find pc graph in
269     interpret_statement sfrs graph sp lenv carry mem stmt trace
270   | CallState (sfrs, f_def, args, mem, trace) ->
271     state_after_call sfrs f_def args mem trace
272   | ReturnState ([], ret_vals, mem, trace) ->
273     assert false (* End of execution; handled in iter_small_step. *)
274   | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
275     state_after_return sf sfrs ret_vals mem trace
276
277
278 let compute_result vs =
279   let f res v = res && (Val.is_int v) in
280   let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
281   if is_int vs then
282     let chunks =
283       List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
284     IntValue.Int32.merge chunks
285   else IntValue.Int32.zero
286
287 let rec iter_small_step debug st =
288   let print_and_return_result (res, cost_labels) =
289     if debug then Printf.printf "Result = %s\n%!"
290       (IntValue.Int32.to_string res) ;
291     (res, cost_labels) in
292   if debug then print_state st ;
293   match small_step st with
294     | ReturnState ([], vs, mem, trace) ->
295       print_and_return_result (compute_result vs, List.rev trace)
296     | st' -> iter_small_step debug st'
297
298
299 let add_global_vars =
300   List.fold_left
301     (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
302
303 let add_fun_defs =
304   List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
305
306
307 (* The memory is initialized by loading the code into it, and by reserving space
308    for the global variables. *)
309
310 let init_mem (p : RTL.program) : memory =
311   add_global_vars (add_fun_defs Mem.empty p.RTL.functs) p.RTL.vars
312
313
314 (* Interpret the program only if it has a main. *)
315
316 let interpret debug p =
317   Printf.printf "*** RTL interpret ***\n%!" ;
318   match p.RTL.main with
319     | None -> (IntValue.Int32.zero, [])
320     | Some main ->
321       let mem = init_mem p in
322       let main_def = find_function mem main in
323       let st = CallState ([], main_def, [], mem, []) in
324       iter_small_step debug st