summaryrefslogtreecommitdiff
path: root/mips/mips_extras_ml.ml
blob: 2a624523e490c32367f4361f448ed3c735770ce6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
open Sail_values
open Big_int_Z
open Printf

let big_int_to_hex i = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i))

module Mem = struct
  include Map.Make(struct
      type t = big_int
      let compare = compare_big_int
    end)
end

let mips_mem = (ref Mem.empty : (int Mem.t) ref);;

let _MEMea (addr, size) = ()
let _MEMea_conditional = _MEMea

let _MEMval (addr, size, data) =
  (* assumes data is decreasing vector to be stored in big-endian byte order in mem *)
  let s = int_of_big_int size in
  let a = unsigned_big(addr) in
  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 (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;
    end
  done
  
let _MEMval_conditional (addr, size, data) =
    let _ = _MEMval (addr, size, data) in
    Vone

let _MEMr (addr, size) = begin
  let s = int_of_big_int size in
  let a = unsigned_big(addr) in
  let ret = ref (to_vec_dec_int (0, 0)) in
  for i = 0 to (s - 1) do
    let byte_addr = add_int_big_int i a in
    let byte_vec = 
      try
        let byte = Mem.find byte_addr !mips_mem in
        to_vec_dec_int (8, byte)
      with Not_found -> 
        to_vec_dec_undef_int 8 in
    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);
  !ret;
end
let _MEMr_reserve = _MEMr

let _MEM_sync _ = ()