Remove files in mips directory prior to copying in files from mips_new_tc. Hopefully thiis will help git to spot the rename and hence preserve history.

1 files changed, 0 insertions, 404 deletions

diff --git a/mips/run_embed.ml b/mips/run_embed.ml
deleted file mode 100644
index 1bb6d5f6..00000000
--- a/mips/run_embed.ml
+++ /dev/null
@@ -1,404 +0,0 @@
-(**************************************************************************)
-(*     Sail                                                               *)
-(*                                                                        *)
-(*  Copyright (c) 2013-2017                                               *)
-(*    Kathyrn Gray                                                        *)
-(*    Shaked Flur                                                         *)
-(*    Stephen Kell                                                        *)
-(*    Gabriel Kerneis                                                     *)
-(*    Robert Norton-Wright                                                *)
-(*    Christopher Pulte                                                   *)
-(*    Peter Sewell                                                        *)
-(*                                                                        *)
-(*  All rights reserved.                                                  *)
-(*                                                                        *)
-(*  This software was developed by the University of Cambridge Computer   *)
-(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
-(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
-(*                                                                        *)
-(*  Redistribution and use in source and binary forms, with or without    *)
-(*  modification, are permitted provided that the following conditions    *)
-(*  are met:                                                              *)
-(*  1. Redistributions of source code must retain the above copyright     *)
-(*     notice, this list of conditions and the following disclaimer.      *)
-(*  2. Redistributions in binary form must reproduce the above copyright  *)
-(*     notice, this list of conditions and the following disclaimer in    *)
-(*     the documentation and/or other materials provided with the         *)
-(*     distribution.                                                      *)
-(*                                                                        *)
-(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
-(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
-(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
-(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
-(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
-(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
-(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
-(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
-(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
-(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
-(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
-(*  SUCH DAMAGE.                                                          *)
-(**************************************************************************)
-
-open Printf ;;
-open Big_int_Z ;;
-open Sail_values;;
-open Mips_extras_ml;;
-
-let interact_print = ref true
-let result_print = ref true
-let error_print = ref true
-let interactf : ('a, out_channel, unit) format -> 'a =
-  function f -> if !interact_print then printf f else ifprintf stderr f
-let errorf : ('a, out_channel, unit) format -> 'a =
-  function f -> if !error_print then printf f else ifprintf stderr f
-let resultf : ('a, out_channel, unit) format -> 'a =
-  function f -> if !result_print then printf f else ifprintf stderr f
-
-let rec foldli f acc ?(i=0) = function
-  | [] -> acc
-  | x::xs -> foldli f (f i acc x) ~i:(i+1) xs;;
-
-let big_int_to_hex i = Z.format "%x" i
-let big_int_to_hex64 i = Z.format "%016x" i
-
-let input_buf = (ref [] : int list ref);;
-
-let max_cut_off = ref false
-let max_instr = ref 0
-let model_arg = ref "cheri"
-let raw_list = ref []
-
-let args = [
-  ("--model", Arg.Set_string model_arg, "CPU model to use (mips, cheri, cheri128)");
-  ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop");
-  ("--trace", Arg.Set trace_writes, "trace all register writes"); (* trace_writes is in sail_values.ml *)
-  ("--quiet", Arg.Clear interact_print, "suppress trace of PC");
-  ("--undef", Arg.String (fun s -> undef_val := bit_of_string s), "value to use for undef (u,0,1)");
-]
-
-module type ISA_model = sig
-  type ast
-  val init_model : unit -> unit
-  val inc_nextPC : unit -> unit
-  val get_pc  : unit -> big_int
-  val translate_pc : unit -> big_int option
-  val get_opcode : big_int -> value
-  val decode : value -> ast option
-  val execute : ast -> unit
-  val is_halt : ast -> bool
-  val print_results : unit -> unit
-end
-
-let rec debug_print_gprs gprs start stop =
-  let gpr_val = vector_access gprs (big_int_of_int start) in
-  let gpr_str = 
-    if has_undef gpr_val then
-      "uuuuuuuuuuuuuuuu"
-    else
-      big_int_to_hex64 (unsigned_big(gpr_val)) in
-  resultf "DEBUG MIPS REG %.2d 0x%s\n" start gpr_str;
-  if start < stop
-  then debug_print_gprs gprs (start + 1) stop
-  else ()
-
-let cap_reg_to_string reg =
-  "0b" ^ (string_of_bit_array (get_barray reg))
-
-let read_bit_reg = function
-  | Vregister (array,_,_,_,_) -> (!array).(0) = Vone
-  | _ -> failwith "read_bit_reg of non-reg"
-
-let rec debug_print_caps capregs start stop =
-  let cap_val = vector_access capregs (big_int_of_int start) in
-  let cap_str = cap_reg_to_string cap_val in
-  resultf "DEBUG CAP REG %.2d %s\n" start cap_str;
-  if start < stop
-  then debug_print_caps capregs (start + 1) stop
-  else ()
-
-let handle_uart uart_written uart_wdata uart_rdata uart_rvalid =
-  (try
-    let (pending, _, _) = Unix.select [Unix.stdin] [] [] 0.0 in
-    if pending != [] then
-      input_buf := (!input_buf) @ [(input_byte stdin)]
-  with _ -> ());
-
-  if (read_bit_reg uart_written) then
-    begin
-      let b = unsigned_int(uart_wdata) in
-      printf "%c" (Char.chr b);
-      printf "%!";
-      set_register uart_written (to_vec_dec_int (1,0))
-    end;
-  
-  if not (read_bit_reg uart_rvalid) then
-    (match !input_buf with
-     | x :: xs -> 
-        begin
-          set_register uart_rdata (to_vec_dec_int (8, x));
-          set_register uart_rvalid (to_vec_dec_int (1, 1));
-          input_buf := xs;
-        end
-     | _ -> ())
-
-module MIPS_model : ISA_model = struct
-  type ast = Mips_embed._ast
-
-  let init_model () = 
-    let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
-    set_register Mips_embed._nextPC start_addr;
-    set_register_field_bit Mips_embed._CP0Status "BEV" Vone
-
-  let inc_nextPC () = 
-    handle_uart Mips_embed._UART_WRITTEN Mips_embed._UART_WDATA Mips_embed._UART_RDATA Mips_embed._UART_RVALID;
-
-    set_register Mips_embed._inBranchDelay Mips_embed._branchPending;
-    set_register Mips_embed._branchPending (to_vec_dec_int (1, 0));
-    set_register Mips_embed._PC Mips_embed._nextPC;
-    let inBranchDelay = read_bit_reg Mips_embed._inBranchDelay in
-    if inBranchDelay then
-      set_register Mips_embed._nextPC Mips_embed._delayedPC
-    else
-      let pc_vaddr = unsigned_big(Mips_embed._PC) in
-      let npc_addr = add_int_big_int 4 pc_vaddr in
-      let npc_vec = to_vec_dec_big (bi64, npc_addr) in
-      set_register Mips_embed._nextPC npc_vec
-
-  let get_pc () = unsigned_big (Mips_embed._PC)
-
-  let translate_pc () = 
-    try
-      Some (unsigned_big(Mips_embed._TranslatePC(Mips_embed._PC)))
-    with Sail_exit -> None
-
-  let get_opcode pc_a = Mips_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4))
-
-  let decode = Mips_embed._decode
-
-  let execute = Mips_embed._execute
-  let is_halt i = (i = Mips_embed.HCF)
-  let print_results () =
-    begin
-      resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Mips_embed._PC));
-      debug_print_gprs Mips_embed._GPR 0 31;
-    end
-end
-
-module CHERI_model : ISA_model = struct
-  type ast = Cheri_embed._ast
-
-  let init_model () = 
-    let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
-    set_register Cheri_embed._nextPC start_addr;
-    set_register_field_bit Cheri_embed._CP0Status "BEV" Vone;
-    let initial_cap_val_int = big_int_of_string "0x100000000fffffffe00000000000000000000000000000000ffffffffffffffff" in
-    let initial_cap_vec = to_vec_dec ((big_int_of_int 257), initial_cap_val_int) in 
-    set_register Cheri_embed._PCC initial_cap_vec;
-    set_register Cheri_embed._nextPCC initial_cap_vec;
-    set_register Cheri_embed._delayedPCC initial_cap_vec;
-    cap_size_shift := 5; (* configure memory model cap_size in mips_extras_ml *)
-    for i = 0 to 31 do
-      set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec
-    done
-
-  let inc_nextPC () = 
-    handle_uart Cheri_embed._UART_WRITTEN Cheri_embed._UART_WDATA Cheri_embed._UART_RDATA Cheri_embed._UART_RVALID;
-
-    set_register Cheri_embed._inBranchDelay Cheri_embed._branchPending;
-    set_register Cheri_embed._branchPending (to_vec_dec_int (1, 0));
-    set_register Cheri_embed._PC Cheri_embed._nextPC;
-    set_register Cheri_embed._PCC Cheri_embed._nextPCC;
-    let inBranchDelay = read_bit_reg Cheri_embed._inBranchDelay in
-    if inBranchDelay then
-       begin
-         set_register Cheri_embed._nextPC Cheri_embed._delayedPC;
-         set_register Cheri_embed._nextPCC Cheri_embed._delayedPCC;
-       end
-    else
-       let pc_vaddr = unsigned_big(Cheri_embed._PC) in
-       let npc_addr = add_int_big_int 4 pc_vaddr in
-       let npc_vec = to_vec_dec_big (bi64, npc_addr) in
-       begin
-         set_register Cheri_embed._nextPC npc_vec;
-         set_register Cheri_embed._inCCallDelay (to_vec_dec_int (1, 0))
-       end
-
-  let get_pc () = unsigned_big (Cheri_embed._PC)
-
-  let translate_pc () = 
-    try
-      Some (unsigned_big(Cheri_embed._TranslatePC(Cheri_embed._PC)))
-    with Sail_exit -> None
-
-  let get_opcode pc_a = Cheri_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4))
-
-  let decode = Cheri_embed._decode
-
-  let execute = Cheri_embed._execute
-  let is_halt i = (i = Cheri_embed.HCF)
-  let print_results () =
-    begin
-      resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Cheri_embed._PC));
-      debug_print_gprs Cheri_embed._GPR 0 31;
-      resultf "DEBUG CAP PCC %s\n" (cap_reg_to_string Cheri_embed._PCC);
-      debug_print_caps Cheri_embed._CapRegs 0 31;
-    end 
-end
-
-module CHERI128_model : ISA_model = struct
-  type ast = Cheri128_embed._ast
-
-  let init_model () = 
-    let start_addr = (to_vec_dec_big (bi64, big_int_of_string "0x9000000040000000")) in
-    set_register Cheri128_embed._nextPC start_addr;
-    set_register_field_bit Cheri128_embed._CP0Status "BEV" Vone;
-    let initial_cap_val_int = big_int_of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *)
-    let initial_cap_vec = to_vec_dec ((bi129), initial_cap_val_int) in 
-    set_register Cheri128_embed._PCC initial_cap_vec;
-    set_register Cheri128_embed._nextPCC initial_cap_vec;
-    set_register Cheri128_embed._delayedPCC initial_cap_vec;
-    cap_size_shift := 4; (* configure memory model cap_size in mips_extras_ml *)
-    for i = 0 to 31 do
-      set_register (vector_access_int Cheri128_embed._CapRegs i) initial_cap_vec
-    done
-
-  let inc_nextPC () = 
-    handle_uart Cheri128_embed._UART_WRITTEN Cheri128_embed._UART_WDATA Cheri128_embed._UART_RDATA Cheri128_embed._UART_RVALID;
-
-    set_register Cheri128_embed._inBranchDelay Cheri128_embed._branchPending;
-    set_register Cheri128_embed._branchPending (to_vec_dec_int (1, 0));
-    set_register Cheri128_embed._PC Cheri128_embed._nextPC;
-    set_register Cheri128_embed._PCC Cheri128_embed._nextPCC;
-    let inBranchDelay = read_bit_reg Cheri128_embed._inBranchDelay in
-    if inBranchDelay then
-       begin
-         set_register Cheri128_embed._nextPC Cheri128_embed._delayedPC;
-         set_register Cheri128_embed._nextPCC Cheri128_embed._delayedPCC;
-       end
-    else
-       let pc_vaddr = unsigned_big(Cheri128_embed._PC) in
-       let npc_addr = add_int_big_int 4 pc_vaddr in
-       let npc_vec = to_vec_dec_big (bi64, npc_addr) in
-       begin
-         set_register Cheri128_embed._nextPC npc_vec;
-         set_register Cheri128_embed._inCCallDelay (to_vec_dec_int (1, 0))
-       end
-
-  let get_pc () = unsigned_big (Cheri128_embed._PC)
-
-  let translate_pc () = 
-    try
-      Some (unsigned_big(Cheri128_embed._TranslatePC(Cheri128_embed._PC)))
-    with Sail_exit -> None
-
-  let get_opcode pc_a = Cheri128_embed._reverse_endianness(_MEMr (to_vec_dec_big (bi64, pc_a), bi4))
-
-  let decode = Cheri128_embed._decode
-
-  let execute = Cheri128_embed._execute
-  let is_halt i = (i = Cheri128_embed.HCF)
-  let print_results () =
-    begin
-      resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex (unsigned_big Cheri128_embed._PC));
-      debug_print_gprs Cheri128_embed._GPR 0 31;
-      resultf "DEBUG CAP PCC %s\n" (cap_reg_to_string Cheri128_embed._PCC);
-      debug_print_caps Cheri128_embed._CapRegs 0 31;
-    end 
-end
-
-let time_it action arg =
-  let start_time = Sys.time () in
-  let ret = action arg in
-  let finish_time = Sys.time () in
-  (finish_time -. start_time, ret)
-
-let rec fde_loop (model, count) =
-  if !max_cut_off && count = !max_instr
-  then begin
-      resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count;
-      count
-    end
-  else 
-    begin
-    let module Model = (val model : ISA_model) in
-
-    Model.inc_nextPC ();
-    if !interact_print then
-      interactf "\n**** instruction %d from address %s ****\n"
-                count (big_int_to_hex64 (Model.get_pc ()));
-    let m_paddr = Model.translate_pc () in
-    match m_paddr with
-      | Some pc ->
-          let opcode = Model.get_opcode pc in
-          if !interact_print then
-            interactf "decode: 0x%x\n" (unsigned_int(opcode));
-          let instruction = Model.decode opcode in
-          let i = match instruction with
-            | Some (i) -> i
-            | _ ->  begin
-                errorf "\n**** Decode error ****\n"; 
-                exit 1;
-              end
-          in
-          if Model.is_halt i then 
-            begin
-              Model.print_results ();
-              resultf "\nSUCCESS program terminated after %d instructions\n" count;
-              count
-            end
-          else
-            begin
-              (try
-                Model.execute(i)
-              with Sail_exit -> ()); (* exception during execute *)
-              fde_loop (model, count + 1)
-            end
-      | None -> (* Exception during PC translation *)
-          fde_loop (model, count + 1)
-  end
-
-let rec load_raw_file buf addr len chan =
-    let to_read = min_int len page_size_bytes in
-    really_input chan buf 0 to_read;
-    add_mem_bytes addr buf 0 to_read;
-    if (len > to_read) then
-      load_raw_file buf (add_int_big_int to_read addr) (len - to_read) chan
-
-let get_model = function
-  | "cheri128" -> (module CHERI128_model : ISA_model)
-  | "cheri" -> (module CHERI_model : ISA_model)
-  | "mips" -> (module MIPS_model : ISA_model)
-  | _ -> failwith "unknown model name"
-
-let anon_raw s = 
-  (* some input validation would be nice... *)
-  let len = String.length s in
-  let atidx = try
-      String.index s '@' 
-    with Not_found -> raise (Arg.Bad "expected argument of form file@addr") in
-  let f = String.sub s 0 atidx in
-  let addr =  String.sub s (atidx+1) (len - atidx -1) in
-  raw_list := (!raw_list) @ [(f, big_int_of_string addr)]
-
-let load_raw_arg (f, a) =
-  let buf = Bytes.create page_size_bytes in
-  let chan = open_in_bin f in
-  let len = in_channel_length chan in
-  load_raw_file buf a len chan
-
-let run () =
-  (* Turn off line-buffering of standard input to allow responsive console input  *)
-  if Unix.isatty (Unix.stdin) then begin
-    let tattrs = Unix.tcgetattr (Unix.stdin) in
-    Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false})
-  end;
-  Arg.parse args anon_raw "" ;
-  List.iter load_raw_arg !raw_list;
-  let model = get_model !model_arg in
-  let module Model = (val model  : ISA_model) in
-  Model.init_model ();
-  let (t, count) = time_it fde_loop (model, 0) in
-  resultf "Execution time: %f seconds %f IPS \n" t (float(count) /. t);;
-
-run () ;;