Do you know how deeply LLVM can go in evaluating the constraints? That is, if there is deeply nested call graph, each of which has its own constraints (pre, post, and during), can LLVM evaluate and use that information?
I believe it's mostly a matter of what function get inlined but I'm not an LLVM expert so I won't say so conclusively.
FWIW, it sounds like you're mostly interested in using this data to drive optimizations which (IMO) doesn't require an RFC at all since there's no changes to program or language semantics. This also doesn't require new keywords or macros. It's "just" a matter of writing the optimizations.
Actually, I am proposing a new keyword... or at least, making room for one. assert_constraint!() and try_constraint!() will become reserved macro names, with well-known semantics. ONLY Rust will be permitted to define those macros; attempts to define new macros with the same names will be a hard compiler error. This is the part that needs the RFC right now.
Yes, but my point was that if the motivation for this is smarter optimizations, then we don't need new keywords or macros. assert!() and friends will work just fine.
Yes, the motivation for this proposal is for better optimizations.
That said, I'm trying to think of an example where a keyword would be required instead of a macro; the only thing that I can think of is that keywords can be used in places where a macro can't, e.g. the following doesn't work in rust currently:
assert!(true);
struct Foo;
fn main() {
println!("This file doesn't compile.");
}
Having a keyword that looks like a macro would allow us to put the constraints anywhere we want. I'm still trying to figure out a use for it that can't be covered by attributes and a new compiler pass that emits assert!() in the same way as I suggested for assert_constraint!().
Close, but not quite. The issue is that is static assertions operate on constants only, similar to the constant generics that @mankinskin mentioned earlier. Imagine something like the following (doesn't work today):
assert_constraint!(Foo::a != Bar::b);
pub struct Foo{
a: u8,
}
pub struct Bar {
b: u8
}
pub fn baz(alpha: &Foo, beta: &Bar) {
assert!(alpha::a == beta::b);
}
We can bikeshed what goes into assert_constraint!(), but it should be obvious that this isn't a constant expression. This requires some amount of compile time evaluation (e.g., baz() will always fail, and we can prove this at compile time), or insertion of ordinary assert!() statements in every location that Foo and Bar are instantiated.
1 Like
This looks like multiple things to me. What I understand is,
- for one, you want global assertions, which should always hold, not just when they are encountered in the scope of a function, and should be definable for types rather than values of types.
- Then you want those assertions to be SAT checked at compile time to see if they are satisfiable, and throw compiler errors if they contradict each other, for example
Foo::a != Foo::bandFoo::a == Foo::b. - Then these constraints should also be checked for regular run-time expressions, and throw a compile error (or warning) when a run-time expression will definitely panic because of the knowledge we have from the constraints, i.e, an
assert!(foo.a == bar.b)will always fail if we definedFoo::a != Foo::b
Yes to all of your statements, with the following bullet point:
- If the compiler can't prove something at compile time (or runs out of time trying to do the proof, and needs to give up), then it emits runtime code to do the check.
In general, what I'm after is a way of communicating constraints to the compiler that isn't limited by being a macro (even though it'd just be a macro today). I don't expect to be able to use assert_constraint!() in item position today, or even tomorrow. It might not happen for many, many releases in the future. However, I want the option to be available in the future if we decide it's a good idea. My form of future compatibility is a simple macro, with a significant amount of documentation around it explaining what may happen with it in the future (e.g., my earlier code example suddenly becomes valid Rust), and the ironclad requirement that only the compiler may define assert_constraint!() or try_constraint!(). I think that will give us the greatest flexibility possible.
3 Likes
For me, that is the critical rationale for why it cannot be a macro that some programmer could redefine. @ckaran has made that point repeatedly in this thread. IMO the other issue that reuse of the existing assert!() does not handle as gracefully is the try variant: try_constraint!().
1 Like
Please don't add a SAT solver to rustc. It will make compilation times absolutely terrible.
1 Like
This will make many changes to rustc break compilation, which is against the stability guarantee. Basically it would lock us to a specific implementation even when it could be made more precise. It would also make tiny changes to the mir construction snowball into compilation errors. Lastly it would make any changes to any libstd function a breaking change as it may cause the compiler to be able to find that an assertion doesn't hold.
1 Like
Yes and no. Earlier I mentioned a way around this impasse; additional compiler switches that specify how much effort/time the compiler should spend in executing a SAT solver. We can bikeshed which switches are used, but they would all work to limit the amount of time the SAT solver could spend during compilation. Once the time is up, all further constraints are just emitted as runtime code, which are compiled as normal.
Which changes? How precisely will things be broken? Which compilation guarantees get broken? If the end user never uses assert_constraint!() or try_constraint!(), then how will they break stability?
I'm not sure if I follow what you're saying here. Do you mean it will prevent us from using attributes, or something similar? I think it will actually do the opposite; derive macros will be able to emit assert_constraint!() as needed, hiding it from end users.
Can you give me an example?
That's actually part of the point; libcore and libstd would be annotated with assert_constraint!(), making it possible to check for errors in usage that weren't possible before. As we add more and more constraints to the library, the number of errors that can occur reduce. If your code no longer compiles because it fails a constraint, then that is a good thing; it means that a potential runtime error was caught at compile time, giving you a chance to fix it before it made it into production.
Honestly, your last statement is a major selling point for me because not having to debug customer code at 2 AM (while they are yelling at me that it's all my fault) is something I want more of, not less!
assert_constraint!() will be included in the stability guarantee.
I mean that we can't make any changes to the implementation of the compilation pass that checks if assert_constraint!() should give an error or not.
This will depend on the exact implementation of the checking pass.
The stability guarantee of rust means that only bugfixes in the compiler/standard library are allowed to break things. Adding assert_constraint!() to existing functions in the standard library is a breaking change for some code, so it is not allowed. In addition if assert_constraint!() is allowed to look into function bodies to proof that a constraint doesn't hold (I don't know if you propose this), then any change to the function body may cause it to proof that the constraint doesn't hold. Even if the change was a non-functional refactoring. It doesn't matter that the code would previously panic in some circumstances. What matters is that the code doesn't have memory safety issues.
What you want is likely best left to a separate static verifier like Prusti.
That is true. The breaking change is that if assert_constraint!() or try_constraint!() are already used somewhere, then that code will break. That's why this has to wait for an RFC and an edition boundary. That said, since it is just an addition to rust, rather than a modification of behavior that everyone already depends on, I don't see this as a big deal.
I'm sorry, I really don't understand this statement. At a very high level, the pass that does this check will do one of the following:
- Prove the constraint is violated, and emit a compiler error.
- Prove the constraint is never violated, and remove the
assert_contraint!()entirely, while at the same time providing information to the optimizer so that it can further optimize the code - Be unable to prove anything, so emit code to check the condition at runtime.
My guess is that this part of the compiler is going to have some of the most significant changes, updates, and improvements for many years to come.
The first line of your statement means that the rest of the statement doesn't hold. assert_constraint!() tells the compiler what conditions must be true; if those conditions are false, then they are bugs. The fact that some statements are permitted by the language or library, but are actually incorrect usages, doesn't change the fact that they are bugs. The only thing that changes is that we're better able to detect the bugs.
No.
Consider the humble i8::checked_add method:
pub fn checked_add(self, rhs: i8) -> Option<i8>
Imagine that you have large arrays of i8, like you might have for a simulator. For some reason, the values in the arrays are always less than 10, and your offsets are always in the range [0, 10], inclusive. In that case, which is more efficient below, a or b?
fn a(array: &mut[u8], offset: u8) {
for index in 1..array.len() {
array[index] = array[index].checked_add(offset).expect("Overflowed!");
}
}
fn b(array: &mut[u8], offset: u8) {
assert_constraint!(offset >= 0 && offset <= 10, "Offsets MUST be in the range [0, 10], inclusive!");
assert_constraint!(for v in array.iter() {v < 10}, "All values in the array MUST be < 10!");
for index in 1..array.len() {
array[index] += offset;
}
}
In function a, you will always pay the price for checking for overflow. In function b, there is a chance that the checker and optimizer will be able to determine if the statements are true, removing the constraint checks entirely and leaving a faster loop behind.
Prusti, and other external static analyzers would be able to verify the constraints, but they can't emit optimized code! Only the compiler can do that. That is why this must be in rust and rustc itself.
1 Like
The thing is that any change to the pass may end up proving additional constraints, which would end up in a compilation error. This is a breaking change.
There is a difference between a compiler incorrectly accepting something that causes a memory safety issue or the standard library giving incorrect results and the compiler incorrectly accepting something that causes a safe panic at runtime.
A regular assert! would work just as effective. LLVM already uses panics resulting from assert! to prove certain things to be impossible. For example if you assert the length of a slice once, it will often be able to remove bound checks. Also to tell the optimizer about the proven constraint you will probably have to use something like a panic or assume in it's place.
By the way your example doesn't get optimized even when using assume:
#![feature(core_intrinsics)]
pub fn example(array: &mut[u8], offset: u8) {
unsafe { std::intrinsics::assume(offset >= 0 && offset <= 10); }
for &v in array.iter() {
unsafe { std::intrinsics::assume(v < 10); }
}
for index in 1..array.len() {
array[index] = array[index].checked_add(offset).expect("checked add failed");
}
}
will still have a checked add failed panic message in release mode.
OK, now I get what you're saying. Yes, from this point of view, it is a breaking change because the panic is caught at compile time rather than runtime. Would the following work?
#![cfg(evaluate_constraints_at_compile_time = "true")]
fn b(array: &mut[u8], offset: u8) {
assert_constraint!(offset >= 0 && offset <= 10, "Offsets MUST be in the range [0, 10], inclusive!");
assert_constraint!(for v in array.iter() {v < 10}, "All values in the array MUST be < 10!");
for index in 1..array.len() {
array[index] += offset;
}
}
Assuming I didn't make any typos, that would allow users to opt into the SMT solver by setting -Z evaluate_constraints_at_compile_time = "true", or something similar. If the standard library had this everywhere, then I think it would solve the issue.
That just means that the optimizer isn't yet smart enough. If this proposal were accepted, then this would be something that would be added in (eventually, maybe... depends on how important it is to someone to write it in! 
)
You could certainly add some amount of attributes as macros that sometimes insert additional unsafe assumptions by checking them with a mechanical solver of some sort. This actually sounds very interesting, for example if something like WUFFS could be done as pure macro annotations. Or that additional optimizations could be pulled in as a crate dependency (this removing some burden on rustc to provide them all). However, that still seems like poor motivation for compiler integration per-se. Many of these techniques could be performed with standard proc-macros, no? Have you researched this possibility? If there are demonstrable performance incentives then that might be a much better motivation for the increased compiler surface.
That's genius, I love it!
Forgive me if this sounds peevish, but have you read the entire thread to this point? Starting about here, you'll see why I'm pushing so hard on this; while today these are macros, tomorrow assert_constraint!() and try_constraint!() could become keywords. That would allow both of them to be used in places where macros aren't allowed.