From f47b425765521889d8c3c65ab87f8fd234a1a22b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 26 Jul 2024 10:46:07 -0400 Subject: [PATCH 1/3] Implement macaw-riscv-symbolic This adds the necessary plumbing to simulate Macaw-lifted RISC-V binaries using `macaw-symbolic`. This proves relatively straightforward, given that RISC-V does not have a lot of special primitive functions or statements to deal with. I have also added a basic test suite to ensure that `macaw-riscv-symbolic` works on end-to-end examples. Fixes #409. --- .github/workflows/ci.yaml | 6 +- cabal.project.dist | 1 + macaw-riscv-symbolic/ChangeLog.md | 5 + macaw-riscv-symbolic/LICENSE | 30 ++ macaw-riscv-symbolic/Setup.hs | 2 + .../macaw-riscv-symbolic.cabal | 144 +++++++++ .../src/Data/Macaw/RISCV/Symbolic.hs | 299 ++++++++++++++++++ .../Data/Macaw/RISCV/Symbolic/AtomWrapper.hs | 29 ++ .../Data/Macaw/RISCV/Symbolic/Functions.hs | 54 ++++ .../src/Data/Macaw/RISCV/Symbolic/Panic.hs | 15 + .../src/Data/Macaw/RISCV/Symbolic/Repeat.hs | 30 ++ macaw-riscv-symbolic/tests/Main.hs | 218 +++++++++++++ macaw-riscv-symbolic/tests/README.org | 18 ++ macaw-riscv-symbolic/tests/fail/Makefile | 23 ++ macaw-riscv-symbolic/tests/fail/constant.c | 16 + .../tests/fail/constant.opt32.exe | Bin 0 -> 760 bytes .../tests/fail/constant.opt64.exe | Bin 0 -> 1072 bytes .../tests/fail/constant.unopt32.exe | Bin 0 -> 804 bytes .../tests/fail/constant.unopt64.exe | Bin 0 -> 1128 bytes macaw-riscv-symbolic/tests/pass/Makefile | 23 ++ macaw-riscv-symbolic/tests/pass/identity.c | 15 + .../tests/pass/identity.opt32.exe | Bin 0 -> 756 bytes .../tests/pass/identity.opt64.exe | Bin 0 -> 1072 bytes .../tests/pass/identity.unopt32.exe | Bin 0 -> 792 bytes .../tests/pass/identity.unopt64.exe | Bin 0 -> 1112 bytes .../tests/pass/saturate-add.c | 13 + .../tests/pass/saturate-add.opt32.exe | Bin 0 -> 764 bytes .../tests/pass/saturate-add.opt64.exe | Bin 0 -> 1080 bytes .../tests/pass/saturate-add.unopt32.exe | Bin 0 -> 876 bytes .../tests/pass/saturate-add.unopt64.exe | Bin 0 -> 1224 bytes macaw-riscv/src/Data/Macaw/RISCV.hs | 5 +- macaw-riscv/src/Data/Macaw/RISCV/Arch.hs | 15 + macaw-riscv/src/Data/Macaw/RISCV/RISCVReg.hs | 8 +- 33 files changed, 965 insertions(+), 4 deletions(-) create mode 100644 macaw-riscv-symbolic/ChangeLog.md create mode 100644 macaw-riscv-symbolic/LICENSE create mode 100644 macaw-riscv-symbolic/Setup.hs create mode 100644 macaw-riscv-symbolic/macaw-riscv-symbolic.cabal create mode 100644 macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs create mode 100644 macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/AtomWrapper.hs create mode 100644 macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs create mode 100644 macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Panic.hs create mode 100644 macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Repeat.hs create mode 100644 macaw-riscv-symbolic/tests/Main.hs create mode 100644 macaw-riscv-symbolic/tests/README.org create mode 100644 macaw-riscv-symbolic/tests/fail/Makefile create mode 100644 macaw-riscv-symbolic/tests/fail/constant.c create mode 100755 macaw-riscv-symbolic/tests/fail/constant.opt32.exe create mode 100755 macaw-riscv-symbolic/tests/fail/constant.opt64.exe create mode 100755 macaw-riscv-symbolic/tests/fail/constant.unopt32.exe create mode 100755 macaw-riscv-symbolic/tests/fail/constant.unopt64.exe create mode 100644 macaw-riscv-symbolic/tests/pass/Makefile create mode 100644 macaw-riscv-symbolic/tests/pass/identity.c create mode 100755 macaw-riscv-symbolic/tests/pass/identity.opt32.exe create mode 100755 macaw-riscv-symbolic/tests/pass/identity.opt64.exe create mode 100755 macaw-riscv-symbolic/tests/pass/identity.unopt32.exe create mode 100755 macaw-riscv-symbolic/tests/pass/identity.unopt64.exe create mode 100644 macaw-riscv-symbolic/tests/pass/saturate-add.c create mode 100755 macaw-riscv-symbolic/tests/pass/saturate-add.opt32.exe create mode 100755 macaw-riscv-symbolic/tests/pass/saturate-add.opt64.exe create mode 100755 macaw-riscv-symbolic/tests/pass/saturate-add.unopt32.exe create mode 100755 macaw-riscv-symbolic/tests/pass/saturate-add.unopt64.exe diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 4e81b5463..f3f7d0536 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -130,11 +130,15 @@ jobs: run: cabal test pkg:macaw-ppc-symbolic - name: Build macaw-riscv - run: cabal build pkg:macaw-riscv + run: cabal build pkg:macaw-riscv pkg:macaw-riscv-symbolic - name: Test macaw-riscv run: cabal test pkg:macaw-riscv + - name: Test macaw-riscv-symbolic + if: runner.os == 'Linux' + run: cabal test pkg:macaw-riscv-symbolic + - name: Build macaw-refinement run: cabal build pkg:macaw-refinement diff --git a/cabal.project.dist b/cabal.project.dist index d72f6888f..e982ec96a 100644 --- a/cabal.project.dist +++ b/cabal.project.dist @@ -5,6 +5,7 @@ packages: base/ macaw-ppc/ macaw-ppc-symbolic/ macaw-riscv/ + macaw-riscv-symbolic/ x86/ symbolic/ symbolic-syntax/ diff --git a/macaw-riscv-symbolic/ChangeLog.md b/macaw-riscv-symbolic/ChangeLog.md new file mode 100644 index 000000000..85a6c5ec6 --- /dev/null +++ b/macaw-riscv-symbolic/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for macaw-riscv-symbolic + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/macaw-riscv-symbolic/LICENSE b/macaw-riscv-symbolic/LICENSE new file mode 100644 index 000000000..511de5004 --- /dev/null +++ b/macaw-riscv-symbolic/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2024 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/macaw-riscv-symbolic/Setup.hs b/macaw-riscv-symbolic/Setup.hs new file mode 100644 index 000000000..9a994af67 --- /dev/null +++ b/macaw-riscv-symbolic/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal b/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal new file mode 100644 index 000000000..d203f093c --- /dev/null +++ b/macaw-riscv-symbolic/macaw-riscv-symbolic.cabal @@ -0,0 +1,144 @@ +Cabal-version: 2.2 +Name: macaw-riscv-symbolic +Version: 0.1 +Author: Galois Inc. +Maintainer: rscott@galois.com +Build-type: Simple +License: BSD-3-Clause +License-file: LICENSE +Category: Language +Synopsis: A symbolic reasoning backend for RISC-V +-- Description: +extra-doc-files: README.md + +common shared + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 8.10 or earlier: + ghc-options: + -Wall + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=typed-holes + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unticked-promoted-constructors + -Werror=unused-imports + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc >= 9.2) + ghc-options: + -Werror=ambiguous-fields + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=redundant-bang-patterns + + if impl(ghc >= 9.4) + ghc-options: + -Werror=forall-identifier + -Werror=misplaced-pragmas + -Werror=redundant-strictness-flags + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + + ghc-prof-options: -O2 -fprof-auto-top + default-language: Haskell2010 + +library + import: shared + + build-depends: + base >= 4.13, + containers, + crucible, + crucible-llvm, + exceptions, + grift, + lens, + macaw-base, + macaw-riscv, + macaw-symbolic, + panic, + parameterized-utils, + what4 + + hs-source-dirs: src + + exposed-modules: + Data.Macaw.RISCV.Symbolic + other-modules: + Data.Macaw.RISCV.Symbolic.AtomWrapper + Data.Macaw.RISCV.Symbolic.Functions + Data.Macaw.RISCV.Symbolic.Panic + Data.Macaw.RISCV.Symbolic.Repeat + +test-suite macaw-riscv-symbolic-tests + import: shared + + type: exitcode-stdio-1.0 + main-is: Main.hs + + build-depends: + base >= 4, + bytestring, + containers, + crucible, + crucible-llvm, + elf-edit, + filepath, + Glob >= 0.9 && < 0.11, + grift, + lens, + macaw-base, + macaw-riscv, + macaw-riscv-symbolic, + macaw-symbolic, + parameterized-utils, + prettyprinter, + tasty, + tasty-hunit, + text, + what4, + vector + + hs-source-dirs: tests diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs new file mode 100644 index 000000000..66ae7f741 --- /dev/null +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic.hs @@ -0,0 +1,299 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} +module Data.Macaw.RISCV.Symbolic + ( riscvMacawSymbolicFns + , riscvMacawEvalFn + , lookupReg + , updateReg + ) where + +import Control.Lens ((%~), (&)) +import qualified Control.Monad.Catch as X +import Control.Monad.IO.Class (liftIO) +import Data.Functor (void) +import qualified Data.Kind as DK +import qualified Data.Functor.Identity as I +import qualified Data.Parameterized.Map as MapF +import qualified Data.Parameterized.Classes as PC +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(..)) +import qualified Data.Parameterized.TraversableF as TF +import qualified Data.Parameterized.TraversableFC as FC +import Data.Typeable (Typeable) + +-- crucible +import qualified Lang.Crucible.CFG.Expr as C +import qualified Lang.Crucible.CFG.Reg as C +import qualified Lang.Crucible.Simulator as C +import qualified Lang.Crucible.Types as C + +-- crucible-llvm +import qualified Lang.Crucible.LLVM.MemModel as LCLM + +-- grift +import qualified GRIFT.Types as G + +-- what4 +import qualified What4.Symbol as WS + +-- macaw-base +import qualified Data.Macaw.CFG as MC +import qualified Data.Macaw.Types as MT + +-- macaw-riscv +import qualified Data.Macaw.RISCV as MR + +-- macaw-symbolic +import qualified Data.Macaw.Symbolic as MS +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.Repeat as RR + +riscvMacawSymbolicFns :: + forall rv + . (G.KnownRV rv, MR.RISCVConstraints rv) + => MS.MacawSymbolicArchFunctions (MR.RISCV rv) +riscvMacawSymbolicFns = + MSB.MacawSymbolicArchFunctions + { MSB.crucGenArchConstraints = \x -> x + , MSB.crucGenArchRegName = riscvRegName + , MSB.crucGenRegAssignment = riscvRegAssignment + , MSB.crucGenRegStructType = riscvRegStructType (PC.knownRepr :: G.RVRepr rv) + , MSB.crucGenArchFn = riscvGenFn + , MSB.crucGenArchStmt = riscvGenStmt + , MSB.crucGenArchTermStmt = riscvGenTermStmt + } + +type instance MS.ArchRegContext (MR.RISCV rv) = + (Ctx.EmptyCtx Ctx.::> MT.BVType (G.RVWidth rv) -- PC + Ctx.<+> RR.CtxRepeat 31 (MT.BVType (G.RVWidth rv)) -- GPR regs. We use 31 instead of 32 + -- because we exclude x0, which is + -- hardwired to the constant 0. + Ctx.<+> RR.CtxRepeat 32 (MT.BVType (G.RVFloatWidth rv)) -- FPR regs + Ctx.<+> RR.CtxRepeat 23 (MT.BVType (G.RVWidth rv)) -- CSR regs. Although there is a + -- theoretical maximum of 4096 of + -- these registers, `grift` only + -- supports 23 of them in practice. + Ctx.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 2 -- PrivLevel + Ctx.::> MT.BoolType)) -- EXC + +riscvMacawEvalFn :: RF.SymFuns sym + -> MS.MacawArchStmtExtensionOverride (MR.RISCV rv) + -> MS.MacawArchEvalFn p sym mem (MR.RISCV rv) +riscvMacawEvalFn fs (MS.MacawArchStmtExtensionOverride override) = + MSB.MacawArchEvalFn $ \_ _ xt s -> do + mRes <- override xt s + case mRes of + Nothing -> + case xt of + RISCVPrimFn fn -> RF.funcSemantics fs fn s + RISCVPrimStmt stmt -> RF.stmtSemantics fs stmt s + RISCVPrimTerm term -> RF.termSemantics fs term s + Just res -> return res + +instance (MS.IsMemoryModel mem, G.KnownRV rv, MR.RISCVConstraints rv, Typeable rv) + => MS.GenArchInfo mem (MR.RISCV rv) where + genArchVals _ _ mOverride = Just $ MS.GenArchVals + { MS.archFunctions = riscvMacawSymbolicFns + , MS.withArchEval = \sym k -> do + sfns <- liftIO $ RF.newSymFuns sym + let override = case mOverride of + Nothing -> MS.defaultMacawArchStmtExtensionOverride + Just ov -> ov + k (riscvMacawEvalFn sfns override) + , MS.withArchConstraints = \x -> x + , MS.lookupReg = archLookupReg + , MS.updateReg = archUpdateReg + } + +riscvRegName :: MR.RISCVReg rv tp -> WS.SolverSymbol +riscvRegName r = WS.systemSymbol ("r!" ++ show (MC.prettyF r)) + +-- Note that `repeatAssign` starts indexing from 0, but we want to exclude +-- `GPR 0` (i.e., x0), as this is always hardwired to the constant 0. As such, +-- we offset all of the indexes by one using (+ 1). +gprRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 31 (MT.BVType (G.RVWidth rv))) +gprRegs = RR.repeatAssign (MR.GPR . fromIntegral . (+ 1)) + +fprRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 32 (MT.BVType (G.RVFloatWidth rv))) +fprRegs = RR.repeatAssign (MR.FPR . fromIntegral) + +-- | The RISC-V control/status registers that are directly supported by Macaw. +csrRegs :: Ctx.Assignment (MR.RISCVReg rv) (RR.CtxRepeat 23 (MT.BVType (G.RVWidth rv))) +csrRegs = RR.repeatAssign (MR.CSR . toEnum) + +-- | This contains an assignment that stores the register associated with each index in the +-- RISC-V register structure. +riscvRegAssignment :: Ctx.Assignment (MR.RISCVReg rv) (MS.ArchRegContext (MR.RISCV rv)) +riscvRegAssignment = + Ctx.Empty Ctx.:> MR.PC + Ctx.<++> gprRegs + Ctx.<++> fprRegs + Ctx.<++> csrRegs + Ctx.<++> (Ctx.Empty Ctx.:> MR.PrivLevel Ctx.:> MR.EXC) + +riscvRegStructType :: + forall rv + . G.KnownRV rv + => G.RVRepr rv + -> C.TypeRepr (MSB.ArchRegStruct (MR.RISCV rv)) +riscvRegStructType _rv = + C.StructRepr $ MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr $ riscvRegAssignment @rv + +regIndexMap :: forall rv + . G.KnownRV rv + => MSB.RegIndexMap (MR.RISCV rv) +regIndexMap = MSB.mkRegIndexMap assgn sz + where + assgn = riscvRegAssignment @rv + sz = Ctx.size $ MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr assgn + +lookupReg :: forall rv m f tp + . (G.KnownRV rv, Typeable rv, X.MonadThrow m) + => MR.RISCVReg rv tp + -> Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv)) + -> m (f (MS.ToCrucibleType tp)) +lookupReg r asgn = + case MapF.lookup r regIndexMap of + Nothing -> X.throwM (MissingRegisterInState (Some r)) + Just pair -> return (asgn Ctx.! MSB.crucibleIndex pair) + +archLookupReg :: (G.KnownRV rv, Typeable rv) + => C.RegEntry sym (MS.ArchRegStruct (MR.RISCV rv)) + -> MR.RISCVReg rv tp + -> C.RegEntry sym (MS.ToCrucibleType tp) +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) + +updateReg :: forall rv m f tp + . (G.KnownRV rv, Typeable rv, X.MonadThrow m) + => MR.RISCVReg rv tp + -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp)) + -> Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv)) + -> m (Ctx.Assignment f (MS.MacawCrucibleRegTypes (MR.RISCV rv))) +updateReg r upd asgn = do + case MapF.lookup r regIndexMap of + Nothing -> X.throwM (MissingRegisterInState (Some r)) + Just pair -> return (asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd) + +archUpdateReg :: (G.KnownRV rv, Typeable rv) + => C.RegEntry sym (MS.ArchRegStruct (MR.RISCV rv)) + -> MR.RISCVReg rv tp + -> C.RegValue sym (MS.ToCrucibleType tp) + -> C.RegEntry sym (MS.ArchRegStruct (MR.RISCV 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) + +newtype RISCVSymbolicException rv = MissingRegisterInState (Some (MR.RISCVReg rv)) + deriving Show +instance Typeable rv => X.Exception (RISCVSymbolicException rv) + +data RISCVStmtExtension rv (f :: C.CrucibleType -> DK.Type) (ctp :: C.CrucibleType) where + -- | Wrappers around the arch-specific functions in RISC-V; these are + -- interpreted in 'funcSemantics'. + RISCVPrimFn :: MR.RISCVPrimFn rv (RA.AtomWrapper f) t + -> RISCVStmtExtension rv f (MS.ToCrucibleType t) + -- | Wrappers around the arch-specific statements in RISC-V; these are + -- interpreted in 'stmtSemantics' + RISCVPrimStmt :: MR.RISCVStmt rv (RA.AtomWrapper f) + -> RISCVStmtExtension rv f C.UnitType + -- | Wrappers around the arch-specific terminators in RISC-V; these are + -- interpreted in 'termSemantics' + RISCVPrimTerm :: MR.RISCVTermStmt rv (RA.AtomWrapper f) + -> RISCVStmtExtension rv f C.UnitType + +instance FC.FunctorFC (RISCVStmtExtension ppc) where + fmapFC f (RISCVPrimFn x) = RISCVPrimFn (FC.fmapFC (RA.liftAtomMap f) x) + fmapFC f (RISCVPrimStmt s) = RISCVPrimStmt (TF.fmapF (RA.liftAtomMap f) s) + fmapFC f (RISCVPrimTerm t) = RISCVPrimTerm (TF.fmapF (RA.liftAtomMap f) t) + +instance FC.FoldableFC (RISCVStmtExtension ppc) where + foldMapFC f (RISCVPrimFn x) = FC.foldMapFC (RA.liftAtomIn f) x + foldMapFC f (RISCVPrimStmt s) = TF.foldMapF (RA.liftAtomIn f) s + foldMapFC f (RISCVPrimTerm t) = TF.foldMapF (RA.liftAtomIn f) t + +instance FC.TraversableFC (RISCVStmtExtension ppc) where + traverseFC f (RISCVPrimFn x) = RISCVPrimFn <$> FC.traverseFC (RA.liftAtomTrav f) x + traverseFC f (RISCVPrimStmt s) = RISCVPrimStmt <$> TF.traverseF (RA.liftAtomTrav f) s + traverseFC f (RISCVPrimTerm t) = RISCVPrimTerm <$> TF.traverseF (RA.liftAtomTrav f) t + +instance C.TypeApp (RISCVStmtExtension v) where + appType (RISCVPrimFn x) = MS.typeToCrucible (MT.typeRepr x) + appType (RISCVPrimStmt _s) = C.UnitRepr + appType (RISCVPrimTerm _t) = C.UnitRepr + +instance C.PrettyApp (RISCVStmtExtension v) where + ppApp ppSub (RISCVPrimFn x) = + I.runIdentity (MC.ppArchFn (I.Identity . RA.liftAtomIn ppSub) x) + ppApp ppSub (RISCVPrimStmt s) = + MC.ppArchStmt (RA.liftAtomIn ppSub) s + ppApp ppSub (RISCVPrimTerm t) = MC.ppArchTermStmt (RA.liftAtomIn ppSub) t + +type instance MSB.MacawArchStmtExtension (MR.RISCV rv) = RISCVStmtExtension rv + +riscvGenFn :: forall rv ids s tp + . MR.RISCVPrimFn rv (MC.Value (MR.RISCV rv) ids) tp + -> MSB.CrucGen (MR.RISCV rv) ids s (C.Atom s (MS.ToCrucibleType tp)) +riscvGenFn fn = + case fn of + MR.RISCVEcall w v0 v1 v2 v3 v4 v5 v6 v7 -> do + a0 <- MSB.valueToCrucible v0 + a1 <- MSB.valueToCrucible v1 + a2 <- MSB.valueToCrucible v2 + a3 <- MSB.valueToCrucible v3 + a4 <- MSB.valueToCrucible v4 + a5 <- MSB.valueToCrucible v5 + a6 <- MSB.valueToCrucible v6 + a7 <- MSB.valueToCrucible v7 + + let syscallArgs = Ctx.Empty Ctx.:> a0 Ctx.:> a1 Ctx.:> a2 Ctx.:> a3 Ctx.:> a4 Ctx.:> a5 Ctx.:> a6 Ctx.:> a7 + let argTypes = PC.knownRepr + let retTypes = Ctx.Empty Ctx.:> LCLM.LLVMPointerRepr w Ctx.:> LCLM.LLVMPointerRepr w + let retRepr = C.StructRepr retTypes + syscallArgStructAtom <- MSB.evalAtom (C.EvalApp (C.MkStruct argTypes syscallArgs)) + let lookupHdlStmt = MS.MacawLookupSyscallHandle argTypes retTypes syscallArgStructAtom + hdlAtom <- MSB.evalMacawStmt lookupHdlStmt + MSB.evalAtom $! C.Call hdlAtom syscallArgs retRepr + +riscvGenStmt :: forall rv ids s + . MR.RISCVStmt rv (MC.Value (MR.RISCV rv) ids) + -> MSB.CrucGen (MR.RISCV rv) ids s () +riscvGenStmt s = do + s' <- TF.traverseF f s + void (MSB.evalArchStmt (RISCVPrimStmt s')) + where + f :: forall a + . MC.Value (MR.RISCV rv) ids a + -> MSB.CrucGen (MR.RISCV rv) ids s (RA.AtomWrapper (C.Atom s) a) + f x = RA.AtomWrapper <$> MSB.valueToCrucible x + +riscvGenTermStmt :: forall rv ids s + . MR.RISCVTermStmt rv (MC.Value (MR.RISCV rv) ids) + -> MC.RegState (MR.RISCVReg rv) (MC.Value (MR.RISCV rv) ids) + -> Maybe (C.Label s) + -> MSB.CrucGen (MR.RISCV rv) ids s () +riscvGenTermStmt ts _rs _fallthrough = do + ts' <- TF.traverseF f ts + void (MSB.evalArchStmt (RISCVPrimTerm ts')) + where + f :: forall a + . MC.Value (MR.RISCV rv) ids a + -> MSB.CrucGen (MR.RISCV rv) ids s (RA.AtomWrapper (C.Atom s) a) + f x = RA.AtomWrapper <$> MSB.valueToCrucible x diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/AtomWrapper.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/AtomWrapper.hs new file mode 100644 index 000000000..0666d4170 --- /dev/null +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/AtomWrapper.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} +module Data.Macaw.RISCV.Symbolic.AtomWrapper ( + AtomWrapper(..), + liftAtomMap, + liftAtomTrav, + liftAtomIn + ) where + +import Data.Kind ( Type ) + +import qualified Lang.Crucible.Types as C +import qualified Data.Macaw.Types as MT +import qualified Data.Macaw.Symbolic as MS + +newtype AtomWrapper (f :: C.CrucibleType -> Type) (tp :: MT.Type) + = AtomWrapper (f (MS.ToCrucibleType tp)) + +liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t +liftAtomMap f (AtomWrapper x) = AtomWrapper (f x) + +liftAtomTrav :: + Functor m => + (forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t)) +liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x + +liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a +liftAtomIn f (AtomWrapper x) = f x diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs new file mode 100644 index 000000000..230c7a615 --- /dev/null +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Data.Macaw.RISCV.Symbolic.Functions + ( SymFuns + , newSymFuns + , funcSemantics + , stmtSemantics + , termSemantics + ) where + +-- crucible +import qualified Lang.Crucible.Backend as C +import qualified Lang.Crucible.Simulator.ExecutionTree as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Types as C + +-- macaw-riscv +import qualified Data.Macaw.RISCV as MR + +-- macaw-symbolic +import qualified Data.Macaw.Symbolic as MS + +-- macaw-riscv-symbolic +import qualified Data.Macaw.RISCV.Symbolic.AtomWrapper as RA +import qualified Data.Macaw.RISCV.Symbolic.Panic as RP + +data SymFuns sym = SymFuns + +funcSemantics :: SymFuns sym + -> MR.RISCVPrimFn rv (RA.AtomWrapper f) mt + -> S p rv sym rtp bs r ctx + -> IO (C.RegValue sym (MS.ToCrucibleType mt), S p rv sym rtp bs r ctx) +funcSemantics _sf pf _s = + case pf of + MR.RISCVEcall {} -> + RP.panic RP.RISCV "funcSemantics" ["The RISC-V syscall primitive should be eliminated and replaced by a handle lookup"] + +stmtSemantics :: SymFuns sym + -> MR.RISCVStmt rv (RA.AtomWrapper (C.RegEntry sym)) + -> S p rv sym rtp bs r ctx + -> IO (C.RegValue sym C.UnitType, S p rv sym rtp bs r ctx) +stmtSemantics _sf stmt _s = case stmt of {} + +newSymFuns :: forall sym . (C.IsSymInterface sym) => sym -> IO (SymFuns sym) +newSymFuns _sym = pure SymFuns + +termSemantics :: SymFuns sym + -> MR.RISCVTermStmt rv (RA.AtomWrapper (C.RegEntry sym)) + -> S p rv sym rtp bs r ctx + -> IO (C.RegValue sym C.UnitType, S p rv sym rtp bs r ctx) +termSemantics _fs term _s = case term of {} + +type S p rv sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (MR.RISCV rv)) rtp bs r ctx diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Panic.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Panic.hs new file mode 100644 index 000000000..f7d5f8fc2 --- /dev/null +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Panic.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE TemplateHaskell #-} +module Data.Macaw.RISCV.Symbolic.Panic ( + P.panic, + Component(..) + ) where + +import qualified Panic as P + +data Component = RISCV + 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/Repeat.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Repeat.hs new file mode 100644 index 000000000..9c7359d0e --- /dev/null +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Repeat.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Macaw.RISCV.Symbolic.Repeat ( + CtxRepeat, + RepeatAssign(..) + ) where + +import GHC.TypeLits +import qualified Data.Parameterized.Context as Ctx + +type family CtxRepeat (n :: Nat) (c :: k) :: Ctx.Ctx k where + CtxRepeat 0 c = Ctx.EmptyCtx + CtxRepeat n c = CtxRepeat (n - 1) c Ctx.::> c + +class RepeatAssign (tp :: k) (ctx :: Ctx.Ctx k) where + repeatAssign :: (Int -> f tp) -> Ctx.Assignment f ctx + +instance RepeatAssign tp Ctx.EmptyCtx where + repeatAssign _ = Ctx.Empty + +instance RepeatAssign tp ctx => RepeatAssign tp (ctx Ctx.::> tp) where + repeatAssign f = + let r = repeatAssign f + in r Ctx.:> f (Ctx.sizeInt (Ctx.size r)) diff --git a/macaw-riscv-symbolic/tests/Main.hs b/macaw-riscv-symbolic/tests/Main.hs new file mode 100644 index 000000000..f6b9ad542 --- /dev/null +++ b/macaw-riscv-symbolic/tests/Main.hs @@ -0,0 +1,218 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +module Main (main) where + +import Control.Lens ( (^.) ) +import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BS8 +import qualified Data.ElfEdit as Elf +import qualified Data.Foldable as F +import qualified Data.Map as Map +import Data.Maybe ( mapMaybe ) +import qualified Data.Parameterized.Classes as PC +import qualified Data.Parameterized.Nonce as PN +import Data.Parameterized.Some ( Some(..) ) +import Data.Proxy ( Proxy(..) ) +import GHC.TypeNats ( KnownNat, type (<=) ) +import qualified Prettyprinter as PP +import System.FilePath ( (), (<.>) ) +import qualified System.FilePath.Glob as SFG +import qualified System.IO as IO +import qualified Test.Tasty as TT +import qualified Test.Tasty.HUnit as TTH +import qualified Test.Tasty.Options as TTO +import qualified Test.Tasty.Runners as TTR + +import qualified Data.Macaw.Architecture.Info as MAI +import qualified Data.Macaw.CFG as MC +import qualified Data.Macaw.Discovery as M +import qualified Data.Macaw.Memory.ElfLoader.PLTStubs as MMELP +import qualified Data.Macaw.Symbolic as MS +import qualified Data.Macaw.Symbolic.Testing as MST +import qualified Data.Macaw.RISCV as MR +import Data.Macaw.RISCV.Symbolic () +import qualified GRIFT.Types as G +import qualified What4.Config as WC +import qualified What4.Expr.Builder as WEB +import qualified What4.Interface as WI +import qualified What4.ProblemFeatures as WPF +import qualified What4.Solver as WS + +import qualified Lang.Crucible.Backend as CB +import qualified Lang.Crucible.Backend.Online as CBO +import qualified Lang.Crucible.Simulator as CS +import qualified Lang.Crucible.LLVM.MemModel as LLVM + +-- | A Tasty option to tell us to save SMT queries and responses to /tmp for debugging purposes +data SaveSMT = SaveSMT Bool + deriving (Eq, Show) + +instance TTO.IsOption SaveSMT where + defaultValue = SaveSMT False + parseValue v = SaveSMT <$> TTO.safeReadBool v + optionName = pure "save-smt" + optionHelp = pure "Save SMT sessions to files in /tmp for debugging" + +-- | A tasty option to have the test suite save the macaw IR for each test case to /tmp for debugging purposes +data SaveMacaw = SaveMacaw Bool + +instance TTO.IsOption SaveMacaw where + defaultValue = SaveMacaw False + parseValue v = SaveMacaw <$> TTO.safeReadBool v + optionName = pure "save-macaw" + optionHelp = pure "Save Macaw IR for each test case to /tmp for debugging" + +ingredients :: [TTR.Ingredient] +ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT) + , TTO.Option (Proxy @SaveMacaw) + ] : TT.defaultIngredients + +main :: IO () +main = do + -- These are pass/fail in that the assertions in the "pass" set are true (and + -- the solver returns Unsat), while the assertions in the "fail" set are false + -- (and the solver returns Sat). + passTestFilePaths <- SFG.glob "tests/pass/**/*.exe" + failTestFilePaths <- SFG.glob "tests/fail/**/*.exe" + let passRes = MST.SimulationResult MST.Unsat + let failRes = MST.SimulationResult MST.Sat + let passTests mmPreset = TT.testGroup "True assertions" (map (mkSymExTest passRes mmPreset) passTestFilePaths) + let failTests mmPreset = TT.testGroup "False assertions" (map (mkSymExTest failRes mmPreset) failTestFilePaths) + TT.defaultMainWithIngredients ingredients $ + TT.testGroup "Binary Tests" $ + map (\mmPreset -> + TT.testGroup (MST.describeMemModelPreset mmPreset) + [passTests mmPreset, failTests mmPreset]) + [MST.DefaultMemModel, MST.LazyMemModel] + +hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch)) +hasTestPrefix (Some dfi) = do + bsname <- M.discoveredFunSymbol dfi + if BS8.pack "test_" `BS8.isPrefixOf` bsname + then return (bsname, Some dfi) + else Nothing + +-- | RISC-V functions with a single scalar return value return it in @a0@. +-- +-- Since all test functions must return a value to assert as true, this is +-- straightforward to extract. +riscvResultExtractor :: ( arch ~ MR.RISCV rv + , CB.IsSymInterface sym + , MC.ArchConstraints arch + , MS.ArchInfo arch + , KnownNat (G.RVWidth rv) + ) + => MS.ArchVals arch + -> MST.ResultExtractor sym arch +riscvResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do + let re = MS.lookupReg archVals regs MR.GPR_A0 + k PC.knownRepr (CS.regValue re) + +mkSymExTest :: MST.SimulationResult -> MST.MemModelPreset -> FilePath -> TT.TestTree +mkSymExTest expected mmPreset exePath = TT.askOption $ \saveSMT@(SaveSMT _) -> TT.askOption $ \saveMacaw@(SaveMacaw _) -> TTH.testCaseSteps exePath $ \step -> do + bytes <- BS.readFile exePath + case Elf.decodeElfHeaderInfo bytes of + Left (_, msg) -> TTH.assertFailure ("Error parsing ELF header from file '" ++ show exePath ++ "': " ++ msg) + Right (Elf.SomeElf ehi) -> do + case Elf.headerClass (Elf.header ehi) of + Elf.ELFCLASS32 -> + symExTestSized expected mmPreset exePath saveSMT saveMacaw step ehi (MR.riscv_info G.rv32GCRepr) + Elf.ELFCLASS64 -> + symExTestSized expected mmPreset exePath saveSMT saveMacaw step ehi (MR.riscv_info G.rv64GCRepr) + +data MacawRISCVSymbolicData t = MacawRISCVSymbolicData + +symExTestSized :: forall rv w arch + . ( w ~ G.RVWidth rv + , 16 <= w + , MC.ArchConstraints arch + , arch ~ MR.RISCV rv + , KnownNat w + , Show (Elf.ElfWordType w) + , MS.ArchInfo arch + ) + => MST.SimulationResult + -> MST.MemModelPreset + -> FilePath + -> SaveSMT + -> SaveMacaw + -> (String -> IO ()) + -> Elf.ElfHeaderInfo w + -> MAI.ArchitectureInfo arch + -> TTH.Assertion +symExTestSized expected mmPreset exePath saveSMT saveMacaw step ehi archInfo = do + binfo <- MST.runDiscovery ehi exePath MST.toAddrSymMap archInfo + -- Test cases involving shared libraries are not + -- yet supported on the RISC-V backend. At a + -- minimum, this is blocked on + -- https://github.com/GaloisInc/elf-edit/issues/36. + (MMELP.noPLTStubInfo "RISC-V") + let funInfos = Map.elems (MST.binaryDiscState (MST.mainBinaryInfo binfo) ^. M.funInfo) + let testEntryPoints = mapMaybe hasTestPrefix funInfos + F.forM_ testEntryPoints $ \(name, Some dfi) -> do + step ("Testing " ++ BS8.unpack name ++ " at " ++ show (M.discoveredFunAddr dfi)) + writeMacawIR saveMacaw (BS8.unpack name) dfi + Some (gen :: PN.NonceGenerator IO t) <- PN.newIONonceGenerator + sym <- WEB.newExprBuilder WEB.FloatRealRepr MacawRISCVSymbolicData gen + CBO.withYicesOnlineBackend sym CBO.NoUnsatFeatures WPF.noFeatures $ \bak -> do + -- We are using the z3 backend to discharge proof obligations, so + -- we need to add its options to the backend configuration + let solver = WS.z3Adapter + let backendConf = WI.getConfiguration sym + WC.extendConfig (WS.solver_adapter_config_options solver) backendConf + + execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend bak) + archVals <- case MS.archVals (Proxy @(MR.RISCV rv)) Nothing of + Just archVals -> pure archVals + Nothing -> error "symExTestSized: impossible" + let extract = riscvResultExtractor archVals + logger <- makeGoalLogger saveSMT solver name exePath + let ?memOpts = LLVM.defaultMemOptions + simRes <- MST.simulateAndVerify solver logger bak execFeatures archInfo archVals binfo mmPreset extract dfi + TTH.assertEqual "AssertionResult" expected simRes + +writeMacawIR :: (MC.ArchConstraints arch) => SaveMacaw -> String -> M.DiscoveryFunInfo arch ids -> IO () +writeMacawIR (SaveMacaw sm) name dfi + | not sm = return () + | otherwise = writeFile (toSavedMacawPath name) (show (PP.pretty dfi)) + +toSavedMacawPath :: String -> FilePath +toSavedMacawPath testName = "/tmp" name <.> "macaw" + where + name = fmap escapeSlash testName + +-- | Construct a solver logger that saves the SMT session for the goal solving +-- in /tmp (if requested by the save-smt option) +-- +-- The adapter name is included so that, if the same test is solved with +-- multiple solvers, we can differentiate them. +makeGoalLogger :: SaveSMT -> WS.SolverAdapter st -> BS8.ByteString -> FilePath -> IO WS.LogData +makeGoalLogger (SaveSMT saveSMT) adapter funName p + | not saveSMT = return WS.defaultLogData + | otherwise = do + hdl <- IO.openFile (toSavedSMTSessionPath adapter funName p) IO.WriteMode + return (WS.defaultLogData { WS.logHandle = Just hdl }) + + +-- | Construct a path in /tmp to save the SMT session to +-- +-- Just take the original path name and turn all of the slashes into underscores to escape them +toSavedSMTSessionPath :: WS.SolverAdapter st -> BS8.ByteString -> FilePath -> FilePath +toSavedSMTSessionPath adapter funName p = "/tmp" filename <.> "smtlib2" + where + filename = concat [ fmap escapeSlash p + , "_" + , BS8.unpack funName + , "_" + , WS.solver_adapter_name adapter + ] + +escapeSlash :: Char -> Char +escapeSlash '/' = '_' +escapeSlash c = c diff --git a/macaw-riscv-symbolic/tests/README.org b/macaw-riscv-symbolic/tests/README.org new file mode 100644 index 000000000..836a5a7b9 --- /dev/null +++ b/macaw-riscv-symbolic/tests/README.org @@ -0,0 +1,18 @@ +* Overview +This test suite tests that symbolic execution of RISC-V programs works. It is also a convenient place to test the semantics. The test harness looks for binaries in the ~pass~ and ~fail~ subdirectories. In both cases, it enumerates the functions whose names are prefixed by ~test_~, each of which are symbolically executed with fully symbolic initial states. It treats the return value of each test function as an assertion that it will attempt to prove (i.e., it checks the satisfiability of the assertion). Test cases in ~pass~ are expected to return a value that is always true, while the test cases in ~fail~ are expected to not always be true (but note that the precise models are not inspected). The test harness uses yices for path satisfiability checking and z3 to prove goals. Since path satisfiability checking is enabled, test cases can include loops as long as they symbolically terminate. + +In addition to proving that the result of a test case is always true (or not), the test harness will attempt to prove all generated side conditions for tests with names prefixed by ~test_and_verify_~. In both the ~pass~ and ~fail~ directories, these side conditions are expected to pass (or they will cause test failures). + +* Usage + +The test runner has two command line options (beyond the defaults for tasty): + +- ~--save-macaw~: Saves the Macaw IR for each test case to /tmp for debugging purposes +- ~--save-smt~: Saves the generated SMTLib for each test to /tmp for debugging purposes + + +* Limitations +- It currently tests both optimized an unoptimized binaries. It is intended that this set will expand and that a wide variety of compilers will be tested. +- Only two solvers are involved in the test, rather than a whole matrix +- Function calls are not supported in test cases +- There are no facilities for generating symbolic data beyond the initial symbolic arguments to each function diff --git a/macaw-riscv-symbolic/tests/fail/Makefile b/macaw-riscv-symbolic/tests/fail/Makefile new file mode 100644 index 000000000..c6ec3a4d2 --- /dev/null +++ b/macaw-riscv-symbolic/tests/fail/Makefile @@ -0,0 +1,23 @@ +# These binaries were obtained from https://musl.cc/ +CC64=riscv64-linux-musl-gcc +CC32=riscv32-linux-musl-gcc +CFLAGS=-nostdlib -no-pie -static -fno-stack-protector + +unopt32 = $(patsubst %.c,%.unopt32.exe,$(wildcard *.c)) +unopt64 = $(patsubst %.c,%.unopt64.exe,$(wildcard *.c)) +opt32 = $(patsubst %.c,%.opt32.exe,$(wildcard *.c)) +opt64 = $(patsubst %.c,%.opt64.exe,$(wildcard *.c)) + +all: $(unopt32) $(opt32) $(unopt64) $(opt64) + +%.unopt32.exe : %.c + $(CC32) $(CFLAGS) -O0 $< -o $@ + +%.opt32.exe : %.c + $(CC32) $(CFLAGS) -O2 $< -o $@ + +%.unopt64.exe : %.c + $(CC64) $(CFLAGS) -O0 $< -o $@ + +%.opt64.exe : %.c + $(CC64) $(CFLAGS) -O2 $< -o $@ diff --git a/macaw-riscv-symbolic/tests/fail/constant.c b/macaw-riscv-symbolic/tests/fail/constant.c new file mode 100644 index 000000000..6b5610e3f --- /dev/null +++ b/macaw-riscv-symbolic/tests/fail/constant.c @@ -0,0 +1,16 @@ +// This test fails because x is not always 1 +int __attribute__((noinline)) test_constant(int x) { + return x == 1; +} + +// Notes: +// +// - The entry point is required by the compiler to make an executable +// +// - We can't put the test directly in _start because macaw-symbolic (and macaw +// in general) don't deal well with system calls +// +// - The test harness only looks for function symbols starting with test_ +void _start() { + test_constant(0); +} diff --git a/macaw-riscv-symbolic/tests/fail/constant.opt32.exe b/macaw-riscv-symbolic/tests/fail/constant.opt32.exe new file mode 100755 index 0000000000000000000000000000000000000000..c339ac8761b1e4c64b24983ed4d435fdf1063bab GIT binary patch literal 760 zcma)4O-sW-5S_HORPj)if*?o)4^<>IpB$ zHn9uQve?~XUqm_j{9eWUcym5m1m6ai{sQtk@`30@ts8U!F8_^Rp6SQPlZ1Yn^7m5Q zOYyr@KY3vgvm3DGky6*guNIC{ zKaLeviWu{MZT`Szmy{pi2CVpT#BLv%qj|p375fiNmKTmje!$q~zhetdIWf6QIZJ6? z0d&aON$ddP(-$f4Lwa?HrlEU8dj;NrTmtfDmVqpwV~FNZ6J%LSVhu?8-XZMIl=+~2 EKeJ#|V*mgE literal 0 HcmV?d00001 diff --git a/macaw-riscv-symbolic/tests/fail/constant.opt64.exe b/macaw-riscv-symbolic/tests/fail/constant.opt64.exe new file mode 100755 index 0000000000000000000000000000000000000000..555f82f3ebb495816ce09613515d3007bb297efb GIT binary patch literal 1072 zcmb_a%}T>S5T2&3sCbAF4=NIxfKbFkf31QRr1iX{Y4C?Ok!BBikd{7CkJ6Km z;S2Zx;sfYxvP09w(2E1vZ}!`7zTM5vsBv|!rBXnl!8eH6TQ~xg<-$~pk}N_QN}%Dm z0@+X{xOtFQgfqE72zo@^eDdDPyl81A%iuM)eUgL8crtF*YNv&RX6yE_V48+ym<6k7 znWkwKmzkyU)KhuCxHgTqQbXJ#17ANXzk!5~{47uRjTE~GTQUDtS$G`kQ!vvP_198Q z|C>&5CiU-%{vyGrlfXL({9}SYIKCHf+vA1G+9W!!z{U^xC@ z;CdX7`!BJBF5(5K_oxr1(tTaoh2DecJxoNs+GNzTg*E&Kqh zU}fVE1hEoZKfn(V3o9SzCJx4}ym02;Gw0md*_k=ct}Y27NJog?h}k8^N#w~8Q441> zC`2O^1^ab#C8&y#!9I!+t-q)(E`t%p1Y{ENeGhIh8?Dj<2M4Krdv{8)>z5!a^X14$U literal 0 HcmV?d00001 diff --git a/macaw-riscv-symbolic/tests/fail/constant.unopt64.exe b/macaw-riscv-symbolic/tests/fail/constant.unopt64.exe new file mode 100755 index 0000000000000000000000000000000000000000..2f6f082a4e92d6c2303bf3cfbc365153b82896cf GIT binary patch literal 1128 zcmb<-^>JfjWMqH=CWg-pAl@A?$-v+Mm3YAfVXy)z2L=lUCLqbizzS9c5<>u(SrGaQ zR02jb2tWh^pO&PsAv6(WLA5b33M#!}5Lnf&toG$!v-**L((UXFt?rxIzdKCcF3vFd z`*;3Eb-UK26xPJ121h}*CrS?(I2c{uf7t(rkzr8+Q;H*FQ-iy+vz3B|yI-iLf}x?F zk)EM~k%5t+p`noherGTPeY*h~F32jGfuVs8K)z>T`1l`PoChc%02Kcs0ShOH3OOJp zgk-)BR3nHM0E&MRKvnMxRS%0N38;D-sQMph>OF9n6M{oL8Hacl4)Yn3^Ye;J67x#* zk{ROT({u8Z5_94U@-y>FQj1g=N>YnU;$bR)^1&{SA&&7*uI`?G@$o>uQ*dy+tDg&) zom5;L4>YN$1SpQGEHx#uB#|LLH7|vML9e(nw@GGPyS|{_T}zS)`GoFA_GvT0+jGh_c8fvMEIc%7Ja%Qdu;^ zDi9y#iS9qRD`hfr*nmt~f4NvL>ecFnU8px6PHoq9Jjb=YqUXAUYBt_j&4c$e71L)D8ybIqHu%9G?(}F&lM2Z`R7KvZ?s>n}#vqm1fiUjoPYi$FYey z7&G?&+QM$Y0hw@w(|6+Okb^cdkJq`U6^9chrxOi_mS5T2$#D0qmT3W8Mdpdz8ksfdUE#VTk)TF*<`1g*4XsYOX1p$Zkya4bMR zR4Hy9>=ogP78pT~h`SHz7S=_7W>f}wdof?kTaCtf>A2OtKPj1}VHsx0DqE&$TID~D zP>{t_FX?`9eHL$(40Vefe10eS9VB$*S4F;Wq&Ps>i}~lM@GR74V5M*BZ%NPpn@?~- z`nQDsD#fRp!uM17rxbq}xZYR}J??`gxiin3@q6(65EE6OY&7m~Otxhty?#YIl?wYC|nwhyM?rjSpNJoG^h}kvP4019+6h_WaoC1`j z2-vTiD?xp%4E9l!=-^G&xb#N^8<0uF5-${8Si1Y_S)091A#7h=W@C}3#3PM~;`5rI z`>jMFE3PiBe11Kiv`Rgd(^(|txJqgV^l~A4n3cJrwOf)BJXbEuVyQ5wE3PYDWp@Pvx}Bh}6;m+ivF#!70wP&`~n>AIHD^i*a!qw9KRdEkO5h~Vk&={tn= z5j?#d-f4&6{afZokVqik85iFrP)s6>hWy8CaofO#5C2*jVAsB&p#aEw! + +unsigned int __attribute__((noinline)) test_saturate_add(unsigned int x, unsigned int y) { + unsigned int c = x + y; + if(c < x || c < y) + c = UINT_MAX; + + return c >= x && c >= y; +} + +void _start() { + test_saturate_add(1, 2); +} diff --git a/macaw-riscv-symbolic/tests/pass/saturate-add.opt32.exe b/macaw-riscv-symbolic/tests/pass/saturate-add.opt32.exe new file mode 100755 index 0000000000000000000000000000000000000000..a51069ee7ac11a52f78935e60250aa2632223707 GIT binary patch literal 764 zcma)4%Syvg5S{b|f{W@(a1+Hv6%0-2%3a&UB1lnccf#ei30CYwk`ZeWEd2^U%Rg}C z2Z$e_XId|fSvhd-nR91Oa&spy!TG6WS!5zdUnFXZwFchI5f#BTvMEOuDnYHgC9`OT zRUmy-Cc6CKP||Fauz@lagT;I?Z#A1IcBR$s9@?(!c#dm(RnK)@ubTB4&A)HXr%oWX zJWjSg6H$RazvVr%oz-p`dS7(eXp1~(d0qj$4eo;FoAJ3z?Sr3F{TI+_|8+*+WpteJ zQ=<7H)*Kz{Fm(E))Xi|x(?fMXxgB#9A7H2B*RSfT5wyp|(HK*3lBW^t9+=}54@}0@9d6vW$knVd&;b>V| HEvD}WK$TXg literal 0 HcmV?d00001 diff --git a/macaw-riscv-symbolic/tests/pass/saturate-add.opt64.exe b/macaw-riscv-symbolic/tests/pass/saturate-add.opt64.exe new file mode 100755 index 0000000000000000000000000000000000000000..a854f02c9e11af431680956dd18c216d2edc9fdb GIT binary patch literal 1080 zcmb_a%SyvQ6unI!=q|b{xT)eo1w)fnan)BWf)u58Ck)djsMv=jBkIc1jla`{lzxgo z;0K5wpm&;kX&Nluc%eBrXU;h@)7)40{M1OLfXjey&~NYaCqS7NW=7Ox5z0^k1D`p_ z&Q+RQ6lX;^r3FSXBjWN?dAWsYZAUi9y5rG!)Tq@?3I~m5`>&idQtZw76im%!-a&plwr?hqLz{U1zxf1p z%9$l{E{IR&U$5ZrSMb4#dt0mlK9an|ugrNwP3>5ZDM&Wx>Nf7?P1F*uEzLFh86-0Q;o${X* zSlwa2?++9n`(J7YQ}h?&8RU7GP&)Ix8Gjdk-^E7zlLN+{bGmSx(eRj|ix%d+h83L?0g!r)1ZORp~+Wpv3e()5TMy)(o78S>xsS82M50%he0$os48V%vpYp4p*3_}qr z87RaL8inskB}w=lyt)}~wUulFRS@Blj+DQt$ZU1nZNH;%-2b*GQ1T@C|L_dCc@wS; zU-Z_7v9eA-C;v(A)y6gLx`%5+Nd5p0#GK#r5j+jo_8YnlO@O=?TMi!Ay~XA)ZY$BE Gb^ic&jE=bg literal 0 HcmV?d00001 diff --git a/macaw-riscv-symbolic/tests/pass/saturate-add.unopt64.exe b/macaw-riscv-symbolic/tests/pass/saturate-add.unopt64.exe new file mode 100755 index 0000000000000000000000000000000000000000..057a87e0eacfb6a8404723378b091df5f3babde4 GIT binary patch literal 1224 zcmb`Hzi-n(6vv;FCMsLPLQ9vBAPfks+Ec_(nl{EoilU-Wu^=6n*rKTUQS7VQPBdw& zi2nhJsv}cZI`5gQ>Bm+&KKXAo4iQ6awOAW`+c?tQ(wA9H)r(D zj=Q->y|Z2YWH8s=)%ONpKj-fC&T)Ru=O+VAZ|k+SJ}9y$$VMLquP$*m{&Bi}*mu$g zZKtiz?Pr-yJ3EDR@>}*4CO_H<`^V3xeGLxZ#N2|`*>M&ZpJeVk<&_5+(=;r@%viIQ zX`0sT{~s@oT|63ga?}^cE=Pm6a{_+-iE`eb6!Oxv>c4Pghg^eFdX!tpZ-%bh5q4OS zT)qF>k{3}^=wFW1S(ZFn|MeKYHir9S>O(-;hEJLIn7Xb}147=`TUA;o>#cW9=J|J# zREmX{1+ri}&&z}W^8!Xx7QrlZEL1AQE*Ei?kZKT+fKi{}cqEZ{E@c#m*K`4lV7tL+ z6_xoySJjAlTMUd^tI_b93~&2dVg{@5H>AD^wI7aT^-qzjM0ds=nIGM1>bv9h!=ZLV zSfe$$e^natQYVn{W0EgoObLM-sPY#fiI4+XbaRA?XAPq?PA<#8CE>%c8OQ3r75)o% CXqf;2 literal 0 HcmV?d00001 diff --git a/macaw-riscv/src/Data/Macaw/RISCV.hs b/macaw-riscv/src/Data/Macaw/RISCV.hs index 3b38e5707..acac56287 100644 --- a/macaw-riscv/src/Data/Macaw/RISCV.hs +++ b/macaw-riscv/src/Data/Macaw/RISCV.hs @@ -15,11 +15,12 @@ module Data.Macaw.RISCV ( -- * Type-level tags G.RV(..), G.RVRepr(..), + RISCV, + RISCVConstraints, -- * RISC-V Types - RISCVReg(..), RISCVTermStmt, RISCVStmt, - RISCVPrimFn + RISCVPrimFn(..) ) where import GHC.Stack (HasCallStack) diff --git a/macaw-riscv/src/Data/Macaw/RISCV/Arch.hs b/macaw-riscv/src/Data/Macaw/RISCV/Arch.hs index 3c9697dde..83a09d192 100644 --- a/macaw-riscv/src/Data/Macaw/RISCV/Arch.hs +++ b/macaw-riscv/src/Data/Macaw/RISCV/Arch.hs @@ -104,9 +104,15 @@ type instance MC.ArchFn (RISCV rv) = RISCVPrimFn rv -- | RISC-V architecture-specific statements (none) data RISCVStmt (rv :: G.RV) (expr :: MT.Type -> K.Type) +instance F.FunctorF (RISCVStmt rv) where + fmapF _ s = case s of {} + instance F.FoldableF (RISCVStmt rv) where foldMapF _ s = case s of {} +instance F.TraversableF (RISCVStmt rv) where + traverseF _ s = pure (case s of {}) + instance MC.IsArchStmt (RISCVStmt rv) where ppArchStmt _ s = case s of {} @@ -115,6 +121,15 @@ type instance MC.ArchStmt (RISCV rv) = RISCVStmt rv -- | RISC-V block termination statements (none) data RISCVTermStmt (rv :: G.RV) (f :: MT.Type -> K.Type) +instance F.FunctorF (RISCVTermStmt rv) where + fmapF _ s = case s of {} + +instance F.FoldableF (RISCVTermStmt rv) where + foldMapF _ s = case s of {} + +instance F.TraversableF (RISCVTermStmt rv) where + traverseF _ s = pure (case s of {}) + instance MC.PrettyF (RISCVTermStmt rv) where prettyF s = case s of {} diff --git a/macaw-riscv/src/Data/Macaw/RISCV/RISCVReg.hs b/macaw-riscv/src/Data/Macaw/RISCV/RISCVReg.hs index 4c6e811fc..3ab159e19 100644 --- a/macaw-riscv/src/Data/Macaw/RISCV/RISCVReg.hs +++ b/macaw-riscv/src/Data/Macaw/RISCV/RISCVReg.hs @@ -15,6 +15,7 @@ module Data.Macaw.RISCV.RISCVReg ( -- * RISC-V macaw register state RISCVReg(..) + , GPR(..) -- ** Patterns for GPRs , pattern GPR , pattern GPR_RA @@ -62,6 +63,8 @@ import Data.Parameterized.TH.GADT ( structuralTypeEquality , structuralTypeOrd ) +import qualified Prettyprinter as PP + import qualified GRIFT.Types as G import qualified GRIFT.Semantics.Utils as G @@ -411,7 +414,7 @@ pattern GPR_T6 = GPR 31 instance Show (RISCVReg rv tp) where show PC = "pc" show (RISCV_GPR gpr) = show gpr - show (FPR rid) = "fpr[" <> show rid <> "]" + show (FPR rid) = "f" <> show (G.asUnsignedSized rid) show (CSR csr) = show csr show PrivLevel = "priv" show EXC = "exc" @@ -426,6 +429,9 @@ instance OrdF (RISCVReg rv) where instance ShowF (RISCVReg rv) +instance MC.PrettyF (RISCVReg rv) where + prettyF = PP.pretty . showF + instance G.KnownRV rv => MT.HasRepr (RISCVReg rv) MT.TypeRepr where typeRepr PC = MT.BVTypeRepr knownNat typeRepr (RISCV_GPR _) = MT.BVTypeRepr knownNat From dd7f170bac21cbb255c786dd2db84ceb3a213d82 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 26 Jul 2024 15:00:54 -0400 Subject: [PATCH 2/3] 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 a3b931186..0c129de85 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 ce0f1de1b..d41cd644c 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 000000000..93759a30b --- /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 66ae7f741..6c1a9b970 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 fb889f409..91b0b5a8e 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 24437d2fa..104ace92a 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 000000000..0fc17530c --- /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) From 5ee37cf553c9cf25dbf7d7097f088a7d381c84ae Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 26 Jul 2024 15:03:53 -0400 Subject: [PATCH 3/3] macaw-{ppc,riscv}-symbolic: Move S definition above functions that use it --- macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs | 4 ++-- .../src/Data/Macaw/RISCV/Symbolic/Functions.hs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs index 0fe40390c..c03fb5ace 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs @@ -62,6 +62,8 @@ data SemanticsError = NonUserSymbol String instance X.Exception SemanticsError +type S p v sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (SP.AnyPPC v)) rtp bs r ctx + termSemantics :: (C.IsSymInterface sym, 1 <= SP.AddrWidth v) => SymFuns sym -> MP.PPCTermStmt v ids @@ -409,5 +411,3 @@ withRounding withRounding bak r action = do r' <- toValBV bak r U.withRounding (C.backendGetSym bak) r' action - -type S p v sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (SP.AnyPPC v)) rtp bs r ctx diff --git a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs index 230c7a615..563f2402e 100644 --- a/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs +++ b/macaw-riscv-symbolic/src/Data/Macaw/RISCV/Symbolic/Functions.hs @@ -27,6 +27,8 @@ import qualified Data.Macaw.RISCV.Symbolic.Panic as RP data SymFuns sym = SymFuns +type S p rv sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (MR.RISCV rv)) rtp bs r ctx + funcSemantics :: SymFuns sym -> MR.RISCVPrimFn rv (RA.AtomWrapper f) mt -> S p rv sym rtp bs r ctx @@ -50,5 +52,3 @@ termSemantics :: SymFuns sym -> S p rv sym rtp bs r ctx -> IO (C.RegValue sym C.UnitType, S p rv sym rtp bs r ctx) termSemantics _fs term _s = case term of {} - -type S p rv sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (MR.RISCV rv)) rtp bs r ctx