balazske added a comment.
`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.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D107960/new/
https://reviews.llvm.org/D107960
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
