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?

In D83660#2264963, @OikawaKirie wrote:

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.

In D87239#2259428, @martong wrote:

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

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.

In D86445#2260744, @martong wrote:

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?

Seems fine to me.

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

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

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.

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

• Fixed typo in the link Clang Static Analyser -> Clang Static Analyzer

In D86874#2259105, @Szelethus wrote:

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.

In D86874#2256249, @martong wrote:

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.

• 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

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

In D86874#2255990, @martong wrote:

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.

In D86874#inline-803844, @martong wrote:

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?

In D85528#2232074, @xazax.hun wrote:

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.

Thank you all for the comments!

• Added no-warning.
• Added test-case for __builtin_unique_stable_name as well.

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

• Added tests for Microsoft extensions.
• Added an assert requiring the PredefinedExpression to have a function name.

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.

In D85424#2247598, @gamesh411 wrote:

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.

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.

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

In D81254#2218196, @ASDenysPetrov wrote:

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?

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.

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.

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.

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

• Rephrase paragraph
• Use desktop site wikipedia link

Add link to the static analyzer llvm page.

In D86295#2233694, @vsavchenko wrote:

And what is the error right now?

In D86295#2233401, @vsavchenko wrote:

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.

In D84316#2233368, @Szelethus wrote:

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

AFAIK yes.

In D86295#2233244, @vsavchenko wrote:

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.

In D86295#2233076, @vsavchenko wrote:

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.

In D86223#2232681, @mikhail.ramalho wrote:

In D86223#2231991, @steakhal wrote:

In D86223#2231959, @mikhail.ramalho wrote:

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.

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:

In D86223#2231959, @mikhail.ramalho wrote:

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.

Use virtual getKindStr method for acquiring the kind name.

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.

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

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

In D86295#2228745, @xazax.hun wrote:

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.

In D86223#2228731, @xazax.hun wrote:

In D86223#2227353, @steakhal wrote:

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?

In D86223#2226876, @xazax.hun wrote:

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

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

In D86223#2226630, @xazax.hun wrote:

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

• Refined documentation comments as noted.
• Added tests.
• Removed the complicated ByteOffsetOfElement lambda.
• Rename revision.

In D84979#2190996, @balazske wrote:

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.

Fixed Artem's inline comments:

• cstring::getCStringLength now takes StateRef by value
• cstring::dumpCStringLengths now takes by StateRef by non const value

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.

Ping

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

In D81254#2122449, @ASDenysPetrov wrote:

@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.

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.

In D85528#2205094, @xazax.hun wrote:

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?

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.

• Using dumps instead of reaching in tests.
• Not requiring complete enums anymore (unlike we did before the patch).

In D85424#2199471, @baloghadamsoftware wrote:

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

• 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.