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

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

Deliverable D2.2

File size: 11.9 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.t ;
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.t (* sp *) *
43             local_env * Val.t (* carry *) * memory * AST.trace
44  | CallState of stack_frame list * RTL.function_def *
45                 Val.t list (* args *) * memory * AST.trace
46  | ReturnState of stack_frame list * Val.t list (* return values *) *
47                   memory * AST.trace
48
49
50let find_function mem f =
51  let v = Mem.find_global mem f in
52  Mem.find_fun_def mem v
53
54let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
55  if Register.Map.mem r lenv then Register.Map.find r lenv
56  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
57let get_arg_values lenv args = List.map (get_local_value lenv) args
58
59let get_local_addr lenv f1 f2 =
60  Val.merge (List.map (get_local_value lenv) [f1 ; f2])
61
62(* An address is represented by two pseudo-registers (because in 8051, addresses
63   are coded on two bytes). Thus, assignments may involve several
64   registers. When we want to assign a single value to several registers, we
65   break the value into as many parts as there are registers, and then we update
66   each register with a part of the value. *)
67
68let adds rs v lenv = match rs with
69  | [] -> lenv
70  | _ ->
71    let vs = Val.break v (List.length rs) in
72    let f lenv r v = Register.Map.add r v lenv in
73    List.fold_left2 f lenv rs vs
74
75
76(* Assign a value to some destinations registers. *)
77
78let assign_state cs c lbl sp lenv carry mem t destrs v =
79  let lenv = adds destrs v lenv in
80  State (cs, c, lbl, sp, lenv, carry, mem, t)
81
82(* Branch on a value. *)
83
84let branch_state cs c lbl_true lbl_false sp lenv carry mem t v =
85  let next_lbl =
86    if Val.is_true v then lbl_true
87    else
88      if Val.is_false v then lbl_false
89      else error "Undefined conditional value." in
90  State (cs, c, next_lbl, sp, lenv, carry, mem, t)
91
92
93(* Interpret statements. *)
94
95let interpret_statement
96    (cs    : stack_frame list)
97    (c     : RTL.graph)
98    (sp    : Val.t)
99    (lenv  : local_env)
100    (carry : Val.t)
101    (mem   : memory)
102    (stmt  : RTL.statement)
103    (t     : AST.trace) :
104    state = match stmt with
105
106      | RTL.St_skip lbl ->
107        State (cs, c, lbl, sp, lenv, carry, mem, t)
108
109      | RTL.St_cost (cost_lbl, lbl) ->
110        State (cs, c, lbl, sp, lenv, carry, mem, cost_lbl :: t)
111
112      | RTL.St_addr (r1, r2, x, lbl) ->
113        assign_state cs c lbl sp lenv carry mem t [r1 ; r2]
114          (Mem.find_global mem x)
115
116      | RTL.St_stackaddr (r1, r2, lbl) ->
117        assign_state cs c lbl sp lenv carry mem t [r1 ; r2] sp
118
119      | RTL.St_int (r, i, lbl) ->
120        assign_state cs c lbl sp lenv carry mem t [r] (Val.of_int i)
121
122      | RTL.St_move (destr, srcr, lbl) ->
123        assign_state cs c lbl sp lenv carry mem t [destr]
124          (get_local_value lenv srcr)
125
126      | RTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) ->
127        let v =
128          Eval.opaccs opaccs
129            (get_local_value lenv srcr1)
130            (get_local_value lenv srcr2) in
131        assign_state cs c lbl sp lenv carry mem t [destr] v
132
133      | RTL.St_op1 (op1, destr, srcr, lbl) ->
134        let v = Eval.op1 op1 (get_local_value lenv srcr) in
135        assign_state cs c lbl sp lenv carry mem t [destr] v
136
137      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
138        let (v, carry) =
139          Eval.op2 carry op2
140            (get_local_value lenv srcr1)
141            (get_local_value lenv srcr2) in
142        assign_state cs c lbl sp lenv carry mem t [destr] v
143
144      | RTL.St_clear_carry lbl ->
145        State (cs, c, lbl, sp, lenv, Val.zero, mem, t)
146
147      | RTL.St_load (destr, addr1, addr2, lbl) ->
148        let dph = get_local_value lenv addr1 in
149        let dpl = get_local_value lenv addr2 in
150        let addr = Val.merge [dph ; dpl] in
151        let v = Mem.load2 mem chunk addr in
152        assign_state cs c lbl sp lenv carry mem t [destr] v
153
154      | RTL.St_store (addr1, addr2, srcr, lbl) ->
155        let dph = get_local_value lenv addr1 in
156        let dpl = get_local_value lenv addr2 in
157        let addr = Val.merge [dph ; dpl] in
158        let mem = Mem.store2 mem chunk addr (get_local_value lenv srcr) in
159        State (cs, c, lbl, sp, lenv, carry, mem, t)
160
161      | RTL.St_call_id (f, args, ret_regs, lbl) ->
162        let f_def = find_function mem f in
163        let args = get_arg_values lenv args in
164        let sf =
165          { ret_regs = ret_regs ; graph = c ; pc = lbl ;
166            sp = sp ; lenv = lenv ; carry = carry }
167        in
168        CallState (sf :: cs, f_def, args, mem, t)
169
170      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
171        let addr = get_local_addr lenv f1 f2 in
172        let f_def = Mem.find_fun_def mem addr in
173        let args = get_arg_values lenv args in
174        let sf = { ret_regs = ret_regs ; graph = c ; pc = lbl ;
175                   sp = sp ; lenv = lenv ; carry = carry } in
176        CallState (sf :: cs, f_def, args, mem, t)
177
178      | RTL.St_tailcall_id (f, args) ->
179        let f_def = find_function mem f in
180        let args = get_arg_values lenv args in
181        let mem = Mem.free mem sp in
182        CallState (cs, f_def, args, mem, t)
183
184      | RTL.St_tailcall_ptr (f1, f2, args) ->
185        let addr = get_local_addr lenv f1 f2 in
186        let f_def = Mem.find_fun_def mem addr in
187        let args = get_arg_values lenv args in
188        let mem = Mem.free mem sp in
189        CallState (cs, f_def, args, mem, t)
190
191      | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
192        let v = get_local_value lenv srcr in
193        branch_state cs c lbl_true lbl_false sp lenv carry mem t v
194
195      | RTL.St_return rl ->
196        let vl = List.map (get_local_value lenv) rl in
197        let mem = Mem.free mem sp in
198        ReturnState (cs, vl, mem, t)
199
200
201let get_int () =
202  try Val.of_int (int_of_string (read_line ()))
203  with Failure "int_of_string" -> error "Failed to scan an integer."
204let get_float () =
205  try Val.of_float (float_of_string (read_line ()))
206  with Failure "float_of_string" -> error "Failed to scan a float."
207
208let interpret_external
209    (mem  : memory)
210    (def  : AST.external_function)
211    (args : Val.t list) :
212    memory * Val.t list =
213  match def.AST.ef_tag, args with
214    | s, _ when s = Primitive.scan_int ->
215      (mem, [get_int ()])
216    | "scan_float", _ ->
217      (mem, [get_float ()])
218    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
219      Printf.printf "%d" (Val.to_int v) ;
220      (mem, [Val.zero])
221    | "print_float", v :: _ when Val.is_float v ->
222      Printf.printf "%f" (Val.to_float v) ;
223      (mem, [Val.zero])
224    | "print_ptr", v :: _ when Val.is_pointer v ->
225      let (b, off) = Val.to_pointer v in
226      Printf.printf "block: %s, offset: %s"
227        (Val.Block.to_string b) (Val.Offset.to_string off) ;
228      (mem, [Val.zero])
229    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
230      Printf.printf "%d\n" (Val.to_int v) ;
231      (mem, [Val.zero])
232    | "print_floatln", v :: _ when Val.is_float v ->
233      Printf.printf "%f" (Val.to_float v) ;
234      (mem, [Val.zero])
235    | "print_ptrln", v :: _ when Val.is_pointer v ->
236      let (b, off) = Val.to_pointer v in
237      Printf.printf "block: %s, offset: %s\n"
238        (Val.Block.to_string b) (Val.Offset.to_string off) ;
239      (mem, [Val.zero])
240    | s, v :: _ when s = Primitive.alloc ->
241      let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
242      let vs = Val.break ptr 2 in
243      (mem, vs)
244    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
245      (mem, [Val.modulo v1 v2])
246
247    (* The other cases are either a type error (only integers and pointers
248       may not be differenciated during type checking) or an unknown
249       function. *)
250    | "print_int", _ | "print_intln", _ ->
251      error "Illegal cast from pointer to integer."
252    | "print_ptr", _ | "print_ptrln", _ ->
253      error "Illegal cast from integer to pointer."
254    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
255
256let init_locals
257    (locals : Register.Set.t)
258    (params : Register.t list)
259    (args   : Val.t list) :
260    local_env =
261  let f r lenv = Register.Map.add r Val.undef lenv in
262  let lenv = Register.Set.fold f locals Register.Map.empty in
263  let f lenv r v = Register.Map.add r v lenv in
264  List.fold_left2 f lenv params args
265
266let state_after_call
267    (cs    : stack_frame list)
268    (f_def : RTL.function_def)
269    (args  : Val.t list)
270    (mem   : memory)
271    (t     : AST.trace) :
272    state =
273  match f_def with
274    | RTL.F_int def ->
275      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
276      State (cs, 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', t)
279    | RTL.F_ext def ->
280      let (mem', vs) = interpret_external mem def args in
281      ReturnState (cs, vs, mem', t)
282
283let state_after_return
284    (sf       : stack_frame)
285    (cs       : stack_frame list)
286    (ret_vals : Val.t list)
287    (mem      : memory)
288    (t        : AST.trace) :
289    state =
290  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
291  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
292  State (cs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, t)
293
294
295let small_step (st : state) : state = match st with
296  | State (cs, graph, pc, sp, lenv, carry, mem, t) ->
297    let stmt = Label.Map.find pc graph in
298    interpret_statement cs graph sp lenv carry mem stmt t
299  | CallState (cs, f_def, args, mem, t) ->
300    state_after_call cs f_def args mem t
301  | ReturnState ([], ret_vals, mem, t) ->
302    assert false (* End of execution; handled in iter_small_step. *)
303  | ReturnState (sf :: cs, ret_vals, mem, t) ->
304    state_after_return sf cs ret_vals mem t
305
306
307let print_args = MiscPottier.string_of_list ", " Val.to_string
308let print_ret_vals = MiscPottier.string_of_list ", " Val.to_string
309let print_lenv =
310  Register.Map.iter (fun r v -> Printf.printf "%s = %s\n%!"
311    (Register.print r) (Val.to_string v))
312
313let rec iter_small_step st = match small_step st with
314(*
315  | ReturnState ([], vs, mem, t) ->
316    Mem.print mem ;
317    Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;
318    List.rev t
319  | CallState (_, _, args, mem, _) as st' ->
320    Printf.printf "Call state: %s\n%!" (print_args args) ;
321    Mem.print mem ;
322    iter_small_step st'
323  | ReturnState (_, ret_vals, mem, _) as st' ->
324    Printf.printf "Return state: %s\n%!" (print_ret_vals ret_vals) ;
325    Mem.print mem ;
326    iter_small_step st'
327  | State (_, _, pc, sp, lenv, carry, mem, _) as st' ->
328    Printf.printf "State: PC = %s ; SP = %s\n%!" pc (Val.to_string sp) ;
329    Mem.print mem ;
330    print_lenv lenv ;
331    Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ;
332    iter_small_step st'
333*)
334  | ReturnState ([], vs, mem, t) ->
335(*
336    Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;
337*)
338    List.rev t
339  | st' -> iter_small_step st'
340
341
342let add_global_vars =
343  List.fold_left
344    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
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 load 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 p = match p.RTL.main with
360  | None -> []
361  | Some main ->
362    let mem = init_mem p in
363    let main_def = find_function mem main in
364    let st = CallState ([], main_def, [], mem, []) in
365    iter_small_step st
Note: See TracBrowser for help on using the repository browser.