add goal_when_num and goal_num_ite (#986)

add `goal_num_when` and `goal_num_ite` commands

intTests/test_goal_num_ite/Makefile

@@ -0,0 +1,3 @@
+test.bc : test.c
+	clang -O0 -c -emit-llvm -o test.bc test.c
+

intTests/test_goal_num_ite/test.c

@@ -0,0 +1,14 @@
+#include<stdint.h>
+
+void g(uint64_t* a) {
+  *a = 2*(*a);
+};
+
+void h(uint64_t* a) {
+  *a = 3*(*a);
+};
+
+void f(uint64_t* x) {
+  g(x);
+  h(x);
+};

intTests/test_goal_num_ite/test.saw

@@ -0,0 +1,46 @@
+m <- llvm_load_module "test.bc";
+
+let f_spec = do {
+  xp <- llvm_alloc (llvm_int 64);
+  x <- llvm_fresh_var "x" (llvm_int 64);
+  llvm_points_to xp (crucible_term x);
+  llvm_execute_func [xp];
+  llvm_points_to xp (crucible_term {{ 6*x }});
+};
+
+let g_spec = do {
+  xp <- llvm_alloc (llvm_int 64);
+  x <- llvm_fresh_var "x" (llvm_int 64);
+  llvm_points_to xp (crucible_term x);
+  llvm_execute_func [xp];
+  llvm_points_to xp (crucible_term {{(2*x):[64]}});
+};
+
+let h_spec = do {
+  xp <- llvm_alloc (llvm_int 64);
+  x <- llvm_fresh_var "x" (llvm_int 64);
+  llvm_points_to xp (crucible_term {{x}});
+  llvm_precond {{ x > 1 }};
+  llvm_execute_func [xp];
+  llvm_points_to xp (crucible_term {{(3*x):[64]}});
+};
+
+g_ov <- llvm_verify m "g" [] false g_spec z3;
+h_ov <- llvm_verify m "h" [] false h_spec z3;
+
+enable_experimental;
+
+// we get two verification conditions: on for the precondition of h, and one for the postcondition of f
+// the override precondition of h is violated, but if we assume it's unsat then verification succeeds:
+llvm_verify m "f" [g_ov, h_ov] false f_spec
+  (goal_num_ite 0
+    assume_unsat
+    w4);
+
+// on the other hand, if we provide the wrong goal number, then it fails.
+fails (
+  llvm_verify m "f" [g_ov, h_ov] false f_spec
+    (goal_num_ite 1
+      assume_unsat
+      w4)
+);

intTests/test_goal_num_ite/test.sh

@@ -0,0 +1,4 @@
+set -e
+
+$SAW test.saw
+

src/SAWScript/Builtins.hs

@@ -445,7 +445,7 @@ print_goal :: ProofScript ()
 print_goal =
   withFirstGoal $ \goal ->
   do opts <- getTopLevelPPOpts
-     printOutLnTop Info ("Goal " ++ goalName goal ++ ":")
+     printOutLnTop Info ("Goal " ++ goalName goal ++ " (goal number " ++ (show $ goalNum goal) ++ "):")
      printOutLnTop Info (scPrettyTerm opts (unProp (goalProp goal)))
      return ((), mempty, Just goal)
 
@@ -627,13 +627,27 @@ goal_insert (Theorem (Prop t) _stats) =
          let goal' = goal { goalProp = Prop body' }
          return ((), ProofState (goal' : goals') concl stats timeout)
 
+goal_num_when :: Int -> ProofScript () -> ProofScript ()
+goal_num_when n script =
+  StateT $ \s ->
+  case psGoals s of
+    g : _ | goalNum g == n -> runStateT script s
+    _ -> return ((), s)
+
 goal_when :: String -> ProofScript () -> ProofScript ()
 goal_when str script =
   StateT $ \s ->
   case psGoals s of
     g : _ | str `isInfixOf` goalName g -> runStateT script s
     _ -> return ((), s)
 
+goal_num_ite :: Int -> ProofScript SV.SatResult -> ProofScript SV.SatResult -> ProofScript SV.SatResult
+goal_num_ite n s1 s2 =
+  StateT $ \s ->
+  case psGoals s of
+       g : _ | goalNum g == n -> runStateT s1 s
+       _ -> runStateT s2 s
+
 -- | Bit-blast a proposition and check its validity using ABC.
 proveABC :: ProofScript SV.SatResult
 proveABC = do

src/SAWScript/Interpreter.hs

@@ -1191,6 +1191,17 @@ primitives = Map.fromList
     [ "Run the given proof script only when the goal name contains"
     , "the given string."
     ]
+  , prim "goal_num_ite"       "Int -> ProofScript SatResult -> ProofScript SatResult -> ProofScript SatResult"
+    (pureVal goal_num_ite)
+    Experimental
+    [ "If the goal number is the given number, runs the first script."
+    , "Otherwise runs the second script" ]
+  , prim "goal_num_when"       "Int -> ProofScript () -> ProofScript ()"
+    (pureVal goal_num_when)
+    Experimental
+    [ "Run the given proof script only when the goal number is the"
+    , "the given number."
+    ]
   , prim "print_goal"          "ProofScript ()"
     (pureVal print_goal)
     Current