[WIP] Optionally model the LLVM assume statement in Boogie

[keram88]

Currently we don't do anything with LLVM's assume statement. This is because we
need to be sure that the assumption provided to the function is correct. At best
it might help with verification, but it could also lead SMACK to report erroneous
bugs (or no bugs!). For now, this removes this intrinsic, preventing a warning about an unsound
call to this function.

I could add the closure in the stmtMap, but I think it's valuable to have the rationale somewhere in this function.

[keram88]

My primary impetus to add this is that Rust generates these in just about every program.

[shaobo-he]

LGTM.

[keram88]

Travis is failing this because of clang-format failing something in lib/smack/Regions.cpp. As far as I can tell the failing code is removed in LLVM 7.1. Regardless, this PR is unrelated to this file, and all regressions pass.

Perhaps we should merge this after LLVM 7.1 lands.

[michael-emmi]

I’m curious about knowing more; is there a reference on this?

Overall, I wonder whether it might instead be a good idea to take advantage of these assumptions by modeling them as boogie assumes. Depending on why they’re added. For instance, if they correspond to things the rust type checker has already proven, then why not use them?

[keram88]

@michael-emmi That's a good point, I should have discussed how Rust uses this function.

Rust doesn't appear to do anything interesting with llvm.assume. In all the Rust benchmarks, the uses of llvm.assume follow this pattern:

i1 x = (some boolean expression);
llvm.assume(x <= 1);

Basically, Rust is telling LLVM its booleans are 0 or 1, but LLVM should know this since their type is i1.

The strongest thing I think Rust has ever done with respect to its type-system is add the noalias attribute to function arguments. This issue goes into more detail about some of the problems with this: rust-lang/rust#53105.

Another approach is to make generating Boogie assumptions opt-in or opt-out through a command line argument. Something like --use-llvm-assume or --no-llvm-assume. @shaobo-he @zvonimir What do you think about this?

We should update #53 regardless.

[shaobo-he]

@michael-emmi That's a good point, I should have discussed how Rust uses this function.

Rust doesn't appear to do anything interesting with llvm.assume. In all the Rust benchmarks, the uses of llvm.assume follow this pattern:

i1 x = (some boolean expression);
llvm.assume(x <= 1);

Basically, Rust is telling LLVM its booleans are 0 or 1, but LLVM should know this since their type is i1.

The strongest thing I think Rust has ever done with respect to its type-system is add the noalias attribute to function arguments. This issue goes into more detail about some of the problems with this: rust-lang/rust#53105.

Another approach is to make generating Boogie assumptions opt-in or opt-out through a command line argument. Something like --use-llvm-assume or --no-llvm-assume. @shaobo-he @zvonimir What do you think about this?

We should update #53 regardless.

I think without evident benefits of leveraging the LLVM assume intrinsic, the current PR is the better option.

[zvonimir]

Please fix formatting so that CI is passing. It is an easy fix. Also, please address this compilation warning if possible:

../lib/smack/SmackInstGenerator.cpp:896:31: warning: lambda capture 'this' is not used [-Wunused-lambda-capture]
1984  static const auto assume = [this](CallInst *ci) { return; };

[zvonimir]

I see. Formatting got broken elsewhere. I'll fix it. You still have to take care of the warning though.

[michael-emmi]

Could we at least understand whether the assumes here represent facts that have been “proven” by previous analysis, or whether e.g., they represent speculative optimization hints that may be invalidated and require unoptimized fallback?

[zvonimir]

