Page MenuHomePhabricator

xazax.hun (Gábor Horváth)
User

Projects

User does not belong to any projects.

User Details

User Since
Sep 17 2012, 3:16 AM (331 w, 2 h)

Recent Activity

Today

xazax.hun added a comment to D35068: [analyzer] Detect usages of unsafe I/O functions.

To add an analogy, Clang Tidy will not require C++ Core Guidelines related checks to be evaluated on projects that are not following the guidelines as the results are meaningless for those projects.

Mon, Jan 21, 1:07 AM
xazax.hun added a comment to D35068: [analyzer] Detect usages of unsafe I/O functions.

I've evaluated this checker on LLVM+Clang, there were only a few (about 15) warnings, because of the C11 flag check at the beginning of the checker body. However, if this check was removed, number of the warnings would be increased significantly. I wouldn't say the findings were real security issues, most of the warnings were about usages of deprecated functions, which has not been considered unsecure (but which may cause problems if the code is modified in an improper way in the future).

My problem is that LLVM+Clang isn't really a C (nor a C11) project, and I think judging this checker on it is a little misleading. Could you please test it on some C11 projects? I think tmux uses C11.

Edit: it doesn't, but CMake is mostly a C project and it does!

Mon, Jan 21, 1:05 AM

Thu, Jan 17

xazax.hun accepted D35068: [analyzer] Detect usages of unsafe I/O functions.

Any objections to commit this?
I think this is quiet coding guideline specific check which is useful for a set of security critical projects. As this is an opt in kind of check, I think it does no harm to have it upstream.

Thu, Jan 17, 3:10 AM

Wed, Jan 16

xazax.hun accepted D56632: [analyzer] Track region liveness only through base regions..

Thanks, LGTM! It is interesting to see if we need to traverse all the super regions in scanReachableSymbols, but if we need to change something there, I would prefer that to be in a separate patch.
If visiting the whole super region chain proved to be redundant I would recommend removing it for clarity regardless of having a performance impact.

Wed, Jan 16, 3:59 AM

Mon, Jan 14

xazax.hun added a comment to D56632: [analyzer] Track region liveness only through base regions..

I really like all this detective work and it would be sad to have it forgotten. I would love to see some of your comments in the documentation of symbol reaper.
More specifically:

Mon, Jan 14, 8:34 AM

Tue, Jan 8

xazax.hun accepted D56441: [analyzer][CrossTU][NFC] Generalize to external definitions instead of external functions.

Some nits inline. Otherwise looks good to me.

Tue, Jan 8, 7:15 AM

Dec 18 2018

xazax.hun added a comment to D55804: [analyzer] C++17: Fix leak false positives when an object with destructor is returned from the top frame..

Is there any downsides for using symbolic region for the construction target? For me that would make perfect sense, since this is often modelled by passing the address of the target into the callee. The programmer could do RVO like thing by hand, so modeling automatic and manual RVO the same way would be the least surprising in my opinion.

Dec 18 2018, 12:46 AM

Dec 14 2018

xazax.hun added a comment to D46421: [analyzer][CrossTU] Extend CTU to VarDecls with initializer.

Sorry for the delay. The changes are looking good to me, although I think it might be worth to split this up into two patch, one NFC with the renaming, and one that actually introduces the changes.

Dec 14 2018, 5:31 AM
xazax.hun created D55697: [analyzer] Assume that we always have a SubEngine available.
Dec 14 2018, 2:02 AM · Restricted Project

Dec 7 2018

xazax.hun accepted D55131: [CTU] Add more lit tests and better error handling.

LG!

Dec 7 2018, 7:38 AM
xazax.hun accepted D55134: [CTU] Add triple/lang mismatch handling.

LG!

Dec 7 2018, 7:27 AM
xazax.hun accepted D55135: [CTU][Analyzer]Add DisplayCTUProgress analyzer switch.

While Static Analyzer is the only client of CTU library at the moment, we might have more in the future. I would not use the phrase ANALYZE in the log message. Once this is resolved the rest looks good.

Dec 7 2018, 5:13 AM

Dec 6 2018

xazax.hun added a comment to D55388: [analyzer] MoveChecker Pt.8: Add checks for dereferencing a smart pointer after move..

Hm. I wonder if it would also make sense to model e.g. the get method to return nullptr for moved from smart ptrs. This could help null dereference checker and also aid false path prunning.

Dec 6 2018, 10:55 PM

Dec 5 2018

