VFS: Divine crashes while capturing files created by truncate

[Lukáš Zaoral]

Hello,
following procedure makes Divine 4.3.6 crash:

1) Create a directory (e.g. test) and create a file using truncate
in this directory (e.g. truncate --size 5M test/test).

2) Execute following command: divine check --capture test/ main.c
where main.c is an arbitrary C source file.

Divine crashes with following output (full report is enclosed):

compiling main.c
loading bitcode … DiOS … LART … RR … constants … done
booting … done
states per second: 0                                                              
state count: 0
mips: 0

error found: boot
error trace: |
  FAULT: access of size 8 at [global* 25b 4ffff8h ddp] is 4194304 bytes out of bounds
  DOUBLE FAULT: trying to return without a caller

a report was written to main.report

If the directory contains only text files, Divine boots without any problems.
Thanks.

[Lukáš Zaoral]

Here is the main.report file: ​https://paste.fedoraproject.org/paste/yw3Z6aY9OOk7cX3fY2SkjQ

[mornfall]

The truncate is not the problem, it is the size of the file. The VM currently can't handle globals or constants that are bigger than 2 megabytes, but this is exactly what --capture of the file will create.

As a stopgap, I have made two changes in next:

• there is now a check that errors out if we try to capture a file that is too big
• I bumped the size limit to 16 megabytes, which is the same as the limit on heap object size

Unfortunately, increasing the limit much further is currently not viable.