macaw-symbolic-syntax: Concrete syntax for macaw-symbolic CFGs

This code was ported from ambient-verifier.

.github/workflows/ci.yaml

@@ -95,6 +95,12 @@ jobs:
         YICES_VERSION: "2.6.2"
         CVC4_VERSION: "4.1.8"
 
+    - name: Build macaw-symbolic-syntax
+      run: cabal build pkg:macaw-symbolic-syntax
+
+    - name: Test macaw-symbolic-syntax
+      run: cabal test pkg:macaw-symbolic-syntax
+
     - name: Build macaw-x86
       run: cabal build pkg:macaw-x86 pkg:macaw-x86-symbolic
 

cabal.project.dist

@@ -7,6 +7,7 @@ packages: base/
           macaw-riscv/
           x86/
           symbolic/
+          symbolic-syntax/
           x86_symbolic/
           refinement/
           utils/compare-dwarfdump
@@ -28,6 +29,7 @@ packages: base/
           deps/crucible/crucible/
           deps/crucible/crucible-llvm/
           deps/crucible/crucible-symio/
+          deps/crucible/crucible-syntax/
           deps/what4/what4/
           deps/dwarf/
           deps/elf-edit/

cabal.project.werror

@@ -7,6 +7,8 @@ package macaw-semmc
   ghc-options: -Wall
 package macaw-symbolic
   ghc-options: -Wall -Werror
+package macaw-symbolic-syntax
+  ghc-options: -Wall -Werror
 -- Macaw-ppc has warnings.
 package macaw-ppc
   ghc-options: -Wall -Werror

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

symbolic-syntax/README.md

@@ -0,0 +1,40 @@
+# macaw-symbolic-syntax
+
+This package provides concrete syntax for macaw-symbolic types and operations.
+
+Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn].
+This `ParserHooks` supports the following types and operations:
+
+**Types**:
+
+The main type addition is for representing pointers:
+
+- `Pointer`
+
+Unlike C/C++, these pointers are untyped and essentially correspond to `uint8_t*``.
+
+There are a few wrappers around `Bitvector` types for portability and convenience:
+
+- `Byte` is an alias for `Bitvector 8`.
+- `Int` is an alias for `Bitvector 32`.
+- `Long` is an alias for `Bitvector 32` on Arm32 and `Bitvector 64` on X86_64.
+- `PidT` is an alias for `Bitvector 32`.
+- `Short` is an alias for `Bitvector 16`.
+- `SizeT` is an alias for `Bitvector 32` on Arm32 and `Bitvector 64` on X86_64.
+- `UidT` is an alias for `Bitvector 32`.
+
+**Operations**:
+
+The extra operations are:
+
+- `bv-typed-literal :: Type -> Integer -> Bitvector w` where the first argument is a `Bitvector` type alias (see the Types section), the second argument is the value the `Bitvector` should contain, and `w` is the number of bits in the returned `Bitvector` (will match the width of the `Type` argument).
+- `fresh-vec :: String Unicode -> forall (t :: Type) -> Nat -> Vector t`, where ``(fresh-vec s t n)`` generates a length-`n` vector where each element is a fresh constant of type `t` with the name ``<s>_<i>`` (for each `i` between `0` and ``<n> - 1`). Note that `t` must be a scalar type (e.g., no nested `Vector`\ s), and `s` and `n` must both be concrete values.
+- `make-null :: Pointer` returns a null pointer.
+- `pointer-add :: Pointer -> Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64).
+- `pointer-diff :: Pointer -> Pointer -> Bitvector w` where `w` is the number of bits in a pointer (usually 32 or 64).
+- `pointer-sub :: Pointer -> Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64).
+- `pointer-eq :: Pointer -> Pointer -> Bool`.
+- `pointer-read :: forall (t :: Type) -> Endianness -> Pointer -> t` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)`` (for some positive number `w`) or one of the type aliases listed above.
+- `pointer-write :: forall (t :: Type) -> Endianness -> Pointer -> t -> Unit` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)`` (for some positive number `w`) or one of the type aliases listed above.
+
+[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax

symbolic-syntax/macaw-symbolic-syntax.cabal

@@ -0,0 +1,133 @@
+Cabal-version: 2.2
+Name:          macaw-symbolic-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 macaw-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 >= 0.1,
+    crucible-llvm,
+    crucible-syntax,
+    macaw-base,
+    macaw-symbolic,
+    mtl,
+    parameterized-utils >= 0.1.7,
+    prettyprinter,
+    text,
+    what4,
+    vector,
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.Macaw.Symbolic.Syntax
+
+test-suite macaw-symbolic-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,
+    filepath,
+    macaw-symbolic,
+    macaw-symbolic-syntax,
+    macaw-x86,
+    macaw-x86-symbolic,
+    parameterized-utils >= 0.1.7,
+    tasty,
+    tasty-golden,
+    text,
+