From 2e7aab050dd32f1c2b59d1a4ded646ba7bddf873 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 3 Jul 2024 15:04:15 -0400 Subject: [PATCH 1/6] Simple CLI for macaw-symbolic --- .github/workflows/ci.yaml | 6 ++ cabal.project.dist | 2 + macaw-cli/CHANGELOG.md | 5 ++ macaw-cli/LICENSE | 30 ++++++++ macaw-cli/macaw-cli.cabal | 105 ++++++++++++++++++++++++++++ macaw-cli/src/Data/Macaw/CLI.hs | 85 +++++++++++++++++++++++ macaw-x86-cli/CHANGELOG.md | 5 ++ macaw-x86-cli/LICENSE | 30 ++++++++ macaw-x86-cli/app/Main.hs | 68 ++++++++++++++++++ macaw-x86-cli/macaw-x86-cli.cabal | 110 ++++++++++++++++++++++++++++++ 10 files changed, 446 insertions(+) create mode 100644 macaw-cli/CHANGELOG.md create mode 100644 macaw-cli/LICENSE create mode 100644 macaw-cli/macaw-cli.cabal create mode 100644 macaw-cli/src/Data/Macaw/CLI.hs create mode 100644 macaw-x86-cli/CHANGELOG.md create mode 100644 macaw-x86-cli/LICENSE create mode 100644 macaw-x86-cli/app/Main.hs create mode 100644 macaw-x86-cli/macaw-x86-cli.cabal 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 From e66a0ab7c32e7a0c4fc2998e60370c76e7442fda Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 3 Jul 2024 16:45:35 -0400 Subject: [PATCH 2/6] cli: Command-line options --- macaw-cli/macaw-cli.cabal | 2 ++ macaw-cli/src/Data/Macaw/CLI.hs | 9 ++++--- macaw-cli/src/Data/Macaw/CLI/Options.hs | 35 +++++++++++++++++++++++++ macaw-x86-cli/app/Main.hs | 20 +++++++------- 4 files changed, 51 insertions(+), 15 deletions(-) create mode 100644 macaw-cli/src/Data/Macaw/CLI/Options.hs diff --git a/macaw-cli/macaw-cli.cabal b/macaw-cli/macaw-cli.cabal index 7a0d400f..3c96e47f 100644 --- a/macaw-cli/macaw-cli.cabal +++ b/macaw-cli/macaw-cli.cabal @@ -90,6 +90,7 @@ library bytestring, containers, lens, + optparse-applicative, text, -- first-party (alphabetical) @@ -103,3 +104,4 @@ library what4 exposed-modules: Data.Macaw.CLI + Data.Macaw.CLI.Options diff --git a/macaw-cli/src/Data/Macaw/CLI.hs b/macaw-cli/src/Data/Macaw/CLI.hs index 668141c5..79d1fb85 100644 --- a/macaw-cli/src/Data/Macaw/CLI.hs +++ b/macaw-cli/src/Data/Macaw/CLI.hs @@ -15,7 +15,6 @@ 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) @@ -23,6 +22,7 @@ import GHC.TypeLits (KnownNat) import Data.ElfEdit qualified as Elf import Data.Macaw.Architecture.Info qualified as MAI import Data.Macaw.CFG qualified as MCFG +import Data.Macaw.CLI.Options qualified as MCO import Data.Macaw.Discovery qualified as MD import Data.Macaw.Memory.ElfLoader.PLTStubs qualified as MPLT import Data.Macaw.Symbolic qualified as MS @@ -53,11 +53,12 @@ sim :: MS.GenArchVals MS.LLVMMemory arch -> MPLT.PLTStubInfo reloc -> (forall sym. CB.IsSymInterface sym => MST.ResultExtractor sym arch) -> - FilePath -> Elf.ElfHeaderInfo (MD.ArchAddrWidth arch) -> - Text -> + MCO.Opts -> IO () -sim archInfo archVals pltStubInfo extractor binPath elfHeaderInfo entryFn = do +sim archInfo archVals pltStubInfo extractor elfHeaderInfo opts = do + let binPath = MCO.optsBinaryPath opts + let entryFn = MCO.optsEntrypoint opts Some.Some nonceGen <- PN.newIONonceGenerator binfo <- MST.runDiscovery elfHeaderInfo binPath MST.toAddrSymMap archInfo pltStubInfo let discState = MST.binaryDiscState (MST.mainBinaryInfo binfo) diff --git a/macaw-cli/src/Data/Macaw/CLI/Options.hs b/macaw-cli/src/Data/Macaw/CLI/Options.hs new file mode 100644 index 00000000..b3825340 --- /dev/null +++ b/macaw-cli/src/Data/Macaw/CLI/Options.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE RecordWildCards #-} + +module Data.Macaw.CLI.Options + ( Opts(..) + , getOpts + ) where + +import Control.Applicative ((<**>)) +import Data.Text (Text) +import Options.Applicative qualified as Opt + +data Opts = Opts + { optsBinaryPath :: FilePath + , optsEntrypoint :: Text + } deriving Show + +opts :: Opt.Parser Opts +opts = do + optsBinaryPath <- Opt.strArgument (Opt.help "filename of binary" <> Opt.metavar "FILENAME" ) + optsEntrypoint <- + Opt.strOption (Opt.long "entrypoint" <> Opt.help "name of entrypoint symbol" <> Opt.metavar "ENTRY") + pure Opts{..} + +optsInfo :: Opt.ParserInfo Opts +optsInfo = + Opt.info + (opts <**> Opt.helper) + ( Opt.fullDesc + <> Opt.header "Execute programs using macaw-symbolic" + ) + +getOpts :: IO Opts +getOpts = Opt.execParser optsInfo diff --git a/macaw-x86-cli/app/Main.hs b/macaw-x86-cli/app/Main.hs index fd4d74f8..5a4b4551 100644 --- a/macaw-x86-cli/app/Main.hs +++ b/macaw-x86-cli/app/Main.hs @@ -9,13 +9,12 @@ 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.CLI.Options qualified as MCO import Data.Macaw.Symbolic qualified as MS import Data.Macaw.Symbolic.Testing qualified as MST import Data.Macaw.X86 qualified as X86 @@ -38,31 +37,30 @@ x86ResultExtractor archVals = MST.ResultExtractor $ \regs _sp _mem k -> do k PC.knownRepr (CSRM.regValue re) simX86_64 :: - FilePath -> + MCO.Opts -> Elf.ElfHeaderInfo 64 -> - Text -> IO () -simX86_64 binPath elfHeaderInfo entryFn = do +simX86_64 opts elfHeaderInfo = 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 + MCLI.sim X86.x86_64_linux_info archVals X86.x86_64PLTStubInfo (x86ResultExtractor archVals) elfHeaderInfo opts simFile :: - FilePath -> - Text -> + MCO.Opts -> IO () -simFile binPath entryFn = do +simFile opts = do + let binPath = MCO.optsBinaryPath opts 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 + (Elf.ELFCLASS64, Elf.EM_X86_64) -> simX86_64 opts hdr (_, 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") +main = simFile =<< MCO.getOpts From f2b9213055b1ea9d9f7760b9ac8d55d440ab7e85 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 3 Jul 2024 17:59:27 -0400 Subject: [PATCH 3/6] cli: Properly attribute license copyright --- macaw-cli/LICENSE | 2 +- macaw-x86-cli/LICENSE | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/macaw-cli/LICENSE b/macaw-cli/LICENSE index a3ea82f7..94cfc1a6 100644 --- a/macaw-cli/LICENSE +++ b/macaw-cli/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2024, Langston Barrett +Copyright (c) 2024, Galois Inc. All rights reserved. diff --git a/macaw-x86-cli/LICENSE b/macaw-x86-cli/LICENSE index a3ea82f7..94cfc1a6 100644 --- a/macaw-x86-cli/LICENSE +++ b/macaw-x86-cli/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2024, Langston Barrett +Copyright (c) 2024, Galois Inc. All rights reserved. From 2f1db570dcd2ba32ff8582f4644918eee6d5a6e6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 3 Jul 2024 18:01:10 -0400 Subject: [PATCH 4/6] cli: Remove a defunct TODO --- macaw-x86-cli/app/Main.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/macaw-x86-cli/app/Main.hs b/macaw-x86-cli/app/Main.hs index 5a4b4551..482de33d 100644 --- a/macaw-x86-cli/app/Main.hs +++ b/macaw-x86-cli/app/Main.hs @@ -60,7 +60,6 @@ simFile opts = do Left _ -> bail ("User error: expected x86_64 ELF binary, but found non-ELF file at " List.++ binPath) --- TODO: CLI main :: IO () main = simFile =<< MCO.getOpts From 89af350a4c3e5c581398da769e3a2c50dbc07bfe Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 3 Jul 2024 18:14:53 -0400 Subject: [PATCH 5/6] cli: Refactor for testability --- macaw-cli/src/Data/Macaw/CLI.hs | 58 +++++++++++++--------- macaw-x86-cli/app/Main.hs | 61 +++-------------------- macaw-x86-cli/macaw-x86-cli.cabal | 23 +++++++-- macaw-x86-cli/src/Data/Macaw/X86/CLI.hs | 66 +++++++++++++++++++++++++ 4 files changed, 127 insertions(+), 81 deletions(-) create mode 100644 macaw-x86-cli/src/Data/Macaw/X86/CLI.hs diff --git a/macaw-cli/src/Data/Macaw/CLI.hs b/macaw-cli/src/Data/Macaw/CLI.hs index 79d1fb85..a810deab 100644 --- a/macaw-cli/src/Data/Macaw/CLI.hs +++ b/macaw-cli/src/Data/Macaw/CLI.hs @@ -3,17 +3,20 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} module Data.Macaw.CLI ( sim + , ppSimRes ) where import Control.Lens qualified as Lens -import Control.Monad qualified as Monad import Data.ByteString.Char8 qualified as BS8 +import Data.List qualified as List import Data.Map qualified as Map import Data.Text qualified as Text import GHC.TypeLits (KnownNat) @@ -41,6 +44,7 @@ import What4.Solver.Yices qualified as WSY data MacawCLI t = MacawCLI +-- | Simulate a function using 'MST.simulateAndVerify' sim :: (1 PNat.<= MCFG.ArchAddrWidth arch) => (16 PNat.<= MCFG.ArchAddrWidth arch) => @@ -55,7 +59,8 @@ sim :: (forall sym. CB.IsSymInterface sym => MST.ResultExtractor sym arch) -> Elf.ElfHeaderInfo (MD.ArchAddrWidth arch) -> MCO.Opts -> - IO () + -- | 'Nothing' when the entrypoint couldn\'t be found + IO (Maybe MST.SimulationResult) sim archInfo archVals pltStubInfo extractor elfHeaderInfo opts = do let binPath = MCO.optsBinaryPath opts let entryFn = MCO.optsEntrypoint opts @@ -64,23 +69,32 @@ sim archInfo archVals pltStubInfo extractor elfHeaderInfo opts = do 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 () + let isEntry sdfi = + case sdfi of + Some.Some dfi -> + case MD.discoveredFunSymbol dfi of + Just funSymb -> entryFn8 `BS8.isPrefixOf` funSymb + Nothing -> False + let mEntry = List.find isEntry funInfos + case mEntry of + Nothing -> pure Nothing + Just (Some.Some dfi) -> 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 + Just <$> MST.simulateAndVerify solver WS.defaultLogData bak execFeatures archInfo archVals binfo mmPreset extractor dfi + +ppSimRes :: MST.SimulationResult -> Text.Text +ppSimRes = + \case + MST.SimulationAborted -> "Aborted!" + MST.SimulationTimeout -> "Timeout!" + MST.SimulationPartial -> "Partial!" -- TODO: What does this mean? + MST.SimulationResult MST.Unsat -> "Always returns 0" + MST.SimulationResult MST.Sat -> "May return non-zero" + MST.SimulationResult MST.Unknown -> "Solver returned unknown!" diff --git a/macaw-x86-cli/app/Main.hs b/macaw-x86-cli/app/Main.hs index 482de33d..6e0e6b81 100644 --- a/macaw-x86-cli/app/Main.hs +++ b/macaw-x86-cli/app/Main.hs @@ -1,65 +1,18 @@ -{-# 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 System.Exit qualified as Exit +import Data.Text.IO qualified as Text -- First-party -import Data.ElfEdit qualified as Elf import Data.Macaw.CLI qualified as MCLI import Data.Macaw.CLI.Options qualified as MCO -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 :: - MCO.Opts -> - Elf.ElfHeaderInfo 64 -> - IO () -simX86_64 opts elfHeaderInfo = 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) elfHeaderInfo opts - -simFile :: - MCO.Opts -> - IO () -simFile opts = do - let binPath = MCO.optsBinaryPath opts - 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 opts hdr - (_, 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) +import Data.Macaw.X86.CLI qualified as MX86CLI main :: IO () -main = simFile =<< MCO.getOpts +main = do + mres <- MX86CLI.simFile =<< MCO.getOpts + case mres of + Nothing -> MX86CLI.bail "Entrypoint not found!" + Just res -> Text.putStrLn (MCLI.ppSimRes res) diff --git a/macaw-x86-cli/macaw-x86-cli.cabal b/macaw-x86-cli/macaw-x86-cli.cabal index 80732f70..78590a24 100644 --- a/macaw-x86-cli/macaw-x86-cli.cabal +++ b/macaw-x86-cli/macaw-x86-cli.cabal @@ -82,12 +82,11 @@ common shared ghc-prof-options: -O2 -fprof-auto-top default-language: Haskell2010 -executable macaw-x86-cli +library import: shared - hs-source-dirs: app - main-is: Main.hs - -- other-modules: - -- other-extensions: + hs-source-dirs: src + exposed-modules: + Data.Macaw.X86.CLI build-depends: base >=4.16, bytestring, @@ -108,3 +107,17 @@ executable macaw-x86-cli macaw-x86-symbolic, parameterized-utils, what4 + +executable macaw-x86-cli + import: shared + hs-source-dirs: app + main-is: Main.hs + -- other-modules: + -- other-extensions: + build-depends: + base >=4.16, + text, + + -- first-party (alphabetical) + macaw-cli, + macaw-x86-cli diff --git a/macaw-x86-cli/src/Data/Macaw/X86/CLI.hs b/macaw-x86-cli/src/Data/Macaw/X86/CLI.hs new file mode 100644 index 00000000..c38abc63 --- /dev/null +++ b/macaw-x86-cli/src/Data/Macaw/X86/CLI.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Macaw.X86.CLI + ( bail + , simFile + ) where + +import Data.ByteString qualified as BS +import Data.List qualified as List +import Data.Proxy qualified as Proxy +import System.Exit qualified as Exit + +-- First-party +import Data.ElfEdit qualified as Elf +import Data.Macaw.CLI qualified as MCLI +import Data.Macaw.CLI.Options qualified as MCO +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 :: + MCO.Opts -> + Elf.ElfHeaderInfo 64 -> + -- | 'Nothing' when the entrypoint can\'t be found + IO (Maybe MST.SimulationResult) +simX86_64 opts elfHeaderInfo = 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) elfHeaderInfo opts + +simFile :: + MCO.Opts -> + -- | 'Nothing' when the entrypoint can\'t be found + IO (Maybe MST.SimulationResult) +simFile opts = do + let binPath = MCO.optsBinaryPath opts + 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 opts hdr + (_, 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) From 248518df082ff4999009fe24314e4842e4cdd51d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 8 Jul 2024 12:21:49 -0400 Subject: [PATCH 6/6] Fix error code reporting --- macaw-cli/src/Data/Macaw/CLI.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/macaw-cli/src/Data/Macaw/CLI.hs b/macaw-cli/src/Data/Macaw/CLI.hs index a810deab..bcf50d61 100644 --- a/macaw-cli/src/Data/Macaw/CLI.hs +++ b/macaw-cli/src/Data/Macaw/CLI.hs @@ -17,8 +17,8 @@ module Data.Macaw.CLI import Control.Lens qualified as Lens import Data.ByteString.Char8 qualified as BS8 import Data.List qualified as List -import Data.Map qualified as Map -import Data.Text qualified as Text +import Data.Map qualified as Map +import Data.Text qualified as Text import GHC.TypeLits (KnownNat) -- First-party @@ -69,7 +69,7 @@ sim archInfo archVals pltStubInfo extractor elfHeaderInfo opts = do let discState = MST.binaryDiscState (MST.mainBinaryInfo binfo) let funInfos = Map.elems (discState Lens.^. MD.funInfo) let entryFn8 = BS8.pack (Text.unpack entryFn) - let isEntry sdfi = + let isEntry sdfi = case sdfi of Some.Some dfi -> case MD.discoveredFunSymbol dfi of @@ -95,6 +95,6 @@ ppSimRes = MST.SimulationAborted -> "Aborted!" MST.SimulationTimeout -> "Timeout!" MST.SimulationPartial -> "Partial!" -- TODO: What does this mean? - MST.SimulationResult MST.Unsat -> "Always returns 0" - MST.SimulationResult MST.Sat -> "May return non-zero" + MST.SimulationResult MST.Unsat -> "May return non-zero" + MST.SimulationResult MST.Sat -> "Always returns 0" MST.SimulationResult MST.Unknown -> "Solver returned unknown!"