Use abortExecBecause in abort() override

[RyanGlScott]

We wish to abort on concretely false assertions even if assertThenAssume is set to false, as this prevents exploring blatantly unreachable code paths like the unreachable instruction after a call to abort().

Fixes #787.

[RyanGlScott]

It looks like this has an impact on the crux-mir test suite. As far as I can tell, the changes are benign—some counterexamples are no longer being printed due to certain assertion failures aborting more eagerly. I'll update the expected test output momentarily.

[RyanGlScott]

As I've been updating the test suite output for crux-mir, I'm becoming less sure that the changes are desirable. One example of something which changed is the expected error for div_unsigned:

#[inline(never)]
fn div_signed(x: i8, y: i8) -> i8 {
    x / y
}

#[inline(never)]
fn div_unsigned(x: u8, y: u8) -> u8 {
    x / y
}

#[cfg_attr(crux, crux_test)]
fn crux_test() -> u8 {
    let a: i8 = div_signed(1, 1);
    let b: i8 = div_signed(-128, -1);   // Should fail
    let c: i8 = div_signed(-128, -2);
    let d: i8 = div_signed(-127, -1);
    let e: i8 = div_signed(-1, 0);      // Should fail

    let f: u8 = div_unsigned(1, 1);
    let g: u8 = div_unsigned(1, 0);     // Should fail

    (a + b + c + d + e) as u8 + (f + g)
}

pub fn main() {
    println!("{:?}", crux_test());
}

Before this patch, this would produce three counterexamples, one for each // Should fail line above:

---- checked_div/3a1fbbbh::crux_test[0] counterexamples ----
Failure for test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0]
attempt to divide with overflow
Failure for test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0]
attempt to divide by zero
Failure for test/symb_eval/num/checked_div.rs:8:5: 8:10: error: in checked_div/3a1fbbbh::div_unsigned[0]
attempt to divide by zero

After this patch, however, this only produces a single counterexample:

---- checked_div/3a1fbbbh::crux_test[0] counterexamples ----
Failure for test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/3a1fbbbh::div_signed[0]
attempt to divide with overflow

This isn't wrong, strictly speaking, but it does lose the nice property of reporting on all issues in the program at once.

[robdockins]

shrug I'm of the opinion that this is proper behavior, but I suppose others might disagree. My usual stance is that, once a fatal error has occurred, it doesn't make much sense to keep running the program.

[RyanGlScott]

For some reason, the situation in #789 (comment) feels slightly different to me than in the original abort() example. I suppose it's because if you were to comment out abort() in the original example, you'd never encounter the unreachable code error. On the other hand, if you were to comment out the first of the failing div_signed() lines, the subsequent two failures would still occur. In this sense, there is an argument one could make about causality, but I'm not sure how to make it more precise than that.

[robdockins]

Well, even if we decide this isn't the way to fix this, we should ensure that abort() does actually abort execution. Clang inserts the unreachable instruction precisely because abort has the noreturn attribute, so we should respect that attribute.

[RyanGlScott]

I've pushed a more conservative fix which simply uses abortExecBecause in the override for abort(), which accomplishes the same result without affecting other programs (I hope).