From a42684821d6c0487c248900a89e1f464737da771 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 24 Aug 2017 20:32:17 +0100
Subject: Fix some bugs related to the CHERI spec

- Correctly pass exponentials to Z3
- Infer types of functional record updates
- Support "def Nat"
---
 cheri/cheri_insts.sail       | 4 ++--
 cheri/cheri_prelude_256.sail | 6 +++++-
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 8b5d9dd0..0a286070 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1101,7 +1101,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
   else
     {
       cursor := getCapCursor(cb_val);
-      vAddr  := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
+      vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
       vAddr64:= (bit[64]) vAddr;
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
@@ -1148,7 +1148,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
   else
     {
       cursor := getCapCursor(cb_val);
-      vAddr  := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
+      vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
       vAddr64:= (bit[64]) vAddr;
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index f41d9c14..ee9a91ac 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -35,6 +35,11 @@
 (* 256 bit cap + tag *)
 typedef CapReg = bit[257]
 
+val cast bool -> bit effect pure cast_bool_bit
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_bool_vec
+
+typedef uint64 = range<0, (2** 64) - 1>
+
 typedef CapStruct = const struct {
   bool    tag;
   bit[8]  padding;
@@ -204,4 +209,3 @@ function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65
 
 function CapStruct int_to_cap ((bit[64]) offset) = 
     {null_cap with offset = offset}
-
-- 
cgit v1.2.3