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

.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,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

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: "Unused LANGUAGE pragma" }
+- 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/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 `IntType 64 :: PtrOpaqueType`
+
+[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

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:    [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:
+  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,