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

Last change on this file since 1572 was 1572, checked in by tranquil, 9 years ago
  • corrected previous bug
  • finished propagating immediates
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
80
81let find_function mem f =
82  let addr = Mem.find_global mem f in
83  Mem.find_fun_def mem addr
84
85let 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
89let get_value = get_local_env fst
90
91let get_type = get_local_env snd
92
93let 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
97let 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
101let value_of_address = List.hd
102let address_of_value v = [v]
103
104
105module Eval = CminorInterpret.Eval_op (Mem)
106
107let concrete_stacksize = Eval.concrete_stacksize
108
109
110let 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
114let get_type_arg lenv = function
115  | RTLabs.Reg r -> get_type lenv r
116  | RTLabs.Imm (_, typ) -> typ
117
118let get_args lenv mem sp  args = List.map (eval_arg lenv mem sp) args
119
120(* Assign a value to some destinations registers. *)
121
122let 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
128let 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
136let curr_ind = CostLabel.curr_const_ind
137
138let forget_ind = CostLabel.forget_const_ind
139
140let new_ind = CostLabel.new_const_ind
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 =
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
287module InterpretExternal = Primitive.Interpret (Mem)
288
289let 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
296let 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
306let 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
328let 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
345let 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
357let compute_result v =
358  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
359  else IntValue.Int32.zero
360
361let 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
373let add_global_vars =
374  List.fold_left (fun mem (id, size) -> Mem.add_var mem id size None)
375
376let 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
383let 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
389let 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
Note: See TracBrowser for help on using the repository browser.