[LLVMdev] [PATCH] Adding SMACK software verifier specific target to clang that disallows type coercions

[Zvonimir Rakamaric]

This all sounds good Alp, and I appreciate your help.

I can provide your with some background information to give you more context.

SMACK is a software verifier/bug finder, and as all software
verifiers, it balances scalability with precision of its analysis. And
while there are many aspects of this trade-off, here is one simple
example to illustrate one common source of precision loss:
int x = 10;
chat *y = &x;
y++;
*y = 34;
assert x == 10;

SMACK (and many other verifiers) cannot currently handle this example
precisely and would in fact report no error violations. Now, there are
approaches that we could implement to support precisely this and
similar examples (i.e., byte-level accesses), but we would have to
sacrifice performance and scalability. And so designers of tools such
as SMACK always have to draw a line somewhere wrt what to support
precisely and what not.

Which is where type coercion that started this story comes into play,
since it sometimes creates such situations that (currently) cannot be
handled precisely by SMACK.

In particular, the biggest issues is that type coercion creates these
situations even if they are not present in the actual source code. And
that is the real problem. Why? Well, because it thoroughly confuses
our users, who don't use such tricky operations in their code, and yet
those still magically appear due to type coercion.

Finally, as a side note, we also received a report that clang
sometimes transforms regular loops into irreducible ones, which are
again a big problem for software verifiers. And this is an issue along
the lines of what I mentioned before - a user makes sure that all
their loops are not irreducible, but then an irreducible loop appears
out of nowhere, at least from the user's perspective. We haven't
investigated this issue further and into so much details as type
coercion, and so I am not sure how serious it is.

Anyhow, I hope this helps and that it makes sense somewhat. Please do
let me know if you have any further questions or would need help with
anything. We would really like to get to the bottom of this
eventually.

Thanks!

Best,
-- Zvonimir


--
http://zvonimir.info
http://soarlab.org/


On Sat, Jun 7, 2014 at 3:58 PM, Alp Toker <alp at nuanti.com> wrote:
>
> On 04/06/2014 03:16, Zvonimir Rakamaric wrote:
>>
>> Hi,
>>
>> So I created two tiny patches (see attached) for LLVM and clang that
>> allow target triples of the form e.g. x86_64-unknown-smack to be used,
>> which in turn disables various type coercions. Basically, SMACK
>> software verifier that I've been working on is not happy when it
>> encounters type coercions, which are not easy to handle in their full
>> generality.
>
>
> Hi Zvonimir,
>
> I don't have a strong idea of what the right fix should be, but adding SMACK
> as an OS Triple doesn't feel right beyond a quick-fix.
>
> You'll probably want to use your tool for analysing different frontend
> architectures and the proposed approach would make it difficult to specify a
> suitable backend target in an ordinary build system. It also relies on
> what's so far been a changeable implementation detail.
>
> Reid's line of questioning was going well and if we follow to its conclusion
> it seems we'll achieve a more sustainable solution to your problem. Someone
> on the LLVM side should download your tool and get a feel for the
> requirements -- I'll try to find time for that.
>
> This isn't to hold up the idea, rather to make sure we specify it correctly
> because it's in fact a really important use case that we should support
> explicitly in LLVM without tying it to a single tool.
>
> Alp.
>
>
>>
>> Please take a look at the following discussions for background
>> information on why I created these patches:
>> http://lists.cs.uiuc.edu/pipermail/llvmdev/2014-May/072986.html
>> http://lists.cs.uiuc.edu/pipermail/cfe-dev/2014-May/037120.html
>>
>> I tested the patches on both LLVM and clang regressions suites, and
>> they seem to be working fine.
>>
>> Please let me know how to proceed with this.
>>
>> Thanks!
>>
>> Best,
>> -- Zvonimir
>>
>> --
>> http://zvonimir.info
>> http://soarlab.org/
>>
>>
>> _______________________________________________
>> cfe-commits mailing list
>> cfe-commits at cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
>
>
> --
> http://www.nuanti.com
> the browser experts
>