Some deduplication between Crucible.LLVM and Crucible.JVM (#483)

* Add a Crucible.Common module for slight code de-duplication

Progress on #379

* More deduplication between Crucible(LLVM|JVM)

saw-script.cabal

@@ -129,6 +129,8 @@ library
     SAWScript.Value
     SAWScript.VerificationCheck
 
+    SAWScript.Crucible.Common
+
     SAWScript.Crucible.LLVM.Builtins
     SAWScript.Crucible.LLVM.CrucibleLLVM
     SAWScript.Crucible.LLVM.Override

src/SAWScript/Crucible/Common.hs

@@ -0,0 +1,72 @@
+{- |
+Module      : SAWScript.Crucible.Common
+Description : Crucible-related material that is not specific to a given language
+License     : BSD3
+Maintainer  : langston
+Stability   : provisional
+-}
+
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE RankNTypes #-}
+
+module SAWScript.Crucible.Common
+  ( AllocIndex(..)
+  , nextAllocIndex
+  , PrePost(..)
+  , ppAbortedResult
+  , Sym
+  ) where
+
+import           Data.Data (Data)
+import           GHC.Generics (Generic)
+
+import           Lang.Crucible.Simulator.ExecutionTree (AbortedResult(..), GlobalPair)
+import           Lang.Crucible.Simulator.CallFrame (SimFrame)
+import           Lang.Crucible.Backend (AbortExecReason(..), ppAbortExecReason)
+import           Lang.Crucible.Backend.SAWCore (SAWCoreBackend)
+import qualified Data.Parameterized.Nonce as Nonce
+import qualified What4.Solver.Yices as Yices
+import qualified What4.Expr as W4
+
+import qualified Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
+
+-- | The symbolic backend we use for SAW verification
+type Sym = SAWCoreBackend Nonce.GlobalNonceGenerator (Yices.Connection Nonce.GlobalNonceGenerator) (W4.Flags W4.FloatReal)
+
+-- | How many allocations have we made in this method spec?
+newtype AllocIndex = AllocIndex Int
+  deriving (Data, Eq, Generic, Ord, Show)
+
+nextAllocIndex :: AllocIndex -> AllocIndex
+nextAllocIndex (AllocIndex n) = AllocIndex (n + 1)
+
+-- | Are we writing preconditions or postconditions?
+data PrePost
+  = PreState | PostState
+  deriving (Data, Eq, Generic, Ord, Show)
+
+ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc)
+                -> AbortedResult Sym ext
+                -> PP.Doc
+ppAbortedResult _ (AbortedExec InfeasibleBranch _) =
+  PP.text "Infeasible branch"
+ppAbortedResult ppGP (AbortedExec abt gp) = do
+  ppAbortExecReason abt PP.<$$> ppGP gp
+ppAbortedResult ppGP (AbortedBranch _predicate trueBranch falseBranch) =
+  PP.vcat
+    [ PP.text "Both branches aborted after a symbolic branch."
+    -- TODO: These conditions can be large, symbolic SAWCore predicates, so they
+    -- aren't really helpful to show. It would be nice if Crucible tracked the
+    -- source location associated with the branch, then we could print that.
+    -- See https://github.com/GaloisInc/crucible/issues/260
+
+    -- , text "Branch condition:"
+    -- , indent 2 (text (show predicate))
+    , PP.text "Message from the true branch:"
+    , PP.indent 2 (ppAbortedResult ppGP trueBranch)
+    , PP.text "Message from the false branch:"
+    , PP.indent 2 (ppAbortedResult ppGP falseBranch)
+    ]
+ppAbortedResult _ (AbortedExit ec) =
+  PP.text "Branch exited:" PP.<+> PP.text (show ec)

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -117,22 +117,19 @@ import SAWScript.Crucible.JVM.BuiltinsJVM (prepareClassTopLevel)
 
 import SAWScript.JavaExpr (JavaType(..))
 
+import qualified SAWScript.Crucible.Common as Common
+import           SAWScript.Crucible.Common (AllocIndex(..), PrePost(..), Sym)
+
 import SAWScript.Crucible.JVM.MethodSpecIR
 import SAWScript.Crucible.JVM.Override
 import SAWScript.Crucible.JVM.ResolveSetupValue
 import SAWScript.Crucible.JVM.BuiltinsJVM ()
 
+-- TODO: something useful with the global pair?
 ppAbortedResult :: CrucibleContext
                 -> Crucible.AbortedResult Sym a
                 -> Doc
