Feature request: goto-instrument flag for listing functions in goto in machine readable format

[archigup]

For automating checking contracts, we need to know which contracts need to be verified in a goto-file and which need to be applied.

First we need to get the list of contracts in the goto file. Those contracts fall into three categories: contracts for a function defined in the goto file, contracts for undefined functions that are used, and contracts for functions that are unused. We must make a distinction for the last two, since contracts in a header file for functions that are unused have contracts in the goto, but fail to replace when using goto-instrument --dfcc main --replace-call-with-contract ....

If we have the list of contracts for defined functions, and contracts for used undefined functions, we have the information to select contracts to check/use. For each of the contracts in the contracts for defined functions, we use goto-instrument to enforce that contract, and replace calls for the rest of the contracts for defined functions and for all the contracts for undefined used functions.

All the above is sufficient in the absence of contracts for static functions; for those we need to compile with --export-file-local-symbols and thus the name of the function no longer matches the symbol in the goto. For this we also need a mapping from fn/contact name to the actual symbol name.

The way I'm currently doing this is as follows:

• Create a map of fn name to symbol name by taking goto-instrument --list-goto-functions output, filtering to lines matching <c_ident> /* <c_ident> */, and mapping the first ident to the second.
• defined functions = keys of that map
• undefined functions = output of goto-instrument --list-undefined-functions file.goto
• list of contracts = filter undefined functionns for lines starting with contract:: and strip that prefix
• used functions = union of defined functions and undefined functions
• list of contracts to enforce = intersection of defined functions and contracts
• contracts to use for replacement = intersection of used functions and contracts
• Then for each contract to enforce, enforce that contract and use the contracts to use minus that contract. For the arguments check if the fn/contract name is in the name map, and if so use the <contract_name>/<symbol_name> format for the contract argument

My code is here for reference: https://github.com/aws-greengrass/aws-greengrass-sdk-lite/blob/1ab18f4a93ee9e0541aed1bfa00c57b9fc19068f/misc/check_contracts.py

For the above, relying on the exact output format of --list-goto-functions seems sketchy since it seems not intended for consumption by script, and the lines have similar format for different types of entries. Both flags also have a Reading GOTO program from 'file.goto' line.

I think it would be useful to have a flag for machine readable output (preferably JSON), that includes each function, whether it is defined, if it has a contract, and the symbol name.

[tautschnig]

Do I understand correctly that it is only --export-file-local-symbols that (seemingly) leads to this need? I'd suggest you use crangler to selectively remove static from desired functions. See https://diffblue.github.io/cbmc/man/crangler.html for its HTML-ified man page.

[archigup]

Its not just --export-file-local-symbols that causes complication. --replace-call-with-contract also fails when the contract has no calls in the goto binary.

The main issue is that to obtain information about what is in the goto file, I need to parse output of goto-instrument diagnostic flags which don't seem intended for use in this way.