src/LIN/LINInterpret.ml

   1
   2 (** This module provides an interpreter for the LIN language. *)
   3
   4
   5 let error_prefix = "LIN interpret"
   6 let error s = Error.global_error error_prefix s
   7
   8
   9 module Mem = Driver.LINMemory
  10 module Val = Mem.Value
  11 let chunk = Driver.LINMemory.int_size
  12 module Eval = I8051.Eval (Val)
  13
  14
  15 (* Memory *)
  16
  17 type memory = LIN.function_def Mem.memory
  18
  19 (* Hardware registers environments. They associate a value to each hardware
  20    register. *)
  21
  22 type hdw_reg_env = Val.t I8051.RegisterMap.t
  23
  24 (* Execution states. *)
  25
  26 type state =
  27     { pc     : Val.address ;
  28       isp    : Val.address ;
  29       exit   : Val.address ;
  30       carry  : Val.t ;
  31       renv   : hdw_reg_env ;
  32       mem    : memory ;
  33       trace  : CostLabel.t list }
  34
  35
  36 (* Helpers *)
  37
  38 let change_pc st pc = { st with pc = pc }
  39 let change_isp st isp = { st with isp = isp }
  40 let change_exit st exit = { st with exit = exit }
  41 let change_carry st carry = { st with carry = carry }
  42 let change_renv st renv = { st with renv = renv }
  43 let change_mem st mem = { st with mem = mem }
  44 let change_trace st trace = { st with trace = trace }
  45 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
  46
  47 let empty_state =
  48   { pc     = Val.null ;
  49     isp    = Val.null ;
  50     exit   = Val.null ;
  51     carry  = Val.undef ;
  52     renv   = I8051.RegisterMap.empty ;
  53     mem    = Mem.empty ;
  54     trace  = [] }
  55
  56
  57 let int_fun_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
  58   | LIN.F_int def -> def
  59   | _ -> error "Trying to fetch the definition of an external function."
  60
  61 let current_int_fun st = int_fun_of_ptr st.mem st.pc
  62
  63 let fetch_stmt st =
  64   let msg =
  65     Printf.sprintf "%s does not point to a statement."
  66       (Val.string_of_address st.pc) in
  67   if Val.is_mem_address st.pc then
  68     let off = Val.offset_of_address st.pc in
  69     let def = int_fun_of_ptr st.mem st.pc in
  70     List.nth def (Val.Offset.to_int off)
  71   else error msg
  72
  73 let init_fun_call st ptr =
  74   change_pc st (Val.change_address_offset ptr Val.Offset.zero)
  75
  76 let next_pc st =
  77   change_pc st (Val.add_address st.pc Val.Offset.one)
  78
  79 let add_reg r v st =
  80   let renv = I8051.RegisterMap.add r v st.renv in
  81   change_renv st renv
  82
  83 let get_reg r st =
  84   if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
  85   else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
  86
  87 let push st v =
  88   let mem = Mem.store st.mem chunk st.isp v in
  89   let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
  90   change_mem (change_isp st isp) mem
  91
  92 let pop st =
  93   let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
  94   let st = change_isp st isp in
  95   let v = Mem.load st.mem chunk st.isp in
  96   (st, v)
  97
  98 let save_ra st =
  99   let ra = Val.add_address st.pc Val.Offset.one in
 100   let st = push st (List.nth ra 0) in
 101   let st = push st (List.nth ra 1) in
 102   st
 103
 104 let find_label lbl =
 105   let rec aux i = function
 106   | [] -> error (Printf.sprintf "Unknown label %s." lbl)
 107   | LIN.St_label lbl' :: _ when lbl' = lbl -> i
 108   | _ :: code -> aux (i+1) code
 109   in
 110   aux 0
 111
 112 let pointer_of_label st lbl =
 113   let code = current_int_fun st in
 114   let off = find_label lbl code in
 115   Val.change_address_offset st.pc (Val.Offset.of_int off)
 116
 117 let goto st lbl =
 118   change_pc st (pointer_of_label st lbl)
 119
 120 let return_pc st =
 121   let (st, pch) = pop st in
 122   let (st, pcl) = pop st in
 123   (st, [pcl ; pch])
 124
 125 let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
 126
 127
 128 (* State pretty-printing *)
 129
 130 let print_renv renv =
 131   let f r v =
 132     if not (Val.eq v Val.undef) then
 133     Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
 134   I8051.RegisterMap.iter f renv
 135
 136 let print_state st =
 137   Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
 138   Printf.printf "SP: %s\n%!"
 139     (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
 140   Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
 141   print_renv st.renv ;
 142   Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
 143   Mem.print st.mem ;
 144   Printf.printf "\n%!"
 145
 146
 147 module InterpretExternal = Primitive.Interpret (Mem)
 148
 149 let interpret_external mem f args = match InterpretExternal.t mem f args with
 150   | (mem', InterpretExternal.V vs) -> (mem', vs)
 151   | (mem', InterpretExternal.A addr) -> (mem', addr)
 152
 153 let fetch_external_args f st =
 154   let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
 155   let params = MiscPottier.prefix size I8051.parameters in
 156   List.map (fun r -> get_reg r st) params
 157
 158 let set_result st vs =
 159   let f st (r, v) = add_reg r v st in
 160   List.fold_left f st (MiscPottier.combine I8051.rets vs)
 161
 162 let interpret_external_call st f =
 163   let args = fetch_external_args f st in
 164   let (mem, vs) = interpret_external st.mem f args in
 165   let st = change_mem st mem in
 166   set_result st vs
 167
 168 let interpret_call st ptr =
 169   match Mem.find_fun_def st.mem ptr with
 170     | LIN.F_int def ->
 171       let st = save_ra st in
 172       init_fun_call st ptr
 173     | LIN.F_ext def ->
 174       let st = next_pc st in
 175       interpret_external_call st def.AST.ef_tag
 176
 177 let interpret_return st =
 178   let (st, pc) = return_pc st in
 179   change_pc st pc
 180
 181 let interpret_stmt st stmt =
 182   match stmt with
 183
 184     | LIN.St_goto lbl ->
 185       goto st lbl
 186
 187     | LIN.St_label _ ->
 188       next_pc st
 189
 190     | LIN.St_comment s ->
 191 (*
 192       Printf.printf "*** %s ***\n\n%!" s ;
 193 *)
 194       next_pc st
 195
 196     | LIN.St_cost cost_lbl ->
 197       let st = add_trace st cost_lbl in
 198       next_pc st
 199
 200     | LIN.St_int (r, i) ->
 201       let st = add_reg r (Val.of_int i) st in
 202       next_pc st
 203
 204     | LIN.St_pop ->
 205       let (st, v) = pop st in
 206       let st = add_reg I8051.a v st in
 207       next_pc st
 208
 209     | LIN.St_push ->
 210       let v = get_reg I8051.a st in
 211       let st = push st v in
 212       next_pc st
 213
 214     | LIN.St_addr x ->
 215       let vs = Mem.find_global st.mem x in
 216       let st = add_reg I8051.dpl (List.nth vs 0) st in
 217       let st = add_reg I8051.dph (List.nth vs 1) st in
 218       next_pc st
 219
 220     | LIN.St_from_acc destr ->
 221       let st = add_reg destr (get_reg I8051.a st) st in
 222       next_pc st
 223
 224     | LIN.St_to_acc srcr ->
 225       let st = add_reg I8051.a (get_reg srcr st) st in
 226       next_pc st
 227
 228     | LIN.St_opaccs opaccs ->
 229       let (a, b) =
 230         Eval.opaccs opaccs
 231           (get_reg I8051.a st)
 232           (get_reg I8051.b st) in
 233       let st = add_reg I8051.a a st in
 234       let st = add_reg I8051.b b st in
 235       next_pc st
 236
 237     | LIN.St_op1 op1 ->
 238       let v = Eval.op1 op1 (get_reg I8051.a st) in
 239       let st = add_reg I8051.a v st in
 240       next_pc st
 241
 242     | LIN.St_op2 (op2, srcr) ->
 243       let (v, carry) =
 244         Eval.op2 st.carry op2
 245           (get_reg I8051.a st)
 246           (get_reg srcr st) in
 247       let st = change_carry st carry in
 248       let st = add_reg I8051.a v st in
 249       next_pc st
 250
 251     | LIN.St_clear_carry ->
 252       let st = change_carry st Val.zero in
 253       next_pc st
 254
 255     | LIN.St_set_carry ->
 256       let st = change_carry st (Val.of_int 1) in
 257       next_pc st
 258
 259     | LIN.St_load ->
 260       let addr = dptr st in
 261       let v = Mem.load st.mem chunk addr in
 262       let st = add_reg I8051.a v st in
 263       next_pc st
 264
 265     | LIN.St_store ->
 266       let addr = dptr st in
 267       let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
 268       let st = change_mem st mem in
 269       next_pc st
 270
 271     | LIN.St_call_id f ->
 272       interpret_call st (Mem.find_global st.mem f)
 273
 274     | LIN.St_call_ptr ->
 275       interpret_call st (dptr st)
 276
 277     | LIN.St_condacc lbl_true ->
 278       let v = get_reg I8051.a st in
 279       if Val.is_true v then goto st lbl_true
 280       else
 281         if Val.is_false v then next_pc st
 282         else error "Undecidable branchment."
 283
 284     | LIN.St_return ->
 285       interpret_return st
 286
 287
 288 let compute_result st =
 289   let vs = List.map (fun r -> get_reg r st) I8051.rets in
 290   let f res v = res && (Val.is_int v) in
 291   let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
 292   if is_int vs then
 293     let chunks =
 294       List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
 295     IntValue.Int32.merge chunks
 296   else IntValue.Int32.zero
 297
 298 let rec iter_small_step debug st =
 299   let print_and_return_result (res, cost_labels) =
 300     if debug then Printf.printf "Result = %s\n%!"
 301       (IntValue.Int32.to_string res) ;
 302     (res, cost_labels) in
 303   if debug then print_state st ;
 304   match fetch_stmt st with
 305     | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
 306       print_and_return_result (compute_result st, List.rev st.trace)
 307     | stmt ->
 308       let st' = interpret_stmt st stmt in
 309       iter_small_step debug st'
 310
 311
 312 let add_global_vars =
 313   List.fold_left
 314     (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)
 315
 316 let add_fun_defs =
 317   List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)
 318
 319 let init_prog (st : state) (p : LIN.program) : state =
 320   let mem = add_global_vars (add_fun_defs st.mem p.LIN.functs) p.LIN.vars in
 321   change_mem st mem
 322
 323 let init_sp st =
 324   let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
 325   let sp =
 326     Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
 327   let st = change_mem st mem in
 328   (st, sp)
 329
 330 let init_isp st =
 331   let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
 332   let st = change_mem (change_isp st isp) mem in
 333   let (mem, exit) = Mem.alloc st.mem 1 in
 334   let st = change_exit st exit in
 335   let st = push st (List.nth exit 0) in
 336   let st = push st (List.nth exit 1) in
 337   st
 338
 339 let init_renv st sp =
 340   let f r st = add_reg r Val.undef st in
 341   let st = I8051.RegisterSet.fold f I8051.registers st in
 342   let spl = List.nth sp 0 in
 343   let sph = List.nth sp 1 in
 344   let st = add_reg I8051.spl spl st in
 345   let st = add_reg I8051.sph sph st in
 346   st
 347
 348 let init_main_call st main =
 349   let ptr = Mem.find_global st.mem main in
 350   match Mem.find_fun_def st.mem ptr with
 351     | LIN.F_int def ->
 352       init_fun_call st ptr
 353     | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
 354
 355
 356 (* Before interpreting, the environment is initialized:
 357    - Add function definitions to the memory and reserve space for the globals.
 358    - Allocate memory to emulate the external stack and initialize the external
 359      stack pointer.
 360    - Allocate memory to emulate the internal stack and initialize the internal
 361      stack pointer.
 362    - Initialiaze the physical register environment. All are set to 0, except for
 363      the stack pointer registers that take the high and low bits of the external
 364      stack pointer.
 365    - Initialize a call to the main (set the current program counter to the
 366      beginning of the function).
 367    - Initialize the carry flag to 0. *)
 368
 369 let interpret debug p =
 370   Printf.printf "*** LIN interpret ***\n%!" ;
 371   match p.LIN.main with
 372     | None -> (IntValue.Int32.zero, [])
 373     | Some main ->
 374       let st = empty_state in
 375       let st = init_prog st p in
 376       let (st, sp) = init_sp st in
 377       let st = init_isp st in
 378       let st = init_renv st sp in
 379       let st = init_main_call st main in
 380       let st = change_carry st Val.zero in
 381       iter_small_step debug st