Fix cheri and mips following 1fe8f33fce5aaaaea82fc54b6d198ffc9d7e1eeb which requires syntax change for unit constructors of union types.

6 files changed, 44 insertions, 44 deletions

diff --git a/mips_new_tc/main.sail b/mips_new_tc/main.sail
index 005692ef..2df5c0f8 100644
--- a/mips_new_tc/main.sail
+++ b/mips_new_tc/main.sail
@@ -18,15 +18,15 @@ function fetch_and_execute () = {
       /*print_bits("hex: ", instr);*/
       let instr_ast = decode(instr);
       match instr_ast {
-        Some(HCF) => {
+        Some(HCF()) => {
                        print("simulation stopped due to halt instruction.");
                        return ();
                      },
         Some(ast) => execute(ast),
-        None      => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */
+        None()    => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */
       }
     } catch {
-      ISAException => print("EXCEPTION")
+      ISAException() => print("EXCEPTION")
       /* ISA-level exception occurrred either during TranslatePC or execute --
          just continue from nextPC, which should have been set to the appropriate
          exception vector (along with clearing branchPending etc.) . */
diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail
index 39f8c82b..e8f9a0f7 100644
--- a/mips_new_tc/mips_insts.sail
+++ b/mips_new_tc/mips_insts.sail
@@ -1014,21 +1014,21 @@ function clause execute (BCMPZ(rs, imm, cmp, link, likely)) =
 /* Co-opt syscall 0xfffff for use as thread start in pccmem  */
 union clause ast = SYSCALL_THREAD_START : unit
 function clause decode (0b000000 @ 0xfffff @ 0b001100) =
-  Some(SYSCALL_THREAD_START)
-function clause execute (SYSCALL_THREAD_START) = ()
+  Some(SYSCALL_THREAD_START())
+function clause execute (SYSCALL_THREAD_START()) = ()
 
 
 /* fake stop fetching instruction for ppcmem, execute doesn't do anything,
    decode never produces it */
 
 union clause ast = ImplementationDefinedStopFetching : unit
-function clause execute (ImplementationDefinedStopFetching) = ()
+function clause execute (ImplementationDefinedStopFetching()) = ()
 
 
 union clause ast = SYSCALL : unit
 function clause decode (0b000000 @ code : bits(20) @ 0b001100) =
-  Some(SYSCALL) /* code is ignored */
-function clause execute (SYSCALL) =
+  Some(SYSCALL()) /* code is ignored */
+function clause execute (SYSCALL()) =
   {
     (SignalException(Sys))
   }
@@ -1036,8 +1036,8 @@ function clause execute (SYSCALL) =
 /* BREAK is identical to SYSCALL exception for the exception raised */
 union clause ast = BREAK : unit
 function clause decode (0b000000 @ code : bits(20) @ 0b001101) =
-  Some(BREAK) /* code is ignored */
-function clause execute (BREAK) =
+  Some(BREAK()) /* code is ignored */
+function clause execute (BREAK()) =
   {
     (SignalException(Bp))
   }
@@ -1045,8 +1045,8 @@ function clause execute (BREAK) =
 /* Accept WAIT as a NOP */
 union clause ast = WAIT : unit
 function clause decode (0b010000 @ 0x80000 @ 0b100000) =
-  Some(WAIT) /* we only accept code == 0 */
-function clause execute (WAIT) = {
+  Some(WAIT()) /* we only accept code == 0 */
+function clause execute (WAIT()) = {
   nextPC = PC;
 }
 
@@ -1420,8 +1420,8 @@ function clause execute (PREF(base, op, imm)) =
 /* SYNC  - Memory barrier */
 union clause ast = SYNC : unit
 function clause decode (0b000000 @ 0b00000 @ 0b00000 @ 0b00000 @ stype : regno @ 0b001111) =
-  Some(SYNC) /* stype is currently ignored */
-function clause execute(SYNC) =
+  Some(SYNC()) /* stype is currently ignored */
+function clause execute(SYNC()) =
   MEM_sync()
 
 union clause ast = MFC0 : (regno, regno, bits(3), bool)
@@ -1502,12 +1502,12 @@ function clause execute (MFC0(rt, rd, sel, double)) = {
 /* simulator halt instruction "MTC0 rt, r23" (cheri specific behaviour) */
 union clause ast = HCF : unit
 function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b10111 @ 0b00000000000) =
-  Some(HCF)
+  Some(HCF())
 
 function clause decode (0b010000 @ 0b00100 @ rt : regno @ 0b11010 @ 0b00000000000) =
-  Some(HCF)
+  Some(HCF())
 
-function clause execute (HCF) =
+function clause execute (HCF()) =
   () /* halt instruction actually executed by interpreter framework */
 
 union clause ast = MTC0 : (regno, regno, bits(3), bool)
@@ -1607,22 +1607,22 @@ function TLBWriteEntry(idx) = {
 }
 
 union clause ast = TLBWI : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000010) = Some(TLBWI : ast)
-function clause execute (TLBWI) = {
+function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000010) = Some(TLBWI() : ast)
+function clause execute (TLBWI()) = {
   checkCP0Access();
   TLBWriteEntry(TLBIndex);
 }
 
 union clause ast = TLBWR : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000110) = Some(TLBWR : ast)
-function clause execute (TLBWR) = {
+function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000110) = Some(TLBWR() : ast)
+function clause execute (TLBWR()) = {
   checkCP0Access();
   TLBWriteEntry(TLBRandom);
 }
 
 union clause ast = TLBR : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000001) = Some(TLBR : ast)
