source: Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.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: 11.2 KB
Line 
1
2(** This module provides an interpreter for the RTLabs language. *)
3
4
5let error_prefix = "RTLabs interpret"
6let error s = Error.global_error error_prefix s
7
8
9module Mem = Driver.RTLabsMemory
10module Val = Mem.Value
11
12let error_float () = error "float not supported"
13
14
15type memory = RTLabs.function_def Mem.memory
16
17
18(* Local environments. They associate a value and a type to the registers of the
19   function being executed. *)
20
21type local_env = (Val.t * AST.sig_type) 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 stack pointer, the node, the local environment and the typing
26   environments to resume the execution of the caller. *)
27
28type stack_frame =
29    { ret_reg  : Register.t option ;
30      graph    : RTLabs.graph ;
31      sp       : Val.address ;
32      pc       : Label.t ;
33      lenv     : local_env }
34
35(* Execution states. There are three possible states :
36   - The constructor [State] represents a state when executing a function
37   - The constructor [CallState] represents a state when calling a function
38   - The constructor [ReturnState] represents a state when leaving a function *)
39
40type state =
41  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
42             Label.t * local_env * memory * CostLabel.t list
43  | CallState of stack_frame list * RTLabs.function_def *
44                 Val.t list (* args *) * memory * CostLabel.t list
45  | ReturnState of stack_frame list * Val.t (* return value *) *
46                   memory * CostLabel.t list
47
48let string_of_local_env lenv =
49  let f x (v, _) s =
50    s ^
51      (if Val.eq v Val.undef then ""
52       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
53  Register.Map.fold f lenv ""
54
55let string_of_args args =
56  let f s v = s ^ " " ^ (Val.to_string v) in
57  List.fold_left f "" args
58
59let print_state = function
60  | State (_, _, sp, lbl, lenv, mem, _) ->
61    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
62      (Val.string_of_address sp)
63      (string_of_local_env lenv)
64      (Mem.to_string mem)
65      lbl
66  | CallState (_, _, args, mem, _) ->
67    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
68      (Mem.to_string mem)
69      (string_of_args args)
70  | ReturnState (_, v, mem, _) ->
71    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
72      (Mem.to_string mem)
73      (Val.to_string v)
74
75
76let find_function mem f =
77  let addr = Mem.find_global mem f in
78  Mem.find_fun_def mem addr
79
80let get_local_env f lenv r =
81  if Register.Map.mem r lenv then f (Register.Map.find r lenv)
82  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
83
84let get_value = get_local_env fst
85let get_args lenv args = List.map (get_value lenv) args
86
87let get_type = get_local_env snd
88
89let update_local r v lenv =
90  let f (_, t) = Register.Map.add r (v, t) lenv in
91  get_local_env f lenv r
92
93let update_locals rs vs lenv =
94  let f lenv r v = update_local r v lenv in
95  List.fold_left2 f lenv rs vs
96
97let value_of_address = List.hd
98let address_of_value v = [v]
99
100
101module Eval = CminorInterpret.Eval_op (Mem)
102
103let concrete_stacksize = Eval.concrete_stacksize
104
105
106(* Assign a value to some destinations registers. *)
107
108let assign_state sfrs graph sp lbl lenv mem trace destr v =
109  let lenv = update_local destr v lenv in
110  State (sfrs, graph, sp, lbl, lenv, mem, trace)
111
112(* Branch on a value. *)
113
114let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
115  let next_lbl =
116    if Val.is_true v then lbl_true
117    else
118      if Val.is_false v then lbl_false
119      else error "Undefined conditional value." in
120  State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
121
122
123(* Interpret statements. *)
124
125let interpret_statement
126    (sfrs  : stack_frame list)
127    (graph : RTLabs.graph)
128    (sp    : Val.address)
129    (lenv  : local_env)
130    (mem   : memory)
131    (stmt  : RTLabs.statement)
132    (trace : CostLabel.t list) :
133    state = match stmt with
134
135      | RTLabs.St_skip lbl ->
136        State (sfrs, graph, sp, lbl, lenv, mem, trace)
137
138      | RTLabs.St_cost (cost_lbl, lbl) ->
139        State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
140
141      | RTLabs.St_cst (destr, cst, lbl) ->
142        let v = Eval.cst mem sp (get_type lenv destr) cst in
143        assign_state sfrs graph sp lbl lenv mem trace destr v
144
145      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
146        let v =
147          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
148            (get_value lenv srcr) in
149        assign_state sfrs graph sp lbl lenv mem trace destr v
150
151      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
152        let v =
153          Eval.op2
154            (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2)
155            op2
156            (get_value lenv srcr1)
157            (get_value lenv srcr2) in
158        assign_state sfrs graph sp lbl lenv mem trace destr v
159
160      | RTLabs.St_load (q, addr, destr, lbl) ->
161        let addr = address_of_value (get_value lenv addr) in
162        let v = Mem.loadq mem q addr in
163        assign_state sfrs graph sp lbl lenv mem trace destr v
164
165      | RTLabs.St_store (q, addr, srcr, lbl) ->
166        let addr = address_of_value (get_value lenv addr) in
167        let v = get_value lenv srcr in
168        let mem = Mem.storeq mem q addr v in
169        State (sfrs, graph, sp, lbl, lenv, mem, trace)
170
171      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
172        let f_def = find_function mem f in
173        let args = get_args lenv args in
174        (* Save the stack frame. *)
175        let sf =
176          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
177        in
178        CallState (sf :: sfrs, f_def, args, mem, trace)
179
180      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
181        let addr = get_value lenv r in
182        let f_def = Mem.find_fun_def mem (address_of_value addr) in
183        let args = get_args lenv args in
184        (* Save the stack frame. *)
185        let sf =
186          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
187        in
188        CallState (sf :: sfrs, f_def, args, mem, trace)
189
190      | RTLabs.St_tailcall_id (f, args, sg) ->
191        let f_def = find_function mem f in
192        let args = get_args lenv args in
193        (* No need to save the stack frame. But free the stack. *)
194        let mem = Mem.free mem sp in
195        CallState (sfrs, f_def, args, mem, trace)
196
197      | RTLabs.St_tailcall_ptr (r, args, sg) ->
198        let addr = get_value lenv r in
199        let f_def = Mem.find_fun_def mem (address_of_value addr) in
200        let args = get_args lenv args in
201        (* No need to save the stack frame. But free the stack. *)
202        let mem = Mem.free mem sp in
203        CallState (sfrs, f_def, args, mem, trace)
204
205      | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
206        let v = get_value lenv srcr in
207        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
208
209(*
210      | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) ->
211        let v = Eval.cst mem sp t cst in
212        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
213
214      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
215        let v =
216          Eval.op1 (get_type lenv srcr) (get_type lenv srcr)
217            op1 (get_value lenv srcr) in
218        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
219
220      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
221        let v =
222          Eval.op2 op2
223            (get_value lenv srcr1)
224            (get_value lenv srcr2) in
225        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
226*)
227
228      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
229      (*
230        let i = match get_value lenv r with
231        | Val.Val_int i -> i
232        | Val.Val_ptr _ -> error "Illegal cast from pointer to integer."
233        | _ -> error "Typing error." in
234        (try
235        let next_lbl = List.nth table i in
236        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
237        with
238        | Failure "nth" | Invalid_argument "List.nth" ->
239        error "Index out of jumptable.")
240      *)
241
242      | RTLabs.St_return None ->
243        let mem = Mem.free mem sp in
244        ReturnState (sfrs, Val.undef, mem, trace)
245
246      | RTLabs.St_return (Some r) ->
247        let v = get_value lenv r in
248        let mem = Mem.free mem sp in
249        ReturnState (sfrs, v, mem, trace)
250
251
252module InterpretExternal = Primitive.Interpret (Mem)
253
254let interpret_external mem f args = match InterpretExternal.t mem f args with
255  | (mem', InterpretExternal.V vs) ->
256    let v = if List.length vs = 0 then Val.undef else List.hd vs in
257    (mem', v)
258  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
259
260
261let init_locals
262    (locals           : (Register.t * AST.sig_type) list)
263    (params           : (Register.t * AST.sig_type) list)
264    (args             : Val.t list) :
265    local_env =
266  let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in
267  let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in
268  let lenv = List.fold_left2 f_param Register.Map.empty params args in
269  List.fold_left f_local lenv locals
270
271let state_after_call
272    (sfrs  : stack_frame list)
273    (f_def : RTLabs.function_def)
274    (args  : Val.t list)
275    (mem   : memory)
276    (trace : CostLabel.t list) :
277    state =
278  match f_def with
279    | RTLabs.F_int def ->
280      let (mem', sp) =
281        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
282      let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
283      State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem',
284             trace)
285    | RTLabs.F_ext def ->
286      let (mem', v) = interpret_external mem def.AST.ef_tag args in
287      ReturnState (sfrs, v, mem', trace)
288
289
290let state_after_return
291    (sf      : stack_frame)
292    (sfrs    : stack_frame list)
293    (ret_val : Val.t)
294    (mem     : memory)
295    (trace   : CostLabel.t list) :
296    state =
297  let lenv = match sf.ret_reg with
298    | None -> sf.lenv
299    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
300  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
301
302
303let small_step (st : state) : state = match st with
304  | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
305    let stmt = Label.Map.find pc graph in
306    interpret_statement sfrs graph sp lenv mem stmt trace
307  | CallState (sfrs, f_def, args, mem, trace) ->
308    state_after_call sfrs f_def args mem trace
309  | ReturnState ([], ret_val, mem, trace) ->
310    assert false (* End of execution; handled in iter_small_step. *)
311  | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
312    state_after_return sf sfrs ret_val mem trace
313
314
315let compute_result v =
316  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
317  else IntValue.Int32.zero
318
319let rec iter_small_step debug st =
320  let print_and_return_result (res, cost_labels) =
321    if debug then Printf.printf "Result = %s\n%!"
322      (IntValue.Int32.to_string res) ;
323    (res, cost_labels) in
324  if debug then print_state st ;
325  match small_step st with
326    | ReturnState ([], v, mem, trace) ->
327      print_and_return_result (compute_result v, List.rev trace)
328    | st' -> iter_small_step debug st'
329
330
331let add_global_vars =
332  List.fold_left (fun mem (id, size) -> Mem.add_var mem id 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 : RTLabs.program) : memory =
342  add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars
343
344
345(* Interpret the program only if it has a main. *)
346
347let interpret debug p =
348  Printf.printf "*** RTLabs interpret ***\n%!" ;
349  match p.RTLabs.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.