Allow static attribute to be stripped from symbols

[karkhaz]

This PR is intended to help users that want to write CBMC proofs for individual functions. The typical way to do this is to write a 'harness' in a different file, which calls the function under test with unconstrained values. However, CBMC cannot see the definition of that function if it is marked static (in the C language. static in Java means something else). We would like to enable writing harnesses even for static functions, or functions that call static functions.

There are two issues solved in this PR.

1. goto-cc removes symbols from the symbol table if it determines that those symbols are not externally visible. This PR adds the --keep-implementations flag to goto-cc, which prevents it from removing those symbols from the symbol table.
2. Symbols naming functions defined as static have the file_local flag set. This PR adds the --strip-static flag to goto-instrument, which unsets the file_local flag on all symbols whose name is given as an argument.

So the intended workflow is: compile the file under test with goto-cc, passing in a list of functions that should be exposed. Then pass that same list of functions to goto-instrument so that it can unset the flag. This goto binary can then be successfully linked with a harness that calls the static function.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 82a83e6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105034698

[martin-cs]

On Tue, 2019-03-26 at 07:14 -0700, Kareem Khazem wrote: Thanks for all these comments. I'll need a few days to get this done. I am in two minds about using an existing GCC option. Those options are obviously very appropriate. However, people may already have that option set in their existing build system, so adding behaviour to goto-cc that uses of that flag might break something...however, I am still inclined to use those flags, thanks for the suggestion.

I think you are right in that we should only use the gcc flags if we do exactly the same thing.

Just to be clear, I wasn't proposing to make the C front-end disregard `static` entirely, I think it's better to export particular functions that the user requests only.

OK. I'm just not immediately seeing the need for only exporting some. Exporting all; you've convinced me of the use-case. Some ... I remain open minded and it seems like extra hassle if there isn't a use-case.

I'll implement name-mangling (and everything else) in goto-cc. This is because I will not only have to fix up the symbol table; I'll need to walk over the entire goto-program, mangling every call to the exported function too. It seems like a good idea to do this in goto- cc, which only ever sees one translation unit at a time, so I can safely rename every function I find without worrying what file it came from.

Yes. Sorry to ask for large changes but it will need to be done at some point and it is better that it is now, with you giving it your attention, than as a bug report.

Question: it seems like I will need to recursively walk over irepts to do the name-mangling in the program. Is there an existing way of doing this, i.e. some sort of visitor-pattern thing in the CBMC codebase, or do I just do it manually?

There is `expr_visitort` in `util/expr.h` but `util/replace_symbol.h` might suit your needs better.

Asking because I did a similar thing for the linker script work (where I had to match multi-level nested irepts to change their type)...I remember having a conversation with @tautschnig long ago about having a tool called goto-grep to find particular shapes in irepts, and the natural extension of that would be to have goto-sed ;-)

I tried to write something like goto-grep as one of my first CPROVER projects. It turns out to be much harder than you might think. Maybe I should try again at some point...

[tautschnig]

Question: it seems like I will need to recursively walk over irepts to do the name-mangling in the program. Is there an existing way of doing this, i.e. some sort of visitor-pattern thing in the CBMC codebase, or do I just do it manually? Asking because I did a similar thing for the linker script work (where I had to match multi-level nested irepts to change their type)...I remember having a conversation with @tautschnig long ago about having a tool called goto-grep to find particular shapes in irepts, and the natural extension of that would be to have goto-sed ;-)

Maybe rename_symbolt is all that you need?

[karkhaz]

I'm going to leave the tests to run overnight, but I think I'm ready for review.

Summary

• Everything is done in goto-cc now. There is no more goto-instrument pass.
• The flag is called --export-function-local-symbols, because there isn't actually a GCC flag called -fkeep-static-functions (you probably meant -fkeep-inline-functions or -fkeep-static-consts).
• If the user passes that flag, all static functions in the translation unit are kept and name-mangled.

Name mangling

I've included two implementations. The active one mangles function foo() in path/to/bar.c into

__CPROVER_file_local_bar_c_foo()

which should be good enough almost all of the time. To deal with having the same-named function in a same-named file in a different part of the codebase, you can pass an argument to --mangle-suffix:

__CPROVER_file_local_bar_c_SUFFIX_foo()

this way, users decide whether they need a suffix. They can then pass a different suffix to each invocation of goto-cc. That way, all functions in the same file will be mangled with the same suffix, but different files will have different suffixes.

there is another implementation that hashes the pathname using Daniel J. Bernstein's hash, but it's not currently used. The implementation is chosen using templates, so there's no runtime cost to keeping both. The idea with that implementation is that it takes the entire file path into account, so there's no need for a suffix (but you can still provide one if you like). I turned it off because it's not really readable, I'd like harnesses to be readable.

__CPROVER_file_local_4a82bea1_foo()

Misc

• rename_symbolt worked nicely, thank you!
• regression/goto-cc-file-local/chain.sh has become interesting. Usually we use the third line of test.desc to pass command-line args to whatever tool chain.sh is invoking, but I'm instead passing arguments to chain.sh itself to control what it does. Depending on the test, it sometimes links the goto-binary and sometimes doesn't, and then sometimes runs goto-instrument and other times runs cbmc.
• @martin-cs I just remembered why I wanted to only selectively export functions. The codebase I'm working on is full of function pointers. The more function implementations we have lying around, the more exponential blowup CBMC will encounter while exploring every possible function implementation that fits the signature of a function pointer. Nevertheless, I reasoned that this is such a serious performance problem that I should spend time actually fixing it, rather than merely avoiding making it worse by only exporting some functions. So I'll get round to fixing the function pointer problem one day.

[karkhaz]

(assigning folks for re-review because I've changed the approach significantly. Thank you!)

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 067a665).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106670075

[karkhaz]

Thanks @smowton, I've resolved all your suggestions.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 4438e77).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106771499