xazax.hun accepted D55280: [CTU] Make loadExternalAST return with non nullptr on success.

LG!

Dec 5 2018, 2:49 AM

Dec 4 2018

xazax.hun added inline comments to D55134: [CTU] Add triple/lang mismatch handling.
Dec 4 2018, 10:34 AM
xazax.hun added a comment to D55135: [CTU][Analyzer]Add DisplayCTUProgress analyzer switch.

Having an analyzer config option makes sense.

Dec 4 2018, 7:07 AM
xazax.hun requested changes to D55134: [CTU] Add triple/lang mismatch handling.
Dec 4 2018, 7:06 AM
xazax.hun accepted D55133: [CTU] Add statistics.

The code LGTM! I am not good at wordsmithing, but if the descriptions of the statistics are not clear enough, I agree that they should be rephrased.

Dec 4 2018, 7:00 AM
xazax.hun accepted D55132: [CTU] Add asserts to protect invariants.
Dec 4 2018, 5:56 AM
xazax.hun accepted D55129: [CTU] Eliminate race condition in CTU lit tests.

After the review comment is resolved, the rest LGTM!

Dec 4 2018, 5:53 AM

Dec 3 2018

xazax.hun updated the diff for D52984: [analyzer] Checker reviewer's checklist.
  • Addressed further comments.
Dec 3 2018, 7:29 AM · Restricted Project

Nov 27 2018

xazax.hun accepted D53280: [analyzer] Emit an error for invalid -analyzer-config inputs.

Overall looks good to me, some minor comments inline.

Nov 27 2018, 8:51 AM

Nov 23 2018

xazax.hun accepted D52795: [analyzer][PlistMacroExpansion] Part 3.: Macro arguments are expanded.

Some minor comment inline. Otherwise looks good.

Nov 23 2018, 5:42 AM

Nov 17 2018

xazax.hun added a comment to D54557: [analyzer] MoveChecker Pt.2: Restrict the warning to STL objects and locals..
In D54557#1300654, @NoQ wrote:

It would be great to have a way to extend the list of (possibly non-stl) types to check. But I do understand that the analyzer does not have a great way to set such configuration options right now.

Do you envision room for another attribute here? I.e., a class attribute that says "this object is always unsafe to use after move, unless a method annotated with reinitializes is called"?

Nov 17 2018, 2:31 AM

Nov 15 2018

xazax.hun accepted D54557: [analyzer] MoveChecker Pt.2: Restrict the warning to STL objects and locals..

It would be great to have a way to extend the list of (possibly non-stl) types to check. But I do understand that the analyzer does not have a great way to set such configuration options right now.

Nov 15 2018, 4:50 AM
xazax.hun accepted D54556: [analyzer] MoveChecker Pt.1: Give MisusedMovedObject checker a more consistent name..

Looks good. Do we plan to detect problems other than use after move? Maybe it would be worth to synchronize with the tidy checker name use-after-move or is it going to cause more confusion?

Nov 15 2018, 4:45 AM

Nov 12 2018

xazax.hun added a comment to D54429: [analyzer] Creating standard Sphinx documentation.

I do like the idea of moving the Clang Static Analyzer documentation to where the rest of the tools are documented. I believe the original reason the analyzer had a separate homepage is due to it was off by default in clang at the beginning and users downloaded it from the separate page.

Nov 12 2018, 8:41 AM · Restricted Project
xazax.hun updated the diff for D52984: [analyzer] Checker reviewer's checklist.
  • Use the term checker instead of check.
Nov 12 2018, 4:57 AM · Restricted Project

Nov 10 2018

xazax.hun added inline comments to D52984: [analyzer] Checker reviewer's checklist.
Nov 10 2018, 7:14 AM · Restricted Project
xazax.hun updated the diff for D52984: [analyzer] Checker reviewer's checklist.
  • Move the checklist up before additional info in the HTML file.
  • Fix minor nits.
  • Add missing bullet points (thanks @Szelethus for noticing)
Nov 10 2018, 7:11 AM · Restricted Project
xazax.hun added inline comments to D52984: [analyzer] Checker reviewer's checklist.
Nov 10 2018, 6:52 AM · Restricted Project

Nov 6 2018

xazax.hun added a comment to D52795: [analyzer][PlistMacroExpansion] Part 3.: Macro arguments are expanded.

I would love to see a test with deeper macro in macro expansion and larger number of arguments, with some of the arguments unused. Some minor nits inline, otherwise looks good.

