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

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

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 10.1 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, destr, srcr1, srcr2, lbl) ->
147        let v =
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 [destr] [v]
152
153      | RTL.St_op1 (op1, destr, srcr, lbl) ->
154        let v = Eval.op1 op1 (get_local_value lenv srcr) in
155        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
156
157      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
158        let (v, carry) =
159          Eval.op2 carry op2
160            (get_local_value lenv srcr1)
161            (get_local_value lenv srcr2) in
162        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
163
164      | RTL.St_clear_carry lbl ->
165        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
166
167      | RTL.St_load (destr, addr1, addr2, lbl) ->
168        let addr = get_local_addr lenv addr1 addr2 in
169        let v = Mem.load mem chunk addr in
170        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
171
172      | RTL.St_store (addr1, addr2, srcr, lbl) ->
173        let addr = get_local_addr lenv addr1 addr2 in
174        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
175        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
176
177      | RTL.St_call_id (f, args, ret_regs, lbl) ->
178        let f_def = find_function mem f in
179        let args = get_arg_values lenv args in
180        let sf =
181          { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
182            sp = sp ; lenv = lenv ; carry = carry }
183        in
184        CallState (sf :: sfrs, f_def, args, mem, trace)
185
186      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
187        let addr = get_local_addr lenv f1 f2 in
188        let f_def = Mem.find_fun_def mem addr in
189        let args = get_arg_values lenv args in
190        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
191                   sp = sp ; lenv = lenv ; carry = carry } in
192        CallState (sf :: sfrs, f_def, args, mem, trace)
193
194      | RTL.St_tailcall_id (f, args) ->
195        let f_def = find_function mem f in
196        let args = get_arg_values lenv args in
197        let mem = Mem.free mem sp in
198        CallState (sfrs, f_def, args, mem, trace)
199
200      | RTL.St_tailcall_ptr (f1, f2, args) ->
201        let addr = get_local_addr lenv f1 f2 in
202        let f_def = Mem.find_fun_def mem addr in
203        let args = get_arg_values lenv args in
204        let mem = Mem.free mem sp in
205        CallState (sfrs, f_def, args, mem, trace)
206
207      | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
208        let v = get_local_value lenv srcr in
209        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
210
211      | RTL.St_return rl ->
212        let vl = List.map (get_local_value lenv) rl in
213        let mem = Mem.free mem sp in
214        ReturnState (sfrs, vl, mem, trace)
215
216
217module InterpretExternal = Primitive.Interpret (Mem)
218
219let interpret_external mem f args = match InterpretExternal.t mem f args with
220  | (mem', InterpretExternal.V v) -> (mem', [v])
221  | (mem', InterpretExternal.A addr) -> (mem', addr)
222
223let init_locals
224    (locals : Register.Set.t)
225    (params : Register.t list)
226    (args   : Val.t list) :
227    local_env =
228  let f r lenv = Register.Map.add r Val.undef lenv in
229  let lenv = Register.Set.fold f locals Register.Map.empty in
230  let f lenv r v = Register.Map.add r v lenv in
231  List.fold_left2 f lenv params args
232
233let state_after_call
234    (sfrs  : stack_frame list)
235    (f_def : RTL.function_def)
236    (args  : Val.t list)
237    (mem   : memory)
238    (trace : CostLabel.t list) :
239    state =
240  match f_def with
241    | RTL.F_int def ->
242      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
243      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
244             init_locals def.RTL.f_locals def.RTL.f_params args,
245             Val.undef, mem', trace)
246    | RTL.F_ext def ->
247      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
248      ReturnState (sfrs, vs, mem', trace)
249
250let state_after_return
251    (sf       : stack_frame)
252    (sfrs     : stack_frame list)
253    (ret_vals : Val.t list)
254    (mem      : memory)
255    (trace    : CostLabel.t list) :
256    state =
257  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
258  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
259  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
260
261
262let small_step (st : state) : state = match st with
263  | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
264    let stmt = Label.Map.find pc graph in
265    interpret_statement sfrs graph sp lenv carry mem stmt trace
266  | CallState (sfrs, f_def, args, mem, trace) ->
267    state_after_call sfrs f_def args mem trace
268  | ReturnState ([], ret_vals, mem, trace) ->
269    assert false (* End of execution; handled in iter_small_step. *)
270  | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
271    state_after_return sf sfrs ret_vals mem trace
272
273
274let compute_result vs =
275  try
276    let v = List.hd vs in
277    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
278    else IntValue.Int8.zero
279  with Not_found -> IntValue.Int8.zero
280
281let rec iter_small_step debug st =
282  if debug then print_state st ;
283  match small_step st with
284    | ReturnState ([], vs, mem, trace) -> (compute_result vs, List.rev trace)
285    | st' -> iter_small_step debug st'
286
287
288let add_global_vars =
289  List.fold_left
290    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
291
292let add_fun_defs =
293  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
294
295
296(* The memory is initialized by loading the code into it, and by reserving space
297   for the global variables. *)
298
299let init_mem (p : RTL.program) : memory =
300  add_global_vars (add_fun_defs Mem.empty p.RTL.functs) p.RTL.vars
301
302
303(* Interpret the program only if it has a main. *)
304
305let interpret debug p =
306  if debug then Printf.printf "*** RTL ***\n\n%!" ;
307  match p.RTL.main with
308    | None -> (IntValue.Int8.zero, [])
309    | Some main ->
310      let mem = init_mem p in
311      let main_def = find_function mem main in
312      let st = CallState ([], main_def, [], mem, []) in
313      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.