source: Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml @ 619

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

Update of D2.2 from Paris.

File size: 14.6 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
12
13type memory = RTLabs.function_def Mem.memory
14
15
16(* Local environments. They associate a value to the registers of the function
17   being executed. *)
18
19type local_env = Val.t Register.Map.t
20
21(* Call frames. The execution state has a call stack, each element of
22   the stack being composed of the return registers to store the result
23   of the callee, the graph, the stack pointer, the node and the local
24   environment to resume the execution of the caller. *)
25
26type stack_frame =
27    { ret_regs : Register.t list ;
28      graph    : RTLabs.graph ;
29      sp       : Val.t ;
30      pc       : Label.t ;
31      lenv     : local_env }
32
33(* Execution states. There are three possible states :
34   - The constructor [State] represents a state when executing a function
35   - The constructor [CallState] represents a state when calling a function
36   - The constructor [ReturnState] represents a state when leaving a function *)
37
38type state =
39  | State of stack_frame list * RTLabs.graph * Val.t (* stack pointer *) *
40             Label.t * local_env * memory * CostLabel.t list
41  | CallState of stack_frame list * RTLabs.function_def *
42                 Val.t list (* args *) * memory * CostLabel.t list
43  | ReturnState of stack_frame list * Val.t (* return value *) *
44                   memory * CostLabel.t list
45
46
47let find_function mem f =
48  let v = Mem.find_global mem f in
49  Mem.find_fun_def mem v
50
51let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
52  if Register.Map.mem r lenv then Register.Map.find r lenv
53  else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
54let get_arg_values lenv args = List.map (get_local_value lenv) args
55
56let get_local_valuel (lenv : local_env) (rl : Register.t list) : Val.t =
57  let vl = List.map (get_local_value lenv) rl in
58  Val.merge vl
59let get_arg_valuesl lenv argsl = List.map (get_local_valuel lenv) argsl
60
61(* An address is represented by two pseudo-registers (because in 8051, addresses
62   are coded on two bytes). Thus, assignments may involve several
63   registers. When we want to assign a single value to several registers, we
64   break the value into as many parts as there are registers, and then we update
65   each register with a part of the value. *)
66
67let adds rs v lenv = match rs with
68  | [] -> lenv
69  | _ ->
70    let vs = Val.break v (List.length rs) in
71    let f lenv r v = Register.Map.add r v lenv in
72    List.fold_left2 f lenv rs vs
73
74
75let eval_addressing
76    (mem  : memory)
77    (sp   : Val.t)
78    (mode : RTLabs.addressing)
79    (args : Val.t list) :
80    Val.t = match mode, args with
81
82      | RTLabs.Aindexed off, addr :: _ when Val.is_pointer addr ->
83        Val.add addr (Val.of_int off)
84
85      | RTLabs.Aindexed2, addr :: shift :: _
86        when Val.is_pointer addr && Val.is_int shift ->
87        Val.add addr shift
88
89      | RTLabs.Aindexed2, shift :: addr :: _
90        when Val.is_pointer addr && Val.is_int shift ->
91        Val.add addr shift
92
93      | RTLabs.Aglobal (id, off), _ ->
94        Val.add (Mem.find_global mem id) (Val.of_int off)
95
96      | RTLabs.Abased (id, off), v :: _ ->
97        let addr = Val.add (Mem.find_global mem id) (Val.of_int off) in
98        Val.add addr v
99
100      | RTLabs.Ainstack off, _ ->
101        Val.add sp (Val.of_int off)
102
103      | _, _ -> error "Bad addressing mode."
104
105
106let eval_cst mem sp = function
107  | AST.Cst_int i -> Val.of_int i
108  | AST.Cst_float f -> Val.of_float f
109  | AST.Cst_addrsymbol id -> Mem.find_global mem id
110  | AST.Cst_stackoffset shift -> Val.add sp (Val.of_int shift)
111
112let eval_op1 = function
113  | AST.Op_cast8unsigned -> Val.cast8unsigned
114  | AST.Op_cast8signed -> Val.cast8signed
115  | AST.Op_cast16unsigned -> Val.cast16unsigned
116  | AST.Op_cast16signed -> Val.cast16signed
117  | AST.Op_negint -> Val.negint
118  | AST.Op_notbool -> Val.notbool
119  | AST.Op_notint -> Val.notint
120  | AST.Op_negf -> Val.negf
121  | AST.Op_absf -> Val.absf
122  | AST.Op_singleoffloat -> Val.singleoffloat
123  | AST.Op_intoffloat -> Val.intoffloat
124  | AST.Op_intuoffloat -> Val.intuoffloat
125  | AST.Op_floatofint -> Val.floatofint
126  | AST.Op_floatofintu -> Val.floatofintu
127  | AST.Op_id -> (fun (v : Val.t) -> v)
128  | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO? *)
129
130let rec eval_op2 = function
131  | AST.Op_add | AST.Op_addp -> Val.add
132  | AST.Op_sub | AST.Op_subp -> Val.sub
133  | AST.Op_mul -> Val.mul
134  | AST.Op_div -> Val.div
135  | AST.Op_divu -> Val.divu
136  | AST.Op_mod -> Val.modulo
137  | AST.Op_modu -> Val.modulou
138  | AST.Op_and -> Val.and_op
139  | AST.Op_or -> Val.or_op
140  | AST.Op_xor -> Val.xor
141  | AST.Op_shl -> Val.shl
142  | AST.Op_shr -> Val.shr
143  | AST.Op_shru -> Val.shru
144  | AST.Op_addf -> Val.addf
145  | AST.Op_subf -> Val.subf
146  | AST.Op_mulf -> Val.mulf
147  | AST.Op_divf -> Val.divf
148  | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq
149  | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne
150  | AST.Op_cmp AST.Cmp_lt -> Val.cmp_lt
151  | AST.Op_cmp AST.Cmp_le -> Val.cmp_le
152  | AST.Op_cmp AST.Cmp_gt -> Val.cmp_gt
153  | AST.Op_cmp AST.Cmp_ge -> Val.cmp_ge
154  | AST.Op_cmpu AST.Cmp_eq -> Val.cmp_eq_u
155  | AST.Op_cmpu AST.Cmp_ne -> Val.cmp_ne_u
156  | AST.Op_cmpu AST.Cmp_lt -> Val.cmp_lt_u
157  | AST.Op_cmpu AST.Cmp_le -> Val.cmp_le_u
158  | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u
159  | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u
160  | AST.Op_cmpf AST.Cmp_eq -> Val.cmp_eq_f
161  | AST.Op_cmpf AST.Cmp_ne -> Val.cmp_ne_f
162  | AST.Op_cmpf AST.Cmp_lt -> Val.cmp_lt_f
163  | AST.Op_cmpf AST.Cmp_le -> Val.cmp_le_f
164  | AST.Op_cmpf AST.Cmp_gt -> Val.cmp_gt_f
165  | AST.Op_cmpf AST.Cmp_ge -> Val.cmp_ge_f
166  | AST.Op_cmpp cmp -> eval_op2 (AST.Op_cmp cmp)
167
168(* Assign a value to some destinations registers. *)
169
170let assign_state cs c sp lbl lenv mem t destrs v =
171  let lenv = adds destrs v lenv in
172  State (cs, c, sp, lbl, lenv, mem, t)
173
174(* Branch on a value. *)
175
176let branch_state cs c sp lbl_true lbl_false lenv mem t v =
177  let next_lbl =
178    if Val.is_true v then lbl_true
179    else
180      if Val.is_false v then lbl_false
181      else error "Undefined conditional value." in
182  State (cs, c, sp, next_lbl, lenv, mem, t)
183
184
185(* Interpret statements. *)
186
187let interpret_statement
188    (cs   : stack_frame list)
189    (c    : RTLabs.graph)
190    (sp   : Val.t)
191    (lenv : local_env)
192    (mem  : memory)
193    (stmt : RTLabs.statement)
194    (t    : CostLabel.t list) :
195    state = match stmt with
196
197      | RTLabs.St_skip lbl -> State (cs, c, sp, lbl, lenv, mem, t)
198
199      | RTLabs.St_cost (cost_lbl, lbl) ->
200        State (cs, c, sp, lbl, lenv, mem, cost_lbl :: t)
201
202      | RTLabs.St_cst (destrs, cst, lbl) ->
203        let v = eval_cst mem sp cst in
204        assign_state cs c sp lbl lenv mem t destrs v
205
206      | RTLabs.St_op1 (op1, destrs, srcrs, lbl) ->
207        let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
208        assign_state cs c sp lbl lenv mem t destrs v
209
210      | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl) ->
211        let v =
212          eval_op2 op2
213            (get_local_valuel lenv srcrs1)
214            (get_local_valuel lenv srcrs2) in
215        assign_state cs c sp lbl lenv mem t destrs v
216
217      | RTLabs.St_load (chunk, mode, args, destrs, lbl) ->
218        let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
219        let v = Mem.load mem chunk addr in
220        assign_state cs c sp lbl lenv mem t destrs v
221
222      | RTLabs.St_store (chunk, mode, args, srcrs, lbl) ->
223        let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
224        let mem = Mem.store mem chunk addr (get_local_valuel lenv srcrs) in
225        State (cs, c, sp, lbl, lenv, mem, t)
226
227      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
228        let f_def = find_function mem f in
229        let args = get_arg_valuesl lenv args in
230        (* Save the stack frame. *)
231        let sf =
232          { ret_regs = destr ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
233        in
234        CallState (sf :: cs, f_def, args, mem, t)
235
236      | RTLabs.St_call_ptr (rs, args, destrs, sg, lbl) ->
237        let addr = get_local_valuel lenv rs in
238        let f_def = Mem.find_fun_def mem addr in
239        let args = get_arg_valuesl lenv args in
240        (* Save the stack frame. *)
241        let sf =
242          { ret_regs = destrs ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
243        in
244        CallState (sf :: cs, f_def, args, mem, t)
245
246      | RTLabs.St_tailcall_id (f, args, sg) ->
247        let f_def = find_function mem f in
248        let args = get_arg_valuesl lenv args in
249        (* No need to save the stack frame. But free the stack. *)
250        let mem = Mem.free mem sp in
251        CallState (cs, f_def, args, mem, t)
252
253      | RTLabs.St_tailcall_ptr (rs, args, sg) ->
254        let addr = get_local_valuel lenv rs in
255        let f_def = Mem.find_fun_def mem addr in
256        let args = get_arg_valuesl lenv args in
257        (* No need to save the stack frame. But free the stack. *)
258        let mem = Mem.free mem sp in
259        CallState (cs, f_def, args, mem, t)
260
261      | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
262        let v = eval_cst mem sp cst in
263        branch_state cs c sp lbl_true lbl_false lenv mem t v
264
265      | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
266        let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
267        branch_state cs c sp lbl_true lbl_false lenv mem t v
268
269      | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
270        let v =
271          eval_op2 op2
272            (get_local_valuel lenv srcrs1)
273            (get_local_valuel lenv srcrs2) in
274        branch_state cs c sp lbl_true lbl_false lenv mem t v
275
276      | RTLabs.St_jumptable (r, table) -> assert false (* TODO *)
277      (*
278        let i = match get_local_value lenv r with
279        | Val.Val_int i -> i
280        | Val.Val_ptr _ -> error "Illegal cast from pointer to integer."
281        | _ -> error "Typing error." in
282        (try
283        let next_lbl = List.nth table i in
284        State (cs, c, sp, next_lbl, lenv, mem, t)
285        with
286        | Failure "nth" | Invalid_argument "List.nth" ->
287        error "Index out of jumptable.")
288      *)
289
290      | RTLabs.St_return rs ->
291        let v = get_local_valuel lenv rs in
292        let mem = Mem.free mem sp in
293        ReturnState (cs, v, mem, t)
294
295
296let get_int () =
297  try Val.of_int (int_of_string (read_line ()))
298  with Failure "int_of_string" -> error "Failed to scan an integer."
299let get_float () =
300  try Val.of_float (float_of_string (read_line ()))
301  with Failure "float_of_string" -> error "Failed to scan a float."
302
303let interpret_external
304    (mem  : memory)
305    (def  : AST.external_function)
306    (args : Val.t list) :
307    memory * Val.t =
308  match def.AST.ef_tag, args with
309    | s, _ when s = Primitive.scan_int ->
310      (mem, get_int ())
311    | "scan_float", _ ->
312      (mem, get_float ())
313    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
314      Printf.printf "%d" (Val.to_int v) ;
315      (mem, Val.zero)
316    | "print_float", v :: _ when Val.is_float v ->
317      Printf.printf "%f" (Val.to_float v) ;
318      (mem, Val.zero)
319    | "print_ptr", v :: _ when Val.is_pointer v ->
320      let (b, off) = Val.to_pointer v in
321      Printf.printf "block: %s, offset: %s"
322        (Val.Block.to_string b) (Val.Offset.to_string off) ;
323      (mem, Val.zero)
324    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
325      Printf.printf "%d\n" (Val.to_int v) ;
326      (mem, Val.zero)
327    | "print_floatln", v :: _ when Val.is_float v ->
328      Printf.printf "%f" (Val.to_float v) ;
329      (mem, Val.zero)
330    | "print_ptrln", v :: _ when Val.is_pointer v ->
331      let (b, off) = Val.to_pointer v in
332      Printf.printf "block: %s, offset: %s\n"
333        (Val.Block.to_string b) (Val.Offset.to_string off) ;
334      (mem, Val.zero)
335    | s, v :: _ when s = Primitive.alloc ->
336      let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
337      (mem, ptr)
338    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
339      (mem, Val.modulo v1 v2)
340
341    (* The other cases are either a type error (only integers and pointers
342       may not be differenciated during type checking) or an unknown
343       function. *)
344    | "print_int", _ | "print_intln", _ ->
345      error "Illegal cast from pointer to integer."
346    | "print_ptr", _ | "print_ptrln", _ ->
347      error "Illegal cast from integer to pointer."
348    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
349
350
351let init_locals
352    (locals : Register.t list list)
353    (params : Register.t list list)
354    (args   : Val.t list) :
355    local_env =
356  let f lenv rs = adds rs Val.undef lenv in
357  let lenv = List.fold_left f Register.Map.empty locals in
358  let f lenv rs v = adds rs v lenv in
359  List.fold_left2 f lenv params args
360
361let state_after_call
362    (cs    : stack_frame list)
363    (f_def : RTLabs.function_def)
364    (args  : Val.t list)
365    (mem   : memory)
366    (t     : CostLabel.t list) :
367    state =
368  match f_def with
369    | RTLabs.F_int def ->
370      let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in
371      State (cs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
372             init_locals def.RTLabs.f_locals def.RTLabs.f_params args,
373             mem', t)
374    | RTLabs.F_ext def ->
375      let (mem', v) = interpret_external mem def args in
376      ReturnState (cs, v, mem', t)
377
378
379let state_after_return
380    (sf      : stack_frame)
381    (cs      : stack_frame list)
382    (ret_val : Val.t)
383    (mem     : memory)
384    (t       : CostLabel.t list) :
385    state =
386  let lenv = adds sf.ret_regs ret_val sf.lenv in
387  State (cs, sf.graph, sf.sp, sf.pc, lenv, mem, t)
388
389
390let small_step (st : state) : state = match st with
391  | State (cs, graph, sp, pc, lenv, mem, t) ->
392    let stmt = Label.Map.find pc graph in
393    interpret_statement cs graph sp lenv mem stmt t
394  | CallState (cs, f_def, args, mem, t) ->
395    state_after_call cs f_def args mem t
396  | ReturnState ([], ret_val, mem, t) ->
397    assert false (* End of execution; handled in iter_small_step. *)
398  | ReturnState (sf :: cs, ret_val, mem, t) ->
399    state_after_return sf cs ret_val mem t
400
401
402let compute_result v =
403  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
404  else IntValue.Int8.zero
405
406let rec iter_small_step print_result st = match small_step st with
407(*
408  (* <DEBUG> *)
409  | ReturnState ([], v, mem, t) ->
410    Mem.print mem ;
411    Printf.printf "Return: %s\n%!" (Val.to_string v) ;
412    List.rev t
413  | CallState (_, _, _, mem, _)
414  | ReturnState (_, _, mem, _)
415  | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st'
416  (* </DEBUG> *)
417*)
418  | ReturnState ([], v, mem, t) ->
419    let (res, cost_labels) as trace = (compute_result v, List.rev t) in
420    if print_result then
421      Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ;
422    trace
423  | st' -> iter_small_step print_result st'
424
425
426let add_global_vars =
427  List.fold_left
428    (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])
429
430let add_fun_defs =
431  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
432
433
434(* The memory is initialized by load the code into it, and by reserving space
435   for the global variables. *)
436
437let init_mem (p : RTLabs.program) : memory =
438  add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars
439
440
441(* Interpret the program only if it has a main. *)
442
443let interpret print_result p = match p.RTLabs.main with
444  | None -> (IntValue.Int8.zero, [])
445  | Some main ->
446    let mem = init_mem p in
447    let main_def = find_function mem main in
448    let st = CallState ([], main_def, [], mem, []) in
449    iter_small_step print_result st
Note: See TracBrowser for help on using the repository browser.