Error message from library mechanism are unhelpful to users

[michael-schwarz]

For the --- admittedly incorrect --- program:

// PARAM: --set ana.context.gas_value 0 --set ana.activated[+] thread --set ana.activated[+] threadid

#include <pthread.h>
#include <stdio.h>

void *t_fun(void *arg) {
  return NULL;
}

int main(void) {
  pthread_create(t_fun);
  return 0;
}

we produce the error message

./goblint --enable warn.debug --enable dbg.regression --html --set ana.context.gas_value 0 --set ana.activated[+] thread --set ana.activated[+] threadid  tests/regression/80-context_gas/26-thread.c
Fatal error: exception LibraryDsl.Pattern.Expected("^::")
See result/index.xml

We should instead maybe produce some warning detailing that we failed because the arguments of pthread_create are strange.

[sim642]

#1560 was supposed to fix this, but looks like I somehow missed some calls still. I'll look into this.

More broadly, this is in the flavor of #38. It's not sustainable for us to reimplement every typecheck that the compiler does in Goblint itself. But I'm also surprised that CIL has no problem with this (or have we disabled some warnings?) because it does the typechecking to insert implicit casts as explicit, etc.

Our library function specifications have the number of arguments, but not their types. It's also possible to call such functions with the right number of arguments of wrong types (e.g. in the wrong order). This wouldn't even crash in LibraryFunctions but somewhere down the line in analyses. I don't think LibraryFunctions should also include types, if anything, CIL knows them and could warn about them.

[sim642]

#1560 was supposed to fix this, but looks like I somehow missed some calls still. I'll look into this.

Hmm, not even that. With -v we do say:

Fatal error: exception LibraryDsl.Pattern.Expected("^::")
Marked with function pthread_create

I wonder if it's even possible to have that with backtraces disabled.

[sim642]

There's definitely something going on in the CIL side as well.

If the program contains both the correct and the incorrect one:

  pthread_create(t_fun);
  pthread_create(&id, NULL, t_fun, NULL);

Then this crash no longer happens and the analysis finishes with

[Warning][Unsound][Call][CWE-685] Potential call to function pthread_create with wrong number of arguments (expected: 4, actual: 1). This call will be ignored. (foo.c:12:3-12:24)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (foo.c:12:3-12:24)