More typechecking for ghost variables

intTests/test_ghost_types_00/test.saw

@@ -28,6 +28,6 @@ let main : TopLevel () = do {
   f_ov <- crucible_llvm_unsafe_assume_spec m "f" (f_spec x);
   // This spec should probably use a different variable, but doesn't:
   g_ov <- crucible_llvm_unsafe_assume_spec m "g" (g_spec x);
-  crucible_llvm_verify m "h" [f_ov, g_ov] false h_spec z3;
+  fails (crucible_llvm_verify m "h" [f_ov, g_ov] false h_spec z3);
   print "done";
 };

src/SAWScript/Crucible/JVM/Override.hs

@@ -616,6 +616,7 @@ valueToSC _sym loc failMsg _tval _val =
 
 ------------------------------------------------------------------------
 
+-- | NOTE: The two 'Term' arguments must have the same type.
 matchTerm ::
   SharedContext   {- ^ context for constructing SAW terms    -} ->
   JVMCrucibleContext {- ^ context for interacting with Crucible -} ->

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -32,6 +32,7 @@ Stability   : provisional
 module SAWScript.Crucible.LLVM.MethodSpecIR where
 
 import           Control.Lens
+import           Control.Monad (when)
 import           Data.Functor.Compose (Compose(..))
 import           Data.IORef
 import           Data.Monoid ((<>))
@@ -41,6 +42,8 @@ import qualified Text.LLVM.PP as L
 import qualified Text.PrettyPrint.ANSI.Leijen as PPL hiding ((<$>), (<>))
 import qualified Text.PrettyPrint.HughesPJ as PP
 
+import qualified Cryptol.Utils.PP as Cryptol (pp)
+
 import           Data.Parameterized.All (All(All))
 import           Data.Parameterized.Some (Some(Some))
 import qualified Data.Parameterized.Map as MapF
@@ -185,7 +188,12 @@ showLLVMModule (LLVMModule name m _) =
 instance Crucible.IntrinsicClass (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) MS.GhostValue where
   type Intrinsic (Crucible.SAWCoreBackend n solver (B.Flags B.FloatReal)) MS.GhostValue ctx = TypedTerm
   muxIntrinsic sym _ _namerep _ctx prd thn els =
-    do st <- readIORef (B.sbStateManager sym)
+    do when (ttSchema thn /= ttSchema els) $ fail $ unlines $
+         [ "Attempted to mux ghost variables of different types:"
+         , show (Cryptol.pp (ttSchema thn))
+         , show (Cryptol.pp (ttSchema els))
+         ]
+       st <- readIORef (B.sbStateManager sym)
        let sc  = Crucible.saw_ctx st
        prd' <- Crucible.toSC sym prd
        typ  <- scTypeOf sc (ttTerm thn)

src/SAWScript/Crucible/LLVM/Override.hs

@@ -66,6 +66,7 @@ import qualified Text.LLVM.AST as L
 
 import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..))
 import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType)
+import qualified Cryptol.Utils.PP as Cryptol (pp)
 
 import qualified Lang.Crucible.Backend as Crucible
 import qualified Lang.Crucible.Backend.SAWCore as Crucible
@@ -1025,6 +1026,7 @@ typeToSC sc t =
 
 ------------------------------------------------------------------------
 
+-- | NOTE: The two 'Term' arguments must have the same type.
 matchTerm ::
   SharedContext   {- ^ context for constructing SAW terms    -} ->
   LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
@@ -1086,6 +1088,11 @@ learnGhost ::
   OverrideMatcher (LLVM arch) md ()
 learnGhost sc cc loc prepost var expected =
   do actual <- readGlobal var
+     when (ttSchema actual /= ttSchema expected) $ fail $ unlines $
+       [ "Ghost variable had the wrong type:"
+       , "- Expected: " ++ show (Cryptol.pp (ttSchema expected))
+       , "- Actual:   " ++ show (Cryptol.pp (ttSchema actual))
+       ]
      matchTerm sc cc loc prepost (ttTerm actual) (ttTerm expected)
 
 ------------------------------------------------------------------------