source: Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

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