Nov 6 2018, 1:30 AM

Nov 2 2018

xazax.hun updated the diff for D52984: [analyzer] Checker reviewer's checklist.

This new version based on the bullets by NoQ. I also included some additional ones from other lists and added some new ones, e.g. the NamedDecl::getName will fail if the name of the decl is not a single token. I also reordered a bit. Advice that is more advanced and guidelines that are less likely to be violated should be closer to the bottom of the list.

Nov 2 2018, 7:31 AM · Restricted Project
xazax.hun accepted D53995: [analyzer] Drastically simplify the tblgen files used for checkers.

LGTM, but let's wait for @NoQ before committing.

Nov 2 2018, 5:09 AM
xazax.hun added a comment to D52790: [analyzer][PlistMacroExpansion] New flag to convert macro expansions to events.

I also would like to see in a tool how this would look like as an event before committing :) Just a sanity check to make sure this feature makes sense. Could you post a screenshot of CodeChecker or any other tool using this feature?

Nov 2 2018, 5:04 AM
xazax.hun accepted D52986: [analyzer][PlistMacroExpansion] Part 4.: Support for __VA_ARGS__.

One question otherwise looks good.

Nov 2 2018, 5:03 AM
xazax.hun accepted D52988: [analyzer][PlistMacroExpansion] Part 5.: Support for # and ##.
Nov 2 2018, 4:58 AM
xazax.hun added inline comments to D52795: [analyzer][PlistMacroExpansion] Part 3.: Macro arguments are expanded.
Nov 2 2018, 4:56 AM
xazax.hun accepted D52794: [analyzer][PlistMacroExpansion] Part 2.: Retrieving the macro name and primitive expansion.

One question and one nit otherwise looks good. Feel free to commit once those are resolved without another round of reviews.

Nov 2 2018, 4:49 AM
xazax.hun added inline comments to D53692: [analyzer] Evaluate all non-checker config options before analysis.
Nov 2 2018, 4:34 AM

Nov 1 2018

xazax.hun updated the diff for D53979: [analyzer][CTU] Correctly signal in the function index generation tool if there was an error.
  • Remove yet another dependency from the tool that is no longer used.
Nov 1 2018, 8:38 AM
xazax.hun created D53979: [analyzer][CTU] Correctly signal in the function index generation tool if there was an error.
Nov 1 2018, 8:35 AM

Oct 31 2018

xazax.hun added a comment to D52794: [analyzer][PlistMacroExpansion] Part 2.: Retrieving the macro name and primitive expansion.

Please add a test case where a bug path goes through a macro definition and this macro is undefed at the end of the translation unit.

Oct 31 2018, 7:16 AM
xazax.hun accepted D52742: [analyzer][PlistMacroExpansion] Part 1.: New expand-macros flag.

LGTM! Thanks, I think it is much easier to understand what is going on this way.

Oct 31 2018, 6:51 AM

Oct 30 2018

xazax.hun accepted D52730: [analyzer] ConversionChecker: handle floating point.

LGTM!
I only wonder if this should be on by default or guarded by a config option. I do not have strong feelings about any of the options though.

Oct 30 2018, 5:27 AM

Oct 29 2018

xazax.hun added inline comments to D53810: [analyzer][NFC] Refactor PlistDiagnostics to use a class instead of passing 9 parameters around.
Oct 29 2018, 8:20 AM

Oct 22 2018

xazax.hun added inline comments to D53277: [analyzer][NFC] Collect all -analyzer-config options in a .def file.
Oct 22 2018, 2:43 AM
xazax.hun added a comment to D53280: [analyzer] Emit an error for invalid -analyzer-config inputs.

I agree with NoQ. Forward and backward compatibility might be important for CodeChecker as well.
But I wonder if it make sense to have analyzer-config compatibility mode on a per config basis?
E.g., if we have two configs:

  • One did not exist in earlier clang versions, but a tool (like CodeChecker) would like to pass this to the analyzer without doing a version check first. Passing this in a compatibility mode makes sense. This could be the regural -analyzer-config
  • The second option also did not exist in earlier clang versions, but we do not want to support those versions. In the case passing this config in a more strict mode makes sense. This could be something like -analyzer-config-strict.
Oct 22 2018, 2:39 AM
xazax.hun added a comment to D53296: [analyzer] New flag to print all -analyzer-config options.

Overall looks good, minor comments inline.

