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

Last change on this file since 1340 was 1340, checked in by tranquil, 8 years ago

work on RTLabs and RTL completed

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