[RPC] f-string-like Cryptol quasiquotation

cryptol-remote-api/python/.gitignore

@@ -128,3 +128,8 @@ dmypy.json
 
 # Pyre type checker
 .pyre/
+
+# Files generated from running tests/cryptol/test_cryptol_api.py
+*.crt
+*.csr
+*.key

cryptol-remote-api/python/CHANGELOG.md

@@ -1,8 +1,9 @@
 # Revision history for `cryptol` Python package
 
-## 2.12.2 -- YYYY-MM-DD
+## 2.12.2 -- 2021-11-19
 
-* NEW CHANGELOG ENTRIES SINCE 2.12.0 GO HERE
+* Add an interface for Cryptol quasiquotation using an f-string-like syntax,
+  see `tests/cryptol/test_quoting` for some examples.
 
 ## 2.12.0 -- 2021-11-19
 

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

@@ -16,6 +16,8 @@
 from . import cryptoltypes
 from . import solver
 from .bitvector import BV
+from .cryptoltypes import fail_with
+from .quoting import cry, cry_f
 from .commands import *
 from .connection import *
 # import everything from `.synchronous` except `connect` and `connect_stdio`
@@ -25,13 +27,4 @@
 from . import synchronous
 sync = synchronous
 
-__all__ = ['bitvector', 'commands', 'connection', 'cryptoltypes', 'opaque', 'single_connection', 'solver', 'synchronous']
-
-
-def fail_with(x : Exception) -> NoReturn:
-    "Raise an exception. This is valid in expression positions."
-    raise x
-
-
-def cry(string : str) -> cryptoltypes.CryptolCode:
-    return cryptoltypes.CryptolLiteral(string)
+__all__ = ['bitvector', 'commands', 'connection', 'cryptoltypes', 'opaque', 'quoting', 'single_connection', 'solver', 'synchronous']

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

@@ -9,6 +9,8 @@
 
 import argo_client.interaction as argo
 from argo_client.connection import DynamicSocketProcess, ServerConnection, ServerProcess, StdIOProcess, HttpProcess
+from .custom_fstring import *
+from .quoting import *
 from . import cryptoltypes
 from . import solver
 from .commands import *
@@ -217,21 +219,35 @@ def eval_raw(self, expression : Any, *, timeout:Optional[float] = None) -> argo.
 
         :param timeout: Optional timeout for this request (in seconds).
         """
+        if hasattr(expression, '__to_cryptol__'):
+            expression = cryptoltypes.to_cryptol(expression)
         timeout = timeout if timeout is not None else self.timeout
         self.most_recent_result = CryptolEvalExprRaw(self, expression, timeout)
         return self.most_recent_result
 
     def eval(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
-        """Evaluate a Cryptol expression, represented according to
-        :ref:`cryptol-json-expression`, with Python datatypes standing
-        for their JSON equivalents.
+        """Evaluate a Cryptol expression, with the result represented
+        according to :ref:`cryptol-json-expression`, with Python datatypes
+        standing for their JSON equivalents.
 
         :param timeout: Optional timeout for this request (in seconds).
         """
+        if hasattr(expression, '__to_cryptol__'):
+            expression = cryptoltypes.to_cryptol(expression)
         timeout = timeout if timeout is not None else self.timeout
         self.most_recent_result = CryptolEvalExpr(self, expression, timeout)
         return self.most_recent_result
 
+    def eval_f(self, s : str, *, timeout:Optional[float] = None) -> argo.Command:
+        """Parses the given string like ``cry_f``, then evalues it, with the
+        result represented according to :ref:`cryptol-json-expression`, with
+        Python datatypes standing for their JSON equivalents.
+
+        :param timeout: Optional timeout for this request (in seconds).
+        """
+        expression = to_cryptol_str_customf(s, frames=1, filename="<eval_f>")
+        return self.eval(expression, timeout=timeout)
+
     def evaluate_expression(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
         """Synonym for member method ``eval``.
 
@@ -251,7 +267,7 @@ def call_raw(self, fun : str, *args : List[Any], timeout:Optional[float] = None)
         ``from_cryptol_arg`` on the ``.result()``.
         """
         timeout = timeout if timeout is not None else self.timeout
-        encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args]
+        encoded_args = [cryptoltypes.to_cryptol(a) for a in args]
         self.most_recent_result = CryptolCallRaw(self, fun, encoded_args, timeout)
         return self.most_recent_result
 
