Page MenuHomePhabricator

[clang][analyzer] Make ReturnPtrRange checker warn at negative index.
Needs RevisionPublic

Authored by balazske on Aug 12 2021, 6:29 AM.

Details

Summary

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.

Diff Detail

Event Timeline

balazske created this revision.Aug 12 2021, 6:29 AM
balazske requested review of this revision.Aug 12 2021, 6:29 AM
Herald added a project: Restricted Project. · View Herald TranscriptAug 12 2021, 6:29 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
steakhal requested changes to this revision.Aug 12 2021, 7:00 AM

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.

This revision now requires changes to proceed.Aug 12 2021, 7:00 AM

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