open Printf ;;
(*open Interp ;;*)
open Interp_ast ;;
(*open Interp_lib ;;*)
open Interp_interface ;;
open Interp_inter_imp ;;
open Run_interp_model ;;

open Sail_interface ;;

let startaddr = ref [] ;;
let mainaddr  = ref "0" ;;
let sections = ref [] ;;
let file = ref "" ;;
let print_bytes = ref false ;;
let bytes_file = ref "bytes_out.lem";;

let rec foldli f acc ?(i=0) = function
  | [] -> acc
  | x::xs -> foldli f (f i acc x) ~i:(i+1) xs
;;

let big_endian = true ;;

let hex_to_big_int s = Big_int.big_int_of_int64 (Int64.of_string s) ;;

let big_int_to_vec for_mem b size =
  fst (extern_value
	 (make_mode true false)
	 for_mem
	 ((if big_endian then Interp_lib.to_vec_inc else Interp_lib.to_vec_dec)
	     (Interp.V_tuple [(Interp.V_lit (L_aux (L_num size, Unknown))); 
			      (Interp.V_lit (L_aux (L_num b, Unknown)))])))
;;

let mem = ref Mem.empty ;;

let add_mem byte addr =
  assert(byte >= 0 && byte < 256);
  (*Printf.printf "adder is %s, byte is %s\n" (Big_int.string_of_big_int addr) (string_of_int byte);*)
  let addr = big_int_to_vec true addr (Big_int.big_int_of_int 64) in
  (*Printf.printf "adder is %s byte is %s\n" (val_to_string addr) (string_of_int byte);*)
  match addr with
    | Bytevector addr -> mem := Mem.add addr byte !mem
;;

let add_section s =
  match Str.split (Str.regexp ",") s with
  | [name;offset;size;addr] ->
      begin try
        sections := (
          int_of_string offset,
          int_of_string size,
          hex_to_big_int addr) ::
            !sections
      with Failure msg -> raise (Arg.Bad (msg ^ ": " ^ s))
      end
  | _ -> raise (Arg.Bad ("Wrong section format: "^s))
;;

let load_section ic (offset,size,addr) =
  seek_in ic offset;
  for i = 0 to size - 1 do
    add_mem (input_byte ic) (Big_int.add_int_big_int i addr);
  done
;;

let load_memory (bits,addr) =
  let rec loop bits addr = 
    if (Bitstring.bitstring_length bits = 0)
    then ()
    else let (Error.Success(bitsnum,rest)) = Ml_bindings.read_unsigned_char Endianness.default_endianness bits in
	 add_mem (Uint32.to_int bitsnum) (Big_int.big_int_of_int addr);
	 loop rest (1 + addr)
  in loop bits addr

let lem_print_memory m =
  let format_addr a = "[" ^ (List.fold_right (fun i r -> "(" ^ (string_of_int i) ^ ": word8);" ^ r) a "") ^ "]" in
  let preamble = "open import Pervasives\ntype word8 = nat\n" in
  let start_addr = "let start_adder_address = " ^ format_addr !startaddr ^ ";;\n" in
  let start_list_def = "let instruction_byte_list = [" in
  let list_elements = 
    Mem.fold (fun key byte rest -> 
      rest ^ "(" ^ (format_addr key) ^ ", (" ^ (string_of_int byte) ^ ":word8) );\n") m "" in
  let close_list_def = "];;" in
  let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
  let o' = Format.formatter_of_out_channel o in
  Format.fprintf o' "%s" (preamble ^ start_addr ^ start_list_def ^ list_elements ^ close_list_def);
  let _ = close_out o in
  Sys.rename temp_file_name !bytes_file 

