Goblint C library functions

README.md

Compilation and linking with undefined functions

GCC compilation process

Linking fails if an undefined function is used:

❯ gcc test.c
Undefined symbols for architecture x86_64:
  "_f", referenced from:
      _main in test-3943c9.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Commenting out the prototype declaration of the function (line 3) only leads to a warning during compilation:

❯ gcc test.c
test.c:8:7: warning: implicit declaration of function 'f' is invalid in C99 [-Wimplicit-function-declaration]
  x = f(1);
      ^
1 warning generated.
Undefined symbols for architecture x86_64:
  "_f", referenced from:
      _main in test-5a10c9.o
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

However, if the function is later (after use) defined with a different signature than the compiler inferred, it's an error (no implicit conversions apply!):

❯ gcc test2.c
test2.c:8:7: warning: implicit declaration of function 'f' is invalid in C99 [-Wimplicit-function-declaration]
  x = f(1);
      ^
test2.c:13:5: error: conflicting types for 'f'
int f(float x){
    ^
test2.c:8:7: note: previous implicit declaration is here
  x = f(1);
      ^
1 warning and 1 error generated.

The next problem: we can link either implementation, yielding different results:

❯ gcc -c test.c f1.c f2.c
❯ gcc test.o f1.o && ./a.out
1
❯ gcc test.o f2.o && ./a.out
2

So, we can't be sure what the semantics of linked files are. But let's assume for now that linked functions with names and types that correspond to those from the standard library, will behave as such. Later on we could be more pedantic and abort if the content of the header file differs (maybe have a set of valid hashes), or even check the version that will be linked against.

standard library functions

C standard library headers

TODOs:

• Currently Goblint only cares about the name and not the type signature. We should warn if the function is called with incompatible types.
• If we can't find the definition of a function and it's not a library function, we should issue a warning and assume the worst (writes all arguments and spawns every reachable function) - which is bad b/c it can turn a single-threaded program into a multi-threaded one. So it's probably useful to list these 'bad' functions again at the end.
• If we encounter a function that's part of the standard library, but the corresponding header file was not included, we should abort with a warning. There should be an option to disable this behavior and assume the worst (see previous point).

Right now Goblint has a list of library functions with their abstract effect (see categories) and which of their arguments are read/written. This should be more modular and easily extendable. One idea would be to have one .ml file per header file, and implement some function in Goblint to write out a template (possibly already with results from some analysis) for new header files. E.g. ./goblint --enable ana.lib.generate_headers file.c would write out a template stdio.ml (if stdio.h was included in file.c) which could then be adjusted and put in, say, src/lib/ and Goblint could be recompiled with it. In the end, we should try to cover all the standard library functions.

The names of included headers are an heuristic for choosing the correct abstract function. E.g. if there is a function f() that is defined with different behaviors in libraries A and B, then we should look which of them is included to pick the right one, and abort with a warning if the name of the included file doesn't match.

Desired information per function:

• read/written arguments (exists), maybe we could implement an analysis to figure this out automatically (given the source)
• abstract effect (exists, but there are only some predefined groups). Additionally, we would like to be able to give an OCaml function here (pull out the behavior specified in base.ml.

First steps:

• Find out which files are included. This should also work with the preprocessed source code generated by ./goblint --enable justcil file.c, which contains annotations where the orignal code is from:

        #line 156 "/usr/include/stdio.h"
        extern FILE *__stdinp ;
        #line 157
        extern FILE *__stdoutp ;
  

f1.c

int f(int x){
  return x+1;
}

f2.c

int f(int x){
  return x+2;
}

test.c

#include <stdio.h>

int f(int);

int main(){
  int x = f(0);
  printf("%d\n", x);
  return 0;
}

test2.c

#include <stdio.h>

int main(){
  int x = f(0);
  printf("%d\n", x);
  return 0;
}

int f(float x){
  return 3;
}