crucible-llvm: Simplify 'MemoryErrorReason'

crucible-llvm/src/Lang/Crucible/LLVM/Errors.hs

@@ -106,7 +106,7 @@ undefinedBehavior :: UB.UndefinedBehavior (RegValue' sym)
 undefinedBehavior ub pred =
   LLVMSafetyAssertion (BBUndefinedBehavior ub) pred Nothing
 
-memoryError :: (1 <= w) => ME.MemoryOp sym w -> ME.MemoryErrorReason sym w -> Pred sym -> LLVMSafetyAssertion sym
+memoryError :: (1 <= w) => ME.MemoryOp sym w -> ME.MemoryErrorReason -> Pred sym -> LLVMSafetyAssertion sym
 memoryError mop rsn pred =
   LLVMSafetyAssertion (BBMemoryError (ME.MemoryError mop rsn)) pred Nothing
 

crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs

@@ -25,18 +25,19 @@ module Lang.Crucible.LLVM.Errors.MemoryError
 , ppMemoryOp
 , MemoryErrorReason(..)
 , ppMemoryErrorReason
+, FuncLookupError(..)
+, ppFuncLookupError
 
 , concMemoryError
 , concMemoryOp
-, concMemoryErrorReason
 ) where
 
 import           Prelude hiding (pred)
 
 import           Data.Text (Text)
-import           Data.Void
 import qualified Text.LLVM.PP as L
 import qualified Text.LLVM.AST as L
+import           Type.Reflection (SomeTypeRep(SomeTypeRep))
 import           Prettyprinter
 
 import           What4.Interface
@@ -47,7 +48,6 @@ import           Lang.Crucible.LLVM.MemModel.Common
 import           Lang.Crucible.LLVM.MemModel.Type
 import           Lang.Crucible.LLVM.MemModel.MemLog
 
-
 data MemoryOp sym w
   = MemLoadOp  StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
   | MemStoreOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
@@ -64,22 +64,43 @@ data MemoryOp sym w
 data MemoryError sym where
   MemoryError :: (1 <= w) =>
     MemoryOp sym w ->
-    MemoryErrorReason sym w ->
+    MemoryErrorReason ->
     MemoryError sym
 
 -- | The kinds of type errors that arise while reading memory/constructing LLVM
 -- values
-data MemoryErrorReason sym w =
+data MemoryErrorReason =
     TypeMismatch StorageType StorageType
   | UnexpectedArgumentType Text [StorageType]
   | ApplyViewFail ValueView
   | Invalid StorageType
   | Invalidated Text
-  | NoSatisfyingWrite StorageType (LLVMPtr sym w)
+  | NoSatisfyingWrite StorageType
   | UnwritableRegion
   | UnreadableRegion
-  | BadFunctionPointer (Doc Void)
+  | BadFunctionPointer FuncLookupError
   | OverlappingRegions
+  deriving (Eq, Ord)
+
+-- | Reasons that looking up a function handle associated with an LLVM pointer
+-- may fail
+data FuncLookupError
+  = SymbolicPointer
+  | RawBitvector
+  | NoOverride
+  | Uncallable SomeTypeRep
+  deriving (Eq, Ord)
+
+ppFuncLookupError :: FuncLookupError -> Doc ann
+ppFuncLookupError =
+  \case
+    SymbolicPointer -> "Cannot resolve a symbolic pointer to a function handle"
+    RawBitvector -> "Cannot treat raw bitvector as function pointer"
+    NoOverride -> "No implementation or override found for pointer"
+    Uncallable (SomeTypeRep typeRep) ->
+      vsep [ "Data associated with the pointer found, but was not a callable function:"
+           , hang 2 (viaShow typeRep)
+           ]
 
 type MemErrContext sym w = MemoryOp sym w
 
@@ -148,7 +169,7 @@ details (MemoryError mop _rsn) = ppMemoryOp mop
 ppMemoryError :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
 ppMemoryError (MemoryError mop rsn) = vcat [ppMemoryErrorReason rsn, ppMemoryOp mop]
 
-ppMemoryErrorReason :: IsExpr (SymExpr sym) => MemoryErrorReason sym w -> Doc ann
+ppMemoryErrorReason :: MemoryErrorReason -> Doc ann
 ppMemoryErrorReason =
   \case
     TypeMismatch ty1 ty2 ->
@@ -170,20 +191,19 @@ ppMemoryErrorReason =
       "Load from invalid memory at type" <+> ppType ty
     Invalidated msg ->
       "Load from explicitly invalidated memory:" <+> pretty msg
-    NoSatisfyingWrite tp ptr ->
+    NoSatisfyingWrite tp ->
       vcat
        [ "No previous write to this location was found"
        , indent 2 ("Attempting load at type:" <+> ppType tp)
-       , indent 2 ("Via pointer:" <+> ppPtr ptr)
        ]
     UnwritableRegion ->
       "The region wasn't allocated, wasn't large enough, or was marked as readonly"
     UnreadableRegion ->
       "The region wasn't allocated or wasn't large enough"
