This is an archive of the discontinued LLVM Phabricator instance.

[analyzer] Generalised the SMT state constraints
ClosedPublic

Authored by mikhail.ramalho on Nov 27 2018, 2:26 PM.

Details

Summary

This patch moves the ConstraintSMT definition to the SMTConstraintManager header to make it easier to move the Z3 backend around.

We achieve this by not using shared_ptr anymore, as llvm::ImmutableSet doesn't seem to like it.

The solver specific exprs and sorts are cached in the Z3Solver object now and we move pointers to those objects around.

As a nice side-effect, SMTConstraintManager doesn't have to be a template anymore. Yay!

Diff Detail

Repository
rL LLVM

Event Timeline

TBH this seems overly complicated. Z3 already hash-conses all objects; I don't think there is benefit of doing it again on the LLVM side.

What is the benefit from this patch, apart from being able to use ImmutableSet?

TBH this seems overly complicated. Z3 already hash-conses all objects; I don't think there is benefit of doing it again on the LLVM side.

What is the benefit from this patch, apart from being able to use ImmutableSet?

The cache is only used to hold the exprs and sorts in the Solver class.

The idea here is to make it similar to the SymbolManager class in the CSA and store all the exprs and sorts in the solver specific class, so we don't have to manage their lifetime.

NoQ added inline comments.Nov 30 2018, 5:19 PM
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
21–24 ↗(On Diff #175580)

Why is this a path-sensitive data?

Wouldn't we always automatically map the same symbol to the same SMT expression? If we would, then this should be a global. If we wouldn't, then the path-sensitive trait is already useless, because the SMT expression would probably change between nodes on the same path as well.

mikhail.ramalho marked an inline comment as done.Dec 10 2018, 11:59 AM
mikhail.ramalho added inline comments.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
21–24 ↗(On Diff #175580)

By "this should be global" do you mean moving it to RangedConstraintManager.h along with ConstraintRangeTy?

The only reason I didn't do it was because I was trying to keep everything SMT-related together.

NoQ accepted this revision.Dec 14 2018, 3:03 PM
NoQ added inline comments.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
21–24 ↗(On Diff #175580)

Wait, i guess i misunderstood. Yes, this should be state-specific, never mind.

314–317 ↗(On Diff #175580)

Mmm, would this sometimes cause non-deterministic collisions? I think that NewState->get<ConstraintSMT>().getRootWithoutRetain() should be used as hash directly, as it does actually uniquely identify the set. ID also uniquely identifies the set (being the same thing), but ID.ComputeHash() doesn't (being a shorter integer).

This revision is now accepted and ready to land.Dec 14 2018, 3:03 PM
mikhail.ramalho marked an inline comment as done.Dec 17 2018, 7:57 AM
mikhail.ramalho added inline comments.
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
314–317 ↗(On Diff #175580)

Oh, I didn't know that! I'll update it.

This revision was automatically updated to reflect the committed changes.
Herald added a project: Restricted Project. · View Herald TranscriptFeb 6 2019, 7:18 PM
michaelplatings added inline comments.
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
22

This does not compile with Visual Studio 2015:

1>  SMTConstraintManager.cpp
1>StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23): error C2872: 'ConstraintSMTTy': ambiguous symbol
1>  StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(22): note: could be 'llvm::ImmutableSet<std::pair<clang::ento::SymbolRef,const llvm::SMTExpr *>,llvm::ImutContainerInfo<ValT>> ConstraintSMTTy'
1>    with
1>    [
1>        ValT=std::pair<clang::ento::SymbolRef,const llvm::SMTExpr *>
1>    ]
1>  StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23): note: or       '`anonymous-namespace'::ConstraintSMTTy'

It could be fixed by changing ConstraintSMTTy to e.g. ConstraintSMTType

carwil added a subscriber: carwil.Feb 8 2019, 7:10 AM

@michaelplatings, thanks for the report.

That's weird, did you try to run the tests? You can do it with ninja check-clang-analyzer-z3

@michaelplatings, thanks for the report.

That's weird, did you try to run the tests? You can do it with ninja check-clang-analyzer-z3

If you look at the lines referenced by the error you may find it less weird - the patch adds a typedef that has the same name as a using statement added by the REGISTER_TRAIT_WITH_PROGRAMSTATE macro.

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

dyung added a subscriber: dyung.Feb 11 2019, 4:24 PM

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

I can give it a try. But just to be clear, the fix is to change ConstraintSMTTy on line 22 to ConstraintSMTType? Would line 23 require a similar change, or is it fine as it currently is?

dyung added a comment.Feb 11 2019, 4:50 PM

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

I can give it a try. But just to be clear, the fix is to change ConstraintSMTTy on line 22 to ConstraintSMTType? Would line 23 require a similar change, or is it fine as it currently is?

I can answer my own question, both seem to need updating. I am building/testing now.

dyung added a comment.Feb 11 2019, 5:22 PM

To be clear, this patch breaks compilation with Visual Studio 2015. Running tests requires that the code can be built, so no I didn't run the tests.

Maybe I didn't express myself very clearly: if you change it to ConstraintSMTType, do the tests pass?

If so, I don't see why not pushing the fix. Unfortunately, I don't have Windows to test it.

I can give it a try. But just to be clear, the fix is to change ConstraintSMTTy on line 22 to ConstraintSMTType? Would line 23 require a similar change, or is it fine as it currently is?

I can answer my own question, both seem to need updating. I am building/testing now.

Build and test passed for me with Visual Studio 2015 and on Linux. Should I submit the fix?

dyung added a comment.Feb 11 2019, 6:18 PM

Build and test passed for me with Visual Studio 2015 and on Linux. Should I submit the fix?

I committed the change in r353791. Hopefully this fixes the problem.