Crucible/LLVM: Group argument equality assertions in override matching (

#525)

* More explicit handling of assertions in override matching

* Crucible/LLVM: Better errors for argument and return value equalities

Fixes #522

* Propagate changes to methodSpecHandler

* add space

* Simplify

* Add an assertion

src/SAWScript/Crucible/Common/Override.hs

@@ -22,6 +22,7 @@ module SAWScript.Crucible.Common.Override
   ( Pointer
   , OverrideState(..)
   , osAsserts
+  , osArgAsserts
   , osAssumes
   , osFree
   , osLocation
@@ -104,6 +105,11 @@ data OverrideState ext = OverrideState
     -- | Accumulated assertions
   , _osAsserts :: [LabeledPred Sym]
 
+    -- | Assertions about the values of function arguments
+    --
+    -- These come from @crucible_execute_func@.
+  , _osArgAsserts :: [[W4.LabeledPred (W4.Pred Sym) PP.Doc]]
+
     -- | Accumulated assumptions
   , _osAssumes :: [W4.Pred Sym]
 
@@ -131,6 +137,7 @@ initialState ::
   OverrideState ext
 initialState sym globals allocs terms free loc = OverrideState
   { _osAsserts       = []
+  , _osArgAsserts    = []
   , _osAssumes       = []
   , _syminterface    = sym
   , _overrideGlobals = globals

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -63,7 +63,7 @@ import           Control.Monad.State hiding (fail)
 import           Control.Monad.Fail (MonadFail(..))
 import qualified Data.Bimap as Bimap
 import           Data.Char (isDigit)
-import           Data.Foldable (for_, toList, find)
+import           Data.Foldable (toList, find)
 import           Data.Function
 import           Data.IORef
 import           Data.List
@@ -98,7 +98,6 @@ import           Data.Parameterized.Some
 import qualified What4.Concrete as W4
 import qualified What4.Config as W4
 import qualified What4.FunctionName as W4
-import qualified What4.LabeledPred as W4
 import qualified What4.ProgramLoc as W4
 import qualified What4.Interface as W4
 import qualified What4.Expr.Builder as W4
@@ -863,14 +862,23 @@ verifyPoststate opts sc cc mspec env0 globals ret =
                                     (view (MS.csPostState . MS.csFreshVars) mspec))
      matchPost <- io $
           runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $
-           do matchResult
+           do -- Assert that the function returned the correct value
+              retAsserts <- matchResult
+              liftIO $ forM_ retAsserts $
+                Crucible.addAssertion sym . labelWithSimError poststateLoc
+                  (\doc -> unlines [ "When checking a crucible_return statement:"
+                                   , show doc
+                                   ])
+
+              -- Assert other post-state conditions (equalities, points-to)
               learnCond opts sc cc mspec PostState (mspec ^. MS.csPostState)
 
      st <- case matchPost of
              Left err      -> fail (show err)
              Right (_, st) -> return st
-     io $ for_ (view osAsserts st) $ \(W4.LabeledPred p r) ->
-       Crucible.addAssertion sym (Crucible.LabeledPred p r)
+
+     io $ mapM_ (Crucible.addAssertion sym) (st ^. osAsserts)
+     when (not (null (st ^. osArgAsserts))) $ fail "verifyPoststate: impossible"
 
      obligations <- io $ Crucible.getProofObligations sym
      io $ Crucible.clearProofObligations sym
@@ -890,7 +898,7 @@ verifyPoststate opts sc cc mspec env0 globals ret =
         (Just (rty,r), Just expect) -> matchArg opts sc cc mspec PostState r rty expect
         (Nothing     , Just _ )     ->
           fail "verifyPoststate: unexpected crucible_return specification"
-        _ -> return ()
+        _ -> return []
 
 --------------------------------------------------------------------------------