This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Symbolicate float values with integral casting
AbandonedPublic

Authored by ASDenysPetrov on Feb 1 2021, 10:07 AM.

Details

Summary

Create nonloc::SymbolVal with SymbolCast expression from integral type to float type.

Diff Detail

Event Timeline

ASDenysPetrov created this revision.Feb 1 2021, 10:07 AM
ASDenysPetrov requested review of this revision.Feb 1 2021, 10:07 AM

Hi, folk! Please, review this tiny patch.

Updated. Moved comments as well.

void clang_analyzer_dumpi(int);
void clang_analyzer_dumpf(float);
void clang_analyzer_dumpip(int*);
void clang_analyzer_dumpfp(float*);

void SymbolCast_of_float_type_aux(int *p) {
  *p += 1;
  clang_analyzer_dumpi(*p); // (Previously): Unknown  ->  (Now): (float) (conj_$1{int, LC2, S790, #1})
  clang_analyzer_dumpf(*p); // (Previously): Unknown  ->  (Now): (float) (conj_$1{int, LC2, S790, #1})
  clang_analyzer_dumpip(p); // &Element{x1,1 S64b,float}
  clang_analyzer_dumpfp(p); // &Element{x1,1 S64b,float}
}

void SymbolCast_of_float_type() {
  extern float x1;
  extern double x2;
  extern long double x3;

  void (*f)() = SymbolCast_of_float_type_aux;

  clang_analyzer_dumpi(*(&x1 + 1));  // Unknown
  clang_analyzer_dumpf(*(&x1 + 1));  // Unknown
  clang_analyzer_dumpip(&x1 + 1);    // &Element{x1,1 S64b,int}
  clang_analyzer_dumpfp(&x1 + 1);    // &Element{x1,1 S64b,float}

  f(&x1 + 1);
  // f(&x2 + 1);
  // f(&x3 + 1);
}

Only lines 8-9 have changed. But IMO, in a bad way.
We should have just (conj_$1{float, LC2, S790, #1}) there, because the object you read from that location is of type float.
Reading an int and casting it to float means a different thing.

Before the patch - saying Unknown, it was not accurate, but at least correct.

This is just a note for me to correctly rebase it in the future:
https://reviews.llvm.org/D96090?vs=321602&id=322422#toc

NoQ added a comment.Mar 3 2021, 5:54 PM

tiny patch

IIUC this is roughly the first time ever when SValBuilder starts emitting symbols of float type. This is a huge change with an almost unlimited scope of unexpected side effects and very rigorous testing is required to understand the actual effect of this patch on programs that use floats. I think that generally some symbols are always better than no symbols, even if the constraint manager is completely unable to handle them. But we have to make sure that the entirety of SValBuilder and the entirety of RegionStore (and possibly the entirety of ExprEngine) are ready to deal with completely new kinds of values that they've never seen before.

clang/test/Analysis/svalbuilder-float-cast.c
11

You silently ignored and removed this comment. The author of the original code was pretty certain that your solution is incorrect and most likely added this comment there specifically to make sure your solution doesn't get implemented.

If you see potential problems with your patch, please don't try to sweep them under the rug. If you're sure your solution is correct, please explain why. If not, please ask about it in the summary or in the comments.

Generally, every commit should be obvious. If there are obvious questions that remain unanswered then the commit is not obvious and needs improvement.

ASDenysPetrov added a comment.EditedMar 9 2021, 1:23 AM

@NoQ wrote:

IIUC this is roughly the first time ever when SValBuilder starts emitting symbols of float type. This is a huge change with an almost unlimited scope of unexpected side effects and very rigorous testing is required to understand the actual effect of this patch on programs that use floats. I think that generally some symbols are always better than no symbols, even if the constraint manager is completely unable to handle them. But we have to make sure that the entirety of SValBuilder and the entirety of RegionStore (and possibly the entirety of ExprEngine) are ready to deal with completely new kinds of values that they've never seen before.

I kind of abandoned this patch. I realized that too much circumstances appeared that I am not an expert in. It is more like an experimental patch which serves to make clear some information, raise a discussion of what another people know about handling floats. Thank you for your sharing. Now I see what potential problems could be. I'm going to proceed as soon as I feel more confident answering these questions.

clang/test/Analysis/svalbuilder-float-cast.c
11

Very good objection! Sorry, honestly I somehow missed that it should NOT. Of course we should have strong arguments introducing the opposite effect. This is my mistake.

ASDenysPetrov abandoned this revision.Mar 22 2021, 7:43 AM