missing function definition in goblint-regression benchmarks?
omainv opened this issue · 4 comments
The following files in c/goblint-regression invoke a function ftw() which does not seem to be defined anywhere:
04-mutex_19-call_by_ptr_rc.i
28-race_reach_19-callback_racing.i
28-race_reach_20-callback_racefree.i
That function might affect reachability (in 28-race_reach_19-callback_racing.i).
Just wondering, is that intended?
@sim642 ???
The intent of these benchmarks is that an extern function, which is given a function pointer, may call the function pointer. Using the POSIX ftw function from ftw.h is pretty obscure though.
I found qsort and bsearch in the C standard library which take function pointer arguments. I suppose the benchmarks can be changed to do it via those instead but they'd still be externs after preprocessing.
Or shouldn't calls to extern functions be part of benchmarks at all? (Or rather, where is the line drawn then since all of C standard library comes via extern declarations as well and needs to be modeled by a verifier somehow?)
Or shouldn't calls to extern functions be part of benchmarks at all? (Or rather, where is the line drawn then since all of C standard library comes via extern declarations as well and needs to be modeled by a verifier somehow?)
For the other programs of the same category, I can't remember to have seen calls to external libraries, apart from the pthread routines and malloc.
Would be nice if somebody else could comment on this.
The intent of these benchmarks is that an extern function, which is given a function pointer, may call the function pointer. Using the POSIX ftw function from ftw.h is pretty obscure though.
Not sure I understand correctly, but if the purpose is to non-deterministically invoke a given function F, wouldn't it be possible to simply write a function that takes a pointer to F as an argument and non-deterministically decides whether to invoke F? That would avoid using external functions.
Not sure I understand correctly, but if the purpose is to non-deterministically invoke a given function F, wouldn't it be possible to simply write a function that takes a pointer to F as an argument and non-deterministically decides whether to invoke F? That would avoid using external functions.
That would be close, but not exactly. As is, it's actually testing what a verifier is assuming about functions whose implementations it cannot see. When given a callback function, it may be called and that possibility should be accounted for, even though the verifier wouldn't have a concrete place where it is called.
This is something that happens in practice where you might not have all the code for all the libraries also under analysis and thus an interesting aspect to check. But I admit it's a difficult one because it requires a clearer set of assumptions what one is allowed to make about extern functions (e.g. they may call function pointers given as argument, they may modify non-static global variables, they don't invoke undefined behavior). It also potentially complicates what a witness for such behavior should look like.
The rules for tasks also say:
Each program contains all code that is needed for the verification
Having to analyze some non-fundamental functions opaquely, even if standard C like qsort, possibly goes against that rule.
Anyway, I'll open a PR to add mock implementations which non-deterministically call the function pointer to these benchmarks. That should settle the issue even if not 100% the same thing but more suitable for SV-COMP.