diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/Makefile | 3 | ||||
| -rw-r--r-- | mips/main.sail | 1 | ||||
| -rw-r--r-- | mips/mips_extras.lem | 10 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 9 | ||||
| -rw-r--r-- | mips/prelude.sail | 17 |
5 files changed, 35 insertions, 5 deletions
diff --git a/mips/Makefile b/mips/Makefile index a6a5bbdf..c0670380 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -28,5 +28,8 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ sed -i 's/datatype ast/datatype (plugins only: size) ast/' M$*_types.thy +LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) +include ../etc/loc.mk + clean: rm -rf mips Mips.thy mips.lem _sbuild diff --git a/mips/main.sail b/mips/main.sail index 2c4ee064..8ec91ba6 100644 --- a/mips/main.sail +++ b/mips/main.sail @@ -38,6 +38,7 @@ function fetch_and_execute () = { val elf_entry = { ocaml: "Elf_loader.elf_entry", + lem: "elf_entry", c: "elf_entry" } : unit -> int diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index 28fa07fb..f0f6a0c5 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -111,3 +111,13 @@ let undefined_atom i = return i let undefined_nat () = return (0:ii) let skip () = return () + +val elf_entry : unit -> integer +let elf_entry () = 0 +declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` + +let print_bits msg bs = prerr_endline (msg ^ (string_of_bits bs)) + +val get_time_ns : unit -> integer +let get_time_ns () = 0 +declare ocaml target_rep function get_time_ns = `(fun () -> Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())))` diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 9e81a5d0..f9049b5d 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -469,11 +469,18 @@ function int_of_AccessLevel level = Kernel => 2 } +/*! +Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level. + */ val grantsAccess : (AccessLevel, AccessLevel) -> bool function grantsAccess (currentLevel, requiredLevel) = int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel) -function getAccessLevel() : unit -> AccessLevel= +/*! +Returns the current effective access level determined by accessing the relevant parts of the MIPS status register. + */ +val getAccessLevel : unit -> AccessLevel effect {rreg} +function getAccessLevel() = if ((CP0Status.EXL()) | (CP0Status.ERL())) then Kernel else match CP0Status.KSU() diff --git a/mips/prelude.sail b/mips/prelude.sail index 281ef5ea..5bb79f97 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -90,8 +90,14 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys) overload operator | = {or_bool, or_vec} +/*! +The \function{unsigned} function converts a bit vector to an integer assuming an unsigned representation: +*/ val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +/*! +The \function{signed} function converts a bit vector to an integer assuming a signed twos-complement representation: +*/ val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) val "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) @@ -245,10 +251,10 @@ infix 4 >=_s infix 4 <_u infix 4 >=_u -val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator <_s : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool function operator <_s (x, y) = signed(x) < signed(y) function operator >=_s (x, y) = signed(x) >= signed(y) @@ -286,6 +292,9 @@ val operator *_s = "mults_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n infix 7 *_u val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n) +/*! +\function{to\_bits} converts an integer to a bit vector of given length. If the integer is negative a twos-complement representation is used. If the integer is too large (or too negative) to fit in the requested length then it is truncated to the least significant bits. +*/ val to_bits : forall 'l.(atom('l), int) -> bits('l) function to_bits (l, n) = get_slice_int(l, n, 0) |