added add delta

CHERICC_Fat.bsv

@@ -37,6 +37,10 @@ export CapMem;
 export CapReg;
 export CapPipe;
 
+export encodeDelta;
+export addDelta;
+export decodeDelta;
+
 export CapFat;
 export MW;
 export OTypeW;
@@ -84,6 +88,7 @@ typedef 0  UPermW;
 typedef 8  MW;
 typedef 6  ExpW;
 typedef 4  OTypeW;
+// typedef 24  Delta;
 typedef `FLAGSW FlagsW;
 typedef 32 CapAddrW;
 typedef 64 CapW;
@@ -92,8 +97,10 @@ typedef 4   UPermW;
 typedef 14  MW;
 typedef 6   ExpW;
 typedef 18  OTypeW;
+// typedef 44  Delta;
 typedef `FLAGSW FlagsW;
 typedef 64  CapAddrW;
+// The capability width changes
 typedef 128 CapW;
 `endif
 
@@ -139,7 +146,7 @@ typedef SizeOf#(Perms) PermsW;
 // The reserved bits
 typedef TSub#(CapW, TAdd#( CapAddrW
                          , TAdd#( OTypeW
-                                , TAdd#( CBoundsW
+                                    , TAdd#( CBoundsW
                                        , TAdd#(PermsW, FlagsW))))) ResW;
 // The full capability structure, including the "tag" bit.
 typedef struct {
@@ -148,6 +155,7 @@ typedef struct {
   Bit#(ResW)   reserved;
   Bit#(FlagsW) flags;
   Bit#(OTypeW) otype;
+  // Bit#(Delta) delta;
   CBounds      bounds;
   CapAddr      address;
 } CapabilityInMemory deriving (Bits, Eq, FShow); // CapW + 1 (tag bit)
@@ -183,6 +191,7 @@ typedef struct {
   Bit#(FlagsW)   flags;
   Bit#(ResW)     reserved;
   Bit#(OTypeW)   otype;
+  // Bit#(Delta)    delta;
   Format         format;
   Bounds         bounds;
 } CapFat deriving (Bits);
@@ -229,6 +238,7 @@ function CapFat unpackCap(Capability thin);
   fat.flags        = memCap.flags;
   fat.reserved     = memCap.reserved;
   fat.otype        = memCap.otype;
+  // fat.delta        = memCap.delta;
   match {.f, .b}   = decBounds(memCap.bounds);
   fat.format       = f;
   fat.bounds       = b;
@@ -691,6 +701,13 @@ function CapFat unseal(CapFat cap, x _);
   ret.otype = otype_unsealed;
   return ret;
 endfunction
+// TODOD Creating Cap function to all delta value 
+// function CapFat addDelta(CapFat cap, x _);
+//   CapFat ret = cap;
+//   ret.delta = x;
+//   return ret;
+// endfunction
+
 function VnD#(CapFat) incOffsetFat( CapFat cap
                                   , CapAddr pointer
                                   , CapAddr offset // this is the increment in inc offset, and the offset in set offset
@@ -1106,6 +1123,7 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
            , pack (cap.reserved)
            , pack (cap.flags)
            , pack (cap.otype)
+          //  , pack (cap.delta)
            , pack (cap.bounds) };
   endfunction
   function getAddr (capMem);
@@ -1167,6 +1185,10 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
   //////////////////////////////////////////////////////////////////////////////
   function isDerivable = error ("isDerivable not implemented for CapMem");
 
+  function encodeDelta (cap, delta) = error ("encode delta not implemented");
+  function addDelta (cap, delta) = error ("addDelta not implemented");
+  function decodeDelta (cap) = error ("decode delta not implemented");
+
 endinstance
 
 instance FShow #(CapPipe);
@@ -1320,6 +1342,11 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
   // capability derivation (bounds set)
   //////////////////////////////////////////////////////////////////////////////
   function setBoundsCombined (cap, length) = error ("setBoundsCombined not implemented for CapReg");
+
+  function encodeDelta (cap, delta) = error ("encode delta not implemented");
+  function addDelta (cap, delta) = error ("addDelta not implemented");
+  function decodeDelta (cap) = error ("decode delta not implemented");
+
   //function setBounds = error ("setBounds not implemented for CapReg");
   //function roundLength = error ("roundLength not implemented for CapReg");
   //function alignmentMask = error ("alignmentMask not implemented for CapReg");
@@ -1392,6 +1419,31 @@ instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
       , mask: result.mask };
   endfunction
 
+  // TODO: Similar to set bounds but sets the delta value between the 38th and 64th bit
+  // function setDeltaValue (cap, length);
+  // endfunction
+
+  function encodeDelta(cap, delta);
+    // Make a test case of adding 3
+    Bit#(25) d = truncate(delta);
+    // d = 15;
+    Bit#(39) va_bits = cap.capFat.address[38:0];
+    cap.capFat.address = {d, va_bits};
+    return cap;
+  endfunction
+
+  function addDelta(cap, delta);
+    Bit#(25) d = truncate(delta);
+    cap.capFat.address = cap.capFat.address + zeroExtend(delta);
+    return cap;
+  endfunction
+
+  
+  // Extract the delta stored in bits 63:39 of the address
+  function decodeDelta(cap);
+    return cap.capFat.address[63:39];
+  endfunction
+
   function nullWithAddr (addr);
     CapReg res = nullWithAddr(addr);
     return CapPipe { capFat: res, tempFields: getTempFields(res) };
@@ -1518,6 +1570,7 @@ typedef 48 VA_Width;
 typedef struct {
   Perms        perms;
   Bit#(FlagsW) flags;
+  // Bit#(Delta)  delta;
   CBounds      bounds;
   Bit#(VA_Width)     address;
   Bool         validAddress;
@@ -1527,7 +1580,7 @@ function CapTrim  trimCap(CapMem cm);
   Bit#(TSub#(CapAddrW,VA_Width)) addr_upper = truncateLSB(cap.address);
   return CapTrim{perms: cap.perms,
                  flags: cap.flags,
-                 bounds: cap.bounds,
+                 bounds: cap.bounds,  
                  address: truncate(cap.address),
                  validAddress: (addr_upper==signExtend(cap.address[valueOf(VA_Width)-1]))
   };
@@ -1547,4 +1600,32 @@ function CapMem untrimCap(CapTrim ct);
   });
 endfunction
 
+  // We do not implement the functions as interfaces 
+  // because all them will have the same implementation/
+  // This negates the purpose of having type classes. 
+  // Create function to set delta value 
+  // function setDeltaValue (CapPipe cap, Bit#(Delta) delta);
+  //   // let result = setDelta(cap.capFat, delta);
+  //   cap.capFat.delta = delta;
+  //   return cap;
+  // endfunction
+
+//   typedef struct {
+//   CapFat capFat;
+//   TempFields tempFields;
+// } CapPipe deriving (Bits);
+
+// typedef struct {
+//   Bool           isCapability;
+//   Bit#(CapAddrW) address;
+//   Bit#(MW)       addrBits;
+//   Perms          perms;
+//   Bit#(FlagsW)   flags;
+//   Bit#(ResW)     reserved;
+//   Bit#(OTypeW)   otype;
+//   // Bit#(Delta)    delta;
+//   Format         format;
+//   Bounds         bounds;
+// } CapFat deriving (Bits);
+
 endpackage

CHERICap.bsv

@@ -172,6 +172,11 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
   // Set the flags field
   function capT setFlags (capT cap, Bit #(flgW) flags);
 
+  function capT encodeDelta(capT cap, Bit #(64) delta);
+  function capT addDelta(capT cap, Bit #(25) delta);
+
+  function Bit #(25) decodeDelta(capT cap);
+
   // capability permissions
   //////////////////////////////////////////////////////////////////////////////
 
@@ -320,6 +325,9 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
   // the null capability (requires a dummy proxy)
   function capT nullCapFromDummy (capT dummy);
 
+  // define set delta function (Disabled when we will use the virtual addresses)
+  // function capT setDeltaValue (capT cap, Bit #(delta) length);
+
   // Assert that the encoding is valid
   //////////////////////////////////////////////////////////////////////////////
 

Makefile

@@ -45,5 +45,5 @@ clean-counterexamples:
 
 clean:
 	rm -rf $(BUILD_DIR)
-
+	
 full-clean: clean clean-counterexamples

assertions.sv

@@ -180,4 +180,3 @@ module assert_prop_setBounds(
   always @(*) begin
     assert(prop_ok);
   end
-endmodule

check.sby

@@ -51,4 +51,3 @@ counterexamples/module_prop_getLength.v
 counterexamples/module_prop_isInBounds.v
 counterexamples/module_prop_setAddr.v
 counterexamples/module_prop_fromToMem.v
-counterexamples/module_prop_setBounds.v