Skip to content

Commit

Permalink
Check bitvector types in crucible_llvm_extract (#567)
Browse files Browse the repository at this point in the history
Because `crucible-llvm` merges integer and pointer types, it is not
sufficient to look at Crucible types to determine whether a CFG coming
from LLVM takes pointer arguments or returns a pointer. Instead, we have
to look at the original LLVM types. This commit does that, and produces
an error if `crucible_llvm_extract` is used with a function that has
poiinter types anywhere in its signature.

Fixes #521.
  • Loading branch information
Aaron Tomb authored Oct 17, 2019
1 parent f3badd0 commit 6adf6f1
Show file tree
Hide file tree
Showing 5 changed files with 20 additions and 1 deletion.
Binary file added intTests/test_issue521/ptr.bc
Binary file not shown.
3 changes: 3 additions & 0 deletions intTests/test_issue521/ptr.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
unsigned int add(unsigned int *x, unsigned int *y) {
return *x + *y;
}
2 changes: 2 additions & 0 deletions intTests/test_issue521/test.saw
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
m <- llvm_load_module "ptr.bc";
fails (crucible_llvm_extract m "add");
3 changes: 3 additions & 0 deletions intTests/test_issue521/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw
13 changes: 12 additions & 1 deletion src/SAWScript/Crucible/LLVM/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"]
Expand Down

0 comments on commit 6adf6f1

Please sign in to comment.