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

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.

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