Have print_goal print out the provenance of each goal when sim-verbose is high enough

[RyanGlScott]

Typically, using print_goal in a proof results in output like this:

[12:53:16.191] Goal ECDSA_do_sign (safety assertion:) (goal number 0):
<elided>

[12:53:16.377] Goal ECDSA_do_sign (safety assertion:) (goal number 1):
<elided>

[12:53:16.603] Goal ECDSA_do_sign (safety assertion:) (goal number 2):
<elided>

This tells me the relevant function (ECDSA_do_sign), what kind of goal it is (safety assertion:), and the goal number for each goal. However, it doesn't really give any sort of indication of why this goal needs to be proved, which makes the associated SAWCore term rather mysterious.

It turns out that SAW is intentionally omitting some information, however. If I apply this quick-and-dirty patch:

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index a2f56ebf..8c43f497 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -599,7 +624,7 @@ verifyObligations cc mspec tactic assumes asserts =
        forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) ->
        do goal   <- io $ scImplies sc assume assert
           goal'  <- io $ boolToProp sc [] goal
-          let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"]
+          let goalname = concat [nm, " (", {- takeWhile (/= '\n') -} msg, ")"]
               proofgoal = ProofGoal n "vc" goalname goal'
           res <- runProofScript tactic proofgoal
           case res of

Then the output of print_goal becomes much more useful:

[13:35:35.786] Goal ECDSA_do_sign (safety assertion:
/home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/ECDSA/ECDSA.saw:290:21: error: in overrideBranches
No override specification applies for ec_point_mul_scalar_base.
Arguments:
- concrete pointer: allocation = 6237, offset = 0
- concrete pointer: allocation = 6257, offset = 0
- concrete pointer: allocation = 6254, offset = 0
Run SAW with --sim-verbose=3 to see a description of each override.
) (goal number 0):
<elided>

[13:35:35.974] Goal ECDSA_do_sign (safety assertion:
/home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/ECDSA/ECDSA.saw:290:21: error: in overrideBranches
No override specification applies for ec_scalar_is_zero.
Arguments:
- concrete pointer: allocation = 6237, offset = 0
- concrete pointer: allocation = 6258, offset = 0
Run SAW with --sim-verbose=3 to see a description of each override.
) (goal number 1):
<elided>

[13:35:36.214] Goal ECDSA_do_sign (safety assertion:
/home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/ECDSA/ECDSA.saw:290:21: error: in overrideBranches
No override specification applies for ec_scalar_add.
Arguments:
- concrete pointer: allocation = 6237, offset = 0
- concrete pointer: allocation = 6259, offset = 0
- concrete pointer: allocation = 6259, offset = 0
- concrete pointer: allocation = 6260, offset = 0
The following overrides had some preconditions that failed concretely:
- Name: ec_scalar_add
  Location: /home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/EC/EC.saw:881:21
  Argument types: 
  - %struct.ec_group_st*
  - %union.EC_FELEM*
  - %union.EC_FELEM*
  - %union.EC_FELEM*
  Return type: <void>
  * /home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/EC/EC.saw:881:21: error: in _SAW_verify_prestate
    Memory regions not disjoint:
      (base=(6259, 0x0:[64]), size=Prelude.bvNat 64 48)
      from llvm_alloc (/home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/EC/EC.saw:368:12)
      and 
      (base=(6259, 0x0:[64]), size=Prelude.bvNat 64 48)
      from llvm_alloc (/home/rscott/Documents/Hacking/SAW/aws-lc-verification/SAW/proof/common/helpers.saw:23:8)
Run SAW with --sim-verbose=3 to see a description of each override.
) (goal number 2):
<elided>

It now reveals that the overrides for ec_point_mul_scalar_base, ec_scalar_is_zero, and ec_scalar_add are the sources of these goals. Obviously, the output could stand to be printed somewhat more neatly, but the information is definitely there.

Would it be reasonable to have print_goal print this information if sim-verbose is set to a high enough level (perhaps 2 or higher)?

[kquick]

Need to determine how to toggle this. Could also be handled via a structured log viewer where the toggling was of the output log information.