Oct 22 2018, 2:25 AM
xazax.hun added a comment to D53483: [analyzer] Restrict AnalyzerOptions' interface so that non-checker objects have to be registered.

Overall looks good if the community agrees with the directions. Some comments inline.

Oct 22 2018, 2:08 AM

Oct 18 2018

xazax.hun added inline comments to D52730: [analyzer] ConversionChecker: handle floating point.
Oct 18 2018, 2:10 AM

Oct 10 2018

xazax.hun added a comment to D53069: [analyzer][www] Update avaible_checks.html.

I am not sure what to do about implcit checks. Those are probably should never be turned on or off by the user, but they should be on or off by default based on the set of checks the user enabled and the platform she is using. Thus, I am perfectly ok with the implicit_checks.html only being accessible from the checker development manual. Maybe we should extend the checker list with a notice that the user should never disable the core checks.

Oct 10 2018, 3:01 AM

Oct 9 2018

xazax.hun added inline comments to D52742: [analyzer][PlistMacroExpansion] Part 1.: New expand-macros flag.
Oct 9 2018, 2:16 AM
xazax.hun added inline comments to D52984: [analyzer] Checker reviewer's checklist.
Oct 9 2018, 12:46 AM · Restricted Project
xazax.hun added a comment to D52983: [analyzer] Support Reinitializes attribute in MisusedMovedObject check.
In D52983#1258466, @NoQ wrote:

Yay, these look useful. Is there also an attribute for methods that should never be called on a 'moved-from' object?

Oct 9 2018, 12:27 AM · Restricted Project

Oct 8 2018

xazax.hun updated the diff for D52984: [analyzer] Checker reviewer's checklist.
  • Added the ideas from Kristof.
Oct 8 2018, 7:42 AM · Restricted Project
xazax.hun created D52984: [analyzer] Checker reviewer's checklist.
Oct 8 2018, 6:46 AM · Restricted Project
xazax.hun created D52983: [analyzer] Support Reinitializes attribute in MisusedMovedObject check.
Oct 8 2018, 6:28 AM · Restricted Project
xazax.hun added inline comments to D51866: [analyzer][UninitializedObjectChecker] New flag to ignore guarded uninitialized fields.
Oct 8 2018, 2:41 AM
xazax.hun added inline comments to D51866: [analyzer][UninitializedObjectChecker] New flag to ignore guarded uninitialized fields.
Oct 8 2018, 2:35 AM
xazax.hun accepted D52957: [analyzer] Teach CallEvent about C++17 aligned new..

I agree that it would make sense to either not have arguments that are not represented in the AST or create expressions for those implicit arguments.

Oct 8 2018, 2:22 AM

Sep 6 2018

xazax.hun added a comment to D51665: [analyzer] Skip printing trivial nodes in exploded graph.

I like that we print the program points for hidden nodes :) Great work!

Sep 6 2018, 5:32 PM

Aug 21 2018

xazax.hun added inline comments to D51041: [clang-tidy] Don't run misc-unused-using-decls check in C++17..
Aug 21 2018, 8:19 AM
xazax.hun added a comment to D48027: [analyzer] Improve `CallDescription` to handle c++ method..

Oh, and thanks for working on this, this improvement was long overdue, but everybody was busy with something else :)

Aug 21 2018, 8:16 AM
xazax.hun accepted D48027: [analyzer] Improve `CallDescription` to handle c++ method..

Sorry for the delay, I think this is OK to commit.
As a possible improvement, I can imagine making it slightly stricter, e.g. you could only skip QualifiedNames for inline namespaces and the beginning. Maybe add support for staring with "" or :: to even disable skipping namespaces at the beginning?
But these are just nice to have features, I am perfectly ok with not having them or doing it in a followup patch.

Aug 21 2018, 8:15 AM

Aug 15 2018

xazax.hun added a comment to D48027: [analyzer] Improve `CallDescription` to handle c++ method..

Generally looks good, I only wonder if this works well with inline namespaces. Could you test? Probably it will.

Aug 15 2018, 12:51 PM

Aug 2 2018

xazax.hun accepted D49361: [analyzer] Detect pointers escaped after return statement execution in MallocChecker.
Aug 2 2018, 10:54 AM
xazax.hun accepted D49811: [analyzer] Obtain a ReturnStmt from a CFGAutomaticObjDtor.

We could also print something about the ReturnStmt, like source location or pretty print of its expressions so we can check that we picked the right one in case we have multiple.
But consider this as an optional task if you have nothing better to do. I am ok with committing this as is.

