From c91f8400a0c3fb260c57b32297c896fe762ea450 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 16 Aug 2024 16:47:44 -0400 Subject: [PATCH] x86-cli: A CLI for running macaw-x86-symbolic S-expression CFGs --- deps/crucible | 2 +- macaw-x86-cli/LICENSE | 30 ++++ macaw-x86-cli/app/Main.hs | 55 +++++++ 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 + 7 files changed, 247 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/deps/crucible b/deps/crucible index e8614064..4e97150e 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit e86140641260b00f64fdbd51d73d48d766c55bdf +Subproject commit 4e97150ec38de6bbdb923744c3a6285d3891cace 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..d2d22b5c --- /dev/null +++ b/macaw-x86-cli/app/Main.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# 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.newGlobalMemoryWith + DMS.defaultGlobalMemoryHooks + (Proxy @X86_64) + bak + LittleEndian + DMS.ConcreteMutable + elfMem + let mmConf = DMS.memModelConfig @_ @_ @64 @X86_64 bak ptrTable + 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 ()