Replace fake ZeroInit lattice with flat lattice#2035
Conversation
| if x = Bot then | ||
| zero_init_value t (* This should be zero initialized *) | ||
| else | ||
| x (* This already contains some value *) |
There was a problem hiding this comment.
This already existing logic seems suspicious: seems it could be non-monotonic and unsound that zero_init_value isn't always included.
Maybe this was fine because the malloc and calloc cases were mutually exclusive before, but now with the top possibility, I'm not so sure anymore. If an initialized malloc blob (so not bot) is joined with an uninitialized calloc blob, then this doesn't add the zero-initialization.
Extracted from SV-COMP where it even crashed instead of being unsound.
|
In addition to fixing the exceptions introduced by #2030 (comment), this fixes an existing |
| let zero_init_calloced_memory zeroinit x t = | ||
| if ZeroInit.is_malloc zeroinit then | ||
| (* This Blob came from malloc *) | ||
| x | ||
| else if x = Bot then | ||
| (* This Blob came from calloc *) | ||
| zero_init_value t (* This should be zero initialized *) | ||
| else | ||
| x (* This already contains some value *) | ||
| let malloc = | ||
| if ZeroInit.may_malloc zeroinit then | ||
| (* This Blob came from malloc *) | ||
| x | ||
| else | ||
| Bot | ||
| in | ||
| let calloc = | ||
| if ZeroInit.may_calloc zeroinit then ( | ||
| (* This Blob came from calloc *) | ||
| if x = Bot then | ||
| zero_init_value t (* This should be zero initialized *) | ||
| else | ||
| x (* This already contains some value *) | ||
| ) | ||
| else | ||
| Bot | ||
| in | ||
| join malloc calloc |
|
Can you elaborate on why calloc and malloc blobs ever need to be merged? Should we not try to keep these mutually exclusive? |
|
I think we've tried to keep it that way for so long and been surprisingly successful at it. The added tests show cases where such joins are already happening. In one case it caused unsoundness, in the other a crash. I don't know how else we could fix those. I guess being path-sensitive w.r.t. the kind of allocation for each one in the state would avoid it but that can be exponentially expensive. |
Another option would be to replace blobs with sets of blobs in the |
|
I left a TODO with the possibly strange behavior of top I suspect the reason a few more instances where this happens came up in #2030 is a temporary situation. While staring at memOutOfBounds I discovered another significant imprecision in it: for a given points-to-set, it joins all the pointed abstract values and all of their sizes and then does the bounds check, as opposed to checking per-pointee. Although in general it might not be entirely avoidable due to mallocWrappers collapsing things, as seen in one of the tests added here. |
This is to potentially fix the issue from #2030 (comment).
The added test shows a handcrafted case where a
mallocblob is joined with acallocblob, which requires the joining of theirZeroInitvalues.Previously, this raised an exception and even caused unsoundness because of the fake lattice being used.
This PR replaces that with a flat boolean lattice which can represent top.
TODO