x86-cli: A CLI for running macaw-x86-symbolic S-expression CFGs

.github/workflows/ci.yaml

@@ -116,6 +116,12 @@ jobs:
     - name: Test macaw-x86-syntax
       run: cabal test pkg:macaw-x86-syntax
 
+    - name: Build macaw-x86-cli
+      run: cabal build pkg:macaw-x86-cli
+
+    - name: Test macaw-x86-cli
+      run: cabal test 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

@@ -6,6 +6,7 @@ packages: base/
           macaw-ppc-symbolic/
           macaw-riscv/
           macaw-riscv-symbolic/
+          macaw-x86-cli/
           macaw-x86-syntax/
           x86/
           symbolic/
@@ -29,6 +30,7 @@ packages: base/
           deps/dismantle/dismantle-arm-xml/
           deps/dismantle/dismantle-thumb/
           deps/crucible/crucible/
+          deps/crucible/crucible-cli/
           deps/crucible/crucible-llvm/
           deps/crucible/crucible-llvm-syntax/
           deps/crucible/crucible-symio/

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 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.

macaw-x86-cli/app/Main.hs

@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Lang.Crucible.CLI.Options qualified as Opts
+
+import Data.Macaw.X86.Symbolic.CLI (withX86Hooks)
+
+main :: IO ()
+main = withX86Hooks (Opts.main "macaw-x86")

macaw-x86-cli/macaw-x86-cli.cabal

