SAW inexplicably prints blank lines when type annotation is omitted

[RyanGlScott]

Given the following C and SAWScript program:

// test.c

#include <stdint.h>

// In LLVM 7+, this will have type <{ [128 x i32], [128 x i32] }>, see
// https://llvm.discourse.group/t/array-layout-changed-by-clang-llvm-starting-from-version-7/2271
const int8_t countLeadingZerosHigh[256] = {
    8, 7, 6, 6, 5, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4,
    3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
    2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
    2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
  };

void f() {}

// test.saw

let fromTo (from : Int) (to : Int) : LLVMSetup [Int] =
  for (eval_list {{ fromTo`{first=from, last=to, a=[64]} }})
      (\x -> return (eval_int x));

let
{{
countLeadingZerosHigh : [256][8]
countLeadingZerosHigh = [
    8, 7, 6, 6, 5, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4,
    3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
    2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
    2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
  ]
}};

let f_spec = do {
  llvm_execute_func [];

  rows <- fromTo 0 127;
  for [0, 1] (\col -> for rows (\row ->
    llvm_points_to (llvm_elem (llvm_elem (llvm_global "countLeadingZerosHigh") col) row)
                   (llvm_term {{ countLeadingZerosHigh @ (`(128 * col + row)) }})));
  return ();
};

m <- llvm_load_module "test.bc";
llvm_verify m "f" [] false f_spec z3;

If I run this program, SAW will print a wall of blank lines before verifying the spec:

$ clang -O0 -g -emit-llvm -frecord-command-line test.c -c
$ ~/Software/saw-0.8/bin/saw test.saw


[14:16:45.519] Loading file "/home/rscott/Documents/Hacking/C/test.saw"
































































































































































































































































[14:16:50.398] Verifying f ...
[14:16:50.398] Simulating f ...
[14:16:50.562] Checking proof obligations f ...
[14:16:50.562] Proof succeeded! f

On the other hand, if I change (`(128 * col + row)) to (`(128 * col + row) : [8]), then SAW does not print a wall of blank lines:

$ clang -O0 -g -emit-llvm -frecord-command-line test.c -c
$ ~/Software/saw-0.8/bin/saw test.saw


[14:18:18.206] Loading file "/home/rscott/Documents/Hacking/C/test.saw"
[14:18:23.048] Verifying f ...
[14:18:23.048] Simulating f ...
[14:18:23.211] Checking proof obligations f ...
[14:18:23.211] Proof succeeded! f

[RyanGlScott]

Here's a slightly more minimal example that doesn't require C code:

// test.saw

let fromTo (from : Int) (to : Int) : TopLevel [Int] =
  for (eval_list {{ fromTo`{first=from, last=to, a=[64]} }})
      (\x -> return (eval_int x));

range <- fromTo 0 20;

// Prints wall of newlines
for range (\_ -> print {{ [True] @ 0 }});

// Doesn't print wall of newlines
// for range (\_ -> print {{ [True] @ (0 : [8]) }});

[robdockins]

This is probably due to the transition to prettyprinter. In that package <+> inserts a separation even if one of the two documents is empty, whereas our older library did not.

[RyanGlScott]

Indeed, I suspect that prettyprinter is not collapsing empty lines in a call to (<+>) or hsep somewhere, given prettyprinter's stance on the topic here. We will need to investigate to see what in particular is causing the empty line to appear.

[samcowger]

I happened upon this issue today and realized I encountered it, and fixed it, earlier this year. The problem is in Verifier.SAW.CryptolEnv.moduleCmdResult. Its intent is to filter out/silence warnings about type defaults, but it does so by filtering those warnings from inside ModuleWarning objects, which can leave "empty" objects (i.e. TypeCheckWarnings mempty mempty) if the only warnings they contained were about type defaults. As it turns out, printing an empty TypeCheckWarnings object produces a newline.

I fixed this in 5475383 by filtering out empty TypeCheckWarnings from the list of warnings that gets printed. This fix also has the happy side-effect of eliminating some newlines that saw prints when you open its REPL. I'd be happy to discuss this solution, or consider others, or make a PR.

[samcowger]

Ah - given that this change stops several newlines from being printed upon launching the REPL and that these newlines mean that typechecking warnings were produced and suppressed, it seems that simply launching the REPL yields warnings. I eliminated all warning suppression in moduleCmdResult to see what they were:

> bin/saw
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 1.0.0.99 (2d0e3d1cf-dirty)

[warning] at Cryptol:840:11--840:17:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol:834:11--834:17:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:731:22--731:25:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:718:15--718:35:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:711:10--711:13:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:710:10--710:13:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:709:10--709:13:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:967:46--976:12:
  Defaulting type of 2nd tuple field to Integer
[warning] at Cryptol:967:46--976:12:
  Defaulting type of 1st tuple field to Integer
[warning] at Cryptol:970:14--970:26:
  Defaulting type argument 'rep' of 'Cryptol::number' to Integer
[warning] at Cryptol:969:14--969:26:
  Defaulting type argument 'rep' of 'Cryptol::number' to Integer
[warning] at Array:55:33--55:41:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol::Reference:44:37--44:43:
  Defaulting type argument 'ix' of '(Cryptol::<<)' to Integer
[warning] at Cryptol::Reference:10:19--10:25:
  Defaulting type argument 'ix' of '(Cryptol::<<)' to Integer
sawscript> 

They seem to refer to files in the Cryptol "standard library". I can't say whether these warnings represent actual problems, but I thought I'd record my findings here for posterity.

[RyanGlScott]

Excellent sleuthing, @samcowger! I agree with your proposed fix, and as it turns out, Cryptol itself uses similar code here. Would you be willing to submit a PR with this fix?

The Cryptol standard library warnings that you observe when enabling all warnings are interesting. Ultimately, it doesn't seem like that serious of an issue, as even Cryptol appears to suppress those warnings when loading the standard library in the REPL. Why Cryptol chooses to suppress those warnings is a bit mysterious to me, as all of those warnings look quite fixable. Perhaps worth filing an issue about this, but I wouldn't lose much sleep over it.

[samcowger]

Done! See #2001.