donat.nagy added a comment.

In D158499#4608974 <https://reviews.llvm.org/D158499#4608974>, @danix800 wrote:

> One of the observable issue with inconsistent size type is
>
>   void clang_analyzer_eval(int);
>   
>   typedef unsigned long long size_t;
>   void *malloc(unsigned long size);
>   void free(void *);
>   
>   void symbolic_longlong_and_int0(long long len) {
>     char *a = malloc(5);
>     (void)a[len + 1]; // no-warning
>     // len: [-1,3]
>     clang_analyzer_eval(-1 <= len && len <= 3); // expected-warning {{TRUE}}
>     clang_analyzer_eval(0 <= len);              // expected-warning 
> {{UNKNOWN}}
>     clang_analyzer_eval(len <= 2);              // expected-warning 
> {{UNKNOWN}}
>     free(a);
>   }
>
> which is extracted from 
> `clang/test/Analysis/array-bound-v2-constraint-check.c`,
> with `DynamicMemoryModeling` turned on,
> the second warning does not hold anymore: `clang_analyzer_eval(0 <= len);`
> will be reported as `TRUE` which is not expected.
>
> `DynamicMemoryModeling` will record the extent of allocated memory as `5ULL`,
> `ArrayBoundV2` will do `len + 1 < 5ULL` assumption, simplified to `len < 
> 4ULL`,
> which casts `len` to unsigned, dropping `-1`, similar to
>
>   void clang_analyzer_eval(int);
>   
>   void test(int len) {
>     if (len >= -1 && len <= 4U) { // len is promoted into unsigned, thus can 
> never be negative
>         clang_analyzer_eval(0 <= len);              // TRUE
>     }
>   }

This issue is very interesting and scary -- I wouldn't have guessed that the 
core constraint handling algorithms are so buggy that things like this can 
happen 😦. I reproduced the issue and double-checked that the logic error is 
//not// in ArrayBoundV2 (despite that its simplification algorithm is messy and 
suspicious); I'd be very happy if this issue could be resolved (perhaps along 
with other inaccuracies of APSInt math...).


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D158499/new/

https://reviews.llvm.org/D158499

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to