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

Last change on this file since 1589 was 1589, checked in by tranquil, 9 years ago
  • turned to argument-less return statements for RTLabs and RTL (there was a hidden invariant, for which the arguments of return statements where equal to the f_result field of the function definition: they were useless and an optimization was breaking the compilation)
  • corrected a bug in liveness analysis I had introduced
File size: 12.8 KB
RevLine 
[486]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
[740]12let error_float () = error "float not supported"
[486]13
[740]14
[486]15type memory = RTLabs.function_def Mem.memory
16
17
[818]18(* Local environments. They associate a value and a type to the registers of the
19   function being executed. *)
[486]20
[1589]21type local_env = {
22  le_vals : (Val.t * AST.sig_type) Register.Map.t ;
23  le_ret : Register.t option
24}
[486]25
[818]26(* Call frames. The execution state has a call stack, each element of the stack
27   being composed of the return registers to store the result of the callee, the
28   graph, the stack pointer, the node, the local environment and the typing
29   environments to resume the execution of the caller. *)
[486]30
31type stack_frame =
[1589]32    { result   : Register.t option ;
[486]33      graph    : RTLabs.graph ;
[740]34      sp       : Val.address ;
[486]35      pc       : Label.t ;
36      lenv     : local_env }
37
[1542]38type indexing = CostLabel.const_indexing
39
[486]40(* Execution states. There are three possible states :
41   - The constructor [State] represents a state when executing a function
42   - The constructor [CallState] represents a state when calling a function
43   - The constructor [ReturnState] represents a state when leaving a function *)
44
45type state =
[740]46  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
[1542]47       Label.t * local_env * memory * indexing list * CostLabel.t list
[486]48  | CallState of stack_frame list * RTLabs.function_def *
[1542]49              Val.t list (* args *) * memory * indexing list * CostLabel.t list
[486]50  | ReturnState of stack_frame list * Val.t (* return value *) *
[1542]51        memory * indexing list * CostLabel.t list
[486]52
[740]53let string_of_local_env lenv =
[818]54  let f x (v, _) s =
[740]55    s ^
56      (if Val.eq v Val.undef then ""
57       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
[1589]58  Register.Map.fold f lenv.le_vals ""
[486]59
[740]60let string_of_args args =
61  let f s v = s ^ " " ^ (Val.to_string v) in
62  List.fold_left f "" args
63
[1542]64let print_state state = match state with
65  | State (_, _, sp, lbl, lenv, mem, inds, _) ->
66    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
[740]67      (Val.string_of_address sp)
68      (string_of_local_env lenv)
[1542]69      (Mem.to_string mem);
70    let i = CostLabel.curr_const_ind inds in
71    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
72    Printf.printf "Regular state: %s\n\n%!"
[740]73      lbl
[1542]74  | CallState (_, _, args, mem, _, _) ->
[740]75    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
76      (Mem.to_string mem)
77      (string_of_args args)
[1542]78  | ReturnState (_, v, mem, _, _) ->
[740]79    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
80      (Mem.to_string mem)
81      (Val.to_string v)
82
83
[486]84let find_function mem f =
[740]85  let addr = Mem.find_global mem f in
86  Mem.find_fun_def mem addr
[486]87
[818]88let get_local_env f lenv r =
[1589]89  let a = try Register.Map.find r lenv.le_vals with
90    | Not_found ->
91      error ("Unknown local register \"" ^ (Register.print r) ^ "\".") in
92  f a
[486]93
[818]94let get_value = get_local_env fst
95
96let get_type = get_local_env snd
97
98let update_local r v lenv =
[1589]99  let f (_, t) = Register.Map.add r (v, t) lenv.le_vals in
100  { lenv with le_vals = get_local_env f lenv r }
[818]101
102let update_locals rs vs lenv =
103  let f lenv r v = update_local r v lenv in
[740]104  List.fold_left2 f lenv rs vs
[486]105
[740]106let value_of_address = List.hd
107let address_of_value v = [v]
[486]108
109
[818]110module Eval = CminorInterpret.Eval_op (Mem)
[486]111
[818]112let concrete_stacksize = Eval.concrete_stacksize
[486]113
114
[1572]115let eval_arg lenv mem sp = function
116  | RTLabs.Reg r -> get_value lenv r
117  | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
118
119let get_type_arg lenv = function
120  | RTLabs.Reg r -> get_type lenv r
121  | RTLabs.Imm (_, typ) -> typ
122
123let get_args lenv mem sp  args = List.map (eval_arg lenv mem sp) args
124
[486]125(* Assign a value to some destinations registers. *)
126
[1542]127let assign_state sfrs graph sp lbl lenv mem inds trace destr v =
[818]128  let lenv = update_local destr v lenv in
[1542]129  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
[486]130
131(* Branch on a value. *)
132
[1542]133let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v =
[486]134  let next_lbl =
135    if Val.is_true v then lbl_true
136    else
137      if Val.is_false v then lbl_false
138      else error "Undefined conditional value." in
[1542]139  State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace)
[486]140
[1542]141let curr_ind = CostLabel.curr_const_ind
[486]142
[1542]143let forget_ind = CostLabel.forget_const_ind
144
145let new_ind = CostLabel.new_const_ind
146
[486]147(* Interpret statements. *)
148
149let interpret_statement
[740]150    (sfrs  : stack_frame list)
151    (graph : RTLabs.graph)
152    (sp    : Val.address)
153    (lenv  : local_env)
154    (mem   : memory)
155    (stmt  : RTLabs.statement)
[1542]156    (inds  : indexing list)
[740]157    (trace : CostLabel.t list) :
[486]158    state = match stmt with
159
[818]160      | RTLabs.St_skip lbl ->
[1542]161        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
[486]162
163      | RTLabs.St_cost (cost_lbl, lbl) ->
[1542]164        let cost_lbl =
165          CostLabel.ev_indexing (curr_ind inds) cost_lbl in
166        State (sfrs, graph, sp, lbl, lenv,
167               mem, inds, cost_lbl :: trace)
[486]168
[1542]169      | RTLabs.St_ind_0 (i, lbl) ->
170        CostLabel.enter_loop inds i; 
171        State (sfrs, graph, sp, lbl, lenv,
172               mem, inds, trace)
173
174      | RTLabs.St_ind_inc (i, lbl) ->
175        CostLabel.continue_loop inds i; 
176        State (sfrs, graph, sp, lbl, lenv,
177               mem, inds, trace)
178
[740]179      | RTLabs.St_cst (destr, cst, lbl) ->
[818]180        let v = Eval.cst mem sp (get_type lenv destr) cst in
[1542]181        assign_state sfrs graph sp lbl lenv mem inds trace destr v
[486]182
[740]183      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
[818]184        let v =
185          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
186            (get_value lenv srcr) in
[1542]187        assign_state sfrs graph sp lbl lenv mem inds trace destr v
[486]188
[740]189      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
[486]190        let v =
[818]191          Eval.op2
[1542]192            (get_type lenv destr)
193            (get_type_arg lenv srcr1)
194            (get_type_arg lenv srcr2)
[818]195            op2
[1542]196            (eval_arg lenv mem sp srcr1)
197            (eval_arg lenv mem sp srcr2) in
198        assign_state sfrs graph sp lbl lenv mem inds trace destr v
[486]199
[818]200      | RTLabs.St_load (q, addr, destr, lbl) ->
[1542]201        let addr = address_of_value (eval_arg lenv mem sp addr) in
[740]202        let v = Mem.loadq mem q addr in
[1542]203        assign_state sfrs graph sp lbl lenv mem inds trace destr v
[486]204
[818]205      | RTLabs.St_store (q, addr, srcr, lbl) ->
[1542]206        let addr = address_of_value (eval_arg lenv mem sp addr) in
207        let v = eval_arg lenv mem sp srcr in
[740]208        let mem = Mem.storeq mem q addr v in
[1542]209        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
[486]210
211      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
212        let f_def = find_function mem f in
[1572]213        let args = get_args lenv mem sp args in
[486]214        (* Save the stack frame. *)
215        let sf =
[1589]216          { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
[486]217        in
[1542]218        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
[486]219
[740]220      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
[818]221        let addr = get_value lenv r in
[740]222        let f_def = Mem.find_fun_def mem (address_of_value addr) in
[1572]223        let args = get_args lenv mem sp args in
[486]224        (* Save the stack frame. *)
225        let sf =
[1589]226          { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
[486]227        in
[1542]228        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
[486]229
230      | RTLabs.St_tailcall_id (f, args, sg) ->
231        let f_def = find_function mem f in
[1572]232        let args = get_args lenv mem sp args in
[486]233        (* No need to save the stack frame. But free the stack. *)
234        let mem = Mem.free mem sp in
[1542]235        CallState (sfrs, f_def, args, mem, inds, trace)
[486]236
[740]237      | RTLabs.St_tailcall_ptr (r, args, sg) ->
[818]238        let addr = get_value lenv r in
[740]239        let f_def = Mem.find_fun_def mem (address_of_value addr) in
[1572]240        let args = get_args lenv mem sp args in
[486]241        (* No need to save the stack frame. But free the stack. *)
242        let mem = Mem.free mem sp in
[1542]243        CallState (sfrs, f_def, args, mem, inds, trace)
[486]244
[818]245      | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
246        let v = get_value lenv srcr in
[1542]247        branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v
[486]248
[818]249(*
250      | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) ->
251        let v = Eval.cst mem sp t cst in
252        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
253
[740]254      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
[818]255        let v =
256          Eval.op1 (get_type lenv srcr) (get_type lenv srcr)
257            op1 (get_value lenv srcr) in
[740]258        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
[486]259
[740]260      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
[486]261        let v =
[818]262          Eval.op2 op2
263            (get_value lenv srcr1)
264            (get_value lenv srcr2) in
[740]265        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
[818]266*)
[486]267
[740]268      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
[486]269      (*
[818]270        let i = match get_value lenv r with
[486]271        | Val.Val_int i -> i
272        | Val.Val_ptr _ -> error "Illegal cast from pointer to integer."
273        | _ -> error "Typing error." in
274        (try
275        let next_lbl = List.nth table i in
[740]276        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
[486]277        with
278        | Failure "nth" | Invalid_argument "List.nth" ->
279        error "Index out of jumptable.")
280      *)
281
[1589]282      | RTLabs.St_return ->
[486]283        let mem = Mem.free mem sp in
[1589]284        let res =  match lenv.le_ret with
285          | None -> Val.undef
286          | Some r -> get_value lenv r in
287        ReturnState (sfrs, res, mem, inds, trace)
[818]288
[740]289module InterpretExternal = Primitive.Interpret (Mem)
[486]290
[740]291let interpret_external mem f args = match InterpretExternal.t mem f args with
[818]292  | (mem', InterpretExternal.V vs) ->
293    let v = if List.length vs = 0 then Val.undef else List.hd vs in
294    (mem', v)
[740]295  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
[486]296
[818]297
[486]298let init_locals
[818]299    (locals           : (Register.t * AST.sig_type) list)
300    (params           : (Register.t * AST.sig_type) list)
[1589]301    (ret              : (Register.t * AST.sig_type) option)
[818]302    (args             : Val.t list) :
[486]303    local_env =
[818]304  let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in
305  let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in
[1589]306  let lenv_vals = List.fold_left2 f_param Register.Map.empty params args in
307  let ret = Option.map fst ret in
308  { le_vals = List.fold_left f_local lenv_vals locals; le_ret = ret }
[486]309
310let state_after_call
[740]311    (sfrs  : stack_frame list)
[486]312    (f_def : RTLabs.function_def)
313    (args  : Val.t list)
314    (mem   : memory)
[1542]315    (inds  : indexing list)
[740]316    (trace : CostLabel.t list) :
[486]317    state =
318  match f_def with
319    | RTLabs.F_int def ->
[818]320      let (mem', sp) =
321        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
[1589]322      let lenv = init_locals
323        def.RTLabs.f_locals
324        def.RTLabs.f_params
325        def.RTLabs.f_result
326        args in
327      let graph = def.RTLabs.f_graph in
[1542]328      (* allocate new constant indexing *)
329      let inds = new_ind inds in
330      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
[486]331    | RTLabs.F_ext def ->
[740]332      let (mem', v) = interpret_external mem def.AST.ef_tag args in
[1542]333      ReturnState (sfrs, v, mem', inds, trace)
[486]334
335
336let state_after_return
337    (sf      : stack_frame)
[740]338    (sfrs    : stack_frame list)
[486]339    (ret_val : Val.t)
340    (mem     : memory)
[1542]341    (inds    : indexing list)
[740]342    (trace   : CostLabel.t list) :
[486]343    state =
[1589]344  let lenv = match sf.result with
[818]345    | None -> sf.lenv
346    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
[1589]347  (* erase current indexing and revert to previous one *)
348  let inds = forget_ind inds in
349  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, trace)
[486]350
351
352let small_step (st : state) : state = match st with
[1542]353  | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) ->
[486]354    let stmt = Label.Map.find pc graph in
[1542]355    interpret_statement sfrs graph sp lenv mem stmt inds trace
356  | CallState (sfrs, f_def, args, mem, inds, trace) ->
357    state_after_call sfrs f_def args mem inds trace
358  | ReturnState ([], ret_val, mem, inds, trace) ->
[486]359    assert false (* End of execution; handled in iter_small_step. *)
[1542]360  | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) ->
361    state_after_return sf sfrs ret_val mem inds trace
[486]362
363
[619]364let compute_result v =
[818]365  if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
366  else IntValue.Int32.zero
[619]367
[740]368let rec iter_small_step debug st =
[818]369  let print_and_return_result (res, cost_labels) =
370    if debug then Printf.printf "Result = %s\n%!"
371      (IntValue.Int32.to_string res) ;
372    (res, cost_labels) in
[740]373  if debug then print_state st ;
374  match small_step st with
[1542]375    | ReturnState ([], v, mem, inds, trace) ->
[818]376      print_and_return_result (compute_result v, List.rev trace)
[740]377    | st' -> iter_small_step debug st'
[486]378
379
380let add_global_vars =
[818]381  List.fold_left (fun mem (id, size) -> Mem.add_var mem id size None)
[486]382
383let add_fun_defs =
384  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
385
386
[818]387(* The memory is initialized by loading the code into it, and by reserving space
[486]388   for the global variables. *)
389
390let init_mem (p : RTLabs.program) : memory =
391  add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars
392
393
394(* Interpret the program only if it has a main. *)
395
[740]396let interpret debug p =
[818]397  Printf.printf "*** RTLabs interpret ***\n%!" ;
[740]398  match p.RTLabs.main with
[818]399    | None -> (IntValue.Int32.zero, [])
[740]400    | Some main ->
401      let mem = init_mem p in
402      let main_def = find_function mem main in
[1542]403      let st = CallState ([], main_def, [], mem, [], []) in
[740]404      iter_small_step debug st
Note: See TracBrowser for help on using the repository browser.