Implement macaw-riscv-symbolic

.github/workflows/ci.yaml

@@ -130,11 +130,15 @@ jobs:
       run: cabal test pkg:macaw-ppc-symbolic
 
     - name: Build macaw-riscv
-      run: cabal build pkg:macaw-riscv
+      run: cabal build pkg:macaw-riscv pkg:macaw-riscv-symbolic
 
     - name: Test macaw-riscv
       run: cabal test pkg:macaw-riscv
 
+    - name: Test macaw-riscv-symbolic
+      if: runner.os == 'Linux'
+      run: cabal test pkg:macaw-riscv-symbolic
+
     - name: Build macaw-refinement
       run: cabal build pkg:macaw-refinement
 

cabal.project.dist

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

macaw-ppc-symbolic/macaw-ppc-symbolic.cabal

@@ -19,11 +19,13 @@ library
   exposed-modules: Data.Macaw.PPC.Symbolic
   other-modules:   Data.Macaw.PPC.Symbolic.AtomWrapper
                    Data.Macaw.PPC.Symbolic.Functions
+                   Data.Macaw.PPC.Symbolic.Panic
                    Data.Macaw.PPC.Symbolic.Repeat
   -- other-extensions:
   build-depends:       base >=4.10 && <5,
                        containers,
                        lens,
+                       panic,
                        exceptions,
                        text,
                        parameterized-utils,

macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs

@@ -69,6 +69,7 @@ import qualified SemMC.Architecture.PPC as SP
 
 import qualified Data.Macaw.PPC.Symbolic.AtomWrapper as A
 import qualified Data.Macaw.PPC.Symbolic.Functions as F
+import qualified Data.Macaw.PPC.Symbolic.Panic as P
 import qualified Data.Macaw.PPC.Symbolic.Repeat as R
 
 ppcMacawSymbolicFns :: ( SP.KnownVariant v
@@ -219,7 +220,10 @@ archLookupReg :: ( MP.KnownVariant v
 archLookupReg regEntry reg =
   case lookupReg reg (MCR.regValue regEntry) of
     Just (MCRV.RV val) -> MCR.RegEntry (MS.typeToCrucible $ MT.typeRepr reg) val
-    Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
+    Nothing -> P.panic
+                 P.PPC
+                 "archLookupReg"
+                 ["unexpected register: " ++ show (MC.prettyF reg)]
 
 updateReg :: forall v ppc m f tp
            . (MP.KnownVariant v,
@@ -244,7 +248,10 @@ archUpdateReg :: ( MP.KnownVariant v
 archUpdateReg regEntry reg val =
   case updateReg reg (const $ MCRV.RV val) (MCR.regValue regEntry) of
     Just r -> regEntry { MCR.regValue = r }
-    Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
+    Nothing -> P.panic
+                 P.PPC
+                 "archUpdateReg"
+                 ["unexpected register: " ++ show (MC.prettyF reg)]
 
 
 ppcGenFn :: forall ids s tp v ppc

macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs

@@ -62,6 +62,8 @@ data SemanticsError = NonUserSymbol String
 
 instance X.Exception SemanticsError
 
+type S p v sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (SP.AnyPPC v)) rtp bs r ctx
+
 termSemantics :: (C.IsSymInterface sym, 1 <= SP.AddrWidth v)
               => SymFuns sym
               -> MP.PPCTermStmt v ids
@@ -409,5 +411,3 @@ withRounding
 withRounding bak r action = do
   r' <- toValBV bak r
   U.withRounding (C.backendGetSym bak) r' action
-
-type S p v sym rtp bs r ctx = C.CrucibleState p sym (MS.MacawExt (SP.AnyPPC v)) rtp bs r ctx

macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Panic.hs

@@ -0,0 +1,15 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Data.Macaw.PPC.Symbolic.Panic (
+  P.panic,
+  Component(..)
+  ) where
+
+import qualified Panic as P
+
+data Component = PPC
+  deriving (Show)
+
+instance P.PanicComponent Component where
+  panicComponentName = show
+  panicComponentIssues _ = "https://github.com/GaloisInc/macaw/issues"
+  panicComponentRevision = $(P.useGitRevision)

macaw-riscv-symbolic/ChangeLog.md

@@ -0,0 +1,5 @@
+# Revision history for macaw-riscv-symbolic
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

macaw-riscv-symbolic/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-symbolic/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

macaw-riscv-symbolic/macaw-riscv-symbolic.cabal

@@ -0,0 +1,144 @@
+Cabal-version: 2.2
+Name:          macaw-riscv-symbolic
+Version:       0.1
+Author:        Galois Inc.
+Maintainer:    [email protected]
+Build-type:    Simple
+License:       BSD-3-Clause
+License-file:  LICENSE
+Category:      Language
+Synopsis:      A symbolic reasoning backend for RISC-V
+-- Description:
+extra-doc-files: README.md
+
+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,
+    crucible-llvm,
+    exceptions,
+    grift,
+    lens,
+    macaw-base,
+    macaw-riscv,
+    macaw-symbolic,
+    panic,
+    parameterized-utils,
+    what4
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.Macaw.RISCV.Symbolic
+  other-modules:
+    Data.Macaw.RISCV.Symbolic.AtomWrapper
+    Data.Macaw.RISCV.Symbolic.Functions
+    Data.Macaw.RISCV.Symbolic.Panic
+    Data.Macaw.RISCV.Symbolic.Repeat
+
+test-suite macaw-riscv-symbolic-tests
+  import: shared
+
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+
+  build-depends:
+    base >= 4,
+    bytestring,
+    containers,
+    crucible,
+    crucible-llvm,
+    elf-edit,
+    filepath,
+    Glob >= 0.9 && < 0.11,
+    grift,
+    lens,
+    macaw-base,
+    macaw-riscv,
+    macaw-riscv-symbolic,
+    macaw-symbolic,
+    parameterized-utils,
+    prettyprinter,
+    tasty,
+    tasty-hunit,
+    text,
+    what4,
+    vector
+
+  hs-source-dirs: tests