Merge pull request #1397 from GaloisInc/at-rpc-java

Add Java support to RPC API

saw-remote-api/docs/SAW.rst

@@ -132,6 +132,119 @@ No return fields
 
 
 
+SAW/JVM/load class (command)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Load the JVM class with the given name for later verification.
+
+Parameter fields
+++++++++++++++++
+
+
+``name``
+  The name of the class on the server.
+
+
+
+``class name``
+  The java class to load.
+
+
+
+Return fields
++++++++++++++
+
+No return fields
+
+
+
+SAW/JVM/verify (command)
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+Verify the named JVM method meets its specification.
+
+Parameter fields
+++++++++++++++++
+
+
+``module``
+  The module of the function being verified.
+
+
+
+``function``
+  The function being verified.
+
+
+
+``lemmas``
+  The specifications to use for other functions during this verification.
+
+
+
+``check sat``
+  Whether or not to enable path satisfiability checking.
+
+
+
+``contract``
+  The specification to verify for the function.
+
+
+
+``script``
+  The script to use to prove the validity of the resulting verification conditions.
+
+
+
+``lemma name``
+  The name to refer to this verification/contract by later.
+
+
+
+Return fields
++++++++++++++
+
+No return fields
+
+
+
+SAW/JVM/assume (command)
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+Assume the named JVM method meets its specification.
+
+Parameter fields
+++++++++++++++++
+
+
+``module``
+  The LLVM  module containing the function.
+
+
+
+``function``
+  The function we are assuming a contract for.
+
+
+
+``contract``
+  The specification to assume for the function.
+
+
+
+``lemma name``
+  The name to refer to this assumed contract by later.
+
+
+
+Return fields
++++++++++++++
+
+No return fields
+
+
+
 SAW/LLVM/load module (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

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

@@ -381,6 +381,130 @@ def create_ghost_variable(name: str) -> llvm.GhostVariable:
     return llvm.GhostVariable(name, server_name)
 
 
+@dataclass
+class JVMClass:
+    class_name: str
+    server_name: str
+
+
+def jvm_load_class(class_name: str) -> JVMClass:
+    name = __fresh_server_name(class_name)
+    __get_designated_connection().jvm_load_class(name, class_name).result()
+    return JVMClass(class_name, name)
+
+# TODO: this is almost identical to llvm_assume. Can we reduce duplication?
+def jvm_assume(cls: JVMClass,
+               method_name: str,
+               contract: llvm.Contract,
+               lemma_name_hint: Optional[str] = None) -> VerificationResult:
+    """Assume that the given method satisfies the given contract. Returns an
+    override linking the method and contract that can be passed as an
+    argument in calls to `jvm_verify`
+    """
+    if lemma_name_hint is None:
+        lemma_name_hint = contract.__class__.__name__ + "_" + method_name
+    name = __fresh_server_name(lemma_name_hint)
+
+    result: VerificationResult
+    try:
+        conn = __get_designated_connection()
+        res = conn.jvm_assume(cls.class_name,
+                              method_name,
+                              contract.to_json(),
+                              name)
+        result = AssumptionSucceeded(server_name=name,
+                                     contract=contract,
+                                     stdout=res.stdout(),
+                                     stderr=res.stderr())
+        __global_success = True
+        # If something stopped us from even **assuming**...
+    except exceptions.VerificationError as err:
+        __global_success = False
+        result = AssumptionFailed(server_name=name,
+                                  assumptions=[],
+                                  contract=contract,
+                                  exception=err)
+    except Exception as err:
+        __global_success = False
+        for view in __designated_views:
+            view.on_python_exception(err)
+        raise err from None
+
+    return result
+
+# TODO: this is almost identical to llvm_verify. Can we reduce duplication?
+def jvm_verify(cls: JVMClass,
+               method_name: str,
+               contract: llvm.Contract,
+               lemmas: List[VerificationResult] = [],
+               check_sat: bool = False,
+               script: Optional[proofscript.ProofScript] = None,
+               lemma_name_hint: Optional[str] = None) -> VerificationResult:
+    """Verify that the given method satisfies the given contract. Returns an
+    override linking the method and contract that can be passed as an
+    argument in further calls to `jvm_verify`
+    """
+
+    if script is None:
+        script = proofscript.ProofScript([proofscript.z3([])])
+    if lemma_name_hint is None:
+        lemma_name_hint = contract.__class__.__name__ + "_" + method_name
+
+    name = __fresh_server_name(lemma_name_hint)
+
+    result: VerificationResult
+    conn = __get_designated_connection()
+
+    global __global_success
+    global __designated_views
+
+    try:
+        res = conn.jvm_verify(cls.class_name,
+                              method_name,
+                              [l.server_name for l in lemmas],
+                              check_sat,
+                              contract.to_json(),
+                              script.to_json(),
+                              name)
+
+        stdout = res.stdout()
+        stderr = res.stderr()
+        result = VerificationSucceeded(server_name=name,
+                                       assumptions=lemmas,
+                                       contract=contract,
+                                       stdout=stdout,
+                                       stderr=stderr)
+    # If the verification did not succeed...
+    except exceptions.VerificationError as err:
+        # FIXME add the goal as an assumption if it failed...?
+        result = VerificationFailed(server_name=name,
+                                    assumptions=lemmas,
+                                    contract=contract,
+                                    exception=err)
+    # If something else went wrong...
+    except Exception as err:
+        __global_success = False
+        for view in __designated_views:
+            view.on_python_exception(err)
+        raise err from None
+
+    # Log or otherwise process the verification result
+    for view in __designated_views:
+        if isinstance(result, VerificationSucceeded):
+            view.on_success(result)
+        elif isinstance(result, VerificationFailed):
+            view.on_failure(result)
+
+    # Note when any failure occurs
+    __global_success = __global_success and result.is_success()
+
+    # Abort the proof if we failed to assume a failed verification, otherwise
+    # return the result of the verification
+    if isinstance(result, AssumptionFailed):
+        raise result.exception from None
+
+    return result
+
 @dataclass
 class LLVMModule:
     bitcode_file: str
@@ -435,13 +559,11 @@ def llvm_assume(module: LLVMModule,
 def llvm_verify(module: LLVMModule,
                 function: str,
                 contract: llvm.Contract,
-                lemmas: Optional[List[VerificationResult]] = None,
+                lemmas: List[VerificationResult] = [],
                 check_sat: bool = False,
                 script: Optional[proofscript.ProofScript] = None,
                 lemma_name_hint: Optional[str] = None) -> VerificationResult:
 
-    if lemmas is None:
-        lemmas = []
     if script is None:
         script = proofscript.ProofScript([proofscript.z3([])])
     if lemma_name_hint is None:

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

@@ -98,6 +98,59 @@ def __init__(
     def process_result(self, res : Any) -> Any:
         return res
 
+class JVMLoadClass(SAWCommand):
+    def __init__(self, connection : argo.HasProtocolState,
+                 name : str,
+                 class_name : str) -> None:
+        super(JVMLoadClass, self).__init__(
+            'SAW/JVM/load class',
+            {'name': name, 'class name': class_name},
+            connection
+        )
+
+    def process_result(self, res : Any) -> Any:
+        return res
+
+class JVMAssume(SAWCommand):
+    def __init__(
+            self,
+            connection : argo.HasProtocolState,
+            module : str,
+            function : str,
+            setup : Any,
+            lemma_name : str) -> None:
+        params = {'module': module,
+                  'function': function,
+                  'contract': setup,
+                  'lemma name': lemma_name}
+        super(JVMAssume, self).__init__('SAW/JVM/assume', params, connection)
+
+    def process_result(self, _res : Any) -> Any:
+        return None
+
+class JVMVerify(SAWCommand):
+    def __init__(
+            self,
+            connection : argo.HasProtocolState,
+            class_name : str,
+            method_name : str,
+            lemmas : List[str],
+            check_sat : bool,
+            setup : Any,
+            script : ProofScript,
+            lemma_name : str) -> None:
+        params = {'module': class_name,
+                  'function': method_name,
+                  'lemmas': lemmas,
+                  'check sat': check_sat,
+                  'contract': setup,
+                  'script': script,
+                  'lemma name': lemma_name}
+        super(JVMVerify, self).__init__('SAW/JVM/verify', params, connection)
+
+    def process_result(self, res : Any) -> Any:
+        return res
+
 class Prove(SAWCommand):
     def __init__(
             self,

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

@@ -158,6 +158,43 @@ def create_ghost_variable(self, name: str, server_name: str) -> Command:
         self.most_recent_result = CreateGhostVariable(self, name, server_name)
         return self.most_recent_result
 
+    def jvm_load_class(self, name: str, class_name: str)  -> Command:
+        """Create an instance of the `JVMLoadClass` command. Documentation on the purpose
+        and use of this command is associated with the top-level `jvm_load_class`
+        function.
+        """
+        self.most_recent_result = JVMLoadClass(self, name, class_name)
+        return self.most_recent_result
+
+    def jvm_verify(self,
+                   class_name: str,
+                   method_name: str,
+                   lemmas: List[str],
+                   check_sat: bool,
+                   contract: Any,
+                   script: ProofScript,
+                   lemma_name: str) -> Command:
+        """Create an instance of the `JVMVerify` command. Documentation on the purpose
+        and use of this command is associated with the top-level `jvm_assume`
+        function.
+        """
+        self.most_recent_result = \
+            JVMVerify(self, class_name, method_name, lemmas, check_sat, contract, script, lemma_name)
+        return self.most_recent_result
+
+    def jvm_assume(self,
+                   class_name: str,
+                   method_name: str,
+                   contract: Any,
+                   lemma_name: str) -> Command:
+        """Create an instance of the `JVMAssume` command. Documentation on the purpose
+        and use of this command is associated with the top-level `jvm_assume`
+        function.
+        """
+        self.most_recent_result = \
+            JVMAssume(self, class_name, method_name, contract, lemma_name)
+        return self.most_recent_result
+
     def llvm_load_module(self, name: str, bitcode_file: str)  -> Command:
         self.most_recent_result = LLVMLoadModule(self, name, bitcode_file)
         return self.most_recent_result