Aug 2 2018, 10:51 AM

Jul 27 2018

xazax.hun accepted D49656: [analyzer] Add support for more pointer invalidating functions in InnerPointerChecker.

LGTM!

Jul 27 2018, 6:52 PM

Jul 25 2018

xazax.hun added inline comments to D49656: [analyzer] Add support for more pointer invalidating functions in InnerPointerChecker.
Jul 25 2018, 9:17 AM
xazax.hun added a comment to D49656: [analyzer] Add support for more pointer invalidating functions in InnerPointerChecker.

Small comments inline.

Jul 25 2018, 8:42 AM

Jul 23 2018

xazax.hun added a comment to D49693: [analyzer] Try to minimize the number of equivalent bug reports evaluated by the refutation manager.

What I'm suggesting is: first run all visitors, since no other visitor mark them as invalid, the evaluation of all 497 bugs will be fast and will return only on bug report. We run the refutation manager in this one bug report.

Jul 23 2018, 4:00 PM
xazax.hun added inline comments to D49656: [analyzer] Add support for more pointer invalidating functions in InnerPointerChecker.
Jul 23 2018, 10:04 AM
xazax.hun requested changes to D49656: [analyzer] Add support for more pointer invalidating functions in InnerPointerChecker.

Some comments, mostly nits inline.

Jul 23 2018, 9:01 AM

Jul 19 2018

xazax.hun added a comment to D49568: [analyzer][WIP] Scan the program state map in the visitor only once in DanglingInternalBufferChecker.

Yeah, I would rather have the cleanups and do extra work in the visitor. But lets wait what @NoQ thinks.

Jul 19 2018, 3:00 PM

Jul 11 2018

xazax.hun added a comment to D49074: [Analyzer] [WIP] Basic support for multiplication and division in the constraint manager.

This may remove false-positives (like the example above), but we surely cannot find new errors where multiplicative operations are used.

Do you have examples of those? In my understanding, (almost) all of the imprecisions in the solver lead purely to false positives.
The only example where you lose bugs is when you stop exploring due to reaching a (false) fatal error.

Jul 11 2018, 12:19 PM

Jul 9 2018

xazax.hun added a comment to D49058: [analyzer] Move InnerPointerChecker out of alpha.

Don't you need to edit the tests as well?

Jul 9 2018, 9:46 PM

Jul 8 2018

xazax.hun added a comment to D49057: [analyzer] Track multiple raw pointer symbols in DanglingInternalBufferChecker.

Thanks! The changes look good, I forgot to mark one double lookup though in my previous review.

Jul 8 2018, 10:59 AM
xazax.hun accepted D49057: [analyzer] Track multiple raw pointer symbols in DanglingInternalBufferChecker.

Overall looks good, some nits inline. Let's run it on some projects to exercise this change.

Jul 8 2018, 10:21 AM

Jul 4 2018

xazax.hun added a comment to D48027: [analyzer] Improve `CallDescription` to handle c++ method..
In D48027#1142324, @MTC wrote:
  • There is possible match the wrong AST node, e.g. for the NamedDecl foo(), if the function body has the a::b::x, when we match a::b::X(), we will match foo() . Because I'm not familiar with ASTMatcher, my bad, I can't think of a perfect way to match only the specified nodes.
Jul 4 2018, 12:30 PM

Jun 26 2018

xazax.hun added a comment to D48565: [analyzer] Replace the vector of ConstraintSets by a single ConstraintSet and a function to merge ConstraintSets.

Ok, it looks like naively just dropping all the constraints at Z3 is not the most efficient way.

Jun 26 2018, 12:29 AM

Jun 25 2018

xazax.hun added inline comments to D48532: [analyzer] Add support for std::basic_string::data() in DanglingInternalBufferChecker.
Jun 25 2018, 8:47 AM
xazax.hun accepted D48532: [analyzer] Add support for std::basic_string::data() in DanglingInternalBufferChecker.

LG!

Jun 25 2018, 8:42 AM

Jun 24 2018

xazax.hun accepted D48522: [analyzer] Highlight c_str() call in DanglingInternalBuffer checker.
Jun 24 2018, 10:08 AM
xazax.hun accepted D48460: [analyzer] Fix invalidation on C++ const methods..

LGTM!

Jun 24 2018, 9:59 AM
xazax.hun accepted D48521: [analyzer] Highlight container object destruction in MallocChecker.

