Revert the change to the use of unbounded arrays #6232
Conversation
This was introduced in diffblue#6194 but reported as breaking in diffblue#6230.
|
@SaswatPadhi it would be great if you could let me know if this fixes your issue. |
Codecov Report
@@ Coverage Diff @@
## develop #6232 +/- ##
===========================================
+ Coverage 67.40% 75.41% +8.01%
===========================================
Files 1157 1459 +302
Lines 95236 161447 +66211
===========================================
+ Hits 64197 121761 +57564
- Misses 31039 39686 +8647
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
|
@TGWDB I would love a regression test and was hoping that @SaswatPadhi might be able to provide one. |
|
Thanks for the fix, @martin-cs. We noticed this on a large s2n proof harness, but let me try to reduce it to a small regression test. I would look into large / dynamically allocated arrays, as you suggested. |
|
Thanks @SaswatPadhi |
|
This is the most I could shrink it to: #include <assert.h>
#include <stdint.h>
#include <stdlib.h>
static const uint16_t extensions[] = { 0, 1, 2, 3, 4, 5 };
#define COUNT (sizeof(extensions) / sizeof(extensions[0]))
typedef struct {
uint8_t *data;
uint32_t size;
uint32_t allocated;
unsigned growable :1;
} ext;
struct context {
ext exts[COUNT];
};
struct conn {
void *test;
struct context ctx;
};
int main() {
struct conn *s = malloc(sizeof(*s));
if(s != NULL) s->test = NULL;
}If I shrink the |
|
I have tried this example with the latest develop ( 06c563a ) and it doesn't crash. Can you double check and say something about the environment? |
|
I also tested the example on |
|
Sorry, I should have mentioned the full commandline: |
|
Ah, yes, that does it! Thanks @SaswatPadhi |
|
Any updates on that PR? @martin-cs @kroening |
|
@feliperodri I am working on the test case that @SaswatPadhi sent and will add it ASAP. |
Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. This reverts diffblue#6232, but now includes additional changes to the array theory to handle nested struct members no different from members of a top-level struct. Fixes: diffblue#2018
Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. This reverts diffblue#6232, but now includes additional changes to the array theory to handle nested struct members no different from members of a top-level struct. Fixes: diffblue#2018
Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. We previously attempted to do this in in diffblue#6194 (inspired by diffblue#2108, but not picking up all its changes), but then reverted the gist of the change in diffblue#6232 as `array-bug-6230/main.c` demonstrated lingering issues. This PR now addresses the flaw in the array theory back-end. We may still run into performance regressions as the threshold of 1000 bits of total size of the array object is possibly lower than where the cost of bit-blasting exceeds the cost of constraints produced by our current array theory implementation. Two of our existing regression tests already demonstrate this problem, hence those now use `--arrays-uf-never`.
This was introduced in #6194 but reported as breaking in #6230.