Clang Static Analyzer has issues with handling floating-point numbers

[tianxinghe]

version: clang17.0.1

It seems that CSA has problems handling floating-point operations. https://godbolt.org/z/37T31jzY3

#include <stdio.h>
int llvm_fcmp_one(double X, double Y) { 
  int res = (X != Y && X == X && Y == Y);
  return res; 
}

int main(int argc, char ** argv) {
  int *llvm_cbe_a46 = ((int *)/*NULL*/0);
  if (llvm_fcmp_one(744753600, 41) != 0) {
    printf("%d\n", *llvm_cbe_a46);
  }
  return 1;
}

When the formal parameter is of type int, the checker can correctly find the bug. https://godbolt.org/z/xx769hYjo

#include <stdio.h>
int llvm_fcmp_one(int X, int Y) { 
  int res = (X != Y && X == X && Y == Y);
  return res; 
}

int main(int argc, char ** argv) {
  int *llvm_cbe_a46 = ((int *)/*NULL*/0);
  if (llvm_fcmp_one(744753600, 41) != 0) {
    printf("%d\n", *llvm_cbe_a46);
  }
  return 1;
}

[llvmbot]

@llvm/issue-subscribers-clang-static-analyzer

Author: Tianxing He (tianxinghe)

version: clang17.0.1 It seems that CSA has problems handling floating-point operations. https://godbolt.org/z/37T31jzY3 #include <stdio.h> int llvm_fcmp_one(double X, double Y) { int res = (X != Y && X == X && Y == Y); return res; } int main(int argc, char ** argv) { int *llvm_cbe_a46 = ((int *)/*NULL*/0); if (llvm_fcmp_one(744753600, 41) != 0) { printf("%d\n", *llvm_cbe_a46); } return 1; } When the formal parameter is of type int, the checker can correctly find the bug. https://godbolt.org/z/xx769hYjo #include <stdio.h> int llvm_fcmp_one(int X, int Y) { int res = (X != Y && X == X && Y == Y); return res; } int main(int argc, char ** argv) { int *llvm_cbe_a46 = ((int *)/*NULL*/0); if (llvm_fcmp_one(744753600, 41) != 0) { printf("%d\n", *llvm_cbe_a46); } return 1; }

[EugeneZelenko]

Same problem in main: https://godbolt.org/z/KKnzjK77s

[steakhal]

In CSA we don't model floating-point arithmetic. We only ever focused on the integral domain. I don't think we will support floating-point stuff in the next 5 years at least given the priorities.

[a-price]

Out of curiosity, is there a write-up on what would be required to model floating-point operations? It's a little confusing when you call clang_tidy -checks=-*,clang-analyzer-core.DivideZero on

double DivZero(double v) { return v / 0.0; }

and it seems perfectly happy.

Conditionals seem to work OK for doubles - some simple code like

double testSafeInv(double x) {
  if (x == 0.0) {
    return 0.0;
  }
  return 1.0 / x;
}

gives a CFG like:

double testSafeInv(double x)
 [B4 (ENTRY)]
   Succs (1): B3

 [B1]
   1: 1.
   2: x
   3: [B1.2] (ImplicitCastExpr, LValueToRValue, double)
   4: [B1.1] / [B1.3]
   5: return [B1.4];
   Preds (1): B3
   Succs (1): B0

 [B2]
   1: 0.
   2: return [B2.1];
   Preds (1): B3
   Succs (1): B0

 [B3]
   1: x
   2: [B3.1] (ImplicitCastExpr, LValueToRValue, double)
   3: 0.
   4: [B3.2] == [B3.3]
   T: if [B3.4]
   Preds (1): B4
   Succs (2): B2 B1

 [B0 (EXIT)]
   Preds (2): B1 B2

[tianxinghe]

For all I know, Clang Static Analyzer hasn't modeled floating-point operations yet. It doesn't record the range of a floating-point variable on a certain path (with a symbolic value), but replaces it with an UNKNOWN VALUE.

So the tool may crookedly detect a bug on a certain branch (such as the true branch), but if the bug appears on another branch, the tool's performance may deviate. When unknown values are used as conditions for conditional jump statements, false positives and negatives are more common.

