source: Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml @ 818

(** This module provides an interpreter for the ERTL language. *)


let error_prefix = "ERTL interpret"
let error s = Error.global_error error_prefix s


module Mem = Driver.ERTLMemory
module Val = Mem.Value
let chunk = Driver.ERTLMemory.int_size
module Eval = I8051.Eval (Val)


(* Memory *)

type memory = ERTL.function_def Mem.memory

(* Local environments. They associate a value to the pseudo-registers of the
   function being executed. *)

type local_env = Val.t Register.Map.t

(* Hardware registers environments. They associate a value to each hardware
   register. *)

type hdw_reg_env = Val.t I8051.RegisterMap.t

(* Call frames. The execution state has a call stack, each element of the stack
   being composed of the local environment to resume the execution of the
   caller. *)

type stack_frame = local_env

(* Execution states. *)

type state =
    { st_frs : stack_frame list ;
      pc     : Val.address ;
      isp    : Val.address ;
      exit   : Val.address ;
      lenv   : local_env ;
      carry  : Val.t ;
      renv   : hdw_reg_env ;
      mem    : memory ;
      trace  : CostLabel.t list }


(* Helpers *)

let add_st_frs st frame = { st with st_frs = frame :: st.st_frs }
let pop_st_frs st = match st.st_frs with
  | [] -> error "Empty stack frames."
  | lenv :: st_frs -> { st with st_frs = st_frs ; lenv = lenv }
let change_pc st pc = { st with pc = pc }
let change_isp st isp = { st with isp = isp }
let change_exit st exit = { st with exit = exit }
let change_lenv st lenv = { st with lenv = lenv }
let change_carry st carry = { st with carry = carry }
let change_renv st renv = { st with renv = renv }
let change_mem st mem = { st with mem = mem }
let change_trace st trace = { st with trace = trace }
let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)

let empty_state =
  { st_frs = [] ;
    pc     = Val.null ;
    isp    = Val.null ;
    exit   = Val.null ;
    lenv   = Register.Map.empty ;
    carry  = Val.undef ;
    renv   = I8051.RegisterMap.empty ;
    mem    = Mem.empty ;
    trace  = [] }


(* Each label of each function is associated an address. The base of this
   address is the base of the function in memory. Inside a function, offsets are
   bijectively associated to labels. *)

module Labels_Offsets = Bijection.Make (Label) (Val.Offset)

let labels_offsets_internal int_fun =
  let f lbl _ (lbls_offs, i) =
    (Labels_Offsets.add1 lbl i lbls_offs, Val.Offset.succ i) in
  Label.Map.fold f int_fun.ERTL.f_graph

(* [labels_offsets p] builds a bijection between the labels found in the
   functions of [p] and some memory addresses. *)

let labels_offsets p =
  let f (lbls_offs, i) (_, def) = match def with
    | ERTL.F_int int_fun -> labels_offsets_internal int_fun (lbls_offs, i)
    | _ -> (lbls_offs, i) in
  fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.ERTL.functs)

let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
  | ERTL.F_int def -> def
  | _ -> error "Trying to fetch the definition of an external function."

let fetch_stmt lbls_offs st =
  let msg =
    Printf.sprintf "%s does not point to a statement."
      (Val.string_of_address st.pc) in
  if Val.is_mem_address st.pc then
    let off = Val.offset_of_address st.pc in
    let def = fun_def_of_ptr st.mem st.pc in
    let lbl = Labels_Offsets.find2 off lbls_offs in
    Label.Map.find lbl def.ERTL.f_graph
  else error msg

let entry_pc lbls_offs ptr def =
  let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in
  Val.change_address_offset ptr off

let init_fun_call lbls_offs st ptr def =
  let f r lenv = Register.Map.add r Val.undef lenv in
  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
  let pc = entry_pc lbls_offs ptr def in
  change_lenv (change_pc st pc) lenv

let next_pc lbls_offs st lbl =
  let off = Labels_Offsets.find1 lbl lbls_offs in
  change_pc st (Val.change_address_offset st.pc off)

