crucible-llvm-syntax: Concrete syntax for Crucible-LLVM

This commit introduces an instance of crucible-syntax's `ParserHooks` for the
LLVM language extension. It's far from optimal or complete, but later commits
can build on this foundation.

.github/workflows/crux-llvm-build.yml

@@ -150,26 +150,28 @@ 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
  run: .github/ci.sh configure
 
  - 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
  .github/ci.sh build exe:uc-crux-llvm
 
  - 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

.github/workflows/uc-crux-llvm-lint.yaml

@@ -16,11 +16,16 @@ 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
+
+ pushd crucible-llvm-syntax/
+ ../hlint-3.3/hlint src test
+ popd
+
+ cd uc-crux-llvm/
+ ../hlint-3.3/hlint exe src test
 
  - uses: mrkkrp/ormolu-action@v2
  # This is currently disabled, since it complains about

cabal.project

@@ -9,6 +9,7 @@ packages:
  crucible-go/
  crucible-jvm/
  crucible-llvm/
+ crucible-llvm-syntax/
  crucible-mir/
  crucible-wasm/
  crucible-syntax/

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: "Use unless" }
+- error: { name: "Use when" }
+

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.

crucible-llvm-syntax/crucible-llvm-syntax.cabal

@@ -0,0 +1,124 @@
+Cabal-version: 2.2
+Name: crucible-llvm-syntax
+Version: 0.1
+Author: Galois Inc.
+Maintainer: [email protected]
+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:
+
+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.16,
+ crucible >= 0.1,
+ crucible-llvm,
+ crucible-syntax,
+ mtl,
+ parameterized-utils >= 0.1.7,
+ text,
+ what4,
+
+ hs-source-dirs: src
+
+ exposed-modules:
+ Lang.Crucible.LLVM.Syntax
+
+test-suite crucible-llvm-syntax-tests
+ 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,
+ directory,
+ filepath,
+ parameterized-utils >= 0.1.7,
+ tasty,
+ tasty-golden,
+ tasty-hunit,
+ text,
+ what4,

crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs

@@ -0,0 +1,70 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Lang.Crucible.LLVM.Syntax where
+
+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 Data.Parameterized.NatRepr (knownNat)
+import Data.Parameterized.Some (Some(..))
+
+import What4.ProgramLoc (Posd(..))
+
+import Lang.Crucible.CFG.Reg (Atom(..), Stmt(..))
+import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
+import Lang.Crucible.Types (TypeRepr(..))
+
+import Lang.Crucible.LLVM.Extension (LLVM)
+import Lang.Crucible.LLVM.MemModel (pattern LLVMPointerRepr)
+
+import Lang.Crucible.Syntax.Atoms (Atomic)
+import Lang.Crucible.Syntax.Concrete (ParserHooks(..), SyntaxState)
+import Lang.Crucible.Syntax.ExprParse (MonadSyntax)
+import qualified Lang.Crucible.Syntax.Concrete as Parse
+import qualified Lang.Crucible.Syntax.ExprParse as Parse
+
+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 :: ParserHooks LLVM
+llvmParserHooks =
+ ParserHooks
+ { extensionTypeParser = llvmTypeParser
+ , extensionParser = llvmAtomParser
+ }
+
+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
+ atom <- Parse.string
+ unless (atom == "Ptr") Parse.cut
+
+ let ptrWidth = do
+ atom <- Parse.string
+ if atom == "64"
+ then pure (Some (LLVMPointerRepr (knownNat @64)))
+ else Parse.cut
+
+ unary ptrName ptrWidth
+
+llvmAtomParser ::
+ ( MonadSyntax Atomic m
+ , MonadWriter [Posd (Stmt ext s)] m
+ , MonadState (SyntaxState s) m
+ , MonadIO m
+ , IsSyntaxExtension ext
+ , ?parserHooks :: ParserHooks ext
+ ) =>
+ m (Some (Atom s))
+llvmAtomParser = Parse.cut

crucible-llvm-syntax/test-data/.gitignore

@@ -0,0 +1 @@
+*.out

crucible-llvm-syntax/test-data/ptr.cbl

@@ -0,0 +1,3 @@
+(defun @test-ptr ((_ ("Ptr" "64"))) Bool
+ (start start:
+ (return #t)))

crucible-llvm-syntax/test-data/ptr.out.good

@@ -0,0 +1,9 @@
+(defun @test-ptr ((_ "Ptr64")) Bool (start start: (return #t)))
+
+test-ptr
+%0
+ % 3:13
+ $1 = boolLit(True)
+ % 3:5
+ return $1
+ % no postdom