Missing handling of atexit

There are two wrong proofs in new sv-benchmarks memsafety tasks.

• global-atexit-2.i
• global-atexit-5.i

Command lines to reproduce: scripts/cpa.sh -spec ../sv-benchmarks/c/properties/valid-memsafety.prp -svcomp21 ../sv-benchmarks/c/memsafety/global-atexit-2.i

scripts/cpa.sh -spec ../sv-benchmarks/c/properties/valid-memsafety.prp -svcomp21 ../sv-benchmarks/c/memsafety/global-atexit-5.i

LOG:

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.

changed milestone to %2.0

added SV-COMP component: PredicateCPA task unsound labels

assigned to @Stephh93

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?

Because the function which is passed to atexit() causes a double free.

Update: In Program global-atexit-5.c

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.

Sorry for the confusion I missed mentioning the investigated program. global-atexit-5.yml claims that valid-free is violated and the MWE was wrong

Yes, for global-atexit-5.yml the cause seems clear.

Looking at global-atexit-2.c:

There is a memory leak in line 20:

if __VERIFIER_nondet_bool() returns true, the program terminates, but before terminating free_g1() is called and free_g2() afterwards. So *g is leaked.

This issue is due to missing support of atexit().

From the manual:

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.

Update the previous MWE was false:

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.

Commits 1c6409d1 and f8ebd70d add atexit to unsupported features list. This will for now return UNKNOWN if atexit is used.

But these commits add the option only to some configs. I think it should be the default.

Yes I agree. I will add it to CallstackOptions... Should we revert the changes introduced by those commits?

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.

removed component: PredicateCPA label

removed task label

added enhancement function pointer labels

changed title from Wrong proofs for MemSafety tasks to Missing handling of atexit

changed the description

unassigned @Stephh93

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.

removed milestone %2.0

removed unsound label

changed milestone to %Release 4.0

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:

void foo( void );

int main( void )
{
   atexit( foo );
}

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.

assigned to @daniel-raffler and @BaierD

mentioned in merge request !150 (merged)

The core of the implementation is in !150 (merged), some further improvements are in !195.

removed milestone %Release 4.0