What to do when we must make unsound translational choices?

[michael-emmi]

e.g. when we encounter an inline assembly call.

One idea would be to have a warning system: generate the Boogie code, and signal to the user that certain code is unsound. This could even be as simple as "WARNING" comments in the generated Boogie code.

[zvonimir]

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.

[zvonimir]

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

[michael-emmi]

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

[shaobo-he]

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

[zvonimir]

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?

[michael-emmi]

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.