ftruncate to grow a file does not allocate blocks

[tchajed]

The implementation of ftruncate calls the wrong function in AsyncFS.v, setting the inode size blindly without allocating new blocks if the size grows. Here's a bug that results from implicitly using block 0 for the new blocks:

test-case.c:

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

int main() {
  chdir("/tmp/fscqmnt");

  unsigned char buf[2] = { 1, 2 };
  int fd_foo = open("foo", O_CREAT | O_RDWR, 0777);
  ftruncate(fd_foo, 5);
  pwrite(fd_foo, buf, 2, 0);

  int fd_bar = open("bar", O_CREAT | O_RDWR, 0777);
  ftruncate(fd_bar, 5);

  unsigned char rbuf[2];
  pread(fd_bar, &rbuf, 2, 0);
  // BUG: this outputs "bar: 01 02" instead of the expected "bar: 00 00"
  printf("bar: %02d %02d\n", (int) rbuf[0], (int) rbuf[1]);
  close(fd_bar);

  // just to demonstrate what gets written
  sync();

  return 0;
}

bug.sh:

#!/bin/bash

set -e

DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
FSCQ=$HOME/fscq

start_fscq() {
  "$FSCQ"/src/fscq "$FSCQ"/src/disk.img -f -o big_writes,atomic_o_trunc,use_ino "$1" &
  sleep 0.5
}

unmount_fscq() {
  fusermount -u "$1"
}

mkdir -p /tmp/fscqmnt
gcc "$DIR"/test-case.c -o "$DIR"/test-case
if [ ! -f /tmp/empty.img ]; then
  "$FSCQ"/src/mkfs /tmp/empty.img
fi
cp /tmp/empty.img "$FSCQ"/src/disk.img

start_fscq /tmp/fscqmnt
"$DIR"/test-case
tree -s /tmp/fscqmnt
unmount_fscq /tmp/fscqmnt

Running bug.sh (or compiling and running test-case.c after mounting FSCQ to /tmp/fscqmnt) produces bar: 01 02, since foo and bar point to the same disk blocks.

[tchajed]

Specifically what happened was that we were calling AsyncFS.file_set_sz to implement ftruncate, which merely sets the inode size. That works for shrinking the file but doesn't grow the file correctly. There is a function AsyncFS.file_truncate with a specification and proof, but it operates on blocks, not bytes. We fixed the bug by implementing ftruncate correctly, but that code does not have a proof.