LGTM, given that the assert does not fire for the projects you tested on.

Jun 24 2018, 9:56 AM

Jun 23 2018

xazax.hun added a comment to D48522: [analyzer] Highlight c_str() call in DanglingInternalBuffer checker.

Looks better, thanks!

Jun 23 2018, 1:39 PM
xazax.hun added a comment to D48522: [analyzer] Highlight c_str() call in DanglingInternalBuffer checker.

Regarding the visitor:
Maybe rather than looking at the AST, we should check the states, when we started to track the returned symbol?

Jun 23 2018, 12:11 PM
xazax.hun added inline comments to D48521: [analyzer] Highlight container object destruction in MallocChecker.
Jun 23 2018, 12:05 PM
xazax.hun added inline comments to D48513: [analyzer] Correctly create a non-fatal error node for VA list checker..
Jun 23 2018, 1:29 AM

Jun 18 2018

xazax.hun added a comment to D48285: [analyzer][UninitializedObjectChecker] Added "NotesAsWarnings" flag.

I wonder if this could be done when plist is emitted generally, independent of any checks.

Jun 18 2018, 10:50 AM

Jun 13 2018

xazax.hun added inline comments to D48027: [analyzer] Improve `CallDescription` to handle c++ method..
Jun 13 2018, 9:32 AM

Jun 11 2018

xazax.hun added a comment to D48027: [analyzer] Improve `CallDescription` to handle c++ method..

Having C++ support would be awesome!
Thanks for working on this!

Jun 11 2018, 8:09 AM

Jun 10 2018

xazax.hun added a comment to D47671: [analyzer] Implement copy elision..

Just for the record, there is a common example where relying on copy elision might bite and google do not recommend relying on it for correctness: https://abseil.io/tips/120

Jun 10 2018, 3:58 AM

Jun 5 2018

xazax.hun added a comment to D47671: [analyzer] Implement copy elision..

So having an analyzer-config option would be useful for those codebases that are expected to be compiled with less advanced compilers that do not elide copies or not doing it aggressively enough.

I'm not sure it makes sense. From my understanding, that's just how c++17 is defined, and that's unrelated to what compiler implementation is used.

Jun 5 2018, 3:03 PM

Jun 4 2018

xazax.hun added a comment to D47671: [analyzer] Implement copy elision..

So having an analyzer-config option would be useful for those codebases that are expected to be compiled with less advanced compilers that do not elide copies or not doing it aggressively enough. Maybe it is worth to ask on the mailing list of the community wants to have an option for this? I am not sure though how often the end users end up fine tuning the analyzer. It might be nice to have a guide how to do that (and in what circumstances does each of the config values make sense).

Jun 4 2018, 1:29 PM

Jun 1 2018

xazax.hun added inline comments to D45532: [StaticAnalyzer] Checker to find uninitialized fields after a constructor call.
Jun 1 2018, 8:37 AM
xazax.hun added a comment to D46421: [analyzer][CrossTU] Extend CTU to VarDecls with initializer.

Sorry for the limited activity. Unfortunately, I have very little time reviewing patches lately.
I think we need to answer the following questions:

  • Does this change affect the analysis of the constructors of global objects? If so, how?
  • Do we want to import non-const object's initializer expressions? The analyzer might not end up using the value anyways.
  • How big can the index get with this modification for large projects?
Jun 1 2018, 8:29 AM

May 30 2018

xazax.hun added a comment to D45517: [analyzer] False positive refutation with Z3.

I am not not sure that I got the idea what are you suggesting here. If we have the constraint of for example a symbol s > 10 and later on a path we discover s > 20, will we also deduplicate this that way?

No. But I thought in your optimization atoms inside the constraints would be the same?
Could you give an example where they are not?

May 30 2018, 1:44 PM
xazax.hun added a comment to D45517: [analyzer] False positive refutation with Z3.

@xazax.hun (I'll reply here to avoid scattering the conversation across many subtrees)

I was thinking about the optimization for not adding redundant constraints some more, and I've decided I'm still against it ---
we are creating a higher potential for bugs, and we are tightly coupling the visitor to an internal implementation detail (all formulas are eventually purged at purge locations),
which creates a more fragile code.

The proper way to do this would be to have a set of constraints, and then add all constraints there as we iterate through the states (and through constraints inside the state).
If we use the hashing function provided by Z3, the simple act of construction of a set would implicitly drop all redundant constraints.

May 30 2018, 1:03 PM