From f77d848ec10d9b431e041029f1409ef31d06f7f2 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 15 Aug 2024 10:28:54 -0400 Subject: [PATCH] macaw-x86-syntax: Syntactic sugar for macaw-x86-symbolic CFGs --- macaw-x86-syntax/LICENSE | 30 ++++ macaw-x86-syntax/README.md | 17 +++ macaw-x86-syntax/macaw-x86-syntax.cabal | 131 ++++++++++++++++++ .../src/Data/Macaw/X86/Symbolic/Syntax.hs | 52 +++++++ macaw-x86-syntax/test-data/.gitignore | 1 + macaw-x86-syntax/test-data/regs.cbl | 3 + macaw-x86-syntax/test-data/regs.out.good | 8 ++ macaw-x86-syntax/test/Test.hs | 56 ++++++++ 8 files changed, 298 insertions(+) create mode 100644 macaw-x86-syntax/LICENSE create mode 100644 macaw-x86-syntax/README.md create mode 100644 macaw-x86-syntax/macaw-x86-syntax.cabal create mode 100644 macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs create mode 100644 macaw-x86-syntax/test-data/.gitignore create mode 100644 macaw-x86-syntax/test-data/regs.cbl create mode 100644 macaw-x86-syntax/test-data/regs.out.good create mode 100644 macaw-x86-syntax/test/Test.hs diff --git a/macaw-x86-syntax/LICENSE b/macaw-x86-syntax/LICENSE new file mode 100644 index 00000000..511de500 --- /dev/null +++ b/macaw-x86-syntax/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-syntax/README.md b/macaw-x86-syntax/README.md new file mode 100644 index 00000000..0f4cf763 --- /dev/null +++ b/macaw-x86-syntax/README.md @@ -0,0 +1,17 @@ +# macaw-x86-syntax + +This package provides concrete syntax for macaw-x86-symbolic types and +operations. + +Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn]. +This `ParserHooks` supports the following types and operations: + +**Types**: + +- `X86Regs`: the struct of all x86_64 registers + +**Operations**: + +(none so far) + +[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax diff --git a/macaw-x86-syntax/macaw-x86-syntax.cabal b/macaw-x86-syntax/macaw-x86-syntax.cabal new file mode 100644 index 00000000..fff2adb9 --- /dev/null +++ b/macaw-x86-syntax/macaw-x86-syntax.cabal @@ -0,0 +1,131 @@ +Cabal-version: 2.2 +Name: macaw-x86-syntax +Version: 0.1 +Author: Galois Inc. +Maintainer: langston@galois.com +Build-type: Simple +License: BSD-3-Clause +License-file: LICENSE +Category: Language +Synopsis: A syntax for 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-syntax, + macaw-base, + macaw-symbolic, + macaw-x86, + macaw-x86-symbolic, + parameterized-utils, + text, + + hs-source-dirs: src + + exposed-modules: + Data.Macaw.X86.Symbolic.Syntax + +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, diff --git a/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs new file mode 100644 index 00000000..8291a80b --- /dev/null +++ b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | 'LCSC.ParserHooks' for parsing macaw-x86-symbolic CFGs. +module Data.Macaw.X86.Symbolic.Syntax + ( x86ParserHooks + , x86TypeParser + ) where + +import Control.Applicative ( empty ) +import Control.Monad qualified as Monad +import Data.Text qualified as Text +import Data.Parameterized.Some ( Some(..) ) + +import Data.Macaw.Symbolic qualified as DMS +import Data.Macaw.X86 qualified as X86 +import Data.Macaw.X86.Symbolic qualified as X86 +import Lang.Crucible.Syntax.Atoms qualified as LCSA +import Lang.Crucible.Syntax.Concrete qualified as LCSC +import Lang.Crucible.Syntax.Monad qualified as LCSM +import Lang.Crucible.Types qualified as LCT + +-- | Parser hooks for macaw-x86-symbolic CFGs +x86ParserHooks :: LCSC.ParserHooks ext +x86ParserHooks = + LCSC.ParserHooks + { LCSC.extensionTypeParser = x86TypeParser + , LCSC.extensionParser = empty + } + +--------------------------------------------------------------------- +-- Types + +-- Helper, not exported +namedAtom :: LCSM.MonadSyntax LCSA.Atomic m => Text.Text -> m () +namedAtom expectName = do + name <- LCSC.atomName + Monad.unless (name == LCSA.AtomName expectName) LCSM.cut + +-- Helper, not exported +x86RegStructType :: LCT.TypeRepr (DMS.ArchRegStruct X86.X86_64) +x86RegStructType = + LCT.StructRepr (DMS.crucArchRegTypes X86.x86_64MacawSymbolicFns) + +-- | Parser for type extensions to Crucible syntax +x86TypeParser :: + LCSM.MonadSyntax LCSA.Atomic m => + m (Some LCT.TypeRepr) +x86TypeParser = do + namedAtom "X86Regs" + pure (Some x86RegStructType) diff --git a/macaw-x86-syntax/test-data/.gitignore b/macaw-x86-syntax/test-data/.gitignore new file mode 100644 index 00000000..f47cb204 --- /dev/null +++ b/macaw-x86-syntax/test-data/.gitignore @@ -0,0 +1 @@ +*.out diff --git a/macaw-x86-syntax/test-data/regs.cbl b/macaw-x86-syntax/test-data/regs.cbl new file mode 100644 index 00000000..ebf6cf9b --- /dev/null +++ b/macaw-x86-syntax/test-data/regs.cbl @@ -0,0 +1,3 @@ +(defun @id ((regs X86Regs)) X86Regs + (start start: + (return regs))) \ No newline at end of file diff --git a/macaw-x86-syntax/test-data/regs.out.good b/macaw-x86-syntax/test-data/regs.out.good new file mode 100644 index 00000000..14e7a19e --- /dev/null +++ b/macaw-x86-syntax/test-data/regs.out.good @@ -0,0 +1,8 @@ +(defun @id ((regs X86Regs)) X86Regs + (start start: (return regs))) + +id +%0 + % 3:5 + return $0 + % no postdom diff --git a/macaw-x86-syntax/test/Test.hs b/macaw-x86-syntax/test/Test.hs new file mode 100644 index 00000000..83f57b15 --- /dev/null +++ b/macaw-x86-syntax/test/Test.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} + +module Main (main) where + +import Data.List (sort) +import Data.Proxy (Proxy(Proxy)) +import Data.Text.IO qualified as T +import System.FilePath +import System.IO + +import Test.Tasty (defaultMain, TestTree, testGroup) +import Test.Tasty.Golden + +import Lang.Crucible.Syntax.Prog (doParseCheck) + +import Data.Macaw.Symbolic.Syntax (machineCodeParserHooks) + +import Data.Macaw.X86 (X86_64) +import Data.Macaw.X86.Symbolic () -- TraversableFC instance for (MacawExt X86) statements and expressions +import Data.Macaw.X86.Symbolic.Syntax (x86ParserHooks) + +main :: IO () +main = do + parseTests <- findTests "Parse tests" "test-data" testParser + defaultMain $ testGroup "Tests" [parseTests] + +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" + +testParser :: FilePath -> FilePath -> IO () +testParser inFile outFile = + do contents <- T.readFile inFile + let ?parserHooks = machineCodeParserHooks (Proxy @X86_64) x86ParserHooks + withFile outFile WriteMode $ doParseCheck inFile contents True +