saw-remote-api: No explanation printed when allocating insufficient memory

[RyanGlScott]

I recently made a mistake when coming up with a specification using the Python bindings to SAW:

// alloc_aligned.c
#include <stddef.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

struct buffer {
    size_t len;
    uint8_t data[];
};

typedef struct buffer buffer;

buffer *buffer_alloc(size_t len)
{
    buffer *buf = malloc(sizeof(struct buffer) + (sizeof(uint8_t) * len));
    if(buf) {
        buf->len = len;
    }
    return buf;
}

buffer *buffer_create(const uint8_t *data, size_t len)
{
    buffer *buf = buffer_alloc(len);
    if(!buf) {
        return 0;
    }

    memcpy(buf->data, data, len);
    return buf;
}

buffer *buffer_copy(const buffer *buf)
{
    return buffer_create(buf->data, buf->len);
}

# bug.py
from saw import *
from saw.llvm import Contract, SetupVal, cryptol, struct
from saw.llvm_types import LLVMType, array, i8


dir_path = os.path.dirname(os.path.realpath(__file__))

server = os.environ.get('SAW_SERVER')
if not server:
    server = "cabal new-exec --verbose=0 saw-remote-api socket"
print("Running: " + server)
connect(server)
view(LogResults())


def int_to_64_cryptol(length: int):
    return cryptol("`{i}:[64]".format(i=length))


def buffer_type(length: int) -> LLVMType:
    return array(8 + length, i8)


def alloc_buffer_aligned(spec: Contract, length: int) -> SetupVal:
    return spec.alloc(buffer_type(16), alignment = 16)


def alloc_buffer_aligned_readonly(spec: Contract, length: int) -> SetupVal:
    return spec.alloc(buffer_type(16), alignment = 16, read_only = True)
    # return spec.alloc(buffer_type(length), alignment = 16, read_only = True)


def alloc_pointsto_buffer(spec: Contract, length: int, data: SetupVal) -> SetupVal:
    buf = alloc_buffer_aligned(spec, length)
    spec.points_to(buf, struct(int_to_64_cryptol(length)), check_target_type = None)
    return buf


def alloc_pointsto_buffer_readonly(spec: Contract, length: int, data: SetupVal) -> SetupVal:
    buf = alloc_buffer_aligned_readonly(spec, length)
    spec.points_to(buf, struct(int_to_64_cryptol(length)), check_target_type = None)
    return buf


class BufferCopySpec(Contract):
    length: int

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

    def specification(self) -> None:
        data = self.fresh_var(array(self.length, i8), "data")
        buf  = alloc_pointsto_buffer_readonly(self, self.length, data)

        self.execute_func(buf)

        new_buf = alloc_pointsto_buffer(self, self.length, data)
        self.returns(new_buf)


path = [dir_path, "alloc_aligned.bc"]
bcname = os.path.join(*path)
mod = llvm_load_module(bcname)

llvm_verify(mod, 'buffer_copy', BufferCopySpec(63))

The mistake is that I wrote return spec.alloc(buffer_type(16), alignment = 16, read_only = True) instead of the commented-out line below it (return spec.alloc(buffer_type(length), alignment = 16, read_only = True)). However, the error message that was produced did not make this at all obvious:

$ clang -g -c -emit-llvm alloc_aligned.c
$ python bug.py
Running: cabal new-exec --verbose=0 saw-remote-api socket
⚠️  Failed to verify: lemma_BufferCopySpec (defined at bug.py:50):
error: Proof failed.
🛑  The goal failed to verify.

Compare this to an equivalent SAWScript program:

// bug.saw
let i8 = llvm_int 8;

let buffer_type (len : Int) : LLVMType = (llvm_array (eval_size {| 8 + len|}) i8);

let alloc_buffer_aligned (len : Int) =
  llvm_alloc_aligned 16 (buffer_type len);

let alloc_buffer_aligned_readonly (len: Int ) =
  llvm_alloc_readonly_aligned 16 (buffer_type 16);
  // llvm_alloc_readonly_aligned 16 (buffer_type len);

