SAW fails silently

[weaversa]

saw nightly fails silently after about 10 seconds. An earlier version 0.7 (670e349) does not fail, but rather sits doing something for a about 6 minutes and then says:

You have encountered a bug in What4's implementation.
*** Please create an issue at https://github.com/GaloisInc/what4/issues

%< ---------------------------------------------------
  Revision:  8402ae2e14de61eba778f3b56b6de6fb41ece610
  Branch:    HEAD
  Location:  bvSliceBE
  Message:   invalid arguments to slice: 128 0 from vector of length 128
CallStack (from HasCallStack):
  panic, called at src/What4/Panic.hs:17:9 in what4-1.0.0.0.99-inplace:What4.Panic
  panic, called at src/What4/SWord.hs:325:5 in what4-1.0.0.0.99-inplace:What4.SWord
%< ---------------------------------------------------

swapping to offline_unint_smtlib2 also fails quickly with the nightly, and spins much longer than I waited in the older version of saw

All details are in the attached tarball -
silent_bug.tar.gz

[robdockins]

Current master definitely spends more than 10 seconds doing something. Do you remember which nightly you were using when you saw this behavior?

[weaversa]

It was the nightly from 17 days ago.

[robdockins]

OK, I'll check out what's going on with the nightly. In the meantime, that panic looks like an assumptions mismatch between the What4 SWord module and the saw-core simulator. I think the easiest fix is to relax the restriction in What4.

[robdockins]

I'm not able to reproduce the silent failure behavior using nightlies from around that time. Maybe the process was hitting a memory limit?

[brianhuffman]

Adding a check_goal command in a do block before the offline_w4_unint_yices tactic reveals that the goal is ill-typed:

[20:52:25.415] Stack trace:
"sat_print" (/Users/huffman/Documents/saw/issue1166/silent_bug/bug.saw:5:1-5:10):
"check_goal" (/Users/huffman/Documents/saw/issue1166/silent_bug/bug.saw:9:5-9:15):
Inferred type
  let { x@1 = Prelude.Vec 128 Prelude.Bool * #(-empty-)
    }
 in Prelude.Eq sort 0 x@1 x@1
Not a subtype of expected type
  let { x@1 = Prelude.Vec 128 Prelude.Bool
    }
 in Prelude.Eq sort 0 x@1 x@1
For term
  let { x@1 = Cryptol.TCNum 128
      x@2 = Cryptol.tcMul (Cryptol.TCNum 8) (Cryptol.TCNum 16)
    }
 in Cryptol.pair_cong1 (Cryptol.seq x@2 Prelude.Bool)
      (Prelude.Vec 128 Prelude.Bool)
      #(-empty-)
      (Cryptol.seq_cong1 x@2 x@1 Prelude.Bool
         (Prelude.unsafeAssert Cryptol.Num x@2 x@1))

So this is the root cause of the problem. I'll have a closer look to see if I can figure out where the type error originates.

[brianhuffman]

It looks like an inconsistency in how Cryptol tuple types are encoded in saw-core. We probably have a few functions that assume a different encoding, and now things don't match. I'll try to track it down.