From cc2e15911d006f0abb033a9147953b0b60a83251 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 17 Feb 2017 15:49:25 +0000
Subject: use fast representable check for csetoffset as well as cincoffset.

---
 cheri/cheri_prelude_128.sail | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 08fd8cf3..345d9502 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -214,16 +214,6 @@ function CapLen getCapLength((CapStruct) c)  = getCapTop(c) - getCapBase(c)
 
 function uint64 getCapCursor((CapStruct) cap) = unsigned(cap.address)
 
-function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
-    let oldBase    = getCapBase(c) in
-    let oldTop     = getCapTop(c) in
-    let (bit[64]) newAddress =  oldBase + offset in
-    let newCap     = { c with address = newAddress } in
-    let newBase    = getCapBase(newCap) in
-    let newTop     = getCapTop(newCap) in
-    let representable = (oldBase == newBase) & (oldTop == newTop) in
-    (representable, newCap)
-
 function bool fastRepCheck((CapStruct) c, (bit[64]) i) =
     let E        = min(unsigned(c.E), 45) in
     let i_top    = signed(i[63..E+20]) in
@@ -238,6 +228,13 @@ function bool fastRepCheck((CapStruct) c, (bit[64]) i) =
       case _  -> false
     } | (E >= 44)
 
+function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
+    let (bit[64]) base       = (bit[64]) (getCapBase(c)) in
+    let (bit[64]) newAddress = base + offset in
+    let newCap     = { c with address = newAddress } in
+    let representable = fastRepCheck(c, (newAddress - c.address)) in
+    (representable, newCap)
+
 function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) =
     let (bit[64]) newAddress = c.address + delta in
     let newCap     = { c with address = newAddress } in
-- 
cgit v1.2.3