source: Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLInterpret.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: 11.9 KB
Line 
1
2(** This module provides an interpreter for the RTL language. *)
3
4
5let error_prefix = "RTL interpret"
6let error s = Error.global_error error_prefix s
7
8
9module Mem = Driver.RTLMemory
10module Val = Mem.Value
11let chunk = Driver.RTLMemory.int_size
12module Eval = I8051.Eval (Val)
13
14
15type memory = RTL.function_def Mem.memory
16
17
18(* Local environments. They associate a value to the registers of the function
19   being executed. *)
20
21type local_env = Val.t 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 node, the local environment and the value of the carry to resume
26   the execution of the caller. *)
27
28type stack_frame =
29    { ret_regs : Register.t list ;
30      graph    : RTL.graph ;
31      pc       : Label.t ;
32      sp       : Val.address ;
33      lenv     : local_env ;
34      carry    : Val.t }
35
36type indexing = CostLabel.const_indexing
37
38(* Execution states. There are three possible states :
39   - The constructor [State] represents a state when executing a function
40   - The constructor [CallState] represents a state when calling a function
41   - The constructor [ReturnState] represents a state when leaving a function *)
42
43type state =
44  | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
45             local_env * Val.t (* carry *) * memory * indexing list *
46                                                 CostLabel.t list
47  | CallState of stack_frame list * RTL.function_def *
48              Val.t list (* args *) * memory * indexing list * CostLabel.t list
49  | ReturnState of stack_frame list * Val.t list (* return values *) *
50                   memory * indexing list * CostLabel.t list
51
52let string_of_local_env lenv =
53  let f x v s =
54    s ^
55      (if Val.eq v Val.undef then ""
56       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
57  Register.Map.fold f lenv ""
58
59let string_of_args args =
60  let f s v = s ^ " " ^ (Val.to_string v) in
61  List.fold_left f "" args
62
63let print_state = function
64  | State (_, _, lbl, sp, lenv, carry, mem, ind::_, _) ->
65    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
66      (Val.string_of_address sp)
67      (Val.to_string carry)
68      (string_of_local_env lenv)
69      (Mem.to_string mem);
70                        Array.iter (fun a -> Printf.printf "%d, " a) ind;
71                        Printf.printf "Regular state: %s\n\n%!"
72      lbl
73        | State (_, _, _, _, _, _, _, [], _) -> assert false (* indexings non-empty *)
74  | CallState (_, _, args, mem, _, _) ->
75    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
76      (Mem.to_string mem)
77      (string_of_args args)
78  | ReturnState (_, vs, mem, _, _) ->
79    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
80      (Mem.to_string mem)
81      (string_of_args vs)
82
83
84let find_function mem f =
85  let addr = Mem.find_global mem f in
86  Mem.find_fun_def mem addr
87
88let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
89  if Register.Map.mem r lenv then Register.Map.find r lenv
90  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
91let get_arg_values lenv args = List.map (get_local_value lenv) args
92
93let get_local_addr lenv f1 f2 =
94  List.map (get_local_value lenv) [f1 ; f2]
95
96
97let adds rs vs lenv =
98  let f lenv r v = Register.Map.add r v lenv in
99  List.fold_left2 f lenv rs vs
100
101
102(* Assign a value to some destinations registers. *)
103
104let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs =
105  let lenv = adds destrs vs lenv in
106  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
107
108(* Branch on a value. *)
109
110let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v =
111  let next_lbl =
112    if Val.is_true v then lbl_true
113    else
114      if Val.is_false v then lbl_false
115      else error "Undefined conditional value." in
116  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace)
117
118let curr_ind : indexing list -> indexing = function
119    | ind :: _ -> ind
120    | _ -> assert false (* indexing list must be non-empty *) 
121
122let forget_ind : indexing list -> indexing list = function
123    | _ :: tail -> tail
124    | _ -> assert false (* indexing list must be non-empty *)
125
126let max_depth graph =
127    let f_stmt _ = function
128        | RTL.St_ind_0(i,_) | RTL.St_ind_inc(i,_) -> max (i + 1) 
129        | _ -> fun x -> x in
130    Label.Map.fold f_stmt graph 0 
131
132
133(* Interpret statements. *)
134
135let interpret_statement
136    (sfrs  : stack_frame list)
137    (graph : RTL.graph)
138    (sp    : Val.address)
139    (lenv  : local_env)
140    (carry : Val.t)
141    (mem   : memory)
142                (inds  : indexing list)
143    (stmt  : RTL.statement)
144    (trace : CostLabel.t list) :
145    state = match stmt with
146
147      | RTL.St_skip lbl ->
148        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
149
150      | RTL.St_cost (cost_lbl, lbl) ->
151        let cost_lbl = CostLabel.apply_const_indexing (curr_ind inds) cost_lbl in
152        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
153
154      | RTL.St_ind_0 (i, lbl) ->
155  CostLabel.enter_loop (Some i) (curr_ind inds); 
156  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
157
158      | RTL.St_ind_inc (i, lbl) ->
159  CostLabel.continue_loop (Some i) (curr_ind inds); 
160  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
161
162      | RTL.St_addr (r1, r2, x, lbl) ->
163        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2]
164          (Mem.find_global mem x)
165
166      | RTL.St_stackaddr (r1, r2, lbl) ->
167        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
168
169      | RTL.St_int (r, i, lbl) ->
170        assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
171
172      | RTL.St_move (destr, srcr, lbl) ->
173        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
174          [get_local_value lenv srcr]
175
176      | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
177        let (v1, v2) =
178          Eval.opaccs opaccs
179            (get_local_value lenv srcr1)
180            (get_local_value lenv srcr2) in
181        assign_state sfrs graph lbl sp lenv carry mem inds trace
182          [destr1 ; destr2] [v1 ; v2]
183
184      | RTL.St_op1 (op1, destr, srcr, lbl) ->
185        let v = Eval.op1 op1 (get_local_value lenv srcr) in
186        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
187
188      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
189        let (v, carry) =
190          Eval.op2 carry op2
191            (get_local_value lenv srcr1)
192            (get_local_value lenv srcr2) in
193        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
194
195      | RTL.St_clear_carry lbl ->
196        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace)
197
198      | RTL.St_set_carry lbl ->
199        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace)
200
201      | RTL.St_load (destr, addr1, addr2, lbl) ->
202        let addr = get_local_addr lenv addr1 addr2 in
203        let v = Mem.load mem chunk addr in
204        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
205
206      | RTL.St_store (addr1, addr2, srcr, lbl) ->
207        let addr = get_local_addr lenv addr1 addr2 in
208        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
209        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
210
211      | RTL.St_call_id (f, args, ret_regs, lbl) ->
212        let f_def = find_function mem f in
213        let args = get_arg_values lenv args in
214        let sf =
215          { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
216            sp = sp ; lenv = lenv ; carry = carry }
217        in
218        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
219
220      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
221        let addr = get_local_addr lenv f1 f2 in
222        let f_def = Mem.find_fun_def mem addr in
223        let args = get_arg_values lenv args in
224        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
225                   sp = sp ; lenv = lenv ; carry = carry } in
226        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
227
228      | RTL.St_tailcall_id (f, args) ->
229        let f_def = find_function mem f in
230        let args = get_arg_values lenv args in
231        let mem = Mem.free mem sp in
232        CallState (sfrs, f_def, args, mem, inds, trace)
233
234      | RTL.St_tailcall_ptr (f1, f2, args) ->
235        let addr = get_local_addr lenv f1 f2 in
236        let f_def = Mem.find_fun_def mem addr in
237        let args = get_arg_values lenv args in
238        let mem = Mem.free mem sp in
239        CallState (sfrs, f_def, args, mem, inds, trace)
240
241      | RTL.St_cond (srcr, lbl_true, lbl_false) ->
242        let v = get_local_value lenv srcr in
243        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
244
245      | RTL.St_return rl ->
246        let vl = List.map (get_local_value lenv) rl in
247        let mem = Mem.free mem sp in
248        ReturnState (sfrs, vl, mem, inds, trace)
249
250
251module InterpretExternal = Primitive.Interpret (Mem)
252
253let interpret_external mem f args = match InterpretExternal.t mem f args with
254  | (mem', InterpretExternal.V vs) -> (mem', vs)
255  | (mem', InterpretExternal.A addr) -> (mem', addr)
256
257let init_locals
258    (locals : Register.Set.t)
259    (params : Register.t list)
260    (args   : Val.t list) :
261    local_env =
262  let f r lenv = Register.Map.add r Val.undef lenv in
263  let lenv = Register.Set.fold f locals Register.Map.empty in
264  let f lenv r v = Register.Map.add r v lenv in
265  List.fold_left2 f lenv params args
266
267let state_after_call
268    (sfrs  : stack_frame list)
269    (f_def : RTL.function_def)
270    (args  : Val.t list)
271    (mem   : memory)
272                (inds  : indexing list)
273    (trace : CostLabel.t list) :
274    state =
275  match f_def with
276    | RTL.F_int def ->
277                        let ind = Array.make (max_depth def.RTL.f_graph) 0 in
278      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
279      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
280             init_locals def.RTL.f_locals def.RTL.f_params args,
281             Val.undef, mem', ind::inds, trace)
282    | RTL.F_ext def ->
283      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
284      ReturnState (sfrs, vs, mem', inds, trace)
285
286let state_after_return
287    (sf       : stack_frame)
288    (sfrs     : stack_frame list)
289    (ret_vals : Val.t list)
290    (mem      : memory)
291                (inds     : indexing list)
292    (trace    : CostLabel.t list) :
293    state =
294  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
295  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
296        let inds = forget_ind inds in
297  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
298
299
300let small_step (st : state) : state = match st with
301  | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) ->
302    let stmt = Label.Map.find pc graph in
303    interpret_statement sfrs graph sp lenv carry mem inds stmt trace
304  | CallState (sfrs, f_def, args, mem, inds, trace) ->
305    state_after_call sfrs f_def args mem inds trace
306  | ReturnState ([], ret_vals, mem, inds, trace) ->
307    assert false (* End of execution; handled in iter_small_step. *)
308  | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) ->
309    state_after_return sf sfrs ret_vals mem inds trace
310
311
312let compute_result vs =
313  let f res v = res && (Val.is_int v) in
314  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
315  if is_int vs then
316    let chunks =
317      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
318    IntValue.Int32.merge chunks
319  else IntValue.Int32.zero
320
321let rec iter_small_step debug st =
322  let print_and_return_result (res, cost_labels) =
323    if debug then Printf.printf "Result = %s\n%!"
324      (IntValue.Int32.to_string res) ;
325    (res, cost_labels) in
326  if debug then print_state st ;
327  match small_step st with
328    | ReturnState ([], vs, mem, _, trace) ->
329      print_and_return_result (compute_result vs, trace)
330    | st' -> iter_small_step debug st'
331
332
333let add_global_vars =
334  List.fold_left
335    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
336
337let add_fun_defs =
338  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
339
340
341(* The memory is initialized by loading the code into it, and by reserving space
342   for the global variables. *)
343
344let init_mem (p : RTL.program) : memory =
345  add_global_vars (add_fun_defs Mem.empty p.RTL.functs) p.RTL.vars
346
347
348(* Interpret the program only if it has a main. *)
349
350let interpret debug p =
351  Printf.printf "*** RTL interpret ***\n%!" ;
352  match p.RTL.main with
353    | None -> (IntValue.Int32.zero, [])
354    | Some main ->
355      let mem = init_mem p in
356      let main_def = find_function mem main in
357      let st = CallState ([], main_def, [], mem, [], []) in
358      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.