SAW Python missing counterexamples

[phsmenon]

SAW can usually produce counterexamples (and additional details) when verification fails. However, these are not displayed to the user when using SAW through the Python interface.

It would be ideal if using the remote interfaces produced the same level of detail as SAWScript itself.

As an example, consider the following function: https://github.com/signalapp/libsignal-protocol-c/blob/3a83a4f4ed2302ff6e68ab569c88793b50c22d28/src/signal_protocol.c#L605-L611

The following specification (in Python) contains an off-by-one error in the postconditions

class SerializeProtobufSpec(Contract):
    length: int

    def __init__(self, length: int):
        super().__init__()
        self.length = length

    def specification(self) -> None:
        buffer = self.alloc(alias_ty("struct.ProtobufCBinaryData"))

        data = self.fresh_var(array_ty(self.length, i8), "data")
        self.precondition(f"{data.name()} ! 0 == 0")
        for i in range(self.length - 1):
            self.precondition(f"{data.name()} @ {i} > 0")

        stringp = self.alloc(array_ty(self.length, i8), points_to=data)

        self.execute_func(buffer, stringp)

        nval = int_to_64_cryptol(self.length) # Error: off-by-one
        self.points_to(buffer, struct(nval, stringp))
        self.returns(void)

The resulting error is below. It does not really tell you what went wrong.

  Failed to verify: lemma_SerializeProtobufSpec (defined at /home/hari/Work/saw-demos/demos/signal-protocol/python/misc.py:24):
error: Proof failed.
⚠️  Failed to verify: lemma_DeserializeProtobufSpec (defined at /home/hari/Work/saw-demos/demos/signal-protocol/python/misc.py:51):
error: Proof failed.
🛑  All 2 goals failed to verify.
Exception ignored in: <function SAWConnection.__del__ at 0x7f7d621d75e0>
Traceback (most recent call last):
  File "/home/hari/.cache/pypoetry/virtualenvs/signal-protocol-JzAWaEe0-py3.8/lib/python3.8/site-packages/saw_client/connection.py", line 113, in __del__
  File "/home/hari/.cache/pypoetry/virtualenvs/signal-protocol-JzAWaEe0-py3.8/lib/python3.8/site-packages/saw_client/commands.py", line 118, in __init__
  File "/home/hari/.cache/pypoetry/virtualenvs/signal-protocol-JzAWaEe0-py3.8/lib/python3.8/site-packages/saw_client/connection.py", line 137, in protocol_state
  File "/home/hari/.cache/pypoetry/virtualenvs/signal-protocol-JzAWaEe0-py3.8/lib/python3.8/site-packages/argo_client/interaction.py", line 164, in state
  File "/home/hari/.cache/pypoetry/virtualenvs/signal-protocol-JzAWaEe0-py3.8/lib/python3.8/site-packages/argo_client/interaction.py", line 153, in _result_and_state_and_out_err
saw_client.exceptions.VerificationError: error: Proof failed.

A similar spec in SAWScript (with the same error) is below:

let serialize_protobuf_spec (length : Int ) = do {
  sinit <- llvm_fresh_var "sinit" (llvm_array length (llvm_type "i8")) ;
  llvm_precond {{ `length > 0 }} ;
  llvm_precond {{ sinit ! 0 == 0 }} ;
  let terms = eval_list {{ [ (sinit @ k) > 0 | k <- [0 .. (length - 2)]] }} ;
  for terms (\c -> llvm_precond c) ;
  
  stringp <- alloc_init (llvm_array length (llvm_type "i8")) (llvm_term sinit);
  
  (binit, buffer) <- ptr_to_fresh "buffer" (llvm_alias "struct.ProtobufCBinaryData");
  llvm_points_to (llvm_elem stringp length) (llvm_term {{ 0 : [8] }}) ;
  
  llvm_execute_func [buffer, stringp];
  
  llvm_points_to (llvm_field buffer "data") stringp ;
  llvm_points_to (llvm_field buffer "len") (llvm_term {{ (`length ):[64] }}) ; //Error: off-by-one
};

This produces a better error message that includes a counter example:

[17:40:53.010] Subgoal failed: signal_protocol_str_serialize_protobuf safety assertion:
/home/hari/Work/saw-demos/demos/signal-protocol/saw/protocol.saw:216:26: error: in _SAW_verify_prestate
Literal equality postcondition
Expected term: Cryptol.ecNumber (Cryptol.TCNum 32) (Prelude.Vec 64 Prelude.Bool)
  (Cryptol.PLiteralSeqBool (Cryptol.TCNum 64))
