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

Last change on this file since 818 was 818, checked in by ayache, 9 years ago

32 and 16 bits operations support in D2.2/8051

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