<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Ok, first of all, the example false positive you're debugging is not
an example of the bug you're trying to look into, but an example of
a completely different long-standing bug:
<a class="moz-txt-link-freetext" href="https://bugs.llvm.org/show_bug.cgi?id=44114">https://bugs.llvm.org/show_bug.cgi?id=44114</a>. Both bugzilla entries
contain a large number of examples to choose from. None of those are
beginner bugs though, the reason why they're not fixed is because
they require a relatively large amount of work and a relatively good
understanding of the subject.<br>
<br>
For your specific example, no, you didn't identify the buggy
transition correctly, so you're debugging the part that has nothing
to do with the false positive. I strongly recommend finding the
buggy transition in your ExplodedGraph dump *before* jumping into
the debugger. This usually goes from bottom to top, exactly like
you're expected to read a static analyzer report. Let me explain
this procedure on your example.<br>
<br>
I attached a screenshot of the tail of the ExplodedGraph dump for
your code (i hope this works fine with the mailing list). That's
just three last nodes of the graph but they're enough to identify
the problem.<br>
<br>
Node 53 is the bug node, as stated in red; this is the node that was
produced by generateErrorNode() and fed into the BugReport object.
The bug report says "Branch condition evaluates to a garbage value".
The AST expression p[1] (which acts as the branch condition which we
can confirm by looking at the source code) has symbolic value
"Undefined". Therefore we can conclude that the bug report was
emitted correctly and the our problem is not in the checker callback
that emitted the bug report; it was simply fed an incorrect State
1337. Since the only reason why the bug report was emitted was that
the value was Undefined, we have to find a node in which "Undefined"
was written into the state.<br>
<br>
Node 52 doesn't update the state, so we can skip it. In fact it's
nicely grouped with node 51 so we barely even notice it.<br>
<br>
Node 51 is the nearest node on which the AST expression p[1] was
first evaluated into Undefined. Whatever code was responsible for
evaluating node 51 is directly responsible for assigning Undefined
value to the expression - which ultimately led to the false positive
in node 53. It is easy to see what was supposed to happen at this
node: this is a memory load (which is also known in C and C++
formalism as "implicit lvalue-to-rvalue conversion" - the operation
that converts object-as-in-"location" into object-as-in-"data"). The
operation does not change contents of memory, it only reads the
existing memory.<br>
<br>
Static analyzer represents the knowledge of existing memory in a
data structure known as the Store, aka "Region Store".
Straightforwardly, it maps "memory regions" (symbolic
representations of locations) into arbitrary SVals (symbolic
representations of data). No, Balazs, it doesn't map "values to
expressions" =/ The Store is written down in the dump and labeled
accordingly. In our case there are three entries in the Store:<br>
<br>
(1) Variable "myvar" has 16-bit unsigned integer 4386 written into
it at byte offset 0;<br>
(2) Variable "p" has a pointer to the first char (hence index 0) of
variable "myvar" written into it at byte offset 0.<br>
(3) Variable "x" has 32-bit signed integer 1 written into it at byte
offset 0.<br>
<br>
The location we're loading from is already evaluated: it's the value
of AST expression p[1] before the load. The Expressions section (aka
the Environment) contains two entries for p[1] because implicit
lvalue-to-rvalue casts do not have any visual representation in C,
however by matching statement identifiers (S780 and S784) with the
respective program point dumps (S780: ArraySubscriptExpr, S784:
ImplicitCastExpr (LValueToRValue)) you can easily see that S780 is
the sub-expression of the load and S784 is the load itself.
Therefore the location which we're loading from is the value of AST
expression p[1], namely the *second* char of variable "myvar".<br>
<br>
Knowing these facts about the memory of our program, we need to
decide whether the load was performed correctly. If the load was
performed incorrectly, our job is done: we've found the root cause.
If the load was performed correctly that'd have meant that the state
is incorrect and we have to go further up in order to find it.<br>
<br>
It's fairly obvious that the load was not performed correctly.
Looking at Store entry (1), it is easy to see that the second
character of variable "myvar" has value 17 rather than "Undefined".<br>
<br>
Therefore our problem consists entirely in incorrect construction of
node 51. Now's the good time to jump into the debugger, set
conditional breakpoint on evalLoad with condition "predecessor node
has identifier 50" and debug from there.<br>
<br>
The pointer cast that you were trying to debug was not at fault. We
can still discuss it separately but it's not what really causes this
specific false positive to show up.<br>
<br>
This entire debugging procedure is very straightforward and requires
almost no thinking. You simply match static analyzer's simulation of
the program's behavior to the actual runtime behavior of the program
and check whether the former is a correct abstraction over the
latter. Static analyzer is just an interpreter (cf. "abstract
interpretation") so it's very easy to reason about the correctness
of every transition as long as you know the language it's trying to
interpret (in this case, C). Which is why i made this 2018
conference talk in order to explain it. The only non-trivial part is
knowing the structure of the program state (store vs environment,
what are regions and symbols and how to read them) which is why i
did this whole workbook thing on that subject in 2016. I wish i did
it properly so that all the documentation was in one place but for
now that's where we are i guess.<br>
<br>
<div class="moz-cite-prefix">On 12/7/20 7:40 AM, Balázs Benics via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAF2=K3U_-5MWKo6LbVDgNPmW8tm51NzdbSfdi0Oq9n5cj7CcnQ@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>Ok, you are saying that we should know that `p[1]` points
to an object which was initialized. And according to the
target's endianness, resolve the DeclRefExpr to the
appropriate constant value.</div>
<div><br>
</div>
<div>The dumps are probably from the line `char *p =
&myvar;` if I'm right.<br>
</div>
<div>That is the reason why the right-hand side is evaluated to
the location of `myvar`, but wrapped into an ElementRegion of
type char representing the reinterpret cast.</div>
<div>IMO, it's the correct behavior to this point.<br>
</div>
<div><br>
</div>
<div>You should probably dig around the evaluation of the
`DeclRefExpr` of the expression `p[1]`. That should return
your concrete value.<br>
</div>
<div>AFAIK, the store maps the values to expressions and the
problem probably resides there.<br>
</div>
<div>But it's just a wide guess :D</div>
<div><br>
</div>
<div>Unfortunately, that is all I can say about this right now
:(<br>
</div>
<div><br>
</div>
<div>Balazs.<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">Vince Bridgers via cfe-dev
<<a href="mailto:cfe-dev@lists.llvm.org"
moz-do-not-send="true">cfe-dev@lists.llvm.org</a>> ezt
írta (időpont: 2020. dec. 7., H, 11:54):<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr">Hi all, I thought I'd look at this problem <a
href="https://bugs.llvm.org/show_bug.cgi?id=43364"
target="_blank" moz-do-not-send="true">https://bugs.llvm.org/show_bug.cgi?id=43364</a>
(Pointer cast representation problems). maybe use it as an
opportunity to dig into the inner workings of the analyzer
and maybe even solve a concrete problem :) But it seems I
need guidance about possible paths to pursue.
<div><br>
</div>
<div>Starting with a concrete case, a simple reproducer is
below. I debugged this down to
SimpleSValBuilder.cpp:evalCastFromLoc(). val is an SVal
and castTy is a Loc, and this code path attempts to
extract a concrete integer from the SVal (did I get this
right?). So I think a solution to this specific case would
be to dig into the SVal to see if casted data is concrete,
and extract that data. Seems to me this would be
the location for that (evalCastFromLoc seems
appropropriate enough). If that's true, can someone point
me to an example that's similar? I'll keep digging, but
thought I'd ask in case this is easy for someone to drop a
few helpful hints. </div>
<div><br>
</div>
<div>I've included some select dumps, state and a bt below
in case this is helpful. </div>
<div><br>
</div>
<div>Best</div>
<div><br>
</div>
<div>(gdb) p val.dump()<br>
&Element{myvar,0 S64b,char}$2 = void<br>
</div>
<div><br>
</div>
<div>(gdb) p castTy.dump()<br>
PointerType 0xf931740 'char *'<br>
`-BuiltinType 0xf930b50 'char'<br>
$3 = void<br>
</div>
<div><br>
</div>
<div><br>
</div>
<div>Invocation: clang -cc1 -analyze -analyzer-checker=core
case.c <br>
</div>
<div><br>
</div>
<div>struct mystruct {<br>
</div>
<div> unsigned short _u16;<br>
};<br>
<br>
int main(void) {<br>
struct mystruct myvar = { 0x1122 };<br>
<br>
char *p = &myvar;<br>
int x = 0;<br>
if (p[0])<br>
x+=1;<br>
if (p[1]) // Branch condition evaluates to a garbage
value [core.uninitialized.Branch]<br>
x+=1;<br>
return x;<br>
}<br>
</div>
<div><br>
</div>
<div>(gdb) p state<br>
$4 = {Obj = 0xf9b81b8}<br>
(gdb) p state->dump()<br>
"program_state": {<br>
"store": { "pointer": "0xf9b6fa2", "items": [<br>
{ "cluster": "myvar", "pointer": "0xf9b2250", "items":
[<br>
{ "kind": "Direct", "offset": 0, "value": "4386
U16b" }<br>
]},<br>
{ "cluster": "p", "pointer": "0xf9b2aa8", "items": [<br>
{ "kind": "Direct", "offset": 0, "value":
"&Element{myvar,0 S64b,char}" }<br>
]},<br>
{ "cluster": "x", "pointer": "0xf9b6ed0", "items": [<br>
{ "kind": "Direct", "offset": 0, "value": "1 S32b" }<br>
]}<br>
]},<br>
"environment": { "pointer": "0xf9b16e0", "items": [<br>
{ "lctx_id": 1, "location_context": "#0 Call",
"calling": "main", "location": null, "items": [<br>
{ "stmt_id": 898, "pretty": "p", "value": "&p" }<br>
]}<br>
]},<br>
"constraints": null,<br>
"dynamic_types": null,<br>
"dynamic_casts": null,<br>
"constructing_objects": null,<br>
"checker_messages": null<br>
}$5 = void<br>
</div>
<div><br>
</div>
<div><br>
</div>
<div>(gdb) bt<br>
#0 (anonymous
namespace)::SimpleSValBuilder::evalCastFromLoc
(this=0xf9aedf0, val=..., castTy=...) at
../../clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:136<br>
#1 0x0000000007ec6ecb in (anonymous
namespace)::SimpleSValBuilder::dispatchCast
(this=0xf9aedf0, Val=..., CastTy=...) at
../../clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:70<br>
#2 0x0000000007edd75e in
clang::ento::StoreManager::CastRetrievedVal
(this=0xf9b02a0, V=..., R=0xf9b2aa8, castTy=...) at
../../clang/lib/StaticAnalyzer/Core/Store.cpp:438<br>
#3 0x0000000007ea0480 in (anonymous
namespace)::RegionStoreManager::getBinding
(this=0xf9b02a0, B=..., L=..., T=...) at
../../clang/lib/StaticAnalyzer/Core/RegionStore.cpp:1511<br>
#4 0x0000000007e9d059 in (anonymous
namespace)::RegionStoreManager::getBinding
(this=0xf9b02a0, S=0xf9b6fa2, L=..., T=...) at
../../clang/lib/StaticAnalyzer/Core/RegionStore.cpp:551<br>
#5 0x0000000007753856 in
clang::ento::ProgramState::getRawSVal (this=0xf9b81b8,
LV=..., T=...) at
../../clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:785<br>
#6 0x0000000007e64d61 in
clang::ento::ProgramState::getSVal (this=0xf9b81b8,
location=..., T=...) at
../../clang/lib/StaticAnalyzer/Core/ProgramState.cpp:267<br>
#7 0x0000000007df0d77 in
clang::ento::ExprEngine::evalLoad (this=0x7fffffffa828,
Dst=..., NodeEx=0xf985e00, BoundEx=0xf985e00,
Pred=0xf9b8230, state=..., location=..., tag=0x0,
LoadTy=...)<br>
at
../../clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:2982<br>
#8 0x0000000007e10402 in
clang::ento::ExprEngine::VisitCast (this=0x7fffffffa828,
CastE=0xf985e00, Ex=0xf985dc0, Pred=0xf9b8230, Dst=...) at
../../clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp:313<br>
#9 0x0000000007de88a8 in clang::ento::ExprEngine::Visit
(this=0x7fffffffa828, S=0xf985e00, Pred=0xf9b8230,
DstTop=...) at
../../clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:1729<br>
#10 0x0000000007de4d9c in
clang::ento::ExprEngine::ProcessStmt (this=0x7fffffffa828,
currStmt=0xf985e00, Pred=0xf9b8230) at
../../clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:791<br>
#11 0x0000000007de4a89 in
clang::ento::ExprEngine::processCFGElement
(this=0x7fffffffa828, E=..., Pred=0xf9b8230, StmtIdx=1,
Ctx=0x7fffffffa338) at
../../clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:637<br>
#12 0x0000000007db6fa9 in
clang::ento::CoreEngine::HandlePostStmt
(this=0x7fffffffa848, B=0xf9a8860, StmtIdx=1,
Pred=0xf9b8230) at
../../clang/lib/StaticAnalyzer/Core/CoreEngine.cpp:466<br>
#13 0x0000000007db6717 in
clang::ento::CoreEngine::dispatchWorkItem
(this=0x7fffffffa848, Pred=0xf9b8230, Loc=..., WU=...) at
../../clang/lib/StaticAnalyzer/Core/CoreEngine.cpp:191<br>
#14 0x0000000007db6323 in
clang::ento::CoreEngine::ExecuteWorkList
(this=0x7fffffffa848, L=0xf9b16e0, Steps=224975,
InitState=...) at
../../clang/lib/StaticAnalyzer/Core/CoreEngine.cpp:147<br>
#15 0x000000000734dc74 in
clang::ento::ExprEngine::ExecuteWorkList
(this=0x7fffffffa828, L=0xf9b16e0, Steps=225000) at
../../clang/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h:192<br>
</div>
</div>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank"
moz-do-not-send="true">cfe-dev@lists.llvm.org</a><br>
<a
href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>