Link order matters with --export-file-local-symbols

[markrtuttle]

CBMC version: 5.37
Operating system: macOS
Exact command line resulting in the issue: See below
What behaviour did you expect: See below
What happened instead: See below

When linking goto binaries built with --export-file-local-symbols, link order matters.

Consider the attached files project.c

static int foo(int x) {
  return x+1;
}

static int bar(int x) {
  return x+2;
}

and proof.c

int __CPROVER_file_local_project_c_foo(int x);

int main() {
  int x = __CPROVER_file_local_project_c_foo(1);
  assert(x == 2);
}

Linking with proof.goto and project.goto fails to update the Pretty name, Module, and Base name entries of the symbol table:

goto-cc -o project.goto --export-file-local-symbols project.c
goto-cc -o proof.goto --export-file-local-symbols proof.c
goto-cc -o main1.goto proof.goto project.goto

the symbol table contains

cbmc --show-symbol-table main1.goto | awk '/Symbol......: __CPROVER_file_local/ ' RS="" ORS="\n\n"

Symbol......: __CPROVER_file_local_project_c_bar
Pretty name.: bar
Module......: project
Base name...: bar
Mode........: C
Type........: signed int (signed int x)
Value.......: irep("(\"compiled\")")
Flags.......: lvalue
Location....: file project.c line 5

Symbol......: __CPROVER_file_local_project_c_foo
Pretty name.: __CPROVER_file_local_project_c_foo
Module......: proof
Base name...: __CPROVER_file_local_project_c_foo
Mode........: C
Type........: signed int (signed int x)
Value.......: irep("(\"compiled\")")
Flags.......: lvalue
Location....: file project.c line 1

and the reachable functions are

goto-analyzer --reachable-functions main1.goto | grep '^/'

/Users/mrtuttle/export/proof.c main 3 6
/Users/mrtuttle/export/project.c __CPROVER_file_local_project_c_foo 1 3
/Users/mrtuttle/export/<built-in-additions> __CPROVER_initialize 40 7

Linking with proof.goto and project.goto in the other order updates the symbol table as I expect, but omits foo from the list of reachable functions:

goto-cc -o project.goto --export-file-local-symbols project.c
goto-cc -o proof.goto --export-file-local-symbols proof.c
goto-cc -o main2.goto project.goto proof.goto

the symbol table contains

cbmc --show-symbol-table main2.goto | awk '/Symbol......: __CPROVER_file_local/ ' RS="" ORS="\n\n"

Symbol......: __CPROVER_file_local_project_c_bar
Pretty name.: bar
Module......: project
Base name...: bar
Mode........: C
Type........: signed int (signed int x)
Value.......: irep("(\"compiled\")")
Flags.......: lvalue
Location....: file project.c line 5

Symbol......: __CPROVER_file_local_project_c_foo
Pretty name.: foo
Module......: project
Base name...: foo
Mode........: C
Type........: signed int (signed int x)
Value.......: irep("(\"compiled\")")
Flags.......: lvalue
Location....: file project.c line 1

and the reachable functions are

goto-analyzer --reachable-functions main2.goto | grep '^/'

/Users/mrtuttle/export/proof.c main 3 6
/Users/mrtuttle/export/<built-in-additions> __CPROVER_initialize 40 7

export.tar.gz

[jimgrundy]

@markrtuttle Can you take this unless/until you can convince Michael to take it.

[tautschnig]

We have the following things happening:
For code-typed symbols (i.e., functions), the linker will only replace selected fields when updating the symbol table: https://github.com/diffblue/cbmc/blob/develop/src/linking/linking.cpp#L775..L779 The base_name is not one of these.
When listing (un)reachable functions, the base_name is compared to the list of called functions: https://github.com/diffblue/cbmc/blob/develop/src/goto-analyzer/unreachable_instructions.cpp#L317..L321. The latter seems wrong for sure, but I'm not entirely sure what the "right" behaviour for export-file-local-symbols and/or the linker is. Further discussion with @markrtuttle is taking place.

[tautschnig]

#6337 now does the tidying up of the linker, and #6338 fixes the bug in goto-analyzer. #6338 will ensure that the output of --reachable-functions is complete, but only together with #6337 will the output be consistent irrespective of linking order.