A Static Analysis-based Repair Tool for Memory Deallocation Errors for C Programs

MemFix is a static analysis-based repair tool for memory deallocation errors for C programs. MemFix takes a possibly erroneous source code as an input.
The tool attempts to properly insert or delete free-statements for dynamic memory allocations and ouputs an error-free code if succeeds.

The key features of MemFix include:


The key idea of MemFix is to formulate the repair problem as an instance of the Exact Cover Problem. Suppose we have a set of possible execution paths for each dynamically allocated objects (we call it "object traces"). For example, we have 3 object traces for the buggy program above as follows:

Finding a proper set of free-statements corresponds to finding an exact cover, given a set of object traces and a collection of subsets of traces that each free-statement deallocates. In the example code, we have a set of object traces {τ1, τ2, τ3} and a collection of subsets {{τ1}, {τ1, τ2}, {τ2, τ3}}. To understand the problem formulation, let's take a look at the matrix. Rows and colums represent free-statements and object traces respectively. Each bullet in (i,j) represents the free statement at the i-th row deallocates the j-th object trace. For example, the matrix shows that free(p) and free(q) after the line 8 would deallocate the second object trace twice, capturing the double-free situation in the buggy program.

However, simply applying the idea to the real-world fixing problem is impractical because programs mostly have unbounded number of object traces. To deal with the problem, MemFix takes an approach which adopts a static analysis that soundly abstracts the object traces and computes their deallocators at each progarm point.

For further details, please refer to our paper [pdf].

Tool Demo


Contact Information

If you have any questions on this project, please contact us: