Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

2 files changed, 76 insertions, 49 deletions

diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml
index 1565c7c6..29f4a13d 100644
--- a/mips/mips_extras_ml.ml
+++ b/mips/mips_extras_ml.ml
@@ -23,7 +23,7 @@ let _MEMval (addr, size, data) =
   for i = 0 to (s - 1) do
     let bit_idx = i * 8 in
     let byte = unsigned_int(slice_raw (data, big_int_of_int bit_idx, big_int_of_int (bit_idx + 7))) in
-    let byte_addr = add_int_big_int i a in
+    let byte_addr = add_int_big_int (s-1-i) a in
     begin
       (*printf "MEM [%s] <- %x\n" (big_int_to_hex byte_addr) byte;*)
       mips_mem := Mem.add byte_addr byte !mips_mem;
@@ -42,7 +42,7 @@ let _MEMr (addr, size) = begin
     let byte_addr = add_int_big_int i a in
     let byte = Mem.find byte_addr !mips_mem in
     let byte_vec = to_vec_dec_int (8, byte) in
-    ret := vector_concat (!ret) byte_vec;
+    ret := vector_concat byte_vec (!ret);
     (*printf "MEM [%s] -> %x %s %s\n" (big_int_to_hex byte_addr) byte (string_of_value byte_vec) (string_of_value !ret);*)
   done;
   ret := set_start_to_length (!ret);
diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index b65f74d9..42e36a6e 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -47,7 +47,7 @@ open Mips_extras_ml;;
 (* The linksem ELF interface *)
 open Sail_interface ;;
 
-module Mips_model=Mips_notlb_embed;;
+module Mips_model=Mips_embed;;
 
 let interact_print = ref true
 let result_print = ref true
@@ -64,7 +64,23 @@ let rec foldli f acc ?(i=0) = function
   | x::xs -> foldli f (f i acc x) ~i:(i+1) xs;;
 
 let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;;
-let big_int_to_hex i = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i))
+let big_int_to_hex i = 
+  (* annoyingly Uint64.to_string_hex prefixes the string with 0x UNLESS it is zero... *) 
+  if i = zero_big_int then
+    "0"
+  else
+    let s = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i)) in
+    let len = String.length s in
+    String.sub s 2 (len - 2)
+
+let big_int_to_hex64 i = 
+  let hex = big_int_to_hex i in
+  let len = String.length hex in
+  if (len < 16) then
+    (String.make (16-len) '0') ^ hex
+  else
+    hex
+    
 let input_buf = (ref [] : int list ref);;
 
 let add_mem byte addr mem = begin
@@ -278,14 +294,14 @@ let initial_system_state_of_elf_file name =
 let max_cut_off = ref false
 let max_instr = ref 0
 let raw_file = ref ""
-let raw_at   = ref 0
+let raw_at   = ref ""
 let elf_file = ref ""
 
 let args = [
   ("--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_int raw_at, "address to load raw file in memory");
+  ("--at", Arg.Set_string raw_at, "address to load raw file in memory");
 ]
 
 let time_it action arg =
@@ -295,12 +311,19 @@ let time_it action arg =
   (finish_time -. start_time, ret)
 
 let rec debug_print_gprs start stop =
-  resultf "DEBUG MIPS REG %.2d %s\n" start (big_int_to_hex (unsigned_big(vector_access Mips_model._GPR (big_int_of_int start))));
+  resultf "DEBUG MIPS REG %.2d 0x%s\n" start (big_int_to_hex64 (unsigned_big(vector_access Mips_model._GPR (big_int_of_int start))));
   if start < stop
   then debug_print_gprs (start + 1) stop
   else ()
 
-let get_opcode pc_a = _MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)
+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))
+
+let get_pc () = begin
+    try
+      Some (unsigned_big(Mips_model._TranslatePC(Mips_model._PC)))
+    with Sail_exit -> None
+  end
+
 
 let rec fde_loop count =
   if !max_cut_off && count = !max_instr