-ppAbortedResult _ (Crucible.AbortedExec Crucible.InfeasibleBranch _) =
-  text "Infeasible branch"
-ppAbortedResult cc (Crucible.AbortedExec abt gp) = do
-  Crucible.ppAbortExecReason abt -- <$$> ppGlobalPair cc gp
-ppAbortedResult _ (Crucible.AbortedBranch _ _ _) =
-  text "Aborted branch"
-ppAbortedResult _ (Crucible.AbortedExit ec) =
-  text "Branch exited:" <+> text (show ec)
+ppAbortedResult _cc = Common.ppAbortedResult (\_gp -> mempty)
 
 -- FIXME: We need a better way to identify a set of class names to
 -- load. This function has two problems: First, unless we put in a

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -124,8 +124,6 @@ prepareClassTopLevel bic str = do
 
 -----------------------------------------------------------------------
 
-type Sym = CrucibleSAW.SAWCoreBackend Nonce.GlobalNonceGenerator (Yices.Connection Nonce.GlobalNonceGenerator) (W4.Flags W4.FloatReal)
-
 
 -- | Extract a JVM method to saw-core
 --

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -34,12 +34,9 @@ import           Control.Lens
 import           Data.IORef
 import           Data.Monoid ((<>))
 
-import qualified Data.Parameterized.Nonce as Crucible
-
 -- what4
 import qualified What4.Expr.Builder as B
 import           What4.ProgramLoc (ProgramLoc)
-import qualified What4.Solver.Yices as Yices
 
 import qualified Lang.Crucible.Types as Crucible
   (IntrinsicType, EmptyCtx)
@@ -67,8 +64,7 @@ import Verifier.SAW.TypedTerm
 import SAWScript.Options
 import SAWScript.Prover.SolverStats
 
-newtype AllocIndex = AllocIndex Int
-  deriving (Eq, Ord, Show)
+import SAWScript.Crucible.Common (AllocIndex(..), PrePost(..), Sym)
 
 nextAllocIndex :: AllocIndex -> AllocIndex
 nextAllocIndex (AllocIndex n) = AllocIndex (n + 1)
@@ -97,10 +93,6 @@ setupToTerm _opts _sc sv =
     SetupTerm term -> return (ttTerm term)
     _ -> MaybeT $ return Nothing
 
-data PrePost
-  = PreState | PostState
-  deriving (Eq, Show)
-
 
 data PointsTo
   = PointsToField ProgramLoc SetupValue String SetupValue
@@ -229,8 +221,6 @@ data CrucibleSetupState =
   , _csCrucibleContext :: CrucibleContext
   }
 
