rpc: Fix bug where an empty list is sent back from the server as Unit (…

…#1194) * make readBack of an empty list actually return an empty list * update test_SHA256
GaloisInc · May 26, 2021 · a8d79c5 · a8d79c5
1 parent 5df7a79
commit a8d79c5
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git a/cryptol-remote-api/python/tests/cryptol/test_SHA256.py b/cryptol-remote-api/python/tests/cryptol/test_SHA256.py
@@ -17,11 +17,9 @@ def test_SHA256(self):
         expected_h1 = BV(size=256, value=0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1)
         self.assertEqual(h1, expected_h1)
 
-        # ugh, this gives a type error...
-        # m2 = CryptolLiteral('""')
-        # j2 = c.call('join', m2).result()
-        # h2 = c.call('sha256', j2).result()
-        h2 = c.eval('sha256 (join "")').result()
+        m2 = CryptolLiteral('""')
+        j2 = c.call('join', m2).result()
+        h2 = c.call('sha256', j2).result()
         expected_h2 = BV(size=256, value=0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
         self.assertEqual(h2, expected_h2)
 

diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs
@@ -389,8 +389,6 @@ readBack ty val =
         VInteger i -> pure (IntegerModulo i n)
         _ -> mismatchPanic
     TVSeq len contents
-      | len == 0 ->
-        return Unit
       | contents == TVBit
       , VWord width wv <- val ->
         do BV w v <- asWordVal C.Concrete wv