let framesize st =
  if Val.is_mem_address st.pc then
    let def = fun_def_of_ptr st.mem st.pc in
    def.ERTL.f_stacksize
  else error "No function at the given address."

type register = Hdw of I8051.register | Psd of Register.t

let add_reg r v st = match r with
  | Hdw r ->
    let renv = I8051.RegisterMap.add r v st.renv in
    change_renv st renv
  | Psd r ->
    let lenv = Register.Map.add r v st.lenv in
    change_lenv st lenv

let get_reg r st = match r with
  | Hdw r ->
    if I8051.RegisterMap.mem r st.renv then I8051.RegisterMap.find r st.renv
    else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
  | Psd r ->
    if Register.Map.mem r st.lenv then Register.Map.find r st.lenv
    else error ("Unknown local register " ^ (Register.print r) ^ ".")

let push st v =
  let mem = Mem.store st.mem chunk st.isp v in
  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
  change_mem (change_isp st isp) mem

let pop st =
  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
  let st = change_isp st isp in
  let v = Mem.load st.mem chunk st.isp in
  (st, v)

let get_ra st =
  let (st, pch) = pop st in
  let (st, pcl) = pop st in
  [pcl ; pch]

let save_ra lbls_offs st lbl =
  let ra =
    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
  let st = push st (List.nth ra 0) in
  let st = push st (List.nth ra 1) in
  st

let save_frame st = add_st_frs st st.lenv

let label_of_pointer lbls_offs ptr =
(*
  Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
*)
  let off = Val.offset_of_address ptr in
  Labels_Offsets.find2 off lbls_offs

let pointer_of_label lbls_offs ptr lbl =
  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)

let get_sp st =
  List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]

let set_sp vs st =
  let spl = List.nth vs 0 in
  let sph = List.nth vs 1 in
  let st = add_reg (Hdw I8051.spl) spl st in
  let st = add_reg (Hdw I8051.sph) sph st in
  st


module InterpretExternal = Primitive.Interpret (Mem)

let interpret_external mem f args = match InterpretExternal.t mem f args with
  | (mem', InterpretExternal.V vs) -> (mem', vs)
  | (mem', InterpretExternal.A addr) -> (mem', addr)

let fetch_external_args f st =
  let size = Mem.size_of_quantity (Primitive.args_byte_size f) in
  let params = MiscPottier.prefix size I8051.parameters in
  List.map (fun r -> get_reg (Hdw r) st) params

let set_result st vs =
  let f st (r, v) = add_reg (Hdw r) v st in
  List.fold_left f st (MiscPottier.combine I8051.rets vs)

let interpret_external_call st f next_pc =
  let args = fetch_external_args f st in
  let (mem, vs) = interpret_external st.mem f args in
  let st = change_mem st mem in
  let st = set_result st vs in
  change_pc st next_pc

let interpret_call lbls_offs st f ra =
  let ptr = Mem.find_global st.mem f in
  match Mem.find_fun_def st.mem ptr with
    | ERTL.F_int def ->
      let st = save_ra lbls_offs st ra in
      let st = save_frame st in
      init_fun_call lbls_offs st ptr def
    | ERTL.F_ext def ->
      let next_pc = 
        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
      interpret_external_call st def.AST.ef_tag next_pc

let interpret_return lbls_offs st =
  let st = pop_st_frs st in
  let (st, pch) = pop st in
  let (st, pcl) = pop st in
  let pc = [pcl ; pch] in
  change_pc st pc


(* Interpret statements. *)

let interpret_stmt lbls_offs st stmt =
  let next_pc = next_pc lbls_offs in
  match stmt with

    | ERTL.St_skip lbl ->
      next_pc st lbl

    | ERTL.St_comment (s, lbl) ->
