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 | type indexing = CostLabel.const_indexing |
---|
36 | |
---|
37 | (* Execution states. There are three possible states : |
---|
38 | - The constructor [State] represents a state when executing a function |
---|
39 | - The constructor [CallState] represents a state when calling a function |
---|
40 | - The constructor [ReturnState] represents a state when leaving a function *) |
---|
41 | |
---|
42 | type state = |
---|
43 | | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) * |
---|
44 | Label.t * local_env * memory * indexing list * CostLabel.t list |
---|
45 | | CallState of stack_frame list * RTLabs.function_def * |
---|
46 | Val.t list (* args *) * memory * indexing list * CostLabel.t list |
---|
47 | | ReturnState of stack_frame list * Val.t (* return value *) * |
---|
48 | memory * indexing list * CostLabel.t list |
---|
49 | |
---|
50 | let string_of_local_env lenv = |
---|
51 | let f x (v, _) s = |
---|
52 | s ^ |
---|
53 | (if Val.eq v Val.undef then "" |
---|
54 | else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in |
---|
55 | Register.Map.fold f lenv "" |
---|
56 | |
---|
57 | let string_of_args args = |
---|
58 | let f s v = s ^ " " ^ (Val.to_string v) in |
---|
59 | List.fold_left f "" args |
---|
60 | |
---|
61 | let print_state state = match state with |
---|
62 | | State (_, _, sp, lbl, lenv, mem, inds, _) -> |
---|
63 | Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:" |
---|
64 | (Val.string_of_address sp) |
---|
65 | (string_of_local_env lenv) |
---|
66 | (Mem.to_string mem); |
---|
67 | let i = CostLabel.curr_const_ind inds in |
---|
68 | CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i; |
---|
69 | Printf.printf "Regular state: %s\n\n%!" |
---|
70 | lbl |
---|
71 | | CallState (_, _, args, mem, _, _) -> |
---|
72 | Printf.printf "Memory:%s\nCall state: %s\n\n%!" |
---|
73 | (Mem.to_string mem) |
---|
74 | (string_of_args args) |
---|
75 | | ReturnState (_, v, mem, _, _) -> |
---|
76 | Printf.printf "Memory:%s\nReturn state: %s\n\n%!" |
---|
77 | (Mem.to_string mem) |
---|
78 | (Val.to_string v) |
---|
79 | |
---|
80 | |
---|
81 | let find_function mem f = |
---|
82 | let addr = Mem.find_global mem f in |
---|
83 | Mem.find_fun_def mem addr |
---|
84 | |
---|
85 | let get_local_env f lenv r = |
---|
86 | if Register.Map.mem r lenv then f (Register.Map.find r lenv) |
---|
87 | else error ("Unknown local register \"" ^ (Register.print r) ^ "\".") |
---|
88 | |
---|
89 | let get_value = get_local_env fst |
---|
90 | |
---|
91 | let get_type = get_local_env snd |
---|
92 | |
---|
93 | let update_local r v lenv = |
---|
94 | let f (_, t) = Register.Map.add r (v, t) lenv in |
---|
95 | get_local_env f lenv r |
---|
96 | |
---|
97 | let update_locals rs vs lenv = |
---|
98 | let f lenv r v = update_local r v lenv in |
---|
99 | List.fold_left2 f lenv rs vs |
---|
100 | |
---|
101 | let value_of_address = List.hd |
---|
102 | let address_of_value v = [v] |
---|
103 | |
---|
104 | |
---|
105 | module Eval = CminorInterpret.Eval_op (Mem) |
---|
106 | |
---|
107 | let concrete_stacksize = Eval.concrete_stacksize |
---|
108 | |
---|
109 | |
---|
110 | let eval_arg lenv mem sp = function |
---|
111 | | RTLabs.Reg r -> get_value lenv r |
---|
112 | | RTLabs.Imm (c, t) -> Eval.cst mem sp t c |
---|
113 | |
---|
114 | let get_type_arg lenv = function |
---|
115 | | RTLabs.Reg r -> get_type lenv r |
---|
116 | | RTLabs.Imm (_, typ) -> typ |
---|
117 | |
---|
118 | let get_args lenv mem sp args = List.map (eval_arg lenv mem sp) args |
---|
119 | |
---|
120 | (* Assign a value to some destinations registers. *) |
---|
121 | |
---|
122 | let assign_state sfrs graph sp lbl lenv mem inds trace destr v = |
---|
123 | let lenv = update_local destr v lenv in |
---|
124 | State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) |
---|
125 | |
---|
126 | (* Branch on a value. *) |
---|
127 | |
---|
128 | let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v = |
---|
129 | let next_lbl = |
---|
130 | if Val.is_true v then lbl_true |
---|
131 | else |
---|
132 | if Val.is_false v then lbl_false |
---|
133 | else error "Undefined conditional value." in |
---|
134 | State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace) |
---|
135 | |
---|
136 | let curr_ind = CostLabel.curr_const_ind |
---|
137 | |
---|
138 | let forget_ind = CostLabel.forget_const_ind |
---|
139 | |
---|
140 | let new_ind = CostLabel.new_const_ind |
---|
141 | |
---|
142 | (* Interpret statements. *) |
---|
143 | |
---|
144 | let interpret_statement |
---|
145 | (sfrs : stack_frame list) |
---|
146 | (graph : RTLabs.graph) |
---|
147 | (sp : Val.address) |
---|
148 | (lenv : local_env) |
---|
149 | (mem : memory) |
---|
150 | (stmt : RTLabs.statement) |
---|
151 | (inds : indexing list) |
---|
152 | (trace : CostLabel.t list) : |
---|
153 | state = match stmt with |
---|
154 | |
---|
155 | | RTLabs.St_skip lbl -> |
---|
156 | State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) |
---|
157 | |
---|
158 | | RTLabs.St_cost (cost_lbl, lbl) -> |
---|
159 | let cost_lbl = |
---|
160 | CostLabel.ev_indexing (curr_ind inds) cost_lbl in |
---|
161 | State (sfrs, graph, sp, lbl, lenv, |
---|
162 | mem, inds, cost_lbl :: trace) |
---|
163 | |
---|
164 | | RTLabs.St_ind_0 (i, lbl) -> |
---|
165 | CostLabel.enter_loop inds i; |
---|
166 | State (sfrs, graph, sp, lbl, lenv, |
---|
167 | mem, inds, trace) |
---|
168 | |
---|
169 | | RTLabs.St_ind_inc (i, lbl) -> |
---|
170 | CostLabel.continue_loop inds i; |
---|
171 | State (sfrs, graph, sp, lbl, lenv, |
---|
172 | mem, inds, trace) |
---|
173 | |
---|
174 | | RTLabs.St_cst (destr, cst, lbl) -> |
---|
175 | let v = Eval.cst mem sp (get_type lenv destr) cst in |
---|
176 | assign_state sfrs graph sp lbl lenv mem inds trace destr v |
---|
177 | |
---|
178 | | RTLabs.St_op1 (op1, destr, srcr, lbl) -> |
---|
179 | let v = |
---|
180 | Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1 |
---|
181 | (get_value lenv srcr) in |
---|
182 | assign_state sfrs graph sp lbl lenv mem inds trace destr v |
---|
183 | |
---|
184 | | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> |
---|
185 | let v = |
---|
186 | Eval.op2 |
---|
187 | (get_type lenv destr) |
---|
188 | (get_type_arg lenv srcr1) |
---|
189 | (get_type_arg lenv srcr2) |
---|
190 | op2 |
---|
191 | (eval_arg lenv mem sp srcr1) |
---|
192 | (eval_arg lenv mem sp srcr2) in |
---|
193 | assign_state sfrs graph sp lbl lenv mem inds trace destr v |
---|
194 | |
---|
195 | | RTLabs.St_load (q, addr, destr, lbl) -> |
---|
196 | let addr = address_of_value (eval_arg lenv mem sp addr) in |
---|
197 | let v = Mem.loadq mem q addr in |
---|
198 | assign_state sfrs graph sp lbl lenv mem inds trace destr v |
---|
199 | |
---|
200 | | RTLabs.St_store (q, addr, srcr, lbl) -> |
---|
201 | let addr = address_of_value (eval_arg lenv mem sp addr) in |
---|
202 | let v = eval_arg lenv mem sp srcr in |
---|
203 | let mem = Mem.storeq mem q addr v in |
---|
204 | State (sfrs, graph, sp, lbl, lenv, mem, inds, trace) |
---|
205 | |
---|
206 | | RTLabs.St_call_id (f, args, destr, sg, lbl) -> |
---|
207 | let f_def = find_function mem f in |
---|
208 | let args = get_args lenv mem sp args in |
---|
209 | (* Save the stack frame. *) |
---|
210 | let sf = |
---|
211 | { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } |
---|
212 | in |
---|
213 | CallState (sf :: sfrs, f_def, args, mem, inds, trace) |
---|
214 | |
---|
215 | | RTLabs.St_call_ptr (r, args, destr, sg, lbl) -> |
---|
216 | let addr = get_value lenv r in |
---|
217 | let f_def = Mem.find_fun_def mem (address_of_value addr) in |
---|
218 | let args = get_args lenv mem sp args in |
---|
219 | (* Save the stack frame. *) |
---|
220 | let sf = |
---|
221 | { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } |
---|
222 | in |
---|
223 | CallState (sf :: sfrs, f_def, args, mem, inds, trace) |
---|
224 | |
---|
225 | | RTLabs.St_tailcall_id (f, args, sg) -> |
---|
226 | let f_def = find_function mem f in |
---|
227 | let args = get_args lenv mem sp args in |
---|
228 | (* No need to save the stack frame. But free the stack. *) |
---|
229 | let mem = Mem.free mem sp in |
---|
230 | CallState (sfrs, f_def, args, mem, inds, trace) |
---|
231 | |
---|
232 | | RTLabs.St_tailcall_ptr (r, args, sg) -> |
---|
233 | let addr = get_value lenv r in |
---|
234 | let f_def = Mem.find_fun_def mem (address_of_value addr) in |
---|
235 | let args = get_args lenv mem sp args in |
---|
236 | (* No need to save the stack frame. But free the stack. *) |
---|
237 | let mem = Mem.free mem sp in |
---|
238 | CallState (sfrs, f_def, args, mem, inds, trace) |
---|
239 | |
---|
240 | | RTLabs.St_cond (srcr, lbl_true, lbl_false) -> |
---|
241 | let v = get_value lenv srcr in |
---|
242 | branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v |
---|
243 | |
---|
244 | (* |
---|
245 | | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) -> |
---|
246 | let v = Eval.cst mem sp t cst in |
---|
247 | branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v |
---|
248 | |
---|
249 | | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) -> |
---|
250 | let v = |
---|
251 | Eval.op1 (get_type lenv srcr) (get_type lenv srcr) |
---|
252 | op1 (get_value lenv srcr) in |
---|
253 | branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v |
---|
254 | |
---|
255 | | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) -> |
---|
256 | let v = |
---|
257 | Eval.op2 op2 |
---|
258 | (get_value lenv srcr1) |
---|
259 | (get_value lenv srcr2) in |
---|
260 | branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v |
---|
261 | *) |
---|
262 | |
---|
263 | | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *) |
---|
264 | (* |
---|
265 | let i = match get_value lenv r with |
---|
266 | | Val.Val_int i -> i |
---|
267 | | Val.Val_ptr _ -> error "Illegal cast from pointer to integer." |
---|
268 | | _ -> error "Typing error." in |
---|
269 | (try |
---|
270 | let next_lbl = List.nth table i in |
---|
271 | State (sfrs, graph, sp, next_lbl, lenv, mem, trace) |
---|
272 | with |
---|
273 | | Failure "nth" | Invalid_argument "List.nth" -> |
---|
274 | error "Index out of jumptable.") |
---|
275 | *) |
---|
276 | |
---|
277 | | RTLabs.St_return None -> |
---|
278 | let mem = Mem.free mem sp in |
---|
279 | ReturnState (sfrs, Val.undef, mem, inds, trace) |
---|
280 | |
---|
281 | | RTLabs.St_return (Some r) -> |
---|
282 | let v = eval_arg lenv mem sp r in |
---|
283 | let mem = Mem.free mem sp in |
---|
284 | ReturnState (sfrs, v, mem, inds, trace) |
---|
285 | |
---|
286 | |
---|
287 | module InterpretExternal = Primitive.Interpret (Mem) |
---|
288 | |
---|
289 | let interpret_external mem f args = match InterpretExternal.t mem f args with |
---|
290 | | (mem', InterpretExternal.V vs) -> |
---|
291 | let v = if List.length vs = 0 then Val.undef else List.hd vs in |
---|
292 | (mem', v) |
---|
293 | | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) |
---|
294 | |
---|
295 | |
---|
296 | let init_locals |
---|
297 | (locals : (Register.t * AST.sig_type) list) |
---|
298 | (params : (Register.t * AST.sig_type) list) |
---|
299 | (args : Val.t list) : |
---|
300 | local_env = |
---|
301 | let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in |
---|
302 | let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in |
---|
303 | let lenv = List.fold_left2 f_param Register.Map.empty params args in |
---|
304 | List.fold_left f_local lenv locals |
---|
305 | |
---|
306 | let state_after_call |
---|
307 | (sfrs : stack_frame list) |
---|
308 | (f_def : RTLabs.function_def) |
---|
309 | (args : Val.t list) |
---|
310 | (mem : memory) |
---|
311 | (inds : indexing list) |
---|
312 | (trace : CostLabel.t list) : |
---|
313 | state = |
---|
314 | match f_def with |
---|
315 | | RTLabs.F_int def -> |
---|
316 | let (mem', sp) = |
---|
317 | Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in |
---|
318 | let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in |
---|
319 | (* allocate new constant indexing *) |
---|
320 | let graph = def.RTLabs.f_graph in |
---|
321 | let inds = new_ind inds in |
---|
322 | State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace) |
---|
323 | | RTLabs.F_ext def -> |
---|
324 | let (mem', v) = interpret_external mem def.AST.ef_tag args in |
---|
325 | ReturnState (sfrs, v, mem', inds, trace) |
---|
326 | |
---|
327 | |
---|
328 | let state_after_return |
---|
329 | (sf : stack_frame) |
---|
330 | (sfrs : stack_frame list) |
---|
331 | (ret_val : Val.t) |
---|
332 | (mem : memory) |
---|
333 | (inds : indexing list) |
---|
334 | (trace : CostLabel.t list) : |
---|
335 | state = |
---|
336 | let lenv = match sf.ret_reg with |
---|
337 | | None -> sf.lenv |
---|
338 | | Some ret_reg -> update_local ret_reg ret_val sf.lenv in |
---|
339 | (* erase current indexing and revert to previous one *) |
---|
340 | let inds = forget_ind inds in |
---|
341 | State (sfrs, sf.graph, sf.sp, sf.pc, lenv, |
---|
342 | mem, inds, trace) |
---|
343 | |
---|
344 | |
---|
345 | let small_step (st : state) : state = match st with |
---|
346 | | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) -> |
---|
347 | let stmt = Label.Map.find pc graph in |
---|
348 | interpret_statement sfrs graph sp lenv mem stmt inds trace |
---|
349 | | CallState (sfrs, f_def, args, mem, inds, trace) -> |
---|
350 | state_after_call sfrs f_def args mem inds trace |
---|
351 | | ReturnState ([], ret_val, mem, inds, trace) -> |
---|
352 | assert false (* End of execution; handled in iter_small_step. *) |
---|
353 | | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) -> |
---|
354 | state_after_return sf sfrs ret_val mem inds trace |
---|
355 | |
---|
356 | |
---|
357 | let compute_result v = |
---|
358 | if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v) |
---|
359 | else IntValue.Int32.zero |
---|
360 | |
---|
361 | let rec iter_small_step debug st = |
---|
362 | let print_and_return_result (res, cost_labels) = |
---|
363 | if debug then Printf.printf "Result = %s\n%!" |
---|
364 | (IntValue.Int32.to_string res) ; |
---|
365 | (res, cost_labels) in |
---|
366 | if debug then print_state st ; |
---|
367 | match small_step st with |
---|
368 | | ReturnState ([], v, mem, inds, trace) -> |
---|
369 | print_and_return_result (compute_result v, List.rev trace) |
---|
370 | | st' -> iter_small_step debug st' |
---|
371 | |
---|
372 | |
---|
373 | let add_global_vars = |
---|
374 | List.fold_left (fun mem (id, size) -> Mem.add_var mem id size None) |
---|
375 | |
---|
376 | let add_fun_defs = |
---|
377 | List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def) |
---|
378 | |
---|
379 | |
---|
380 | (* The memory is initialized by loading the code into it, and by reserving space |
---|
381 | for the global variables. *) |
---|
382 | |
---|
383 | let init_mem (p : RTLabs.program) : memory = |
---|
384 | add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars |
---|
385 | |
---|
386 | |
---|
387 | (* Interpret the program only if it has a main. *) |
---|
388 | |
---|
389 | let interpret debug p = |
---|
390 | Printf.printf "*** RTLabs interpret ***\n%!" ; |
---|
391 | match p.RTLabs.main with |
---|
392 | | None -> (IntValue.Int32.zero, []) |
---|
393 | | Some main -> |
---|
394 | let mem = init_mem p in |
---|
395 | let main_def = find_function mem main in |
---|
396 | let st = CallState ([], main_def, [], mem, [], []) in |
---|
397 | iter_small_step debug st |
---|