From dd7f170bac21cbb255c786dd2db84ceb3a213d82 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 26 Jul 2024 15:00:54 -0400 Subject: [PATCH] symbolic: Make {lookup,update}Reg implementations panic rather than error See https://github.com/GaloisInc/macaw/issues/412 for the remaining task of allowing the return types of `GenArchVals`' `{lookup,update}Reg` functions to indicate the possibility of an error. --- macaw-ppc-symbolic/macaw-ppc-symbolic.cabal | 2 ++ macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs | 11 +++++++++-- .../src/Data/Macaw/PPC/Symbolic/Panic.hs | 15 +++++++++++++++ .../src/Data/Macaw/RISCV/Symbolic.hs | 11 +++++++++-- x86_symbolic/macaw-x86-symbolic.cabal | 3 +++ x86_symbolic/src/Data/Macaw/X86/Symbolic.hs | 11 +++++++++-- x86_symbolic/src/Data/Macaw/X86/Symbolic/Panic.hs | 15 +++++++++++++++ 7 files changed, 62 insertions(+), 6 deletions(-) create mode 100644 macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Panic.hs create mode 100644 x86_symbolic/src/Data/Macaw/X86/Symbolic/Panic.hs diff --git a/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal b/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal index a3b93118..0c129de8 100644 --- a/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal +++ b/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal @@ -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, diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs index ce0f1de1..d41cd644 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs @@ -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 @@ -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, @@ -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 diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Panic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Panic.hs new file mode 100644 index 00000000..93759a30 --- /dev/null +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Panic.hs @@ -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) diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs index 66ae7f74..6c1a9b97 100644 --- a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs @@ -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 :: @@ -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) @@ -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 diff --git a/x86_symbolic/macaw-x86-symbolic.cabal b/x86_symbolic/macaw-x86-symbolic.cabal index fb889f40..91b0b5a8 100644 --- a/x86_symbolic/macaw-x86-symbolic.cabal +++ b/x86_symbolic/macaw-x86-symbolic.cabal @@ -18,6 +18,7 @@ library macaw-symbolic, macaw-x86 >= 0.3.1, mtl, + panic, parameterized-utils, prettyprinter >= 1.7.0, vector, @@ -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 diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs index 24437d2f..104ace92 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs @@ -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 @@ -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) @@ -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 diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic/Panic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic/Panic.hs new file mode 100644 index 00000000..0fc17530 --- /dev/null +++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic/Panic.hs @@ -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)