This is an archive of the discontinued LLVM Phabricator instance.

[analyzer][z3] Use more elaborate Z3 variable names
ClosedPublic

Authored by steakhal on Aug 19 2020, 9:15 AM.

Details

Summary

Previously, it was a tedious task to comprehend Z3 dumps.
We will use the same name prefix just as we use in the corresponding dump method.

For all SymbolData values:

  • $### -> conj_$###
  • $### -> derived_$###
  • $### -> extent_$###
  • $### -> meta_$###
  • $### -> reg_$###

Diff Detail

Event Timeline

steakhal created this revision.Aug 19 2020, 9:15 AM
steakhal requested review of this revision.Aug 19 2020, 9:15 AM
xazax.hun accepted this revision.Aug 19 2020, 10:24 AM

LGTM!

I wonder whether having a virtual method for symbols to get the prefix would be cleaner (something like getKindCStr), but I do not insist.

This revision is now accepted and ready to land.Aug 19 2020, 10:24 AM

I wonder whether having a virtual method for symbols to get the prefix would be cleaner (something like getKindCStr), but I do not insist.

Are you implying to have something like:

virtual SmallString<8> clang::ento::SymbolData::getKindStr() const;

BTW probably we could make use of this in the SymbolData dump method family.

Or do you want to lift this function to the SymExpr class?

Exactly, but you could return a StringRef to static storage.

I am fine with both approach. Whichever you find cleaner.

Exactly, but you could return a StringRef to static storage.

I am fine with both approach. Whichever you find cleaner.

Eh, I'm not sure if it worth it to put these into virtual functions - as conditionally overriding functions is not really a good idea.
So we would not win much.

I still think that this way is the cleanest AFAIK.

Eh, I'm not sure if it worth it to put these into virtual functions - as conditionally overriding functions is not really a good idea.

I am not sure I follow. What do you mean by conditionally overriding? What is the condition?

Eh, I'm not sure if it worth it to put these into virtual functions - as conditionally overriding functions is not really a good idea.

I am not sure I follow. What do you mean by conditionally overriding? What is the condition?

I wanted to conditionally, aka. in debug configuration override the base implementation of the SymbolData::getKindStr to print return the specific kind string. In any other configuration I wanted to indef out the overriding functions to let the SymbolData implementation to be triggered.
In that way less macro expansion would have been necessary, resulting in cleaner code.

Unfortunately I would have needed even more macros to make the subtype override function declarations disappear.

This was the reason that I suggested to leave the current implementation as-is.

I wanted to conditionally, aka. in debug configuration override the base implementation of the SymbolData::getKindStr

I see. Yeah, that does not make much sense. I was thinking about always overriding the methods but call them conditionally.

steakhal updated this revision to Diff 287192.Aug 22 2020, 8:14 AM
steakhal edited the summary of this revision. (Show Details)

Use virtual getKindStr method for acquiring the kind name.

xazax.hun accepted this revision.Aug 22 2020, 8:43 AM

This is what I had in mind, thanks!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
335

Maybe, in this case, it is cleaner to duplicate the line rather than introduce PRETTY_SYMBOL_KIND?

xazax.hun added inline comments.Aug 22 2020, 8:44 AM
clang/test/Analysis/z3/pretty-dump.c
16

Will this test case work with non-debug builds?

I don't mind having it for release builds as well, why are you applying it only for debug builds?

steakhal updated this revision to Diff 287197.Aug 22 2020, 9:43 AM
steakhal marked 2 inline comments as done.
steakhal edited the summary of this revision. (Show Details)

I don't mind having it for release builds as well, why are you applying it only for debug builds?

It might introduce a slight overhead since Z3 will parse longer the symbol names.


Diff update:

  • Simplify macro usage.
  • Introduce the llvm_enable_dump lit test requires clause.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
335

Thanks.

clang/test/Analysis/z3/pretty-dump.c
16

Fixed.

mikhail.ramalho requested changes to this revision.Aug 23 2020, 3:24 PM

I don't mind having it for release builds as well, why are you applying it only for debug builds?

It might introduce a slight overhead since Z3 will parse longer the symbol names.

That overhead should be negligible, in the worst case you are adding just a few extra characters to the variable's name.

I rather have it for release builds as well so we don't introduce different outputs depending on the build options, and we can improve debugging for release builds as well.

Also as a bonus, we don't have to change the test scripts for a single test.

This revision now requires changes to proceed.Aug 23 2020, 3:24 PM
steakhal updated this revision to Diff 287303.Aug 24 2020, 12:44 AM
steakhal retitled this revision from [analyzer][z3] Use more elaborate z3 variable names in debug build to [analyzer][z3] Use more elaborate Z3 variable names.
steakhal edited the summary of this revision. (Show Details)

I don't mind having it for release builds as well, why are you applying it only for debug builds?

It might introduce a slight overhead since Z3 will parse longer the symbol names.

That overhead should be negligible, in the worst case you are adding just a few extra characters to the variable's name.

I rather have it for release builds as well so we don't introduce different outputs depending on the build options, and we can improve debugging for release builds as well.

Also as a bonus, we don't have to change the test scripts for a single test.

Fixed.


Revision updated:

  • Use the prettier symbol names unconditionally
  • Revert changes to the test infra
This revision is now accepted and ready to land.Aug 24 2020, 10:47 AM
This revision was landed with ongoing or failed builds.Sep 13 2020, 11:44 PM
This revision was automatically updated to reflect the committed changes.