common: make model_print() use OS file descriptor, not C library FILE*

common: make model_print() use OS file descriptor, not C library FILE*

A C library FILE does buffering (and possibly other opaque operations)
that can conflict with the model-checker's methods of snapshotting
memory. Particularly, it seems like we could corrupt and drop data that
was written to model_out, if the data was large enough and buffered in
just the right way.

Really, with the presence of dprintf(), there is no reason to print to a
FILE stream; we can just use the file descriptor (either STDOUT_FILENO
or the descriptor received from dup2()).

This fixes bugs seen in verbose mode, with a lot of extra debug
printing. Some of the output was being dropped.