[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-05 Thread Balazs Benics via cfe-commits

steakhal wrote:

My take is that the z3-based solver is crashing all over the place. So its not 
just slower. We anyways don't have CI checks for it.
Given all these, I'd rather not put more burden to the issue tracker regarding 
this. I'd consider it if these issues wouldn't be present though, but we are 
really far from that.

https://github.com/llvm/llvm-project/pull/74141
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-05 Thread via cfe-commits

DonatNagyE wrote:

With Z3 the new functionality does not work, but its absence is handled 
gracefully (the new methods return `NULL` and `core.BitwiseShift` emits the 
"old" message).

The Z3 solver is very "shaky" ground for me (if I understand it correctly it's 
too slow for stand-alone use, and so I didn't pay too much attention to it), so 
I don't have the confidence to create FIXMEs/tickets (my understanding of the 
goals is too vague and I don't understand the priorities/importance at all).

https://github.com/llvm/llvm-project/pull/74141
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-04 Thread Gábor Horváth via cfe-commits

Xazax-hun wrote:

Does this work with Z3 as the solver? Since Z3 is not officially supported, I 
think it is not a blocker, but I'd love to see some FIXMEs/tickets opened in 
that case. 

https://github.com/llvm/llvm-project/pull/74141
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-04 Thread via cfe-commits

https://github.com/DonatNagyE closed 
https://github.com/llvm/llvm-project/pull/74141
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-04 Thread via cfe-commits

DonatNagyE wrote:

I tested this patch on four open source projects (openssl, ffmpeg, postgres, 
contour) and the results were not affected (and there were no crashes). This is 
not surprising, because released open source code doesn't contain too many bugs 
and the message change only affects a specific subcase.

https://github.com/llvm/llvm-project/pull/74141
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-04 Thread Balazs Benics via cfe-commits

https://github.com/steakhal approved this pull request.

The patch makes sense to me.

https://github.com/llvm/llvm-project/pull/74141
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits


[clang] [analyzer] Let the checkers query upper and lower bounds on symbols (PR #74141)

2023-12-01 Thread via cfe-commits

llvmbot wrote:



@llvm/pr-subscribers-clang

@llvm/pr-subscribers-clang-static-analyzer-1

Author: None (DonatNagyE)


Changes

This commit extends the class `SValBuilder` with the methods `getMinValue()` 
and `getMaxValue()` to that work like `SValBuilder::getKnownValue()` but return 
the minimal/maximal possible value the `SVal` is not perfectly constrained.

This extension of the ConstraintManager API is discussed at: 
https://discourse.llvm.org/t/expose-the-inferred-range-information-in-warning-messages/75192

As a simple proof-of-concept application of this new API, this commit extends a 
message from `core.BitwiseShift` with some range information that reports the 
assumptions of the analyzer.

My main motivation for adding these methods is that I'll also want to use them 
in `ArrayBoundCheckerV2` to make the error messages less awkward, but I'm 
starting with this simpler and less important usecase because I want to avoid 
merge conflicts with my other commit 
https://github.com/llvm/llvm-project/pull/72107 which is currently under review.

The testcase `too_large_right_operand_compound()` shows a situation where 
querying the range information does not work (and the extra information is not 
added to the error message). This also affects the debug utility 
`clang_analyzer_value()`, so the problem isn't in the fresh code. I'll do some 
investigations to resolve this, but I think that this commit is a step forward 
even with this limitation.

---
Full diff: https://github.com/llvm/llvm-project/pull/74141.diff


6 Files Affected:

- (modified) 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h (+16) 
- (modified) 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h (+8) 
- (modified) clang/lib/StaticAnalyzer/Checkers/BitwiseShiftChecker.cpp (+11-5) 
- (modified) clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp (+22) 
- (modified) clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp (+50-6) 
- (modified) clang/test/Analysis/bitwise-shift-common.c (+11-3) 


``diff
diff --git 
a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h 
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index 4e94ad49a783360..4de04bc4d397ac4 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -110,6 +110,22 @@ class ConstraintManager {
 return nullptr;
   }
 
+  /// Attempt to return the minimal possible value for a given symbol. Note
+  /// that a ConstraintManager is not obligated to return a lower bound, it may
+  /// also return nullptr.
+  virtual const llvm::APSInt *getSymMinVal(ProgramStateRef state,
+   SymbolRef sym) const {
+return nullptr;
+  }
+
+  /// Attempt to return the minimal possible value for a given symbol. Note
+  /// that a ConstraintManager is not obligated to return a lower bound, it may
+  /// also return nullptr.
+  virtual const llvm::APSInt *getSymMaxVal(ProgramStateRef state,
+   SymbolRef sym) const {
+return nullptr;
+  }
+
   /// Scan all symbols referenced by the constraints. If the symbol is not
   /// alive, remove it.
   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
diff --git 
a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h 
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
index a64cf7ae4efcb82..d7cff49036cb810 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
@@ -110,6 +110,14 @@ class SValBuilder {
   /// that value is returned. Otherwise, returns NULL.
   virtual const llvm::APSInt *getKnownValue(ProgramStateRef state, SVal val) = 
0;
 
+  /// Tries to get the minimal possible (integer) value of a given SVal. If the
+  /// constraint manager cannot provide an useful answer, this returns NULL.
+  virtual const llvm::APSInt *getMinValue(ProgramStateRef state, SVal val) = 0;
+
+  /// Tries to get the maximal possible (integer) value of a given SVal. If the
+  /// constraint manager cannot provide an useful answer, this returns NULL.
+  virtual const llvm::APSInt *getMaxValue(ProgramStateRef state, SVal val) = 0;
+
   /// Simplify symbolic expressions within a given SVal. Return an SVal
   /// that represents the same value, but is hopefully easier to work with
   /// than the original SVal.
diff --git a/clang/lib/StaticAnalyzer/Checkers/BitwiseShiftChecker.cpp 
b/clang/lib/StaticAnalyzer/Checkers/BitwiseShiftChecker.cpp
index 8a933d124d7700d..d4aa9fa1339f47c 100644
--- a/clang/lib/StaticAnalyzer/Checkers/BitwiseShiftChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/BitwiseShiftChecker.cpp
@@ -172,18 +172,24 @@ BugReportPtr BitwiseShiftValidator::checkOvershift() {
 
   const SVal Right = Ctx.getSVal(operandExpr(Op