@@ -0,0 +1,144 @@
+Cabal-version: 2.2
+Name:          macaw-x86-cli
+Version:       0.1
+Author:        Galois Inc.
+Maintainer:    [email protected]
+Build-type:    Simple
+License:       BSD-3-Clause
+License-file:  LICENSE
+Category:      Language
+Synopsis:      CLI for running macaw-x86-symbolic control-flow graphs
+-- Description:
+
+extra-doc-files: README.md
+extra-source-files:
+  test-data/*.cbl
+  test-data/*.out.good
+
+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,
+    crucible,
+    crucible-cli,
+    crucible-llvm,
+    crucible-syntax,
+    macaw-base,
+    macaw-symbolic,
+    macaw-symbolic-syntax,
+    macaw-x86,
+    macaw-x86-symbolic,
+    macaw-x86-syntax,
+    parameterized-utils,
+    what4,
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.Macaw.X86.Symbolic.CLI
+
+test-suite macaw-x86-syntax-tests
+  import: shared
+  type: exitcode-stdio-1.0
+  main-is: Test.hs
+  hs-source-dirs: test
+  build-depends:
+    base,
+    containers,
+    crucible >= 0.1,
+    crucible-cli,
+    filepath,
+    macaw-symbolic,
+    macaw-symbolic-syntax,
+    macaw-x86,
+    macaw-x86-cli,
+    macaw-x86-symbolic,
+    macaw-x86-syntax,
+    parameterized-utils >= 0.1.7,
+    tasty,
+    tasty-golden,
+    text,
+    what4,
+
+executable macaw-x86
+  import: shared
+  hs-source-dirs: app
+  main-is: Main.hs
+  build-depends:
+    base >= 4.13,
+    crucible-cli,
+    macaw-x86-cli,

macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs

@@ -0,0 +1,79 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Macaw.X86.Symbolic.CLI
+  ( withX86Hooks
+  ) where
+
+
+import Data.Proxy (Proxy(..))
+
+import Data.Parameterized.NatRepr (knownNat)
+
+import What4.Expr (ExprBuilder)
+
+import Lang.Crucible.Backend qualified as C
+import Lang.Crucible.CLI (SimulateProgramHooks, defaultSimulateProgramHooks)
+import Lang.Crucible.FunctionHandle (newHandleAllocator)
+import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian))
+import Lang.Crucible.LLVM.MemModel qualified as Mem
+import Lang.Crucible.Simulator.ExecutionTree (ExtensionImpl)
+import Lang.Crucible.Syntax.Concrete (ParserHooks)
+
+import Data.Macaw.CFG qualified as DMC
+import Data.Macaw.Memory qualified as DMM
+import Data.Macaw.Symbolic qualified as DMS
+import Data.Macaw.Symbolic.Memory qualified as DMS
+import Data.Macaw.Symbolic.Syntax (machineCodeParserHooks)
+import Data.Macaw.X86 (X86_64)
+import Data.Macaw.X86.Symbolic (newSymFuns, x86_64MacawEvalFn)
+import Data.Macaw.X86.Symbolic.Syntax (x86ParserHooks)
+
+ -- | Small helper for providing LLVM language-specific hooks, e.g., for use with
+-- 'Lang.Crucible.CLI.execCommand'.
+withX86Hooks ::
+  ((?parserHooks :: ParserHooks (DMS.MacawExt X86_64)) =>
+   (forall sym bak t st fs. 
+     ( C.IsSymBackend sym bak
+     , sym ~ ExprBuilder t st fs
+     ) =>
+     bak ->
+     IO (ExtensionImpl () sym (DMS.MacawExt X86_64))) ->
+    SimulateProgramHooks (DMS.MacawExt X86_64) ->
+    IO a) ->
+  IO a
+withX86Hooks k = do
+  ha <- newHandleAllocator
+  mvar <- Mem.mkMemVar "llvm_memory" ha
+  let ?ptrWidth = knownNat @64
+  let ?memOpts = Mem.defaultMemOptions
+  let ext ::
+        forall sym bak t st fs.
+        (C.IsSymBackend sym bak, sym ~ ExprBuilder t st fs) =>
+        bak ->
+        IO (ExtensionImpl () sym (DMS.MacawExt X86_64))
+      ext bak =  do
+        let sym = C.backendGetSym bak
+        let ?recordLLVMAnnotation = \_ _ _ -> pure ()
+        symFns <- newSymFuns sym
+        let elfMem = DMC.emptyMemory DMM.Addr64
+        let eFn = x86_64MacawEvalFn symFns DMS.defaultMacawArchStmtExtensionOverride
+        (_initMem, ptrTable) <-
+          DMS.newGlobalMemory
+            (Proxy @X86_64)
+            bak
+            LittleEndian
+            DMS.ConcreteMutable
+            elfMem
+        -- TOOD?
+        -- C.writeGlobal mvar initMem
+        let mmConf = DMS.memModelConfig bak ptrTable
+        pure (DMS.macawExtensions eFn mvar mmConf)
+  let ?parserHooks = machineCodeParserHooks (Proxy :: Proxy X86_64) x86ParserHooks
+  k ext defaultSimulateProgramHooks

macaw-x86-cli/test-data/.gitignore

@@ -0,0 +1 @@
+*.out

macaw-x86-cli/test-data/byte-id.cbl

@@ -0,0 +1,10 @@
+(defun @byte_id ((x (Bitvector 8))) (Bitvector 8)
+  (start start:
+    (return x)))
+
+(defun @main () Unit
+  (start start:
+    (let input (fresh (Bitvector 8)))
+    (let input_back (funcall @byte_id input))
+    (assert! (equal? input input_back) "byte_id test")
+    (return ())))

macaw-x86-cli/test-data/byte-id.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

macaw-x86-cli/test/Test.hs

@@ -0,0 +1,51 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Main (main) where
+
+import Data.List (sort)
+import Data.Text.IO qualified as T
+import System.FilePath
+import System.IO
+
+import Test.Tasty (defaultMain, TestTree, testGroup)
+import Test.Tasty.Golden
+
+import What4.Solver.Z3 (z3Options)
+
+import Lang.Crucible.CLI (simulateProgramWithExtension)
+
+import Data.Macaw.X86.Symbolic.CLI (withX86Hooks)
+
+main :: IO ()
+main = do
+  simTests <- findTests "x86 simulation" "test-data" testSimulator
+  defaultMain simTests
+
+findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree
+findTests groupName testDir testAction =
+  do inputs <- findByExtension [".cbl"] testDir
+     return $ testGroup groupName
+       [ goldenFileTestCase input testAction
+       | input <- sort inputs
+       ]
+
+goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree
+goldenFileTestCase input testAction =
+  goldenVsFileDiff
+   (takeBaseName input) -- test name
+   (\x y -> ["diff", "-u", x, y])
+   goodFile -- golden file path
+   outFile
+   (testAction input outFile) -- action whose result is tested
+  where
+    outFile = replaceExtension input ".out"
+    goodFile = replaceExtension input ".out.good"
+
+testSimulator :: FilePath -> FilePath -> IO ()
+testSimulator inFile outFile =
+  do contents <- T.readFile inFile
+     withFile outFile WriteMode $ \outh ->
+       withX86Hooks $ \ext hooks ->
+         simulateProgramWithExtension ext inFile contents outh Nothing z3Options hooks