let alloc_pointsto_buffer (len : Int) (data : Term) = do {
  buf <- alloc_buffer_aligned len;
  llvm_points_to_untyped buf (llvm_struct_value [llvm_term {{`(len) : [64]}}, llvm_term data]);
  return buf;
};

let alloc_pointsto_buffer_readonly (len : Int) (data : Term) = do {
  buf <- alloc_buffer_aligned_readonly len;
  llvm_points_to_untyped buf (llvm_struct_value [llvm_term {{`(len) : [64]}}, llvm_term data]);
  return buf;
};

let buffer_copy_spec (len : Int) = do {
  data   <- crucible_fresh_var "data" (llvm_array len i8);
  buffer <- alloc_pointsto_buffer_readonly len data;

  llvm_execute_func[buffer];

  newbuf <- alloc_pointsto_buffer len data;
  llvm_return newbuf;
};

m <- llvm_load_module "alloc_aligned.bc";
buffer_copy_ov <-llvm_verify m "buffer_copy" [] false (buffer_copy_spec 63) abc;

This will actually give somewhat of an explanation as to why it failed:

$ cabal exec saw -- bug.saw


[14:45:59.074] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/signal-verification/bug.saw"
[14:45:59.117] Verifying buffer_copy ...
[14:45:59.126] Simulating buffer_copy ...
[14:45:59.129] Checking proof obligations buffer_copy ...
[14:45:59.155] Subgoal failed: buffer_copy safety assertion:
internal: error: in _SAW_verify_prestate
Memory store failed
Details:
  The region wasn't allocated, wasn't large enough, or was marked as readonly

[14:45:59.155] SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 19}
[14:45:59.155] ----------Counterexample----------
[14:45:59.155] <<All settings of the symbolic variables constitute a counterexample>>
[14:45:59.155] ----------------------------------
[14:45:59.155] Stack trace:
"llvm_verify" (/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/signal-verification/bug.saw:36:18-36:29):
Proof failed.

[RyanGlScott]

I believe the culprit is the use of printOutLnTop here:

saw-script/src/SAWScript/Crucible/LLVM/Builtins.hs

Lines 608 to 618 in 0e93b7a

	do printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg]
	printOutLnTop Info (show stats)
	printOutLnTop OnlyCounterExamples "----------Counterexample----------"
	opts <- sawPPOpts <$> rwPPOpts <$> getTopLevelRW
	if null vals then
	printOutLnTop OnlyCounterExamples "<<All settings of the symbolic variables constitute a counterexample>>"
	else
	let showAssignment (name, val) = " " ++ name ++ ": " ++ show (ppFirstOrderValue opts val) in
	mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals
	printOutLnTop OnlyCounterExamples "----------------------------------"
	throwTopLevel "Proof failed." -- Mirroring behavior of llvm_verify

When run with saw, this will print information out to the terminal. When run with the Python bindings, however, these won't be printed at all. Indeed, the only thing that gets printed is the Proof failed. bit, and that's because that is the only part that is put into an exception.

One heavy-handed way to rectify this would be to stuff all of this information into an exception. I hacked together a quick proof of concept:

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 551efc2d..8b080c40 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -605,17 +605,24 @@ verifyObligations cc mspec tactic assumes asserts =
           case r of
             Unsat stats -> return stats
             SatMulti stats vals ->
