More LLVMSetup error checking

CHANGES.md

@@ -6,6 +6,26 @@ This release supports [version
 
 ## Changes
 
+* `llvm_verify` now enforces that an `llvm_return` specification is
+  included for any function with a non-void return type.
+  To write a spec that asserts nothing about the return value,
+  `llvm_return` may be used with a fresh variable declared with
+  `llvm_fresh_var` in the post-state section, like this:
+
+  do {
+    ...
+    llvm_execute_func <args>;
+    ...
+    ret <- llvm_fresh_var "ret" <type>;
+    llvm_return (llvm_term ret);
+  }
+
+* `jvm_verify` now enforces that a `jvm_return` specification is
+  included for any method with a non-void return type.
+  To write a spec that asserts nothing about the return value,
+  `jvm_return` may be used with a fresh variable declared with
+  `jvm_fresh_var` in the post-state section.
+
 * The `cryptol_load` and `cryptol_prims` commands now fail if used
   in a nested scope, instead of behaving strangely.
 

intTests/test0061_path_sat/test.saw

@@ -3,6 +3,9 @@ m <- llvm_load_module "termination.bc";
 let g_spec = do {
   x <- llvm_fresh_var "x" (llvm_int 64);
   llvm_execute_func [llvm_term x];
+  // unspecified return value
+  ret <- llvm_fresh_var "ret" (llvm_int 64);
+  llvm_return (llvm_term ret);
   };
 
 llvm_verify m "g1" [] false g_spec z3;

intTests/test0064_detect_vacuity/test.saw

@@ -8,6 +8,9 @@ let bad_spec = do {
     llvm_precond {{ a == 1 }};
     llvm_execute_func [llvm_term a];
     llvm_postcond {{ a == 2 }};
+    // unspecified return value
+    ret <- llvm_fresh_var "ret" (llvm_int 32);
+    llvm_return (llvm_term ret);
 };
 
 m <- llvm_load_module "test.bc";

intTests/test0067_term_eqs/test.saw

@@ -14,10 +14,10 @@ let f_false_spec = do {
 
 let test_spec = do {
   llvm_execute_func [];
+  crucible_return (crucible_term {{ 0:[32] }});
 };
 
 f_ov <- llvm_unsafe_assume_spec m "f" f_spec;
 f_false_ov <- llvm_unsafe_assume_spec m "f" f_false_spec;
 llvm_verify m "test_f" [f_ov] false test_spec trivial;
 fails (llvm_verify m "test_f" [f_false_ov] false test_spec trivial);
-

intTests/test_sanitize/test.saw

@@ -5,6 +5,9 @@ let f_spec = do {
     x <- llvm_fresh_var "x" (llvm_int 32);
     y <- llvm_fresh_var "y" (llvm_int 32);
     llvm_execute_func [llvm_term x, llvm_term y];
+    // unspecified return value
+    z <- llvm_fresh_var "z" (llvm_int 32);
+    llvm_return (llvm_term z);
 };
 
 llvm_verify m_norm "f" [] false f_spec z3;

intTests/test_stack_traces/trace004.log.good

@@ -4,28 +4,40 @@
  just llvm_stack
 Stack trace:
    (builtin) in llvm_stack
-   trace004.saw:15:32-15:42 in (callback)
+   trace004.saw:15:39-15:49 in (callback)
    (builtin) in llvm_verify
-   trace004.saw:15:1-15:45 (at top level)
+   trace004.saw:15:8-15:52 in (callback)
+   (builtin) in fails
+   trace004.saw:15:1-15:52 (at top level)
+
+== Anticipated failure message ==
+Stack trace:
+   (builtin) in llvm_verify
+   trace004.saw:15:8-15:52 in (callback)
+   (builtin) in fails
+   trace004.saw:15:1-15:52 (at top level)
+Missing llvm_execute_func specification when verifying foo
 
- Verifying foo...
- Simulating foo...
- Checking proof obligations foo...
- Proof succeeded! foo
 
  ------------------------------------------------------------
  llvm_stack via let
 Stack trace:
    (builtin) in llvm_stack
    trace004.saw:22:13-22:23 in spec0
-   trace004.saw:23:32-23:37 in (callback)
+   trace004.saw:23:39-23:44 in (callback)
    (builtin) in llvm_verify
-   trace004.saw:23:1-23:40 (at top level)
+   trace004.saw:23:8-23:47 in (callback)
+   (builtin) in fails
+   trace004.saw:23:1-23:47 (at top level)
+
+== Anticipated failure message ==
+Stack trace:
+   (builtin) in llvm_verify
+   trace004.saw:23:8-23:47 in (callback)
+   (builtin) in fails
+   trace004.saw:23:1-23:47 (at top level)
+Missing llvm_execute_func specification when verifying foo
 
- Verifying foo...
- Simulating foo...
- Checking proof obligations foo...
- Proof succeeded! foo
 
  ------------------------------------------------------------
  do-block

intTests/test_stack_traces/trace004.saw

@@ -9,18 +9,18 @@ print "";
 
 
 // Test just llvm_stack by itself.
-// This probably should not actually verify, but it does...
+// This should not actually verify.
 print "------------------------------------------------------------";
 print "just llvm_stack";
-llvm_verify mod "foo" [] false llvm_stack z3;
+fails (llvm_verify mod "foo" [] false llvm_stack z3);
 print "";
 
 // Test just llvm_stack via a let-binding.
-// This probably should not actually verify, but it does...
+// This should not actually verify.
 print "------------------------------------------------------------";
 print "llvm_stack via let";
 let spec0 = llvm_stack;
-llvm_verify mod "foo" [] false spec0 z3;
+fails (llvm_verify mod "foo" [] false spec0 z3);
 print "";
 
 // Test with an inline do-block.

saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs

@@ -108,7 +108,10 @@ crucible_execute_func ::
   [MS.SetupValue ext] ->
   CrucibleSetup ext ()
 crucible_execute_func args = do
+  st <- get
   tps <- use (csMethodSpec . MS.csArgs)
+  when (st ^. csPrePost == MS.PostState) $
+    fail "duplicate execute_func declaration"
   csPrePost .= MS.PostState
   csMethodSpec . MS.csArgBindings .= Map.fromList [ (i, (t,a))
                                                   | i <- [0..]

saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs

@@ -574,14 +574,20 @@ withMethodSpec pathSat lm nm setup action =
               -- execute commands of the method spec
               io $ W4.setCurrentProgramLoc sym setupLoc
 
-
               setupState  <-
                 (execStateT
                    (runReaderT (runLLVMCrucibleSetupM setup)
                                (Setup.makeCrucibleSetupRO))
                      st0)
               let methodSpec = setupState ^. Setup.csMethodSpec
                   cc1        = setupState ^. Setup.csCrucibleContext
+
+              -- check for missing llvm_execute_func
+              unless (setupState ^. Setup.csPrePost == PostState) $
+                io $ throwMethodSpec methodSpec $ Text.unpack $
+                "Missing llvm_execute_func specification when verifying " <>
+                methodSpec^.csName
+
               io $ checkSpecArgumentTypes cc1 methodSpec
               io $ checkSpecReturnType cc1 methodSpec
 
@@ -909,7 +915,12 @@ checkSpecReturnType cc mspec =
            , "Expected: " <> Text.pack (show retTy)
            , "but given value of type: " <> Text.pack (show retTy')
            ]
-    (Nothing, _) -> return ()
+    (Nothing, Just retTy) ->
+      throwMethodSpec mspec $ Text.unpack $ Text.unlines
+      [ "Missing return value specification for function with non-void return type"
+      , "Expected: " <> Text.pack (show retTy)
+      ]
+    (Nothing, Nothing) -> pure ()
 
 -- | Evaluate the precondition part of a Crucible method spec:
 --