From the LLVM language spec (https://llvm.org/docs/LangRef.html#llvm-assume-intrinsic):

The llvm.assume allows the optimizer to assume that the provided condition is true. This information can then be used in simplifying other parts of the code.

and also

If the condition is violated during execution, the behavior is undefined.

So to me it seems that the purpose of assume intrinsics is to provide "proven" facts.

I think we should ultimately have a command line switch --leverage-llvm-assumes that turns on using them for verification, and we drop them otherwise. Then we can experiment with this more.

[keram88]

From https://llvm.org/docs/LangRef.html#llvm-assume-intrinsic:

The intrinsic allows the optimizer to assume that the provided condition is
always true whenever the control flow reaches the intrinsic call. No code is
generated for this intrinsic, and instructions that contribute only to the
provided condition are not used for code generation. If the condition is
violated during execution, the behavior is undefined.

Note that the optimizer might limit the transformations performed on values used
by the llvm.assume intrinsic in order to preserve the instructions only used to
form the intrinsic’s input argument. This might prove undesirable if the extra
information provided by the llvm.assume intrinsic does not cause sufficient
overall improvement in code quality. For this reason, llvm.assume should not be
used to document basic mathematical invariants that the optimizer can otherwise
deduce or facts that are of little use to the optimizer.

Could we at least understand whether the assumes here represent facts that have been “proven” by previous analysis, or whether e.g., they represent speculative optimization hints that may be invalidated and require unoptimized fallback?

LLVM appears to treat these as axioms, so it won't generate any code to handle an invalid assumption.

I think the uses of llvm.assume by Rust I gave earlier are of the kind that LLVM says not to generate, but this doesn't affect the correctness of SMACK. One of the most powerful uses of the assume statement is documentation of loop invariants from the compiler. LLVM probably can't discover these facts due to the loss of semantic information. This information is likely very helpful for SMACK.

I'm starting to fall on the side of generating boogie assumes for these; they can't hurt verification time and might help. My biggest concern is that the compiler will generate an assume which is false. However, we already assume that the compiler reasonably transforms the source. If erroneous assumes were being routinely generated, then incorrect optimizations in LLVM would occur and compiler bugs would be reported. My other consideration is that the compiler provides a correct assumption, but an undefined behavior invalidates it. I'm not too worried about this because the program is already ill-formed, and SMACK has an expanding set of checks for undefined behaviors to help diagnose this.

[keram88]

So to me it seems that the purpose of assume intrinsics is to provide "proven" facts.

I think we should ultimately have a command line switch --leverage-llvm-assumes that turns on using them for verification, and we drop them otherwise. Then we can experiment with this more.

This seems reasonable. We should try generating assumes to see how they behave before enabling or disabling them generally. I want to update this PR with your proposal.

[michael-emmi]

Yea, I agree that experimenting with whether these generated llvm.assumes provide useful information to the verifier is the right thing to do. My hunch would also be that they could help significantly, e.g., if they carried higher-level program invariants from, e.g., rustc to LLVM.

One small note: it’s not obvious to me that additional assumes “can’t hurt verification time”, but perhaps that is another conversation altogether :-)

[keram88]

One small note: it’s not obvious to me that additional assumes “can’t hurt verification time”, but perhaps that is another conversation altogether :-)

This is worth investigating. I know some of our floating-point axioms slowed down verification. Solvers are complex beasts and it's hard to know what hurts or helps.

[keram88]

I implemented Zvonimir's suggestion. I witnessed one interesting case along the lines of this (translated from Rust):

int x = __VERIFIER_nondet_int();
int y = 2*x;
...
int z = y&1;
...
// @llvm.assume(z == 0);
__VERIFIER_assert(z == 0);

SMACK is able to verify this with --leverage-llvm-assumes despite --bit-precise being off; without --bit-precice, z would be nondet and the assertion would fail.

Rust also generates some useful assume statements, namely it states that its pointers are not null.

[keram88]

What do you think of also adding a "strict" assume mode? Clang has __builtin_assume:
https://clang.llvm.org/docs/LanguageExtensions.html#builtin-assume
This seems to always emit an @llvm.assume statement. We could emit an assert to check that the assumption always holds.

[zvonimir]

I see. So there should be a command line argument with 3 options: ignore assumes, assume assumes, and assert assumes. I like that. Please add the assert assumes option as well then. Good suggestion.

[zvonimir]

Also, could you create a regression that checks for this?

[zvonimir]

@keram88 : What's the status of this pull request? Any chance you could finish it this week?

[keram88]

I have implemented the following:

• --llvm-assumes=none: This ignores LLVM assume statements as SMACK currently does, and is the default behavior.
• --llvm-assumes=use: This uses LLVM assumes as boogie assumes.
• --llvm-assumes=check: This uses LLVM assumes and additionally checks their validity.

I added the regressions here: https://github.com/smackers/smack/tree/no-warn-assume/test/special.
I wasn't sure where to put them since they are kind of weird tests. I think it covers the range of odd behaviors that could be verified using __builtin_assume, such as confirming that 1=0.

But as I found in Rust, using the assumes generated by the compiler could help us avoid running bit-precise.

[keram88]

I addressed @zvonimir's comments. I don't like force pushing, so if this looks good, I can squash the commits.

[zvonimir]

Looks good to me. Please squash and clean up your commits and then I'll merge it.

[keram88]

Done. Thanks, @michael-emmi for driving this toward what I think is a much better solution.