(*
      Printf.printf "*** %s ***\n\n%!" s ;
*)
      next_pc st lbl

    | ERTL.St_cost (cost_lbl, lbl) ->
      let st = add_trace st cost_lbl in
      next_pc st lbl

    | ERTL.St_get_hdw (destr, srcr, lbl) ->
      let st = add_reg (Psd destr) (get_reg (Hdw srcr) st) st in
      next_pc st lbl

    | ERTL.St_set_hdw (destr, srcr, lbl) ->
      let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
      next_pc st lbl

    | ERTL.St_hdw_to_hdw (destr, srcr, lbl) ->
      let st = add_reg (Hdw destr) (get_reg (Hdw srcr) st) st in
      next_pc st lbl

    | ERTL.St_newframe lbl ->
      let size = framesize st in
      let sp = get_sp st in
      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
      let st = set_sp new_sp st in
      next_pc st lbl

    | ERTL.St_delframe lbl ->
      let size = framesize st in
      let sp = get_sp st in
      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
      let st = set_sp new_sp st in
      next_pc st lbl

    | ERTL.St_framesize (destr, lbl) ->
      let size = framesize st in
      let st = add_reg (Psd destr) (Val.of_int size) st in
      next_pc st lbl

    | ERTL.St_pop (destr, lbl) ->
      let (st, v) = pop st in
      let st = add_reg (Psd destr) v st in
      next_pc st lbl

    | ERTL.St_push (srcr, lbl) ->
      let v = get_reg (Psd srcr) st in
      let st = push st v in
      next_pc st lbl

    | ERTL.St_addrH (r, x, lbl) ->
      let vs = Mem.find_global st.mem x in
      let st = add_reg (Psd r) (List.nth vs 1) st in
      next_pc st lbl

    | ERTL.St_addrL (r, x, lbl) ->
      let vs = Mem.find_global st.mem x in
      let st = add_reg (Psd r) (List.nth vs 0) st in
      next_pc st lbl

    | ERTL.St_int (r, i, lbl) ->
      let st = add_reg (Psd r) (Val.of_int i) st in
      next_pc st lbl

    | ERTL.St_move (destr, srcr, lbl) ->
      let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
      next_pc st lbl

    | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) ->
      let (v, _) =
        Eval.opaccs opaccs
          (get_reg (Psd srcr1) st)
          (get_reg (Psd srcr2) st) in
      let st = add_reg (Psd destr) v st in
      next_pc st lbl

    | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) ->
      let (_, v) =
        Eval.opaccs opaccs
          (get_reg (Psd srcr1) st)
          (get_reg (Psd srcr2) st) in
      let st = add_reg (Psd destr) v st in
      next_pc st lbl

    | ERTL.St_op1 (op1, destr, srcr, lbl) ->
      let v = Eval.op1 op1 (get_reg (Psd srcr) st) in
      let st = add_reg (Psd destr) v st in
      next_pc st lbl

    | ERTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
      let (v, carry) =
        Eval.op2 st.carry op2
          (get_reg (Psd srcr1) st)
          (get_reg (Psd srcr2) st) in
      let st = change_carry st carry in
      let st = add_reg (Psd destr) v st in
      next_pc st lbl

    | ERTL.St_clear_carry lbl ->
      let st = change_carry st Val.zero in
      next_pc st lbl

    | ERTL.St_set_carry lbl ->
      let st = change_carry st (Val.of_int 1) in
      next_pc st lbl

    | ERTL.St_load (destr, addr1, addr2, lbl) ->
      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
      let v = Mem.load st.mem chunk addr in
      let st = add_reg (Psd destr) v st in
      next_pc st lbl

    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
      let st = change_mem st mem in
      next_pc st lbl

    | ERTL.St_call_id (f, _, lbl) ->
      interpret_call lbls_offs st f lbl

    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
      let v = get_reg (Psd srcr) st in
      let lbl =
        if Val.is_true v then lbl_true
        else
          if Val.is_false v then lbl_false
          else error "Undecidable branchment." in
      next_pc st lbl

    | ERTL.St_return _ ->
      interpret_return lbls_offs st


