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