[cfe-dev] Tackling open project - BitwiseMaskingChecker

[Ryan Govostes via cfe-dev]

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> 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
> 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/20160222/dca4a281/attachment.html>