source: Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.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: 12.7 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 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
24   the stack being composed of the return registers to store the result
25   of the callee, the graph, the stack pointer, the node and the local
26   environment to resume the execution of the caller. *)
27
28type stack_frame =
29    { ret_reg  : Register.t ;
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_value (lenv : local_env) (r : Register.t) : Val.t =
81  if Register.Map.mem r lenv then Register.Map.find r lenv
82  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
83let get_arg_values lenv args = List.map (get_local_value lenv) args
84
85let adds rs vs lenv =
86  let f lenv r v = Register.Map.add r v lenv in
87  List.fold_left2 f lenv rs vs
88
89let value_of_address = List.hd
90let address_of_value v = [v]
91
92
93let eval_addressing
94    (mem  : memory)
95    (sp   : Val.address)
96    (mode : RTLabs.addressing)
97    (args : Val.t list) :
98    Val.address = match mode, args with
99
100      | RTLabs.Aindexed off, v :: _ ->
101        address_of_value (Val.add v (Val.of_int off))
102
103      | RTLabs.Aindexed2, v1 :: v2 :: _ ->
104        address_of_value (Val.add v1 v2)
105
106      | RTLabs.Aglobal (id, off), _ ->
107        Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off)
108
109      | RTLabs.Abased (id, off), v :: _ ->
110        let addr =
111          Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) in
112        address_of_value (Val.add (value_of_address addr) v)
113
114      | RTLabs.Ainstack off, _ ->
115        Val.add_address sp (Val.Offset.of_int off)
116
117      | _, _ -> error "Bad addressing mode."
118
119
120let eval_cst mem sp = function
121  | AST.Cst_int i -> Val.of_int i
122  | AST.Cst_float f -> error_float ()
123  | AST.Cst_addrsymbol id -> value_of_address (Mem.find_global mem id)
124  | AST.Cst_stackoffset shift ->
125    value_of_address (Val.add_address sp (Val.Offset.of_int shift))
126
127let eval_op1 = function
128  | AST.Op_cast8unsigned -> Val.cast8unsigned
129  | AST.Op_cast8signed -> Val.cast8signed
130  | AST.Op_cast16unsigned -> Val.cast16unsigned
131  | AST.Op_cast16signed -> Val.cast16signed
132  | AST.Op_negint -> Val.negint
133  | AST.Op_notbool -> Val.notbool
134  | AST.Op_notint -> Val.notint
135  | AST.Op_negf
136  | AST.Op_absf
137  | AST.Op_singleoffloat
138  | AST.Op_intoffloat
139  | AST.Op_intuoffloat
140  | AST.Op_floatofint
141  | AST.Op_floatofintu -> error_float ()
142  | AST.Op_id -> (fun (v : Val.t) -> v)
143  | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *)
144
145let rec eval_op2 = function
146  | AST.Op_add | AST.Op_addp -> Val.add
147  | AST.Op_sub | AST.Op_subp -> Val.sub
148  | AST.Op_mul -> Val.mul
149  | AST.Op_div -> Val.div
150  | AST.Op_divu -> Val.divu
151  | AST.Op_mod -> Val.modulo
152  | AST.Op_modu -> Val.modulou
153  | AST.Op_and -> Val.and_op
154  | AST.Op_or -> Val.or_op
155  | AST.Op_xor -> Val.xor
156  | AST.Op_shl -> Val.shl
157  | AST.Op_shr -> Val.shr
158  | AST.Op_shru -> Val.shru
159  | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq
160  | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne
161  | AST.Op_cmp AST.Cmp_lt -> Val.cmp_lt
162  | AST.Op_cmp AST.Cmp_le -> Val.cmp_le
163  | AST.Op_cmp AST.Cmp_gt -> Val.cmp_gt
164  | AST.Op_cmp AST.Cmp_ge -> Val.cmp_ge
165  | AST.Op_cmpu AST.Cmp_eq -> Val.cmp_eq_u
166  | AST.Op_cmpu AST.Cmp_ne -> Val.cmp_ne_u
167  | AST.Op_cmpu AST.Cmp_lt -> Val.cmp_lt_u
168  | AST.Op_cmpu AST.Cmp_le -> Val.cmp_le_u
169  | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u
170  | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u
171  | AST.Op_cmpp cmp -> eval_op2 (AST.Op_cmp cmp)
172  | AST.Op_addf
173  | AST.Op_subf
174  | AST.Op_mulf
175  | AST.Op_divf
176  | AST.Op_cmpf _ -> error_float ()
177
178(* Assign a value to some destinations registers. *)
179
180let assign_state sfrs graph sp lbl lenv mem trace destr v =
181  let lenv = Register.Map.add destr v lenv in
182  State (sfrs, graph, sp, lbl, lenv, mem, trace)
183
184(* Branch on a value. *)
185
186let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
187  let next_lbl =
188    if Val.is_true v then lbl_true
189    else
190      if Val.is_false v then lbl_false
191      else error "Undefined conditional value." in
192  State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
193
194
195(* Interpret statements. *)
196
197let interpret_statement
198    (sfrs  : stack_frame list)
199    (graph : RTLabs.graph)
200    (sp    : Val.address)
201    (lenv  : local_env)
202    (mem   : memory)
203    (stmt  : RTLabs.statement)
204    (trace : CostLabel.t list) :
205    state = match stmt with
206
207      | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace)
208
209      | RTLabs.St_cost (cost_lbl, lbl) ->
210        State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
211
212      | RTLabs.St_cst (destr, cst, lbl) ->
213        let v = eval_cst mem sp cst in
214        assign_state sfrs graph sp lbl lenv mem trace destr v
215
216      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
217        let v = eval_op1 op1 (get_local_value lenv srcr) in
218        assign_state sfrs graph sp lbl lenv mem trace destr v
219
220      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
221        let v =
222          eval_op2 op2
223            (get_local_value lenv srcr1)
224            (get_local_value lenv srcr2) in
225        assign_state sfrs graph sp lbl lenv mem trace destr v
226
227      | RTLabs.St_load (q, mode, args, destr, lbl) ->
228        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
229        let v = Mem.loadq mem q addr in
230        assign_state sfrs graph sp lbl lenv mem trace destr v
231
232      | RTLabs.St_store (q, mode, args, srcr, lbl) ->
233        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
234        let v = get_local_value lenv srcr in
235        let mem = Mem.storeq mem q addr v in
236        State (sfrs, graph, sp, lbl, lenv, mem, trace)
237
238      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
239        let f_def = find_function mem f in
240        let args = get_arg_values lenv args in
241        (* Save the stack frame. *)
242        let sf =
243          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
244        in
245        CallState (sf :: sfrs, f_def, args, mem, trace)
246
247      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
248        let addr = get_local_value lenv r in
249        let f_def = Mem.find_fun_def mem (address_of_value addr) in
250        let args = get_arg_values lenv args in
251        (* Save the stack frame. *)
252        let sf =
253          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
254        in
255        CallState (sf :: sfrs, f_def, args, mem, trace)
256
257      | RTLabs.St_tailcall_id (f, args, sg) ->
258        let f_def = find_function mem f in
259        let args = get_arg_values lenv args in
260        (* No need to save the stack frame. But free the stack. *)
261        let mem = Mem.free mem sp in
262        CallState (sfrs, f_def, args, mem, trace)
263
264      | RTLabs.St_tailcall_ptr (r, args, sg) ->
265        let addr = get_local_value lenv r in
266        let f_def = Mem.find_fun_def mem (address_of_value addr) in
267        let args = get_arg_values lenv args in
268        (* No need to save the stack frame. But free the stack. *)
269        let mem = Mem.free mem sp in
270        CallState (sfrs, f_def, args, mem, trace)
271
272      | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
273        let v = eval_cst mem sp cst in
274        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
275
276      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
277        let v = eval_op1 op1 (get_local_value lenv srcr) in
278        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
279
280      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
281        let v =
282          eval_op2 op2
283            (get_local_value lenv srcr1)
284            (get_local_value lenv srcr2) in
285        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
286
287      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
288      (*
289        let i = match get_local_value lenv r with
290        | Val.Val_int i -> i
291        | Val.Val_ptr _ -> error "Illegal cast from pointer to integer."
292        | _ -> error "Typing error." in
293        (try
294        let next_lbl = List.nth table i in
295        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
296        with
297        | Failure "nth" | Invalid_argument "List.nth" ->
298        error "Index out of jumptable.")
299      *)
300
301      | RTLabs.St_return r ->
302        let v = get_local_value lenv r in
303        let mem = Mem.free mem sp in
304        ReturnState (sfrs, v, mem, trace)
305
306
307module InterpretExternal = Primitive.Interpret (Mem)
308
309let interpret_external mem f args = match InterpretExternal.t mem f args with
310  | (mem', InterpretExternal.V v) -> (mem', v)
311  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
312
313let init_locals
314    (locals : Register.t list)
315    (params : Register.t list)
316    (args   : Val.t list) :
317    local_env =
318  let f lenv r = Register.Map.add r Val.undef lenv in
319  let lenv = List.fold_left f Register.Map.empty locals in
320  let f lenv r v = Register.Map.add r v lenv in
321  List.fold_left2 f lenv params args
322
323let state_after_call
324    (sfrs  : stack_frame list)
325    (f_def : RTLabs.function_def)
326    (args  : Val.t list)
327    (mem   : memory)
328    (trace : CostLabel.t list) :
329    state =
330  match f_def with
331    | RTLabs.F_int def ->
332      let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in
333      State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
334             init_locals def.RTLabs.f_locals def.RTLabs.f_params args,
335             mem', trace)
336    | RTLabs.F_ext def ->
337      let (mem', v) = interpret_external mem def.AST.ef_tag args in
338      ReturnState (sfrs, v, mem', trace)
339
340
341let state_after_return
342    (sf      : stack_frame)
343    (sfrs    : stack_frame list)
344    (ret_val : Val.t)
345    (mem     : memory)
346    (trace   : CostLabel.t list) :
347    state =
348  let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in
349  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
350
351
352let small_step (st : state) : state = match st with
353  | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
354    let stmt = Label.Map.find pc graph in
355    interpret_statement sfrs graph sp lenv mem stmt trace
356  | CallState (sfrs, f_def, args, mem, trace) ->
357    state_after_call sfrs f_def args mem trace
358  | ReturnState ([], ret_val, mem, trace) ->
359    assert false (* End of execution; handled in iter_small_step. *)
360  | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
361    state_after_return sf sfrs ret_val mem trace
362
363
364let compute_result v =
365  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
366  else IntValue.Int8.zero
367
368let rec iter_small_step debug st =
369  if debug then print_state st ;
370  match small_step st with
371    | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace)
372    | st' -> iter_small_step debug st'
373
374
375let add_global_vars =
376  List.fold_left
377    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
378
379let add_fun_defs =
380  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
381
382
383(* The memory is initialized by load the code into it, and by reserving space
384   for the global variables. *)
385
386let init_mem (p : RTLabs.program) : memory =
387  add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars
388
389
390(* Interpret the program only if it has a main. *)
391
392let interpret debug p =
393  if debug then Printf.printf "*** RTLabs ***\n\n%!" ;
394  match p.RTLabs.main with
395    | None -> (IntValue.Int8.zero, [])
396    | Some main ->
397      let mem = init_mem p in
398      let main_def = find_function mem main in
399      let st = CallState ([], main_def, [], mem, []) in
400      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.