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

Last change on this file since 1568 was 1568, checked in by tranquil, 8 years ago
  • Immediates introduced (but not fully used yet in RTLabs to RTL pass)
  • translation streamlined
  • BUGGY: interpretation fails in LTL, trying to fetch a function with incorrect address
File size: 11.7 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    let i = CostLabel.curr_const_ind ind in
71    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
72    Printf.printf "Regular state: %s\n\n%!"
73      lbl
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) ^ "\".")
91
92let get_local_arg_value (lenv : local_env) : RTL.argument -> Val.t = function
93  | RTL.Reg r -> get_local_value lenv r
94  | RTL.Imm i -> Val.of_int i
95
96let get_arg_values lenv args = List.map (get_local_value lenv) args
97
98let get_local_addr lenv f1 f2 =
99  List.map (get_local_value lenv) [f1 ; f2]
100
101
102let adds rs vs lenv =
103  let f lenv r v = Register.Map.add r v lenv in
104  List.fold_left2 f lenv rs vs
105
106
107(* Assign a value to some destinations registers. *)
108
109let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs =
110  let lenv = adds destrs vs lenv in
111  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
112
113(* Branch on a value. *)
114
115let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v =
116  let next_lbl =
117    if Val.is_true v then lbl_true
118    else
119      if Val.is_false v then lbl_false
120      else error "Undefined conditional value." in
121  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace)
122
123let curr_ind = CostLabel.curr_const_ind
124
125let forget_ind = CostLabel.forget_const_ind
126
127let new_ind = CostLabel.new_const_ind
128
129
130(* Interpret statements. *)
131
132let interpret_statement
133    (sfrs  : stack_frame list)
134    (graph : RTL.graph)
135    (sp    : Val.address)
136    (lenv  : local_env)
137    (carry : Val.t)
138    (mem   : memory)
139    (inds  : indexing list)
140    (stmt  : RTL.statement)
141    (trace : CostLabel.t list) :
142    state = match stmt with
143
144      | RTL.St_skip lbl ->
145        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
146
147      | RTL.St_cost (cost_lbl, lbl) ->
148        let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
149        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
150
151      | RTL.St_ind_0 (i, lbl) ->
152        CostLabel.enter_loop inds i; 
153        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
154
155      | RTL.St_ind_inc (i, lbl) ->
156        CostLabel.continue_loop inds i; 
157        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
158
159      | RTL.St_addr (r1, r2, x, lbl) ->
160        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2]
161          (Mem.find_global mem x)
162
163      | RTL.St_stackaddr (r1, r2, lbl) ->
164        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
165
166      (* | RTL.St_int (r, i, lbl) -> *)
167      (*   assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] *)
168
169      | RTL.St_move (destr, srcr, lbl) ->
170        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
171          [get_local_arg_value lenv srcr]
172
173      | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
174        let (v1, v2) =
175          Eval.opaccs opaccs
176            (get_local_value lenv srcr1)
177            (get_local_value lenv srcr2) in
178        assign_state sfrs graph lbl sp lenv carry mem inds trace
179          [destr1 ; destr2] [v1 ; v2]
180
181      | RTL.St_op1 (op1, destr, srcr, lbl) ->
182        let v = Eval.op1 op1 (get_local_value lenv srcr) in
183        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
184
185      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
186        let (v, carry) =
187          Eval.op2 carry op2
188            (get_local_value lenv srcr1)
189            (get_local_arg_value lenv srcr2) in
190        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
191
192      | RTL.St_clear_carry lbl ->
193        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace)
194
195      | RTL.St_set_carry lbl ->
196        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace)
197
198      | RTL.St_load (destr, addr1, addr2, lbl) ->
199        let addr = get_local_addr lenv addr1 addr2 in
200        let v = Mem.load mem chunk addr in
201        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
202
203      | RTL.St_store (addr1, addr2, srcr, lbl) ->
204        let addr = get_local_addr lenv addr1 addr2 in
205        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
206        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
207
208      | RTL.St_call_id (f, args, ret_regs, lbl) ->
209        let f_def = find_function mem f in
210        let args = get_arg_values lenv args in
211        let sf =
212          { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
213            sp = sp ; lenv = lenv ; carry = carry }
214        in
215        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
216
217      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
218        let addr = get_local_addr lenv f1 f2 in
219        let f_def = Mem.find_fun_def mem addr in
220        let args = get_arg_values lenv args in
221        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
222                   sp = sp ; lenv = lenv ; carry = carry } in
223        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
224
225      | RTL.St_tailcall_id (f, args) ->
226        let f_def = find_function mem f in
227        let args = get_arg_values lenv args in
228        let mem = Mem.free mem sp in
229        CallState (sfrs, f_def, args, mem, inds, trace)
230
231      | RTL.St_tailcall_ptr (f1, f2, args) ->
232        let addr = get_local_addr lenv f1 f2 in
233        let f_def = Mem.find_fun_def mem addr 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_cond (srcr, lbl_true, lbl_false) ->
239        let v = get_local_value lenv srcr in
240        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
241
242      | RTL.St_return rl ->
243        let vl = List.map (get_local_value lenv) rl in
244        let mem = Mem.free mem sp in
245        ReturnState (sfrs, vl, mem, inds, trace)
246
247
248module InterpretExternal = Primitive.Interpret (Mem)
249
250let interpret_external mem f args = match InterpretExternal.t mem f args with
251  | (mem', InterpretExternal.V vs) -> (mem', vs)
252  | (mem', InterpretExternal.A addr) -> (mem', addr)
253
254let init_locals
255    (locals : Register.Set.t)
256    (params : Register.t list)
257    (args   : Val.t list) :
258    local_env =
259  let f r lenv = Register.Map.add r Val.undef lenv in
260  let lenv = Register.Set.fold f locals Register.Map.empty in
261  let f lenv r v = Register.Map.add r v lenv in
262  List.fold_left2 f lenv params args
263
264let state_after_call
265    (sfrs  : stack_frame list)
266    (f_def : RTL.function_def)
267    (args  : Val.t list)
268    (mem   : memory)
269    (inds  : indexing list)
270    (trace : CostLabel.t list) :
271    state =
272  match f_def with
273    | RTL.F_int def ->
274      let inds = new_ind inds in
275      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
276      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
277             init_locals def.RTL.f_locals def.RTL.f_params args,
278             Val.undef, mem', inds, trace)
279    | RTL.F_ext def ->
280      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
281      ReturnState (sfrs, vs, mem', inds, trace)
282
283let state_after_return
284    (sf       : stack_frame)
285    (sfrs     : stack_frame list)
286    (ret_vals : Val.t list)
287    (mem      : memory)
288    (inds     : indexing list)
289    (trace    : CostLabel.t list) :
290    state =
291  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
292  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
293  let inds = forget_ind inds in
294  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
295
296
297let small_step (st : state) : state = match st with
298  | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) ->
299    let stmt = Label.Map.find pc graph in
300    interpret_statement sfrs graph sp lenv carry mem inds stmt trace
301  | CallState (sfrs, f_def, args, mem, inds, trace) ->
302    state_after_call sfrs f_def args mem inds trace
303  | ReturnState ([], ret_vals, mem, inds, trace) ->
304    assert false (* End of execution; handled in iter_small_step. *)
305  | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) ->
306    state_after_return sf sfrs ret_vals mem inds trace
307
308
309let compute_result vs =
310  let f res v = res && (Val.is_int v) in
311  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
312  if is_int vs then
313    let chunks =
314      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
315    IntValue.Int32.merge chunks
316  else IntValue.Int32.zero
317
318let rec iter_small_step debug st =
319  let print_and_return_result (res, cost_labels) =
320    if debug then Printf.printf "Result = %s\n%!"
321      (IntValue.Int32.to_string res) ;
322    (res, cost_labels) in
323  if debug then print_state st ;
324  match small_step st with
325    | ReturnState ([], vs, mem, _, trace) ->
326      print_and_return_result (compute_result vs, List.rev trace)
327    | st' -> iter_small_step debug st'
328
329
330let add_global_vars =
331  List.fold_left
332    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
333
334let add_fun_defs =
335  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
336
337
338(* The memory is initialized by loading the code into it, and by reserving space
339   for the global variables. *)
340
341let init_mem (p : RTL.program) : memory =
342  add_global_vars (add_fun_defs Mem.empty p.RTL.functs) p.RTL.vars
343
344
345(* Interpret the program only if it has a main. *)
346
347let interpret debug p =
348  Printf.printf "*** RTL interpret ***\n%!" ;
349  match p.RTL.main with
350    | None -> (IntValue.Int32.zero, [])
351    | Some main ->
352      let mem = init_mem p in
353      let main_def = find_function mem main in
354      let st = CallState ([], main_def, [], mem, [], []) in
355      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.