Page MenuHomePhabricator

steakhal (Balázs Benics)
User

Projects

User does not belong to any projects.

User Details

User Since
Mar 7 2019, 1:49 AM (80 w, 6 d)

Recent Activity

Wed, Sep 16

steakhal added inline comments to D87785: [analyzer][StdLibraryFunctionsChecker] Fix a BufferSize constraint crash.
Wed, Sep 16, 12:53 PM · Restricted Project

Mon, Sep 14

Herald added a reviewer for D61657: Add implementation to two OMPT API routines: jdoerfert.
Mon, Sep 14, 12:42 AM · Restricted Project

Sun, Sep 13

steakhal committed rGcdacffe4acc0: [analyzer][z3] Use more elaborate Z3 variable names (authored by steakhal).
[analyzer][z3] Use more elaborate Z3 variable names
Sun, Sep 13, 11:45 PM
steakhal committed rGd7ae9696e31f: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon (authored by steakhal).
[analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon
Sun, Sep 13, 11:44 PM
steakhal committed rG163863604f9c: [analyzer] Evaluate PredefinedExpressions (authored by steakhal).
[analyzer] Evaluate PredefinedExpressions
Sun, Sep 13, 11:44 PM
steakhal closed D86223: [analyzer][z3] Use more elaborate Z3 variable names.
Sun, Sep 13, 11:44 PM · Restricted Project
steakhal closed D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
Sun, Sep 13, 11:44 PM · Restricted Project
steakhal closed D87004: [analyzer] Evaluate PredefinedExpressions.
Sun, Sep 13, 11:44 PM · Restricted Project
steakhal updated subscribers of D84544: [ConstraintSystem] Add helpers to deal with linear constraints..

I'm curious if we could make use of this in the Clang Static Analyzer.
We always hit the limitations of the current Constraint manager implementation.
What do you think about this @NoQ @xazax.hun @Szelethus?

Sun, Sep 13, 6:56 AM · Restricted Project

Thu, Sep 10

steakhal added a comment to D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h..

After reviewing the code of this snippet, I think it would be very difficult to make a regression test case for the crash, as far as what I know about Z3 and SMT solvers.

First of all, all calls to Solver->check() will return true for sat, false for unsat, and empty for a timeout.
On line 132, the manager invokes Z3 for solving the constraints under the current state.
On line 137, the manager invokes Z3 for getting a model (a valid result) satisfying the constraints.
On line 141, the manager adds another constraint to exclude the model gotten from the model.
On line 149, the manager invokes Z3 for solving the excluded constraint.
In summary, the manager will first solver the constraint for a result of the queried symbolic variable. If there is a valid value, it excludes the value and solves again to check whether it is the only valid result.

To trigger the crash, we need to construct a group of constraints that are sat. Then, we need to exclude a valid value for a symbolic variable and make the constraints lead to a timeout (rather than an unsat). Simple linear constraints have very few chances to lead to a timeout. I tried to create a group of constraints from https://stackoverflow.com/questions/20536435/z3-what-might-be-the-reason-for-timeout, which are a group of non-linear unsat constraints that can trigger a timeout (under a timeout of 10 seconds). However, I have not successfully made one, as it has too many things to do with mathematics. And my SMT solver colleagues also think it is quite difficult to make one.

I suspected this one due to my previous investigation.

Thu, Sep 10, 12:56 AM · Restricted Project

Wed, Sep 9

steakhal accepted D87239: [analyzer][StdLibraryFunctionsChecker] Remove strcasecmp.

So, the problem is rather that the constraint check should be done in checkPreCall, but that should be in an NFC refactoring.

Wed, Sep 9, 11:13 AM · Restricted Project
steakhal added a comment to D84316: [analyzer][NFC] Split CStringChecker to modeling and reporting.

I would like to discuss why don't we have a distinct checker managing the bookkeeping stuff of the CString lengths.
I just want a clean understanding and wide consensus about this.

Wed, Sep 9, 1:15 AM · Restricted Project

Tue, Sep 8

steakhal added a comment to D86445: [analyzer][RFC] Simplify MetadataSymbol representation and resolve a CStringChecker FIXME.

But if the string is invalidated (or the new length is completely unknown), do not remove the length from the state; instead, set it to SymbolConjured.

Where exactly do you implement the above?

When strlen(R) is used for the first time on a region R, produce $meta<size_t R> as the answer, but *do not store* it in the string length map.

And this?

Tue, Sep 8, 7:45 AM · Restricted Project

Mon, Sep 7

steakhal accepted D87138: [analyzer][NFC] Introduce refactoring of PthreadLockChecker.

Seems fine to me.

Mon, Sep 7, 8:21 AM · Restricted Project
steakhal added a comment to D87239: [analyzer][StdLibraryFunctionsChecker] Remove strcasecmp.

I completely agree with you.
I plan to further refactor the CStringChecker, but the related patches are pretty much stuck :D

Mon, Sep 7, 8:18 AM · Restricted Project
steakhal added a comment to D86135: [analyzer][MacroExpansion] Fix a crash where multiple parameters resolved to __VA_ARGS__.

Perfectly clear, thank you. However, I would still rely on the others to accept this :|

Mon, Sep 7, 8:05 AM · Restricted Project
steakhal added a comment to D85984: [analyzer] Add a new checker alpha.cplusplus.CPlusPlus11Lock.

I have checked only your test, but the readability of the reports should be improved.
You frequently refer to previous events, such as This lock has already been unlocked, This lock has already been acquired, etc.
It isn't clear to the reader where do you refer to. IMO you should put a NoteTag at the interesting locations to achieve more readable diagnostics.

Mon, Sep 7, 7:58 AM · Restricted Project
steakhal added a comment to D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h..

Ping @OikawaKirie .
How should we proceed?
I would happily participate in creating a minimal repro for this, but I need at least one crash.

Mon, Sep 7, 7:41 AM · Restricted Project
steakhal updated the diff for D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
  • Fixed typo in the link Clang Static Analyser -> Clang Static Analyzer
Mon, Sep 7, 7:37 AM · Restricted Project
steakhal added a comment to D86874: [analyzer] Fix ArrayBoundCheckerV2 false positive regarding size_t indexer.

I can only imagine how long it took for you to write all this, because reading it wasn't that short either. Thank you so much! It really gave me a perspective on how you see this problem, as well as what is actually happening (and should happen) in the checker.

Thank you very much. I tied to make it as short as possible while keeping all the necessary details to make my reasoning perfectly clean. Now I think I was on a bad track, but @martong helped me to pinpoint some issues.

Mon, Sep 7, 7:28 AM · Restricted Project
steakhal added a comment to D86874: [analyzer] Fix ArrayBoundCheckerV2 false positive regarding size_t indexer.
Calculation of the RegionRawOffsetV2

Let's see how does these subscript expressions used during the calculation of the RegionRawOffsetV2:
For multi-dimension arrays we fold the index expressions of the nested ElementRegions.
We are doing that by simply calculating the byte-offset of the nested region, and adding the current level's index*sizeof(Type).
So, the ByteOffset that we build up will contain mostly multiplications by a constant OR additions of symbolic expressions (like the x+1 in the example).

We have these lines in the case of handling the ElementRegion:

if (!index.getAs<NonLoc>())
  return RegionRawOffsetV2();

So, if the index is symbolic we give up, don't we? So, how could this work with x+1? What am I missing here?

In my example, I'm speaking about the case when it's nonloc::SymbolVal wrapping the expression x+1. So not every NonLoc is ConcreteInt.

Mon, Sep 7, 7:11 AM · Restricted Project
steakhal updated the diff for D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
  • Mentioned the previous namespaces as well (GR, entoGR)
  • Slightly rephrased previous sentences
  • Updated the summary, to give a deeper dive into the history of the Clang Static Analyzer - for git blame
Mon, Sep 7, 5:38 AM · Restricted Project
steakhal added a comment to D85424: [Analyzer] Crash fix for alpha.cplusplus.IteratorRange.

OK, after a few hours of debugging, the test code simplifies to this:

// RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,alpha.cplusplus.IteratorRange -analyzer-config aggressive-binary-operation-simplification=true %s -verify
Mon, Sep 7, 3:20 AM · Restricted Project

Fri, Sep 4

steakhal added a comment to D86874: [analyzer] Fix ArrayBoundCheckerV2 false positive regarding size_t indexer.

Hi Balázs,

Since reviews.llvm.org is offline, I am sending my comments below, inline.
Thanks for your huge effort in explaining all this!

Overall, I have a feeling that this approach targets only one specific
case, which is fine. But I believe we should think about all the other
possible cases, so we could get rid of other false positives too:

  1. In case of multidimensional arrays, there may be a symbolic value in any

dimension.

Yes, obviously - but it's not a problem. See my next comment.

Fri, Sep 4, 3:16 AM · Restricted Project

Thu, Sep 3

steakhal added a comment to D86874: [analyzer] Fix ArrayBoundCheckerV2 false positive regarding size_t indexer.

I really feel that this check would have a better place in the implementation of eval. This seems really counter-intuitive to do this stuff at the Checker's level. Is there any reason why we can't do this in eval?
evalBinOpNN could return with Unknown, and the state should remain unchanged. Am I missing something?

Thu, Sep 3, 7:52 AM · Restricted Project

Wed, Sep 2

steakhal added a comment to D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.

I'm not opposed to landing this to master, as we will have more time there to see whether there are any unwanted side effects in practice.

Wed, Sep 2, 9:51 AM · Restricted Project
steakhal added a comment to D87004: [analyzer] Evaluate PredefinedExpressions.

Thank you all for the comments!

Wed, Sep 2, 7:51 AM · Restricted Project
steakhal updated the diff for D87004: [analyzer] Evaluate PredefinedExpressions.
  • Added no-warning.
  • Added test-case for __builtin_unique_stable_name as well.
Wed, Sep 2, 7:50 AM · Restricted Project
steakhal added inline comments to D87004: [analyzer] Evaluate PredefinedExpressions.
Wed, Sep 2, 6:30 AM · Restricted Project
steakhal updated the diff for D87004: [analyzer] Evaluate PredefinedExpressions.

We only analyze instantiated functions, which are not dependently typed.
Safe to assume that every encountered PredefinedExpression has a defined (non-null) function name.

Wed, Sep 2, 6:30 AM · Restricted Project
steakhal added inline comments to D87004: [analyzer] Evaluate PredefinedExpressions.
Wed, Sep 2, 4:45 AM · Restricted Project
steakhal updated the diff for D87004: [analyzer] Evaluate PredefinedExpressions.
  • Added tests for Microsoft extensions.
  • Added an assert requiring the PredefinedExpression to have a function name.
Wed, Sep 2, 4:43 AM · Restricted Project
steakhal requested review of D87004: [analyzer] Evaluate PredefinedExpressions.
Wed, Sep 2, 2:30 AM · Restricted Project

Tue, Sep 1

steakhal added inline comments to D86870: [analyzer] Add more tests for ArrayBoundCheckerV2.
Tue, Sep 1, 2:47 AM · Restricted Project
steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.

I tried to run the benchmark on the small set of projects but it would take an enormous time to analyze all such projects 20 times each...
Dedicating a box for this is unfeasible for me.
So I stuck with analyzing only tmux with 20 iterations.
The results are not convincing enough IMO.

Tue, Sep 1, 2:26 AM · Restricted Project
steakhal added inline comments to D86873: [analyzer][NFC] Refactor ArrayBoundCheckerV2.
Tue, Sep 1, 2:02 AM · Restricted Project
steakhal added inline comments to D86870: [analyzer] Add more tests for ArrayBoundCheckerV2.
Tue, Sep 1, 1:52 AM · Restricted Project

Mon, Aug 31

steakhal added a comment to D85424: [Analyzer] Crash fix for alpha.cplusplus.IteratorRange.

CReduce did not manage to produce any meaningful result after a week worth of runtime (more than ~2000 lines of code still remaining after reduction). We could track this down by tracing the ExprEngine code that assigns the Undefined SVal but that seems a huge effort as well. That could be done by debugging the SVal-assigning statements, and setting conditional breakpoints (ie. only break when the value is Undefined). When a breakpoint is hit, we could dump the statement that triggered it and try to reason about the conditions at that point. I also recommend using the rr tool as it allows you to use fixed pointer values while debugging.

Mon, Aug 31, 10:16 AM · Restricted Project
steakhal resigned from D86736: [analyzer][NFC] Don't bind values to ObjCForCollectionStmt, replace it with a GDM trait.

I don't have much to say, but to keep up the good work xD
I will follow this and the rest of your patches @Szelethus.

Mon, Aug 31, 5:39 AM · Restricted Project
steakhal requested review of D86874: [analyzer] Fix ArrayBoundCheckerV2 false positive regarding size_t indexer.
Mon, Aug 31, 5:18 AM · Restricted Project
steakhal requested review of D86873: [analyzer][NFC] Refactor ArrayBoundCheckerV2.
Mon, Aug 31, 4:53 AM · Restricted Project
steakhal updated the summary of D86870: [analyzer] Add more tests for ArrayBoundCheckerV2.
Mon, Aug 31, 4:31 AM · Restricted Project
steakhal requested review of D86870: [analyzer] Add more tests for ArrayBoundCheckerV2.
Mon, Aug 31, 4:30 AM · Restricted Project

Thu, Aug 27

steakhal added a comment to D86465: [analyzer][solver] Redesign constraint ranges data structure.

Previously, I liked this. Now I love it!
The benchmarks look promising as well.

Thu, Aug 27, 9:11 AM · Restricted Project

Wed, Aug 26

steakhal added inline comments to D86465: [analyzer][solver] Redesign constraint ranges data structure.
Wed, Aug 26, 5:49 AM · Restricted Project
steakhal added inline comments to D86533: (Urgent!) [release][docs][analyzer] Add 11.0.0. release notes.
Wed, Aug 26, 5:30 AM · Restricted Project
steakhal added inline comments to D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
Wed, Aug 26, 2:51 AM · Restricted Project
steakhal added a comment to D81254: [analyzer] Produce symbolic values for C-array elements.

We know where it points to (aka. the pointer's value is conjured), but we don't know what the value if there.

Absolutely right. I looked at this patch after a while and don't currently see a proper solution.

I feel like this problem should be handled by some sort of invalidation mechanism.

Definitely it should be some criteria/mark/flag about the region invalidation. Maybe someone more confident could prompt us how to.

How about using the mistical SymbolDerived?
The clang-analyzer-guide says:

Another atomic symbol, closely related to SymbolRegionValue, is SymbolDerived. It represents a value of a region after another symbol was written into a direct or indirect super-region. SymbolDerived contains a reference to both the parent symbol and the parent region. This symbol is mostly a technical hack. Usually SymbolDerived appears after invalidation: the whole structure of a certain type gets smashed with a single SymbolConjured, and then values of its fields become represented with the help of SymbolDerived of that conjured symbol and the region of the field. In any case, SymbolDerived is similar to SymbolRegionValue, just refers to a value after a certain event during analysis rather than at start of analysis.

Could we use that here @NoQ?

Wed, Aug 26, 2:41 AM · Restricted Project
steakhal added inline comments to D86445: [analyzer][RFC] Simplify MetadataSymbol representation and resolve a CStringChecker FIXME.
Wed, Aug 26, 1:28 AM · Restricted Project

Tue, Aug 25

steakhal added a comment to D85728: [Analyzer] Support for the new variadic isa<> and isa_and_not_null<> in CastValueChecker.
In D85728#2237006, @NoQ wrote:

Hans is pinging us on Bugzilla because this patch is marked as a release blocker (and i believe that it indeed is). I think we should land these patches.

I believe @baloghadamsoftware is on vacation.
I'm sure he won't be mad if you commit on his behalf.

Tue, Aug 25, 12:19 PM · Restricted Project
steakhal added a comment to D86135: [analyzer][MacroExpansion] Fix a crash where multiple parameters resolved to __VA_ARGS__.

I'm not sure about the status of this patch.
If you say that further improvements will be done later and this functionality is enough, I'm fine with that.

Tue, Aug 25, 7:59 AM · Restricted Project
steakhal added a comment to D86465: [analyzer][solver] Redesign constraint ranges data structure.

This is a huge change, I've got pretty tired at the end of the review.
I haven't checked the test-cases too deeply.

Tue, Aug 25, 7:36 AM · Restricted Project
steakhal requested changes to D86135: [analyzer][MacroExpansion] Fix a crash where multiple parameters resolved to __VA_ARGS__.

This preprocessor expansion stuff is definitely not my expertise, nvm here is my review.

Tue, Aug 25, 2:55 AM · Restricted Project

Aug 24 2020

steakhal updated the diff for D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
  • Rephrase paragraph
  • Use desktop site wikipedia link
Aug 24 2020, 10:52 AM · Restricted Project
steakhal added inline comments to D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
Aug 24 2020, 8:04 AM · Restricted Project
steakhal updated the diff for D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.

Add link to the static analyzer llvm page.

Aug 24 2020, 8:04 AM · Restricted Project
steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.

And what is the error right now?

Aug 24 2020, 7:55 AM · Restricted Project
steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.

Yep, I guess that is the cause. I'll take a look. Did you try it with this fast fix?

I tried, but it lacks further fixes.

Aug 24 2020, 7:26 AM · Restricted Project
steakhal added a comment to D84316: [analyzer][NFC] Split CStringChecker to modeling and reporting.

Do I sense correctly that the only information CSrtingLengthModeling.cpp requires from the actual CStringChecker is a checker tag?

AFAIK yes.

Aug 24 2020, 6:49 AM · Restricted Project
steakhal added inline comments to D86445: [analyzer][RFC] Simplify MetadataSymbol representation and resolve a CStringChecker FIXME.
Aug 24 2020, 6:39 AM · Restricted Project
steakhal added inline comments to D86445: [analyzer][RFC] Simplify MetadataSymbol representation and resolve a CStringChecker FIXME.
Aug 24 2020, 6:33 AM · Restricted Project
steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.

Here is a short summary how to do regression testing (check that all warnings are the same):

Oh thanks for the detailed guide, I will make the experiment.

Aug 24 2020, 5:40 AM · Restricted Project
steakhal requested review of D86446: [analyzer][docs][NFC] Document the ento namespace in the llvm/Lexicon.
Aug 24 2020, 5:07 AM · Restricted Project
steakhal requested review of D86445: [analyzer][RFC] Simplify MetadataSymbol representation and resolve a CStringChecker FIXME.
Aug 24 2020, 4:15 AM · Restricted Project
steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.
In D86295#2231760, @NoQ wrote:

I believe @vsavchenko's docker thingy already knows how to do that.

Yep, it sure does! Additionally, there is a benchmark subcommand that can chart memory consumption for measured projects.

Could you point me to some docs to help getting started? I haven't used this docker image.

Aug 24 2020, 3:09 AM · Restricted Project
steakhal updated the diff for D86223: [analyzer][z3] Use more elaborate Z3 variable names.

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.

Aug 24 2020, 12:44 AM · Restricted Project

Aug 22 2020

steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.
In D86295#2231760, @NoQ wrote:

I mean, like, you can measure the entire process with time or something like that. I believe @vsavchenko's docker thingy already knows how to do that.

I tried to measure this with time, without much luck:

Aug 22 2020, 9:49 AM · Restricted Project
steakhal added inline comments to D86223: [analyzer][z3] Use more elaborate Z3 variable names.
Aug 22 2020, 9:44 AM · Restricted Project
steakhal updated the diff for D86223: [analyzer][z3] Use more elaborate Z3 variable names.

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.

Aug 22 2020, 9:43 AM · Restricted Project
steakhal updated the diff for D86223: [analyzer][z3] Use more elaborate Z3 variable names.

Use virtual getKindStr method for acquiring the kind name.

Aug 22 2020, 8:14 AM · Restricted Project

Aug 21 2020

steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.
In D86295#2229712, @NoQ wrote:

Heh, nice! Did you try to measure the actual impact of this change on memory and/or performance?

Eh, I don't really know how to bench this.
Here is how I did it in nutshell:
Added STATISTIC counters to MemRegion ctor, dtor, getAsOffset begining and the path of just returning the cached value.

Aug 21 2020, 8:23 AM · Restricted Project
steakhal added a comment to D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h..

It seems that this patch is stuck.
How can I reproduce the crash? @OikawaKirie

Aug 21 2020, 6:28 AM · Restricted Project

Aug 20 2020

steakhal added a comment to D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.

It would be nice to have this fix in clang11.
Do you think it's qualified for it?

Aug 20 2020, 2:02 PM · Restricted Project
steakhal added a comment to D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.

But unless you add a comment one will probably replace the offset with an optional as the part of a refactoring.

Sure, I will leave a note.

Aug 20 2020, 10:11 AM · Restricted Project
steakhal added a comment to D86223: [analyzer][z3] Use more elaborate Z3 variable names.

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?

Aug 20 2020, 10:08 AM · Restricted Project
steakhal retitled D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size from [analyzer] Reorder the the layout of MemRegion and cache by hand for optimal size to [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.
Aug 20 2020, 8:20 AM · Restricted Project
steakhal requested review of D86295: [analyzer] Reorder the layout of MemRegion and cache by hand for optimal size.
Aug 20 2020, 8:19 AM · Restricted Project

Aug 19 2020

steakhal added a comment to D86223: [analyzer][z3] Use more elaborate Z3 variable names.

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

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

Aug 19 2020, 3:49 PM · Restricted Project
steakhal added a comment to D86223: [analyzer][z3] Use more elaborate Z3 variable names.

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

Aug 19 2020, 11:49 AM · Restricted Project
steakhal requested review of D86223: [analyzer][z3] Use more elaborate Z3 variable names.
Aug 19 2020, 9:15 AM · Restricted Project

Aug 18 2020

steakhal added inline comments to D84736: [analyzer] Handle pointer difference of ElementRegion and SymbolicRegion.
Aug 18 2020, 10:19 AM · Restricted Project
steakhal added inline comments to D84736: [analyzer] Handle pointer difference of ElementRegion and SymbolicRegion.
Aug 18 2020, 10:12 AM · Restricted Project
steakhal updated the diff for D84736: [analyzer] Handle pointer difference of ElementRegion and SymbolicRegion.
  • Refined documentation comments as noted.
  • Added tests.
  • Removed the complicated ByteOffsetOfElement lambda.
  • Rename revision.
Aug 18 2020, 10:08 AM · Restricted Project
steakhal added a comment to D84979: [analyzer][NFC] Refine CStringLength modeling API.

Really I am still not totally familiar how the checkers work and if it is good to have these function names.

Yea, naming things is pretty hard. I'm open to have a less verbose one - especially since these API functions will live under some namespace.

Aug 18 2020, 1:27 AM · Restricted Project
steakhal updated the diff for D84979: [analyzer][NFC] Refine CStringLength modeling API.

Fixed Artem's inline comments:

  • cstring::getCStringLength now takes StateRef by value
  • cstring::dumpCStringLengths now takes by StateRef by non const value
Aug 18 2020, 1:25 AM · Restricted Project
steakhal abandoned D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs.

I no longer think that we should support Symbol to Symbol comparisons.
It would introduce certain anomalies, like Why could the CM reason about this and that comparisons wile could not in others.

Aug 18 2020, 12:51 AM · Restricted Project
steakhal added a comment to D84316: [analyzer][NFC] Split CStringChecker to modeling and reporting.

Ping

Aug 18 2020, 12:45 AM · Restricted Project
steakhal updated the diff for D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.

Add an extra RUN line without refutation.
The expected result is the same as with refutation.

Aug 18 2020, 12:44 AM · Restricted Project

Aug 10 2020

steakhal added a comment to D81254: [analyzer] Produce symbolic values for C-array elements.

@NoQ, thanks for the examples.

I didn't get the first one. How do you get to the "In reality we don't know", if we don't touch a[index1]:

If index1 and index2 has the same value, we should not be confident that the x == y holds.

Aug 10 2020, 11:15 AM · Restricted Project
steakhal updated the summary of D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
Aug 10 2020, 5:23 AM · Restricted Project

Aug 9 2020

steakhal updated the summary of D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
Aug 9 2020, 4:41 AM · Restricted Project
steakhal added a comment to D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.

I mean, this shouldn't be an issue. Since we already omitted the 'unnecessary' cast expressions... That decision is the root cause of this, we should have expected that.

Aug 9 2020, 4:02 AM · Restricted Project
steakhal added a comment to D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.

Looks reasonable to me, but I am not very familiar with the impacts of the additional casts. Do we lose some modeling power when we are using the regular constraint solver?

For example, when we have constraints both on the original and the cased symbol can the analyzer "merge" them?

Something like:

ScopedPrimitive sym = conjure<ScopedPrimitive>();
if (sym == ScopedPrimitive::Max)
  return;
int sym2 = static_cast<unsigned char>(sym);
if (sym2 == 0)
  return;
// Do we know here that both sym and sym2 has the same range?
// Is there a change in the behavior compared to before the patch?
Aug 9 2020, 3:30 AM · Restricted Project

Aug 8 2020

steakhal added a comment to D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
In D85528#2203325, @NoQ wrote:

Aha, ok, sounds like the right thing to do. Like, for Z3 it's actually the wrong thing to do (you'd prefer to evaluate the cast perfectly by adding SymbolCast) but for pure RangeConstraintManager this is the lesser of two evils.

My primary objective is to fix all the crashes related to Range CM + Z3 refutation.

Aug 8 2020, 2:24 AM · Restricted Project
steakhal updated the diff for D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
  • Using dumps instead of reaching in tests.
  • Not requiring complete enums anymore (unlike we did before the patch).
Aug 8 2020, 2:22 AM · Restricted Project

Aug 7 2020

steakhal added a comment to D85424: [Analyzer] Crash fix for alpha.cplusplus.IteratorRange.

Unfortunately, I could not create test for it. It is extremely rare that the Analyzer creates an UndefinedVal.

Aug 7 2020, 10:36 AM · Restricted Project
steakhal updated the diff for D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
  • Moved the FIXME closer to the subject.
  • Added tests for covering incomplete enums as well.
  • Added REQUIRES: z3. This will mark the test case unsupported on every buildbots. See my notes about this behavior at D83677.
  • Refined test file.
Aug 7 2020, 9:52 AM · Restricted Project
steakhal planned changes to D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
Aug 7 2020, 9:14 AM · Restricted Project
steakhal requested review of D85528: [analyzer] Fix cast evaluation on scoped enums in ExprEngine.
Aug 7 2020, 8:10 AM · Restricted Project

Aug 5 2020

steakhal planned changes to D84736: [analyzer] Handle pointer difference of ElementRegion and SymbolicRegion.
Aug 5 2020, 3:40 AM · Restricted Project