Skip to content

Commit

Permalink
symbolic: Make {lookup,update}Reg implementations panic rather than e…
Browse files Browse the repository at this point in the history
…rror

See #412 for the remaining task of
allowing the return types of `GenArchVals`' `{lookup,update}Reg` functions to
indicate the possibility of an error.
  • Loading branch information
RyanGlScott committed Jul 26, 2024
1 parent f47b425 commit dd7f170
Show file tree
Hide file tree
Showing 7 changed files with 62 additions and 6 deletions.
2 changes: 2 additions & 0 deletions macaw-ppc-symbolic/macaw-ppc-symbolic.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,13 @@ library
exposed-modules: Data.Macaw.PPC.Symbolic
other-modules: Data.Macaw.PPC.Symbolic.AtomWrapper
Data.Macaw.PPC.Symbolic.Functions
Data.Macaw.PPC.Symbolic.Panic
Data.Macaw.PPC.Symbolic.Repeat
-- other-extensions:
build-depends: base >=4.10 && <5,
containers,
lens,
panic,
exceptions,
text,
parameterized-utils,
Expand Down
11 changes: 9 additions & 2 deletions macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ import qualified SemMC.Architecture.PPC as SP

import qualified Data.Macaw.PPC.Symbolic.AtomWrapper as A
import qualified Data.Macaw.PPC.Symbolic.Functions as F
import qualified Data.Macaw.PPC.Symbolic.Panic as P
import qualified Data.Macaw.PPC.Symbolic.Repeat as R

ppcMacawSymbolicFns :: ( SP.KnownVariant v
Expand Down Expand Up @@ -219,7 +220,10 @@ archLookupReg :: ( MP.KnownVariant v
archLookupReg regEntry reg =
case lookupReg reg (MCR.regValue regEntry) of
Just (MCRV.RV val) -> MCR.RegEntry (MS.typeToCrucible $ MT.typeRepr reg) val
Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
Nothing -> P.panic
P.PPC
"archLookupReg"
["unexpected register: " ++ show (MC.prettyF reg)]

updateReg :: forall v ppc m f tp
. (MP.KnownVariant v,
Expand All @@ -244,7 +248,10 @@ archUpdateReg :: ( MP.KnownVariant v
archUpdateReg regEntry reg val =
case updateReg reg (const $ MCRV.RV val) (MCR.regValue regEntry) of
Just r -> regEntry { MCR.regValue = r }
Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
Nothing -> P.panic
P.PPC
"archUpdateReg"
["unexpected register: " ++ show (MC.prettyF reg)]


ppcGenFn :: forall ids s tp v ppc
Expand Down
15 changes: 15 additions & 0 deletions macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Panic.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{-# LANGUAGE TemplateHaskell #-}
module Data.Macaw.PPC.Symbolic.Panic (
P.panic,
Component(..)
) where

import qualified Panic as P

data Component = PPC
deriving (Show)

instance P.PanicComponent Component where
panicComponentName = show
panicComponentIssues _ = "https://github.com/GaloisInc/macaw/issues"
panicComponentRevision = $(P.useGitRevision)
11 changes: 9 additions & 2 deletions macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ import qualified Data.Macaw.Symbolic.Backend as MSB
-- macaw-riscv-symbolic
import qualified Data.Macaw.RISCV.Symbolic.AtomWrapper as RA
import qualified Data.Macaw.RISCV.Symbolic.Functions as RF
import qualified Data.Macaw.RISCV.Symbolic.Panic as RP
import qualified Data.Macaw.RISCV.Symbolic.Repeat as RR

riscvMacawSymbolicFns ::
Expand Down Expand Up @@ -178,7 +179,10 @@ archLookupReg :: (G.KnownRV rv, Typeable rv)
archLookupReg regEntry reg =
case lookupReg reg (C.regValue regEntry) of
Just (C.RV val) -> C.RegEntry (MS.typeToCrucible $ MT.typeRepr reg) val
Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
Nothing -> RP.panic
RP.RISCV
"archLookupReg"
["unexpected register: " ++ show (MC.prettyF reg)]

updateReg :: forall rv m f tp
. (G.KnownRV rv, Typeable rv, X.MonadThrow m)
Expand All @@ -199,7 +203,10 @@ archUpdateReg :: (G.KnownRV rv, Typeable rv)
archUpdateReg regEntry reg val =
case updateReg reg (const $ C.RV val) (C.regValue regEntry) of
Just r -> regEntry { C.regValue = r }
Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
Nothing -> RP.panic
RP.RISCV
"archUpdateReg"
["unexpected register: " ++ show (MC.prettyF reg)]

newtype RISCVSymbolicException rv = MissingRegisterInState (Some (MR.RISCVReg rv))
deriving Show
Expand Down
3 changes: 3 additions & 0 deletions x86_symbolic/macaw-x86-symbolic.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ library
macaw-symbolic,
macaw-x86 >= 0.3.1,
mtl,
panic,
parameterized-utils,
prettyprinter >= 1.7.0,
vector,
Expand All @@ -28,6 +29,8 @@ library
exposed-modules:
Data.Macaw.X86.Symbolic
Data.Macaw.X86.Crucible
other-modules:
Data.Macaw.X86.Symbolic.Panic

ghc-options: -Wall -Wcompat
ghc-prof-options: -O2 -fprof-auto-top
Expand Down
11 changes: 9 additions & 2 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ import qualified Data.Macaw.Types as M
import qualified Data.Macaw.X86 as M
import qualified Data.Macaw.X86.X86Reg as M
import Data.Macaw.X86.Crucible
import qualified Data.Macaw.X86.Symbolic.Panic as P
import qualified Flexdis86.Register as F

import qualified What4.Interface as WI
Expand Down Expand Up @@ -367,7 +368,10 @@ x86LookupReg
x86LookupReg reg_struct_entry macaw_reg =
case lookupX86Reg macaw_reg (C.regValue reg_struct_entry) of
Just (C.RV val) -> C.RegEntry (typeToCrucible $ M.typeRepr macaw_reg) val
Nothing -> error $ "unexpected register: " ++ showF macaw_reg
Nothing -> P.panic
P.X86_64
"x86LookupReg"
["unexpected register: " ++ showF macaw_reg]

x86UpdateReg
:: C.RegEntry sym (ArchRegStruct M.X86_64)
Expand All @@ -377,7 +381,10 @@ x86UpdateReg
x86UpdateReg reg_struct_entry macaw_reg val =
case updateX86Reg macaw_reg (\_ -> C.RV val) (C.regValue reg_struct_entry) of
Just res_reg_struct -> reg_struct_entry { C.regValue = res_reg_struct }
Nothing -> error $ "unexpected register: " ++ showF macaw_reg
Nothing -> P.panic
P.X86_64
"x86UpdateReg"
["unexpected register: " ++ showF macaw_reg]

instance GenArchInfo LLVMMemory M.X86_64 where
genArchVals _ _ mOverride = Just $ GenArchVals
Expand Down
15 changes: 15 additions & 0 deletions x86_symbolic/src/Data/Macaw/X86/Symbolic/Panic.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
{-# LANGUAGE TemplateHaskell #-}
module Data.Macaw.X86.Symbolic.Panic (
P.panic,
Component(..)
) where

import qualified Panic as P

data Component = X86_64
deriving (Show)

instance P.PanicComponent Component where
panicComponentName = show
panicComponentIssues _ = "https://github.com/GaloisInc/macaw/issues"
panicComponentRevision = $(P.useGitRevision)

0 comments on commit dd7f170

Please sign in to comment.