<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Ideally we should implement things according to the standard,
producing an UndefinedVal() every time the value is undefined. This
will also force us to teach our uninitialized value checkers to
understand why the value is uninitialized.<br>
<br>
However this approach would prevent us from making union-specific
undefined values an opt-in thing. And i believe that we might
eventually want that because not all developers are worried about
undefined behavior; there might be codebases in which it is normal
to believe that on a specific platform type-punning is always going
to happen, even in C++.<br>
<br>
So i guess we'll have to stick to believing in type punning as much
as possible and never produce UndefinedVal()s in ExprEngine but let
union-specific checkers decide if we want to emit warnings on any of
those.<br>
<br>
---<br>
<br>
When it comes to representing symbolic values loaded from union
fields (the problem explained as
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/pipermail/cfe-dev/2017-March/052881.html">http://lists.llvm.org/pipermail/cfe-dev/2017-March/052881.html</a>) i
don't know how exactly do i want to represent them, but i would
imagine producing a new sort of symbol (let's call it
"SymbolUnionValue") that has the following as its identity:<br>
<br>
- MemRegion of the union.<br>
- Unsigned integer type of the same size as the read.<br>
<br>
Then the read can be represented as the result of a cast from the
value to the actual read type. This way we'd discriminate between
reads of different size but we'll know that reads of the same size
would produce the same value up to casts. This reduces the problem
to the problem of representing casts (which will likely be your
second problem). Derived symbols would need to be handled similarly
(dunno how to call the corresponding derived union symbols). It is
safe to assume that every read can be represented as an integer read
of a certain type because otherwise we can always return a
LazyCompoundValue that doesn't have any identity problems whatsoever
(because it doesn't promise anything) or an UnknownVal for types
that aren't supported anyway (like floats). If you enjoy the idea of
using our experimental Z3 refutation, it shouldn't be hard to teach
a clever solver how exactly reads of different sizes are related to
each other, but our usual RangeConstraintManager wouldn't be able to
reason about this stuff anyway, you shouldn't bother.<br>
<br>
Supporting loads/stores of concrete values should be straightforward
but may still need some work.<br>
<br>
<div class="moz-cite-prefix">On 8/19/18 5:52 PM, Keno Fischer wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CABV8kRyoo3-4kOHSkD23PeU9JnYOHhSy4X+Aq5cUkSQfxNm7XA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">Sorry for bumping an old thread, but I ended up
trying to pick up the project that brought this up again after
<div>giving up last year because of the analyzer's lacking union
support. Naturally I ran into the same problems again :/.</div>
<div>It seems like the first step here is to decide what model
of unions the analyzer intends to support. I'd be</div>
<div>happy to try fix some things here, but of course those
decisions need to be made first.</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Fri, Mar 3, 2017 at 2:12 AM, Aaron
Ballman <span dir="ltr"><<a
href="mailto:aaron@aaronballman.com" target="_blank"
moz-do-not-send="true">aaron@aaronballman.com</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="HOEnZb">
<div class="h5">On Thu, Mar 2, 2017 at 8:54 PM, Keno
Fischer <<a href="mailto:keno@juliacomputing.com"
moz-do-not-send="true">keno@juliacomputing.com</a>>
wrote:<br>
> This behavior also differs between C and C++. For
example, C has explicitly:<br>
><br>
> [N1570, Footnote 95]<br>
> If the member used to read the contents of a union
object is not the<br>
> same as the member last used to store a value in
the object, the<br>
> appropriate part of the object representation of
the value is<br>
> reinterpreted as an object representation in the
new type as described<br>
> in 6.2.6 (a process sometimes called ‘‘type
punning’’). This might be<br>
> a trap representation.<br>
><br>
> where object representation is essentially what
you'd get if you<br>
> memcpyed the value.<br>
<br>
</div>
</div>
Yes, if everything lines up just perfectly, then in C this
may be<br>
okay. I say may because it can still be a trap
representation, it<br>
could be a misaligned access, there could be unspecified
values within<br>
the union member, etc (so it depends on the types and the
specific<br>
values), so it is *not* strictly a safe operation to do in C
either.<br>
<span class="HOEnZb"><font color="#888888"><br>
~Aaron<br>
</font></span></blockquote>
</div>
<br>
</div>
</blockquote>
<br>
</body>
</html>