Add an eval_int command to the remote API and Python interface

saw-remote-api/CHANGELOG.md

@@ -1,6 +1,5 @@
 # Revision history for saw-remote-api
 
-
 ## 0.9.1 -- YYYY-MM-DD
 
 * `SAW/set option`'s `"option"` parameter is now allowed to be `"What4 eval"`,
@@ -16,7 +15,8 @@
   verification, so JVM specifications must leave these lists empty. Attempting
   to provide a non-empty list for either of these fields in a JVM specification
   will result in an error.
-
+* Introduced new methods `SAW/eval int` and `SAW/eval bool` that allow the
+  evaluation of Cryptol expressions into Python values.
 
 ## 0.9.0 -- 2021-11-19
 

saw-remote-api/docs/SAW.rst

@@ -505,6 +505,54 @@ Return fields
 
 
 
+SAW/eval int (command)
+~~~~~~~~~~~~~~~~~~~~~~
+
+Attempt to evaluate the given term to a concrete integer.
+
+Parameter fields
+++++++++++++++++
+
+
+``expr``
+  The Cryptol expression to evaluate.
+
+
+
+Return fields
++++++++++++++
+
+
+``value``
+  The integer value of the expresssion.
+
+
+
+
+SAW/eval bool (command)
+~~~~~~~~~~~~~~~~~~~~~~~
+
+Attempt to evaluate the given term to a concrete boolean.
+
+Parameter fields
+++++++++++++++++
+
+
+``expr``
+  The Cryptol expression to evaluate.
+
+
+
+Return fields
++++++++++++++
+
+
+``value``
+  The boolean value of the expresssion.
+
+
+
+
 SAW/set option (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~
 

saw-remote-api/python/CHANGELOG.md

@@ -13,6 +13,8 @@
   `set_option(LaxLoadsAndStores(), True)` in order for `points_to_bitfield` to
   work as expected. `points_to_bitfield` is only supported for LLVM (and not
   JVM) verification.
+* Added two new commands, `eval_int` and `eval_bool`, that evaluate Cryptol
+  expressions to Python integers or booleans.
 
 
 ## 0.9.0 -- 2021-11-19

saw-remote-api/python/saw_client/__init__.py

@@ -648,6 +648,26 @@ def prove(goal: cryptoltypes.CryptolJSON,
         pr.counterexample = None
     return pr
 
+def eval_int(expr: cryptoltypes.CryptolJSON) -> int:
+    """Atempts to evaluate the given expression as a concrete integer.
+    """
+    conn = __get_designated_connection()
+    res = conn.eval_int(expr).result()
+    v = res['value']
+    if not isinstance(v, int):
+        raise ValueError(str(v) + " is not an integer")
+    return v
+
+def eval_bool(expr: cryptoltypes.CryptolJSON) -> bool:
+    """Atempts to evaluate the given expression as a concrete boolean.
+    """
+    conn = __get_designated_connection()
+    res = conn.eval_bool(expr).result()
+    v = res['value']
+    if not isinstance(v, bool):
+        raise ValueError(str(v) + " is not a boolean")
+    return v
+
 def set_option(option : option.SAWOption, value : bool) -> None:
     """Set a boolean-valued SAW option."""
     global __designated_connection

saw-remote-api/python/saw_client/commands.py

@@ -184,6 +184,30 @@ def __init__(
     def process_result(self, res : Any) -> Any:
         return res
 
+class EvalInt(SAWCommand):
+    def __init__(
+            self,
+            connection : argo.HasProtocolState,
+            expr : cryptoltypes.CryptolJSON,
+            timeout : Optional[float]) -> None:
+        params = {'expr': cryptoltypes.to_cryptol(expr)}
+        super(EvalInt, self).__init__('SAW/eval int', params, connection, timeout=timeout)
+
+    def process_result(self, res : Any) -> Any:
+        return res
+
+class EvalBool(SAWCommand):
+    def __init__(
+            self,
+            connection : argo.HasProtocolState,
+            expr : cryptoltypes.CryptolJSON,
+            timeout : Optional[float]) -> None:
+        params = {'expr': cryptoltypes.to_cryptol(expr)}
+        super(EvalBool, self).__init__('SAW/eval bool', params, connection, timeout=timeout)
+
+    def process_result(self, res : Any) -> Any:
+        return res
+
 class SAWReset(argo.Notification):
     def __init__(self, connection : argo.HasProtocolState) -> None:
         super(SAWReset, self).__init__(

saw-remote-api/python/saw_client/connection.py

@@ -239,6 +239,24 @@ def prove(self,
         self.most_recent_result = Prove(self, goal, proof_script, timeout)
         return self.most_recent_result
 
+    def eval_int(self,
+              expr: cryptoltypes.CryptolJSON,
+              timeout : Optional[float] = None) -> Command:
+        """Create an instance of the `EvalInt` command. Documentation on the purpose and
+        use of this command is associated with the top-level `eval_int` function.
+        """
+        self.most_recent_result = EvalInt(self, expr, timeout)
+        return self.most_recent_result
+
+    def eval_bool(self,
+              expr: cryptoltypes.CryptolJSON,
+              timeout : Optional[float] = None) -> Command:
+        """Create an instance of the `EvalBool` command. Documentation on the purpose and
+        use of this command is associated with the top-level `eval_bool` function.
+        """
+        self.most_recent_result = EvalBool(self, expr, timeout)
+        return self.most_recent_result
+
     def set_option(self,
                    option : SAWOption,
                    value : bool,

saw-remote-api/python/tests/saw/test_eval.py

@@ -0,0 +1,22 @@
+import cryptol
+import saw_client as saw
+
+import unittest
+from pathlib import Path
+
+class ProverTest(unittest.TestCase):
+
+    def test_provers(self):
+        saw.connect(reset_server=True)
+
+        if __name__ == "__main__": saw.view(saw.LogResults())
+
+        expr1 = cryptol.cry_f('(6 : [8]) * 7')
+        self.assertEqual(saw.eval_int(expr1), 42)
+
+        expr2 = cryptol.cry_f('(1 < 2) : Bit')
+        self.assertTrue(saw.eval_bool(expr2))
+
+
+if __name__ == "__main__":
+    unittest.main()

saw-remote-api/saw-remote-api.cabal

@@ -74,6 +74,7 @@ library
                    SAWServer.Data.JVMType,
                    SAWServer.Data.LLVMType,
                    SAWServer.Data.SetupValue,
+                   SAWServer.Eval,
                    SAWServer.Exceptions,
                    SAWServer.Ghost,
                    SAWServer.JVMCrucibleSetup,

saw-remote-api/saw-remote-api/Main.hs

@@ -17,6 +17,11 @@ import SAWServer.CryptolSetup
       cryptolLoadFileDescr,
       cryptolLoadFile )
 import SAWServer.Data.JVMType()
+import SAWServer.Eval
+    ( evalIntDescr,
+      evalInt,
+      evalBoolDescr,
+      evalBool )
 import SAWServer.Ghost
     ( createGhostVariableDescr,
       createGhostVariable )
@@ -117,6 +122,14 @@ sawMethods =
      "SAW/prove"
      proveDescr
      prove
+  , Argo.command
+     "SAW/eval int"
+     evalIntDescr
+     evalInt
+  , Argo.command
+     "SAW/eval bool"
+     evalBoolDescr
+     evalBool
   , Argo.command
      "SAW/set option"
      setOptionDescr