Suppress defaulting warnings

[robdockins]

Now that cryptol is using more conservative defaulting rules (defaulting will only ever choose unlimited precision types for literals), the default for the Cryptol REPL/interpreter is to suppress defaulting warnings. We should suppress these warnings in saw-script as well.

[brianhuffman]

Is this issue intended to cover the defaulting warnings that saw now displays upon startup? I guess that the cryptol REPL does the same defaulting while checking the cryptol prelude (Cryptol.cry) but it just doesn't tell you about it.

 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.4.0.99 (265ef9544d5430686b522a267d212a0f0288067a)

[warning] at Cryptol:1041:18--1041:24:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol:1032:18--1032:24:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol:921:37--921:43:
  Defaulting type argument 'ix' of '(Cryptol::<<)' to Integer
[warning] at Cryptol:889:19--889:25:
  Defaulting type argument 'ix' of '(Cryptol::<<)' to Integer
[warning] at Cryptol:861:28--861:33:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol:844:25--844:30:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol:756:11--756:17:
  Defaulting type argument 'ix' of '(Cryptol::!)' to Integer
[warning] at Cryptol:750:11--750:17:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:648:22--648:25:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:635:15--635:35:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:628:10--628:13:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:627:10--627:13:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
[warning] at Cryptol:626:10--626:13:
  Defaulting type argument 'ix' of '(Cryptol::@)' to Integer
sawscript>

[robdockins]

Yes, and when importing other Cryptol files as well, I think. The Cryptol REPL now suppresses printing defaulting warnings by default, and we should do the same here.

[brianhuffman]

The startup warning messages are printed by this call to initCryptolEnv inside the buildTopLevelEnv function:

saw-script/src/SAWScript/Interpreter.hs

Line 417 in 3fce7d1

ce0 <- CEnv.initCryptolEnv sc

Function initCryptolEnv is implemented in the cryptol-saw-core package, so this will require a patch to the saw-core repository to fix.

[brianhuffman]

I narrowed it down to this call to loadModuleFrom: https://github.com/GaloisInc/saw-core/blob/3ec1be28aeec1497643873246757a76f548c5cfe/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs#L170-L173