Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow pointers to one past the end of allocations #519

Merged
merged 4 commits into from
Aug 5, 2019
Merged

Allow pointers to one past the end of allocations #519

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
239573c
typeOfSetupValue: names for numbers in array length error messages
langston-barrett Jul 30, 2019
b673279
Crucible/LLVM: Allow pointers to one past the end of allocations
langston-barrett Aug 5, 2019
e7859e9
matchArg: cases for SetupElem and SetupField
langston-barrett Aug 5, 2019
828e04f
fix incomplete pattern match
langston-barrett Aug 5, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions src/SAWScript/Crucible/Common/Override.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ data OverrideFailureReason ext
| BadReturnSpecification (Some Crucible.TypeRepr)
-- ^ type mismatch in return specification
| NonlinearPatternNotSupported
| BadEqualityComparison String -- ^ Comparison on an undef value
| BadEqualityComparison -- ^ Comparison on an undef value
| BadPointerLoad (Either (MS.PointsTo ext) PP.Doc) PP.Doc
-- ^ @loadRaw@ failed due to type error
| StructuralMismatch PP.Doc PP.Doc (Maybe (ExtType ext)) (ExtType ext)
Expand Down Expand Up @@ -194,9 +194,8 @@ ppOverrideFailureReason rsn = case rsn of
]
NonlinearPatternNotSupported ->
PP.text "nonlinear pattern not supported"
BadEqualityComparison globName ->
PP.text "global initializer containing `undef` compared for equality:" PP.<$$>
(PP.indent 2 (PP.text globName))
BadEqualityComparison ->
PP.text "value containing `undef` compared for equality"
BadPointerLoad pointsTo msg ->
PP.text "error when loading through pointer that" PP.<+>
PP.text "appeared in the override's points-to precondition(s):" PP.<$$>
Expand Down
110 changes: 58 additions & 52 deletions src/SAWScript/Crucible/LLVM/Override.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -850,61 +850,67 @@ matchArg ::
SetupValue (Crucible.LLVM arch) {- ^ expected specification value -} ->
OverrideMatcher (LLVM arch) md ()

matchArg opts sc cc cs prepost actual expectedTy expected@(SetupTerm expectedTT)
| Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT
, Right tval <- Cryptol.evalType mempty tyexpr
= do sym <- Ov.getSymInterface
failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual
matchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)

-- match the fields of struct point-wise
matchArg opts sc cc cs prepost (Crucible.LLVMValStruct xs) (Crucible.StructType fields) (SetupStruct () _ zs) =
sequence_
[ matchArg opts sc cc cs prepost x y z
| ((_,x),y,z) <- zip3 (V.toList xs)
(V.toList (Crucible.fiType <$> Crucible.siFields fields))
zs ]

matchArg opts sc cc cs prepost actual expectedTy g@(SetupGlobalInitializer () n) = do
(globInitTy, globInitVal) <- resolveSetupValueLLVM opts cc sc cs g
sym <- Ov.getSymInterface
if expectedTy /= globInitTy
then failure (cs ^. MS.csLoc) =<<
mkStructuralMismatch opts cc sc cs actual g expectedTy
else liftIO (Crucible.testEqual sym globInitVal actual) >>=
\case
Nothing -> failure (cs ^. MS.csLoc) (BadEqualityComparison n)
Just pred_ ->
addAssert pred_ =<<
notEqual prepost opts (cs ^. MS.csLoc) cc sc cs g actual

matchArg opts sc cc cs prepost actual@(Crucible.LLVMValInt blk off) expectedTy setupval =
case setupval of
SetupVar var | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
do assignVar cc (cs ^. MS.csLoc) var (Crucible.LLVMPointer blk off)

SetupNull () | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
do sym <- Ov.getSymInterface
p <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off))
addAssert p =<<
notEqual prepost opts (cs ^. MS.csLoc) cc sc cs setupval actual

SetupGlobal () name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
do let mem = cc^.ccLLVMEmptyMem
sym <- Ov.getSymInterface
ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name)
pred_ <- liftIO $
Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2
addAssert pred_ =<<
notEqual prepost opts (cs ^. MS.csLoc) cc sc cs setupval actual
matchArg opts sc cc cs prepost actual expectedTy expected =
case (actual, expectedTy, expected) of
(_, _, SetupTerm expectedTT)
| Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT
, Right tval <- Cryptol.evalType mempty tyexpr
-> do sym <- Ov.getSymInterface
failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual
matchTerm sc cc (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)