(* use zero as a sentinel --- it might prevent a minimal loop from
 * working in principle, but won't happen in practice *)
let lr_init_value = Big_int.zero_big_int

let init_reg () =
  let init name value size =
    (* fix index - this is necessary for CR, indexed from 32 *)
    let offset = function
      | Bitvector(bits,inc,fst) ->
        Bitvector(bits,inc,Big_int.big_int_of_int (64 - size))
     | _ -> assert false in
    name, offset (big_int_to_vec false value (Big_int.big_int_of_int size)) in
  List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
    (* XXX execute main() directly until we can handle the init phase *)
    init "CIA" (hex_to_big_int !mainaddr) 64;
    init "GPR0" Big_int.zero_big_int 64;
    init "GPR1" Big_int.zero_big_int 64;
    init "GPR2" Big_int.zero_big_int 64;
    init "GPR31" Big_int.zero_big_int 64;
    init "CTR" Big_int.zero_big_int 64;
    init "CR" Big_int.zero_big_int 32;
    init "LR" lr_init_value 64;
    init "XER" Big_int.zero_big_int 64;
    "mode64bit", Bitvector([true],true,Big_int.zero_big_int);
  ]
;;

let eager_eval = ref true

let args = [
  ("--file", Arg.Set_string file, "filename binary code to load in memory");
  ("--data", Arg.String add_section, "name,offset,size,addr add a data section");
  ("--code", Arg.String add_section, "name,offset,size,addr add a code section");
  (*("--startaddr", Arg.Set_string startaddr, "addr initial address (UNUSED)");*)
  ("--mainaddr", Arg.Set_string mainaddr, "addr address of the main section (entry point; default: 0)");
  ("--quiet", Arg.Clear Run_interp_model.debug, " do not display interpreter actions");
  ("--interactive", Arg.Clear eager_eval , " interactive execution");
  ("--dump", Arg.Set print_bytes , " do not run, just generate a lem file of a list of bytes");
  ("--out", Arg.Set_string bytes_file, " specify the name for a file generated by --dump");
] ;;

let time_it action arg =
  let start_time = Sys.time () in
  ignore (action arg);
  let finish_time = Sys.time () in
  finish_time -. start_time
;;

let get_reg reg name =
  let reg_content = Reg.find name reg in reg_content
;;

let eq_zero = function
  | Bitvector(bools,_,_) -> List.for_all (not) bools
;;

let rec fde_loop count main_func parameters mem reg ?mode track_dependencies prog =
  debugf "\n**** instruction %d  ****\n" count;
  match Run_interp_model.run ~main_func ~parameters ~mem ~reg ~eager_eval:!eager_eval ~track_dependencies:(ref track_dependencies) ?mode prog with
  | false, _,_, _ -> eprintf "FAILURE\n"; exit 1
  | true, mode, track_dependencies, (reg, mem) ->
      if eq_zero (get_reg reg "CIA") then
        eprintf "\nSUCCESS: returned with value %s\n"
          (Printing_functions.val_to_string (get_reg reg "GPR3"))
      else
        fde_loop (count+1) main_func parameters mem reg ~mode:mode track_dependencies prog
;;

let run () =
  Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ;
  if !file = "" then begin
    Arg.usage args "";
    exit 1;
  end;
  if !eager_eval then Run_interp_model.debug := true;
  let (locations,start_address) = populate !file in
  let total_size = (List.length locations) in
  eprintf "Loading binary into memory (%d sections)... %!" total_size;
  let t = time_it (List.iter load_memory) locations in
  eprintf "done. (%f seconds)\n%!" t;
  let rec reading loc length = 
    if length = 0  
    then []
    else 
      let location = big_int_to_vec true loc (Big_int.big_int_of_int 64) in
      match location with
	| Bytevector location ->
	  (Mem.find location !mem)::(reading (Big_int.add_big_int loc Big_int.unit_big_int) (length - 1)) in
  let addr = reading (Big_int.big_int_of_int start_address) 8 in
  let _ = begin
    startaddr := addr;
    mainaddr := "0x" ^ (List.fold_left (^) "" (List.map (Printf.sprintf "%02x") addr));
  end in
  let reg = init_reg () in
  (* entry point: unit -> unit fde *)
  let funk_name = "fde" in
  let parms = [] in
  let name = Filename.basename !file in
  if !print_bytes 
  then lem_print_memory !mem
  else let t =time_it (fun () -> fde_loop 0 funk_name parms !mem reg false (name, Power.defs)) () in
       eprintf "Execution time: %f seconds\n" t
;;

run () ;;