diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml index 3a22fd5cd..c51a1f7a8 100644 --- a/.github/workflows/crux-llvm-build.yml +++ b/.github/workflows/crux-llvm-build.yml @@ -150,11 +150,12 @@ jobs: setup_src() { if [ ! -f Setup.hs ] ; then defsetup > DefSetup.hs; fi; ls *Setup.hs; } setup_bin() { echo setup.${{ matrix.ghc }}; } with_ghc() { $NS -c ${@}; } - (cd crucible; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) - (cd crucible-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) - (cd crux; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) - (cd crux-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) - (cd uc-crux-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crucible; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crucible-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crucible-llvm-syntax; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crux; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd crux-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) + (cd uc-crux-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean) - shell: bash @@ -162,6 +163,7 @@ jobs: - shell: bash run: | + .github/ci.sh build lib:crucible-llvm-syntax .github/ci.sh build exe:crux-llvm .github/ci.sh build exe:crux-llvm-for-ide .github/ci.sh build exe:crux-llvm-svcomp @@ -169,7 +171,7 @@ jobs: - shell: bash name: Haddock - run: cabal v2-haddock crucible-symio crucible-llvm crux-llvm uc-crux-llvm + run: cabal v2-haddock crucible-symio crucible-llvm{,-syntax} crux-llvm uc-crux-llvm - shell: bash name: Test crucible @@ -189,6 +191,11 @@ jobs: LLVM_AS: "llvm-as-12" CLANG: "clang-12" + - shell: bash + name: Test crucible-llvm-syntax (Linux) + run: .github/ci.sh test crucible-llvm-syntax + if: runner.os == 'Linux' + - shell: bash name: Test crux-llvm (Linux) run: .github/ci.sh test crux-llvm diff --git a/.github/workflows/uc-crux-llvm-lint.yaml b/.github/workflows/uc-crux-llvm-lint.yaml index 6ef5f116e..437fb3951 100644 --- a/.github/workflows/uc-crux-llvm-lint.yaml +++ b/.github/workflows/uc-crux-llvm-lint.yaml @@ -16,11 +16,14 @@ jobs: - shell: bash run: | - cd uc-crux-llvm/ curl --location -o hlint.tar.gz \ https://github.com/ndmitchell/hlint/releases/download/v3.3/hlint-3.3-x86_64-linux.tar.gz tar xvf hlint.tar.gz - ./hlint-3.3/hlint exe src test + + (cd crucible-llvm-syntax/; ../hlint-3.3/hlint src test) + + cd uc-crux-llvm/ + ../hlint-3.3/hlint exe src test - uses: mrkkrp/ormolu-action@v2 # This is currently disabled, since it complains about diff --git a/cabal.project b/cabal.project index 6be2d3c9e..4fe55bd54 100644 --- a/cabal.project +++ b/cabal.project @@ -9,6 +9,7 @@ packages: crucible-go/ crucible-jvm/ crucible-llvm/ + crucible-llvm-syntax/ crucible-mir/ crucible-wasm/ crucible-syntax/ diff --git a/crucible-llvm-syntax/.hlint.yaml b/crucible-llvm-syntax/.hlint.yaml new file mode 100644 index 000000000..33e11424c --- /dev/null +++ b/crucible-llvm-syntax/.hlint.yaml @@ -0,0 +1,8 @@ +# HLint's default suggestions are opinionated, so we disable all of them by +# default and enable just a small subset we can agree on. + +- ignore: {} # ignore all +- error: { name: "Redundant do" } +- error: { name: "Unused LANGUAGE pragma" } +- error: { name: "Use unless" } +- error: { name: "Use when" } diff --git a/crucible-llvm-syntax/LICENSE b/crucible-llvm-syntax/LICENSE new file mode 100644 index 000000000..f01e82c96 --- /dev/null +++ b/crucible-llvm-syntax/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2023 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/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md new file mode 100644 index 000000000..7bccded00 --- /dev/null +++ b/crucible-llvm-syntax/README.md @@ -0,0 +1,37 @@ +# crucible-llvm-syntax + +This package provides concrete syntax for Crucible-LLVM types and operations. + +Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn]. +This `ParserHooks` supports the following types, primitive atoms, and +statements: + +**Types**: + +- `(Ptr n)` for a positive numeral `n` represents the type of LLVM pointers that are `n` bits wide; for example `(Ptr 8)` is the type of bytes + +**Primitive atoms**: + +- `none : Alignment`: no alignment +- `i8 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 8 :: MemType` +- `i16 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 16 :: MemType` +- `i32 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 32 :: MemType` +- `i64 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 64 :: MemType` +- `ptr : LLVMType`: [LLVM docs][ptr-type], corresponds to Crucible-LLVM's `PtrOpaqueType :: MemType` + +[int-type]: https://llvm.org/docs/LangRef.html#integer-type +[ptr-type]: https://llvm.org/docs/LangRef.html#pointer-type + +**Statements**: + +If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral, + +- `ptr : Nat -> Bitvector n -> Ptr n`: construct a pointer from a block and offset +- `ptr-block : Ptr n -> Nat`: get the block number of a pointer +- `ptr-offset : Ptr n -> Bitvector n`: get the offset of a pointer +- `ptr-ite : Bool -> Ptr n -> Ptr n -> Ptr n`: if-then-else for pointers +- `alloca : Alignment -> Bitvector w -> Ptr w`: allocate space on the stack +- `load : Alignment -> LLVMType -> Ptr w -> T`: load a value from memory, where the type `T` is determined by the `LLVMType` +- `store : Alignment -> LLVMType -> Ptr w -> T -> Unit`: store a value to memory, where the type `T` is determined by the `LLVMType` + +[syn]: ../crucible-syntax diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal new file mode 100644 index 000000000..aca0ae3a1 --- /dev/null +++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal @@ -0,0 +1,126 @@ +Cabal-version: 2.2 +Name: crucible-llvm-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 reading and writing Crucible-LLVM 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, + crucible >= 0.1, + crucible-llvm, + crucible-syntax, + mtl, + parameterized-utils >= 0.1.7, + prettyprinter, + text, + what4, + + hs-source-dirs: src + + exposed-modules: + Lang.Crucible.LLVM.Syntax + +test-suite crucible-llvm-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-llvm, + crucible-llvm-syntax, + crucible-syntax, + filepath, + parameterized-utils >= 0.1.7, + tasty, + tasty-golden, + text, diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs new file mode 100644 index 000000000..71bce2c27 --- /dev/null +++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs @@ -0,0 +1,186 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} + +module Lang.Crucible.LLVM.Syntax (llvmParserHooks) where + +import Control.Applicative (empty) +import Control.Monad (unless) +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.State.Strict (MonadState(..)) +import Control.Monad.Writer.Strict (MonadWriter(..)) +import Data.Functor ((<&>)) + +import Prettyprinter (pretty) + +import Data.Parameterized.Context qualified as Ctx +import Data.Parameterized.Some (Some(..)) + +import What4.ProgramLoc (Posd(..)) + +import Lang.Crucible.CFG.Expr qualified as Expr +import Lang.Crucible.CFG.Reg (Atom, GlobalVar, Stmt) +import Lang.Crucible.CFG.Reg qualified as Reg +import Lang.Crucible.CFG.Extension (IsSyntaxExtension) +import Lang.Crucible.Types (TypeRepr(..)) + +import Lang.Crucible.LLVM.DataLayout (Alignment) +import Lang.Crucible.LLVM.DataLayout qualified as DataLayout +import Lang.Crucible.LLVM.Extension (LLVM) +import Lang.Crucible.LLVM.Extension qualified as Ext +import Lang.Crucible.LLVM.MemModel (Mem, pattern LLVMPointerRepr) +import Lang.Crucible.LLVM.MemModel qualified as Mem +import Lang.Crucible.LLVM.MemType (MemType) +import Lang.Crucible.LLVM.MemType qualified as MemType +import Lang.Crucible.LLVM.Translation (llvmTypeAsRepr) + +import Lang.Crucible.Syntax.Atoms (Atomic) +import Lang.Crucible.Syntax.Atoms qualified as Atom +import Lang.Crucible.Syntax.Concrete (ParserHooks(..), SyntaxState) +import Lang.Crucible.Syntax.Concrete qualified as Parse +import Lang.Crucible.Syntax.ExprParse (MonadSyntax) +import Lang.Crucible.Syntax.ExprParse qualified as Parse + +-- | Like 'Lang.Crucible.Syntax.Concrete.Unary', but takes an arbitrary parser +-- for its first argument. +unary :: MonadSyntax Atomic m => m b -> m a -> m a +unary p0 p = Parse.followedBy p0 (Parse.commit *> Parse.cons p Parse.emptyList) <&> fst + +llvmParserHooks :: + Mem.HasPtrWidth w => + GlobalVar Mem -> + ParserHooks LLVM +llvmParserHooks mvar = + ParserHooks + { extensionTypeParser = llvmTypeParser + , extensionParser = llvmAtomParser mvar + } + +llvmTypeParser :: MonadSyntax Atomic m => m (Some TypeRepr) +llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType + where + ptrType :: MonadSyntax Atomic m => m (Some TypeRepr) + ptrType = do + let ptrName = do + s <- Parse.atomName + unless (s == Atom.AtomName "Ptr") Parse.cut + let -- This type signature is needed for GHC 8.10 + ptrWidth :: MonadSyntax Atomic m => m (Some TypeRepr) + ptrWidth = do + Parse.BoundedNat n <- Parse.posNat + pure (Some (LLVMPointerRepr n)) + unary ptrName ptrWidth + +llvmAtomParser :: + ( MonadSyntax Atomic m + , MonadWriter [Posd (Stmt LLVM s)] m + , MonadState (SyntaxState s) m + , MonadIO m + , IsSyntaxExtension LLVM + , ?parserHooks :: ParserHooks LLVM + , Mem.HasPtrWidth w + ) => + GlobalVar Mem -> + m (Some (Atom s)) +llvmAtomParser mvar = + Parse.depCons Parse.atomName $ + \case + Atom.AtomName "ptr" -> Parse.describe "LLVM ptr arguments" $ do + loc <- Parse.position + Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do + assign <- Parse.operands (Ctx.Empty Ctx.:> NatRepr Ctx.:> BVRepr w) + let (rest, off) = Ctx.decompose assign + let (Ctx.Empty, blk) = Ctx.decompose rest + let expr = Ext.LLVM_PointerExpr w blk off + ptrAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr)) + return (Some ptrAtom) + + Atom.AtomName "ptr-block" -> Parse.describe "LLVM ptr-block arguments" $ do + loc <- Parse.position + Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do + assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr w) + let (Ctx.Empty, ptr) = Ctx.decompose assign + let expr = Ext.LLVM_PointerBlock w ptr + Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr)) + + Atom.AtomName "ptr-offset" -> Parse.describe "LLVM ptr-offset arguments" $ do + loc <- Parse.position + Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do + assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr w) + let (Ctx.Empty, ptr) = Ctx.decompose assign + let expr = Ext.LLVM_PointerOffset w ptr + Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr)) + + Atom.AtomName "ptr-ite" -> Parse.describe "LLVM ptr-ite arguments" $ do + loc <- Parse.position + Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do + assign <- Parse.operands (Ctx.Empty Ctx.:> BoolRepr Ctx.:> LLVMPointerRepr w Ctx.:> LLVMPointerRepr w) + let (rest, p2) = Ctx.decompose assign + let (rest', p1) = Ctx.decompose rest + let (Ctx.Empty, b) = Ctx.decompose rest' + let expr = Ext.LLVM_PointerIte w b p1 p2 + Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr)) + + Atom.AtomName "alloca" -> Parse.describe "LLVM alloca arguments" $ do + loc <- Parse.position + (align, assign) <- + Parse.cons + parseAlign + (Parse.operands (Ctx.Empty Ctx.:> BVRepr ?ptrWidth)) + let (Ctx.Empty, sz) = Ctx.decompose assign + let stmt = Ext.LLVM_Alloca ?ptrWidth mvar sz align (show (pretty loc)) + Some <$> Parse.freshAtom loc (Reg.EvalExt stmt) + + Atom.AtomName "load" -> Parse.describe "LLVM load arguments" $ do + loc <- Parse.position + (align, (memTy, assign)) <- + Parse.cons + parseAlign + (Parse.cons + parseMemType + (Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth))) + llvmTypeAsRepr memTy $ \tyRep -> do + case Mem.toStorableType memTy of + Nothing -> empty + Just storTy -> do + let (Ctx.Empty, ptr) = Ctx.decompose assign + let stmt = Ext.LLVM_Load mvar ptr tyRep storTy align + Some <$> Parse.freshAtom loc (Reg.EvalExt stmt) + + Atom.AtomName "store" -> Parse.describe "LLVM store arguments" $ do + loc <- Parse.position + Parse.depCons parseAlign $ \align -> + Parse.depCons parseMemType $ \memTy -> + llvmTypeAsRepr memTy $ \tyRep -> do + assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth Ctx.:> tyRep) + case Mem.toStorableType memTy of + Nothing -> empty + Just storTy -> do + let (rest, val) = Ctx.decompose assign + let (Ctx.Empty, ptr) = Ctx.decompose rest + let stmt = Ext.LLVM_Store mvar ptr tyRep storTy align val + Some <$> Parse.freshAtom loc (Reg.EvalExt stmt) + + _ -> empty + where + parseAlign :: MonadSyntax Atomic m => m Alignment + parseAlign = Parse.describe "alignment" $ do + s <- Parse.atomName + unless (s == Atom.AtomName "none") Parse.cut + pure DataLayout.noAlignment + + parseMemType :: MonadSyntax Atomic m => m MemType + parseMemType = Parse.describe "LLVM type" $ do + nm <- Parse.atomName + case nm of + Atom.AtomName "i8" -> pure (MemType.IntType 8) + Atom.AtomName "i16" -> pure (MemType.IntType 16) + Atom.AtomName "i32" -> pure (MemType.IntType 32) + Atom.AtomName "i64" -> pure (MemType.IntType 64) + Atom.AtomName "ptr" -> pure MemType.PtrOpaqueType + _ -> empty diff --git a/crucible-llvm-syntax/test-data/.gitignore b/crucible-llvm-syntax/test-data/.gitignore new file mode 100644 index 000000000..f47cb2045 --- /dev/null +++ b/crucible-llvm-syntax/test-data/.gitignore @@ -0,0 +1 @@ +*.out diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl new file mode 100644 index 000000000..4faec82c8 --- /dev/null +++ b/crucible-llvm-syntax/test-data/ptr.cbl @@ -0,0 +1,24 @@ +(defun @test-ptr () (Ptr 64) + (start start: + (let blk0 (the Nat 0)) + (let off0 (bv 64 0)) + (let p0 (ptr 64 blk0 off0)) + (let p (ptr-ite 64 #t p0 p0)) + (let blk (ptr-block 64 p)) + (let off (ptr-offset 64 p)) + (assert! (equal? blk0 blk) "block numbers equal") + (assert! (equal? off0 off) "offsets equal") + + (let sz (bv 64 1)) + (let a (alloca none sz)) + (let vblk0 (the Nat 0)) + (let voff0 (bv 8 255)) + (let v0 (ptr 8 vblk0 voff0)) + (store none i8 a v0) + (let v (load none i8 a)) + (let vblk (ptr-block 8 v)) + (let voff (ptr-offset 8 v)) + (assert! (equal? vblk0 vblk) "stored block numbers equal") + (assert! (equal? voff0 voff) "stored offsets equal") + + (return p))) diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good new file mode 100644 index 000000000..691192e90 --- /dev/null +++ b/crucible-llvm-syntax/test-data/ptr.out.good @@ -0,0 +1,82 @@ +(defun @test-ptr () (Ptr 64) + (start start: + (let blk0 (the Nat 0)) + (let off0 (bv 64 0)) + (let p0 (ptr 64 blk0 off0)) + (let p (ptr-ite 64 #t p0 p0)) + (let blk (ptr-block 64 p)) + (let off (ptr-offset 64 p)) + (assert! (equal? blk0 blk) "block numbers equal") + (assert! (equal? off0 off) "offsets equal") + (let sz (bv 64 1)) + (let a (alloca none sz)) + (let vblk0 (the Nat 0)) + (let voff0 (bv 8 255)) + (let v0 (ptr 8 vblk0 voff0)) + (store none i8 a v0) + (let v (load none i8 a)) + (let vblk (ptr-block 8 v)) + (let voff (ptr-offset 8 v)) + (assert! (equal? vblk0 vblk) "stored block numbers equal") + (assert! (equal? voff0 voff) "stored offsets equal") + (return p))) + +test-ptr +%0 + % 3:15 + $0 = natLit(0) + % 4:15 + $1 = bVLit(64, BV 0) + % 5:13 + $2 = extensionApp(pointerExpr $0 $1) + % 6:12 + $3 = boolLit(True) + % 6:12 + $4 = extensionApp(pointerIte $3 $2 $2) + % 7:14 + $5 = extensionApp(pointerBlock $4) + % 8:14 + $6 = extensionApp(pointerOffset $4) + % 9:14 + $7 = natEq($0, $5) + % 9:32 + $8 = stringLit("block numbers equal") + % 9:5 + assert($7, $8) + % 10:14 + $9 = baseIsEq(BaseBVRepr 64, $1, $6) + % 10:32 + $10 = stringLit("offsets equal") + % 10:5 + assert($9, $10) + % 12:13 + $11 = bVLit(64, BV 1) + % 13:12 + $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12 + % 15:16 + $13 = bVLit(8, BV 255) + % 16:13 + $14 = extensionApp(pointerExpr $0 $13) + % 17:5 + $15 = store crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0 $14 + % 18:12 + $16 = load crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0 + % 19:15 + $17 = extensionApp(pointerBlock $16) + % 20:15 + $18 = extensionApp(pointerOffset $16) + % 21:14 + $19 = natEq($0, $17) + % 21:34 + $20 = stringLit("stored block numbers equal") + % 21:5 + assert($19, $20) + % 22:14 + $21 = baseIsEq(BaseBVRepr 8, $13, $18) + % 22:34 + $22 = stringLit("stored offsets equal") + % 22:5 + assert($21, $22) + % 24:5 + return $4 + % no postdom diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs new file mode 100644 index 000000000..507e1c6e0 --- /dev/null +++ b/crucible-llvm-syntax/test/Test.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} + +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 Data.Parameterized.NatRepr (knownNat) + +import Lang.Crucible.FunctionHandle (newHandleAllocator) + +import Lang.Crucible.LLVM.Extension (LLVM) +import Lang.Crucible.LLVM.MemModel (mkMemVar) + +import Lang.Crucible.Syntax.Concrete (ParserHooks) +import Lang.Crucible.Syntax.Prog (doParseCheck) + +import Lang.Crucible.LLVM.Syntax (llvmParserHooks) + +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" + +parserHooks :: IO (ParserHooks LLVM) +parserHooks = do + halloc <- newHandleAllocator + memVar <- mkMemVar "crucible-llvm-syntax-test-memory" halloc + let ?ptrWidth = knownNat @64 + return (llvmParserHooks memVar) + +testParser :: FilePath -> FilePath -> IO () +testParser inFile outFile = + do contents <- T.readFile inFile + hooks <- parserHooks + let ?parserHooks = hooks + withFile outFile WriteMode $ doParseCheck inFile contents True + diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs index d21626813..eb322bbe9 100644 --- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs +++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs @@ -43,6 +43,9 @@ module Lang.Crucible.Syntax.Concrete , string , isType , operands + , BoundedNat(..) + , PosNat + , posNat -- * Rules for pretty-printing language syntax , printExpr ) diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs index da40054bc..58eb82960 100644 --- a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs +++ b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs @@ -30,6 +30,7 @@ import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(Some)) import qualified Lang.Crucible.CFG.Core as C +import Lang.Crucible.CFG.Extension (IsSyntaxExtension) import Lang.Crucible.CFG.Reg import Lang.Crucible.CFG.SSAConversion @@ -56,7 +57,8 @@ import What4.Solver (defaultLogData, runZ3InOverride) -- | The main loop body, useful for both the program and for testing. doParseCheck - :: FilePath -- ^ The name of the input (appears in source locations) + :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) + => FilePath -- ^ The name of the input (appears in source locations) -> Text -- ^ The contents of the input -> Bool -- ^ Whether to pretty-print the input data as well -> Handle -- ^ A handle that will receive the output @@ -72,7 +74,6 @@ doParseCheck fn theInput pprint outh = do when pprint $ forM_ v $ \e -> T.hPutStrLn outh (printExpr e) >> hPutStrLn outh "" - let ?parserHooks = defaultParserHooks cs <- top ng ha [] $ prog v case cs of Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e diff --git a/crucible-syntax/test/Tests.hs b/crucible-syntax/test/Tests.hs index a5cff8ab3..f12896ca7 100644 --- a/crucible-syntax/test/Tests.hs +++ b/crucible-syntax/test/Tests.hs @@ -95,6 +95,7 @@ goldenFileTestCase input test_action = testParser :: FilePath -> FilePath -> IO () testParser inFile outFile = do contents <- T.readFile inFile + let ?parserHooks = defaultParserHooks withFile outFile WriteMode $ doParseCheck inFile contents True testOptions :: [ConfigDesc]