================
@@ -50,6 +101,44 @@ class BuiltinFunctionChecker : public Checker<eval::Call> {
 
 } // namespace
 
+void BuiltinFunctionChecker::HandleOverflowBuiltin(const CallEvent &Call,
+                                                   CheckerContext &C,
+                                                   BinaryOperator::Opcode Op,
+                                                   QualType ResultType) const {
+  // All __builtin_*_overflow functions take 3 argumets.
+  assert(Call.getNumArgs() == 3);
+
+  ProgramStateRef State = C.getState();
+  SValBuilder &SVB = C.getSValBuilder();
+  const Expr *CE = Call.getOriginExpr();
+
+  SVal Arg1 = Call.getArgSVal(0);
+  SVal Arg2 = Call.getArgSVal(1);
+
+  SVal RetVal = SVB.evalBinOp(State, Op, Arg1, Arg2, ResultType);
+
+  // TODO: Handle overflows with values that known to overflow. Like INT_MAX + 
1
+  // should not produce state for non-overflow case and threat it as
----------------
NagyDonat wrote:

I did some digging in `RangedConstraintManager` and it seems that algebraic 
expressions that involve two symbolic values **are handled as black boxes** by 
the analyzer: in your example it creates a `SymSymExpr` that is known to be the 
sum of `a` and `b`, but we don't have any logic which would constrain the 
potential values of this `SymSymExpr` based on the constraints known about the 
operands. (The analyzer can propagate information in the easier case when it 
knows the exact value of one of the operands.)

I don't know why do we have this shameful limitation... I'd guess that 
implementing the necessary `RangeSet` operation wouldn't be prohibitively 
difficult, but there may be performance implications, and perhaps 
well-constrained (but not exactly known) values are not common enough to make 
this a valuable investment.

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

Reply via email to