From 2f0dbefa39876d37d1f402a20094597b98ce5d53 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 5 Jul 2023 15:45:27 -0400 Subject: [PATCH 1/5] sanitize strings in to_cryptol_str in quoting.py --- cryptol-remote-api/python/cryptol/quoting.py | 3 ++- cryptol-remote-api/python/tests/cryptol/test_quoting.py | 3 +++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/cryptol-remote-api/python/cryptol/quoting.py b/cryptol-remote-api/python/cryptol/quoting.py index 7503c87ff..488a13983 100644 --- a/cryptol-remote-api/python/cryptol/quoting.py +++ b/cryptol-remote-api/python/cryptol/quoting.py @@ -29,7 +29,8 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str: elif isinstance(val, OpaqueValue): return str(val) elif isinstance(val, str): - return f'"{val}"' + val_san = val.replace('\\', '\\\\').replace('"', '\\"').replace('\n', '\\n') + return f'"{val_san}"' elif hasattr(val, '__to_cryptol_str__'): return parenthesize(val.__to_cryptol_str__()) else: diff --git a/cryptol-remote-api/python/tests/cryptol/test_quoting.py b/cryptol-remote-api/python/tests/cryptol/test_quoting.py index 64508c1a1..b52656a6e 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_quoting.py +++ b/cryptol-remote-api/python/tests/cryptol/test_quoting.py @@ -33,6 +33,9 @@ def test_quoting(self): self.assertEqual(cry_f('id {5:#x}'), cry('id "0x5"')) self.assertEqual(cry_f('id {BV(4,5)}'), cry('id 0x5')) + s = '" \ \n' + self.assertEqual(cry_f('{s}'), cry('"\\" \\\\ \\n"')) + # Only here to check backwards compatability, the above syntax is preferred y = cry('g')(cry_f('{x}')) z = cry('h')(cry_f('{y}')) From 1410728a74084c2664339df4a5f13e098c453195 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Wed, 5 Jul 2023 16:22:15 -0400 Subject: [PATCH 2/5] add reference to lexer in to_cryptol_str --- cryptol-remote-api/python/cryptol/quoting.py | 1 + 1 file changed, 1 insertion(+) diff --git a/cryptol-remote-api/python/cryptol/quoting.py b/cryptol-remote-api/python/cryptol/quoting.py index 488a13983..d2adddd03 100644 --- a/cryptol-remote-api/python/cryptol/quoting.py +++ b/cryptol-remote-api/python/cryptol/quoting.py @@ -29,6 +29,7 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str: elif isinstance(val, OpaqueValue): return str(val) elif isinstance(val, str): + # Sanitizing strings for Cryptol - see of src/Cryptol/Parser/Lexer.x val_san = val.replace('\\', '\\\\').replace('"', '\\"').replace('\n', '\\n') return f'"{val_san}"' elif hasattr(val, '__to_cryptol_str__'): From e876142fdff40e4c47aa4bc06487e7e67d12c360 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 10:13:39 -0400 Subject: [PATCH 3/5] encode strings as lists of bytes using latin-1 in to_cryptol_str --- cryptol-remote-api/python/cryptol/quoting.py | 5 ++--- cryptol-remote-api/python/tests/cryptol/test_quoting.py | 8 ++++---- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/cryptol-remote-api/python/cryptol/quoting.py b/cryptol-remote-api/python/cryptol/quoting.py index d2adddd03..82ecdc0d1 100644 --- a/cryptol-remote-api/python/cryptol/quoting.py +++ b/cryptol-remote-api/python/cryptol/quoting.py @@ -29,9 +29,8 @@ def to_cryptol_str(val : Union[CryptolValue, str, CryptolJSON]) -> str: elif isinstance(val, OpaqueValue): return str(val) elif isinstance(val, str): - # Sanitizing strings for Cryptol - see of src/Cryptol/Parser/Lexer.x - val_san = val.replace('\\', '\\\\').replace('"', '\\"').replace('\n', '\\n') - return f'"{val_san}"' + 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: diff --git a/cryptol-remote-api/python/tests/cryptol/test_quoting.py b/cryptol-remote-api/python/tests/cryptol/test_quoting.py index b52656a6e..20e803dcd 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_quoting.py +++ b/cryptol-remote-api/python/tests/cryptol/test_quoting.py @@ -29,12 +29,12 @@ def test_quoting(self): self.assertEqual(cry_f('{{a = {x}, b = {x}}}'), cry('{a = 0x01, b = 0x01}')) 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('"\\" \\\\ \\n"')) + s = '" \n ÿ \\' + self.assertEqual(cry_f('{s}'), cry('([34, 32, 10, 32, 255, 32, 92] : [7][8])')) # "\" \n ÿ \\" # Only here to check backwards compatability, the above syntax is preferred y = cry('g')(cry_f('{x}')) From b2b5e9b4f4f6621e57b73fa76c3995de401f2bb7 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 10:22:22 -0400 Subject: [PATCH 4/5] add eval, latin-1 codec tests to test_quoting --- cryptol-remote-api/python/tests/cryptol/test_quoting.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cryptol-remote-api/python/tests/cryptol/test_quoting.py b/cryptol-remote-api/python/tests/cryptol/test_quoting.py index 20e803dcd..d4da70491 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_quoting.py +++ b/cryptol-remote-api/python/tests/cryptol/test_quoting.py @@ -35,6 +35,9 @@ def test_quoting(self): 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}')) From 93b3d79f3cbc0d11e2806d5400a2d903402f473d Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 6 Jul 2023 13:06:58 -0400 Subject: [PATCH 5/5] fixed BV and 1-tuple edge cases in to_cryptol_str --- cryptol-remote-api/python/cryptol/bitvector.py | 2 +- cryptol-remote-api/python/cryptol/quoting.py | 4 +++- cryptol-remote-api/python/tests/cryptol/test_quoting.py | 5 +++++ 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/cryptol-remote-api/python/cryptol/bitvector.py b/cryptol-remote-api/python/cryptol/bitvector.py index ec9e3111b..6155217f1 100644 --- a/cryptol-remote-api/python/cryptol/bitvector.py +++ b/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) diff --git a/cryptol-remote-api/python/cryptol/quoting.py b/cryptol-remote-api/python/cryptol/quoting.py index 82ecdc0d1..9cb6e75ab 100644 --- a/cryptol-remote-api/python/cryptol/quoting.py +++ b/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,7 +24,7 @@ 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()}])' diff --git a/cryptol-remote-api/python/tests/cryptol/test_quoting.py b/cryptol-remote-api/python/tests/cryptol/test_quoting.py index d4da70491..dd6fbac56 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_quoting.py +++ b/cryptol-remote-api/python/tests/cryptol/test_quoting.py @@ -24,10 +24,15 @@ 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 ([53] : [1][8])')) # id "5" self.assertEqual(cry_f('id {5:#x}'), cry('id ([48, 120, 53] : [3][8])')) # id "0x5"