summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mips/mips_extras_ml.ml4
-rw-r--r--mips/run_embed.ml121
-rw-r--r--src/Makefile10
-rw-r--r--src/gen_lib/sail_values.ml42
-rw-r--r--src/pretty_print_ocaml.ml11
5 files changed, 125 insertions, 63 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
diff --git a/src/Makefile b/src/Makefile
index acdd0075..e98b896b 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -133,6 +133,12 @@ _build/mips_notlb_embed.ml: $(MIPS_NOTLB_SAILS_PRE) ./sail.native
cd _build ; \
../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_notlb_embed $(MIPS_NOTLB_SAILS_PRE)
+_build/mips_embed.ml: $(MIPS_SAILS_PRE) ./sail.native
+ mkdir -p _build
+ cd _build ; \
+ ../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_embed $(MIPS_SAILS_PRE)
+
+
_build/cheri.lem: $(CHERI_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
@@ -175,8 +181,8 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail
run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native
-run_mips_embed.native: _build/mips_notlb_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml
- env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_notlb_embed.ml _build/run_embed.ml -o run_mips_embed.native
+run_mips_embed.native: _build/mips_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml
+ env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_embed.ml _build/run_embed.ml -o run_mips_embed.native
run_mips_embed.bytes: _build/mips_notlb_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml
env OCAMLRUNPARAM=l=100M ocamlfind ocamlc -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cma $(LEMLIBOCAML)/extract.cma $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cma $(ELFDIR)/src/linksem.cma _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_notlb_embed.ml _build/run_embed.ml -o run_mips_embed.bytes
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index d287b2cd..ebde00a7 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -1,4 +1,5 @@
open Big_int_Z
+open Printf
(* only expected to be 0, 1, 2; 2 represents undef *)
type vbit = Vone | Vzero | Vundef
@@ -13,6 +14,8 @@ type value =
| Vregister of vbit array ref * int * bool * (string * (int * int)) list
| Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*)
+exception Sail_exit
+
let string_of_bit = function
| Vone -> "1"
| Vzero -> "0"
@@ -23,7 +26,7 @@ let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a)
let string_of_value = function
| Vvector(bits, start, inc) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array bits)
| VvectorR(values, start, inc) -> ""
- | Vregister(bits, start, inc, fields) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits)
+ | Vregister(bits, start, inc, fields) -> "reg" ^ (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits)
| Vbit(b) -> string_of_bit b
let to_bool = function
@@ -37,7 +40,7 @@ let is_one i =
else Vzero
-let exit _ = failwith "called exit"
+let exit _ = raise Sail_exit
let is_one_int i =
@@ -157,7 +160,7 @@ let set_register register value = match register,value with
a := !new_v
| Vregister(a,_,_,_), Vvector(new_v,_,_) ->
a := new_v
- | _ -> ()
+ | _ -> failwith "set_register of non-register"
let set_vector_subrange_vec_int v n m new_v =
let walker array length offset new_values =
@@ -532,11 +535,34 @@ let to_vec_dec_undef_big len = to_vec_undef_big false len
let to_vec_inc_undef = to_vec_inc_undef_big
let to_vec_dec_undef = to_vec_dec_undef_big
-let exts_int (len, vec) = to_vec_int (get_ord vec) len (signed_int vec)
-let extz_int (len, vec) = to_vec_int (get_ord vec) len (unsigned_int vec)
+let exts_int (len, vec) =
+ let barray = get_barray(vec) in
+ let vlen = Array.length barray in
+ let arr =
+ if (vlen < len) then
+ (* copy most significant bit into new bits *)
+ Array.append (Array.make (len - vlen) barray.(0)) barray
+ else
+ (* truncate to least significant bits *)
+ Array.sub barray (vlen - len) len in
+ let inc = get_ord vec in
+ Vvector(arr, (if inc then 0 else (len - 1)), inc)
+
+let extz_int (len, vec) =
+ let barray = get_barray(vec) in
+ let vlen = Array.length barray in
+ let arr =
+ if (vlen < len) then
+ (* fill new bits with zero *)
+ Array.append (Array.make (len - vlen) Vzero) barray
+ else
+ (* truncate to least significant bits *)
+ Array.sub barray (vlen - len) len in
+ let inc = get_ord vec in
+ Vvector(arr, (if inc then 0 else (len - 1)), inc)
-let exts_big (len,vec) = to_vec_big (get_ord vec) len (signed_big vec)
-let extz_big (len,vec) = to_vec_big (get_ord vec) len (unsigned_big vec)
+let exts_big (len,vec) = exts_int (int_of_big_int len, vec)
+let extz_big (len,vec) = extz_int (int_of_big_int len, vec)
let exts = exts_big
let extz = extz_big
@@ -1121,7 +1147,7 @@ let gt_range_vec = gt_range_vec_big
let lteq_range_vec = lteq_range_vec_big
let gteq_range_vec = gteq_range_vec_big
-let eq (l,r) = if l == r then Vone else Vzero
+let eq (l,r) = if l = r then Vone else Vzero
let eq_vec_vec (l,r) = eq (to_num_big true l, to_num_big true r)
let eq_vec (l,r) = eq_vec_vec(l,r)
let eq_vec_range (l,r) = eq (to_num_big false l,r)
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 47aacf0c..5df8691e 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -479,10 +479,13 @@ let doc_exp_ocaml, doc_let_ocaml =
| _ -> (false,false) in
match lexp with
| LEXP_vector(v,e) ->
- doc_op (string "<-")
- (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^
- dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e)))
- (exp e_new_v)
+ if is_bit then
+ doc_op (string "<-") (group (parens (string "get_barray" ^^ space ^^ doc_lexp_ocaml false v)) ^^
+ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) (exp e_new_v)
+ else (* XXX Check whether vector of reg? *)
+ parens ((string "set_register") ^^ space ^^
+ ((group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v)) ^^
+ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) ^^ space ^^ (exp e_new_v)))
| LEXP_vector_range(v,e1,e2) ->
parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^
doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 04:48:34 +0000