Kristina halt no pending

app/Main.hs

@@ -22,7 +22,7 @@ import System.Exit (exitWith, ExitCode(..))
 import Types (Word)
 import Util
 import System.IO
-import Data.Maybe (fromMaybe, isJust)
+import Data.Maybe (fromMaybe, isJust, isNothing)
 import qualified Prelude as P
 import Prelude hiding (Ordering (..), Word, break, init, log, map, not, repeat, undefined, (&&), (++), (||), replicate, zip, take)
 import Data.Traversable
@@ -241,10 +241,10 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta
           (s', o) <- step i s
           let halted = Core.stateHalt s'
           (mi', sysExit) <- case halted of
-            Core.Running -> do
+            Nothing -> do
               mi'' <- next s' o
               pure (mi'', False)
-            Core.Syscall -> do
+            Just (Core.Syscall resumePc) -> do
               -- Handle syscall, write return value to a0, resume
               let serialize = if idx == 0
                     then BS.toStrict . encode
@@ -254,8 +254,9 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta
               case mRet of
                 Nothing -> pure (Nothing, True)  -- exit
                 Just ret -> do
-                  let s'' = s' {Core.stateHalt = Core.Running,
-                                Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')}
+                  let s'' = Core.init {Core.stateFePc = resumePc,
+                                       Core.stateDePc = resumePc,
+                                       Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')}
                   mi'' <- next s'' o
                   pure (mi'', False)
             _ -> pure (Nothing, False)  -- EBreak, SecurityViolation: stop
@@ -270,7 +271,7 @@ runNormalMemory Options{..} elf entryOffset leakOutputHandle leakDigest finalSta
           { stepMem = mem
           , stepSim = newSim
           , stepNextInput = mi'
-          , stepContinue = not sysExit && (halted == Core.Running || halted == Core.Syscall)
+          , stepContinue = not sysExit && (isNothing halted || (\case { Just (Core.Syscall _) -> True; _ -> False }) halted)
           , stepFinalState = s'
           , stepLeakage = leakOutput
           }
@@ -336,7 +337,7 @@ runExecutable opts@Options{..} = do
                 }
           finalState <- readIORef finalStateRef
           case finalState of
-            Just state | Core.stateHalt state == Core.SecurityViolation -> do
+            Just state | Core.stateHalt state == Just Core.SecurityViolation -> do
               putStrLn "Program aborted due to security violation"
             _ -> pure ()
         else do

src/Core.hs

@@ -281,8 +281,7 @@ fetch = do
 decode :: (Access f) => CPUM f ()
 decode = do
   input <- ask
-  ctrl <- gets stateCtrl
-  status <- gets stateHalt
+  ctrl <- gets stateCtrl  
 
   ir <-
     if (inputIsInstr input)
@@ -294,6 +293,7 @@ decode = do
   let load_hazard_first_cycle = maybe False isNopLoadHazardFirstCycle (ctrlExInstr ctrl)
   let call_current_cycle = maybe False isCall (ctrlExInstr ctrl)
   let break_current_cycle = maybe False isBreak (ctrlExInstr ctrl)
+  let halted = maybe False isNopHalted (ctrlExInstr ctrl)
 
   let ir'
         -- If a branch was taken in this cycle, we stall.
@@ -309,7 +309,7 @@ decode = do
         -- If a break is executed in this cycle, we halt.
         | break_current_cycle = Nop Halted
         -- If the core is not running anymore, we halt.
-        | status /= Running = Nop Halted
+        | halted = Nop Halted
         -- Otherwise we process the decoded instruction.
         | otherwise = ir
 
@@ -395,10 +395,8 @@ execute = do
             PC -> gets $ pack . stateExPc
           let imm' = imm ++# (0 :: BitVector 12)
           pure (ADD, pure base', pure imm')
-        Instruction.IType (Env Call) _ _ _ ->
-          lift halt >> empty
-        Instruction.IType (Env Break) _ _ _ ->
-          lift halt >> empty
+        Instruction.IType (Env Call) _ _ _ -> empty
+        Instruction.IType (Env Break) _ _ _ -> empty
         Instruction.Nop _ -> empty
 
     rs1 :: MaybeT (CPUM f) (f Word)
@@ -492,12 +490,10 @@ memory = do
       setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)}
     Instruction.UType _ rd _ ->
       setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)}
-    Instruction.IType (Env Call) _ _ _ -> do
+    Instruction.IType (Env Call) _ _ _ ->
       setSyscall
-    Instruction.IType (Env Break) _ _ _ -> do
+    Instruction.IType (Env Break) _ _ _ ->
       halt
-    Instruction.Nop Halted -> do
-      halt    
     _ -> pure ()
 
 -- | Commit computations to the register file.
@@ -506,7 +502,6 @@ writeback = do
   input <- asks inputMem
   ir <- gets stateWbInstr
   res <- gets stateWbAluRes
