What to do when we must make unsound translational choices? about smack HOT 6 OPEN

Good point Mike.
I would actually like to see something similar even for imprecise choices, such as for example our current implementation of inttoptr. Something like "WARNING: false bugs possible due to inttoptr" or something like that.

from smack.

Mike, I think we are not issuing these warnings, right?
We should then close this one...

from smack.

Ah but we are issuing (some of) these warnings; for instance, here's an excerpt from the "globals" regression:

$bb0:
assume {:sourceloc "globals.c", 8, 18} true;
call $p := $malloc($off($ptr($NULL, 4)));
assume {:sourceloc "globals.c", 8, 18} true;
// WARNING: ignoring bitcast instruction : %"$p1" = bitcast i8* %"$p" to i32*, !dbg !14
$p1 := $p;
assume {:sourceloc "globals.c", 8, 18} true;
// WARNING: ignoring llvm.debug call.
assume true;

However, I'm not sure we should close this issue before doing a more careful review of all places where we might be unsound :-)

M

from smack.

Just a follow-up on this issue: currently we provide warnings when unsoundness occurs.

from smack.

To me it seems that sometimes we print out such warnings into bpl files and sometimes to the console. Is that right?
I think that printing them just into bpl files is not enough. I think we should do both for each warning, where that is feasible.
Thoughts?

from smack.

I tend to agree: the Boogie code we generate should probably be thought of as opaque, and not inspected by any Smack user. Therefore issuing warnings (only) there would not be caught. I am not against leaving comments there in the code also though.

As far as Console warnings go: perhaps it would be good to follow the style of Clang warnings and errors. People tend to find them effective.

Also related: @danielsn was wondering whether we can regularize Smack’s output information, e.g., as JSON. This could include any information currently printed to the console and warnings included in the BPL file. Such a data format would simplify the lives of tools which consume Smack results. I think these unsoundness warnings might be a good place to start with that.

from smack.