truncate extension sometimes extends with file names instead of zeros

[dsheets]

On an empty file system built from 27c4078a00b517671163f668ebd644614171d966, running

#include <unistd.h>
#include <fcntl.h>

int main() {
  close(creat("spaaaaaace"));
  truncate("spaaaaaace",10);

  return 0;
}

results in a file, spaaaaaace, which contains the text spaaaaaace instead of 10 null bytes. For applications which expect POSIX, OS X, Linux, or BSD behavior when using truncate to extend files, this unexpected data can result in incorrectly formatted files.

[zeldovich]

Thanks; I will take a look. Sounds like we might have gotten the spec wrong.

[zeldovich]

Indeed, we proved the wrong spec about truncate -- the FS.file_set_sz_recover_ok theorem. The implementation just sets the length field but doesn't do anything useful with the data blocks (and the theorem just talks about the file metadata). This is because we wrote this operation before implementing byte-level file contents, and forgot to go back and fix it. The truncate operation should instead call something like ByteFile.grow_file, but passed through the tree abstraction in DirTree.v. I'll try to fix this soon.

[zeldovich]

This should be fixed in c6799211b2a7d3565888590bfac13b13e9f6b4de.

Incidentally, your test case didn't compile on a strict C compiler because it was missing a second argument to creat(). :-)

[tomjridge]

This issue is closed, but I just need to add that this problem was detected by David Sheets (dsheets) using SibylFS (David is one of the authors on the SibylFS paper). This is part of the "evidence trail" for the UK "research excellence framework".