Standard library not linked in single file compilation

[adpaco-aws]

The number of verification failures in the dashboard increased significantly this week. The most common reason is this single failure:

function _ZN3std2io5stdio6_print17h8a4943aaa5dd417dE
[_ZN3std2io5stdio6_print17h8a4943aaa5dd417dE.assertion.1] assertion false: FAILURE

We are now failing to verify any example with print macros on it. This is due to the changes in #535 and the fact that the standard library is not linked in during single file compilation.

[adpaco-aws]

#602 has been resolved and work on this has been resumed. Unfortunately, this does not work out of the box.

Now I am trying to include std-<hash>.symtab.json.out into the goto-cc command we use for linking.

The problem is that, even if that works, the name of the function appears not to be the same. For example, if I take a look into the goto functions I can find a call to _ZN3std2io5stdio6_print17hda093ea5ce7aa05bE in the example file, but this function cannot be found in the std file.

The problem may be that the version built using Z build-std is different from the one expected in the examples.

[adpaco-aws]

Yesterday I was able to link in the standard library in a small piece of code which just prints a value.

I did so by setting up a library project, using a public function named "public" in lib.rs and adding the #[no_mangle] directive to it. The project can be found in this repository (it will be deleted at a later time).

However, when I run CBMC in the link-std.sh script, I got an unwinding failure if I did not unwind. I tried using --unwind 2 which gets me no verification result and the following error:

aborting path on assume(false) at file /home/ubuntu/rmc-dash/library/alloc/src/alloc.rs line 170 column 27 function alloc_crate::alloc::Global::alloc_impl thread 0
aborting path on assume(false) at file /home/ubuntu/rmc-dash/library/alloc/src/alloc.rs line 318 column 11 function alloc_crate::alloc::exchange_malloc thread 0
Unwinding loop _ZN4core3ptr74drop_in_place$LT$core..option..Option$LT$std..process..ChildStdout$GT$$GT$17h47ed3623eb2c786aE.0 iteration 1  thread 0
aborting path on assume(false) at  thread 0
Not unwinding recursion sys::unix::thread::Thread::new::thread_start iteration 3
l2_rename_rvalues case `address_of' not handled

I believe this is due to an incomplete code generation on our end, but this is the first time I am seeing this message so I am not sure.

[adpaco-aws]

@danielsn pointed out this is a CBMC unwinding issue (case not handled here)

[zhassan-aws]

@adpaco-aws the print issue has been addressed in #825. Should we keep this issue open?

[zhassan-aws]

Document this limitation and change "bug" label to "feature".

[zhassan-aws]

Relevant discussion: #576 (comment)

[celinval]

This has been fixed as part of the MIR Linker work. #1588