Simple CLI for macaw-symbolic

.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

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/

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.

macaw-cli/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 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.

macaw-cli/macaw-cli.cabal

@@ -0,0 +1,107 @@
+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,
+    optparse-applicative,
+    text,
+
+    -- first-party (alphabetical)
+    crucible,
+    crucible-llvm,
+    elf-edit,
+    macaw-base,
+    macaw-loader,
+    macaw-symbolic,
+    parameterized-utils,
+    what4
+  exposed-modules:
+    Data.Macaw.CLI
+    Data.Macaw.CLI.Options

macaw-cli/src/Data/Macaw/CLI.hs

@@ -0,0 +1,100 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# 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 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)
+
+-- 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.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
+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
+
+-- | Simulate a function using 'MST.simulateAndVerify'
+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) ->
+  Elf.ElfHeaderInfo (MD.ArchAddrWidth arch) ->
+  MCO.Opts ->
+  -- | '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
+  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)
+  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 -> "May return non-zero"
+    MST.SimulationResult MST.Sat -> "Always returns 0"
+    MST.SimulationResult MST.Unknown -> "Solver returned unknown!"

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

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.

macaw-x86-cli/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 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.

macaw-x86-cli/app/Main.hs

@@ -0,0 +1,18 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+
+module Main where
+
+import Data.Text.IO qualified as Text
+
+-- First-party
+import Data.Macaw.CLI qualified as MCLI
+import Data.Macaw.CLI.Options qualified as MCO
+import Data.Macaw.X86.CLI qualified as MX86CLI
+
+main :: IO ()
+main = do
+  mres <- MX86CLI.simFile =<< MCO.getOpts
+  case mres of
+    Nothing -> MX86CLI.bail "Entrypoint not found!"
+    Just res -> Text.putStrLn (MCLI.ppSimRes res)
+