Implement C library string functions via array_{copy,replace,set} #795
Conversation
tautschnig
force-pushed
the
array-replace
branch
from
5b4b957 to
de3de81
Compare
|
Some cleanup and debugging is still in progress -> do not merge. |
| __CPROVER_array_set(res, 0); | ||
| else if(nmemb==1) | ||
| for(__CPROVER_size_t i=0; i<size; ++i) | ||
| ((char*)res)[i]=0; | ||
| #endif |
There was a problem hiding this comment.
Is there a reason not to use array_set for the nmemb==1 case?
| @@ -500,7 +516,7 @@ inline char *strdup(const char *str) | |||
|
|
|||
| #undef memcpy | |||
|
|
|||
| inline void *memcpy(void *dst, const void *src, size_t n) | |||
| void *memcpy(void *dst, const void *src, size_t n) | |||
There was a problem hiding this comment.
A benefit of the 'inline' is that the assertions get the location of the call site.
There was a problem hiding this comment.
The problem is that we don't have frames for inlined copies of functions. Thus goto-symex cannot remove local variables when leaving the inlined function scope. Consequently we get type conflicts because we have multiple copies of an array of dynamic size with different size in the same frame.
| @@ -2315,7 +2315,7 @@ class extractbits_exprt:public exprt | |||
| const exprt &_lower, | |||
| const typet &_type):exprt(ID_extractbits, _type) | |||
| { | |||
| copy_to_operands(_src, _lower, _upper); | |||
| copy_to_operands(_src, _upper, _lower); | |||
| } | |||
There was a problem hiding this comment.
Should we swap the order of the parameters?
There was a problem hiding this comment.
A comment elsewhere says that this is the order that SMT-LIB uses. Otherwise I have no particular opinion about this...
tautschnig
force-pushed
the
array-replace
branch
2 times, most recently
from
6818e57 to
a320c8c
Compare
|
Some further testing on the code base that triggered this work is required on my end. Note that a320c8c is not acceptable as is. |
tautschnig
force-pushed
the
array-replace
branch
4 times, most recently
from
55fb898 to
237f248
Compare
|
I'm still unhappy and unsure about 37f248, but otherwise this appears to be ok in my (limited) testing. |
tautschnig
force-pushed
the
array-replace
branch
3 times, most recently
from
a257611 to
5d79f11
Compare
This hack is now gone as it proved unnecessary. |
This constructor had not been used thus far, thus this bug had gone unnoticed.
… vectors The additional example complements the existing big-endian-array1 test to also exercise little-endian flattening.
All other tests appear to be using arrays, these new ones don't.
This isn't well supported (if at all) in the back-end.
Multiple uses of the same library function might cause phi nodes merging arrays of different size, when really their objects have actually gone out of scope.
Properly handle byte_extract from arrays or structs, and also support the case where at least one of source or target size are known. This is a best-effort attempt: there could be out-of-bounds accesses in the program under scrutiny, which will be ignored. Finally ensure that flatten_byte_extract never returns another byte_extract.
…ter_predicates This will ensure consistent typing.
…ize_type member_offset_expr would otherwise yield mixed signed/unsigned plus expressions as size_of_expr is combined with member_offset_expr results.
This avoids byte-wise copy loops in several places.