diff --git a/saw-script.cabal b/saw-script.cabal index cbeb75b6d1..d88bc9eb8a 100644 --- a/saw-script.cabal +++ b/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 diff --git a/src/SAWScript/JVM/CrucibleBuiltins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs similarity index 98% rename from src/SAWScript/JVM/CrucibleBuiltins.hs rename to src/SAWScript/Crucible/JVM/Builtins.hs index 731a991995..efd07df074 100644 --- a/src/SAWScript/JVM/CrucibleBuiltins.hs +++ b/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 diff --git a/src/SAWScript/CrucibleBuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs similarity index 97% rename from src/SAWScript/CrucibleBuiltinsJVM.hs rename to src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 344fd7fc00..b514bb11ca 100644 --- a/src/SAWScript/CrucibleBuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -1,5 +1,5 @@ {- | -Module : SAWScript.CrucibleBuiltinsJVM +Module : SAWScript.Crucible.JVM.BuiltinsJVM Description : crucible-jvm specific code Maintainer : sweirich@galois.com 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 diff --git a/src/SAWScript/JVM/CrucibleMethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs similarity index 98% rename from src/SAWScript/JVM/CrucibleMethodSpecIR.hs rename to src/SAWScript/Crucible/JVM/MethodSpecIR.hs index 3124aa11ef..facf1a1f14 100644 --- a/src/SAWScript/JVM/CrucibleMethodSpecIR.hs +++ b/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 diff --git a/src/SAWScript/JVM/CrucibleOverride.hs b/src/SAWScript/Crucible/JVM/Override.hs similarity index 99% rename from src/SAWScript/JVM/CrucibleOverride.hs rename to src/SAWScript/Crucible/JVM/Override.hs index 18d2a0a544..da1600a2f8 100644 --- a/src/SAWScript/JVM/CrucibleOverride.hs +++ b/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) diff --git a/src/SAWScript/JVM/CrucibleResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs similarity index 97% rename from src/SAWScript/JVM/CrucibleResolveSetupValue.hs rename to src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index f4c01b4829..cdfa0b1686 100644 --- a/src/SAWScript/JVM/CrucibleResolveSetupValue.hs +++ b/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 diff --git a/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs similarity index 99% rename from src/SAWScript/CrucibleBuiltins.hs rename to src/SAWScript/Crucible/LLVM/Builtins.hs index 1bef9c7f78..583685ef6d 100644 --- a/src/SAWScript/CrucibleBuiltins.hs +++ b/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 diff --git a/src/SAWScript/CrucibleLLVM.hs b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs similarity index 98% rename from src/SAWScript/CrucibleLLVM.hs rename to src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs index 6bf26e1bf4..fec63d0f27 100644 --- a/src/SAWScript/CrucibleLLVM.hs +++ b/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 diff --git a/src/SAWScript/CrucibleMethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs similarity index 99% rename from src/SAWScript/CrucibleMethodSpecIR.hs rename to src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index b6605772a9..a63ad38fa3 100644 --- a/src/SAWScript/CrucibleMethodSpecIR.hs +++ b/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) diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/Crucible/LLVM/Override.hs similarity index 99% rename from src/SAWScript/CrucibleOverride.hs rename to src/SAWScript/Crucible/LLVM/Override.hs index b594b66a5b..006c7b91bd 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/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) diff --git a/src/SAWScript/CrucibleResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs similarity index 98% rename from src/SAWScript/CrucibleResolveSetupValue.hs rename to src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 3ea3fbc9d6..dcf396a921 100644 --- a/src/SAWScript/CrucibleResolveSetupValue.hs +++ b/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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index a0294b6c0b..a27d749c29 100644 --- a/src/SAWScript/Interpreter.hs +++ b/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) diff --git a/src/SAWScript/LLVMBuiltins.hs b/src/SAWScript/LLVMBuiltins.hs index 3a0b951e88..8d9cfadbc1 100644 --- a/src/SAWScript/LLVMBuiltins.hs +++ b/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 = diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index adf778b984..4ee8c1907b 100644 --- a/src/SAWScript/Value.hs +++ b/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) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index ec9604acef..afcfbd348d 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -69,7 +69,7 @@ import Lang.Crucible.FunctionHandle(HandleAllocator,newHandleAllocator,insertHan -- Crucible LLVM -import SAWScript.CrucibleLLVM +import SAWScript.Crucible.LLVM.CrucibleLLVM (Mem, ppPtr, pattern LLVMPointer, bytesToInteger) import Lang.Crucible.LLVM.Intrinsics(llvmIntrinsicTypes) import Lang.Crucible.LLVM.MemModel (mkMemVar) @@ -629,4 +629,3 @@ statusBlock msg m = a <- m sayOK return a - diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index ecbb252a37..0fd80101aa 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -88,7 +88,7 @@ import What4.Interface import What4.ProgramLoc import Lang.Crucible.FunctionHandle -import SAWScript.CrucibleLLVM +import SAWScript.Crucible.LLVM.CrucibleLLVM ( EndianForm(LittleEndian) , MemImpl, doLoad, doPtrAddOffset, emptyMem , AllocType(HeapAlloc, GlobalAlloc), Mutability(..), Mem