diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 4e81b546..ba3452aa 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -111,6 +111,12 @@ jobs: if: runner.os == 'Linux' run: cabal test pkg:macaw-x86-symbolic + - name: Build macaw-cli + run: cabal build pkg:macaw-cli + + - name: Build macaw-x86-cli + run: cabal build pkg:macaw-x86-cli + - name: Build macaw-aarch32 run: cabal build pkg:macaw-aarch32 pkg:macaw-aarch32-symbolic - name: Test macaw-aarch32 diff --git a/cabal.project.dist b/cabal.project.dist index d72f6888..5133798e 100644 --- a/cabal.project.dist +++ b/cabal.project.dist @@ -1,10 +1,12 @@ packages: base/ macaw-aarch32/ macaw-aarch32-symbolic/ + macaw-cli/ macaw-semmc/ macaw-ppc/ macaw-ppc-symbolic/ macaw-riscv/ + macaw-x86-cli/ x86/ symbolic/ symbolic-syntax/ diff --git a/macaw-cli/CHANGELOG.md b/macaw-cli/CHANGELOG.md new file mode 100644 index 00000000..75dfb599 --- /dev/null +++ b/macaw-cli/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for macaw-x86-cli + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/macaw-cli/LICENSE b/macaw-cli/LICENSE new file mode 100644 index 00000000..a3ea82f7 --- /dev/null +++ b/macaw-cli/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2024, Langston Barrett + +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 Langston Barrett nor the names of other + 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-cli/macaw-cli.cabal b/macaw-cli/macaw-cli.cabal new file mode 100644 index 00000000..7a0d400f --- /dev/null +++ b/macaw-cli/macaw-cli.cabal @@ -0,0 +1,105 @@ +cabal-version: 3.0 +name: macaw-cli +version: 0.1.0.0 +homepage: https://github.com/GaloisInc/macaw +license: BSD-3-Clause +license-file: LICENSE +author: Langston Barrett +maintainer: langston@galois.com +build-type: Simple +extra-doc-files: CHANGELOG.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 + hs-source-dirs: src + build-depends: + base >=4.16, + bytestring, + containers, + lens, + text, + + -- first-party (alphabetical) + crucible, + crucible-llvm, + elf-edit, + macaw-base, + macaw-loader, + macaw-symbolic, + parameterized-utils, + what4 + exposed-modules: + Data.Macaw.CLI diff --git a/macaw-cli/src/Data/Macaw/CLI.hs b/macaw-cli/src/Data/Macaw/CLI.hs new file mode 100644 index 00000000..668141c5 --- /dev/null +++ b/macaw-cli/src/Data/Macaw/CLI.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Macaw.CLI + ( sim + ) where + +import Control.Lens qualified as Lens +import Control.Monad qualified as Monad +import Data.ByteString.Char8 qualified as BS8 +import Data.Map qualified as Map +import Data.Text (Text) +import Data.Text qualified as Text +import GHC.TypeLits (KnownNat) + +-- First-party +import Data.ElfEdit qualified as Elf +import Data.Macaw.Architecture.Info qualified as MAI +import Data.Macaw.CFG qualified as MCFG +import Data.Macaw.Discovery qualified as MD +import Data.Macaw.Memory.ElfLoader.PLTStubs qualified as MPLT +import Data.Macaw.Symbolic qualified as MS +import Data.Macaw.Symbolic.Testing qualified as MST +import Data.Parameterized.NatRepr qualified as PNat +import Data.Parameterized.Nonce qualified as PN +import Data.Parameterized.Some qualified as Some +import Lang.Crucible.Backend qualified as CB +import Lang.Crucible.Backend.Online qualified as CBO +import Lang.Crucible.CFG.Extension qualified as CCE +import Lang.Crucible.LLVM.MemModel qualified as LLVM +import What4.Expr.Builder qualified as WEB +import What4.ProblemFeatures qualified as WPF +import What4.Solver qualified as WS +import What4.Solver.Yices qualified as WSY + +data MacawCLI t = MacawCLI + +sim :: + (1 PNat.<= MCFG.ArchAddrWidth arch) => + (16 PNat.<= MCFG.ArchAddrWidth arch) => + MCFG.MemWidth (MCFG.ArchAddrWidth arch) => + CCE.IsSyntaxExtension (MS.MacawExt arch) => + KnownNat (MCFG.ArchAddrWidth arch) => + (Elf.RelocationWidth reloc ~ MCFG.ArchAddrWidth arch) => + Elf.IsRelocationType reloc => + MAI.ArchitectureInfo arch -> + MS.GenArchVals MS.LLVMMemory arch -> + MPLT.PLTStubInfo reloc -> + (forall sym. CB.IsSymInterface sym => MST.ResultExtractor sym arch) -> + FilePath -> + Elf.ElfHeaderInfo (MD.ArchAddrWidth arch) -> + Text -> + IO () +sim archInfo archVals pltStubInfo extractor binPath elfHeaderInfo entryFn = do + Some.Some nonceGen <- PN.newIONonceGenerator + binfo <- MST.runDiscovery elfHeaderInfo binPath MST.toAddrSymMap archInfo pltStubInfo + let discState = MST.binaryDiscState (MST.mainBinaryInfo binfo) + let funInfos = Map.elems (discState Lens.^. MD.funInfo) + let entryFn8 = BS8.pack (Text.unpack entryFn) + Monad.forM_ funInfos $ \(Some.Some dfi) -> do + case MD.discoveredFunSymbol dfi of + Just funSymb | entryFn8 `BS8.isPrefixOf` funSymb -> do + let floatMode = WEB.FloatRealRepr -- TODO: make configurable via cli + sym <- WEB.newExprBuilder floatMode MacawCLI nonceGen + -- TODO: make solver configurable via cli + CBO.withYicesOnlineBackend sym CBO.NoUnsatFeatures WPF.noFeatures $ \bak -> do + let solver = WSY.yicesAdapter + execFeatures <- MST.defaultExecFeatures (MST.SomeOnlineBackend bak) + let ?memOpts = LLVM.defaultMemOptions + let mmPreset = MST.DefaultMemModel -- TODO: make configurable via cli + simRes <- MST.simulateAndVerify solver WS.defaultLogData bak execFeatures archInfo archVals binfo mmPreset extractor dfi + case simRes of + MST.SimulationAborted -> putStrLn "Aborted!" + MST.SimulationTimeout -> putStrLn "Timeout!" + MST.SimulationPartial -> putStrLn "Partial!" -- TODO: ??? + MST.SimulationResult MST.Unsat -> putStrLn "Always returns 0" + MST.SimulationResult MST.Sat -> putStrLn "May return non-zero" + MST.SimulationResult MST.Unknown -> putStrLn "Solver returned unknown!" + _ -> pure () diff --git a/macaw-x86-cli/CHANGELOG.md b/macaw-x86-cli/CHANGELOG.md new file mode 100644 index 00000000..75dfb599 --- /dev/null +++ b/macaw-x86-cli/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for macaw-x86-cli + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/macaw-x86-cli/LICENSE b/macaw-x86-cli/LICENSE new file mode 100644 index 00000000..a3ea82f7 --- /dev/null +++ b/macaw-x86-cli/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2024, Langston Barrett + +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 Langston Barrett nor the names of other + 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-x86-cli/app/Main.hs b/macaw-x86-cli/app/Main.hs new file mode 100644 index 00000000..fd4d74f8 --- /dev/null +++ b/macaw-x86-cli/app/Main.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE TypeApplications #-} + +module Main where + +import Data.ByteString qualified as BS +import Data.List qualified as List +import Data.Proxy qualified as Proxy +import Data.Text (Text) +import Data.Text qualified as Text +import System.Exit qualified as Exit + +-- First-party +import Data.ElfEdit qualified as Elf +import Data.Macaw.CLI qualified as MCLI +import Data.Macaw.Symbolic qualified as MS +import Data.Macaw.Symbolic.Testing qualified as MST +import Data.Macaw.X86 qualified as X86 +import Data.Macaw.X86.Symbolic () +import Data.Parameterized.Classes qualified as PC +import Lang.Crucible.Backend qualified as CB +import Lang.Crucible.Simulator.RegMap qualified as CSRM + +bail :: String -> IO a +bail msg = do + putStrLn msg + Exit.exitFailure + +x86ResultExtractor :: + CB.IsSymInterface sym => + MS.ArchVals X86.X86_64 -> + MST.ResultExtractor sym X86.X86_64 +x86ResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do + let re = MS.lookupReg archVals regs X86.RAX + k PC.knownRepr (CSRM.regValue re) + +simX86_64 :: + FilePath -> + Elf.ElfHeaderInfo 64 -> + Text -> + IO () +simX86_64 binPath elfHeaderInfo entryFn = do + archVals <- case MS.archVals (Proxy.Proxy @X86.X86_64) Nothing of + Just archVals -> pure archVals + Nothing -> bail "Internal error: no archVals?" + MCLI.sim X86.x86_64_linux_info archVals X86.x86_64PLTStubInfo (x86ResultExtractor archVals) binPath elfHeaderInfo entryFn + +simFile :: + FilePath -> + Text -> + IO () +simFile binPath entryFn = do + bs <- BS.readFile binPath + case Elf.decodeElfHeaderInfo bs of + Right (Elf.SomeElf hdr) -> + case (Elf.headerClass (Elf.header hdr), Elf.headerMachine (Elf.header hdr)) of + (Elf.ELFCLASS64, Elf.EM_X86_64) -> simX86_64 binPath hdr entryFn + (_, mach) -> bail ("User error: unexpected ELF architecture: " List.++ show mach) + Left _ -> + bail ("User error: expected x86_64 ELF binary, but found non-ELF file at " List.++ binPath) + +-- TODO: CLI +main :: IO () +main = simFile "test.exe" (Text.pack "entry") + diff --git a/macaw-x86-cli/macaw-x86-cli.cabal b/macaw-x86-cli/macaw-x86-cli.cabal new file mode 100644 index 00000000..80732f70 --- /dev/null +++ b/macaw-x86-cli/macaw-x86-cli.cabal @@ -0,0 +1,110 @@ +cabal-version: 3.0 +name: macaw-x86-cli +version: 0.1.0.0 +homepage: https://github.com/GaloisInc/macaw +license: BSD-3-Clause +license-file: LICENSE +author: Langston Barrett +maintainer: langston@galois.com +build-type: Simple +extra-doc-files: CHANGELOG.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 + +executable macaw-x86-cli + import: shared + hs-source-dirs: app + main-is: Main.hs + -- other-modules: + -- other-extensions: + build-depends: + base >=4.16, + bytestring, + containers, + lens, + text, + + -- first-party (alphabetical) + crucible, + crucible-llvm, + elf-edit, + macaw-base, + macaw-cli, + macaw-loader, + macaw-loader-x86, + macaw-symbolic, + macaw-x86, + macaw-x86-symbolic, + parameterized-utils, + what4