From 654e9fbc68f6e253af41e91bb91edeaba204a9b8 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 27 Apr 2016 12:54:16 +0100
Subject: cheri: add translation and bounds checking of PC via PCC. Slightly
 clunky implementation for now and exceptions not properly handled.

---
 mips/mips_prelude.sail  | 4 ++--
 mips/mips_wrappers.sail | 2 ++
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'mips')

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 18eec9cc..801802de 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -185,7 +185,7 @@ function unit SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) =
 
 typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
 typedef AccessLevel   = enumerate {Kernel; Supervisor; User}
-function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = 
+function (option<Exception>, option<bit[64]>) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
   {
     err := (if (accessType == StoreData) then Some(AdES) else Some(AdEL));
     switch(vAddr[63..62]) {
@@ -203,7 +203,7 @@ function (option<Exception>, option<bit[64]>) TranslateAddress ((bit[64]) vAddr,
   }
 
 function bit[64] TranslateOrExit((bit[64]) vAddr, (MemAccessType) accessType) =
-  switch (TranslateAddress(vAddr, accessType)) {
+  switch (TLBTranslate(vAddr, accessType)) {
     case ((Some(ex)), _)    -> (exit (SignalExceptionBadAddr (ex, vAddr)))
     case (_, (Some(pAddr))) -> pAddr
   }
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index 799b8cc0..d77f176c 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -5,3 +5,5 @@ function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
 function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
     addr
 
+function (option<Exception>, option<bit[64]>) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = 
+    TLBTranslate(vAddr, accessType)
-- 
cgit v1.2.3