GaloisInc/saw-script

Currently there is no way in SAWScript to construct an Int value that is less than zero. This may or may not have been intentional; however, it's undocumented, unexpected, and not consistent with the name of the type. Rather than rename the type to Nat or UInt or something at great length, we should just lift this restriction. One way is via #3392: currently you can only lift back to Int from Cryptol bitvectors and that mechanism is unsigned-only, but #3392 expands that to Cryptol's Integer type. We don't necessarily need to add SAWScript-level arithmetic, but we should at least allow negative integer literals. That is neither difficult to parse nor difficult to implement. Note that before allowing negative Int values we do need to take steps to avoid exposing them as Cryptol numeric types, which are unsigned. This is being handled in #3392 and #3393.

In the course of chasing #3343 it became clear that bvEq_refl is missing from basic_ss. This is silly and should be fixed. (There are reasons to not necessarily unfold or rewrite equalities, which is why a lot of the equality-related rules are left out. But those reasons don't extend to reducing reflexivity.)

Suppose you have these files: a/a.saw b/b.saw c/c.saw and suppose both b.saw and c.saw do include_once "../a/a.saw", and c.saw also includes b.saw. Then from the perspective of c.saw the path of a.saw is ../a/a.saw, but from the perspective of b.saw the path is ../b/../a/a.saw, because we try to make includes relative to where they're included from. But include_once just looks at the path strings, and they're different, so this doesn't work as intended. This does, however, seem like a reasonable thing to do and to want include_once to work for, so I guess we do need it to normalize paths for comparison... much as normalizing paths is annoying and generally wrong. (That or we could check the system-level file identity... but I'm not sure how you do that from Haskell or whether it's workable in Windows.) @qsctr

The SAWScript typechecker and interpreter are built with -Wno-incomplete-uni-patterns and there's a long comment at the bottom of Typechecker.hs that explains why. Basically, there are a couple places that use irrefutable patterns with incomplete matches as a shortcut. These basically function as assertions that the omitted cases of the partial matches are not reached, which is fine until they are and then it turns out that the generated code throws UserError behind your back. That results in the following undesirable behavior: sawscript> let x = 3 saw-script/src/SAWScript/Typechecker.hs:2216:5-60: Non-exhaustive patterns in [(pat'', e1, s)] sawscript> IOW, it crashes but doesn't exit, and while it does print the Haskell source location, it doesn't print what the offending value was. This is not what we want; the handful of affected cases should be turned into explicit panics that print useful messages. We can afford a couple extra lines of code for that in a project the size of SA

When you run saw --help, it returns exit code 2: $ saw --help <snip> $ echo $? 2 This is a bit unfortunate, as I sometimes use saw --help as a basic smoke test to verify if saw can run at all on a given machine, but the non-zero exit code makes scripts believe that saw --help isn't working as expected. Any objections to changing the behavior to return exit code 0 instead?