diff --git a/cabal.project.dist b/cabal.project.dist index 2ca35e4e..68356fec 100644 --- a/cabal.project.dist +++ b/cabal.project.dist @@ -1,6 +1,7 @@ packages: base/ macaw-aarch32/ macaw-aarch32-symbolic/ + macaw-aarch32-syntax/ macaw-dump/ macaw-semmc/ macaw-ppc/ diff --git a/macaw-aarch32-syntax/LICENSE b/macaw-aarch32-syntax/LICENSE new file mode 100644 index 00000000..511de500 --- /dev/null +++ b/macaw-aarch32-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-aarch32-syntax/README.md b/macaw-aarch32-syntax/README.md new file mode 100644 index 00000000..17df27c9 --- /dev/null +++ b/macaw-aarch32-syntax/README.md @@ -0,0 +1,70 @@ +# macaw-aarch32-syntax + +This package provides concrete syntax for macaw-aarch32-symbolic types and +operations. + +Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn]. +This `ParserHooks` supports the following types and operations: + +**Types**: + +- `AArch32Regs`: the struct of all AArch32 registers + +**Operations**: + +- `get-reg :: AArch32Reg -> AArch32Regs -> t`: extract an x86 register +- `set-reg :: AArch32Reg -> t -> AArch32Regs -> AArch32Regs`: set an x86 register +- Registers: + - `r0 :: AArch32Reg` + - `r1 :: AArch32Reg` + - `r2 :: AArch32Reg` + - `r3 :: AArch32Reg` + - `r4 :: AArch32Reg` + - `r5 :: AArch32Reg` + - `r6 :: AArch32Reg` + - `r7 :: AArch32Reg` + - `r8 :: AArch32Reg` + - `r9 :: AArch32Reg` + - `r10 :: AArch32Reg` + - `r11 :: AArch32Reg`, AKA `fp` + - `fp :: AArch32Reg`, AKA `r11` + - `r12 :: AArch32Reg`, AKA `ip` + - `ip :: AArch32Reg`, AKA `r12` + - `r13 :: AArch32Reg`, AKA `sp` + - `sp :: AArch32Reg`, AKA `r13` + - `r14 :: AArch32Reg`, AKA `lr` + - `lr :: AArch32Reg`, AKA `r14` + - `v0 :: AArch32Reg` + - `v1 :: AArch32Reg` + - `v2 :: AArch32Reg` + - `v3 :: AArch32Reg` + - `v4 :: AArch32Reg` + - `v5 :: AArch32Reg` + - `v6 :: AArch32Reg` + - `v7 :: AArch32Reg` + - `v8 :: AArch32Reg` + - `v9 :: AArch32Reg` + - `v10 :: AArch32Reg` + - `v11 :: AArch32Reg` + - `v12 :: AArch32Reg` + - `v13 :: AArch32Reg` + - `v14 :: AArch32Reg` + - `v15 :: AArch32Reg` + - `v16 :: AArch32Reg` + - `v17 :: AArch32Reg` + - `v18 :: AArch32Reg` + - `v19 :: AArch32Reg` + - `v20 :: AArch32Reg` + - `v21 :: AArch32Reg` + - `v22 :: AArch32Reg` + - `v23 :: AArch32Reg` + - `v24 :: AArch32Reg` + - `v25 :: AArch32Reg` + - `v26 :: AArch32Reg` + - `v27 :: AArch32Reg` + - `v28 :: AArch32Reg` + - `v29 :: AArch32Reg` + - `v30 :: AArch32Reg` + - `v31 :: AArch32Reg` + +[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax diff --git a/macaw-aarch32-syntax/macaw-aarch32-syntax.cabal b/macaw-aarch32-syntax/macaw-aarch32-syntax.cabal new file mode 100644 index 00000000..2424d4bf --- /dev/null +++ b/macaw-aarch32-syntax/macaw-aarch32-syntax.cabal @@ -0,0 +1,127 @@ +Cabal-version: 2.2 +Name: macaw-aarch32-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-aarch32-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 9.4 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -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=forall-identifier + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -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 + + ghc-prof-options: -O2 -fprof-auto-top + default-language: Haskell2010 + +library + import: shared + + build-depends: + base >= 4.13, + containers, + crucible, + crucible-syntax, + macaw-aarch32, + macaw-aarch32-symbolic, + macaw-base, + macaw-symbolic, + mtl, + parameterized-utils, + text, + what4, + + hs-source-dirs: src + + exposed-modules: + Data.Macaw.AArch32.Symbolic.Syntax + +test-suite macaw-aarch32-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-aarch32, + macaw-aarch32-symbolic, + macaw-aarch32-syntax, + macaw-symbolic, + macaw-symbolic-syntax, + parameterized-utils >= 0.1.7, + tasty, + tasty-golden, + text, diff --git a/macaw-aarch32-syntax/src/Data/Macaw/AArch32/Symbolic/Syntax.hs b/macaw-aarch32-syntax/src/Data/Macaw/AArch32/Symbolic/Syntax.hs new file mode 100644 index 00000000..179236a5 --- /dev/null +++ b/macaw-aarch32-syntax/src/Data/Macaw/AArch32/Symbolic/Syntax.hs @@ -0,0 +1,175 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | 'LCSC.ParserHooks' for parsing macaw-aarch32-symbolic CFGs. +module Data.Macaw.AArch32.Symbolic.Syntax + ( aarch32ParserHooks + -- * Types + , aarch32TypeParser + -- * Operations + , parseRegs + , parseReg + , aarch32AtomParser + ) where + +import Control.Applicative ( empty ) +import Control.Monad qualified as Monad +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.State.Strict (MonadState) +import Control.Monad.Writer.Strict (MonadWriter) +import Data.Text qualified as Text + +import Data.Macaw.Symbolic qualified as DMS +import Data.Macaw.ARM qualified as ARM +import Data.Macaw.AArch32.Symbolic qualified as AArch32 +import Data.Macaw.AArch32.Symbolic.Regs qualified as AArch32R +import Data.Parameterized.Context qualified as Ctx +import Data.Parameterized.Some (Some(..)) +import Lang.Crucible.CFG.Expr as Expr +import Lang.Crucible.CFG.Reg (Atom, Stmt) +import Lang.Crucible.CFG.Reg qualified as Reg +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 +import What4.ProgramLoc (Posd(..)) + +-- | Parser hooks for macaw-aarch32-symbolic CFGs +aarch32ParserHooks :: LCSC.ParserHooks ext +aarch32ParserHooks = + LCSC.ParserHooks + { LCSC.extensionTypeParser = aarch32TypeParser + , LCSC.extensionParser = aarch32AtomParser + } + +--------------------------------------------------------------------- +-- 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 +aarch32RegTypes :: Ctx.Assignment LCT.TypeRepr (DMS.MacawCrucibleRegTypes ARM.ARM) +aarch32RegTypes = DMS.crucArchRegTypes AArch32.aarch32MacawSymbolicFns + +-- Helper, not exported +aarch32RegStructType :: LCT.TypeRepr (DMS.ArchRegStruct ARM.ARM) +aarch32RegStructType = LCT.StructRepr aarch32RegTypes + +-- | Parser for type extensions to Crucible syntax +aarch32TypeParser :: + LCSM.MonadSyntax LCSA.Atomic m => + m (Some LCT.TypeRepr) +aarch32TypeParser = do + namedAtom "AArch32Regs" + pure (Some aarch32RegStructType) + +--------------------------------------------------------------------- +-- Operations + +parseRegs :: + ( LCSM.MonadSyntax LCSA.Atomic m + , MonadIO m + , MonadState (LCSC.SyntaxState s) m + , MonadWriter [Posd (Stmt ext s)] m + , IsSyntaxExtension ext + , ?parserHooks :: LCSC.ParserHooks ext + ) => + m (Atom s (DMS.ArchRegStruct ARM.ARM)) +parseRegs = + LCSM.describe "a struct of AArch32 register values" $ do + assign <- LCSC.operands (Ctx.Empty Ctx.:> aarch32RegStructType) + pure (assign Ctx.! Ctx.baseIndex) + +parseReg :: LCSM.MonadSyntax LCSA.Atomic m => m (Some (Ctx.Index (DMS.MacawCrucibleRegTypes ARM.ARM))) +parseReg = + LCSM.describe "an AArch32 register" $ do + name <- LCSC.atomName + case name of + LCSA.AtomName "r0" -> pure (Some AArch32R.r0) + LCSA.AtomName "r1" -> pure (Some AArch32R.r1) + LCSA.AtomName "r2" -> pure (Some AArch32R.r2) + LCSA.AtomName "r3" -> pure (Some AArch32R.r3) + LCSA.AtomName "r4" -> pure (Some AArch32R.r4) + LCSA.AtomName "r5" -> pure (Some AArch32R.r5) + LCSA.AtomName "r6" -> pure (Some AArch32R.r6) + LCSA.AtomName "r7" -> pure (Some AArch32R.r7) + LCSA.AtomName "r8" -> pure (Some AArch32R.r8) + LCSA.AtomName "r9" -> pure (Some AArch32R.r9) + LCSA.AtomName "r10" -> pure (Some AArch32R.r10) + LCSA.AtomName "r11" -> pure (Some AArch32R.r11) + LCSA.AtomName "fp" -> pure (Some AArch32R.fp) + LCSA.AtomName "r12" -> pure (Some AArch32R.r12) + LCSA.AtomName "ip" -> pure (Some AArch32R.ip) + LCSA.AtomName "r13" -> pure (Some AArch32R.r13) + LCSA.AtomName "sp" -> pure (Some AArch32R.sp) + LCSA.AtomName "r14" -> pure (Some AArch32R.r14) + LCSA.AtomName "lr" -> pure (Some AArch32R.lr) + LCSA.AtomName "v0" -> pure (Some AArch32R.v0) + LCSA.AtomName "v1" -> pure (Some AArch32R.v1) + LCSA.AtomName "v2" -> pure (Some AArch32R.v2) + LCSA.AtomName "v3" -> pure (Some AArch32R.v3) + LCSA.AtomName "v4" -> pure (Some AArch32R.v4) + LCSA.AtomName "v5" -> pure (Some AArch32R.v5) + LCSA.AtomName "v6" -> pure (Some AArch32R.v6) + LCSA.AtomName "v7" -> pure (Some AArch32R.v7) + LCSA.AtomName "v8" -> pure (Some AArch32R.v8) + LCSA.AtomName "v9" -> pure (Some AArch32R.v9) + LCSA.AtomName "v10" -> pure (Some AArch32R.v10) + LCSA.AtomName "v11" -> pure (Some AArch32R.v11) + LCSA.AtomName "v12" -> pure (Some AArch32R.v12) + LCSA.AtomName "v13" -> pure (Some AArch32R.v13) + LCSA.AtomName "v14" -> pure (Some AArch32R.v14) + LCSA.AtomName "v15" -> pure (Some AArch32R.v15) + LCSA.AtomName "v16" -> pure (Some AArch32R.v16) + LCSA.AtomName "v17" -> pure (Some AArch32R.v17) + LCSA.AtomName "v18" -> pure (Some AArch32R.v18) + LCSA.AtomName "v19" -> pure (Some AArch32R.v19) + LCSA.AtomName "v20" -> pure (Some AArch32R.v20) + LCSA.AtomName "v21" -> pure (Some AArch32R.v21) + LCSA.AtomName "v22" -> pure (Some AArch32R.v22) + LCSA.AtomName "v23" -> pure (Some AArch32R.v23) + LCSA.AtomName "v24" -> pure (Some AArch32R.v24) + LCSA.AtomName "v25" -> pure (Some AArch32R.v25) + LCSA.AtomName "v26" -> pure (Some AArch32R.v26) + LCSA.AtomName "v27" -> pure (Some AArch32R.v27) + LCSA.AtomName "v28" -> pure (Some AArch32R.v28) + LCSA.AtomName "v29" -> pure (Some AArch32R.v29) + LCSA.AtomName "v30" -> pure (Some AArch32R.v30) + LCSA.AtomName "v31" -> pure (Some AArch32R.v31) + LCSA.AtomName _ -> empty + +aarch32AtomParser :: + ( LCSM.MonadSyntax LCSA.Atomic m + , MonadIO m + , MonadState (LCSC.SyntaxState s) m + , MonadWriter [Posd (Stmt ext s)] m + , IsSyntaxExtension ext + , ?parserHooks :: LCSC.ParserHooks ext + ) => + m (Some (Atom s)) +aarch32AtomParser = + LCSM.depCons LCSC.atomName $ + \case + LCSA.AtomName "get-reg" -> do + loc <- LCSM.position + (Some reg, regs) <- LCSM.cons parseReg parseRegs + let regTy = aarch32RegTypes Ctx.! reg + Some <$> LCSC.freshAtom loc (Reg.EvalApp (Expr.GetStruct regs reg regTy)) + LCSA.AtomName "set-reg" -> do + loc <- LCSM.position + LCSM.depCons parseReg $ \(Some reg) -> do + let regTy = aarch32RegTypes Ctx.! reg + assign <- LCSC.operands (Ctx.Empty Ctx.:> regTy Ctx.:> aarch32RegStructType) + let (rest, regs) = Ctx.decompose assign + let (Ctx.Empty, val) = Ctx.decompose rest + Some <$> LCSC.freshAtom loc (Reg.EvalApp (Expr.SetStruct aarch32RegTypes regs reg val)) + LCSA.AtomName _ -> empty diff --git a/macaw-aarch32-syntax/test-data/.gitignore b/macaw-aarch32-syntax/test-data/.gitignore new file mode 100644 index 00000000..f47cb204 --- /dev/null +++ b/macaw-aarch32-syntax/test-data/.gitignore @@ -0,0 +1 @@ +*.out diff --git a/macaw-aarch32-syntax/test-data/get-regs.cbl b/macaw-aarch32-syntax/test-data/get-regs.cbl new file mode 100644 index 00000000..d5c375a0 --- /dev/null +++ b/macaw-aarch32-syntax/test-data/get-regs.cbl @@ -0,0 +1,54 @@ +(defun @id ((regs AArch32Regs)) AArch32Regs + (start start: + (let r0 (get-reg r0 regs)) + (let r1 (get-reg r1 regs)) + (let r2 (get-reg r2 regs)) + (let r3 (get-reg r3 regs)) + (let r4 (get-reg r4 regs)) + (let r5 (get-reg r5 regs)) + (let r6 (get-reg r6 regs)) + (let r7 (get-reg r7 regs)) + (let r8 (get-reg r8 regs)) + (let r9 (get-reg r9 regs)) + (let r10 (get-reg r10 regs)) + (let r11 (get-reg r11 regs)) + (let fp (get-reg fp regs)) + (let r12 (get-reg r12 regs)) + (let ip (get-reg ip regs)) + (let r13 (get-reg r13 regs)) + (let sp (get-reg sp regs)) + (let r14 (get-reg r14 regs)) + (let lr (get-reg lr regs)) + (let v0 (get-reg v0 regs)) + (let v1 (get-reg v1 regs)) + (let v2 (get-reg v2 regs)) + (let v3 (get-reg v3 regs)) + (let v4 (get-reg v4 regs)) + (let v5 (get-reg v5 regs)) + (let v6 (get-reg v6 regs)) + (let v7 (get-reg v7 regs)) + (let v8 (get-reg v8 regs)) + (let v9 (get-reg v9 regs)) + (let v10 (get-reg v10 regs)) + (let v11 (get-reg v11 regs)) + (let v12 (get-reg v12 regs)) + (let v13 (get-reg v13 regs)) + (let v14 (get-reg v14 regs)) + (let v15 (get-reg v15 regs)) + (let v16 (get-reg v16 regs)) + (let v17 (get-reg v17 regs)) + (let v18 (get-reg v18 regs)) + (let v19 (get-reg v19 regs)) + (let v20 (get-reg v20 regs)) + (let v21 (get-reg v21 regs)) + (let v22 (get-reg v22 regs)) + (let v23 (get-reg v23 regs)) + (let v24 (get-reg v24 regs)) + (let v25 (get-reg v25 regs)) + (let v26 (get-reg v26 regs)) + (let v27 (get-reg v27 regs)) + (let v28 (get-reg v28 regs)) + (let v29 (get-reg v29 regs)) + (let v30 (get-reg v30 regs)) + (let v31 (get-reg v31 regs)) + (return regs))) diff --git a/macaw-aarch32-syntax/test-data/get-regs.out.good b/macaw-aarch32-syntax/test-data/get-regs.out.good new file mode 100644 index 00000000..e4997082 --- /dev/null +++ b/macaw-aarch32-syntax/test-data/get-regs.out.good @@ -0,0 +1,154 @@ +(defun @id ((regs AArch32Regs)) AArch32Regs + (start start: + (let r0 (get-reg r0 regs)) + (let r1 (get-reg r1 regs)) + (let r2 (get-reg r2 regs)) + (let r3 (get-reg r3 regs)) + (let r4 (get-reg r4 regs)) + (let r5 (get-reg r5 regs)) + (let r6 (get-reg r6 regs)) + (let r7 (get-reg r7 regs)) + (let r8 (get-reg r8 regs)) + (let r9 (get-reg r9 regs)) + (let r10 (get-reg r10 regs)) + (let r11 (get-reg r11 regs)) + (let fp (get-reg fp regs)) + (let r12 (get-reg r12 regs)) + (let ip (get-reg ip regs)) + (let r13 (get-reg r13 regs)) + (let sp (get-reg sp regs)) + (let r14 (get-reg r14 regs)) + (let lr (get-reg lr regs)) + (let v0 (get-reg v0 regs)) + (let v1 (get-reg v1 regs)) + (let v2 (get-reg v2 regs)) + (let v3 (get-reg v3 regs)) + (let v4 (get-reg v4 regs)) + (let v5 (get-reg v5 regs)) + (let v6 (get-reg v6 regs)) + (let v7 (get-reg v7 regs)) + (let v8 (get-reg v8 regs)) + (let v9 (get-reg v9 regs)) + (let v10 (get-reg v10 regs)) + (let v11 (get-reg v11 regs)) + (let v12 (get-reg v12 regs)) + (let v13 (get-reg v13 regs)) + (let v14 (get-reg v14 regs)) + (let v15 (get-reg v15 regs)) + (let v16 (get-reg v16 regs)) + (let v17 (get-reg v17 regs)) + (let v18 (get-reg v18 regs)) + (let v19 (get-reg v19 regs)) + (let v20 (get-reg v20 regs)) + (let v21 (get-reg v21 regs)) + (let v22 (get-reg v22 regs)) + (let v23 (get-reg v23 regs)) + (let v24 (get-reg v24 regs)) + (let v25 (get-reg v25 regs)) + (let v26 (get-reg v26 regs)) + (let v27 (get-reg v27 regs)) + (let v28 (get-reg v28 regs)) + (let v29 (get-reg v29 regs)) + (let v30 (get-reg v30 regs)) + (let v31 (get-reg v31 regs)) + (return regs))) + +id +%0 + % 3:13 + $1 = getStruct($0, 36, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 4:13 + $2 = getStruct($0, 37, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 5:13 + $3 = getStruct($0, 38, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 6:13 + $4 = getStruct($0, 39, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 7:13 + $5 = getStruct($0, 40, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 8:13 + $6 = getStruct($0, 41, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 9:13 + $7 = getStruct($0, 42, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 10:13 + $8 = getStruct($0, 43, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 11:13 + $9 = getStruct($0, 44, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 12:13 + $10 = getStruct($0, 45, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 13:14 + $11 = getStruct($0, 46, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 14:14 + $12 = getStruct($0, 47, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 16:14 + $13 = getStruct($0, 48, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 18:14 + $14 = getStruct($0, 49, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 20:14 + $15 = getStruct($0, 50, IntrinsicRepr LLVM_pointer [BVRepr 32]) + % 22:13 + $16 = getStruct($0, 51, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 23:13 + $17 = getStruct($0, 52, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 24:13 + $18 = getStruct($0, 53, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 25:13 + $19 = getStruct($0, 54, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 26:13 + $20 = getStruct($0, 55, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 27:13 + $21 = getStruct($0, 56, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 28:13 + $22 = getStruct($0, 57, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 29:13 + $23 = getStruct($0, 58, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 30:13 + $24 = getStruct($0, 59, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 31:13 + $25 = getStruct($0, 60, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 32:14 + $26 = getStruct($0, 61, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 33:14 + $27 = getStruct($0, 62, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 34:14 + $28 = getStruct($0, 63, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 35:14 + $29 = getStruct($0, 64, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 36:14 + $30 = getStruct($0, 65, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 37:14 + $31 = getStruct($0, 66, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 38:14 + $32 = getStruct($0, 67, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 39:14 + $33 = getStruct($0, 68, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 40:14 + $34 = getStruct($0, 69, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 41:14 + $35 = getStruct($0, 70, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 42:14 + $36 = getStruct($0, 71, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 43:14 + $37 = getStruct($0, 72, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 44:14 + $38 = getStruct($0, 73, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 45:14 + $39 = getStruct($0, 74, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 46:14 + $40 = getStruct($0, 75, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 47:14 + $41 = getStruct($0, 76, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 48:14 + $42 = getStruct($0, 77, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 49:14 + $43 = getStruct($0, 78, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 50:14 + $44 = getStruct($0, 79, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 51:14 + $45 = getStruct($0, 80, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 52:14 + $46 = getStruct($0, 81, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 53:14 + $47 = getStruct($0, 82, IntrinsicRepr LLVM_pointer [BVRepr 128]) + % 54:5 + return $0 + % no postdom diff --git a/macaw-aarch32-syntax/test-data/regs.cbl b/macaw-aarch32-syntax/test-data/regs.cbl new file mode 100644 index 00000000..b8135a41 --- /dev/null +++ b/macaw-aarch32-syntax/test-data/regs.cbl @@ -0,0 +1,3 @@ +(defun @id ((regs AArch32Regs)) AArch32Regs + (start start: + (return regs))) diff --git a/macaw-aarch32-syntax/test-data/regs.out.good b/macaw-aarch32-syntax/test-data/regs.out.good new file mode 100644 index 00000000..464abc86 --- /dev/null +++ b/macaw-aarch32-syntax/test-data/regs.out.good @@ -0,0 +1,8 @@ +(defun @id ((regs AArch32Regs)) AArch32Regs + (start start: (return regs))) + +id +%0 + % 3:5 + return $0 + % no postdom diff --git a/macaw-aarch32-syntax/test/Test.hs b/macaw-aarch32-syntax/test/Test.hs new file mode 100644 index 00000000..93186406 --- /dev/null +++ b/macaw-aarch32-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.ARM (ARM) +import Data.Macaw.AArch32.Symbolic () -- TraversableFC instance for (MacawExt ARM) statements and expressions +import Data.Macaw.AArch32.Symbolic.Syntax (aarch32ParserHooks) + +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 @ARM) aarch32ParserHooks + withFile outFile WriteMode $ doParseCheck inFile contents True +