Actual term:   let { x@1 = Prelude.Vec 64 Prelude.Bool
      x@2 = Prelude.bvNat 64 0
      x@3 = Prelude.Vec 8 Prelude.Bool
      x@4 = Prelude.bvNat 8 0
    }
 in Prelude.ite x@1 (Prelude.bvEq 8 x@4 (Prelude.at 32 x@3 fresh:sinit#821 0))
      x@2
      (Prelude.ite x@1
         (Prelude.bvEq 8 x@4 (Prelude.at 32 x@3 fresh:sinit#821 1))
         (Prelude.bvNat 64 1)
         (Prelude.ite x@1
            (Prelude.bvEq 8 x@4 (Prelude.at 32 x@3 fresh:sinit#821 2))
            (Prelude.bvNat 64 2)
            (Prelude.ite x@1
               (Prelude.bvEq 8 x@4 (Prelude.at 32 x@3 fresh:sinit#821 3))
               (Prelude.bvNat 64 3)
               (Prelude.ite x@1
                  (Prelude.bvEq 8 x@4 (Prelude.at 32 x@3 fresh:sinit#821 4))
                  (Prelude.bvNat 64 4)
                  (Prelude.ite x@1
                     (Prelude.bvEq 8 x@4 (Prelude.at 32 x@3 fresh:sinit#821 5))
                     (Prelude.bvNat 64 5)
                     (Prelude.ite x@1
                        (Prelude.bvEq 8 x@4
                           (Prelude.at 32 x@3 fresh:sinit#821 6))
                        (Prelude.bvNat 64 6)
                        (Prelude.ite x@1
                           (Prelude.bvEq 8 x@4
                              (Prelude.at 32 x@3 fresh:sinit#821 7))
                           (Prelude.bvNat 64 7)
                           (Prelude.ite x@1
                              (Prelude.bvEq 8 x@4
                                 (Prelude.at 32 x@3 fresh:sinit#821 8))
                              (Prelude.bvNat 64 8)
                              (Prelude.ite x@1
                                 (Prelude.bvEq 8 x@4
                                    (Prelude.at 32 x@3 fresh:sinit#821 9))
                                 (Prelude.bvNat 64 9)
                                 (Prelude.ite x@1
                                    (Prelude.bvEq 8 x@4
                                       (Prelude.at 32 x@3 fresh:sinit#821 10))
                                    (Prelude.bvNat 64 10)
                                    (Prelude.ite x@1
                                       (Prelude.bvEq 8 x@4
                                          (... ... x@3 fresh:sinit#821 11))
                                       (Prelude.bvNat 64 11)
                                       (Prelude.ite x@1
                                          (Prelude.bvEq 8 x@4
                                             (... ... fresh:sinit#821 12))
                                          (Prelude.bvNat 64 12)
                                          (Prelude.ite x@1
                                             (... ... x@4 (... ... 13))
                                             (Prelude.bvNat 64 13)
                                             (Prelude.ite x@1
                                                (... ... (... ...))
                                                (Prelude.bvNat 64 14)
                                                (... ... (... ...) (... ... 15)
                                                   (... ... (... ...)
                                                      (... ...
                                                         (...
                                                            ...))))))))))))))))))


[17:40:53.011] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 1385}
[17:40:53.012] ----------Counterexample----------
[17:40:53.012]   sinit: [255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
255,
0]
[17:40:53.013] ----------------------------------
[17:40:53.013] Stack trace:
"include" (/home/hari/Work/saw-demos/demos/signal-protocol/saw/main.saw:3:1-3:8):
"llvm_verify" (/home/hari/Work/saw-demos/demos/signal-protocol/saw/protocol.saw:216:26-216:37):
"crucible_llvm_verify" (/home/hari/Work/saw-demos/demos/signal-protocol/saw/saw_helpers.saw:59:8-59:28):
Proof failed.
make: *** [Makefile:14: all-saw-script] Error 2

[RyanGlScott]

As a sanity check, are you using view(LogResults(verbose_failure=True))? I ask since I instead used view(LogResults()) in unrelated work, which caused SAW to omit important details about the failure. I'm not sure if the issue you're experiencing would be revealed by enabling verbose_failure=True, but it would be worth a shot.

[RyanGlScott]

I'm guessing that the context of this issue is GaloisInc/saw-demos#11, which adds SerializeProtobufSpec. Indeed, if I run that with the following changes:

diff --git a/demos/signal-protocol/python/load.py b/demos/signal-protocol/python/load.py
index e046b09..0612301 100644
--- a/demos/signal-protocol/python/load.py
+++ b/demos/signal-protocol/python/load.py
@@ -6,7 +6,8 @@ from saw_client import LogResults, connect, llvm_load_module, view
 dir_path = os.path.dirname(os.path.realpath(__file__))
 
 connect()
-view(LogResults(verbose_failure=True))
+# view(LogResults(verbose_failure=True))
+view(LogResults())
 
 path = [os.path.dirname(dir_path), "c", "libsignal-everything.bc"]
 bcname = os.path.join(*path)
diff --git a/demos/signal-protocol/python/signal_protocol.py b/demos/signal-protocol/python/signal_protocol.py
index b3f2a14..4b47eae 100644
--- a/demos/signal-protocol/python/signal_protocol.py
+++ b/demos/signal-protocol/python/signal_protocol.py
@@ -196,7 +196,7 @@ class SerializeProtobufSpec(Contract):
 
         self.execute_func(buffer, stringp)
 
-        nval = int_to_64_cryptol(self.length - 1)
+        nval = int_to_64_cryptol(self.length) # Error: off-by-one
         self.points_to(buffer, struct(nval, stringp))
         self.returns(void)
 

Then I observe the original error. If I use view(LogResults(verbose_failure=True)) instead, however, I get a counterexample quite similar to the SAWScript one. Granted, it's pretty lengthy, so there is perhaps a question to be asked about whether verbose_failure failure should be the default or not. If we decide to keep verbose_failure=False the default, then at the very least we should add a disclaimer to the abridged error message that (1) some additional information was suppressed, and (2) explain how a user can enable the additional information if they so choose.