The checker did not work with negative array index at return.
Specially for -1 it did not produce a bug.
assumeInBound may not work correct with negative values so a pre-
check is added to the checker for negative array index.
Details
Diff Detail
- Repository
- rG LLVM Github Monorepo
Event Timeline
If assumeInBound() behaves unexpectedly, we should probably fix that instead.
This change would workaround the issue, instead of fixing it. By fixing the root cause all users of assumeInBound() would benefit.
I recommend you to have a deeper look at the insides of assumeInBound() investigating why it behaves that way.
assumeInBound should check if 0<=Idx<UpperBound. In this case it makes no sense of UpperBound is negative.
The problem appears in cases like this:
int *conjure(); int *m1() { int *p = conjure(); return p - 1; }
The extent of the region is symbolic and the index is a constant, so a constraint for the extent appears after assumeInBound.
For positive index (at p - 1 in the code) it looks correct, if p + 1 is used:
StOutBound:"program_state": { "store": { "pointer": "0x6acdd8", "items": [ { "cluster": "GlobalInternalSpaceRegion", "pointer": "0x6acb98", "items": [ { "kind": "Default", "offset": 0, "value": "conj_$0{int, LC1, S666, #1}" } ]}, { "cluster": "GlobalSystemSpaceRegion", "pointer": "0x6accb8", "items": [ { "kind": "Default", "offset": 0, "value": "conj_$1{int, LC1, S666, #1}" } ]} ]}, "environment": { "pointer": "0x6ac010", "items": [ { "lctx_id": 1, "location_context": "#0 Call", "calling": "conjured::b3", "location": null, "items": [ { "stmt_id": 684, "pretty": "p + 1", "value": "&Element{SymRegion{conj_$2{int *, LC1, S666, #1}},1 S64b,int}" } ]} ]}, "constraints": [ { "symbol": "(extent_$3{SymRegion{conj_$2{int *, LC1, S666, #1}}}) / 4", "range": "{ [0, 1] }" } ], "equivalence_classes": null, "disequality_info": null, "dynamic_types": null, "dynamic_casts": null, "constructing_objects": null, "checker_messages": null } StInBound:"program_state": { "store": { "pointer": "0x6acdd8", "items": [ { "cluster": "GlobalInternalSpaceRegion", "pointer": "0x6acb98", "items": [ { "kind": "Default", "offset": 0, "value": "conj_$0{int, LC1, S666, #1}" } ]}, { "cluster": "GlobalSystemSpaceRegion", "pointer": "0x6accb8", "items": [ { "kind": "Default", "offset": 0, "value": "conj_$1{int, LC1, S666, #1}" } ]} ]}, "environment": { "pointer": "0x6ac010", "items": [ { "lctx_id": 1, "location_context": "#0 Call", "calling": "conjured::b3", "location": null, "items": [ { "stmt_id": 684, "pretty": "p + 1", "value": "&Element{SymRegion{conj_$2{int *, LC1, S666, #1}},1 S64b,int}" } ]} ]}, "constraints": [ { "symbol": "(extent_$3{SymRegion{conj_$2{int *, LC1, S666, #1}}}) / 4", "range": "{ [-9223372036854775808, -1], [2, 9223372036854775807] }" } ], "equivalence_classes": null, "disequality_info": null, "dynamic_types": null, "dynamic_casts": null, "constructing_objects": null, "checker_messages": null }
For p - 1 only the StOutBound exists:
OutBound:"program_state": { "store": { "pointer": "0x161bdd8", "items": [ { "cluster": "GlobalInternalSpaceRegion", "pointer": "0x161bb98", "items": [ { "kind": "Default", "offset": 0, "value": "conj_$0{int, LC1, S666, #1}" } ]}, { "cluster": "GlobalSystemSpaceRegion", "pointer": "0x161bcb8", "items": [ { "kind": "Default", "offset": 0, "value": "conj_$1{int, LC1, S666, #1}" } ]} ]}, "environment": { "pointer": "0x161b010", "items": [ { "lctx_id": 1, "location_context": "#0 Call", "calling": "conjured::b3", "location": null, "items": [ { "stmt_id": 684, "pretty": "p - 1", "value": "&Element{SymRegion{conj_$2{int *, LC1, S666, #1}},-1 S64b,int}" } ]} ]}, "constraints": [ { "symbol": "(extent_$3{SymRegion{conj_$2{int *, LC1, S666, #1}}}) / 4", "range": "{ [-9223372036854775808, 9223372036854775807] }" } ], "equivalence_classes": null, "disequality_info": null, "dynamic_types": null, "dynamic_casts": null, "constructing_objects": null, "checker_messages": null }
For p - 2 the StOutBound has constraint { [-9223372036854775808, -2], [0, 9223372036854775807] } and StInBound has { [-1, -1] }. Probably this is how the overflow situation is handled or it is not correct.
This checker can do anyway nothing with a negative index. It may be out of bound in a non-symbolic region but can be valid.
Would it make sense to tweak assumeInBound in a way to handle symbolic regions differently than concrete regions?
I mean
static int arr[10]; return arr - 1; // we want a warning here ... int *p = conjure(); return p - 1; // no warning here