Reorganize Crucible-related modules (#482)

Fixes #455

saw-script.cabal

@@ -101,11 +101,6 @@ library
     SAWScript.AutoMatch.Util
     SAWScript.Builtins
     SAWScript.CongruenceClosure
-    SAWScript.CrucibleBuiltins
-    SAWScript.CrucibleLLVM
-    SAWScript.CrucibleOverride
-    SAWScript.CrucibleResolveSetupValue
-    SAWScript.CrucibleMethodSpecIR
     SAWScript.Exceptions
     SAWScript.Import
     SAWScript.ImportAIG
@@ -134,12 +129,17 @@ library
     SAWScript.Value
     SAWScript.VerificationCheck
 
-    SAWScript.CrucibleBuiltinsJVM
-
-    SAWScript.JVM.CrucibleBuiltins
-    SAWScript.JVM.CrucibleMethodSpecIR
-    SAWScript.JVM.CrucibleOverride
-    SAWScript.JVM.CrucibleResolveSetupValue
+    SAWScript.Crucible.LLVM.Builtins
+    SAWScript.Crucible.LLVM.CrucibleLLVM
+    SAWScript.Crucible.LLVM.Override
+    SAWScript.Crucible.LLVM.MethodSpecIR
+    SAWScript.Crucible.LLVM.ResolveSetupValue
+
+    SAWScript.Crucible.JVM.Builtins
+    SAWScript.Crucible.JVM.BuiltinsJVM
+    SAWScript.Crucible.JVM.MethodSpecIR
+    SAWScript.Crucible.JVM.Override
+    SAWScript.Crucible.JVM.ResolveSetupValue
 
     SAWScript.Prover.Mode
     SAWScript.Prover.Rewrite

src/SAWScript/JVM/CrucibleBuiltins.hs → src/SAWScript/Crucible/JVM/Builtins.hs

@@ -1,6 +1,6 @@
 {- |
-Module      : SAWScript.CrucibleBuiltins
-Description : Implementations of Crucible-related SAW-Script primitives.
+Module      : SAWScript.Crucible.JVM.Builtins
+Description : Implementations of crucible-jvm-related SAW-Script primitives.
 License     : BSD3
 Maintainer  : atomb
 Stability   : provisional
@@ -28,7 +28,7 @@ Stability   : provisional
 {-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
 
-module SAWScript.JVM.CrucibleBuiltins
+module SAWScript.Crucible.JVM.Builtins
     ( crucible_jvm_verify
     , crucible_jvm_unsafe_assume_spec
     , jvm_return
@@ -113,14 +113,14 @@ import SAWScript.Value
 import SAWScript.Utils as SS
 import qualified SAWScript.Position as SS
 import SAWScript.Options
-import SAWScript.CrucibleBuiltinsJVM (prepareClassTopLevel)
+import SAWScript.Crucible.JVM.BuiltinsJVM (prepareClassTopLevel)
 
 import SAWScript.JavaExpr (JavaType(..))
 
-import SAWScript.JVM.CrucibleMethodSpecIR
-import SAWScript.JVM.CrucibleOverride
-import SAWScript.JVM.CrucibleResolveSetupValue
-import SAWScript.CrucibleBuiltinsJVM ()
+import SAWScript.Crucible.JVM.MethodSpecIR
+import SAWScript.Crucible.JVM.Override
+import SAWScript.Crucible.JVM.ResolveSetupValue
+import SAWScript.Crucible.JVM.BuiltinsJVM ()
 
 ppAbortedResult :: CrucibleContext
                 -> Crucible.AbortedResult Sym a

src/SAWScript/CrucibleBuiltinsJVM.hs → src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -1,5 +1,5 @@
 {- |
-Module      : SAWScript.CrucibleBuiltinsJVM
+Module      : SAWScript.Crucible.JVM.BuiltinsJVM
 Description : crucible-jvm specific code
 Maintainer  : [email protected]
 Stability   : provisional
@@ -18,7 +18,7 @@ Stability   : provisional
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 
-module SAWScript.CrucibleBuiltinsJVM
+module SAWScript.Crucible.JVM.BuiltinsJVM
        (
          loadJavaClass           -- java_load_class: reads a class from the codebase
        , prepareClassTopLevel
@@ -68,7 +68,7 @@ import Verifier.SAW.TypedTerm(TypedTerm, mkTypedTerm)
 import SAWScript.Builtins(fixPos)
 import SAWScript.Value
 import SAWScript.Options(Options,simVerbose)
-import SAWScript.CrucibleBuiltins(setupArg, setupArgs, getGlobalPair, runCFG)
+import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, runCFG)
 
 -- jvm-verifier
 import qualified Language.JVM.Common as J

src/SAWScript/JVM/CrucibleMethodSpecIR.hs → src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -1,8 +1,7 @@
 {- |
-Module      : SAWScript.CrucibleMethodSpecIR
-Description : Provides type-checked representation for Crucible/LLVM function
-              specifications and function for creating it from AST
-              representation.
+Module      : SAWScript.Crucible.JVM.MethodSpecIR
+Description : Provides type-checked representation for Crucible/JVM function
+              specifications and functions for creating it from a SAWscript AST.
 Maintainer  : atomb
 Stability   : provisional
 -}
@@ -23,7 +22,7 @@ Stability   : provisional
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -fno-warn-orphans  #-}
 
-module SAWScript.JVM.CrucibleMethodSpecIR where
+module SAWScript.Crucible.JVM.MethodSpecIR where
 
 import           Data.Map (Map)
 import qualified Data.Map as Map

src/SAWScript/JVM/CrucibleOverride.hs → src/SAWScript/Crucible/JVM/Override.hs

@@ -1,3 +1,11 @@
+{- |
+Module      : SAWScript.Crucible.JVM.Override
+Description : Override matching and application for JVM
+License     : BSD3
+Maintainer  : atomb
+Stability   : provisional
+-}
+
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ImplicitParams #-}
@@ -14,7 +22,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ViewPatterns #-}
 
-module SAWScript.JVM.CrucibleOverride
+module SAWScript.Crucible.JVM.Override
   ( OverrideMatcher(..)
   , runOverrideMatcher
 
@@ -82,8 +90,8 @@ import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
 
 --import           SAWScript.JavaExpr (JavaType(..))
-import           SAWScript.JVM.CrucibleMethodSpecIR
-import           SAWScript.JVM.CrucibleResolveSetupValue
+import           SAWScript.Crucible.JVM.MethodSpecIR
+import           SAWScript.Crucible.JVM.ResolveSetupValue
 import           SAWScript.Options
 import           SAWScript.Utils (handleException)
 

src/SAWScript/JVM/CrucibleResolveSetupValue.hs → src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -1,10 +1,17 @@
+{- |
+Module      : SAWScript.Crucible.JVM.ResolveSetupValue
+License     : BSD3
+Maintainer  : atomb
+Stability   : provisional
+-}
+
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 
-module SAWScript.JVM.CrucibleResolveSetupValue
+module SAWScript.Crucible.JVM.ResolveSetupValue
   ( JVMVal(..)
   , JVMRefVal
   , resolveSetupVal
@@ -55,7 +62,7 @@ import qualified Language.JVM.Parser as J
 
 --import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.Prover.Rewrite
-import SAWScript.JVM.CrucibleMethodSpecIR
+import SAWScript.Crucible.JVM.MethodSpecIR
 
 --import qualified SAWScript.LLVMBuiltins as LB
 

src/SAWScript/CrucibleBuiltins.hs → src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1,5 +1,5 @@
 {- |
-Module      : SAWScript.CrucibleBuiltins
+Module      : SAWScript.Crucible.LLVM.Builtins
 Description : Implementations of Crucible-related SAW-Script primitives.
 License     : BSD3
 Maintainer  : atomb
@@ -26,7 +26,7 @@ Stability   : provisional
 {-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
 
-module SAWScript.CrucibleBuiltins
+module SAWScript.Crucible.LLVM.Builtins
     ( show_cfg
     , crucible_llvm_cfg
     , crucible_llvm_extract
@@ -116,7 +116,7 @@ import qualified Lang.Crucible.LLVM.DataLayout as Crucible
 import qualified Lang.Crucible.LLVM.MemModel as Crucible
 import qualified Lang.Crucible.LLVM.Translation as Crucible
 
-import qualified SAWScript.CrucibleLLVM as Crucible
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
 
 import qualified Data.Parameterized.TraversableFC as Ctx
 import qualified Data.Parameterized.Context as Ctx
@@ -136,9 +136,9 @@ import SAWScript.Value
 import SAWScript.Position as SS
 import SAWScript.Options
 
-import SAWScript.CrucibleMethodSpecIR
-import SAWScript.CrucibleOverride
-import SAWScript.CrucibleResolveSetupValue
+import SAWScript.Crucible.LLVM.Override
+import SAWScript.Crucible.LLVM.ResolveSetupValue
+import SAWScript.Crucible.LLVM.MethodSpecIR
 
 
 type MemImpl = Crucible.MemImpl Sym

src/SAWScript/CrucibleLLVM.hs → src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs

@@ -1,5 +1,5 @@
 {- |
-Module      : SAWScript.CrucibleLLVM
+Module      : SAWScript.Crucible.LLVM.CrucibleLLVM
 Description : Re-exports from the crucible-llvm package
 License     : BSD3
 Maintainer  : huffman
@@ -11,7 +11,7 @@ This module collects declarations from various modules in the
 -}
 {-# LANGUAGE PatternSynonyms #-}
 
-module SAWScript.CrucibleLLVM
+module SAWScript.Crucible.LLVM.CrucibleLLVM
   (
     -- * Re-exports from "Lang.Crucible.LLVM"
     llvmGlobals

src/SAWScript/CrucibleMethodSpecIR.hs → src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -1,13 +1,14 @@
-{-# LANGUAGE DeriveFunctor #-}
 {- |
-Module      : SAWScript.CrucibleMethodSpecIR
+Module      : SAWScript.Crucible.LLVM.MethodSpecIR
 Description : Provides type-checked representation for Crucible/LLVM function
               specifications and function for creating it from AST
               representation.
 Maintainer  : atomb
 Stability   : provisional
 -}
+
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE Rank2Types #-}
@@ -24,7 +25,7 @@ Stability   : provisional
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -fno-warn-orphans  #-}
 
-module SAWScript.CrucibleMethodSpecIR where
+module SAWScript.Crucible.LLVM.MethodSpecIR where
 
 import           Data.List (isPrefixOf)
 import           Data.Map (Map)
@@ -61,7 +62,7 @@ import qualified Lang.Crucible.Simulator.Intrinsics as Crucible
   (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn))
 import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
-import qualified SAWScript.CrucibleLLVM as CL
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL
 import           SAWScript.Options
 import           SAWScript.Utils (bullets)
 

src/SAWScript/CrucibleOverride.hs → src/SAWScript/Crucible/LLVM/Override.hs

@@ -1,3 +1,10 @@
+{- |
+Module      : SAWScript.Crucible.LLVM.Override
+Description : Override matching and application for LLVM
+License     : BSD3
+Maintainer  : atomb
+Stability   : provisional
+-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -17,7 +24,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
 
-module SAWScript.CrucibleOverride
+module SAWScript.Crucible.LLVM.Override
   ( OverrideMatcher(..)
   , runOverrideMatcher
 
@@ -82,7 +89,7 @@ import qualified What4.Partial as W4
 import qualified What4.ProgramLoc as W4
 import qualified What4.Symbol as W4
 
-import qualified SAWScript.CrucibleLLVM as Crucible
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
 
 import           Data.Parameterized.Classes ((:~:)(..), testEquality)
 import qualified Data.Parameterized.TraversableFC as Ctx
@@ -95,8 +102,8 @@ import           Verifier.SAW.TypedAST
 import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
 
-import           SAWScript.CrucibleMethodSpecIR
-import           SAWScript.CrucibleResolveSetupValue
+import           SAWScript.Crucible.LLVM.MethodSpecIR
+import           SAWScript.Crucible.LLVM.ResolveSetupValue
 import           SAWScript.Options
 import           SAWScript.Utils (bullets, handleException)
 

src/SAWScript/CrucibleResolveSetupValue.hs → src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -1,10 +1,18 @@
+{- |
+Module      : SAWScript.Crucible.LLVM.ResolveSetupValue
+Description : Turn SetupValues back into LLVMVals
+License     : BSD3
+Maintainer  : atomb
+Stability   : provisional
+-}
+
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-module SAWScript.CrucibleResolveSetupValue
+module SAWScript.Crucible.LLVM.ResolveSetupValue
   ( LLVMVal, LLVMPtr
   , resolveSetupVal
   , typeOfLLVMVal
@@ -44,7 +52,7 @@ import qualified What4.ProgramLoc   as W4
 import qualified Lang.Crucible.LLVM.MemModel    as Crucible
 import qualified Lang.Crucible.LLVM.Translation as Crucible
 import qualified Lang.Crucible.Backend.SAWCore  as Crucible
-import qualified SAWScript.CrucibleLLVM         as Crucible
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
 
 import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
@@ -56,7 +64,7 @@ import qualified Verifier.SAW.Simulator.SBV as SBV (sbvSolveBasic, toWord)
 import qualified Data.SBV.Dynamic as SBV (svAsInteger)
 
 import SAWScript.Prover.Rewrite
-import SAWScript.CrucibleMethodSpecIR
+import SAWScript.Crucible.LLVM.MethodSpecIR
 
 --import qualified SAWScript.LLVMBuiltins as LB
 

src/SAWScript/Interpreter.hs

@@ -50,10 +50,10 @@ import SAWScript.AST (Located(..),Import(..))
 import SAWScript.Builtins
 import SAWScript.Exceptions (failTypecheck)
 import qualified SAWScript.Import
-import SAWScript.CrucibleBuiltins
+import SAWScript.Crucible.LLVM.Builtins
 import qualified Lang.Crucible.JVM as CJ
-import qualified SAWScript.CrucibleBuiltinsJVM as CJ
-import qualified SAWScript.CrucibleMethodSpecIR as CIR
+import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ
+import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR
 import SAWScript.JavaBuiltins
 import SAWScript.JavaExpr
 import SAWScript.LLVMBuiltins
@@ -80,8 +80,8 @@ import qualified Verifier.Java.SAWBackend as JavaSAW
 
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 
-import SAWScript.JVM.CrucibleBuiltins
-import qualified SAWScript.JVM.CrucibleMethodSpecIR as JIR
+import SAWScript.Crucible.JVM.Builtins
+import qualified SAWScript.Crucible.JVM.MethodSpecIR as JIR
 
 import Cryptol.ModuleSystem.Env (meSolverConfig)
 import qualified Cryptol.Utils.Ident as T (packIdent, packModName)

src/SAWScript/LLVMBuiltins.hs

@@ -31,7 +31,7 @@ import qualified Text.LLVM.Parser as LLVM (parseType)
 
 import SAWScript.Value as SV
 
-import qualified SAWScript.CrucibleLLVM as Crucible (translateModule)
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible (translateModule)
 
 llvm_load_module :: FilePath -> TopLevel LLVMModule
 llvm_load_module file =

src/SAWScript/Value.hs

@@ -63,9 +63,9 @@ import qualified Data.AIG as AIG
 import qualified SAWScript.AST as SS
 import qualified SAWScript.Position as SS
 import qualified SAWScript.JavaMethodSpecIR as JIR
-import qualified SAWScript.CrucibleLLVM as Crucible
-import qualified SAWScript.CrucibleMethodSpecIR as CIR
-import qualified SAWScript.JVM.CrucibleMethodSpecIR as JCIR
+import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
+import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CIR
+import qualified SAWScript.Crucible.JVM.MethodSpecIR as JCIR
 import qualified Verifier.Java.Codebase as JSS
 import qualified Text.LLVM.AST as LLVM (Type)
 import qualified Text.LLVM.PP as LLVM (ppType)