[cfe-dev] Tackling open project - BitwiseMaskingChecker

[Ryan Govostes via cfe-dev]

I see your point. The checker would not issue any warnings, it can just modify the constraints on the symbolic value that is the result of the expression.


> On 28 Feb 2016, at 21:49, יהודה שפירא <yehudahs at gmail.com> wrote:
> 
> Hi,
> I understand the masking but I didn't understand what scenarios this checker should catch ?
> Should the checker just update the variable masking state  and let other checkers use this masking states ?
> Cause as I understand from the example in bug 16615 <https://llvm.org/bugs/show_bug.cgi?id=16615> we should use the masking state in the "uninitialized value checker" to conclude that it always switch into one of the cases in the example.
> So, does the BitwiseMaskingChecker should warn ? Or just update the state with the relevant mask and let other check use this states ?
> 
> Regards,
> Yehuda.
> 
> On Mon, Feb 22, 2016 at 2:17 AM, Ryan Govostes <rzg at apple.com <mailto:rzg at apple.com>> wrote:
> The BitwiseMaskingChecker described in the document is for a subset of possible bitwise expressions, namely, bitwise AND with a mask of the form 2^n - 1. This is because we can easily reason about the bounds of the result of the operation using the existing range-based constraint manager. That is, if I have x & 0xFFF, you know the result can be any number between 0 and 0xFFF.
> 
> However if the mask is not of the form 2^n - 1, the results do not make a contiguous range, and hence the existing constraint manager can’t reason about it. For instance, for x & 9, the possible values are { 0, 1, 8, 9 }, which is not a contiguous range.
> 
> 
> A more powerful BitwiseConstraintManager would be able to reason about a wider variety of bitwise expressions, probably by tracking constraints on each bit. For instance, it could determine that (x & 0xFFE) & 0x1 will always be zero; this cannot be efficiently proved by using a range-based constraint manager.
> 
> 
> I did implement a SMT-solver-based constraint manager that could handle arbitrary bitwise expressions, but it has not been accepted into mainline Clang. It is also very slow, and there would be huge performance benefits for using specialized constraint managers and leaving the SMT solver as a last-ditch effort.
> 
> Ryan
> 
> 
> 
>> On 20 Feb 2016, at 17:26, יהודה שפירא via cfe-dev <cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>> wrote:
>> 
>> I have been working on the llvm project - more on the backend and I want to get more familiarized with the clang and especially with the static analyzer project.
>> So I want to try and tackle one of the open projects that listed in the site http://clang-analyzer.llvm.org/open_projects.html <http://clang-analyzer.llvm.org/open_projects.html>.
>> I want to start with something simple, and so I was thinking about working on the BitwiseMaskingChecker  (PR16615 <http://llvm.org/bugs/show_bug.cgi?id=16615>) unless you think it not a good start.
>> I understand that bitwise reasoning is missing, but should it be in a checker ? Isn't that suppose to be in the "BitwiseConstraintManager" (another open project in the site above).
>> What am I missing ? What is the purpose of the BitwiseMaskingChecker ? to check what exactly ?
>> 
>> Regards,
>> Yehuda.
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev <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/20160228/06f204ac/attachment.html>