build a single run_embed.native with mips and cheri models linked and choose between them using a command line switch.

1 files changed, 167 insertions, 70 deletions

diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index 8b752f03..ce5c8fe0 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -44,10 +44,6 @@ open Printf ;;
 open Big_int_Z ;;
 open Sail_values;;
 open Mips_extras_ml;;
-(* The linksem ELF interface *)
-open Sail_interface ;;
-
-module Mips_model=Mips_embed;;
 
 let interact_print = ref true
 let result_print = ref true
@@ -80,7 +76,7 @@ let big_int_to_hex64 i =
     (String.make (16-len) '0') ^ hex
   else
     hex
-    
+
 let input_buf = (ref [] : int list ref);;
 
 let add_mem byte addr mem = begin
@@ -94,22 +90,33 @@ let max_instr = ref 0
 let raw_file = ref ""
 let raw_at   = ref ""
 let elf_file = ref ""
+let model_arg = ref "cheri"
 
 let args = [
+  ("--model", Arg.Set_string model_arg, "CPU model to use (mips, cheri, cheri128)");
   ("--file", Arg.Set_string elf_file, "filename of elf binary to load in memory");
   ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop");
   ("--raw", Arg.Set_string raw_file, "filename of raw file to load in memory");
   ("--at", Arg.Set_string raw_at, "address to load raw file in memory");
+  ("--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");
 ]
 
-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)
+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 start stop =
-  let gpr_val = vector_access Mips_model._GPR (big_int_of_int start) in
+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"
@@ -117,43 +124,147 @@ let rec debug_print_gprs start stop =
       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 (start + 1) stop
+  then debug_print_gprs gprs (start + 1) stop
+  else ()
+
+let cap_reg_to_string reg =
+  "0b" ^ (String.sub (string_of_value reg) 9 257)
+
+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 get_opcode pc_a = Mips_model._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4))
+module MIPS_model : ISA_model = struct
+  type ast = Mips_embed._ast
 
-let get_pc () = begin
+  let init_model () = 
+    let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x9000000040000000")) in
+    set_register Mips_embed._nextPC start_addr;
+    set_register_field_bit Mips_embed._CP0Status "BEV" Vone
+
+  let inc_nextPC () = 
+    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 = unsigned_int(Mips_embed._inBranchDelay) in
+    (match inBranchDelay with
+    | 0 ->
+       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 (big_int_of_int 64, npc_addr) in
+       set_register Mips_embed._nextPC npc_vec;
+    | 1 ->
+       set_register Mips_embed._nextPC Mips_embed._delayedPC;
+    | _ -> failwith "invalid value of inBranchDelay")
+
+  let get_pc () = unsigned_big (Mips_embed._PC)
+
+  let translate_pc () = 
     try
-      Some (unsigned_big(Mips_model._TranslatePC(Mips_model._PC)))
+      Some (unsigned_big(Mips_embed._TranslatePC(Mips_embed._PC)))
     with Sail_exit -> None
-  end
 
+  let get_opcode pc_a = Mips_embed._reverse_endianness(_MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4))
+
+  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 (big_int_of_int 64, hex_to_big_int "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;
+    for i = 0 to 31 do
+      set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec
+    done
+
+  let inc_nextPC () = 
+    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 = unsigned_int(Cheri_embed._inBranchDelay) in
+    (match inBranchDelay with
+    | 0 ->
+       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 (big_int_of_int 64, npc_addr) in
+       set_register Cheri_embed._nextPC npc_vec;
+    | 1 ->
+       begin
+         set_register Cheri_embed._nextPC Cheri_embed._delayedPC;
+         set_register Cheri_embed._nextPCC Cheri_embed._delayedPCC;
+       end
+    | _ -> failwith "invalid value of inBranchDelay")
 
-let rec fde_loop count =
+  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 (big_int_of_int 64, pc_a), big_int_of_int 4))
+
+  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
+
+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 pc_vaddr = unsigned_big(Mips_model._PC) in
-    interactf "\n**** instruction %d from address %s ****\n"
-      count (big_int_to_hex64 pc_vaddr);
-    let m_paddr = get_pc () in
+  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 inBranchDelay = Some(unsigned_int(Mips_model._inBranchDelay)) in
-          (match inBranchDelay with
-          | Some 0 -> 
-            let npc_addr = add_int_big_int 4 pc_vaddr in
-            let npc_vec = to_vec_dec_big (big_int_of_int 64, npc_addr) in
-            set_register Mips_model._nextPC npc_vec;
-          | Some 1 ->
-            set_register Mips_model._nextPC Mips_model._delayedPC;
-          | _ -> failwith "invalid value of inBranchDelay");
-          let opcode = get_opcode pc in
-          let _ = resultf "decode: 0x%x\n" (unsigned_int(opcode)) in
-          let instruction = Mips_model._decode opcode in
+          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
@@ -161,33 +272,23 @@ let rec fde_loop count =
                 exit 1;
               end
           in
-          if (i == Mips_model.HCF)
-          then 
+          if Model.is_halt i then 
             begin
-              resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex pc_vaddr);
-              debug_print_gprs 0 31;
+              Model.print_results ();
               resultf "\nSUCCESS program terminated after %d instructions\n" count;
               count
-            end 
+            end
           else
             begin
               (try
-                Mips_model._execute(i)
-              with Sail_exit -> ());
-              set_register Mips_model._inBranchDelay Mips_model._branchPending;
-              set_register Mips_model._branchPending (to_vec_dec_int (1, 0));
-              set_register Mips_model._PC Mips_model._nextPC;
-              fde_loop (count + 1)
+                Model.execute(i)
+              with Sail_exit -> ()); (* exception during execute *)
+              fde_loop (model, count + 1)
             end
-      | None -> begin (* Exception during PC translation *)
-          set_register Mips_model._inBranchDelay Mips_model._branchPending;
-          set_register Mips_model._branchPending (to_vec_dec_int (1, 0));
-          set_register Mips_model._PC Mips_model._nextPC;
-          fde_loop (count + 1)
-        end
+      | None -> (* Exception during PC translation *)
+          fde_loop (model, count + 1)
   end
 
-
  (*
  (try
    let (pending, _, _)  = (Unix.select [(Unix.stdin)] [] [] 0.0) in
@@ -232,30 +333,26 @@ let rec load_raw_file mem addr chan =
   | End_of_file -> ()
 
 
+let get_model = function
+  | "cheri" -> (module CHERI_model : ISA_model)
+  | "mips" -> (module MIPS_model : ISA_model)
+  | _ -> failwith "unknown model name"
+
 let run () =
   Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ;
-  (*if !elf_file = "" then begin
-    Arg.usage args "";
-    exit 1;
-  end;*)
-(*
-  let ((isa_defs,
-       (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4),
-        isa_externs,
-        isa_model,
-        model_reg_d,
-        startaddr,
-        startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
- *)
+
   if String.length(!raw_file) != 0 then
     load_raw_file mips_mem (big_int_of_string !raw_at) (open_in_bin !raw_file);
-  set_register_field_bit Mips_model._CP0Status "BEV" Vone;
-  let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x9000000040000000")) in
-  set_register Mips_model._PC start_addr;
+
   let name = Filename.basename !raw_file in
-  let (t, count) = time_it fde_loop 0 in
+  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 for file %s: %f seconds %f IPS \n" name t (float(count) /. t);;
 
+
+
 (* 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