From 01486bf4914c14389a0bf0d4b42088165e9c0289 Mon Sep 17 00:00:00 2001 From: Kristina Sojakova Date: Tue, 2 Jun 2026 15:02:19 +0200 Subject: [PATCH 1/5] Update Core.hs Removed double halt --- src/Core.hs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Core.hs b/src/Core.hs index 5401a98..adbd693 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -396,7 +396,7 @@ execute = do let imm' = imm ++# (0 :: BitVector 12) pure (ADD, pure base', pure imm') Instruction.IType (Env Call) _ _ _ -> - lift halt >> empty + lift setSyscall >> empty Instruction.IType (Env Break) _ _ _ -> lift halt >> empty Instruction.Nop _ -> empty @@ -492,12 +492,6 @@ memory = do setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} Instruction.UType _ rd _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} - Instruction.IType (Env Call) _ _ _ -> do - setSyscall - Instruction.IType (Env Break) _ _ _ -> do - halt - Instruction.Nop Halted -> do - halt _ -> pure () -- | Commit computations to the register file. From 931a2555a90438517ba76dfa06790c31fceefe1c Mon Sep 17 00:00:00 2001 From: Wind Date: Tue, 2 Jun 2026 15:25:37 +0200 Subject: [PATCH 2/5] Revert "Update Core.hs" This reverts commit 01486bf4914c14389a0bf0d4b42088165e9c0289. --- src/Core.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Core.hs b/src/Core.hs index adbd693..5401a98 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -396,7 +396,7 @@ execute = do let imm' = imm ++# (0 :: BitVector 12) pure (ADD, pure base', pure imm') Instruction.IType (Env Call) _ _ _ -> - lift setSyscall >> empty + lift halt >> empty Instruction.IType (Env Break) _ _ _ -> lift halt >> empty Instruction.Nop _ -> empty @@ -492,6 +492,12 @@ memory = do setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} Instruction.UType _ rd _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} + Instruction.IType (Env Call) _ _ _ -> do + setSyscall + Instruction.IType (Env Break) _ _ _ -> do + halt + Instruction.Nop Halted -> do + halt _ -> pure () -- | Commit computations to the register file. From 708078e6b5dcb3df1f783553685a53304884af59 Mon Sep 17 00:00:00 2001 From: Wind Date: Tue, 2 Jun 2026 15:41:04 +0200 Subject: [PATCH 3/5] Remove unnecessary halts --- src/Core.hs | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/Core.hs b/src/Core.hs index 5401a98..f84be4c 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -231,12 +231,11 @@ withCtrlReset :: CPUM f () -> CPUM f (Control f) withCtrlReset m = do modify $ \s -> s {stateCtrl = initCtrl} m - ctrl <- gets stateCtrl - pure ctrl + gets stateCtrl -- | Stop the CPU due to ebreak. -halt :: CPUM f () -halt = +setEBreak :: CPUM f () +setEBreak = modify $ \s -> s {stateHalt = EBreak} -- | Stop the CPU due to syscall. @@ -258,7 +257,7 @@ fetch = do -- Always try to read unless the instruction in the `memory` stage is a load or a store. unless (ctrlMeMemInstr ctrl) $ readPC pc - + -- We stall if the instruction in the `memory` stage is a load or a store. let stall = ctrlMeMemInstr ctrl @@ -285,7 +284,7 @@ decode = do status <- gets stateHalt ir <- - if (inputIsInstr input) + if inputIsInstr input then noSecrets' (inputMem input) (Nop Halted) (pure . decode') else pure $ Nop MemoryBusBusy @@ -396,9 +395,9 @@ execute = do let imm' = imm ++# (0 :: BitVector 12) pure (ADD, pure base', pure imm') Instruction.IType (Env Call) _ _ _ -> - lift halt >> empty + lift setEBreak >> empty Instruction.IType (Env Break) _ _ _ -> - lift halt >> empty + lift setEBreak >> empty Instruction.Nop _ -> empty rs1 :: MaybeT (CPUM f) (f Word) @@ -494,10 +493,6 @@ memory = do setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} Instruction.IType (Env Call) _ _ _ -> do setSyscall - Instruction.IType (Env Break) _ _ _ -> do - halt - Instruction.Nop Halted -> do - halt _ -> pure () -- | Commit computations to the register file. @@ -506,7 +501,6 @@ writeback = do input <- asks inputMem ir <- gets stateWbInstr res <- gets stateWbAluRes - status <- gets stateHalt case ir of Instruction.RType _ rd _ _ -> do From 66df0abcec2a9e5989c3daf606b2a8ac2ddeba21 Mon Sep 17 00:00:00 2001 From: Wind Date: Tue, 2 Jun 2026 16:10:28 +0200 Subject: [PATCH 4/5] Halt the core gracefully by flushing the pipeline before halting --- app/Main.hs | 14 ++++---- src/Core.hs | 64 ++++++++++++++++++--------------- src/Elf/ElfLoader.hs | 16 +++++---- src/Leak/MonitorPC/PC.hs | 6 ++-- src/Leak/PC/Leak.hs | 24 ++++++------- src/Leak/PC/PC.hs | 1 + src/Leak/PC/Sim.hs | 78 +++++++++++++++++++++++----------------- src/Simulate.hs | 3 +- test/Spec.hs | 7 +++- 9 files changed, 123 insertions(+), 90 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index b52c1e5..91d5ba4 100644 --- a/app/Main.hs +++ b/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,7 +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, + let s'' = s' {Core.stateHalt = Nothing, + Core.stateFePc = resumePc, + Core.stateDePc = resumePc, Core.stateRegFile = modifyRF 10 ret (Core.stateRegFile s')} mi'' <- next s'' o pure (mi'', False) @@ -270,7 +272,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 +338,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 diff --git a/src/Core.hs b/src/Core.hs index f84be4c..c8236fa 100644 --- a/src/Core.hs +++ b/src/Core.hs @@ -1,6 +1,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE DerivingStrategies #-} module Core ( initInput, @@ -80,7 +81,7 @@ deriving instance Generic (MemAccess f) deriving instance (Generic (f Word), NFDataX (f Word)) => NFDataX (MemAccess f) -- | The output of the CPU. -data Output f = Output +newtype Output f = Output { -- | A memory access. outMem :: First (MemAccess f) } @@ -99,7 +100,7 @@ instance Monoid (Output f) where mempty = Output mempty -- | CPU halt state -data HaltState = Running | EBreak | Syscall | SecurityViolation +data HaltState = EBreak Address | Syscall Address | SecurityViolation deriving (Show, Eq, Generic) instance NFDataX HaltState @@ -129,7 +130,9 @@ data State f = State -- | Control/forwarding lines. stateCtrl :: Control f, -- | CPU halt state - stateHalt :: HaltState + stateHalt :: Maybe HaltState, + -- | Pending halt state (propagating through pipeline to ensure flush) + stateHaltPending :: Maybe HaltState } deriving instance (Show (f Word)) => Show (State f) @@ -175,7 +178,7 @@ setLines f = modify $ \s -> s {stateCtrl = f (stateCtrl s)} -- | No secrets here, buddy: unwrap a word. If it's public, we gucci. If it's -- private, die. noSecrets' :: (Access f) => f a -> b -> (a -> CPUM f b) -> CPUM f b -noSecrets' w a m = noSecrets w (setSecurityViolation >> pure a) m +noSecrets' w a = noSecrets w (setSecurityViolation >> pure a) -- | Run the CPU for one step. circuit :: (Access f) => State f -> Input f -> (State f, Output f) @@ -211,7 +214,8 @@ init = stateWbAluRes = pure 0, stateRegFile = initRF, stateCtrl = initCtrl, - stateHalt = Running + stateHalt = Nothing, + stateHaltPending = Nothing } -- | Initial control lines. @@ -233,33 +237,27 @@ withCtrlReset m = do m gets stateCtrl --- | Stop the CPU due to ebreak. -setEBreak :: CPUM f () -setEBreak = - modify $ \s -> s {stateHalt = EBreak} - --- | Stop the CPU due to syscall. -setSyscall :: CPUM f () -setSyscall = - modify $ \s -> s {stateHalt = Syscall} - -- | Set security violation flag. setSecurityViolation :: CPUM f () setSecurityViolation = - modify $ \s -> s {stateHalt = SecurityViolation} + modify $ \s -> s {stateHalt = Just SecurityViolation} -- | The fetch stage. fetch :: CPUM f () fetch = do pc <- gets stateFePc ctrl <- gets stateCtrl + status <- gets stateHalt + pending <- gets stateHaltPending - -- Always try to read unless the instruction in the `memory` stage is a load or a store. - unless (ctrlMeMemInstr ctrl) $ + let isHalted = isJust status || isJust pending + + -- Always try to read unless the instruction in the `memory` stage is a load or a store, or the core is halting/halted. + unless (ctrlMeMemInstr ctrl || isHalted) $ readPC pc - -- We stall if the instruction in the `memory` stage is a load or a store. - let stall = ctrlMeMemInstr ctrl + -- We stall if the instruction in the `memory` stage is a load or a store, or the core is halting/halted. + let stall = ctrlMeMemInstr ctrl || isHalted let next_pc = fromMaybe @@ -273,7 +271,7 @@ fetch = do s -- Increment program counter for next fetch. { stateFePc = next_pc, -- Propagate program counter to next stage. - stateDePc = pc + stateDePc = if stall then stateDePc s else pc } -- | Decode stage. @@ -282,6 +280,7 @@ decode = do input <- ask ctrl <- gets stateCtrl status <- gets stateHalt + pending <- gets stateHaltPending ir <- if inputIsInstr input @@ -308,7 +307,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 + | isJust status || isJust pending = Nop Halted -- Otherwise we process the decoded instruction. | otherwise = ir @@ -394,12 +393,18 @@ execute = do PC -> gets $ pack . stateExPc let imm' = imm ++# (0 :: BitVector 12) pure (ADD, pure base', pure imm') - Instruction.IType (Env Call) _ _ _ -> - lift setEBreak >> empty - Instruction.IType (Env Break) _ _ _ -> - lift setEBreak >> empty + Instruction.IType (Env Call) _ _ _ -> do + pc <- gets stateExPc + pendingHalt (Syscall (pc + 4)) + Instruction.IType (Env Break) _ _ _ -> do + pc <- gets stateExPc + pendingHalt (EBreak (pc + 4)) Instruction.Nop _ -> empty + pendingHalt :: HaltState -> MaybeT (CPUM f) a + pendingHalt hState = do + lift (modify $ \s -> s {stateHaltPending = Just hState}) >> empty + rs1 :: MaybeT (CPUM f) (f Word) rs1 = do ir <- gets stateExInstr @@ -463,6 +468,11 @@ memory = do ir <- gets stateMeInstr res <- gets stateMeAluRes val <- gets stateMeStoreRes + pending <- gets stateHaltPending + + case pending of + Just hlt -> modify $ \s -> s {stateHalt = Just hlt, stateHaltPending = Nothing} + Nothing -> pure () modify $ \s -> s {stateWbInstr = ir, stateWbAluRes = res} @@ -491,8 +501,6 @@ memory = do setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} Instruction.UType _ rd _ -> setLines $ \c -> c {ctrlMeRegFwd = Just (rd, res)} - Instruction.IType (Env Call) _ _ _ -> do - setSyscall _ -> pure () -- | Commit computations to the register file. diff --git a/src/Elf/ElfLoader.hs b/src/Elf/ElfLoader.hs index 25f52ec..62dc99f 100644 --- a/src/Elf/ElfLoader.hs +++ b/src/Elf/ElfLoader.hs @@ -21,7 +21,6 @@ import Data.Char (chr) import Data.Elf import Data.Elf.Constants import Data.Elf.Headers -import Data.Int import Data.Word import Types import RegFile (modifyRF) @@ -29,6 +28,7 @@ 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,29 @@ readStringFromMemory addr count = do -- | 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, + let s'' = s' {Core.stateHalt = Nothing, + Core.stateFePc = resumePc, + Core.stateDePc = 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 () \ No newline at end of file + Just (Core.EBreak _) -> pure () + Just Core.SecurityViolation -> pure () \ No newline at end of file diff --git a/src/Leak/MonitorPC/PC.hs b/src/Leak/MonitorPC/PC.hs index 7d69fa9..5f6468b 100644 --- a/src/Leak/MonitorPC/PC.hs +++ b/src/Leak/MonitorPC/PC.hs @@ -17,7 +17,7 @@ import Control.Monad 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 :: Core.State Identity -> (((), Core.State Identity), Sim.State) 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 @@ proj s = (ts, ss) 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 diff --git a/src/Leak/PC/Leak.hs b/src/Leak/PC/Leak.hs index 617fab0..e098c42 100644 --- a/src/Leak/PC/Leak.hs +++ b/src/Leak/PC/Leak.hs @@ -77,7 +77,7 @@ data State = State 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 @@ init = stateWbRes = 0, stateRegFile = initRF, stateMeMemInstr = False, - stateHalt = Running, + stateHalt = Nothing, stateMeRegFwd = Nothing, stateWbRegFwd = Nothing, stateJumpAddr = Nothing, @@ -202,7 +202,7 @@ decode = do -- 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,7 +307,7 @@ execute = 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.BType {} -> case (fromPublic (interpAddr interp_res), interpBranched interp_res) of (Just mAddr, Just branched) -> @@ -315,19 +315,19 @@ execute = do 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 @@ memory = do 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 @@ memory = do 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 @@ writeback = do stateHalted <- gets stateHalt res <- gets stateWbRes - when (stateHalted /= Running) $ do + when (isJust stateHalted) $ do outputNothing tell $ mempty { outHalt = pure True } @@ -405,7 +405,7 @@ writeback = do s { stateMemInstr = Instr.nop, stateExInstr = Instr.nop, - stateHalt = EBreak + stateHalt = Just (EBreak 0) } outputNothing diff --git a/src/Leak/PC/PC.hs b/src/Leak/PC/PC.hs index c284d3d..14ca01d 100644 --- a/src/Leak/PC/PC.hs +++ b/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, diff --git a/src/Leak/PC/Sim.hs b/src/Leak/PC/Sim.hs index 3aebd34..8635b99 100644 --- a/src/Leak/PC/Sim.hs +++ b/src/Leak/PC/Sim.hs @@ -27,7 +27,8 @@ data State = State stateWbInstr :: Leak.Instr, stateJumpAddr :: Maybe Address, stateMeMemInstr :: Bool, - stateHalt :: AimCore.HaltState, + stateHalt :: Maybe AimCore.HaltState, + stateHaltPending :: Maybe AimCore.HaltState, stateDeLoadHazard :: Maybe Address, stateDeCall :: Bool, stateFirstCycle :: Bool @@ -43,7 +44,8 @@ init = stateExInstr = Leak.nop, stateMemInstr = Leak.nop, stateWbInstr = Leak.nop, - stateHalt = AimCore.Running, + stateHalt = Nothing, + stateHaltPending = Nothing, stateMeMemInstr = False, stateJumpAddr = Nothing, stateDeLoadHazard = Nothing, @@ -67,11 +69,15 @@ fetch = do deLoadHazard <- gets stateDeLoadHazard deCall <- gets stateDeCall meMemInstr <- gets stateMeMemInstr + status <- gets stateHalt + pending <- gets stateHaltPending - unless meMemInstr $ + let isHalted = isJust status || isJust pending + + unless (meMemInstr || isHalted) $ outputPc pc - let stall = deCall || meMemInstr + let stall = deCall || meMemInstr || isHalted let next_pc = fromMaybe @@ -83,7 +89,7 @@ fetch = do modify $ \s -> s { stateFePc = next_pc, - stateDePc = pc + stateDePc = if stall then stateDePc s else pc } decode :: SimM () @@ -93,10 +99,13 @@ decode = do exInstr <- gets stateExInstr mJumpAddr <- gets stateJumpAddr firstCycle <- gets stateFirstCycle + status <- gets stateHalt + pending <- gets stateHaltPending let branch_first_cycle = isNopBranchFirstCycle exInstr let load_hazard_first_cycle = isNopLoadHazardFirstCycle exInstr let call_current_cycle = isCall exInstr + let halt_pending = isJust pending -- In Sim, we don't have the real instruction, but we know if it was stalled. let load_hazard_current_cycle = case instrBase instr of @@ -114,13 +123,15 @@ decode = do else if load_hazard_first_cycle then Leak.Instr (Leak.Nop Instr.LoadHazardSecondCycle) (Nothing, Nothing) -- If a syscall is executed in this cycle, we stall. else if call_current_cycle then Leak.Instr (Leak.Nop Instr.Halted) (Nothing, Nothing) + -- If the core is not running anymore, we halt. + else if isJust status || halt_pending then Leak.Instr (Leak.Nop Instr.Halted) (Nothing, Nothing) -- If this is the first cycle, the instruction to decode is gibberish from memory. else if firstCycle then Leak.Instr (Leak.Nop Instr.FirstCycle) (Nothing, Nothing) -- Otherwise we process the instruction from leakage. else instr when (instrBase ir' == Leak.Nop Instr.Halted) $ - modify $ \s -> s {stateHalt = AimCore.SecurityViolation} + modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} when load_hazard_current_cycle $ do pc <- gets stateDePc @@ -150,20 +161,29 @@ execute = do mBranchTaken <- getFirst . Leak.outBranchTaken <$> ask mJumpValid <- getFirst . Leak.outJumpAddrValid <$> ask - modify $ \s -> - s - { stateJumpAddr = mjmpAddr, - stateMemInstr = killJump instr - } - case Leak.instrBase instr of - Leak.Jump -> - when (isNothing mjmpAddr && isNothing mJumpValid) $ - modify $ \s -> s {stateHalt = AimCore.SecurityViolation} - Leak.Branch -> - when (isNothing mBranchTaken) $ - modify $ \s -> s {stateHalt = AimCore.SecurityViolation} - _ -> pure () + Leak.Break -> do + pc <- gets stateExPc + modify $ \s -> + s + { stateJumpAddr = Nothing, + stateHaltPending = Just (AimCore.EBreak (pc + 4)), + stateMemInstr = killJump instr + } + _ -> do + modify $ \s -> + s + { stateJumpAddr = mjmpAddr, + stateMemInstr = killJump instr + } + case Leak.instrBase instr of + Leak.Jump -> + when (isNothing mjmpAddr && isNothing mJumpValid) $ + modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} + Leak.Branch -> + when (isNothing mBranchTaken) $ + modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} + _ -> pure () where dummy = () @@ -172,10 +192,15 @@ memory = do instr <- gets stateMemInstr modify $ \s -> s {stateWbInstr = killJump instr} + pending <- gets stateHaltPending + case pending of + Just hlt -> modify $ \s -> s {stateHalt = Just hlt, stateHaltPending = Nothing} + Nothing -> pure () + mMeMemInstr <- getFirst . Leak.outMeMemInstr <$> ask case mMeMemInstr of Just True -> modify (\s -> s {stateMeMemInstr = True}) >> outputNothing - Just False -> modify $ \s -> s {stateHalt = AimCore.SecurityViolation} + Just False -> modify $ \s -> s {stateHalt = Just AimCore.SecurityViolation} Nothing -> pure () killJump :: Leak.Instr -> Leak.Instr @@ -188,20 +213,9 @@ writeback = do halted <- gets stateHalt mLeakedHalt <- getFirst . Leak.outHalt <$> ask - when (halted /= AimCore.Running || isJust mLeakedHalt) $ + when (isJust halted || isJust mLeakedHalt) $ outputNothing - case Leak.instrBase instr of - Leak.Break -> do - outputNothing - modify $ \s -> - s - { stateMemInstr = Leak.nop, - stateExInstr = Leak.nop, - stateHalt = AimCore.EBreak - } - _ -> pure () - pipe :: SimM () pipe = withCtrlReset $ do writeback diff --git a/src/Simulate.hs b/src/Simulate.hs index 16c6f51..887e4fa 100644 --- a/src/Simulate.hs +++ b/src/Simulate.hs @@ -20,6 +20,7 @@ import Control.Monad.State import Core hiding (State) import qualified Core import Data.Functor.Identity +import Data.Maybe (isJust) import Data.Monoid import Memory.Types import Memory.Vec @@ -42,7 +43,7 @@ simulator = next :: Core.State f -> Output f -> m (Maybe (Input f)) next s (Output mem) = do (mem_in, mem_instr) <- doMemory - if Core.stateHalt s /= Core.Running + if isJust (Core.stateHalt s) then pure Nothing else pure $ Just $ diff --git a/test/Spec.hs b/test/Spec.hs index fbd573f..a58dd4e 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -309,7 +309,11 @@ instance (Arbitrary a) => Arbitrary (PubSec a) where arbitrary = oneof [Public <$> arbitrary, Secret <$> arbitrary] instance Arbitrary Core.HaltState where - arbitrary = elements [Core.Running, Core.EBreak, Core.SecurityViolation] + arbitrary = oneof + [ Core.EBreak <$> arbitrary + , Core.Syscall <$> arbitrary + , pure Core.SecurityViolation + ] instance (Access f, Arbitrary (f Word)) => Arbitrary (RegFile f) where arbitrary = do @@ -331,6 +335,7 @@ instance {-# OVERLAPPING #-} (Access f, Arbitrary (f Word)) => Arbitrary (Core.S <*> arbitrary <*> arbitrary <*> arbitrary + <*> arbitrary instance {-# OVERLAPPING #-} (Access f) => Arbitrary (Input f) where arbitrary = do From 0394f2ded3c79c13cf1188da81868c83159cbd01 Mon Sep 17 00:00:00 2001 From: Wind Date: Thu, 4 Jun 2026 15:48:28 +0200 Subject: [PATCH 5/5] Empty commit