Use not() instead of ~() for boolean negation (riscv#210)

This may be more readable and also matches the sail-cheri-riscv model.
For now this keeps ~ overloaded to accept bool, but in the future we may
want to consider removing it (which is what I did to find all uses
modified in this patch)

model/prelude.sail

@@ -108,6 +108,8 @@ function not_bit(b) = if b == bitone then bitzero else bitone
 
 overload ~ = {not_bool, not_vec, not_bit}
 
+val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
+
 val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_vec (x, y) = not_bool(eq_bits(x, y))

model/riscv_analysis.sail

@@ -133,7 +133,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                    _      => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0
                };
                iR = RFull(csr_name(csr)) :: iR;
-               if ~(is_imm) then {
+               if not(is_imm) then {
                   iR = RFull(GPRstr(rs1)) :: iR;
                };
                if isWrite then {
@@ -306,7 +306,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
                    _      => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0
                };
                iR = RFull(csr_name(csr)) :: iR;
-               if ~(is_imm) then {
+               if not(is_imm) then {
                   iR = RFull(GPRstr(rs1)) :: iR;
                };
                if isWrite then {

model/riscv_fetch.sail

@@ -70,7 +70,7 @@
  * to check PC validity *before* standard fetch processing checks.
  */
 
-function isRVC(h : half) -> bool = ~ (h[1 .. 0] == 0b11)
+function isRVC(h : half) -> bool = not(h[1 .. 0] == 0b11)
 
 val fetch : unit -> FetchResult effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
 function fetch() -> FetchResult =
@@ -80,7 +80,7 @@ function fetch() -> FetchResult =
   match ext_fetch_check_pc(PC, PC) {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC()))))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _)     => F_Error(e, PC),

model/riscv_fetch_rvfi.sail

@@ -77,7 +77,7 @@ function fetch() -> FetchResult = {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
       /* then check PC alignment */
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC()))))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _) => F_Error(e, PC),

model/riscv_insts_aext.sail

@@ -141,7 +141,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
         /* "LR faults like a normal load, even though it's in the AMO major opcode space."
          * - Andrew Waterman, isa-dev, 10 Jul 2018.
          */
-        if (~ (aligned))
+        if not(aligned)
         then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
         else match translateAddr(vaddr, Read(Data)) {
                TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
@@ -199,7 +199,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
               WORD   => vaddr[1..0] == 0b00,
               DOUBLE => vaddr[2..0] == 0b000
             };
