summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Norton2017-04-05 17:31:44 +0100
committerRobert Norton2017-04-06 12:35:10 +0100
commit83ba712a9897c1b375c1ae4cfb744f718b91c482 (patch)
tree42d7a4230f533bbdc700d6a686636ccd0032d5a2
parentb50cf34a6e700b70b12f9c4bfe81a6c0b703198b (diff)
Model now assumes memory is little endian so adjust extras file accordingly.
-rw-r--r--mips/mips_extras_ml.ml4
-rw-r--r--mips/run_embed.ml2
2 files changed, 3 insertions, 3 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 d4b46747..76b1b222 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -316,7 +316,7 @@ let rec debug_print_gprs 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 rec fde_loop count =
if !max_cut_off && count = !max_instr