diff --git a/intTests/test_issue521/ptr.bc b/intTests/test_issue521/ptr.bc new file mode 100644 index 0000000000..1ecc22bfb8 Binary files /dev/null and b/intTests/test_issue521/ptr.bc differ diff --git a/intTests/test_issue521/ptr.c b/intTests/test_issue521/ptr.c new file mode 100644 index 0000000000..c7f42609cd --- /dev/null +++ b/intTests/test_issue521/ptr.c @@ -0,0 +1,3 @@ +unsigned int add(unsigned int *x, unsigned int *y) { + return *x + *y; +} diff --git a/intTests/test_issue521/test.saw b/intTests/test_issue521/test.saw new file mode 100644 index 0000000000..6e0aea0a93 --- /dev/null +++ b/intTests/test_issue521/test.saw @@ -0,0 +1,2 @@ +m <- llvm_load_module "ptr.bc"; +fails (crucible_llvm_extract m "add"); diff --git a/intTests/test_issue521/test.sh b/intTests/test_issue521/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_issue521/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index f658e5d287..d49b771795 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -64,7 +64,7 @@ import Control.Monad.State hiding (fail) import Control.Monad.Fail (MonadFail(..)) import qualified Data.Bimap as Bimap import Data.Char (isDigit) -import Data.Foldable (for_, toList, find) +import Data.Foldable (for_, toList, find, fold) import Data.Function import Data.IORef import Data.List @@ -1103,6 +1103,17 @@ crucible_llvm_extract :: crucible_llvm_extract bic opts (Some lm) fn_name = do let ctx = lm ^. modTrans . Crucible.transContext let ?lc = ctx^.Crucible.llvmTypeCtx + let edef = findDefMaybeStatic (lm ^. modAST) fn_name + case edef of + Right defs -> do + let defTypes = fold $ + NE.map (map L.typedType . L.defArgs) defs <> + NE.map (\d -> [L.defRetType d]) defs + when (any L.isPointer defTypes) $ + fail "Pointer types are not supported by `crucible_llvm_extract`." + when (any L.isAlias defTypes) $ + fail "Type aliases are not supported by `crucible_llvm_extract`." + Left err -> fail (displayVerifExceptionOpts opts err) setupLLVMCrucibleContext bic opts lm $ \cc -> case Map.lookup (fromString fn_name) (Crucible.cfgMap (cc^.ccLLVMModuleTrans)) of Nothing -> fail $ unwords ["function", fn_name, "not found"]