-type Sym = Crucible.SAWCoreBackend Crucible.GlobalNonceGenerator (Yices.Connection Crucible.GlobalNonceGenerator) (B.Flags B.FloatReal)
-
 data CrucibleContext =
   CrucibleContext
   { _ccJVMClass       :: J.Class

src/SAWScript/Crucible/JVM/Override.hs

@@ -89,6 +89,8 @@ import           Verifier.SAW.TypedAST
 import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
 
+import           SAWScript.Crucible.Common (AllocIndex(..), PrePost(..), Sym)
+
 --import           SAWScript.JavaExpr (JavaType(..))
 import           SAWScript.Crucible.JVM.MethodSpecIR
 import           SAWScript.Crucible.JVM.ResolveSetupValue

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -60,6 +60,8 @@ import qualified Data.SBV.Dynamic as SBV (svAsInteger, svAsBool)
 -- jvm-parser
 import qualified Language.JVM.Parser as J
 
+import SAWScript.Crucible.Common (AllocIndex(..), Sym)
+
 --import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.Prover.Rewrite
 import SAWScript.Crucible.JVM.MethodSpecIR

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -136,6 +136,9 @@ import SAWScript.Value
 import SAWScript.Position as SS
 import SAWScript.Options
 
+import qualified SAWScript.Crucible.Common as Common
+import           SAWScript.Crucible.Common (AllocIndex(..), nextAllocIndex, PrePost(..), Sym)
+
 import SAWScript.Crucible.LLVM.Override
 import SAWScript.Crucible.LLVM.ResolveSetupValue
 import SAWScript.Crucible.LLVM.MethodSpecIR
@@ -171,31 +174,6 @@ show_cfg :: SAW_CFG -> String
 show_cfg (LLVM_CFG (Crucible.AnyCFG cfg)) = show cfg
 show_cfg (JVM_CFG (Crucible.AnyCFG cfg)) = show cfg
 
-ppAbortedResult :: CrucibleContext arch
-                -> Crucible.AbortedResult Sym a
-                -> Doc
-ppAbortedResult _ (Crucible.AbortedExec Crucible.InfeasibleBranch _) =
-  text "Infeasible branch"
-ppAbortedResult cc (Crucible.AbortedExec abt gp) = do
-  Crucible.ppAbortExecReason abt <$$> ppGlobalPair cc gp
-ppAbortedResult cc (Crucible.AbortedBranch _predicate trueBranch falseBranch) =
-  vcat
-    [ text "Both branches aborted after a symbolic branch."
-    -- TODO: These conditions can be large, symbolic SAWCore predicates, so they
-    -- aren't really helpful to show. It would be nice if Crucible tracked the
-    -- source location associated with the branch, then we could print that.
-    -- See https://github.com/GaloisInc/crucible/issues/260
-
-    -- , text "Branch condition:"
-    -- , indent 2 (text (show predicate))
-    , text "Message from the true branch:"
-    , indent 2 (ppAbortedResult cc trueBranch)
-    , text "Message from the false branch:"
-    , indent 2 (ppAbortedResult cc falseBranch)
-    ]
-ppAbortedResult _ (Crucible.AbortedExit ec) =
-  text "Branch exited:" <+> text (show ec)
-
 -- | Determines whether one LLVM symbol is equivalent to another except
 -- for a numeric suffix. This can determine whether one symbol is the
 -- disambiguated name of a duplicated static function.
@@ -618,6 +596,11 @@ doAllocConst = doAllocWithMutability Crucible.Immutable
 
 --------------------------------------------------------------------------------
 
+ppAbortedResult :: CrucibleContext arch
+                -> Crucible.AbortedResult Sym a
+                -> Doc
+ppAbortedResult cc = Common.ppAbortedResult (ppGlobalPair cc)
+
 ppGlobalPair :: CrucibleContext arch
              -> Crucible.GlobalPair Sym a
              -> Doc

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -41,13 +41,11 @@ import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L
 
 import qualified Data.Parameterized.Map as MapF
-import qualified Data.Parameterized.Nonce as Crucible
 
 import           SAWScript.Prover.SolverStats
 
 import qualified What4.Expr.Builder as B
 import           What4.ProgramLoc (ProgramLoc)
-import qualified What4.Solver.Yices as Yices
 
 import qualified Lang.Crucible.Types as Crucible
   (IntrinsicType, EmptyCtx, SymbolRepr, knownSymbol)
@@ -62,19 +60,14 @@ import qualified Lang.Crucible.Simulator.Intrinsics as Crucible
   (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn))
 import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
+import           SAWScript.Crucible.Common (AllocIndex(..), PrePost(..), Sym)
 import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL
 import           SAWScript.Options
 import           SAWScript.Utils (bullets)
 
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.TypedTerm
 
-newtype AllocIndex = AllocIndex Int
-  deriving (Eq, Ord, Show)
-
-nextAllocIndex :: AllocIndex -> AllocIndex
-nextAllocIndex (AllocIndex n) = AllocIndex (n + 1)
-
 -- | From the manual: "The SetupValue type corresponds to values that can occur
 -- during symbolic execution, which includes both Term values, pointers, and
 -- composite types consisting of either of these (both structures and arrays)."
@@ -134,11 +127,6 @@ setupToTerm opts sc sv =
     -- SetupVar, SetupNull, SetupGlobal
     _ -> MaybeT $ return Nothing
 
-data PrePost
-  = PreState | PostState
-  deriving (Eq, Show)
-
-
 data PointsTo = PointsTo ProgramLoc SetupValue SetupValue
   deriving (Show)
 
@@ -270,8 +258,6 @@ data CrucibleSetupState wptr =
   ,_csCrucibleContext :: CrucibleContext wptr
   }
 
-type Sym = Crucible.SAWCoreBackend Crucible.GlobalNonceGenerator (Yices.Connection Crucible.GlobalNonceGenerator) (B.Flags B.FloatReal)
-
 data CrucibleContext wptr =
   CrucibleContext
   { _ccLLVMModule      :: L.Module

src/SAWScript/Crucible/LLVM/Override.hs

@@ -102,6 +102,7 @@ import           Verifier.SAW.TypedAST
 import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
 
+import           SAWScript.Crucible.Common (AllocIndex(..), PrePost(..), Sym)
 import           SAWScript.Crucible.LLVM.MethodSpecIR
 import           SAWScript.Crucible.LLVM.ResolveSetupValue
 import           SAWScript.Options

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -63,6 +63,8 @@ import Text.LLVM.DebugUtils as L
 import qualified Verifier.SAW.Simulator.SBV as SBV (sbvSolveBasic, toWord)
 import qualified Data.SBV.Dynamic as SBV (svAsInteger)
 
+import           SAWScript.Crucible.Common (AllocIndex(..), Sym)
+
 import SAWScript.Prover.Rewrite
 import SAWScript.Crucible.LLVM.MethodSpecIR