[Bug] [kparse] - Weird truncation behavior with stdout

[ehildenb]

K Version

% kompile --version
K version:    v5.2.21-44-gd7d340bd4f
Build date:   Thu Jan 20 01:52:53 UTC 2022

Description

kparse is truncating the output of any file it's redirected to when using --gen-glr-bisor-parser. This results in weird behavior on CI (output looks strange).

Input Files

File test.k:

module TEAL-SYNTAX
  import INT-SYNTAX
endmodule

module TEAL-PARSER-SYNTAX
  imports TEAL-SYNTAX
endmodule

module TEAL-DRIVER
  imports TEAL-SYNTAX

  configuration
      <k> $PGM:Int </k>
endmodule

File pgm1.teal:

1

File pgm2.teal:

2

Reproduction Steps

Kompile the semantics with --gen-glr-parser, then call kparse on both programs (one after the other), redirecting the output to file output, and look at the contents of file output between each step. Note that we are using appending redirect for the second call to kparse. Also note that this reproduces on CI (an Ubuntu Focal image, and I'm also on Ubuntu Focal).

% kompile --backend llvm --verbose --gen-glr-bison-parser \
    --main-module TEAL-DRIVER                           \
    --syntax-module TEAL-PARSER-SYNTAX                  \
    test.k
Parse command line options                                   =  0.020s
Importing: Source(Auto imported prelude)
Importing: Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/prelude.md)
Importing: Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/kast.md)
Importing: Source(/home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)
Importing: Source(/home/dev/src/k/test.k)
Outer parsing [64 modules]                                   =  1.056s
Parse configurations [0/3 declarations]                      =  0.411s
  New scanner: TEAL-DRIVER-RULE-CELLS                        =  0.188s
Parse rules [0/75 rules]                                     =  0.241s
Validate definition                                          =  0.183s
Apply compile pipeline                                       =  0.363s
  New scanner: TEAL-PARSER-SYNTAX-PROGRAM-GRAMMAR            =  0.087s
  New Bison parser: TEAL-PARSER-SYNTAX-PROGRAM-GRAMMAR       =  0.334s
Kompile to kore                                              =  0.343s
Save to disk                                                 =  0.045s
Backend                                                      =  1.204s
Cleanup                                                      =  0.001s
Total                                                        =  3.867s

% cat output

% kparse pgm1.teal >> output

% cat output
\dv{SortInt{}}("1")

% kparse pgm2.teal >> output

% cat output
\dv{SortInt{}}("2")

Note that I injected an extra blank line before each prompt for readability (the prompts are denoted with %).

Expected Behavior

I expect kparse to not truncate whatever stream it's writing to when using the bison parser output. So the final cat output should result in:

% cat output
\dv{SortInt{}}("1")
\dv{SortInt{}}("2")

[radumereuta]

Why isn't the local build picking up the latest tags? v5.2.21-44-gd7d340bd4f I get the same behavior on my PC.

[radumereuta]

If you remove --gen-glr-bison-parser it's fine.

[dwightguth]

This appears to be a bug in how the kparse script (and probably other scripts) handle the case when the --output-file command line flag is not specified, and the file descriptor for stdout on the kparse script is redirected to a file rather than a terminal. I will investigate the best way to address this in each script where this current design pattern is being used.