-  status <- gets stateHalt
 
   case ir of
     Instruction.RType _ rd _ _ -> do

src/Elf/ElfLoader.hs

@@ -21,14 +21,14 @@
 import Data.Elf
 import Data.Elf.Constants
 import Data.Elf.Headers
-import Data.Int
 import Data.Word
 import Types
 import RegFile (modifyRF)
 import Memory.Types
 import Util
 import Prelude hiding (Ordering (..), Word, init, log, map, not, repeat, undefined, (&&), (++), (||))
 import qualified Prelude as P
+import Control.Monad.IO.Class (MonadIO)
 
 loadElf :: (MonadMemory m) => Elf -> m ()
 loadElf elf@(Elf classS _) = withSingElfClassI classS $ do
@@ -96,27 +96,27 @@
 -- | Called when the core halts with a syscall. Return the value to write to a0, or Nothing to truly exit.
 type Instrument f m = Core.State f -> m (Maybe (f Types.Word))
 
-runElf :: forall f m. (Access f, MonadMemory m) => Instrument f m -> CircuitSim m (Core.Input f) (Core.State f) (Core.Output f) -> m ()
+runElf :: forall f m. (Access f, MonadIO m, MonadMemory m) => Instrument f m -> CircuitSim m (Core.Input f) (Core.State f) (Core.Output f) -> m ()
 runElf instr c = go c
   where
     go sim@(CircuitSim i s step next) = do
       (s', o) <- step i s
       case Core.stateHalt s' of
-        Core.Running -> do
+        Nothing -> do
           mi' <- next s' o
           case mi' of
             Just i' -> go $ sim {circuitInput = i', circuitState = s'}
             Nothing -> pure ()
-        Core.Syscall -> do
+        Just (Core.Syscall resumePc) -> do
           mRet <- instr s'
           case mRet of
             Nothing -> pure ()
             Just ret -> do
-              let s'' = s' {Core.stateHalt = Core.Running,
-                            Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')}
+              let s'' = Core.init {Core.stateFePc = resumePc,
+                                   Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')}
               mi' <- next s'' o
               case mi' of
                 Just i' -> go $ sim {circuitInput = i', circuitState = s''}
                 Nothing -> pure ()
-        Core.EBreak -> pure ()
-        Core.SecurityViolation -> pure ()
+        Just (Core.EBreak _) -> pure ()
+        Just Core.SecurityViolation -> pure ()

src/Instruction.hs

@@ -22,6 +22,7 @@ module Instruction
     isCall,
     isNopBranchFirstCycle,
     isNopLoadHazardFirstCycle,
+    isNopHalted,
     break,
     loadHazard,
     isLoad,
@@ -450,6 +451,10 @@ isNopLoadHazardFirstCycle :: Instruction -> Bool
 isNopLoadHazardFirstCycle (Nop LoadHazardFirstCycle) = True
 isNopLoadHazardFirstCycle _ = False
 
+isNopHalted :: Instruction -> Bool
+isNopHalted (Nop Halted) = True
+isNopHalted _ = False
+
 break :: Instruction
 break = IType (Env Break) 0 0 0
 

src/Leak/MonitorPC/PC.hs

@@ -17,7 +17,7 @@
 import Core (Input (..), MemAccess (..), Output (..))
 import qualified Core
 import Data.Functor.Identity
-import Data.Maybe (isJust)
+import Data.Maybe (isJust, isNothing)
 import Data.Monoid
 import qualified Leak.MonitorPC.MonitorLeak as Leak
 import qualified Leak.MonitorPC.Sim as Sim
@@ -43,7 +43,7 @@
 proj s = (ts, ss)
   where
     ts = Leak.leakProject Leak.monitorPC s
-    halted = Core.stateHalt s /= Core.Running
+    halted = isJust (Core.stateHalt s)
     ss =
       Sim.State
         { Sim.stateFePc = if halted then 0 else Core.stateFePc s,
@@ -58,7 +58,7 @@
           Sim.stateStallFetch = not halted && toStallFetch (Core.stateCtrl s),
           Sim.stateStallDecode = not halted && toStallDecode (Core.stateCtrl s),
           Sim.stateJumpAddr = if halted then Nothing else Core.ctrlExAddress $ Core.stateCtrl s,
-          Sim.stateFirstCycle = not halted && Core.stateHalt s == Core.Running
+          Sim.stateFirstCycle = not halted && isNothing (Core.stateHalt s)
         }
 
     killJump :: Leak.Instr -> Leak.Instr

src/Leak/PC/Leak.hs

@@ -77,7 +77,7 @@
     stateWbRes :: Word,
     stateRegFile :: RegFile Identity,
     stateMeMemInstr :: Bool,
-    stateHalt :: HaltState,
+    stateHalt :: Maybe HaltState,
     stateMeRegFwd :: Maybe (RegIdx, Word),
     stateWbRegFwd :: Maybe (RegIdx, Word),
     stateJumpAddr :: Maybe Address,
@@ -101,7 +101,7 @@
       stateWbRes = 0,
       stateRegFile = initRF,
       stateMeMemInstr = False,
-      stateHalt = Running,
+      stateHalt = Nothing,
       stateMeRegFwd = Nothing,
       stateWbRegFwd = Nothing,
       stateJumpAddr = Nothing,
@@ -202,7 +202,7 @@
         -- Otherwise we process the decoded instruction.
         else instr
 
-  when isSecretInstr $ modify $ \s -> s {stateHalt = SecurityViolation}
+  when isSecretInstr $ modify $ \s -> s {stateHalt = Just SecurityViolation}
 
   let rs1Idx = fromMaybe 0 $ Instr.getRs1 ir'
   let rs2Idx = fromMaybe 0 $ Instr.getRs2 ir'
@@ -307,27 +307,27 @@
           informJumpAddr addr
           tell $ mempty { outJumpAddrValid = pure True }
         _ -> unless (isPublic (interpAddr interp_res)) $
-               modify $ \s -> s {stateHalt = SecurityViolation}
+               modify $ \s -> s {stateHalt = Just SecurityViolation}
     Instr.BType {} ->
       case (fromPublic (interpAddr interp_res), interpBranched interp_res) of
         (Just mAddr, Just branched) ->
           case fromPublic branched of
             Just True -> do
               case mAddr of
                 Just addr -> informJumpAddr addr
-                Nothing -> modify $ \s -> s {stateHalt = SecurityViolation}
+                Nothing -> modify $ \s -> s {stateHalt = Just SecurityViolation}
               tell $ mempty { outBranchTaken = pure True }
             Just False -> tell $ mempty { outBranchTaken = pure False }
-            Nothing -> modify $ \s -> s {stateHalt = SecurityViolation}
+            Nothing -> modify $ \s -> s {stateHalt = Just SecurityViolation}
         _ -> unless (isPublic (interpAddr interp_res)) $
-               modify $ \s -> s {stateHalt = SecurityViolation}
+               modify $ \s -> s {stateHalt = Just SecurityViolation}
     Instr.JType _ _ ->
       case fromPublic (interpAddr interp_res) of
         Just (Just addr) -> do
           informJumpAddr addr
           tell $ mempty { outJumpAddrValid = pure True }
         _ -> unless (isPublic (interpAddr interp_res)) $
-               modify $ \s -> s {stateHalt = SecurityViolation}
+               modify $ \s -> s {stateHalt = Just SecurityViolation}
     Instr.SType {} -> do
       r2Val <- unAccess <$> r2M
       modify $ \s -> s { stateMemVal = r2Val }
@@ -369,7 +369,7 @@
       modify $ \s -> s {stateMeRegFwd = Nothing}
       if isSecretAddr
         then do
-          modify $ \s -> s {stateHalt = SecurityViolation}
+          modify $ \s -> s {stateHalt = Just SecurityViolation}
           tell $ mempty {outMeMemInstr = pure False}
         else setMeMemInstr
     Instr.IType (Instr.Env Instr.Call) _ _ _ -> do
@@ -378,7 +378,7 @@
     Instr.SType {} -> do
       if isSecretAddr
         then do
-          modify $ \s -> s {stateHalt = SecurityViolation}
+          modify $ \s -> s {stateHalt = Just SecurityViolation}
           tell $ mempty {outMeMemInstr = pure False}
         else setMeMemInstr
     _ -> pure ()
@@ -396,7 +396,7 @@
   stateHalted <- gets stateHalt
   res <- gets stateWbRes
 
-  when (stateHalted /= Running) $ do
+  when (isJust stateHalted) $ do
     outputNothing
     tell $ mempty { outHalt = pure True }
 
@@ -405,7 +405,7 @@
       s
         { stateMemInstr = Instr.nop,
           stateExInstr = Instr.nop,
-          stateHalt = EBreak
+          stateHalt = Just (EBreak 0)
         }
     outputNothing
 

src/Leak/PC/PC.hs

@@ -105,6 +105,7 @@ proj s = (ts, ss)
           Sim.stateMemInstr = killJump $ toLeakInstr $ Core.stateMeInstr s,
           Sim.stateWbInstr = killJump $ toLeakInstr $ Core.stateWbInstr s,
           Sim.stateHalt = Core.stateHalt s,
+          Sim.stateHaltPending = Core.stateHaltPending s,
           Sim.stateMeMemInstr = Core.ctrlMeMemInstr $ Core.stateCtrl s,
           Sim.stateJumpAddr = Core.ctrlExAddress $ Core.stateCtrl s,
           Sim.stateDeLoadHazard = Core.ctrlDeLoadHazard $ Core.stateCtrl s,