source: Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

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