Merge pull request #1541 from GaloisInc/sanitize-strs-quoting

Sanitize strings in `to_cryptol_str` in quoting.py

cryptol-remote-api/python/cryptol/bitvector.py

@@ -149,7 +149,7 @@ def to_int(self) -> int:
 
     def to_signed_int(self) -> int:
         """Return the signed (i.e., two's complement) integer the ``BV`` represents."""
-        if not self.msb():
+        if self.__size == 0 or not self.msb():
             n = self.__value
         else:
             n = 0 - ((2 ** self.__size) - self.__value)

cryptol-remote-api/python/cryptol/quoting.py

@@ -14,6 +14,8 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str:
     if isinstance(val, bool):
         return 'True' if val else 'False'
     elif isinstance(val, tuple):
+        if len(val) == 1:
+            raise TypeError("Unable to convert 1-tuple to Cryptol syntax: " + str(val))
         return '(' + ', '.join(to_cryptol_str(x) for x in val) + ')'
     elif isinstance(val, dict):
         return '{' + ', '.join(f'{k} = {to_cryptol_str(v)}' for k,v in val.items()) + '}'
@@ -22,14 +24,15 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str:
     elif isinstance(val, list):
         return '[' + ', '.join(to_cryptol_str(x) for x in val) + ']'
     elif isinstance(val, BV):
-        if val.size() % 4 == 0:
+        if val.size() > 0 and val.size() % 4 == 0:
             return val.hex()
         else:
             return f'({val.to_signed_int()} : [{val.size()}])'
     elif isinstance(val, OpaqueValue):
         return str(val)
     elif isinstance(val, str):
-        return f'"{val}"'
+        chars = list(val.encode('latin-1'))
+        return f'({to_cryptol_str(chars)} : [{len(chars)}][8])'
     elif hasattr(val, '__to_cryptol_str__'):
         return parenthesize(val.__to_cryptol_str__())
     else:

cryptol-remote-api/python/tests/cryptol/test_quoting.py

@@ -24,15 +24,26 @@ def test_quoting(self):
 
         self.assertEqual(cry_f('id {BV(size=7, value=1)}'), cry('id (1 : [7])'))
         self.assertEqual(cry_eval_f('id {BV(size=7, value=1)}'), BV(size=7, value=1))
+        self.assertEqual(cry_f('id {BV(size=0, value=0)}'), cry('id (0 : [0])'))
+        self.assertEqual(cry_eval_f('id {BV(size=0, value=0)}'), BV(size=0, value=0))
 
         self.assertEqual(cry_f('{ {"a": x, "b": x} }'), cry('{a = 0x01, b = 0x01}'))
         self.assertEqual(cry_f('{{a = {x}, b = {x}}}'), cry('{a = 0x01, b = 0x01}'))
 
+        with self.assertRaises(TypeError):
+            cry_f('{(0,)}') # Cryptol does not have 1-tuples
+
         self.assertEqual(cry_f('id {5}'),       cry('id 5'))
-        self.assertEqual(cry_f('id {5!s}'),     cry('id "5"'))
-        self.assertEqual(cry_f('id {5:#x}'),    cry('id "0x5"'))
+        self.assertEqual(cry_f('id {5!s}'),     cry('id ([53] : [1][8])')) # id "5"
+        self.assertEqual(cry_f('id {5:#x}'),    cry('id ([48, 120, 53] : [3][8])')) # id "0x5"
         self.assertEqual(cry_f('id {BV(4,5)}'), cry('id 0x5'))
 
+        s = '" \n ÿ \\'
+        self.assertEqual(cry_f('{s}'), cry('([34, 32, 10, 32, 255, 32, 92] : [7][8])')) # "\" \n ÿ \\"
+        self.assertEqual(cry_eval_f('{s}'), [BV(8,c) for c in [34, 32, 10, 32, 255, 32, 92]])
+        with self.assertRaises(UnicodeEncodeError):
+            cry_f('{"π"}') # 'latin-1' codec can't encode character (960 >= 256)
+
         # Only here to check backwards compatability, the above syntax is preferred
         y = cry('g')(cry_f('{x}'))
         z = cry('h')(cry_f('{y}'))