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 ()