Public splint test: memory leak

Hello,

the public.style.splint test fails for me because of an alleged memory leak in destroy(). I get the following error message:

Running test public.style.splint:
  FAIL: splint found warnings.
    stdout:
      Command Line: Setting +ptrnegate redundant with current value
      src/trie.c: (in function destroy)
      src/trie.c:66:14: Only storage *(root->next)->next (type struct Trie **)
          derived from released storage is not released (memory leak): root->next
        A storage leak due to incomplete deallocation of a structure or deep pointer
        is suspected. Unshared storage that is reachable from a reference that is
        being deallocated has not yet been deallocated. Splint assumes when an object
        is passed as an out only void pointer that the outer object will be
        deallocated, but the inner objects will not. (Use -compdestroy to inhibit
        warning)

I have tested my program for memory leaks with valgrind, but could not reproduce any errors.

==620== HEAP SUMMARY:
==620==     in use at exit: 0 bytes in 0 blocks
==620==   total heap usage: 49,563 allocs, 49,563 frees, 5,555,520 bytes allocated
==620== 
==620== All heap blocks were freed -- no leaks are possible

Am I missing a splint annotation or is there actually a memory leak?

I have the same issue, even though I can prove that my code is correct. I think this is because splint can’t know about the invariants that the Trie structure has. It additionally encounters an internal parse error and crashes for me even though my code is correct by the C standard and I’m not using any funky syntax.

Congratulations, you earned a free lesson on ownership. Here it is:

In systems programming language, we have to manually free all resources. To keep track of who’s responsible for deleting a block of memory, we often intuitively develop some hierarchy, where some memory blocks reference others, and where we pass the “responsibility” to free around. For example, in Wordle, you (and many others) implemented the trie such that each trie has sub-tries. These sub-tries are created such that each sub-trie has a unique parent. The responsibility to free the sub-tries of a trie passes to whomever also is responsible for freeing the parent trie. To make this easy, you are suppsed to implement a destruct method, which then recursively frees it subtries.

Another example is the create method. It creates a new trie, but does not free it. Instead, it returns a pointer to that trie to the calling function. It thereby also passes the “responsibility to free” that trie to the calling function.
In the project, that function likely is your generateDict. generateDict similarly returns the trie (and the responsibility) to the calling function, which likely is main. main passes that trie to the guess function, which uses it, but is not responsible for freeing it, since we wrote the code such that main retains that responsibility, while guess expects that it can just use the dictionary without freeing it.

This “responsibility to free” is called ownership. We say that create returns a new tree, which is owned by the calling function. main passes the tree to guess, but retains ownership. free takes a block of memory, which you must own, and frees it, thereby deleting that block of memory, while taking ownership (so that no one owns a free block of memory). Note that none of this is explicit in the code, but rather part of the “ghost state” (i.e. the part of the program that is only visible in the specification / correctness proof).

Now, splint is rather sophisticated at tracking ownership, among other things.

You might have seen the annotation /*@out@*/ in generateDict, which tells splint to check that someone writes to that pointer. Similarly, there are annotations which tell splint how ownership moves through the program.

Concretely, splint gets confused because its automatic ownership inference fails. Thus, you likely want to help it out by setting appropiate ownership hints.

As we have seen, we sometimes pass around a pointer with ownership, and sometimes we do not. The latter is called borrowing. There are more sophisticated borrowing models, like refcounting, where every time you borrow a piece of memory, you increase a counter, and when you’re done, you decrease it again. When the counter reaches 0, you must free the piece of memory.

Splint has quite a sophisticated understanding of these concepts. See the documentation for more information.

To apply this to your project, your destroy method wants to have the parameter dict marked as /*@only@*/, like this:

void destroy(/*@only@*/ Trie *dict);

This means that ownership of the trie is transferred into the function. Since the function does not return, it must delete the given dict. Make sure to apply this change in both header and definition.

Now, we also need to tell splint that that the trie owns all its subtries. For this, we use /*@owned@*/.
Now, your trie has the “double pointer problem”. This means that while you could annotate your tries like this:

struct Trie {
    /* fields */
    /*@owned@*/ struct Trie**  somefield; //whoops, this should be /*@owned@*/
};

however, this will not work, since this only tells splint that the memory at somefield is owned by the overall trie, but not also every memory pointed to by a pointer stored in the memory pointed to by somefield. To do this, we need to do some rather hacky C

