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

Last change on this file since 1542 was 1542, checked in by tranquil, 9 years ago

merge of indexed labels branch

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