[PATCH] D107960: [clang][analyzer] Make ReturnPtrRange checker warn at negative index.

[Balázs Kéri via Phabricator via cfe-commits]

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