Merge pull request #457 from GaloisInc/T349-riscv-sugar

`macaw-riscv-syntax`: Syntactic sugar for RISC-V CFGs

.github/workflows/ci.yaml

@@ -164,6 +164,10 @@ jobs:
       if: runner.os == 'Linux'
       run: cabal test pkg:macaw-riscv-symbolic
 
+    - name: Test macaw-riscv-syntax
+      if: runner.os == 'Linux'
+      run: cabal test pkg:macaw-riscv-syntax
+
     - name: Build macaw-refinement
       run: cabal build pkg:macaw-refinement
 

cabal.project.dist

@@ -9,6 +9,7 @@ packages: base/
           macaw-ppc-syntax/
           macaw-riscv/
           macaw-riscv-symbolic/
+          macaw-riscv-syntax/
           macaw-x86-cli/
           macaw-x86-syntax/
           x86/

macaw-riscv-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.

macaw-riscv-syntax/README.md

@@ -0,0 +1,176 @@
+# macaw-riscv-syntax
+
+This package provides concrete syntax for macaw-riscv-symbolic types and
+operations.
+
+Concretely, it implements `ParserHooks` for use with [`crucible-syntax`][syn].
+Note that we provide separate `ParserHooks` for RISCV32 (32-bit RISC-V) and
+RISCV64 (64-bit RISC-V), as the register types are separate in each variant of
+RISC-V. Nevertheless, many operations work over both RISCV32 and RISCV64 alike.
+
+The `ParserHooks` support the following types and operations:
+
+**Types**:
+
+- `RISCV32Regs`: the struct of all RISCV32 registers (not available on RISCV64)
+- `RISCV64Regs`: the struct of all RISCV64 registers (not available on RISCV32)
+
+**Operations**:
+
+- `get-reg :: RISCV{32,64}Reg -> RISCV{32,64}Regs -> t`: extract a RISC-V register
+- `set-reg :: RISCV{32,64}Reg -> t -> RISCV{32,64}Regs -> RISCV{32,64}Regs`: set a RISC-V register
+- Registers:
+  - `pc :: RISCV{32,64}Reg`
+  - `ra :: RISCV{32,64}Reg`, AKA `x1`
+  - `sp :: RISCV{32,64}Reg`, AKA `x2`
+  - `gp :: RISCV{32,64}Reg`, AKA `x3`
+  - `tp :: RISCV{32,64}Reg`, AKA `x4`
+  - `t0 :: RISCV{32,64}Reg`, AKA `x5`
+  - `t1 :: RISCV{32,64}Reg`, AKA `x6`
+  - `t2 :: RISCV{32,64}Reg`, AKA `x7`
+  - `s0 :: RISCV{32,64}Reg`, AKA `x8`
+  - `s1 :: RISCV{32,64}Reg`, AKA `x9`
+  - `a0 :: RISCV{32,64}Reg`, AKA `x10`
+  - `a1 :: RISCV{32,64}Reg`, AKA `x11`
+  - `a2 :: RISCV{32,64}Reg`, AKA `x12`
+  - `a3 :: RISCV{32,64}Reg`, AKA `x13`
+  - `a4 :: RISCV{32,64}Reg`, AKA `x14`
+  - `a5 :: RISCV{32,64}Reg`, AKA `x15`
+  - `a6 :: RISCV{32,64}Reg`, AKA `x16`
+  - `a7 :: RISCV{32,64}Reg`, AKA `x17`
+  - `s2 :: RISCV{32,64}Reg`, AKA `x18`
+  - `s3 :: RISCV{32,64}Reg`, AKA `x19`
+  - `s4 :: RISCV{32,64}Reg`, AKA `x20`
+  - `s5 :: RISCV{32,64}Reg`, AKA `x21`
+  - `s6 :: RISCV{32,64}Reg`, AKA `x22`
+  - `s7 :: RISCV{32,64}Reg`, AKA `x23`
+  - `s8 :: RISCV{32,64}Reg`, AKA `x24`
+  - `s9 :: RISCV{32,64}Reg`, AKA `x25`
+  - `s10 :: RISCV{32,64}Reg`, AKA `x26`
+  - `s11 :: RISCV{32,64}Reg`, AKA `x27`
+  - `t3 :: RISCV{32,64}Reg`, AKA `x29`
+  - `t4 :: RISCV{32,64}Reg`, AKA `x29`
+  - `t5 :: RISCV{32,64}Reg`, AKA `x30`
+  - `t6 :: RISCV{32,64}Reg`, AKA `x31`
+  - `x1 :: RISCV{32,64}Reg`, AKA `ra`
+  - `x2 :: RISCV{32,64}Reg`, AKA `sp`
+  - `x3 :: RISCV{32,64}Reg`, AKA `gp`
+  - `x4 :: RISCV{32,64}Reg`, AKA `tp`
+  - `x5 :: RISCV{32,64}Reg`, AKA `t0`
+  - `x6 :: RISCV{32,64}Reg`, AKA `t1`
+  - `x7 :: RISCV{32,64}Reg`, AKA `t2`
+  - `x8 :: RISCV{32,64}Reg`, AKA `s0`
+  - `x9 :: RISCV{32,64}Reg`, AKA `s1`
+  - `x10 :: RISCV{32,64}Reg`, AKA `a0`
+  - `x11 :: RISCV{32,64}Reg`, AKA `a1`
+  - `x12 :: RISCV{32,64}Reg`, AKA `a2`
+  - `x13 :: RISCV{32,64}Reg`, AKA `a3`
+  - `x14 :: RISCV{32,64}Reg`, AKA `a4`
+  - `x15 :: RISCV{32,64}Reg`, AKA `a5`
+  - `x16 :: RISCV{32,64}Reg`, AKA `a6`
+  - `x17 :: RISCV{32,64}Reg`, AKA `a7`
+  - `x18 :: RISCV{32,64}Reg`, AKA `s2`
+  - `x19 :: RISCV{32,64}Reg`, AKA `s3`
+  - `x20 :: RISCV{32,64}Reg`, AKA `s4`
+  - `x21 :: RISCV{32,64}Reg`, AKA `s5`
+  - `x22 :: RISCV{32,64}Reg`, AKA `s6`
+  - `x23 :: RISCV{32,64}Reg`, AKA `s7`
+  - `x24 :: RISCV{32,64}Reg`, AKA `s8`
+  - `x25 :: RISCV{32,64}Reg`, AKA `s9`
+  - `x26 :: RISCV{32,64}Reg`, AKA `s10`
+  - `x27 :: RISCV{32,64}Reg`, AKA `s11`
+  - `x28 :: RISCV{32,64}Reg`, AKA `t3`
+  - `x29 :: RISCV{32,64}Reg`, AKA `t4`
+  - `x30 :: RISCV{32,64}Reg`, AKA `t5`
+  - `x31 :: RISCV{32,64}Reg`, AKA `t6`
+  - `ft0 :: RISCV{32,64}Reg`, AKA `f0`
+  - `ft1 :: RISCV{32,64}Reg`, AKA `f1`
+  - `ft2 :: RISCV{32,64}Reg`, AKA `f2`
+  - `ft3 :: RISCV{32,64}Reg`, AKA `f3`
+  - `ft4 :: RISCV{32,64}Reg`, AKA `f4`
+  - `ft5 :: RISCV{32,64}Reg`, AKA `f5`
+  - `ft6 :: RISCV{32,64}Reg`, AKA `f6`
+  - `ft7 :: RISCV{32,64}Reg`, AKA `f7`
+  - `fs0 :: RISCV{32,64}Reg`, AKA `f8`
+  - `fs1 :: RISCV{32,64}Reg`, AKA `f9`
+  - `fa0 :: RISCV{32,64}Reg`, AKA `f10`
+  - `fa1 :: RISCV{32,64}Reg`, AKA `f11`
+  - `fa2 :: RISCV{32,64}Reg`, AKA `f12`
+  - `fa3 :: RISCV{32,64}Reg`, AKA `f13`
+  - `fa4 :: RISCV{32,64}Reg`, AKA `f14`
+  - `fa5 :: RISCV{32,64}Reg`, AKA `f15`
+  - `fa6 :: RISCV{32,64}Reg`, AKA `f16`
+  - `fa7 :: RISCV{32,64}Reg`, AKA `f17`
+  - `fs2 :: RISCV{32,64}Reg`, AKA `f18`
+  - `fs3 :: RISCV{32,64}Reg`, AKA `f19`
+  - `fs4 :: RISCV{32,64}Reg`, AKA `f2`
+  - `fs5 :: RISCV{32,64}Reg`, AKA `f21`
+  - `fs6 :: RISCV{32,64}Reg`, AKA `f22`
+  - `fs7 :: RISCV{32,64}Reg`, AKA `f23`
+  - `fs8 :: RISCV{32,64}Reg`, AKA `f24`
+  - `fs9 :: RISCV{32,64}Reg`, AKA `f25`
+  - `fs10 :: RISCV{32,64}Reg`, AKA `f26`
+  - `fs11 :: RISCV{32,64}Reg`, AKA `f27`
+  - `ft8 :: RISCV{32,64}Reg`, AKA `f28`
+  - `ft9 :: RISCV{32,64}Reg`, AKA `f29`
+  - `ft10 :: RISCV{32,64}Reg`, AKA `f30`
+  - `ft11 :: RISCV{32,64}Reg`, AKA `f31`
+  - `f0 :: RISCV{32,64}Reg`, AKA `ft0`
+  - `f1 :: RISCV{32,64}Reg`, AKA `ft1`
+  - `f2 :: RISCV{32,64}Reg`, AKA `ft2`
+  - `f3 :: RISCV{32,64}Reg`, AKA `ft3`
+  - `f4 :: RISCV{32,64}Reg`, AKA `ft4`
+  - `f5 :: RISCV{32,64}Reg`, AKA `ft5`
+  - `f6 :: RISCV{32,64}Reg`, AKA `ft6`
+  - `f7 :: RISCV{32,64}Reg`, AKA `ft7`
+  - `f8 :: RISCV{32,64}Reg`, AKA `fs0`
+  - `f9 :: RISCV{32,64}Reg`, AKA `fs1`
+  - `f10 :: RISCV{32,64}Reg`, AKA `fa0`
+  - `f11 :: RISCV{32,64}Reg`, AKA `fa1`
+  - `f12 :: RISCV{32,64}Reg`, AKA `fa2`
+  - `f13 :: RISCV{32,64}Reg`, AKA `fa3`
+  - `f14 :: RISCV{32,64}Reg`, AKA `fa4`
+  - `f15 :: RISCV{32,64}Reg`, AKA `fa5`
+  - `f16 :: RISCV{32,64}Reg`, AKA `fa6`
+  - `f17 :: RISCV{32,64}Reg`, AKA `fa7`
+  - `f18 :: RISCV{32,64}Reg`, AKA `fs2`
+  - `f19 :: RISCV{32,64}Reg`, AKA `fs3`
+  - `f20 :: RISCV{32,64}Reg`, AKA `fs4`
+  - `f21 :: RISCV{32,64}Reg`, AKA `fs5`
+  - `f22 :: RISCV{32,64}Reg`, AKA `fs6`
+  - `f23 :: RISCV{32,64}Reg`, AKA `fs7`
+  - `f24 :: RISCV{32,64}Reg`, AKA `fs8`
+  - `f25 :: RISCV{32,64}Reg`, AKA `fs9`
+  - `f26 :: RISCV{32,64}Reg`, AKA `fs10`
+  - `f27 :: RISCV{32,64}Reg`, AKA `fs11`
+  - `f28 :: RISCV{32,64}Reg`, AKA `ft8`
+  - `f29 :: RISCV{32,64}Reg`, AKA `ft9`
+  - `f30 :: RISCV{32,64}Reg`, AKA `ft10`
+  - `f31 :: RISCV{32,64}Reg`, AKA `ft11`
+  - `mvendorid :: RISCV{32,64}Reg`
+  - `marchid :: RISCV{32,64}Reg`
+  - `mimpid :: RISCV{32,64}Reg`
+  - `mhartid :: RISCV{32,64}Reg`
+  - `mstatus :: RISCV{32,64}Reg`
+  - `misa :: RISCV{32,64}Reg`
+  - `medeleg :: RISCV{32,64}Reg`
+  - `mideleg :: RISCV{32,64}Reg`
+  - `mie :: RISCV{32,64}Reg`
+  - `mtvec :: RISCV{32,64}Reg`
+  - `mcounteren :: RISCV{32,64}Reg`
+  - `mscratch :: RISCV{32,64}Reg`
+  - `mepc :: RISCV{32,64}Reg`
+  - `mcause :: RISCV{32,64}Reg`
+  - `mtval :: RISCV{32,64}Reg`
+  - `mip :: RISCV{32,64}Reg`
+  - `mcycle :: RISCV{32,64}Reg`
+  - `minstret :: RISCV{32,64}Reg`
+  - `mcycleh :: RISCV{32,64}Reg`
+  - `minstreth :: RISCV{32,64}Reg`
+  - `frm :: RISCV{32,64}Reg`
+  - `fflags :: RISCV{32,64}Reg`
+  - `fcsr :: RISCV{32,64}Reg`
+  - `priv :: RISCV{32,64}Reg`
+  - `exc :: RISCV{32,64}Reg`
+
+[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax

macaw-riscv-syntax/macaw-riscv-syntax.cabal

@@ -0,0 +1,130 @@
+Cabal-version: 2.2
+Name:          macaw-riscv-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 macaw-riscv-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,
+    grift,
+    macaw-base,
+    macaw-riscv,
+    macaw-riscv-symbolic,
+    macaw-symbolic,
+    mtl,
+    parameterized-utils,
+    text,
+    what4,
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.Macaw.RISCV.Symbolic.Syntax
+
+test-suite macaw-riscv-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,
+    Glob,
+    grift,
+    macaw-base,
+    macaw-riscv,
+    macaw-riscv-syntax,
+    macaw-symbolic,
+    macaw-symbolic-syntax,
+    parameterized-utils >= 0.1.7,
+    tasty,
+    tasty-golden,
+    text,