-    BadFunctionPointer msg ->
+    BadFunctionPointer err ->
       vcat
        [ "The given pointer could not be resolved to a callable function"
-       , unAnnotate msg
+       , ppFuncLookupError err
        ]
     OverlappingRegions ->
       "Memory regions required to be disjoint"
@@ -194,7 +214,7 @@ concMemoryError ::
   (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
   MemoryError sym -> IO (MemoryError sym)
 concMemoryError sym conc (MemoryError mop rsn) =
-  MemoryError <$> concMemoryOp sym conc mop <*> concMemoryErrorReason sym conc rsn
+  MemoryError <$> concMemoryOp sym conc mop <*> pure rsn
 
 concMemoryOp ::
   (1 <= w, IsExprBuilder sym) =>
@@ -223,20 +243,3 @@ concMemoryOp sym conc (MemInvalidateOp msg gsym ptr len mem) =
     concPtr sym conc ptr <*>
     concBV sym conc len <*>
     concMem sym conc mem
-
-concMemoryErrorReason ::
-  (1 <= w, IsExprBuilder sym) =>
-  sym ->
-  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
-  MemoryErrorReason sym w -> IO (MemoryErrorReason sym w)
-concMemoryErrorReason sym conc rsn = case rsn of
-  TypeMismatch t1 t2 -> pure (TypeMismatch t1 t2)
-  UnexpectedArgumentType msg ts -> pure (UnexpectedArgumentType msg ts)
-  ApplyViewFail v -> pure (ApplyViewFail v)
-  Invalid tp -> pure (Invalid tp)
-  Invalidated msg -> pure (Invalidated msg)
-  NoSatisfyingWrite tp ptr -> NoSatisfyingWrite tp <$> concPtr sym conc ptr
-  UnwritableRegion -> pure UnwritableRegion
-  UnreadableRegion -> pure UnreadableRegion
-  BadFunctionPointer msg -> pure (BadFunctionPointer msg)
-  OverlappingRegions -> pure OverlappingRegions

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -67,6 +67,8 @@ module Lang.Crucible.LLVM.MemModel
   , G.AllocType(..)
   , G.Mutability(..)
   , doMallocHandle
+  , ME.FuncLookupError(..)
+  , ME.ppFuncLookupError
   , doLookupHandle
   , doInstallHandle
   , doMemcpy
@@ -202,7 +204,6 @@ import           Data.Text (Text)
 import           Data.Word
 import           GHC.TypeNats
 import           Numeric.Natural
-import           Prettyprinter
 import           System.IO (Handle, hPutStrLn)
 
 import qualified Data.BitVector.Sized as BV
@@ -233,6 +234,7 @@ import           Lang.Crucible.LLVM.Extension
 import           Lang.Crucible.LLVM.Bytes
 import           Lang.Crucible.LLVM.Errors.MemoryError
    (MemErrContext, MemoryErrorReason(..), MemoryOp(..), ppMemoryErrorReason)
+import qualified Lang.Crucible.LLVM.Errors.MemoryError as ME
 import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
 import           Lang.Crucible.LLVM.MemType
 import qualified Lang.Crucible.LLVM.MemModel.MemLog as ML
@@ -315,7 +317,7 @@ assertStoreError ::
   (IsSymInterface sym, Partial.HasLLVMAnn sym, 1 <= wptr) =>
   sym ->
   MemErrContext sym wptr ->
-  MemoryErrorReason sym wptr ->
+  MemoryErrorReason ->
   Pred sym ->
   IO ()
 assertStoreError sym errCtx rsn p =
@@ -428,14 +430,14 @@ evalStmt sym = eval
   eval (LLVM_LoadHandle mvar ltp (regValue -> ptr) args ret) =
      do mem <- getMem mvar
         let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr
-        mhandle <- liftIO $ doLookupHandle sym mem ptr gsym
+        mhandle <- liftIO $ doLookupHandle sym mem ptr
         let mop = MemLoadHandleOp ltp gsym ptr (memImplHeap mem)
         let expectedTp = FunctionHandleRepr args ret
         case mhandle of
-           Left doc -> lift $
-             do p <- Partial.annotateME sym mop (BadFunctionPointer doc) (falsePred sym)
+           Left lookupErr -> lift $
+             do p <- Partial.annotateME sym mop (BadFunctionPointer lookupErr) (falsePred sym)
                 loc <- getCurrentProgramLoc sym
-                let err = SimError loc (AssertFailureSimError "Failed to load function handle" (show doc))
+                let err = SimError loc (AssertFailureSimError "Failed to load function handle" (show (ME.ppFuncLookupError lookupErr)))
                 addProofObligation sym (LabeledPred p err)
                 abortExecBecause (AssertionFailure err)
 
@@ -748,29 +750,19 @@ doLookupHandle
   => sym
   -> MemImpl sym
   -> LLVMPtr sym wptr
-  -> Maybe String
-  -> IO (Either (Doc ann) a)
-doLookupHandle _sym mem ptr gsym = do
+  -> IO (Either ME.FuncLookupError a)
+doLookupHandle _sym mem ptr = do
   let LLVMPointer blk _ = ptr
-  let ptrDoc = hang 2 $
-         case gsym of
-           Just s  -> viaShow s
-           Nothing -> ppPtr ptr
   case asNat blk of
-    Nothing -> return (Left ("Cannot resolve a symbolic pointer to a function handle:" <+> ptrDoc))
+    Nothing -> return (Left ME.SymbolicPointer)
     Just i
-      | i == 0 -> return (Left ("Cannot treat raw bitvector as function pointer:" <+> ptrDoc))
+      | i == 0 -> return (Left ME.RawBitvector)
       | otherwise ->
           case Map.lookup i (memImplHandleMap mem) of
-            Nothing -> return (Left ("No implementation or override found for pointer:" <+> ptrDoc))
+            Nothing -> return (Left ME.NoOverride)
             Just x ->
               case fromDynamic x of
-                Nothing ->
-                  return $ Left $ vcat
-                  [ "Data associated with the pointer found, but was not a callable function:"
-                  , hang 2 (viaShow (dynTypeRep x))
-                  , ptrDoc
-                  ]
+                Nothing -> return (Left (ME.Uncallable (dynTypeRep x)))
                 Just a  -> return (Right a)
 
 -- | Free the memory region pointed to by the given pointer.

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

@@ -770,7 +770,7 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) =
       StorageType ->
       LLVMPtr sym w ->
       ReadMem sym (PartLLVMVal sym)
