From 00e1c03deecb013306cdf0d7438bb5c7e6c8793b Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 16 Aug 2024 16:47:44 -0400 Subject: [PATCH 1/7] x86-cli: A CLI for running macaw-x86-symbolic S-expression CFGs --- .github/workflows/ci.yaml | 6 + cabal.project.dist | 2 + deps/crucible | 2 +- macaw-x86-cli/LICENSE | 30 ++++ macaw-x86-cli/app/Main.hs | 57 +++++++ macaw-x86-cli/macaw-x86-cli.cabal | 153 ++++++++++++++++++ .../src/Data/Macaw/X86/Symbolic/CLI.hs | 3 + macaw-x86-cli/test-data/.gitignore | 1 + macaw-x86-cli/test/Test.hs | 4 + 9 files changed, 257 insertions(+), 1 deletion(-) 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 create mode 100644 macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs create mode 100644 macaw-x86-cli/test-data/.gitignore create mode 100644 macaw-x86-cli/test/Test.hs diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index f3f08104..c927aa2c 100644 --- a/.github/workflows/ci.yaml +++ b/.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-syntax + 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 diff --git a/cabal.project.dist b/cabal.project.dist index 3582147d..7dd5055c 100644 --- a/cabal.project.dist +++ b/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/ diff --git a/deps/crucible b/deps/crucible index e8614064..93bfa7f7 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit e86140641260b00f64fdbd51d73d48d766c55bdf +Subproject commit 93bfa7f7858eb458f83eb3e0f030bf600ef72365 diff --git a/macaw-x86-cli/LICENSE b/macaw-x86-cli/LICENSE new file mode 100644 index 00000000..511de500 --- /dev/null +++ b/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. diff --git a/macaw-x86-cli/app/Main.hs b/macaw-x86-cli/app/Main.hs new file mode 100644 index 00000000..df02ef4b --- /dev/null +++ b/macaw-x86-cli/app/Main.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +module Main (main) where + +import Data.Proxy (Proxy(..)) + +import Data.Parameterized.NatRepr (knownNat) + +import Lang.Crucible.Backend qualified as C +import Lang.Crucible.CLI (defaultSimulateProgramHooks) +import Lang.Crucible.CLI.Options qualified as Opts +import Lang.Crucible.FunctionHandle (newHandleAllocator) +import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian)) +import Lang.Crucible.LLVM.MemModel qualified as Mem + +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.CLI () +import Data.Macaw.X86.Symbolic.Syntax (x86ParserHooks) + +main :: IO () +main = do + let ?parserHooks = machineCodeParserHooks (Proxy :: Proxy X86_64) x86ParserHooks + ha <- newHandleAllocator + mvar <- Mem.mkMemVar "llvm_memory" ha + let ?ptrWidth = knownNat @64 + let ?memOpts = Mem.defaultMemOptions + Opts.main + "macaw-x86" + (\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)) + defaultSimulateProgramHooks diff --git a/macaw-x86-cli/macaw-x86-cli.cabal b/macaw-x86-cli/macaw-x86-cli.cabal new file mode 100644 index 00000000..d712173d --- /dev/null +++ b/macaw-x86-cli/macaw-x86-cli.cabal @@ -0,0 +1,153 @@ +Cabal-version: 2.2 +Name: macaw-x86-cli +Version: 0.1 +Author: Galois Inc. +Maintainer: langston@galois.com +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, + containers, + crucible, + crucible-cli, + crucible-syntax, + -- macaw-base, + -- macaw-symbolic, + macaw-x86, + macaw-x86-symbolic, + macaw-x86-syntax, + -- mtl, + parameterized-utils, + -- text, + -- 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-syntax, + crucible-llvm-syntax, + filepath, + macaw-symbolic, + macaw-symbolic-syntax, + macaw-x86, + macaw-x86-symbolic, + macaw-x86-syntax, + parameterized-utils >= 0.1.7, + tasty, + tasty-golden, + text, + +executable macaw-x86 + import: shared + hs-source-dirs: app + main-is: Main.hs + build-depends: + base >= 4.13, + crucible, + crucible-cli, + crucible-llvm, + macaw-base, + macaw-x86-cli, + macaw-symbolic, + macaw-symbolic-syntax, + macaw-x86, + macaw-x86-symbolic, + macaw-x86-syntax, + parameterized-utils, diff --git a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs new file mode 100644 index 00000000..89dcefa1 --- /dev/null +++ b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs @@ -0,0 +1,3 @@ +module Data.Macaw.X86.Symbolic.CLI + ( + ) where diff --git a/macaw-x86-cli/test-data/.gitignore b/macaw-x86-cli/test-data/.gitignore new file mode 100644 index 00000000..f47cb204 --- /dev/null +++ b/macaw-x86-cli/test-data/.gitignore @@ -0,0 +1 @@ +*.out diff --git a/macaw-x86-cli/test/Test.hs b/macaw-x86-cli/test/Test.hs new file mode 100644 index 00000000..a31c5a02 --- /dev/null +++ b/macaw-x86-cli/test/Test.hs @@ -0,0 +1,4 @@ +module Main (main) where + +main :: IO () +main = pure () From 0ed622b3aca90594bbb9f15c1a9c3ac3e940a9a1 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 20 Aug 2024 13:35:08 -0400 Subject: [PATCH 2/7] x86-cli: Libraryfication Make the code easier to test --- macaw-x86-cli/app/Main.hs | 46 +---------- macaw-x86-cli/macaw-x86-cli.cabal | 20 ++--- .../src/Data/Macaw/X86/Symbolic/CLI.hs | 78 ++++++++++++++++++- 3 files changed, 84 insertions(+), 60 deletions(-) diff --git a/macaw-x86-cli/app/Main.hs b/macaw-x86-cli/app/Main.hs index df02ef4b..0b22b6e2 100644 --- a/macaw-x86-cli/app/Main.hs +++ b/macaw-x86-cli/app/Main.hs @@ -7,51 +7,9 @@ module Main (main) where -import Data.Proxy (Proxy(..)) - -import Data.Parameterized.NatRepr (knownNat) - -import Lang.Crucible.Backend qualified as C -import Lang.Crucible.CLI (defaultSimulateProgramHooks) import Lang.Crucible.CLI.Options qualified as Opts -import Lang.Crucible.FunctionHandle (newHandleAllocator) -import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian)) -import Lang.Crucible.LLVM.MemModel qualified as Mem -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.CLI () -import Data.Macaw.X86.Symbolic.Syntax (x86ParserHooks) +import Data.Macaw.X86.Symbolic.CLI (withX86Hooks) main :: IO () -main = do - let ?parserHooks = machineCodeParserHooks (Proxy :: Proxy X86_64) x86ParserHooks - ha <- newHandleAllocator - mvar <- Mem.mkMemVar "llvm_memory" ha - let ?ptrWidth = knownNat @64 - let ?memOpts = Mem.defaultMemOptions - Opts.main - "macaw-x86" - (\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)) - defaultSimulateProgramHooks +main = withX86Hooks (Opts.main "macaw-x86") diff --git a/macaw-x86-cli/macaw-x86-cli.cabal b/macaw-x86-cli/macaw-x86-cli.cabal index d712173d..900f53d1 100644 --- a/macaw-x86-cli/macaw-x86-cli.cabal +++ b/macaw-x86-cli/macaw-x86-cli.cabal @@ -93,19 +93,18 @@ library build-depends: base >= 4.13, - containers, crucible, crucible-cli, + crucible-llvm, crucible-syntax, - -- macaw-base, - -- macaw-symbolic, + macaw-base, + macaw-symbolic, + macaw-symbolic-syntax, macaw-x86, macaw-x86-symbolic, macaw-x86-syntax, - -- mtl, parameterized-utils, - -- text, - -- what4, + what4, hs-source-dirs: src @@ -140,14 +139,5 @@ executable macaw-x86 main-is: Main.hs build-depends: base >= 4.13, - crucible, crucible-cli, - crucible-llvm, - macaw-base, macaw-x86-cli, - macaw-symbolic, - macaw-symbolic-syntax, - macaw-x86, - macaw-x86-symbolic, - macaw-x86-syntax, - parameterized-utils, diff --git a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs index 89dcefa1..eeeef442 100644 --- a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs +++ b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs @@ -1,3 +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 \ No newline at end of file From 17a1ed1751aae10be9ee751ca3bd86530b643f29 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 20 Aug 2024 13:43:39 -0400 Subject: [PATCH 3/7] x86-cli: Test suite --- macaw-x86-cli/macaw-x86-cli.cabal | 5 ++- macaw-x86-cli/test-data/byte-id.cbl | 10 +++++ macaw-x86-cli/test-data/byte-id.out.good | 4 ++ macaw-x86-cli/test/Test.hs | 49 +++++++++++++++++++++++- 4 files changed, 65 insertions(+), 3 deletions(-) create mode 100644 macaw-x86-cli/test-data/byte-id.cbl create mode 100644 macaw-x86-cli/test-data/byte-id.out.good diff --git a/macaw-x86-cli/macaw-x86-cli.cabal b/macaw-x86-cli/macaw-x86-cli.cabal index 900f53d1..6fc9c975 100644 --- a/macaw-x86-cli/macaw-x86-cli.cabal +++ b/macaw-x86-cli/macaw-x86-cli.cabal @@ -120,18 +120,19 @@ test-suite macaw-x86-syntax-tests base, containers, crucible >= 0.1, - crucible-syntax, - crucible-llvm-syntax, + 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 diff --git a/macaw-x86-cli/test-data/byte-id.cbl b/macaw-x86-cli/test-data/byte-id.cbl new file mode 100644 index 00000000..24d3d81a --- /dev/null +++ b/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 ()))) \ No newline at end of file diff --git a/macaw-x86-cli/test-data/byte-id.out.good b/macaw-x86-cli/test-data/byte-id.out.good new file mode 100644 index 00000000..a0dc0d91 --- /dev/null +++ b/macaw-x86-cli/test-data/byte-id.out.good @@ -0,0 +1,4 @@ +==== Begin Simulation ==== + +==== Finish Simulation ==== +==== No proof obligations ==== diff --git a/macaw-x86-cli/test/Test.hs b/macaw-x86-cli/test/Test.hs index a31c5a02..323604a4 100644 --- a/macaw-x86-cli/test/Test.hs +++ b/macaw-x86-cli/test/Test.hs @@ -1,4 +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 = pure () +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 From 607e14d4b5da6cd3eaf735b17ec5aa96d62e24fd Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 20 Aug 2024 14:48:27 -0400 Subject: [PATCH 4/7] ci: Fix typo in job name --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index c927aa2c..1e5d2514 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -119,7 +119,7 @@ jobs: - name: Build macaw-x86-cli run: cabal build pkg:macaw-x86-cli - - name: Test macaw-x86-syntax + - name: Test macaw-x86-cli run: cabal test pkg:macaw-x86-cli - name: Build macaw-aarch32 From ff85c7857444929a9a68c292471ecc6c19b6d224 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 20 Aug 2024 15:43:17 -0400 Subject: [PATCH 5/7] x86-cli: Prefix name of LLVM memory global with package name --- macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs index eeeef442..10db4bd8 100644 --- a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs +++ b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs @@ -50,7 +50,7 @@ withX86Hooks :: IO a withX86Hooks k = do ha <- newHandleAllocator - mvar <- Mem.mkMemVar "llvm_memory" ha + mvar <- Mem.mkMemVar "macaw-x86:llvm_memory" ha let ?ptrWidth = knownNat @64 let ?memOpts = Mem.defaultMemOptions let ext :: From de9c30a679a6979e19d096fe90bd34e1f624ca2f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 20 Aug 2024 15:44:24 -0400 Subject: [PATCH 6/7] x86-cli: Fix copy/paste error in Haddock --- macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs index 10db4bd8..c49d182c 100644 --- a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs +++ b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs @@ -35,8 +35,8 @@ 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'. + -- | Small helper for providing X86_64 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. From e8570aeec4a1eda539dd4891b31ff8230029f680 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 20 Aug 2024 16:57:39 -0400 Subject: [PATCH 7/7] x86-cli: Add detail to a TODO --- macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs index c49d182c..84a652de 100644 --- a/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs +++ b/macaw-x86-cli/src/Data/Macaw/X86/Symbolic/CLI.hs @@ -71,7 +71,8 @@ withX86Hooks k = do LittleEndian DMS.ConcreteMutable elfMem - -- TOOD? + -- TODO: We should write this variable, but can't here. See Macaw#423 + -- and Crucible#1240 for details. -- C.writeGlobal mvar initMem let mmConf = DMS.memModelConfig bak ptrTable pure (DMS.macawExtensions eFn mvar mmConf)