Opened 5 years ago

Closed 5 years ago

#89 closed defect (fixed)

VFS: Divine crashes while capturing files created by truncate

Reported by: Lukáš Zaoral Owned by:
Priority: major Milestone: 4.3
Component: DiOS Keywords:
Cc: kdudka@…, jamartis@…, lzaoral@…


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

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

Change History (2)

comment:1 Changed 5 years ago by Lukáš Zaoral

comment:2 Changed 5 years ago by mornfall

Resolution: fixed
Status: newclosed

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.

Note: See TracTickets for help on using tickets.