-    fallback0 tp l =
+    fallback0 tp _l =
       liftIO $
         if laxLoadsAndStores ?memOpts
         then Partial.totalLLVMVal sym <$> freshLLVMVal sym tp
@@ -779,7 +779,7 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) =
                 -- and we can be relatively sure the annotation will survive.
                 b <- freshConstant sym emptySymbol BaseBoolRepr
                 Partial.Err <$>
-                  Partial.annotateME sym mop (NoSatisfyingWrite tp l) b
+                  Partial.annotateME sym mop (NoSatisfyingWrite tp) b
 
     go :: (StorageType -> LLVMPtr sym w -> ReadMem sym (PartLLVMVal sym)) ->
           LLVMPtr sym w ->

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

@@ -244,7 +244,7 @@ annotateUB sym ub p =
 annotateME :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
   sym ->
   MemoryOp sym w ->
-  MemoryErrorReason sym w ->
+  MemoryErrorReason ->
   Pred sym ->
   IO (Pred sym)
 annotateME sym mop rsn p =
@@ -271,7 +271,7 @@ data PartLLVMVal sym where
   NoErr :: Pred sym -> LLVMVal sym -> PartLLVMVal sym
 
 partErr :: (IsSymInterface sym, HasLLVMAnn sym, 1 <= w) =>
-  sym -> MemoryOp sym w -> MemoryErrorReason sym w -> IO (PartLLVMVal sym)
+  sym -> MemoryOp sym w -> MemoryErrorReason -> IO (PartLLVMVal sym)
 partErr sym errCtx rsn =
   do p <- annotateME sym errCtx rsn (falsePred sym)
      pure (Err p)
@@ -295,7 +295,7 @@ attachMemoryError ::
   sym ->
   Pred sym ->
   MemoryOp sym w ->
-  MemoryErrorReason sym w ->
+  MemoryErrorReason ->
   PartLLVMVal sym ->
   IO (PartLLVMVal sym)
 attachMemoryError sym pnew mop rsn pv =

crux-llvm/test-data/golden/golden/invoke-test.good

@@ -2,9 +2,9 @@
 [Crux]   internal: error: in _ZN3std2rt10lang_start17h4f32aa1279b9079fE
 [Crux]   Failed to load function handle
 [Crux]   Details:
-[Crux]     No implementation or override found for pointer: "_ZN3std2rt19lang_start_internal17h3dc68cf5532522d7E"
+[Crux]     No implementation or override found for pointer
 [Crux]     The given pointer could not be resolved to a callable function
-[Crux]     No implementation or override found for pointer: "_ZN3std2rt19lang_start_internal17h3dc68cf5532522d7E"
+[Crux]     No implementation or override found for pointer
 [Crux]     Attempting to load callable function with type: i64({ }*, [3 x i64]*, i64, i8**)
 [Crux]       Via pointer: Global symbol "_ZN3std2rt19lang_start_internal17h3dc68cf5532522d7E" (1, 0x0:[64])
 [Crux]     In memory state:

uc-crux-llvm/src/UCCrux/LLVM/Classify.hs

@@ -469,8 +469,8 @@ doClassifyBadBehavior appCtx modCtx funCtx sym memImpl skipped simError (Crucibl
         requirePossiblePointer ReadNonPointer ptr
     LLVMErrors.BBMemoryError
       ( MemError.MemoryError
-          (summarizeOp -> (_expl, _ptr, mem))
-          (MemError.NoSatisfyingWrite _storageType ptr)
+          (summarizeOp -> (_expl, ptr, mem))
+          (MemError.NoSatisfyingWrite _storageType)
         ) ->
         do
           ann <- liftIO $ getPtrBlockOrOffsetAnn ptr