[cfe-dev] Unions in the Clang Static Analyzer

[Alexey Sidorin via cfe-dev]

Hi all,

There is one thing that can make the implementation a bit easier :)
The reading of a union field that was not stored last may cause 
undefined behavior. A discussion on this issue can be found on
https://www.securecoding.cert.org/confluence/display/c/EXP39-C.+Do+not+access+a+variable+through+a+pointer+of+an+incompatible+type

I guess we need some language lawyers here. Aaron, can I disturb you?


02.03.2017 20:12, Artem Dergachev via cfe-dev пишет:
> Hello,
>
> I'm not aware of any unfinished work on union support. I'd gladly give 
> a few hints.
>
> RegionStore itself already operates in a union-friendly manner: even 
> though it presents itself as a MemRegion->SVal map, internally it only 
> stores base regions and byte offsets as keys, regardless of how the 
> bytes stored are interpreted.
>
> However, i suspect bigger problems with actually representing symbolic 
> values for fields that are interpreted in multiple ways during the 
> analysis. First of all, reinterpret-casts of basic types are in 
> general modeled poorly. For example, cast from pointer to integer is 
> represented as a special LocAsInteger SVal sub-class, support for 
> which in SValBuilder is worse than for symbols; at the same time cast 
> from integer to pointer is not represented at all, as i mentioned 
> recently in 
> http://lists.llvm.org/pipermail/cfe-dev/2017-February/052769.html .
>
> Then, unions are even more fun because they challenge the concept of 
> SymbolRegionValue, which is a very basic thing. Consider an example:
>
>   union U { intptr_t x; void *p; }
>
>   void foo(union U u) {
>     intptr_t X = u.x; // reg_$0<u.x>
>     void *P = u.p; // &SymRegion{reg_$1<u.p>}
>     if (X == P) { ... }
>   }
>
> The symbolic values for X and P look completely different, the worst 
> thing here probably being that X is NonLoc while P is Loc. Yet, they 
> represent the same thing. How would we unify these values? If you come 
> up with a single symbol to represent them, what would be the type of 
> that symbol? Or would you prefer to constrain these symbols to be 
> equal, and rely on the constraint solver to figure things out?
>
> So making a proper union support is going to be a fun research 
> project. Smaller incremental improvements that fix particular cases 
> you encounter are also very much welcome. There's not necessarily much 
> thought behind the safety-first bail-outs, so if you are seeing 
> significant improvements by removing them, we could consider lifting 
> them; it may also turn out that they're necessary, and an experienced 
> eye may sometimes understand why, but as long as there is no 
> comprehensive explanation in comments and no testcase coverage, i'd 
> rather encourage you to remove them and see what happens; especially 
> considering that you've got access to a good codebase to test these 
> changes upon.
>
>
> 02/03/2017 1:53 AM, Keno Fischer via cfe-dev wrote:
>> I was having some trouble with using the static analyzer on code that 
>> involves unions. Looking through the code, it seems like this is a 
>> known problem and unions aren't particularly well supported. 
>> Personally, I was able to make some progress by just ripping out all 
>> the checks for union types, particularly in RegionStore. However, 
>> that's obviously a hacky solution, so to ensure that my check will 
>> keep working, I'd like to improve upstream support for unions if 
>> possible. Has anybody thought about this problem before/is there 
>> already a design for this? Alternatively, have people collected test 
>> cases that would benefit from improving union support? I'm sure I'm 
>> not the first person to hit this issue, so I'd appreciate any 
>> pointers to prior work.
>>
>>
>> _______________________________________________ cfe-dev mailing list 
>> cfe-dev at lists.llvm.org 
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20170303/4fcc6874/attachment.html>