-              do printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg]
-                 printOutLnTop Info (show stats)
-                 printOutLnTop OnlyCounterExamples "----------Counterexample----------"
-                 opts <- sawPPOpts <$> rwPPOpts <$> getTopLevelRW
-                 if null vals then
-                   printOutLnTop OnlyCounterExamples "<<All settings of the symbolic variables constitute a counterexample>>"
-                 else
-                   let showAssignment (name, val) = "  " ++ name ++ ": " ++ show (ppFirstOrderValue opts val) in
-                   mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals
-                 printOutLnTop OnlyCounterExamples "----------------------------------"
-                 throwTopLevel "Proof failed." -- Mirroring behavior of llvm_verify
+              do opts <- sawPPOpts <$> rwPPOpts <$> getTopLevelRW
+                 verb <- verbLevel <$> getOptions
+                 let errLines = [ (Info,                unwords ["Subgoal failed:", nm, msg])
+                                , (Info,                show stats)
+                                , (OnlyCounterExamples, "----------Counterexample----------") ]
+                                ++
+                                if null vals then
+                                  [ (OnlyCounterExamples, "<<All settings of the symbolic variables constitute a counterexample>>") ]
+                                else
+                                  let showAssignment (name, val) = "  " ++ name ++ ": " ++ show (ppFirstOrderValue opts val) in
+                                  map (\val -> (OnlyCounterExamples, showAssignment val)) vals
+                                ++
+                                [ (OnlyCounterExamples, "----------------------------------") ]
+                 throwTopLevel $ unlines
+                               $ mapMaybe (\(lvl, errLine) ->
+                                            if verb >= lvl then Just errLine else Nothing)
+                                          errLines
+                                 ++ [ "Proof failed." ] -- Mirroring behavior of llvm_verify
      printOutLnTop Info $ unwords ["Proof succeeded!", nm]
      return (mconcat stats)

Here is what the outputs of the Python bindings and saw, respectively:

Running: cabal new-exec --verbose=0 saw-remote-api socket
⚠️  Failed to verify: lemma_BufferCopySpec (defined at bug.py:50):
error: Subgoal failed: buffer_copy safety assertion:
alloc_aligned.c:30:5: error: in buffer_create
Mem copy failed
Details:
  Invalid copy source

SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 19}
----------Counterexample----------
<<All settings of the symbolic variables constitute a counterexample>>
Proof failed.

🛑  The goal failed to verify.

[19:55:39.102] Loading file "/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/signal-verification/bug.saw"
[19:55:39.161] Verifying buffer_copy ...
[19:55:39.170] Simulating buffer_copy ...
[19:55:39.173] Checking proof obligations buffer_copy ...
[19:55:39.200] Stack trace:
"llvm_verify" (/home/rscott/Documents/Hacking/Haskell/sandbox/saw-script/signal-verification/bug.saw:36:18-36:29):
Subgoal failed: buffer_copy safety assertion:
internal: error: in _SAW_verify_prestate
Memory store failed
Details:
  The region wasn't allocated, wasn't large enough, or was marked as readonly

SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 19}
----------Counterexample----------
<<All settings of the symbolic variables constitute a counterexample>>
Proof failed.

This comes at the downside of losing the timestamp information in front of each of the lines previously passed to printOutLnTop, but perhaps this is acceptable.

[RyanGlScott]

Please ignore #1127 (comment), as I overlooked the fact that saw-remote-api is already recording the output of printOutLnTop, but it simply wasn't being printed on the Python end. As further digging revealed, you can in fact print out this output by increasing the verbosity:

-view(LogResults())
+view(LogResults(verbose_failure=True))

With that, the output becomes quite reasonable:

Running: cabal new-exec --verbose=0 saw-remote-api socket
⚠️  Failed to verify: lemma_BufferCopySpec (defined at bug.py:50):
error: Proof failed.
        stdout:
                [17:34:17.168] Verifying buffer_copy ...
                [17:34:17.168] Simulating buffer_copy ...
                [17:34:17.171] Checking proof obligations buffer_copy ...
                [17:34:17.196] Subgoal failed: buffer_copy safety assertion:
                alloc_aligned.c:30:5: error: in buffer_create
                Mem copy failed
                Details:
                  Invalid copy source

                [17:34:17.196] SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 25}
                [17:34:17.196] ----------Counterexample----------
                [17:34:17.196] <<All settings of the symbolic variables constitute a counterexample>>
                [17:34:17.196] ----------------------------------

🛑  The goal failed to verify.

I suppose there's a debate to be had about what the default settings should be here, but at the very least, this isn't a bug.