Make assert information more precise

[N1ark]

(waiting for a review before taking care of Aeneas / Eurydice)

As mentioned in #1000, relying on reconstruct_fallible_operations is risky and error-prone. However not having this pass enabled currently provided too little information to provide satisfactory user feedback for assertion failures.

We first translate the message associated with each MIR assert, to allow tools to explain what a failed assert may correspond to. This will also allow us to detect what asserts correspond to fallible operations.

Next we translate terminator asserts from MIR into a new TerminatorKind::Assert. We also remove on_failure from Assert; instead, StatementKind::Assert is now { assert: Assert, on_failure: AbortKind }, and TerminatorKind::Assert is now { assert: Assert, target, on_unwind }.

Currently, we initially only translate StatementKind::Assert for the Assume non-diverging intrinsic; later passes then may lower a TerminatorKind::Assert into a StatementKind, e.g. for dynamic checks if --reconstruct-fallible-operations is set.

This mostly closes #868! The last couple cases where we lose edges right now is when converting calls to the language items panic, panic_fmt, begin_panic or to the functions core::panicking::assert_failed and core::panicking::panic_explicit into a TerminatorKind::Abort(AbortKind::Panic). The same happens in inline_local_panic_functions.rs. These function calls have an unwind edge, that is needed e.g. to drop any remaining locals after starting the panic. An option is adding an optional on_unwind to TerminatorKind::Abort.

Small sidenote but I also find it weird we always convert some of these function calls to aborts in translate_bodies; supposedly this should be done as a micro-pass along with inline_local_panic_functions.rs if a specific flag is set (something like --simplify-panics). Technically the only 'magic' associated with panics should be in __rust_start_panic

ci: use AeneasVerif/aeneas#745
ci: use AeneasVerif/eurydice#376

[Nadrieril]

Yeah, Abort should have an unwind edge actually. I'm really not sure that this particular reconstruction we're doing here is useful honestly, this is just a function call that can be caught by tools.

[Nadrieril]

Let's keep it for now, Abort is a useful primitive for when we'll turn Assert into a plain if.

[Nadrieril]

Hm, having assert at all felt like a hack because it's a glorified if. Having it both as a statement and a terminator feels even less motivated. Long-term I'd like to remove both and just use if instead honestly. Not asking you to do this here tho.

[Nadrieril]

Big fan of BuiltinAssertKind, this will make reconstruction more robust. Overall like the shape of this but we shouldn't be changing the llbc output too much yet. I will want to remove ullbc::StatementKind::Assert eventually; you may find this commit instructive xp

[N1ark]

sounds good! and yeah agreed having both StatementKind::Assert and TerminatorKind::Assert is not ideal ^^' fixed your comments, should be ready to merge

edit: forgot about aeneas and eurydice :P will do these tomorrow

[N1ark]

Eurydice and Aeneas are ready :)

[N1ark]

oops, rebased