diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/Makefile | 2 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 6 | ||||
| -rw-r--r-- | mips/prelude.sail | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/mips/Makefile b/mips/Makefile index a8bce143..593ea6d1 100644 --- a/mips/Makefile +++ b/mips/Makefile @@ -21,7 +21,7 @@ mips.c: $(MIPS_PRE) $(MIPS_TLB) $(MIPS_SAILS) $(MIPS_MAIN) Makefile ../sail C_WARNINGS=-Wall -Wno-unused-but-set-variable -Wno-unused-label -Wno-maybe-uninitialized -Wno-return-type C_OPT=-O2 GCOV_FLAGS= -mips_c: mips.c ../lib/sail.h ../lib/*.c Makefile +mips_c: mips.c ../lib/sail.h ../lib/*.c Makefile gcc $(C_OPT) $(C_WARNINGS) $(GCOV_FLAGS) -g -I ../lib $< ../lib/*.c -lgmp -lz -o $@ # Note that for coverage purposes O1 appears optimal. O0 means lots of obviously dead code but O2 risks reducing granularity too much. diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index fbbe74ee..c9bebabb 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -466,7 +466,7 @@ function SignalExceptionTLB(ex, badAddr) = { enum MemAccessType = {Instruction, LoadData, StoreData} enum AccessLevel = {User, Supervisor, Kernel} -val int_of_AccessLevel : AccessLevel -> int effect pure +val int_of_AccessLevel : AccessLevel -> {|0, 1, 2|} effect pure function int_of_AccessLevel level = match level { User => 0, @@ -619,8 +619,8 @@ function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * reverse_endianness'(sizeof 'W, value) }*/ -val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem, rreg, wreg} -function MEMr_wrapper (addr, size) = +val MEMr_wrapper : forall 'n, 1 <= 'n <= 8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem, rreg, wreg} +function MEMr_wrapper (addr, size) = if (addr == 0x000000007f000000) then { let rvalid = UART_RVALID in diff --git a/mips/prelude.sail b/mips/prelude.sail index c411ad83..407482d6 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -53,7 +53,7 @@ val "prerr_endline" : string -> unit val "prerr_string" : string -> unit -val putchar = {c:"sail_putchar", _:"putchar"} : forall ('a : Type). 'a -> unit +val putchar = {c:"sail_putchar", _:"putchar"} : int -> unit val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string |