Heapster Widening and Implication Prover Improvements #1796
Conversation
…e widening by substituting in shape of the equal block for the eqsh shape
…atomic permissions
| splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> | ||
| PExpr_EqShape _len (PExpr_Var b)) | ||
| -- FIXME: make sure the returned shape fits into len bytes! | ||
| | Just sh <- blsubst b | ||
| = splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh }) | ||
| splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_EqShape _ _) = Nothing |
There was a problem hiding this comment.
Nit pick: combine the two llvmBlockShape -> PExpr_EqShape ... cases:
| splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> | |
| PExpr_EqShape _len (PExpr_Var b)) | |
| -- FIXME: make sure the returned shape fits into len bytes! | |
| | Just sh <- blsubst b | |
| = splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh }) | |
| splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_EqShape _ _) = Nothing | |
| splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> | |
| PExpr_EqShape _len (PExpr_Var b)) | |
| -- FIXME: make sure the returned shape fits into len bytes! | |
| | Just sh <- blsubst b | |
| = splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh }) | |
| | otherwise | |
| = Nothing |
Aside from making this slightly more readable, this should be a little easier for GHC's pattern-match coverage checker to handle.
There was a problem hiding this comment.
I see what you mean, that it's weird to use a view pattern with a record accessor. I'll fix that.
There was a problem hiding this comment.
Wait, except I guess that's not what you were suggesting. I guess you were suggesting I use an otherwise branch of the pattern-match. That's not actually quite correct, because that would only match when the second argument to PExpr_EqShape is of the form PExpr_Var b, whereas the current version doesn't match on that argument at all in this case. TBF, PExpr_Var b is the only PermExpr expression that can match at that particular type.
Maybe this is all bikeshedding, because there already is a catch-all case at the end of the function?
There was a problem hiding this comment.
Ah, quite right. Indeed, you would need to move the match on PExpr_Var into a pattern guard to preserve the existing semantics of this function:
| splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> | |
| PExpr_EqShape _len (PExpr_Var b)) | |
| -- FIXME: make sure the returned shape fits into len bytes! | |
| | Just sh <- blsubst b | |
| = splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh }) | |
| splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_EqShape _ _) = Nothing | |
| splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> | |
| PExpr_EqShape _len blk) | |
| -- FIXME: make sure the returned shape fits into len bytes! | |
| | PExpr_Var b <- blk | |
| , Just sh <- blsubst b | |
| = splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh }) | |
| | otherwise | |
| = Nothing |
I'll let you make the call on whether the old or new code is more readable.
| do (bp_l,bp') <- splitLLVMBlockPerm (const Nothing) (bvRangeOffset rng) bp | ||
| return ([bp_l],bp') | ||
| else return ([],bp) | ||
| bp_r <- | ||
| if bvInRange (bvRangeEnd rng) (llvmBlockRange bp) then | ||
| snd <$> splitLLVMBlockPerm (bvRangeEnd rng) bp | ||
| snd <$> splitLLVMBlockPerm (const Nothing) (bvRangeEnd rng) bp |
There was a problem hiding this comment.
Is it worth commenting why these two calls to splitLLVMBlockPerm have empty substitutions?
There was a problem hiding this comment.
Fair enough, I can do that
eddywestbrook
added
PR: ready to merge
This PR includes 3 relatively small changes to Heapster to help in verifying some (somewhat) "real world" C code:
memblockpermissions witheqshshapes can be widening by substituting in shape of the equal block for theeqshshape;recombinePermto handle more cases with named permissions.