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

Last change on this file since 1357 was 1357, checked in by tranquil, 9 years ago
  • changed implementation of constant indexings with extensible arrays
  • work on ASM completed
  • next: optimizations!
File size: 12.3 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
134(* Interpret statements. *)
135
136let interpret_statement
137    (sfrs  : stack_frame list)
138    (graph : RTLabs.graph)
139    (sp    : Val.address)
140    (lenv  : local_env)
141    (mem   : memory)
142    (stmt  : RTLabs.statement)
143                (inds  : indexing list)
144    (trace : CostLabel.t list) :
145    state = match stmt with
146
147      | RTLabs.St_skip lbl ->
148        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
149
150      | RTLabs.St_cost (cost_lbl, lbl) ->
151  let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in 
152        State (sfrs, graph, sp, lbl, lenv, mem, inds, cost_lbl :: trace)
153       
154            | RTLabs.St_ind_0 (i, lbl) ->
155        CostLabel.enter_loop inds i; 
156  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
157
158      | RTLabs.St_ind_inc (i, lbl) ->
159  CostLabel.continue_loop inds i; 
160  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
161
162      | RTLabs.St_cst (destr, cst, lbl) ->
163        let v = Eval.cst mem sp (get_type lenv destr) cst in
164        assign_state sfrs graph sp lbl lenv mem inds trace destr v
165
166      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
167        let v =
168          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
169            (get_value lenv srcr) in
170        assign_state sfrs graph sp lbl lenv mem inds trace destr v
171
172      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
173        let v =
174          Eval.op2
175            (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2)
176            op2
177            (get_value lenv srcr1)
178            (get_value lenv srcr2) in
179        assign_state sfrs graph sp lbl lenv mem inds trace destr v
180
181      | RTLabs.St_load (q, addr, destr, lbl) ->
182        let addr = address_of_value (get_value lenv addr) in
183        let v = Mem.loadq mem q addr in
184        assign_state sfrs graph sp lbl lenv mem inds trace destr v
185
186      | RTLabs.St_store (q, addr, srcr, lbl) ->
187        let addr = address_of_value (get_value lenv addr) in
188        let v = get_value lenv srcr in
189        let mem = Mem.storeq mem q addr v in
190        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
191
192      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
193        let f_def = find_function mem f in
194        let args = get_args lenv args in
195        (* Save the stack frame. *)
196        let sf =
197          {ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv} in
198        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
199
200      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
201        let addr = get_value lenv r in
202        let f_def = Mem.find_fun_def mem (address_of_value addr) in
203        let args = get_args lenv args in
204        (* Save the stack frame. *)
205        let sf =
206          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
207        in
208        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
209
210      | RTLabs.St_tailcall_id (f, args, sg) ->
211        let f_def = find_function mem f in
212        let args = get_args lenv args in
213        (* No need to save the stack frame. But free the stack. *)
214        let mem = Mem.free mem sp in
215        CallState (sfrs, f_def, args, mem, inds, trace)
216
217      | RTLabs.St_tailcall_ptr (r, args, sg) ->
218        let addr = get_value lenv r in
219        let f_def = Mem.find_fun_def mem (address_of_value addr) 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_cond (srcr, lbl_true, lbl_false) ->
226        let v = get_value lenv srcr in
227        branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v
228
229(*
230      | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) ->
231        let v = Eval.cst mem sp t cst in
232        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
233
234      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
235        let v =
236          Eval.op1 (get_type lenv srcr) (get_type lenv srcr)
237            op1 (get_value lenv srcr) in
238        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
239
240      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
241        let v =
242          Eval.op2 op2
243            (get_value lenv srcr1)
244            (get_value lenv srcr2) in
245        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
246*)
247
248      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
249      (*
250        let i = match get_value lenv r with
251        | Val.Val_int i -> i
252        | Val.Val_ptr _ -> error "Illegal cast from pointer to integer."
253        | _ -> error "Typing error." in
254        (try
255        let next_lbl = List.nth table i in
256        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
257        with
258        | Failure "nth" | Invalid_argument "List.nth" ->
259        error "Index out of jumptable.")
260      *)
261
262      | RTLabs.St_return None ->
263        let mem = Mem.free mem sp in
264        ReturnState (sfrs, Val.undef, mem, inds, trace)
265
266      | RTLabs.St_return (Some r) ->
267        let v = get_value lenv r in
268        let mem = Mem.free mem sp in
269        ReturnState (sfrs, v, mem, inds, trace)
270
271
272module InterpretExternal = Primitive.Interpret (Mem)
273
274let interpret_external mem f args = match InterpretExternal.t mem f args with
275  | (mem', InterpretExternal.V vs) ->
276    let v = if List.length vs = 0 then Val.undef else List.hd vs in
277    (mem', v)
278  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
279
280
281let init_locals
282    (locals           : (Register.t * AST.sig_type) list)
283    (params           : (Register.t * AST.sig_type) list)
284    (args             : Val.t list) :
285    local_env =
286  let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in
287  let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in
288  let lenv = List.fold_left2 f_param Register.Map.empty params args in
289  List.fold_left f_local lenv locals
290
291let state_after_call
292    (sfrs  : stack_frame list)
293    (f_def : RTLabs.function_def)
294    (args  : Val.t list)
295    (mem   : memory)
296                (inds  : indexing list)
297    (trace : CostLabel.t list) :
298    state =
299  match f_def with
300    | RTLabs.F_int def ->
301      let (mem', sp) =
302        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
303      let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
304            (* allocate new constant indexing *)
305                        let graph = def.RTLabs.f_graph in
306                        let inds = new_ind inds in
307      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
308    | RTLabs.F_ext def ->
309      let (mem', v) = interpret_external mem def.AST.ef_tag args in
310      ReturnState (sfrs, v, mem', inds, trace)
311
312
313let state_after_return
314    (sf      : stack_frame)
315    (sfrs    : stack_frame list)
316    (ret_val : Val.t)
317    (mem     : memory)
318                (inds    : indexing list)
319    (trace   : CostLabel.t list) :
320    state =
321  let lenv = match sf.ret_reg with
322    | None -> sf.lenv
323    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
324        (* erase current indexing and revert to previous one *)
325  let inds = forget_ind inds in
326  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, trace)
327
328
329let small_step (st : state) : state = match st with
330  | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) ->
331    let stmt = Label.Map.find pc graph in
332    interpret_statement sfrs graph sp lenv mem stmt inds trace
333  | CallState (sfrs, f_def, args, mem, inds, trace) ->
334    state_after_call sfrs f_def args mem inds trace
335  | ReturnState ([], ret_val, mem, inds, trace) ->
336    assert false (* End of execution; handled in iter_small_step. *)
337  | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) ->
338    state_after_return sf sfrs ret_val mem inds trace
339
340
341let compute_result v =
342  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
343  else IntValue.Int32.zero
344
345let rec iter_small_step debug st =
346  let print_and_return_result (res, cost_labels) =
347    if debug then Printf.printf "Result = %s\n%!"
348      (IntValue.Int32.to_string res) ;
349    (res, cost_labels) in
350  if debug then print_state st ;
351  match small_step st with
352    | ReturnState ([], v, mem, inds, trace) ->
353      print_and_return_result (compute_result v, List.rev trace)
354    | st' -> iter_small_step debug st'
355
356
357let add_global_vars =
358  List.fold_left (fun mem (id, size) -> Mem.add_var mem id size None)
359
360let add_fun_defs =
361  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
362
363
364(* The memory is initialized by loading the code into it, and by reserving space
365   for the global variables. *)
366
367let init_mem (p : RTLabs.program) : memory =
368  add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars
369
370
371(* Interpret the program only if it has a main. *)
372
373let interpret debug p =
374  Printf.printf "*** RTLabs interpret ***\n%!" ;
375  match p.RTLabs.main with
376    | None -> (IntValue.Int32.zero, [])
377    | Some main ->
378      let mem = init_mem p in
379      let main_def = find_function mem main in
380      let st = CallState ([], main_def, [], mem, [], []) in
381      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.