src/RTL/RTLInterpret.ml

   1
   2 (** This module provides an interpreter for the RTL language. *)
   3
   4
   5 let error_prefix = "RTL interpret"
   6 let error s = Error.global_error error_prefix s
   7
   8
   9 module Mem = Driver.RTLMemory
  10 module Val = Mem.Value
  11 let chunk = Driver.RTLMemory.int_size
  12 module Eval = I8051.Eval (Val)
  13
  14
  15 type memory = RTL.function_def Mem.memory
  16
  17
  18 (* Local environments. They associate a value to the registers of the function
  19    being executed. *)
  20
  21 type local_env = Val.t 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 node, the local environment and the value of the carry to resume
  26    the execution of the caller. *)
  27
  28 type stack_frame =
  29     { ret_regs : Register.t list ;
  30       graph    : RTL.graph ;
  31       pc       : Label.t ;
  32       sp       : Val.address ;
  33       lenv     : local_env ;
  34       carry    : Val.t }
  35
  36 (* Execution states. There are three possible states :
  37    - The constructor [State] represents a state when executing a function
  38    - The constructor [CallState] represents a state when calling a function
  39    - The constructor [ReturnState] represents a state when leaving a function *)
  40
  41 type state =
  42   | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
  43              local_env * Val.t (* carry *) * memory * CostLabel.t list
  44   | CallState of stack_frame list * RTL.function_def *
  45                  Val.t list (* args *) * memory * CostLabel.t list
  46   | ReturnState of stack_frame list * Val.t list (* return values *) *
  47                    memory * CostLabel.t list
  48
  49 let string_of_local_env lenv =
  50   let f x v s =
  51     s ^
  52       (if Val.eq v Val.undef then ""
  53        else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
  54   Register.Map.fold f lenv ""
  55
  56 let string_of_args args =
  57   let f s v = s ^ " " ^ (Val.to_string v) in
  58   List.fold_left f "" args
  59
  60 let print_state = function
  61   | State (_, _, lbl, sp, lenv, carry, mem, _) ->
  62     Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
  63       (Val.string_of_address sp)
  64       (Val.to_string carry)
  65       (string_of_local_env lenv)
  66       (Mem.to_string mem)
  67       lbl
  68   | CallState (_, _, args, mem, _) ->
  69     Printf.printf "Memory:%s\nCall state: %s\n\n%!"
  70       (Mem.to_string mem)
  71       (string_of_args args)
  72   | ReturnState (_, vs, mem, _) ->
  73     Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
  74       (Mem.to_string mem)
  75       (string_of_args vs)
  76
  77
  78 let find_function mem f =
  79   let addr = Mem.find_global mem f in
  80   Mem.find_fun_def mem addr
  81
  82 let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
  83   if Register.Map.mem r lenv then Register.Map.find r lenv
  84   else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
  85 let get_arg_values lenv args = List.map (get_local_value lenv) args
  86
  87 let get_local_addr lenv f1 f2 =
  88   List.map (get_local_value lenv) [f1 ; f2]
  89
  90
  91 let adds rs vs lenv =
  92   let f lenv r v = Register.Map.add r v lenv in
  93   List.fold_left2 f lenv rs vs
  94
  95
  96 (* Assign a value to some destinations registers. *)
  97
  98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
  99   let lenv = adds destrs vs lenv in
 100   State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
 101
 102 (* Branch on a value. *)
 103
 104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
 105   let next_lbl =
 106     if Val.is_true v then lbl_true
 107     else
 108       if Val.is_false v then lbl_false
 109       else error "Undefined conditional value." in
 110   State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
 111
 112
 113 (* Interpret statements. *)
 114
 115 let interpret_statement
 116     (sfrs  : stack_frame list)
 117     (graph : RTL.graph)
 118     (sp    : Val.address)
 119     (lenv  : local_env)
 120     (carry : Val.t)
 121     (mem   : memory)
 122     (stmt  : RTL.statement)
 123     (trace : CostLabel.t list) :
 124     state = match stmt with
 125
 126       | RTL.St_skip lbl ->
 127         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
 128
 129       | RTL.St_cost (cost_lbl, lbl) ->
 130         State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
 131
 132       | RTL.St_addr (r1, r2, x, lbl) ->
 133         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
 134           (Mem.find_global mem x)
 135
 136       | RTL.St_stackaddr (r1, r2, lbl) ->
 137         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
 138
 139       | RTL.St_int (r, i, lbl) ->
 140         assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
 141
 142       | RTL.St_move (destr, srcr, lbl) ->
 143         assign_state sfrs graph lbl sp lenv carry mem trace [destr]
 144           [get_local_value lenv srcr]
 145
 146       | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
 147         let (v1, v2) =
 148           Eval.opaccs opaccs
 149             (get_local_value lenv srcr1)
 150             (get_local_value lenv srcr2) in
 151         assign_state sfrs graph lbl sp lenv carry mem trace
 152           [destr1 ; destr2] [v1 ; v2]
 153
 154       | RTL.St_op1 (op1, destr, srcr, lbl) ->
 155         let v = Eval.op1 op1 (get_local_value lenv srcr) in
 156         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
 157
 158       | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
 159         let (v, carry) =
 160           Eval.op2 carry op2
 161             (get_local_value lenv srcr1)
 162             (get_local_value lenv srcr2) in
 163         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
 164
 165       | RTL.St_clear_carry lbl ->
 166         State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
 167
 168       | RTL.St_set_carry lbl ->
 169         State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
 170
 171       | RTL.St_load (destr, addr1, addr2, lbl) ->
 172         let addr = get_local_addr lenv addr1 addr2 in
 173         let v = Mem.load mem chunk addr in
 174         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
 175
 176       | RTL.St_store (addr1, addr2, srcr, lbl) ->
 177         let addr = get_local_addr lenv addr1 addr2 in
 178         let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
 179         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
 180
 181       | RTL.St_call_id (f, args, ret_regs, lbl) ->
 182         let f_def = find_function mem f in
 183         let args = get_arg_values lenv args in
 184         let sf =
 185           { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
 186             sp = sp ; lenv = lenv ; carry = carry }
 187         in
 188         CallState (sf :: sfrs, f_def, args, mem, trace)
 189
 190       | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
 191         let addr = get_local_addr lenv f1 f2 in
 192         let f_def = Mem.find_fun_def mem addr in
 193         let args = get_arg_values lenv args in
 194         let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
 195                    sp = sp ; lenv = lenv ; carry = carry } in
 196         CallState (sf :: sfrs, f_def, args, mem, trace)
 197
 198       | RTL.St_tailcall_id (f, args) ->
 199         let f_def = find_function mem f in
 200         let args = get_arg_values lenv args in
 201         let mem = Mem.free mem sp in
 202         CallState (sfrs, f_def, args, mem, trace)
 203
 204       | RTL.St_tailcall_ptr (f1, f2, args) ->
 205         let addr = get_local_addr lenv f1 f2 in
 206         let f_def = Mem.find_fun_def mem addr in
 207         let args = get_arg_values lenv args in
 208         let mem = Mem.free mem sp in
 209         CallState (sfrs, f_def, args, mem, trace)
 210
 211       | RTL.St_cond (srcr, lbl_true, lbl_false) ->
 212         let v = get_local_value lenv srcr in
 213         branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
 214
 215       | RTL.St_return rl ->
 216         let vl = List.map (get_local_value lenv) rl in
 217         let mem = Mem.free mem sp in
 218         ReturnState (sfrs, vl, mem, trace)
 219
 220
 221 module InterpretExternal = Primitive.Interpret (Mem)
 222
 223 let interpret_external mem f args = match InterpretExternal.t mem f args with
 224   | (mem', InterpretExternal.V vs) -> (mem', vs)
 225   | (mem', InterpretExternal.A addr) -> (mem', addr)
 226
 227 let init_locals
 228     (locals : Register.Set.t)
 229     (params : Register.t list)
 230     (args   : Val.t list) :
 231     local_env =
 232   let f r lenv = Register.Map.add r Val.undef lenv in
 233   let lenv = Register.Set.fold f locals Register.Map.empty in
 234   let f lenv r v = Register.Map.add r v lenv in
 235   List.fold_left2 f lenv params args
 236
 237 let state_after_call
 238     (sfrs  : stack_frame list)
 239     (f_def : RTL.function_def)
 240     (args  : Val.t list)
 241     (mem   : memory)
 242     (trace : CostLabel.t list) :
 243     state =
 244   match f_def with
 245     | RTL.F_int def ->
 246       let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
 247       State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
 248              init_locals def.RTL.f_locals def.RTL.f_params args,
 249              Val.undef, mem', trace)
 250     | RTL.F_ext def ->
 251       let (mem', vs) = interpret_external mem def.AST.ef_tag args in
 252       ReturnState (sfrs, vs, mem', trace)
 253
 254 let state_after_return
 255     (sf       : stack_frame)
 256     (sfrs     : stack_frame list)
 257     (ret_vals : Val.t list)
 258     (mem      : memory)
 259     (trace    : CostLabel.t list) :
 260     state =
 261   let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
 262   let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
 263   State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
 264
 265
 266 let small_step (st : state) : state = match st with
 267   | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
 268     let stmt = Label.Map.find pc graph in
 269     interpret_statement sfrs graph sp lenv carry mem stmt trace
 270   | CallState (sfrs, f_def, args, mem, trace) ->
 271     state_after_call sfrs f_def args mem trace
 272   | ReturnState ([], ret_vals, mem, trace) ->
 273     assert false (* End of execution; handled in iter_small_step. *)
 274   | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
 275     state_after_return sf sfrs ret_vals mem trace
 276
 277
 278 let compute_result vs =
 279   let f res v = res && (Val.is_int v) in
 280   let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
 281   if is_int vs then
 282     let chunks =
 283       List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
 284     IntValue.Int32.merge chunks
 285   else IntValue.Int32.zero
 286
 287 let rec iter_small_step debug st =
 288   let print_and_return_result (res, cost_labels) =
 289     if debug then Printf.printf "Result = %s\n%!"
 290       (IntValue.Int32.to_string res) ;
 291     (res, cost_labels) in
 292   if debug then print_state st ;
 293   match small_step st with
 294     | ReturnState ([], vs, mem, trace) ->
 295       print_and_return_result (compute_result vs, List.rev trace)
 296     | st' -> iter_small_step debug st'
 297
 298
 299 let add_global_vars =
 300   List.fold_left
 301     (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
 302
 303 let add_fun_defs =
 304   List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
 305
 306
 307 (* The memory is initialized by loading the code into it, and by reserving space
 308    for the global variables. *)
 309
 310 let init_mem (p : RTL.program) : memory =
 311   add_global_vars (add_fun_defs Mem.empty p.RTL.functs) p.RTL.vars
 312
 313
 314 (* Interpret the program only if it has a main. *)
 315
 316 let interpret debug p =
 317   Printf.printf "*** RTL interpret ***\n%!" ;
 318   match p.RTL.main with
 319     | None -> (IntValue.Int32.zero, [])
 320     | Some main ->
 321       let mem = init_mem p in
 322       let main_def = find_function mem main in
 323       let st = CallState ([], main_def, [], mem, []) in
 324       iter_small_step debug st