@@ -260,7 +276,7 @@ def call(self, fun : str, *args : List[Any], timeout:Optional[float] = None) ->
 
         :param timeout: Optional timeout for this request (in seconds)."""
         timeout = timeout if timeout is not None else self.timeout
-        encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args]
+        encoded_args = [cryptoltypes.to_cryptol(a) for a in args]
         self.most_recent_result = CryptolCall(self, fun, encoded_args, timeout)
         return self.most_recent_result
 

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

@@ -13,16 +13,59 @@
 
 A = TypeVar('A')
 
+def is_parenthesized(s : str) -> bool:
+    """Returns ``True`` iff the given string has balanced parentheses and is
+       enclosed in a matching pair of parentheses.
+
+       :examples:
+
+       >>> is_parenthesized(' ((a) b )')
+       True
+       >>> is_parenthesized('(a) (b)')
+       False
+       >>> is_parenthesized('(a')
+       False
+       """
+    seen_one, depth = False, 0
+    for c in s:
+        if depth > 0:
+            if c == '(': depth += 1
+            if c == ')': depth -= 1
+        else: # depth == 0
+            if c == '(':
+                if not seen_one: seen_one, depth = True, 1
+                # A new left paren after all parens have been closed means our
+                #  string is not enclosed in a matching pair of parentheses
+                else: return False
+            if c == ')':
+                # A right paren with no matching left means our string does
+                #  not have balanced parentheses
+                return False
+    # Return True if in the end all parentheses are balanced and we've seen at
+    #  least one matching pair
+    return seen_one and depth == 0
+
+def parenthesize(s : str) -> str:
+    """Encloses the given string ``s`` in parentheses if
+       ``is_parenthesized(s)`` is ``False``"""
+    return s if is_parenthesized(s) else f'({s})'
+
+
 class CryptolJSON(Protocol):
     def __to_cryptol__(self, ty : CryptolType) -> Any: ...
 
 class CryptolCode(metaclass=ABCMeta):
-    def __call__(self, other : CryptolJSON) -> CryptolCode:
-        return CryptolApplication(self, other)
+    def __call__(self, *others : CryptolJSON) -> CryptolCode:
+        if all(hasattr(other, '__to_cryptol__') for other in others):
+            return CryptolApplication(self, *others)
+        else:
+            raise ValueError("Argument to __call__ on CryptolCode is not CryptolJSON")
 
     @abstractmethod
     def __to_cryptol__(self, ty : CryptolType) -> Any: ...
 
+    @abstractmethod
+    def __str__(self) -> str: ...
 
 class CryptolLiteral(CryptolCode):
     def __init__(self, code : str) -> None:
@@ -31,6 +74,14 @@ def __init__(self, code : str) -> None:
     def __to_cryptol__(self, ty : CryptolType) -> Any:
         return self._code
 
+    def __str__(self) -> str:
+        return self._code
+
+    def __eq__(self, other : Any) -> bool:
+        return isinstance(other, CryptolLiteral) and self._code == other._code
+
+    def __repr__(self) -> str:
+        return f'CryptolLiteral({self._code!r})'
 
 class CryptolApplication(CryptolCode):
     def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None:
@@ -42,6 +93,19 @@ def __to_cryptol__(self, ty : CryptolType) -> Any:
                 'function': to_cryptol(self._rator),
                 'arguments': [to_cryptol(arg) for arg in self._rands]}
 
+    def __str__(self) -> str:
+        if len(self._rands) == 0:
+            return str(self._rator)
+        else:
+            return ' '.join(parenthesize(str(x)) for x in [self._rator, *self._rands])
+
+    def __eq__(self, other : Any) -> bool:
+        return isinstance(other, CryptolApplication) and self._rator == other._rator and self._rands == other._rands
+
+    def __repr__(self) -> str:
+        return f'CryptolApplication({", ".join(repr(x) for x in [self._rator, *self._rands])})'
+
+
 class CryptolArrowKind:
     def __init__(self, dom : CryptolKind, ran : CryptolKind):
         self.domain = dom

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

@@ -0,0 +1,79 @@
+"""An interface for defining custom f-string wrappers"""
+
+from typing import Any, Callable, Dict, List
+import builtins
+import ast
+import sys
+
+def customf(body : str, onAST : Callable[[ast.FormattedValue], List[ast.expr]],
+            globals : Dict[str, Any] = {}, locals : Dict[str, Any] = {},
+            *, frames : int = 0, filename : str = "<custom f-string>") -> str:
+    """This function parses the given string as if it were an f-string,
+    applies the given function to the AST of each of the formatting fields in
+    the string, then evaluates the result to get the resulting string.
+
+    By default, the global and local variables used in the call to ``eval``
+    are the value of ``sys.__getframe(1+frames).f_globals`` and the value of
+    ``sys.__getframe(1+frames).f_locals``, respectively. This is meant to
+    ensure that the all the variables which were in scope when the custom
+    f-string is formed are also in scope when it is evaluated. Thus, the value
+    of ``frames`` should be incremented for each wrapper function defined
+    around this function (e.g. see the definition of ``func_customf``).
+
+    To add additional global or local variable values (which are combined with,
+    but take precedence over, the values mentioned in the previous paragraph)
+    use the ``globals`` and ``locals`` keyword arguments.
+    """
+    # Get the global/local variable context of the previous frame so the local
+    #  names 'body', 'onAST', etc. aren't shadowed our the call to ``eval``
+    previous_frame = sys._getframe(1 + frames)
+    all_globals = {**previous_frame.f_globals, **globals}
+    all_locals = {**previous_frame.f_locals, **locals}
+    # The below line should be where any f-string syntax errors are raised
+    tree = ast.parse('f' + str(repr(body)), filename=filename, mode='eval')
+    if not isinstance(tree, ast.Expression) or not isinstance(tree.body, ast.JoinedStr):
+       raise ValueError(f'Invalid custom f-string: {str(repr(body))}')
+    joined_values : List[ast.expr] = []
+    for node in tree.body.values:
+        if isinstance(node, ast.FormattedValue):
+            joined_values += onAST(node)
+        else:
+            joined_values += [node]
+    tree.body.values = joined_values
+    try:
+        return str(eval(compile(tree, filename=filename, mode='eval'), all_globals, all_locals))
+    except SyntaxError as e:
+        # I can't think of a case where we would raise an error here, but if
+        # we do it's worth telling the user that the column numbers are all
+        # messed up
+        msg = '\nNB: Column numbers refer to positions in the original string'
+        raise type(e)(str(e) + msg).with_traceback(sys.exc_info()[2])
+
+def func_customf(body : str, func : Callable,
+                 globals : Dict[str, Any] = {}, locals : Dict[str, Any] = {},
+                 *, frames : int = 0,  filename : str = "<custom f-string>",
+                    doConvFmtAfter : bool = False,
+                    func_id : str = "_func_customf__func_id") -> str:
+    """Like ``customf``, but can be provided a function to apply to the values
+    of each of the formatting fields before they are formatted as strings,
+    instead of a function applied to their ASTs.
+
+    Unless the parameter ``doConvFmtAfter`` is set to ``True``, any conversions
+    (i.e. ``{...!s}``, ``{...!r}``, or ``{...!a}``) or format specifiers
+    (e.g. ``{...:>30}`` or ``{...:+f}``) in the input string will be applied
+    before the given function is applied. For example,
+    ``func_customf('{5!r}', f)`` is the same as ``f'{f(repr(5))}'``, but
+    ``func_customf('{5!r}', f, doConvFmtAfter=True)`` is ``f'{repr(f(5))}'``.
+    """
+    def onAST(node : ast.FormattedValue) -> List[ast.expr]:
+        kwargs = {'lineno': node.lineno, 'col_offset': node.col_offset}
+        func = ast.Name(id=func_id, ctx=ast.Load(), **kwargs)
+        if doConvFmtAfter or (node.conversion == -1 and node.format_spec is None):
+            node.value = ast.Call(func=func, args=[node.value], keywords=[], **kwargs)
+        else:
+            node_str = ast.JoinedStr(values=[node], **kwargs)
+            node_val = ast.Call(func=func, args=[node_str], keywords=[], **kwargs)
+            node = ast.FormattedValue(value=node_val, conversion=-1, format_spec=None, **kwargs)
+        return [node]
+    return customf(body, onAST, globals, {**locals, func_id:func}, frames=1+frames,
+                                                                   filename=filename)

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

@@ -0,0 +1,84 @@
+"""Cryptol quasiquotation using an f-string-like syntax"""
+
+from typing import Any, Union
+
+from .bitvector import BV
+from .opaque import OpaqueValue
+from .commands import CryptolValue
+from .cryptoltypes import CryptolCode, CryptolLiteral, parenthesize
+from .custom_fstring import *
+
+def to_cryptol_str(val : Union[CryptolValue, str, CryptolCode]) -> str:
+    """Converts a ``CryptolValue``, string literal, or ``CryptolCode`` into
+       a string of cryptol syntax."""
+    if isinstance(val, bool):
+        return 'True' if val else 'False'
+    elif isinstance(val, tuple):
+        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()) + '}'
+    elif isinstance(val, int):
+        return str(val)
+    elif isinstance(val, list):
+        return '[' + ', '.join(to_cryptol_str(x) for x in val) + ']'
+    elif isinstance(val, BV):
+        if 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}"'
+    elif isinstance(val, CryptolCode):
+        return parenthesize(str(val))
+    else:
+        raise TypeError("Unable to convert value to Cryptol syntax: " + str(val))
+
+def to_cryptol_str_customf(s : str, *, frames : int = 0,
+                                       filename : str = "<cry_f>") -> str:
+    """The function used to parse strings given to ``cry_f``"""
+    return func_customf(s, to_cryptol_str, frames=1+frames,
+                                           filename=filename)
+
+def cry(s : str) -> CryptolLiteral:
+    """Embed a string of cryptol syntax as ``CryptolCode``"""
+    return CryptolLiteral(s)
+
+def cry_f(s : str) -> CryptolLiteral:
+    """Embed a string of cryptol syntax as ``CryptolCode``, where the given
+       string is parsed as an f-string, and the values within brackets are
+       converted to cryptol syntax using ``to_cryptol_str``.
+
+       Like f-strings, values in brackets (``{``, ``}``) are parsed as python
+       expressions in the caller's context of local and global variables, and
+       to include a literal bracket in the final string, it must be doubled
+       (i.e. ``{{`` or ``}}``). The latter is needed when using explicit type
+       application or record syntax. For example, if ``x = [0,1]`` then
+       ``cry_f('length `{{2}} {x}')`` is equal to ``cry('length `{2} [0,1]')``
+       and ``cry_f('{{ x = {x} }}')`` is equal to ``cry('{ x = [0,1] }')``.
+
+       When formatting Cryptol, it is recomended to use this function rather
+       than any of python's built-in methods of string formatting (e.g.
+       f-strings, ``str.format``) as the latter will not always produce valid
+       cryptol syntax. Specifically, this function differs from these methods
+       in the cases of ``BV``s, string literals, function application (this
+       function will add parentheses as needed), and dicts. For example,
+       ``cry_f('{ {"x": 5, "y": 4} }')`` equals ``cry('{x = 5, y = 4}')``
+       but ``f'{ {"x": 5, "y": 4} }'`` equals ``'{"x": 5, "y": 4}'``. Only
+       the former is valid cryptol syntax for a record.
+
+       Note that any conversion or format specifier will always result in the
+       argument being rendered as a cryptol string literal with the conversion
+       and/or formating applied. For example, `cry('f {5}')` is equal to
+       ``cry('f 5')`` but ``cry_f('f {5!s}')`` is equal to ``cry(`f "5"`)``
+       and ``cry_f('f {5:+.2%}')`` is equal to ``cry('f "+500.00%"')``.
+
+       :example:
+
+       >>> x = BV(size=7, value=1)
+       >>> y = cry_f('fun1 {x}')
+       >>> cry_f('fun2 {y}')
+       'fun2 (fun1 (1 : [7]))'
+    """
+    return CryptolLiteral(to_cryptol_str_customf(s, frames=1))

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

@@ -6,6 +6,8 @@
 from typing import Any, Optional, Union, List, Dict, TextIO, overload
 from typing_extensions import Literal
 
+from .custom_fstring import *
+from .quoting import *
 from .solver import OfflineSmtQuery, Solver, OnlineSolver, OfflineSolver, Z3
 from .connection import CryptolValue, CheckReport
 from . import synchronous
@@ -144,6 +146,14 @@ def cry_eval(expression : Any, *, timeout:Optional[float] = None) -> CryptolValu
     """
     return __get_designated_connection().eval(expression, timeout=timeout)
 
+def cry_eval_f(s : str, *, timeout:Optional[float] = None) -> CryptolValue:
+    """Parses the given string like ``cry_f``, then evalues it, with the
+    result represented according to :ref:`cryptol-json-expression`, with
+    Python datatypes standing for their JSON equivalents.
+    """
+    expression = to_cryptol_str_customf(s, frames=1, filename="<cry_eval_f>")
+    return cry_eval(expression, timeout=timeout)
+
 def call(fun : str, *args : List[Any], timeout:Optional[float] = None) -> CryptolValue:
     """Evaluate a Cryptol functiom by name, with the arguments and the
     result represented according to :ref:`cryptol-json-expression`, with