"Invalid ELF header" error doesn't print location information

[brianhuffman]

Running the bike_r2 verification from s2n, I got the following error message (due to some C file not being compiled properly, I guess)

[22:21:02.577] Verifying bit_scan_reverse ...
[22:21:02.577] Simulating bit_scan_reverse ...
[22:21:02.715] Checking proof obligations bit_scan_reverse ...
Calling Yices to check sat
Running check sat
[22:21:02.729] Proof succeeded! bit_scan_reverse
[22:21:02.729] Finding symbol for "secure_cmp32"
[22:21:02.737] X86Error "Invalid ELF header"

The problem is that I expected the error message to be printed along with a saw-script call stack and saw-script source location information, but I got none.

Perhaps there is a mismatch of exception types in the x86 verification code compared to the saw-script exception handlers?

[atomb]

This happens because there are various places where the x86 processing code (and other code in SAW) throws exceptions from IO code that are of specific types that we don't currently catch. I'm going to prepare a PR to experiment with adapting the io function in SAWScript.Value to have special processing for each type of exception we specifically want to handle, and then use io in preference to liftIO in most TopLevel code. In preparation for that, I've confirmed that doing so allows us to give a much nicer error message in this case, and we could relatively easily extend that to handle other exceptions, too.