write_goal only writes the last proof goal to a file, unlike other goal-writing proof scripts

[RyanGlScott]

Consider this C program and corresponding proof script:

// test.c
#include <stdint.h>

int64_t foo(int64_t x) {
  return x + 1;
}

// test.saw
enable_experimental;

m <- llvm_load_module "test.bc";

let foo_spec = do {
  x <- llvm_fresh_var "x" (llvm_int 64);
  llvm_precond {{ x <$ 2^^63 - 1 }};

  llvm_execute_func [llvm_term x];

  llvm_return (llvm_term {{ x + 1 }});
};

llvm_verify m "foo" [] false foo_spec (do { write_goal "goal"; z3; });

Note that the proof script in the call to llvm_verify uses write_goal, with the intent that it will write each proof goal to a file. In this particular example, we would expect to see two proof goals written: one when checking the safety assertion that x + 1 will not produce signed integer overflow, and other when checking that the return value in the simulator actually equals x + 1 on the Cryptol side. Despite this, if we run this SAW on it:

$ clang -g -emit-llvm -c test.c -o test.bc
$ ~/Software/saw-1.2/bin/saw test.saw

Then we only see a single file goal written:

$ cat goal
Goal foo (goal number 1): return value matching
at /home/ryanscott/Documents/Hacking/SAW/test.saw:15:1 in _SAW_verify_prestate
/home/ryanscott/Documents/Hacking/SAW/test.saw:15:1: error: in _SAW_verify_prestate
Literal equality postcondition


let { x@1 = Vec 64 Bool
      x@2 = TCNum 64
      x@3 = PRingSeqBool x@2
      x@4 = PLiteralSeqBool x@2
      x@5 = ecNumber (TCNum 1) x@1 x@4
      x@6 = ecSLt x@1 (PSignedCmpSeqBool x@2) x
              (ecMinus x@1 x@3
                 (ecExp x@1 Integer x@3 PIntegralInteger
                    (ecNumber (TCNum 2) x@1 x@4)
                    (ecNumber (TCNum 63) Integer PLiteralInteger))
                 x@5)
    }
 in EqTrue
      (implies x@6
         (implies x@6
            (bvEq 64 (bvAdd 64 (bvNat 64 1) x) (ecPlus x@1 x@3 x x@5))))

This contains goal number 1, which is the second proof goal (note that goal numbers are zero-indexed within SAW). Contrast this to a different proof script, which writes SMT-LIB proof goals to files:

llvm_verify m "foo" [] false foo_spec (offline_w4_unint_z3 [] "goal");

This will write two files, one for each proof goal:

$ cat 'goal.safety assertion0.smt2' 
(set-option :produce-models true)
; :1:0
(declare-fun x0 () (_ BitVec 64))
(define-fun x!0 () Bool (bvslt x0 (_ bv9223372036854775807 64)))
(assert x!0)
(define-fun x!1 () Bool (bvslt x0 (_ bv0 64)))
(assert (not x!1))
(define-fun x!2 () (_ BitVec 64) (bvadd x0 (_ bv1 64)))
(define-fun x!3 () Bool (bvslt x!2 (_ bv0 64)))
(assert x!3)
(check-sat)
(exit)

$ cat 'goal.return value matching1.smt2' 
(set-option :produce-models true)
; :1:0
(assert false)
(check-sat)
(exit)

Note that the names of each file reflect which goal type and number they encode. In this sense, write_goal is the unusual one, as it is (as far as I can tell) the only proof-goal-writing ProofScript that does not disambiguate its files with a similar naming convention. As such, it will write each proof goal to the same file name, clobbering the results of previous goals.

I propose that we alter write_goal to use a similar file naming convention as offline_w4_unint_z3 and friends. I believe something like this would suffice:

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index e305e8c0c..b704ba706 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -453,12 +453,13 @@ goalSummary goal = unlines $ concat
 write_goal :: String -> ProofScript ()
 write_goal fp =
   execTactic $ tacticId $ \goal ->
-  do opts <- getTopLevelPPOpts
+  do let file = fp ++ "." ++ goalType goal ++ show (goalNum goal) ++ ".txt"
+     opts <- getTopLevelPPOpts
      sc <- getSharedContext
      liftIO $ do
        nenv <- scGetNamingEnv sc
        let output = prettySequent opts nenv (goalSequent goal)
-       writeFile fp (unlines [goalSummary goal, output])
+       writeFile file (unlines [goalSummary goal, output])
 
 print_goal :: ProofScript ()
 print_goal =

The same code is shared among all ProofScripts that write proof goals to files, however, so we should consider factoring it out.

[sauclovian-g]

Seems like a plan

(Also, can we adjust it so that it writes the non-saw-core parts as comments so the output can then be reprocessed, and name the output .sawcore? Or is that not actually workable?)

[RyanGlScott]

Also, can we adjust it so that it writes the non-saw-core parts as comments so the output can then be reprocessed, and name the output .sawcore?

That would be even better, yes. I haven't looked deeply into how technically feasible it would be, but if it's not too burdensome, we should try to do so.