How to Detect Resource Leaks Errors?

[lingqiu huang]

Dear CPAChecker developers,

I have a question regarding the detection of resource leaks errors and would appreciate any insights or guidance you can provide.

sample code ：

CAN find memory-related errors through the smg properties

BUT resource-leak，such as fopen/fclose is missing？

I appreciate any guidance or suggestions on how to configure CPAChecker to detect resource leaks,  when programs fail to release resources (such as memory, file handles, network connections, etc) after they are no longer needed. Are there specific properties or configurations that I should be aware of? Any insights or examples would be greatly appreciated.

Thank you for taking the time to read my message, and I look forward to hearing from you soon.

Best regards, Ling

[Philipp Wendler]

Dear Ling,

thank you for your interest in CPAchecker!

Am 18.07.23 um 05:18 schrieb lingqiu huang:

> I have a question regarding the detection of resource leaks errors and
> would appreciate any insights or guidance you can provide.

> BUT resource-leak，such as fopen/fclose is missing？

Yes, currently there are no out-of-the-box analyses available in
CPAchecker for verifying usage of such resources.

> I appreciate any guidance or suggestions on how to configure CPAChecker to
> detect resource leaks, when programs fail to release resources (such as
> memory, file handles, network connections, etc) after they are no longer
> needed. Are there specific properties or configurations that I should be
> aware of? Any insights or examples would be greatly appreciated.

Configuring CPAchecker wouldn't be enough for this.
One would have to either add a component in CPAchecker that keeps track
of such resources, or add a model with stubs for functions like
fopen/fclose to the program and encode the specification on how to use
these functions correctly in the stubs as reachability properties.

If you are interested in more details about how to implement this,
please let me know.

Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[lingqiu huang]

Dear Philipp,

Thank you for your response, 

Configuring CPAchecker wouldn't be enough for this.
One would have to either add a component in CPAchecker that keeps track
of such resources, or add a model with stubs for functions like
fopen/fclose to the program and encode the specification on how to use
these functions correctly in the stubs as reachability properties.

Do you meaning? The first approach indeed adding a similar class like FileResourceCPA?
the second one using stubs to mock the behavior of fopen and fclose functions,which adding some ERROR labels, and using  reachability properties to Check?

Can you provide a simple example modification based on the following code in details? Thanks a lot.

#include <stdio.h>

typedef unsigned char bool;
extern int __VERIFIER_nodet_int(void);
extern bool checkChecksum(char *);
extern int decodeBlock(char *);

#define BUF_SZ 500
#define DECODE_FAIL 1
#define DECODE_SUCCESS 0

int decodeFile(char* fName) {
char buf[BUF_SZ];
FILE* f = fopen(fName, "r");
if (!f) {
printf("cannot open %s\n", fName);
return DECODE_FAIL;
}
else {
while (fgets(buf, BUF_SZ, f)) {
if (!checkChecksum(buf)) {
return DECODE_FAIL;
}
else {
decodeBlock(buf);
}
}
}
fclose(f);
return DECODE_SUCCESS;
}

Waiting for your reply!

Best,

Ling

[Philipp Wendler]

Dear Ling,

Am 19.07.23 um 05:14 schrieb lingqiu huang:

>> Configuring CPAchecker wouldn't be enough for this.
>> One would have to either add a component in CPAchecker that keeps track
>> of such resources, or add a model with stubs for functions like
>> fopen/fclose to the program and encode the specification on how to use
>> these functions correctly in the stubs as reachability properties.
>
> Do you meaning? The first approach indeed adding a similar class like
> FileResourceCPA?
> the second one using stubs to mock the behavior of fopen and fclose
> functions,which adding some ERROR labels, and using reachability
> properties to Check?

Yes, exactly.

> Can you provide a simple example modification based on the following code
> in details? Thanks a lot.

In the stub for fopen, one would need to somehow store which fds are
allocated (e.g., in a global variable). And fclose needs to update this
state as well.
And then it depends somewhat on what you want to check. One could for
example wrap the main function with a check that all fds are closed.

If you want to actually detect that each fd is closed as soon as the
variables storing its number go out of scope, then writing a CPA instead
of stubbing would work better.