search

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
79 stars 14 forks source link

Charon does not generate any output if there is an internal compiler error #401

Open sonmarcho opened 1 day ago

sonmarcho commented 1 day ago

Charon does not generate any output if there is an internal compiler error, even though it actually manages to recover from those errors. Also, I note that if I copy this code to move it here then Charon outputs the serialized file. Maybe this is the solution?...

Nadrieril commented 1 day ago

Does it output something with --errors-as-warnings in the case you're testing?

Nadrieril commented 1 day ago

Said differently, this is charon working as intended: in my mind, calling charon by itself should only produce a well-formed output. --errors-as-warnings is the flag that allows it to produce an output that may be missing some items.

That said, things have changed and a few other options can make the output contain missing items (e.g. --hide-marker-traits or --exclude) so I'm thinking we may simply set --errors-as-warnings to be the default and always emit an llbc file.

sonmarcho commented 10 hours ago

Does it output something with --errors-as-warnings in the case you're testing?

No that's the issue: in case there is a rustc internal error it doesn't output anything, even in the presence of--errors-as-warnings (which is actually expected, because --errors-as-warnings simply changes the way the Charon errors are reported - it doesn't have any effects on rustc's own errors).

Nadrieril commented 10 hours ago

Hm I see. I presume what happens is that when we catch_unwind a compiler panic, this still eventually causes run_compiler to panic because the compiler remembers that it panicked.

In fact the export code used to be where you point to, I moved it because I wanted as little code as possible to be run within the compiler callbacks. Maybe I should just restore the catch_unwind around the compiler invocation that I removed in https://github.com/AeneasVerif/charon/pull/362.

sonmarcho commented 10 hours ago

Actually putting the code there where you put it perfectly makes sense to me: the only issue is that I don't think we can control those internal rustc errors (unless we manage to get rid of all of them of course ^^').