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

Last change on this file since 1542 was 1542, checked in by tranquil, 9 years ago

merge of indexed labels branch

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