source: Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsInterpret.ml @ 1477

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