Prevent truncation of output file by tool

[PhilippWendler]

When a tool truncates the file descriptors that it has for stdout and stderr, this leads to truncation of the log file with the output. So a tool can undo output that it has previously written, and it can remove and overwrite the first few lines of the log that are written by BenchExec (with the command line).

While we could argue that making a tool to remove its own output would be acceptable, it should not be able to overwrite the lines that BenchExec produces.

This can even happen unintentionally if /dev/stdout or /dev/stderr is used for output redirection with > instead of >>.

Example:

runexec -- bash -c 'echo "echo_stdout1" ; echo "echo_stderr1" 1>/dev/stderr ; echo "echo_stdout2"'

The following happens:

1. BenchExec writes the command line.
2. echo_stdout1 is appended.
3. The file content is deleted completely, and echo_stderr1 is written to the beginning of the file.
4. echo_stdout2 is appended to the file, so it appears after the position where the output from 2. ended. The hole in the file between the output from 3. and 4. is filled with null bytes.

We could

• Use a pipe as target for the output. This would solve this completely, but with overhead during the run.
• Add the command line to the log after the run (which involves copying the whole file). This has no overhead during the run but does not solve the tool overwriting its own output and the null bytes.
• Investigate whether there is some option that prevents a file descriptor from being truncated (maybe chattr +a helps).

[PhilippWendler]

chattr is not possible as a regular user.

I hope someone will answer this question.