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

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

merge of indexed labels branch

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