Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)CPAchecker 1.9.2-svn-35703M (OpenJDK 64-Bit Server VM 11.0.8) started (CPAchecker.run, INFO)Parsing CFA from file(s) "../sv-benchmarks/c/memsafety/global-atexit-5.i" (CPAchecker.parse, INFO)Starting analysis ... (CPAchecker.runAlgorithm, INFO)Stopping analysis ... (CPAchecker.runAlgorithm, INFO)Verification result: TRUE. No property violation found by chosen configuration.More details about the verification run can be found in the directory "./output".Graphical representation included in the file "./output/Report.html".
This is caused by missing support for the C function atexit.
Edited
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Child items ...
Show closed items
Linked items 0
Link issues together to show that they're related or that one is blocking others.
Learn more.
There is currently nothing in CPAchecker that supports atexit and this C function is used by these tasks.
However, I don't think this could explain wrong proofs. In these programs, atexit is used to call free at the end of the program, so without that call CPAchecker should at most report an incorrect memory leak. How would this lead to a wrong proof?
Isn't g already 0 when the "at-exit" functions are called? free(0) is a legal no-nop. Furthermore, global-atexit-2a.yml and global-atexit-2b.yml both claim that only memcleanup/memtrack are violated, not invalid-free.
if __VERIFIER_nondet_bool() returns true, the program terminates, but before terminating free_g1() is called and free_g2() afterwards. So *g is leaked.
The atexit() function registers the given function to be called at normal process termination, either via exit(3) or via return from the program's main(). Functions so registered are called in the reverse order of their registration; no arguments are passed.
The same function may be registered multiple times: it is called once for each registration.
To prevent wrong results, we should maybe return UNKNOWN for now when atexit is called. Makes sense because this changes the program semantics in a way that we do not handle (like longjmp, for example).
Properly handling it is some effort due to a stack of function calls being used, but it should be possible in principle by handling it similarly to function pointers.
At each program exit point, we would add conditional calls to all candidate functions that could be used with atexit. Because a function might be added several times, these calls would need to be in a loop. However, unlike for function-pointer calls, there needs to be some special CPAchecker-specific encoding.
Possible example of what kind of code would need to be added to the CFA:
extern void (*__CPAchecker_pop_atexit())(void);void __CPAchecker_implement_atexit() { void (*f)(void) = __CPAchecker_pop_atexit(); while (f) { f(); // would be expanded with usual function-pointer handling __CPAchecker_pop_atexit(); }}
In addition there would be calls to __CPAchecker_implement_atexit() at each program exit point.
Then we need an additional CPA that keeps a stack of function pointers in its abstract state and implements semantics of atexit and __CPAchecker_pop_atexit(). After the latter we need to ensure that the information about the content of f gets propagated via strengthening to other CPAs (at least to the FunctionPointerCPA).
If this new CPA is implemented with explicit state, it should work well as long as the function name is directly passed to atexit like in the above programs. If the value of the atexit parameter comes from some variable or more complex expression, it would get more difficult.
Yes, actually this is important because the changes break the config because all the other functions in the default value are now missing. But you need to add atexit to all those configs that already set this option.
Btw: Why did you change the formatting of the config file while adding the value? Please don't do this, it makes it really hard to see what you actually added.
We now report UNKNOWN if atexit is called, so we are no longer unsound. Because it is a rarely used feature, we currently do not plan to implement it. Please comment if this is necessary for you.
The current plan for handling atexit is the following:
(1) Add post-processing for the CFA similar to function pointers:
Add a CPAchecker specific ghost variable and function of the form (void (__cdecl *atexit_fun_ptr_tmp )( void ) = cpachecker_atexit_pop(). This allows CPAs to handle the atexit stack and the function pointers however they want, similar to the function pointers. cpachecker_atexit_pop() simply pops the atexit function pointer stack and returns null (or an empty collection) if there is no function registered anymore. The variable atexit_fun_ptr_tmp holds the identifier for the function the pointer points to in the CPA.
Add a loop of the form while((void (__cdecl *atexit_fun_ptr_tmp )( void ) = cpachecker_atexit_pop()) != 0) with the function pointer handling inside of it. This way the atexit stack handling is inside of CPAs, while the control-flow is handled in general in the CFA.
This loop then uses the function pointer cascade inside, similar to function pointers, deciding on which function to call.
(2) Build a atexitCPA that handles trivial cases of the form:
This CPA should work similarly to the functionPointerCPA, in that the transfer relation only handles atexit function calls, to register functions in the stack, and the internal atexit stack pop function. The state should hold this stack. Since C allows many transformations and operations on pointers, we should only handle trivial cases as above in the beginning. We could however retrieve additional information via strengthening from other CPAs later.
This would also allow every CPA to implement this on its own if needed (SMGs for example ;D).
Just as additional clarification for other readers: The "ghost variable" mentioned would be only implicit, but invisible in the CFA. And cpachecker_atexit_pop (maybe __CPAchecker_atexit_pop?) would only be called, but would have no body in the CFA.