-- match the fields of struct point-wise
(Crucible.LLVMValStruct xs, Crucible.StructType fields, SetupStruct () _ zs) ->
sequence_
[ matchArg opts sc cc cs prepost x y z
| ((_,x),y,z) <- zip3 (V.toList xs)
(V.toList (Crucible.fiType <$> Crucible.siFields fields))
zs ]

(_, Crucible.PtrType _, SetupElem () _ _) -> resolveAndMatch
(_, Crucible.PtrType _, SetupField () _ _) -> resolveAndMatch
(_, _, SetupGlobalInitializer () _) -> resolveAndMatch

(Crucible.LLVMValInt blk off, _, _) ->
case expected of
SetupVar var | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
do assignVar cc (cs ^. MS.csLoc) var (Crucible.LLVMPointer blk off)

SetupNull () | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
do sym <- Ov.getSymInterface
p <- liftIO (Crucible.ptrIsNull sym Crucible.PtrWidth (Crucible.LLVMPointer blk off))
addAssert p =<<
notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual

SetupGlobal () name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth ->
do let mem = cc^.ccLLVMEmptyMem
sym <- Ov.getSymInterface
ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name)
pred_ <- liftIO $
Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2
addAssert pred_ =<<
notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual

_ -> failure (cs ^. MS.csLoc) =<<
mkStructuralMismatch opts cc sc cs actual expected expectedTy

_ -> failure (cs ^. MS.csLoc) =<<
mkStructuralMismatch opts cc sc cs actual setupval expectedTy
mkStructuralMismatch opts cc sc cs actual expected expectedTy

matchArg opts sc cc cs _prepost actual expectedTy expected = do
failure (cs ^. MS.csLoc) =<<
mkStructuralMismatch opts cc sc cs actual expected expectedTy
where
resolveAndMatch = do
(ty, val) <- resolveSetupValueLLVM opts cc sc cs expected
sym <- Ov.getSymInterface
if expectedTy /= ty
then failure (cs ^. MS.csLoc) =<<
mkStructuralMismatch opts cc sc cs actual expected expectedTy
else liftIO (Crucible.testEqual sym val actual) >>=
\case
Nothing -> failure (cs ^. MS.csLoc) BadEqualityComparison
Just pred_ ->
addAssert pred_ =<<
notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual

------------------------------------------------------------------------

Expand Down
14 changes: 9 additions & 5 deletions src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,15 +199,19 @@ typeOfSetupValue' cc env nameEnv val =
typeOfSetupValue' cc env nameEnv (SetupElem () v i)
SetupElem () v i ->
do memTy <- typeOfSetupValue cc env nameEnv v
let msg = "typeOfSetupValue: crucible_elem requires pointer to struct or array"
let msg = "typeOfSetupValue: crucible_elem requires pointer to struct or array, found " ++ show memTy
case memTy of
Crucible.PtrType symTy ->
case let ?lc = lc in Crucible.asMemType symTy of
Right memTy' ->
case memTy' of
Crucible.ArrayType n memTy''
| fromIntegral i < n -> return (Crucible.PtrType (Crucible.MemType memTy''))
| otherwise -> fail $ "typeOfSetupValue: array type index out of bounds: " ++ show (i, n)
| fromIntegral i <= n -> return (Crucible.PtrType (Crucible.MemType memTy''))
| otherwise -> fail $ unwords $
[ "typeOfSetupValue: array type index out of bounds"
, "(index: " ++ show i ++ ")"
, "(array length: " ++ show n ++ ")"
]
Crucible.StructType si ->
case Crucible.siFieldInfo si i of
Just fi -> return (Crucible.PtrType (Crucible.MemType (Crucible.fiType fi)))
Expand Down Expand Up @@ -284,14 +288,14 @@ resolveSetupVal cc env tyenv nameEnv val =
resolveSetupVal cc env tyenv nameEnv (SetupElem () v i)
SetupElem () v i ->
do memTy <- typeOfSetupValue cc tyenv nameEnv v
let msg = "resolveSetupVal: crucible_elem requires pointer to struct or array"
let msg = "resolveSetupVal: crucible_elem requires pointer to struct or array, found " ++ show memTy
delta <- case memTy of
Crucible.PtrType symTy ->
case let ?lc = lc in Crucible.asMemType symTy of
Right memTy' ->
case memTy' of
Crucible.ArrayType n memTy''
| fromIntegral i < n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
| fromIntegral i <= n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'')
Crucible.StructType si ->
case Crucible.siFieldOffset si i of
Just d -> return d
Expand Down