src/RTLabs/RTLabsInterpret.ml

   1
   2 (** This module provides an interpreter for the RTLabs language. *)
   3
   4
   5 let error_prefix = "RTLabs interpret"
   6 let error s = Error.global_error error_prefix s
   7
   8
   9 module Mem = Driver.RTLabsMemory
  10 module Val = Mem.Value
  11
  12 let error_float () = error "float not supported"
  13
  14
  15 type 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
  21 type 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
  28 type 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
  40 type 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
  48 let 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
  55 let string_of_args args =
  56   let f s v = s ^ " " ^ (Val.to_string v) in
  57   List.fold_left f "" args
  58
  59 let 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
  76 let find_function mem f =
  77   let addr = Mem.find_global mem f in
  78   Mem.find_fun_def mem addr
  79
  80 let 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
  84 let get_value = get_local_env fst
  85 let get_args lenv args = List.map (get_value lenv) args
  86
  87 let get_type = get_local_env snd
  88
  89 let 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
  93 let 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
  97 let value_of_address = List.hd
  98 let address_of_value v = [v]
  99
 100
 101 module Eval = CminorInterpret.Eval_op (Mem)
 102
 103 let concrete_stacksize = Eval.concrete_stacksize
 104
 105
 106 (* Assign a value to some destinations registers. *)
 107
 108 let 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
 114 let 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
 125 let 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       | RTLabs.St_jumptable (r, table) ->
 210         assert false (* TODO: jumptable *)
 211
 212       | RTLabs.St_return None ->
 213         let mem = Mem.free mem sp in
 214         ReturnState (sfrs, Val.undef, mem, trace)
 215
 216       | RTLabs.St_return (Some r) ->
 217         let v = get_value lenv r in
 218         let mem = Mem.free mem sp in
 219         ReturnState (sfrs, v, mem, trace)
 220
 221
 222 module InterpretExternal = Primitive.Interpret (Mem)
 223
 224 let interpret_external mem f args = match InterpretExternal.t mem f args with
 225   | (mem', InterpretExternal.V vs) ->
 226     let v = if List.length vs = 0 then Val.undef else List.hd vs in
 227     (mem', v)
 228   | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
 229
 230
 231 let init_locals
 232     (locals           : (Register.t * AST.sig_type) list)
 233     (params           : (Register.t * AST.sig_type) list)
 234     (args             : Val.t list) :
 235     local_env =
 236   let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in
 237   let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in
 238   let lenv = List.fold_left2 f_param Register.Map.empty params args in
 239   List.fold_left f_local lenv locals
 240
 241 let state_after_call
 242     (sfrs  : stack_frame list)
 243     (f_def : RTLabs.function_def)
 244     (args  : Val.t list)
 245     (mem   : memory)
 246     (trace : CostLabel.t list) :
 247     state =
 248   match f_def with
 249     | RTLabs.F_int def ->
 250       let (mem', sp) =
 251         Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
 252       let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
 253       State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem',
 254              trace)
 255     | RTLabs.F_ext def ->
 256       let (mem', v) = interpret_external mem def.AST.ef_tag args in
 257       ReturnState (sfrs, v, mem', trace)
 258
 259
 260 let state_after_return
 261     (sf      : stack_frame)
 262     (sfrs    : stack_frame list)
 263     (ret_val : Val.t)
 264     (mem     : memory)
 265     (trace   : CostLabel.t list) :
 266     state =
 267   let lenv = match sf.ret_reg with
 268     | None -> sf.lenv
 269     | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
 270   State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
 271
 272
 273 let small_step (st : state) : state = match st with
 274   | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
 275     let stmt = Label.Map.find pc graph in
 276     interpret_statement sfrs graph sp lenv mem stmt trace
 277   | CallState (sfrs, f_def, args, mem, trace) ->
 278     state_after_call sfrs f_def args mem trace
 279   | ReturnState ([], ret_val, mem, trace) ->
 280     assert false (* End of execution; handled in iter_small_step. *)
 281   | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
 282     state_after_return sf sfrs ret_val mem trace
 283
 284
 285 let compute_result v =
 286   if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v)
 287   else IntValue.Int32.zero
 288
 289 let rec iter_small_step debug st =
 290   let print_and_return_result (res, cost_labels) =
 291     if debug then Printf.printf "Result = %s\n%!"
 292       (IntValue.Int32.to_string res) ;
 293     (res, cost_labels) in
 294   if debug then print_state st ;
 295   match small_step st with
 296     | ReturnState ([], v, mem, trace) ->
 297       print_and_return_result (compute_result v, List.rev trace)
 298     | st' -> iter_small_step debug st'
 299
 300
 301 let add_global_vars =
 302   List.fold_left
 303     (fun mem (id, size, inits_opt) -> Mem.add_var mem id size inits_opt)
 304
 305 let add_fun_defs =
 306   List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
 307
 308
 309 (* The memory is initialized by loading the code into it, and by reserving space
 310    for the global variables. *)
 311
 312 let init_mem (p : RTLabs.program) : memory =
 313   add_global_vars (add_fun_defs Mem.empty p.RTLabs.functs) p.RTLabs.vars
 314
 315
 316 (* Interpret the program only if it has a main. *)
 317
 318 let interpret debug p =
 319   Printf.printf "*** RTLabs interpret ***\n%!" ;
 320   match p.RTLabs.main with
 321     | None -> (IntValue.Int32.zero, [])
 322     | Some main ->
 323       let mem = init_mem p in
 324       let main_def = find_function mem main in
 325       let st = CallState ([], main_def, [], mem, []) in
 326       iter_small_step debug st