Viewer support for RMC output

[markrtuttle]

Here are the issues that need to be solved for viewer to begin running on rmc output.

Source locations are missing: Look at a trace in the xml output of property checking (eg, cbmc --traces --xml-ui) on an rmc goto binary and you will find many empty source locations <location/> instead of the usual <location file= .../> and many steps omit the location tag altogether.

Source location use physical path names: The source locations in rmc goto binary (eg, cbmc --show-symbol-table foo.goto) are physical path names like /local/home/mrtuttle and not logical path names /home/mrtuttle. Until this is fixed, because variables like $HOME are typically logical and not physical, viewer needs to be invoked with --srcdir $(realpath $SRCDIR) and --wkdir $(realpath .).

Source locations are missing the working directory: The working directory is the directory in which the compiler was invoked. Viewer assumes that all relative path names like harness.c in source locations are relative to the working directory. If you look at the xml output of property checking, you can see both

<location file="&lt;builtin-library-malloc&gt;" function="malloc" line="45" working-directory="/local/home/mrtuttle/rmc/rust-tests/cbmc-reg/SizeAndAlignOfDst"/>

and

<location column="41" file="main_fail.rs" function="main" line="39"/>

Symbol names contain new characters: Mangled function names contain characters :: and $ that do not appear in the names of symbols in C. Unfortunately, we can't just extend the language of symbols to include them, because CBMC uses :: in the scoping of local symbols like main::1::2::x and parsing this correctly to get the symbol x requires knowing that :: is a separator. At some point we hope to move to the new name mangler that will unmangle to human-readable names, but then the names will include :: as part of the pretty name.

When I temporarily patch these things, viewer will produce a report for an rmc goto binary.

For debugging purposes, the current sequence of steps for running viewer on rmc output is

LIB=$(RMC)/library/rmc/rmc_lib.c

rmc --keep-temps $(HARNESS).rs
goto-cc --function main $(HARNESS).goto -o $(HARNESS)2.goto
cbmc --xml-ui --trace $(LIB) $(HARNESS)2.goto > results.xml
cbmc --xml-ui --cover location $(LIB) $(HARNESS)2.goto > coverage.xml
cbmc --xml-ui --show-properties $(LIB) $(HARNESS)2.goto > property.xml
cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir $(SRCDIR) --wkdir . --goto $(HARNESS)2.goto 

[markrtuttle]

Concerning "Source locations are missing the working directory," an easy work around would be for the rmc code inserting source locations to expand the filenames to absolute pathnames. Then there would be no need for viewer to use the missing working directory. Just to be consistent with other source locations, they should probably be physical paths and not logical. Could the code inserting into symbol tables also ensure that the source locations in symbol tables use absolute and physical paths?

[markrtuttle]

I think that using absolute logical path names is essential (or figuring out how to add working-directory). The reachable function computation by goto-analyzer is producing incorrect filenames for source locations with relative pathnames and missing working-directory.

goto-analyzer --reachable-functions main_fail.goto  --function main  | grep main

includes

/main_fail.rs main 38 38
/main_fail.rs _ZN9main_fail15DummySubscriber3new17h90935f886e767e4aE 23 24
main_fail::alloc4_init

Among other things, this makes filtering coverage data with reachable functions impossible to do in a principled fashion.

[markrtuttle]

This is partially resolved by #142