-function clause execute (TLBR) = {
+function clause decode (0b010000 @ 0b10000000000000000000 @ 0b000001) = Some(TLBR() : ast)
+function clause execute (TLBR()) = {
   checkCP0Access();
   let i as atom(_) = unsigned(TLBIndex) in
   let entry = reg_deref(TLBEntries[i]) in {
@@ -1648,8 +1648,8 @@ function clause execute (TLBR) = {
 }
 
 union clause ast = TLBP : unit
-function clause decode (0b010000 @ 0b10000000000000000000 @ 0b001000) = Some(TLBP : ast)
-function clause execute ((TLBP)) = {
+function clause decode (0b010000 @ 0b10000000000000000000 @ 0b001000) = Some(TLBP() : ast)
+function clause execute (TLBP()) = {
   checkCP0Access();
   let result = tlbSearch(TLBEntryHi.bits()) in
   match result {
@@ -1657,7 +1657,7 @@ function clause execute ((TLBP)) = {
       TLBProbe = [bitzero];
       TLBIndex = idx;
     },
-    None  => {
+    None()  => {
       TLBProbe = [bitone];
       TLBIndex = 0b000000;
     }
@@ -1689,8 +1689,8 @@ function clause execute (RDHWR(rt, rd)) = {
 union clause ast = ERET : unit
 
 function clause decode (0b010000 @ 0b1 @ 0b0000000000000000000 @ 0b011000) =
-      Some(ERET)
-function clause execute (ERET) =
+      Some(ERET())
+function clause execute (ERET()) =
       {
         checkCP0Access();
         ERETHook();
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index d35017eb..b4f09548 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -428,7 +428,7 @@ function SignalExceptionMIPS (ex, kccBase) =
       nextPC = vectorBase + EXTS(vectorOffset) - kccBase;
       CP0Cause->ExcCode() = ExceptionCode(ex);
       CP0Status->EXL()    = 0b1;
-      throw (ISAException);
+      throw (ISAException());
   }
 
 /* Defined either in mips_wrappers (directly calling SignalExceptionMIPS) or in cheri_prelude_common (cheri things plus above) */
diff --git a/mips_new_tc/mips_ri.sail b/mips_new_tc/mips_ri.sail
index 5a221df7..edce0657 100644
--- a/mips_new_tc/mips_ri.sail
+++ b/mips_new_tc/mips_ri.sail
@@ -36,7 +36,7 @@
    exception (like real hardware) instead of die (convenient for ppcmem) */
 
 union clause ast = RI : unit
-function clause decode _ = Some(RI)
-function clause execute (RI) =
+function clause decode _ = Some(RI())
+function clause execute (RI()) =
       SignalException (ResI)
 
diff --git a/mips_new_tc/mips_tlb.sail b/mips_new_tc/mips_tlb.sail
index 4ac2cb90..741eb84c 100644
--- a/mips_new_tc/mips_tlb.sail
+++ b/mips_new_tc/mips_tlb.sail
@@ -55,7 +55,7 @@ function tlbSearch(VAddr) =
       if(tlbEntryMatch(r, vpn2, asid, reg_deref(TLBEntries[idx]))) then
 	return Some(to_bits(6, idx))
     };
-    None
+    None()
   }
 
 /** For given virtual address and accessType returns physical address and
@@ -95,7 +95,7 @@ function TLBTranslate2 (vAddr, accessType) = {
       else
         let res : bits(64) = EXTZ(pfn[23..(evenOddBit - 12)] @ vAddr[(evenOddBit - 1) .. 0]) in
         (res,  bits_to_bool(if (accessType == StoreData) then caps else capl)),
-    None  =>  SignalExceptionTLB(
+    None()  =>  SignalExceptionTLB(
       if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr)
   }
 }
@@ -116,22 +116,22 @@ function TLBTranslateC (vAddr, accessType) =
     let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
     let (requiredLevel, addr) : (AccessLevel, option(bits(64))) = match (vAddr[63..62]) {
       0b11  => match (compat32, vAddr[30..29]) { /* xkseg */
-	(true, 0b11)  => (Kernel, None : option(bits(64))),               /* kseg3 mapped 32-bit compat */
-	(true, 0b10)  => (Supervisor, None : option(bits(64))),           /* sseg  mapped 32-bit compat */
+	(true, 0b11)  => (Kernel, None() : option(bits(64))),               /* kseg3 mapped 32-bit compat */
+	(true, 0b10)  => (Supervisor, None() : option(bits(64))),           /* sseg  mapped 32-bit compat */
 	(true, 0b01)  => (Kernel, Some(0x00000000 @ 0b000 @ vAddr[28..0])), /* kseg1 unmapped uncached 32-bit compat */
 	(true, 0b00)  => (Kernel, Some(0x00000000 @ 0b000 @ vAddr[28..0])), /* kseg0 unmapped cached 32-bit compat */
-	(_, _)        => (Kernel, None : option(bits(64))) /* xkseg mapped */
+	(_, _)        => (Kernel, None() : option(bits(64))) /* xkseg mapped */
       },
       0b10  => (Kernel, Some(0b00000 @ vAddr[58..0])), /* xkphys bits 61-59 are cache mode (ignored) */
-      0b01  => (Supervisor, None : option(bits(64))),  /* xsseg - supervisor mapped */
-      0b00  => (User, None : option(bits(64)))         /* xuseg - user mapped */
+      0b01  => (Supervisor, None() : option(bits(64))),  /* xsseg - supervisor mapped */
+      0b00  => (User, None() : option(bits(64)))         /* xuseg - user mapped */
     } in
     if (cast_AccessLevel(currentAccessLevel) < cast_AccessLevel(requiredLevel)) then
       SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)
     else
       let (pa, c) : (bits(64), bool) = match addr {
         Some(a) => (a, false),
-        None    => if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
+        None()  => if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
             SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr)
           else
             TLBTranslate2(vAddr, accessType)
diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail
index ca13753c..5b89521f 100644
--- a/mips_new_tc/prelude.sail
+++ b/mips_new_tc/prelude.sail
@@ -1,7 +1,7 @@
 default Order dec
 
 type bits ('n : Int) = vector('n, dec, bit)
-union option ('a : Type) = {None, Some : 'a}
+union option ('a : Type) = {None : unit, Some : 'a}
 
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
 
@@ -304,11 +304,11 @@ val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
 val print_string = "print_string" : (string, string) -> unit
 
 union exception = {
-  ISAException,
+  ISAException : unit,
   Error_not_implemented : string,
-  Error_misaligned_access,
-  Error_EBREAK,
-  Error_internal_error
+  Error_misaligned_access : unit,
+  Error_EBREAK : unit,
+  Error_internal_error : unit
 }
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)