-          if (~ (aligned))
+          if not(aligned)
           then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
           else {
             if match_reservation(vaddr) == false then {

model/riscv_insts_base.sail

@@ -127,7 +127,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
     },
     Ext_ControlAddr_OK(target) => {
       /* Perform standard alignment check */
-      if bit_to_bool(target[1]) & (~ (haveRVC()))
+      if bit_to_bool(target[1]) & not(haveRVC())
       then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
@@ -191,7 +191,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
         RETIRE_FAIL
       },
       Ext_ControlAddr_OK(target) => {
-        if bit_to_bool(target[1]) & (~ (haveRVC())) then {
+        if bit_to_bool(target[1]) & not(haveRVC()) then {
           handle_mem_exception(target, E_Fetch_Addr_Align());
           RETIRE_FAIL;
         } else {
@@ -357,8 +357,8 @@ union clause ast = LOAD : (bits(12), regidx, regidx, bool, word_width, bool, boo
 
 /* unsigned loads are only present for widths strictly less than xlen,
    signed loads also present for widths equal to xlen */
-mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
-  <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not_bool(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
+mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
+  <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if (word_width_bytes(size) < sizeof(xlen_bytes)) | (not(is_unsigned) & word_width_bytes(size) <= sizeof(xlen_bytes))
 
 val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
 function extend_value(is_unsigned, value) = match (value) {
@@ -789,7 +789,7 @@ mapping clause encdec = MRET()
 function clause execute MRET() = {
   if   cur_privilege != Machine
   then { handle_illegal(); RETIRE_FAIL }
-  else if ~(ext_check_xret_priv (Machine))
+  else if not(ext_check_xret_priv (Machine))
   then { ext_fail_xret_priv(); RETIRE_FAIL }
   else {
     set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC));
@@ -808,12 +808,12 @@ mapping clause encdec = SRET()
 function clause execute SRET() = {
   let sret_illegal : bool = match cur_privilege {
     User       => true,
-    Supervisor => ~ (haveSupMode ()) | mstatus.TSR() == 0b1,
-    Machine    => ~ (haveSupMode ())
+    Supervisor => not(haveSupMode ()) | mstatus.TSR() == 0b1,
+    Machine    => not(haveSupMode ())
   };
   if   sret_illegal
   then { handle_illegal(); RETIRE_FAIL }
-  else if ~(ext_check_xret_priv (Supervisor))
+  else if not(ext_check_xret_priv (Supervisor))
   then { ext_fail_xret_priv(); RETIRE_FAIL }
   else {
     set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));

model/riscv_insts_next.sail

@@ -75,10 +75,10 @@ mapping clause encdec = URET()
   <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute URET() = {
-  if   (~ (haveUsrMode()) | ~(sys_enable_next()))
+  if   not(haveUsrMode()) | not(sys_enable_next())
   then handle_illegal()
-  else if ~ (ext_check_xret_priv (User))
-  then ext_fail_xret_priv ()
+  else if not(ext_check_xret_priv(User))
+  then ext_fail_xret_priv()
   else set_next_pc(exception_handler(cur_privilege, CTL_URET(), PC));
   RETIRE_FAIL
 }

model/riscv_insts_zbb.sail

@@ -253,7 +253,7 @@ function clause execute (RISCV_CLZ(rs1, rd)) = {
   result : nat = 0;
   done : bool = false;
   foreach (i from (sizeof(xlen) - 1) downto 0)
-    if ~(done) then if rs1_val[i] == bitzero
+    if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
                     else done = true;
   X(rd) = to_bits(sizeof(xlen), result);
@@ -274,7 +274,7 @@ function clause execute (RISCV_CLZW(rs1, rd)) = {
   result : nat = 0;
   done : bool = false;
   foreach (i from 31 downto 0)
-    if ~(done) then if rs1_val[i] == bitzero
+    if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
                     else done = true;
   X(rd) = to_bits(sizeof(xlen), result);
@@ -295,7 +295,7 @@ function clause execute (RISCV_CTZ(rs1, rd)) = {
   result : nat = 0;
   done : bool = false;
   foreach (i from 0 to (sizeof(xlen) - 1))
-    if ~(done) then if rs1_val[i] == bitzero
+    if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
                     else done = true;
   X(rd) = to_bits(sizeof(xlen), result);
@@ -316,7 +316,7 @@ function clause execute (RISCV_CTZW(rs1, rd)) = {
   result : nat = 0;
   done : bool = false;
   foreach (i from 0 to 31)
-    if ~(done) then if rs1_val[i] == bitzero
+    if not(done) then if rs1_val[i] == bitzero
                     then result = result + 1
                     else done = true;
   X(rd) = to_bits(sizeof(xlen), result);

model/riscv_insts_zicsr.sail

@@ -256,9 +256,9 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = {
     CSRRW  => true,
     _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
   };
-  if ~ (check_CSR(csr, cur_privilege, isWrite))
+  if not(check_CSR(csr, cur_privilege, isWrite))
   then { handle_illegal(); RETIRE_FAIL }
-  else if ~ (ext_check_CSR(csr, cur_privilege, isWrite))
+  else if not(ext_check_CSR(csr, cur_privilege, isWrite))
   then { ext_check_CSR_fail(); RETIRE_FAIL }
   else {
     let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */

model/riscv_jalr_seq.sail

@@ -84,7 +84,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
     },
     Ext_ControlAddr_OK(addr) => {
       let target = [addr with 0 = bitzero];  /* clear addr[0] */
-      if bit_to_bool(target[1]) & ~(haveRVC()) then {
+      if bit_to_bool(target[1]) & not(haveRVC()) then {
         handle_mem_exception(target, E_Fetch_Addr_Align());
         RETIRE_FAIL
       } else {

model/riscv_mem.sail

@@ -142,7 +142,7 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(
 
 /* PMP checks if enabled */
 function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), p : Privilege, paddr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool, meta : bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) =
-  if   (~ (plat_enable_pmp ()))
+  if   not(plat_enable_pmp())
   then checked_mem_read(t, paddr, width, aq, rl, res, meta)
   else {
     match pmpCheck(paddr, width, t, p) {
@@ -188,7 +188,7 @@ $endif
 /* The most generic memory read operation */
 function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = {
   let result : MemoryOpResult((bits(8 * 'n), mem_meta)) =
-    if (aq | res) & (~ (is_aligned_addr(paddr, width)))
+    if (aq | res) & not(is_aligned_addr(paddr, width))
     then MemException(E_Load_Addr_Align())
     else match (aq, rl, res) {
       (false, true,  false) => throw(Error_not_implemented("load.rl")),
@@ -213,7 +213,7 @@ function mem_read (typ, paddr, width, aq, rel, res) =
 val mem_write_ea : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
 
 function mem_write_ea (addr, width, aq, rl, con) = {
-  if (rl | con) & (~ (is_aligned_addr(addr, width)))
+  if (rl | con) & not(is_aligned_addr(addr, width))
   then MemException(E_SAMO_Addr_Align())
   else match (aq, rl, con) {
     (false, false, false) => MemValue(write_ram_ea(Write_plain, addr, width)),
@@ -267,7 +267,7 @@ function checked_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kin
 
 /* PMP checks if enabled */
 function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, paddr : xlenbits, width : atom('n), data: bits(8 * 'n), typ: AccessType(ext_access_type), priv: Privilege, meta: mem_meta) -> MemoryOpResult(bool) =
-  if   (~ (plat_enable_pmp ()))
+  if   not(plat_enable_pmp())
   then checked_mem_write(wk, paddr, width, data, meta)
   else {
     match pmpCheck(paddr, width, typ, priv) {
@@ -286,7 +286,7 @@ function pmp_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk: write_kind, pa
 val mem_write_value_priv_meta : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), AccessType(ext_access_type), Privilege, mem_meta, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape}
 function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl, con) = {
   rvfi_write(paddr, width, value, meta);
-  if (rl | con) & (~ (is_aligned_addr(paddr, width)))
+  if (rl | con) & not(is_aligned_addr(paddr, width))
   then MemException(E_SAMO_Addr_Align())
   else {
     let wk : write_kind = match (aq, rl, con) {

model/riscv_step.sail

@@ -145,7 +145,7 @@ function loop () : unit -> unit = {
   let insns_per_tick = plat_insns_per_tick();
   i : int = 0;
   step_no : int = 0;
-  while (~ (htif_done)) do {
+  while not(htif_done) do {
     let stepped = step(step_no);
     if stepped then step_no = step_no + 1;
 

model/riscv_sys_control.sail

@@ -166,21 +166,21 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
 
 val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
 function check_CSR_access(csrrw, csrpr, p, isWrite) =
-    (~ (isWrite == true & csrrw == 0b11))  /* read/write */
+    not(isWrite == true & csrrw == 0b11)  /* read/write */
   & (privLevel_to_bits(p) >=_u csrpr)      /* privilege */
 
 function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
-  ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1)
+  not(csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1)
 
 function check_Counteren(csr : csreg, p : Privilege) -> bool =
   match(csr, p) {
     (0xC00, Supervisor) => mcounteren.CY() == 0b1,
     (0xC01, Supervisor) => mcounteren.TM() == 0b1,
     (0xC02, Supervisor) => mcounteren.IR() == 0b1,
 
-    (0xC00, User) => mcounteren.CY() == 0b1 & ((~ (haveSupMode())) | scounteren.CY() == 0b1),
-    (0xC01, User) => mcounteren.TM() == 0b1 & ((~ (haveSupMode())) | scounteren.TM() == 0b1),
-    (0xC02, User) => mcounteren.IR() == 0b1 & ((~ (haveSupMode())) | scounteren.IR() == 0b1),
+    (0xC00, User) => mcounteren.CY() == 0b1 & (not(haveSupMode()) | scounteren.CY() == 0b1),
+    (0xC01, User) => mcounteren.TM() == 0b1 & (not(haveSupMode()) | scounteren.TM() == 0b1),
+    (0xC02, User) => mcounteren.IR() == 0b1 & (not(haveSupMode()) | scounteren.IR() == 0b1),
 
     (_, _) => /* no HPM counters for now */
               if   0xC03 <=_u csr & csr <=_u 0xC1F
@@ -193,9 +193,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool =
  * allowed in the current priv mode
  */
 function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = {
-  if ~(csr == 0x015) then {
+  if not(csr == 0x015) then {
     true
-  } else if ~(isWrite) then {
+  } else if not(isWrite) then {
     /* Read-only access to the seed CSR is not allowed */
     false
   } else {
@@ -315,7 +315,7 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
       Ints_Empty()      => None(),
       Ints_Pending(p)   => let r = (p, Machine) in Some(r),
       Ints_Delegated(d) =>
-        if (~ (haveSupMode())) then {
+        if not(haveSupMode()) then {
           if uIE then let r = (d, User) in Some(r)
           else                             None()
         } else {
@@ -339,7 +339,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege
   /* If we don't have different privilege levels, we don't need to check delegation.
    * Absence of U-mode implies absence of S-mode.
    */
-  if (~ (haveUsrMode())) | ((~ (haveSupMode())) & (~ (haveNExt()))) then {
+  if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then {
     assert(priv == Machine, "invalid current privilege");
     let enabled_pending = mip.bits() & mie.bits();
     match findPendingInterrupt(enabled_pending) {

model/riscv_sys_regs.sail

@@ -161,11 +161,11 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
          let  v = Mk_Misa(v);
          /* Suppress changing C if nextPC would become misaligned or an extension vetoes or C was disabled at boot (i.e. not supported). */
          let m =
-           if   (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | ~(sys_enable_rvc())
+           if   (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | not(sys_enable_rvc())
            then m
            else update_C(m, v.C());
          /* Handle updates for F/D. */
-         if   ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
+         if   not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0)
          then m
          else update_D(update_F(m, v.F()), v.D())
        }
@@ -316,13 +316,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
           } else m;
 
   /* Hardwired to zero in the absence of 'U' or 'N'. */
-  let m = if (~ (haveNExt())) then {
+  let m = if not(haveNExt()) then {
              let m = update_UPIE(m, 0b0);
              let m = update_UIE(m, 0b0);
              m
           } else m;
 
-  if (~ (haveUsrMode())) then {
+  if not(haveUsrMode()) then {
     let m = update_MPRV(m, 0b0);
     m
   } else m

model/riscv_vmem_sv32.sail

@@ -197,7 +197,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
           match update_PTE_Bits(pteBits, ac, ext_pte) {
             None()           => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw),
             Some(pbits, ext) => {
-              if ~ (plat_enable_dirty_update ())
+              if not(plat_enable_dirty_update())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
                 TR_Failure(PTW_PTE_Update(), ext_ptw)
@@ -230,7 +230,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
               TR_Address(pAddr, ext_ptw)
             },
             Some(pbits, ext) =>
-              if ~ (plat_enable_dirty_update ())
+              if not(plat_enable_dirty_update())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
                 TR_Failure(PTW_PTE_Update(), ext_ptw)

model/riscv_vmem_sv39.sail

@@ -191,7 +191,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
           match update_PTE_Bits(pteBits, ac, ext_pte) {
             None()           => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw),
             Some(pbits, ext) => {
-              if ~ (plat_enable_dirty_update ())
+              if not(plat_enable_dirty_update())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
                 TR_Failure(PTW_PTE_Update(), ext_ptw)
@@ -224,7 +224,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
               TR_Address(pAddr, ext_ptw)
             },
             Some(pbits, ext) =>
-              if ~ (plat_enable_dirty_update ())
+              if not(plat_enable_dirty_update())
               then {
                 /* pte needs dirty/accessed update but that is not enabled */
                 TR_Failure(PTW_PTE_Update(), ext_ptw)

model/riscv_vmem_sv48.sail

@@ -188,7 +188,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
           TR_Address(pAddr, ext_ptw)
         },
         Some(pbits, ext) =>
-          if ~ (plat_enable_dirty_update ())
+          if not(plat_enable_dirty_update())
           then {
             /* pte needs dirty/accessed update but that is not enabled */
             TR_Failure(PTW_PTE_Update(), ext_ptw)

model/riscv_vmem_tlb.sail

@@ -115,8 +115,8 @@ function flush_TLB_Entry(e, asid, addr) = {
   match(asid, addr) {
     ( None(),  None()) => true,
     ( None(), Some(a)) => e.vAddr == (e.vMatchMask & a),
-    (Some(i),  None()) => (e.asid == i) & (~ (e.global)),
+    (Some(i),  None()) => (e.asid == i) & not(e.global),
     (Some(i), Some(a)) => (  (e.asid == i) & (e.vAddr == (a & e.vMatchMask))
-                           & (~ (e.global)))
+                           & not(e.global))
   }
 }