struct Trie; //declares the struct tag "Trie"
typedef /*@owned@*/ struct Trie* subTrie; // define subtrie as /*@owned@*/ pointer to a struct Tre

struct Trie { //give definition to previous struct Trie
    // ... more fields
    subTrie * next;
}

This then makes splint happy, since splint knows that passing *(root->next) to the destroy function will consume the ownership of that pointer, and thus it is not leaked.

In general, ownership is what you want to reason about when thinking about why your programs are correct. There are more benefits to tracking ownership and borrowing than ensuring that everything is freed eventually. Rust, for example, is a systems programming language that is type-safe, by using a type system based on ownership and borrowing. It also prevents concurrency bugs, because data races can not happen when everyone uniquely owns their data. Ownership is also at the core of the theory used to actually verify memory-modifying programs.

I’m sorry you had to fight splint.

Hope this explaination helped,
Johannes

Edit: fixed /*@only@*/ in structs to /*@owned@*/, which actually makes sense. Sorry

5 Likes

For you, the same approach works. Note that you may have to also change it to /*@owned@*/ subTrie* next.

Apart from this, do not use reallocarray, since it is non-standard and splint does not know about it.

Further, you have a method taking a char **buf_ref. First, make sure that the other parameter supposed to give the length of that array actually matches the actual length of the block of memory pointed to by that pointer.
Then, do the same typedef trick, to tell splint that this is a pointer to a maybe-null char. In other words, change it to

typedef /*@null@*/ char* maybe_null_char;
void foo(..., maybe_null_char* buf_ref, ...);

Alternatively, handle the fact that malloc may return null. More likely, you might want to take a close look at the getline specification to see that not mallocing at all is also an option.

First of all, thank you very much for helping me. The first trick helped to fix my first issue, though there two other errors of which I think one can’t actually be fixed at all:

Running test public.style.splint:
  FAIL: splint found warnings.
    stdout:
      Command Line: Setting +ptrnegate redundant with current value
      src/dict.c: (in function insert)
      src/dict.c:80:33: Only storage *(dict->children) (type SubTrie) derived from
          released storage is not released (memory leak): dict->children
        A storage leak due to incomplete deallocation of a structure or deep pointer
        is suspected. Unshared storage that is reachable from a reference that is
        being deallocated has not yet been deallocated. Splint assumes when an object
        is passed as an out only void pointer that the outer object will be
        deallocated, but the inner objects will not. (Use -compdestroy to inhibit
        warning)

    stderr:
      Splint 3.1.2 --- 21 Feb 2021

      src/dict.c:126:13: Parse Error. (For help on parse errors, see splint -help
                   parseerrors.)
      *** Cannot continue.

Also I noted that the unit tests on the server side don’t include splint for some reason, as I passed all tests there.

Hm, maybe @Marcel.Ullrich2 disabled some rules that were annoying people.

Apart from that, I maybe can make your code work using /*@null@*/ /*@owned@*/ struct Trie** foo; (in/around line 23 of dict.c). The typedef trick is not even necessary.

Anyway, your code should work without my typos above.

1 Like

I already this this, and I got the errors I posted earlier.

I took the risk and annotated my code like this:

/*@-compdestroy@*/
free(node->edges); // sample free

to silence the warning, as I knew I freed every sub-edge.
This seemed to be allowed by the build server (maybe its even enables this globally).

We now disabled compdestroy as ownership management should not be a main conceirn of the project.

Please do not use lint suppressions as this will cost you the linter points in the evaluation.

2 Likes

Thank you. Would it be possible to release the full set of rules (especially disabled rules) that are now active on the servers?

The splint rules are:

    args = ["-retvalother","-retvalint","-branchstate", "-exportlocal", "-usedef", "-compdef", "-temptrans", "+charint", "-predboolint", "-predboolothers", "-nullret", "-nullderef", "-nullpass", "-unrecog", "+matchanyintegral", "-mustfreefresh", "-formatcode", "-mustdefine", "-initallelements","-boolops", "-compdestroy", "-I", "include"]

Note: Keep in mind that splint alone is not all of the style tests. There are the two other public style tests and there might be secret style tests like using autoformatter, correct header source distinction or tests for other aspects of good quality code you learned in the lecture.

1 Like

If you destroy() the father/mother, you should also destroy their children. Else they might come back for revenge. And they will.