let print_lenv lenv =
  let f r v =
    if not (Val.eq v Val.undef) then
      Printf.printf "\n%s = %s%!" (Register.print r) (Val.to_string v) in
  Register.Map.iter f lenv

let print_renv renv =
  let f r v =
    if not (Val.eq v Val.undef) then
    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
  I8051.RegisterMap.iter f renv

let current_label lbls_offs st =
  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs

let print_state lbls_offs st =
  Printf.printf "PC: %s (%s)\n%!"
    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
  Printf.printf "Carry: %s%!" (Val.to_string st.carry) ;
  print_lenv st.lenv ;
  print_renv st.renv ;
  Mem.print st.mem ;
  Printf.printf "\n%!"

let compute_result st ret_regs =
  let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
  let f res v = res && (Val.is_int v) in
  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
  if is_int vs then
    let chunks =
      List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in
    IntValue.Int32.merge chunks
  else IntValue.Int32.zero

let rec iter_small_step debug lbls_offs st =
  let print_and_return_result (res, cost_labels) =
    if debug then Printf.printf "Result = %s\n%!"
      (IntValue.Int32.to_string res) ;
    (res, cost_labels) in
  if debug then print_state lbls_offs st ;
  match fetch_stmt lbls_offs st with
    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
      print_and_return_result (compute_result st ret_regs, List.rev st.trace)
    | stmt ->
      let st' = interpret_stmt lbls_offs st stmt in
      iter_small_step debug lbls_offs st'


let add_global_vars =
  List.fold_left
    (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None)

let add_fun_defs =
  List.fold_left (fun mem (f_id, f_def) -> Mem.add_fun_def mem f_id f_def)

let init_prog (st : state) (p : ERTL.program) : state =
  let mem = add_global_vars (add_fun_defs st.mem p.ERTL.functs) p.ERTL.vars in
  change_mem st mem

let init_sp st =
  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
  let sp =
    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
  let st = change_mem st mem in
  (st, sp)

let init_isp st =
  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
  let st = change_mem (change_isp st isp) mem in
  let (mem, exit) = Mem.alloc st.mem 1 in
  let st = change_exit st exit in
  let st = push st (List.nth exit 0) in
  let st = push st (List.nth exit 1) in
  st  

let init_renv st sp =
  let f r renv = I8051.RegisterMap.add r Val.undef renv in
  let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
  let spl = List.nth sp 0 in
  let sph = List.nth sp 1 in
  let renv = I8051.RegisterMap.add I8051.sph sph renv in
  let renv = I8051.RegisterMap.add I8051.spl spl renv in
  change_renv st renv

let init_main_call lbls_offs st main =
  let ptr = Mem.find_global st.mem main in
  match Mem.find_fun_def st.mem ptr with
    | ERTL.F_int def ->
      init_fun_call lbls_offs st ptr def
    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")


(* Before interpreting, the environment is initialized:
   - Build a bijection between the labels in the program and some values (taken
     amongst the offsets).
   - Add function definitions to the memory and reserve space for the globals.
   - Allocate memory to emulate the external stack and initialize the external
     stack pointer.
   - Allocate memory to emulate the internal stack and initialize the internal
     stack pointer.
   - Initialiaze the physical register environment. All are set to 0, except for
     the stack pointer registers that take the high and low bits of the external
     stack pointer.
   - Initialize a call to the main (set the current program counter to the
     beginning of the function).
   - Initialize the carry flag to 0. *)

let interpret debug p =
  Printf.printf "*** ERTL interpret ***\n%!" ;
  match p.ERTL.main with
    | None -> (IntValue.Int32.zero, [])
    | Some main ->
      let lbls_offs = labels_offsets p in
      let st = empty_state in
      let st = init_prog st p in
      let (st, sp) = init_sp st in
      let st = init_isp st in
      let st = init_renv st sp in
      let st = init_main_call lbls_offs st main in
      let st = change_carry st Val.zero in
      iter_small_step debug lbls_offs st