[PATCH] D36471: [StaticAnalyzer] Try to calculate arithmetic result when operand has a range of possible values

Daniel Marjamäki via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon Nov 6 05:42:00 PST 2017


danielmarjamaki updated this revision to Diff 121726.
danielmarjamaki added a comment.
Herald added a subscriber: szepet.

I have updated the patch so it uses evalBinOpNN. This seems to work properly.

I have a number of TODOs in the test cases that should be fixed. Truncations are not handled properly.

Here is a short example code:

  void f(unsigned char X) {
    if (X >= 10 && X <= 50) {
      unsigned char Y = X + 0x100; // truncation
      clang_analyzer_eval(Y >= 10 && Y <= 50); // expected-warning{{FALSE}}
    }
  }

The expected-warning should be TRUE but currently FALSE is written.

When the "Y >= 10" condition is evaluated the ProgramState is:

  Store (direct and default bindings), 0x222ab0fe5f8 :
   (Y,0,direct) : (unsigned char) ((reg_$0<unsigned char X>) + 256)
  
  Expressions:
   (0x222a96d6050,0x222ab0eb930) X + 256 : (unsigned char) ((reg_$0<unsigned char X>) + 256)
   (0x222a96d6050,0x222ab0eb960) clang_analyzer_eval : &code{clang_analyzer_eval}
   (0x222a96d6050,0x222ab0eb988) Y : &Y
   (0x222a96d6050,0x222ab0eb9d8) Y : (unsigned char) ((reg_$0<unsigned char X>) + 256)
   (0x222a96d6050,0x222ab0eb9f0) Y : (unsigned char) ((reg_$0<unsigned char X>) + 256)
   (0x222a96d6050,0x222ab0eba08) Y >= 10 : ((unsigned char) ((reg_$0<unsigned char X>) + 256)) >= 10
   (0x222a96d6050,0x222ab0ebb28) clang_analyzer_eval : &code{clang_analyzer_eval}
  Ranges of symbol values:
   reg_$0<unsigned char X> : { [10, 50] }
   (reg_$0<unsigned char X>) + 256 : { [10, 50] }

It seems to me that the symbol initialization does not handle the range properly. Imho there is nothing wrong with the calculation. What you think about adding a range like below?

  (unsigned char) ((reg_$0<unsigned char X>) + 256) : { [10, 50] }




Repository:
  rL LLVM

https://reviews.llvm.org/D36471

Files:
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
  lib/StaticAnalyzer/Core/ExprEngineC.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  test/Analysis/range_calc.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D36471.121726.patch
Type: text/x-patch
Size: 8855 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20171106/783cf74e/attachment.bin>


More information about the cfe-commits mailing list