@@ -311,8 +334,8 @@ let rec fde_loop count =
   else begin
     let pc_vaddr = unsigned_big(Mips_model._PC) in
     interactf "\n**** instruction %d from address %s ****\n"
-      count (big_int_to_hex pc_vaddr);
-    let m_paddr = Some pc_vaddr in (* XXX should be address translate *)
+      count (big_int_to_hex64 pc_vaddr);
+    let m_paddr = get_pc () in
     match m_paddr with
       | Some pc ->
           let inBranchDelay = Some(unsigned_int(Mips_model._inBranchDelay)) in
@@ -337,49 +360,20 @@ let rec fde_loop count =
           if (i == Mips_model.HCF)
           then 
             begin
+              resultf "DEBUG MIPS PC 0x%s\n" (big_int_to_hex pc_vaddr);
               debug_print_gprs 0 31;
               resultf "\nSUCCESS program terminated after %d instructions\n" count;
               count
             end 
           else
             begin
-              Mips_model._execute(i);
-
-                (*
-                (try
-                  let (pending, _, _)  = (Unix.select [(Unix.stdin)] [] [] 0.0) in
-                  (if (pending != []) then
-                    let char = (input_byte stdin) in (
-                    errorf "Input %x\n" char;
-                    input_buf := (!input_buf) @ [char]));
-                with
-                | _ -> ());
-
-                let uart_rvalid = option_int_of_reg "UART_RVALID" in
-                (match uart_rvalid with
-                | Some 0 ->
-                  (match !input_buf with
-                  | x :: xs -> (
-                      reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg;
-                      reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
-                      input_buf := xs;
-                    )
-                  | [] -> ())
-                | _-> ());
-
-                let uart_written = option_int_of_reg "UART_WRITTEN" in
-                (match uart_written with 
-                | Some 1 ->
-                  (let uart_data = option_int_of_reg "UART_WDATA" in
-                  match uart_data with
-                  | Some b -> (printf "%c" (Char.chr b); printf "%!")
-                  | None   -> (errorf "UART_WDATA was undef" ; exit 1))
-                | _      -> ());
-                reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;*)
-                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)
+              (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)
             end
       | None -> begin (* Exception during PC translation *)
           set_register Mips_model._inBranchDelay Mips_model._branchPending;
@@ -389,6 +383,39 @@ let rec fde_loop count =
         end
   end
 
+
+ (*
+ (try
+   let (pending, _, _)  = (Unix.select [(Unix.stdin)] [] [] 0.0) in
+   (if (pending != []) then
+     let char = (input_byte stdin) in (
+     errorf "Input %x\n" char;
+     input_buf := (!input_buf) @ [char]));
+ with
+ | _ -> ());
+
+ let uart_rvalid = option_int_of_reg "UART_RVALID" in
+ (match uart_rvalid with
+ | Some 0 ->
+   (match !input_buf with
+   | x :: xs -> (
+       reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg;
+       reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
+       input_buf := xs;
+     )
+   | [] -> ())
+ | _-> ());
+
+ let uart_written = option_int_of_reg "UART_WRITTEN" in
+ (match uart_written with 
+ | Some 1 ->
+   (let uart_data = option_int_of_reg "UART_WDATA" in
+   match uart_data with
+   | Some b -> (printf "%c" (Char.chr b); printf "%!")
+   | None   -> (errorf "UART_WDATA was undef" ; exit 1))
+ | _      -> ());
+ reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;*)
+
 let rec load_raw_file' mem addr chan =
   let byte = input_byte chan in
   (add_mem byte addr mem;
@@ -417,10 +444,10 @@ let run () =
         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_int !raw_at) (open_in_bin !raw_file);
+    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;
   printf "CP0Status: %s\n" (string_of_value Mips_model._CP0Status);
-  let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x40000000")) in
+  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