From 972d349919fc5ebe911604330ea3c80e70fdcfad Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 8 May 2018 18:48:18 +0100 Subject: Add tests for Isabelle->OCaml generation for CHERI and AArch64 --- mips/main.sail | 1 + mips/mips_extras.lem | 10 ++++++++++ 2 files changed, 11 insertions(+) (limited to 'mips') 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 ())))` -- cgit v1.2.3 From 680acef72a84b1d3810ffd88c06639bafd1d4b3a Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 9 May 2018 16:30:46 +0100 Subject: Add targets for counting lines in mips, cheri and riscv. Can use either sloccount or cloc. sloccount seems to be reliable but lacks a way to tell it that sail files can be treated like ocaml without renaming the files. cloc has a nicer interface is lower quality in other regards like broken ocaml support in versions shipped with Ubuntu (e.g. treats {...} as comment, no nested comments support). For sail2 syntax this is OK because we use the C parser instead which gives the same results as sloccount. --- mips/Makefile | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'mips') diff --git a/mips/Makefile b/mips/Makefile index 00703f62..6e3ef49e 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -28,5 +28,11 @@ 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 + +cloc: $(LOC_FILES) + cloc --by-file --force-lang C,sail $^ + clean: rm -rf mips Mips.thy mips.lem _sbuild -- cgit v1.2.3 From cd33f38664c620f1eec5d97bde5b837770e7abbc Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 9 May 2018 16:36:54 +0100 Subject: Use latex support for generating cheri documentation and remove sed based hack. Also some minor code cleanups and comments. --- mips/mips_prelude.sail | 9 ++++++++- mips/prelude.sail | 9 +++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) (limited to 'mips') 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 aa81175f..152996f1 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -87,8 +87,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) @@ -277,6 +283,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) -- cgit v1.2.3 From 710ae06814ca26797a9120f2ecd1d69e0074b32b Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 9 May 2018 17:49:12 +0100 Subject: remove redundant cloc targets. --- mips/Makefile | 3 --- 1 file changed, 3 deletions(-) (limited to 'mips') diff --git a/mips/Makefile b/mips/Makefile index 6e3ef49e..6d605d60 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -31,8 +31,5 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem LOC_FILES:=$(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) include ../etc/loc.mk -cloc: $(LOC_FILES) - cloc --by-file --force-lang C,sail $^ - clean: rm -rf mips Mips.thy mips.lem _sbuild -- cgit v1.2.3 From db3b6d21c18f4ac516c2554db6890274d2b8292c Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 10 May 2018 14:23:49 +0100 Subject: Remove buggy bit list comparison functions from Lem library Found bugs by running CHERI test suite on Isabelle-exported model: signed less-than for bit lists was missing negations for the two's complement, and unsigned less-than compared the reverse lists. Since all other backends implement this in Sail, it seems best to just remove this code. Also add support for infix operators to Lem backend, by z-encoding their identifiers like the other backends do. --- mips/prelude.sail | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'mips') diff --git a/mips/prelude.sail b/mips/prelude.sail index 152996f1..e0bcd8cf 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -242,10 +242,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) -- cgit v1.2.3