summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--riscv/riscv.sail21
-rw-r--r--riscv/riscv_sys.sail263
-rw-r--r--riscv/riscv_types.sail38
-rw-r--r--src/gen_lib/sail_operators_bitlists.lem6
-rw-r--r--src/gen_lib/sail_operators_mwords.lem6
-rw-r--r--src/gen_lib/sail_values.lem4
-rw-r--r--src/monomorphise.ml4
-rw-r--r--test/mono/builtins.sail49
-rw-r--r--test/mono/pass/builtins (renamed from test/mono/not-yet/builtins)0
-rw-r--r--test/mono/test.ml4
10 files changed, 244 insertions, 151 deletions
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index c8b3956a..c18c1f44 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -383,6 +383,14 @@ function clause execute MRET() =
nextPC = handle_exception_ctl(cur_privilege, CTL_MRET(), PC)
/* ****************************************************************** */
+union clause ast = SRET : unit
+
+function clause decode 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET())
+
+function clause execute SRET() =
+ nextPC = handle_exception_ctl(cur_privilege, CTL_SRET(), PC)
+
+/* ****************************************************************** */
union clause ast = EBREAK : unit
function clause decode 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(EBREAK())
@@ -525,13 +533,13 @@ function readCSR csr: bits(12) -> xlenbits =
0x100 => mstatus.bits(), /* FIXME: legalize view*/
0x102 => sedeleg.bits(),
0x103 => sideleg.bits(),
- 0x104 => mie.bits(), /* FIXME: legalize view */
+ 0x104 => lower_mie(mie, mideleg).bits(),
0x105 => stvec.bits(),
0x140 => sscratch,
0x141 => sepc,
0x142 => scause.bits(),
0x143 => stval,
- 0x144 => mip.bits(), /* FIXME: legalize view */
+ 0x144 => lower_mip(mip, mideleg).bits(),
0x180 => satp,
/* others */
@@ -558,18 +566,17 @@ function writeCSR (csr : bits(12), value : xlenbits) -> unit =
0x344 => mip = legalize_mip(mip, value),
/* supervisor mode */
- /* FIXME: need legalizers for interrupt regs and satp */
0x100 => mstatus = legalize_sstatus(mstatus, value),
0x102 => sedeleg = legalize_sedeleg(sedeleg, value),
- 0x103 => sideleg->bits() = value,
- 0x104 => sie->bits() = value,
+ 0x103 => sideleg->bits() = value, /* TODO: does this need legalization? */
+ 0x104 => mie = legalize_sie(mie, mideleg, value),
0x105 => stvec = legalize_tvec(stvec, value),
0x140 => sscratch = value,
0x141 => sepc = legalize_xepc(value),
0x142 => scause->bits() = value,
0x143 => stval = value,
- 0x144 => mip->bits() = value,
- 0x180 => satp = value,
+ 0x144 => mip = legalize_sip(mip, mideleg, value),
+ 0x180 => satp = legalize_satp(cur_Architecture(), satp, value),
_ => print_bits("unhandled write to CSR ", csr)
}
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 39d611cf..cee3ede4 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -124,7 +124,6 @@ bitfield Minterrupts : bits(64) = {
MSI : 3, /* software interrupts */
SSI : 1,
USI : 0,
-
}
register mip : Minterrupts /* Pending */
register mie : Minterrupts /* Enabled */
@@ -311,22 +310,89 @@ function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = {
}
/* TODO: handle views for interrupt delegation */
-register sideleg : Minterrupts
-register sip : Minterrupts
-register sie : Minterrupts
+bitfield Sinterrupts : bits(64) = {
+ SEI : 9, /* external interrupts */
+ UEI : 8,
+
+ STI : 5, /* timers interrupts */
+ UTI : 4,
+
+ SSI : 1, /* software interrupts */
+ USI : 0
+}
-bitfield satp64 : bits(64) = {
+/* Provides the sip read view of mip as delegated by mideleg. */
+function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
+ let s : Sinterrupts = Mk_Sinterrupts(EXTZ(0b0));
+ /* M-mode interrupts delegated to S-mode should appear as S-mode interrupts */
+ let s = update_SEI(s, (m.SEI() & d.SEI()) | (m.MEI() & d.MEI()));
+ let s = update_STI(s, (m.STI() & d.STI()) | (m.MTI() & d.MTI()));
+ let s = update_SSI(s, (m.SSI() & d.SSI()) | (m.MSI() & d.MSI()));
+
+ let s = update_UEI(s, m.UEI() & d.UEI());
+ let s = update_UTI(s, m.UTI() & d.UTI());
+ let s = update_USI(s, m.USI() & d.USI());
+ s
+}
+/* Provides the sie read view of mie as delegated by mideleg. */
+function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
+ let s : Sinterrupts = Mk_Sinterrupts(EXTZ(0b0));
+ let s = update_SEI(s, m.SEI() & d.SEI());
+ let s = update_STI(s, m.STI() & d.STI());
+ let s = update_SSI(s, m.SSI() & d.SSI());
+ let s = update_UEI(s, m.UEI() & d.UEI());
+ let s = update_UTI(s, m.UTI() & d.UTI());
+ let s = update_USI(s, m.USI() & d.USI());
+ s
+}
+/* Provides the sip write view of mip as delegated by mideleg. */
+function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
+ let m : Minterrupts = o;
+ let m = update_SSI(m, s.SSI() & d.SSI());
+ let m = update_UEI(m, m.UEI() & d.UEI());
+ let m = update_USI(m, m.USI() & d.USI());
+ m
+}
+function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
+ lift_sip(m, d, Mk_Sinterrupts(v))
+}
+/* Provides the sie write view of mie as delegated by mideleg. */
+function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
+ let m : Minterrupts = o;
+ let m = if d.SEI() == true then update_SEI(m, s.SEI()) else m;
+ let m = if d.STI() == true then update_STI(m, s.STI()) else m;
+ let m = if d.SSI() == true then update_SSI(m, s.SSI()) else m;
+ let m = if d.UEI() == true then update_UEI(m, s.UEI()) else m;
+ let m = if d.UTI() == true then update_UTI(m, s.UTI()) else m;
+ let m = if d.USI() == true then update_USI(m, s.USI()) else m;
+ m
+}
+function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterrupts = {
+ lift_sie(m, d, Mk_Sinterrupts(v))
+}
+
+register sideleg : Sinterrupts
+
+bitfield Satp64 : bits(64) = {
Mode : 63 .. 60,
Asid : 59 .. 44,
PPN : 43 .. 0
}
+register satp : xlenbits
+
+function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = {
+ let s = Mk_Satp64(v);
+ match satpMode_of_bits(a, s.Mode()) {
+ None() => o,
+ Some(_) => s.bits()
+ }
+}
register stvec : Mtvec
register sscratch : xlenbits
register sepc : xlenbits
register scause : Mcause
register stval : xlenbits
-register satp : xlenbits
/* csr access control */
@@ -389,6 +455,22 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
& check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
& check_TVM_SATP(csr, p)
+/* exception delegation: given an exception and the privilege at which
+ * it occured, returns the privilege at which it should be handled.
+ */
+function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
+ let idx = exceptionType_to_nat(e);
+ let super = medeleg.bits()[idx];
+ let user = sedeleg.bits()[idx];
+ let deleg = /* if misa.N() == true & user then User
+ else */
+ if misa.S() == true & super then Supervisor
+ else Machine;
+ /* Ensure there is no transition to a less-privileged mode. */
+ if privLevel_to_bits(deleg) <_u privLevel_to_bits(p)
+ then p else deleg
+}
+
/* instruction control flow */
struct sync_exception = {
@@ -396,125 +478,94 @@ struct sync_exception = {
excinfo : option(xlenbits)
}
+function tval(excinfo : option(xlenbits)) -> xlenbits = {
+ match (excinfo) {
+ Some(e) => e,
+ None() => EXTZ(0b0)
+ }
+}
+
union ctl_result = {
CTL_TRAP : sync_exception,
-/* TODO:
- CTL_URET,
- CTL_SRET,
-*/
+/* TODO: CTL_URET */
+ CTL_SRET : unit,
CTL_MRET : unit
}
/* handle exceptional ctl flow by updating nextPC */
+function handle_trap(curp : Privilege, e : sync_exception,
+ pc : xlenbits) -> xlenbits = {
+ let priv = exception_delegatee(e.trap, curp);
+ cur_privilege = priv;
+ match (priv) {
+ Machine => {
+ mcause->IsInterrupt() = false;
+ mcause->Cause() = EXTZ(exceptionType_to_bits(e.trap));
+
+ mstatus->MPIE() = mstatus.MIE();
+ mstatus->MIE() = false;
+ mstatus->MPP() = privLevel_to_bits(curp);
+ mtval = tval(e.excinfo);
+ mepc = pc;
+
+ match tvec_addr(mtvec, mcause) {
+ Some(epc) => epc,
+ None() => internal_error("Invalid mtvec mode")
+ }
+ },
+ Supervisor => {
+ scause->IsInterrupt() = false;
+ scause->Cause() = EXTZ(exceptionType_to_bits(e.trap));
+
+ mstatus->SPIE() = mstatus.SIE();
+ mstatus->SIE() = false;
+ mstatus->SPP() = match (curp) {
+ User => false,
+ Supervisor => true,
+ Machine => internal_error("invalid privilege for s-mode trap")
+ };
+ stval = tval(e.excinfo);
+ sepc = pc;
+
+ match tvec_addr(stvec, scause) {
+ Some(epc) => epc,
+ None() => internal_error("Invalid stvec mode")
+ }
+
+ },
+ User => internal_error("the N extension is currently unsupported")
+ }
+}
+
function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
pc: xlenbits) -> xlenbits =
- /* TODO: check delegation */
match (cur_priv, ctl) {
- (_, CTL_TRAP(e)) => {
- mepc = pc;
-
- mcause->IsInterrupt() = false;
- mcause->Cause() = EXTZ(exceptionType_to_bits(e.trap));
-
- mstatus->MPIE() = mstatus.MIE();
- mstatus->MIE() = false;
- mstatus->MPP() = privLevel_to_bits(cur_priv);
- cur_privilege = Machine;
-
- match (e.trap) {
- E_Fetch_Addr_Align => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_Fetch_Access_Fault => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_Illegal_Instr => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
-
- E_Breakpoint => not_implemented("breakpoint"),
-
- E_Load_Addr_Align => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_Load_Access_Fault => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_SAMO_Addr_Align => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_SAMO_Access_Fault => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
-
- E_U_EnvCall => {
- mtval = EXTZ(0b0)
- },
- E_S_EnvCall => {
- mtval = EXTZ(0b0)
- },
- E_M_EnvCall => {
- mtval = EXTZ(0b0)
- },
-
- E_Fetch_Page_Fault => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_Load_Page_Fault => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- E_SAMO_Page_Fault => {
- match (e.excinfo) {
- Some(a) => mtval = a,
- None() => throw Error_internal_error()
- }
- },
- _ => throw Error_internal_error() /* Don't expect ReservedExc0 etc. here */
- };
- /* TODO: make register read explicit */
- match (tvec_addr(mtvec, mcause)) {
- Some(addr) => addr,
- None() => throw Error_internal_error()
- }
- },
- (_, CTL_MRET()) => {
+ (_, CTL_TRAP(e)) => handle_trap(cur_priv, e, pc),
+ (_, CTL_MRET()) => {
mstatus->MIE() = mstatus.MPIE();
mstatus->MPIE() = true;
cur_privilege = privLevel_of_bits(mstatus.MPP());
mstatus->MPP() = privLevel_to_bits(User);
mepc
+ },
+ (_, CTL_SRET()) => {
+ mstatus->SIE() = mstatus.SPIE();
+ mstatus->SPIE() = true;
+ cur_privilege = if mstatus.SPP() == true then Supervisor else User;
+ mstatus->SPP() = false;
+ sepc
}
}
function init_sys () : unit -> unit = {
cur_privilege = Machine;
+ misa->MXL() = arch_to_bits(RV64);
misa->C() = true;
+ misa->U() = true;
+ misa->S() = true;
+
+ mstatus->SXL() = misa.MXL();
+ mstatus->UXL() = misa.MXL();
+ mstatus->SD() = false;
}
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 1e41133d..78b0ea89 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -61,6 +61,13 @@ function architecture(a : arch_xlen) -> option(Architecture) = {
_ => None()
}
}
+function arch_to_bits(a : Architecture) -> arch_xlen = {
+ match (a) {
+ RV32 => 0b01,
+ RV64 => 0b10,
+ RV128 => 0b11
+ }
+}
/* privilege levels */
@@ -143,6 +150,28 @@ function exceptionType_to_bits(e) = {
}
}
+val cast exceptionType_to_nat : ExceptionType -> range(0, 15)
+function exceptionType_to_nat(e) = {
+ match (e) {
+ E_Fetch_Addr_Align => 0,
+ E_Fetch_Access_Fault => 1,
+ E_Illegal_Instr => 2,
+ E_Breakpoint => 3,
+ E_Load_Addr_Align => 4,
+ E_Load_Access_Fault => 5,
+ E_SAMO_Addr_Align => 6,
+ E_SAMO_Access_Fault => 7,
+ E_U_EnvCall => 8,
+ E_S_EnvCall => 9,
+ E_Reserved_10 => 10,
+ E_M_EnvCall => 11,
+ E_Fetch_Page_Fault => 12,
+ E_Load_Page_Fault => 13,
+ E_Reserved_14 => 14,
+ E_SAMO_Page_Fault => 15
+ }
+}
+
enum InterruptType = {
I_U_Software,
I_S_Software,
@@ -230,6 +259,15 @@ function extStatus_of_bits(e) = {
type satp_mode = bits(4)
enum SATPMode = {Sbare, Sv32, Sv39}
+function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = {
+ match (a, m) {
+ (_, 0x0) => Some(Sbare),
+ (RV32, 0x1) => Some(Sv32),
+ (RV64, 0x8) => Some(Sv39),
+ (_, _) => None()
+ }
+}
+
/* CSR access control bits (from CSR addresses) */
type csrRW = bits(2) /* read/write */
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index 3c1afe79..18c90c66 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -29,6 +29,12 @@ let extz_vec = extz_bv
val exts_vec : integer -> list bitU -> list bitU
let exts_vec = exts_bv
+val zero_extend : list bitU -> integer -> list bitU
+let zero_extend bits len = extz_bits len bits
+
+val vector_truncate : list bitU -> integer -> list bitU
+let vector_truncate bs len = extz_bv len bs
+
val vec_of_bits_maybe : list bitU -> maybe (list bitU)
val vec_of_bits_fail : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
val vec_of_bits_oracle : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 79b7674e..e3e1151a 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -70,6 +70,12 @@ let extz_vec _ w = Machine_word.zeroExtend w
val exts_vec : forall 'a 'b. Size 'a, Size 'b => integer -> mword 'a -> mword 'b
let exts_vec _ w = Machine_word.signExtend w
+val zero_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let zero_extend w _ = Machine_word.zeroExtend w
+
+val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
+let vector_truncate w _ = Machine_word.zeroExtend w
+
val concat_vec : forall 'a 'b 'c. Size 'a, Size 'b, Size 'c => mword 'a -> mword 'b -> mword 'c
let concat_vec = Machine_word.word_concat
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2fe69211..a89456b9 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -276,8 +276,6 @@ let ext_list pad len xs =
if longer < 0 then drop (nat_of_int (abs (longer))) xs
else pad_list pad xs longer
-let vector_truncate bs len = ext_list B0 len bs
-
let extz_bools len bs = ext_list false len bs
let exts_bools len bs =
match bs with
@@ -343,8 +341,6 @@ let exts_bits len bits =
| _ -> ext_list B0 len bits
end
-let zero_extend bits len = extz_bits len bits
-
let rec add_one_bit_ignore_overflow_aux bits = match bits with
| [] -> []
| B0 :: bits -> B1 :: bits
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 78ccee24..f417d292 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -779,14 +779,14 @@ let bits_of_lit = function
let slice_lit (L_aux (lit,ll)) i len (Ord_aux (ord,_)) =
let i = Big_int.to_int i in
let len = Big_int.to_int len in
+ let bin = bits_of_lit lit in
match match ord with
| Ord_inc -> Some i
- | Ord_dec -> Some (len - i)
+ | Ord_dec -> Some (String.length bin - i - len)
| Ord_var _ -> None
with
| None -> None
| Some i ->
- let bin = bits_of_lit lit in
Some (L_aux (L_bin (String.sub bin i len),Generated ll))
let concat_vec lit1 lit2 =
diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail
index e565ab58..7fb2b822 100644
--- a/test/mono/builtins.sail
+++ b/test/mono/builtins.sail
@@ -1,55 +1,42 @@
$include <smt.sail>
$include <flow.sail>
+$include <vector_dec.sail>
+
default Order dec
-type bits ('n : Int) = vector('n, dec, bit)
-val operator & = "and_bool" : (bool, bool) -> bool
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-overload operator == = {eq_int, eq_vec}
-val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-function neq_vec (x, y) = not_bool(eq_vec(x, y))
-overload operator != = {neq_atom, neq_vec}
-val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
- (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
-val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int
-overload operator * = {mult_range, mult_int, mult_real}
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extz(v) = extz_vec(sizeof('m),v)
-val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val exts : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function exts(v) = exts_vec(sizeof('m),v)
+val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+function neq_vec (x, y) = not_bool(x == y)
+overload operator != = {neq_vec}
val UInt = {
ocaml: "uint",
lem: "uint",
interpreter: "uint",
c: "sail_uint"
} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
-val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
- (bits('m), int, atom('n)) -> bits('n)
/* Test constant propagation's implementation of builtins
TODO: need some way to check that everything has propagated. */
-register r8 : bits(8)
-register r16 : bits(16)
+/* A function that constant propagation won't touch */
+val launder : forall 'n. bits('n) -> bits('n) effect {escape}
+function launder(x) = {
+ assert(true);
+ x
+}
-val test : bool -> unit effect {escape,rreg,wreg}
+val test : bool -> unit effect {escape}
function test(b) = {
let 'n : {'n, 'n in {8,16}. atom('n)} = if b then 8 else 16;
let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 };
- /* Constant propagation doesn't do registers, so uses of x' will be
- evaluated at runtime */
- let x' : bits('n) = match 'n { 8 => {r8 = x; r8}, 16 => {r16 = x; r16} };
+ let x' : bits('n) = launder(x);
let y : bits('n) = match 'n { 8 => 0x35, 16 => 0x5637 };
- assert(x != y);
- assert(slice(x, 0, 4) == slice(x',0,4));
- assert(0x3 == slice(y, 4, 4));
- assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }));
+ assert(x != y, "!= by propagation");
+ assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice");
+ assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice");
+ assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal");
}
-val run : unit -> unit effect {escape,rreg,wreg}
+val run : unit -> unit effect {escape}
function run() = {
test(true);
diff --git a/test/mono/not-yet/builtins b/test/mono/pass/builtins
index 3abb0198..3abb0198 100644
--- a/test/mono/not-yet/builtins
+++ b/test/mono/pass/builtins
diff --git a/test/mono/test.ml b/test/mono/test.ml
index 32d3b2ed..a54e3145 100644
--- a/test/mono/test.ml
+++ b/test/mono/test.ml
@@ -1,3 +1,5 @@
match Out.run() with
| Done _ -> exit 0
-| _ -> exit 1
+| Fail s -> prerr_endline ("Fail: " ^ s); exit 1
+| Error s -> prerr_endline ("Error: " ^ s); exit 1
+| _ -> prerr_endline "Unexpected outcome"; exit 1
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:17:13 +0000