I don't know which papers are related to modeling floating-point operations at the moment, but I think it is very interesting.

Apologies for my poor English expression and wish you a good day.

---Original--- From: "Andrew @.> Date: Sun, Jun 23, 2024 07:31 AM To: @.>; Cc: "Tianxing @.**@.>; Subject: Re: [llvm/llvm-project] Clang Static Analyzer has issues withhandling floating-point numbers (Issue #82910)

Out of curiosity, is there a write-up on what would be required to model floating-point operations? It's a little confusing when you call clang_tidy -checks=-*,clang-analyzer-core.DivideZero on double DivZero(double v) { return v / 0.0; }

and it seems perfectly happy.

Conditionals seem to work OK for doubles - some simple code like double testSafeInv(double x) { if (x == 0.0) { return 0.0; } return 1.0 / x; }

gives a CFG like: double testSafeInv(double x) [B4 (ENTRY)] Succs (1): B3 [B1] 1: 1. 2: x 3: [B1.2] (ImplicitCastExpr, LValueToRValue, double) 4: [B1.1] / [B1.3] 5: return [B1.4]; Preds (1): B3 Succs (1): B0 [B2] 1: 0. 2: return [B2.1]; Preds (1): B3 Succs (1): B0 [B3] 1: x 2: [B3.1] (ImplicitCastExpr, LValueToRValue, double) 3: 0. 4: [B3.2] == [B3.3] T: if [B3.4] Preds (1): B4 Succs (2): B2 B1 [B0 (EXIT)] Preds (2): B1 B2
— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you authored the thread.Message ID: @.***>

[haoNoQ]

Yeah the CFG is perfectly fine, we just don't have a way to describe floating-point "values" (as opposed to variables or expressions).

It shouldn't be too hard to properly simulate "concrete values" of floating-point types. Just wrap an llvm::APFloat in an SVal subclass just like nonloc::ConcreteInt wraps an llvm::APSInt, and then teach SValBuilder to forward all operations on them to respective llvm::APFloat methods just like it already handles nonloc::ConcreteInt.

Unknown (symbolic) floating-point values are harder, the constraint solver will probably need quite a bit of rework to represent possible ranges of values, and solve constraints over floating-point symbolic expressions. You'll also run into edge cases with NaN and such.

[Snape3058]

We used to do some research on modeling floating point numbers around 2016 ^2016. Modeling floating numbers (in CSA) is not as simple as modeling integers, as floating point numbers have a very different and more complex way of representing a value (with a significand and an exponent). It would be very imprecise to simply represent a floating-point number with an interval. But, if you just want to implement some checks of division by zero of floating point numbers, I think you can just model some specific literals just like our approach published in 2016 ^2016. The approach is implemented on a private fork of CSA, but it also works on CSA, it works similarly as CSA.

[tianxinghe]

Out of curiosity, is there a write-up on what would be required to model floating-point operations? It's a little confusing when you call clang_tidy -checks=-*,clang-analyzer-core.DivideZero on

double DivZero(double v) { return v / 0.0; }

and it seems perfectly happy.

Conditionals seem to work OK for doubles - some simple code like

double testSafeInv(double x) {
  if (x == 0.0) {
    return 0.0;
  }
  return 1.0 / x;
}

gives a CFG like:

double testSafeInv(double x)
 [B4 (ENTRY)]
   Succs (1): B3

 [B1]
   1: 1.
   2: x
   3: [B1.2] (ImplicitCastExpr, LValueToRValue, double)
   4: [B1.1] / [B1.3]
   5: return [B1.4];
   Preds (1): B3
   Succs (1): B0

 [B2]
   1: 0.
   2: return [B2.1];
   Preds (1): B3
   Succs (1): B0

 [B3]
   1: x
   2: [B3.1] (ImplicitCastExpr, LValueToRValue, double)
   3: 0.
   4: [B3.2] == [B3.3]
   T: if [B3.4]
   Preds (1): B4
   Succs (2): B2 B1

 [B0 (EXIT)]
   Preds (2): B1 B2

The Clang Static Analyzer is almost prefect at what it claims to detect (almost no false positives or negatives), and there are many developers working on it. But no tool can find all the "bugs" or model all the scenarios. For someone like me who is trying to find bugs, this is a bit difficult. hahah

[a-price]

It would be very imprecise to simply represent a floating-point number with an interval.

@Snape3058, would you mind elaborating on that a little more? I would have assumed that you could partition the space of a double variable using intervals pretty effectively. (I'd assume that you could "flatten" conjunctions like x < 5 && x > 1 to a partition mapping the full range to {feasible, infeasible[, unknown]}?)

(I only read the abstracts for the papers you linked; maybe there was more discussion in the body.)

[Snape3058]

It would be very imprecise to simply represent a floating-point number with an interval.

@Snape3058, would you mind elaborating on that a little more? I would have assumed that you could partition the space of a double variable using intervals pretty effectively. (I'd assume that you could "flatten" conjunctions like x < 5 && x > 1 to a partition mapping the full range to {feasible, infeasible[, unknown]}?)

(I only read the abstracts for the papers you linked; maybe there was more discussion in the body.)

@haoNoQ @steakhal What do you think? Do you think we would need this feature in CSA? If not, I do not pretty want to add it, as I was not originally involved in the two works I listed above, and this feature may introduce instability and more overhead to the engine. According to our experiments in these two papers, if we precisely model floating point numbers with our approach, the overhead will unignorablely increase.

Although the requirement listed above is simple, if we consider all possibilities in the domain of floating point numbers, the model cannot be as simple as integers.

[NagyDonat]

IMHO the main reason for not modeling floating-point numbers is that they are simply rare in those simple algorithms that can be handled by the Analyzer.

It is easy to construct elementary testcases where the Analyzer could track a stand-alone double value and report something useful, but I suspect that most real-world usage of floating-point values would involve lots of data (arrays, matrices, loops) and non-trivial numerical algorithms. In these situations the "brute force" symbolical execution of the Analyzer is practically useless, and there will be an unmanageable amount of false positive due to the heuristics that are needed to "truncate" the loops.

I'd say that the analyzer is mostly suitable for following logic that involves a few discrete states (file opened/closed, pointer null/non-null etc.) and if-then-else branches. Even integer handling can be difficult for the Analyzer: for example we have an alpha checker (alpha.security.ArrayBoundV2) that could report array indexing out-of-bounds errors, and its implementation is practically complete, but it still produces too many false positives, because the loop modeling "feeds" it with incorrect assumptions.

[a-price]

Thanks, that makes a lot of sense. The actual case I was looking at was in some CUDA code, roughly like

double Fn(double a, double b, double c) {
  return (c - a) / (b - a);
}

but complicated enough that the issue wasn't blindingly obvious.

My understanding is that the Analyzer works forward through the program, rather than starting from a potential flaw and working backwards to see if its preimage collapses to nothing, or if it escapes outside of the translation unit. Working forward seems pretty difficult for larger programs, but maybe there is some value in a very pedantic warning emitted when looking at just this function.

I could imagine this type of float analysis becoming much more feasible when (if?) we get Contracts. Pre/Postconditions could provide a natural decomposition that could be verified tractably.

double Fn(double a, double b, double c)
  pre (b > a) {

[Snape3058]

I agree with NagyDonat.

double Fn(double a, double b, double c) pre (b > a);

I used to add such pre-/post-conditions to the engine in a private fork. However, it does not work as you assumed.

Currently, the range-based solver cannot correctly handle such a path constraint with multiple variables. Hence, the engine cannot determine whether b - a can be zero directly without enabling the Z3 solver for all constraint solvings. And the check will simply add another constraint of b != a to the constraint manager. As a result, the code listed above can never be reported, unless the caller arguments the function with the same value for both a and b.

The pre-/post-conditions can only be used to add simple constraints. However, we cannot expect developers will write so, or even provide the engine with a pre-/post-condition.

My understanding is that the Analyzer works forward through the program...

Yes. We use static symbolic execution to model the behavior of each program path that is assumed to be feasible with collected path constraints that the range-based checker can determine. And the engine will report a bug only if there is no chance that it cannot happen, where a potential bug will not be reported, such as the one in your code.