Revert "Crucible/LLVM: Group argument equality assertions in override…

… matching (#525)" This reverts commit 06b0761.
GaloisInc · Aug 12, 2019 · 874d2e6 · 874d2e6
1 parent 798977c
commit 874d2e6
Show file tree

Hide file tree

Showing 5 changed files with 62 additions and 130 deletions.
diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs
@@ -12,11 +12,8 @@ module SAWScript.Crucible.Common
   ( ppAbortedResult
   , Sym
   , LabeledPred
-  , LabeledPred'
-  , labelWithSimError
   ) where
 
-import           Control.Lens
 import           Lang.Crucible.Simulator.ExecutionTree (AbortedResult(..), GlobalPair)
 import           Lang.Crucible.Simulator.CallFrame (SimFrame)
 import qualified Lang.Crucible.Simulator.SimError as Crucible
@@ -32,17 +29,6 @@ import qualified What4.LabeledPred as W4
 import qualified Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
 
 type LabeledPred sym = W4.LabeledPred (W4.Pred sym) Crucible.SimError
-type LabeledPred' sym = W4.LabeledPred (W4.Pred sym) PP.Doc
-
--- | Convert a predicate with a 'PP.Doc' label to one with a 'Crucible.SimError'
-labelWithSimError ::
-  W4.ProgramLoc ->
-  (PP.Doc -> String) ->
-  LabeledPred' Sym ->
-  LabeledPred Sym
-labelWithSimError loc conv lp =
-  lp & W4.labeledPredMsg
-     %~ (Crucible.SimError loc . Crucible.AssertFailureSimError . conv)
 
 -- | The symbolic backend we use for SAW verification
 type Sym = SAWCoreBackend Nonce.GlobalNonceGenerator (Yices.Connection Nonce.GlobalNonceGenerator) (W4.Flags W4.FloatReal)

diff --git a/src/SAWScript/Crucible/Common/Override/Operations.hs b/src/SAWScript/Crucible/Common/Override/Operations.hs
@@ -19,12 +19,12 @@ import Control.Lens
 import           Control.Monad.IO.Class (liftIO)
 import           Data.Map (Map)
 import qualified Data.Set as Set
-import qualified Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
 
 import qualified Lang.Crucible.Backend.SAWCore as CrucibleSAW
+import qualified Lang.Crucible.Simulator.SimError as Crucible
 
 import qualified What4.Interface as W4
-import qualified What4.LabeledPred as W4
+import qualified What4.ProgramLoc as W4
 
 import qualified Verifier.SAW.SharedTerm as SAWVerifier
 import           Verifier.SAW.SharedTerm (Term, SharedContext)
@@ -34,7 +34,7 @@ import           Verifier.SAW.Term.Functor (TermF(..), ExtCns(..), VarIndex)
 import           Verifier.SAW.Term.Functor (FlatTermF(ExtCns))
 import           Verifier.SAW.Prelude (scEq)
 
-import           SAWScript.Crucible.Common (Sym, LabeledPred')
+import           SAWScript.Crucible.Common (Sym)
 import           SAWScript.Crucible.Common.MethodSpec (PrePost(..), SetupValue(..))
 import           SAWScript.Crucible.Common.Override.Monad
 
@@ -48,37 +48,39 @@ resolveSAWPred sym tm = CrucibleSAW.bindSAWTerm sym W4.BaseBoolRepr tm
 assignTerm ::
   SharedContext      {- ^ context for constructing SAW terms    -} ->
   Sym                                                              ->
+  W4.ProgramLoc                                                    ->
   PrePost                                                          ->
   VarIndex {- ^ external constant index -} ->
   Term     {- ^ value                   -} ->
-  OverrideMatcher env md (Maybe (LabeledPred' Sym))
+  OverrideMatcher env md ()
 
-assignTerm sc cc prepost var val =
+assignTerm sc cc loc prepost var val =
   do mb <- OM (use (termSub . at var))
      case mb of
-       Nothing -> OM (termSub . at var ?= val) >> pure Nothing
-       Just old -> matchTerm sc cc prepost val old
+       Nothing -> OM (termSub . at var ?= val)
+       Just old -> matchTerm sc cc loc prepost val old
 
 
 matchTerm ::
   SharedContext   {- ^ context for constructing SAW terms    -} ->
   Sym                                                           ->
+  W4.ProgramLoc                                                    ->
   PrePost                                                       ->
   Term            {- ^ exported concrete term                -} ->
   Term            {- ^ expected specification term           -} ->
-  OverrideMatcher ext md (Maybe (LabeledPred' Sym))
-matchTerm _ _ _ real expect | real == expect = return Nothing
-matchTerm sc sym prepost real expect =
+  OverrideMatcher ext md ()
+matchTerm _ _ _ _ real expect | real == expect = return ()
+matchTerm sc sym loc prepost real expect =
   do free <- OM (use omFree)
      case SAWVerifier.unwrapTermF expect of
        FTermF (ExtCns ec)
          | Set.member (ecVarIndex ec) free ->
-         do assignTerm sc sym prepost (ecVarIndex ec) real
+         do assignTerm sc sym loc prepost (ecVarIndex ec) real
 
        _ ->
          do t <- liftIO $ scEq sc real expect
             p <- liftIO $ resolveSAWPred sym t
-            return $ Just $ W4.LabeledPred p $ PP.vcat $ map PP.text
+            addAssert p $ Crucible.SimError loc $ Crucible.AssertFailureSimError $ unlines $
               [ "Literal equality " ++ stateCond prepost
               , "Expected term: " ++ prettyTerm expect
               , "Actual term:   " ++ prettyTerm real

diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
@@ -87,7 +87,7 @@ import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
 
-import           SAWScript.Crucible.Common (Sym, labelWithSimError)
+import           SAWScript.Crucible.Common (Sym)
 import           SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), PrePost(..))
 import           SAWScript.Crucible.Common.Override
 
@@ -521,22 +521,6 @@ assignVar cc loc var ref =
 
 ------------------------------------------------------------------------
 
-matchTerm' ::
-  SharedContext   {- ^ context for constructing SAW terms    -} ->
-  W4.ProgramLoc ->
-  Sym                                                           ->
-  PrePost                                                       ->
-  Term            {- ^ exported concrete term                -} ->
-  Term            {- ^ expected specification term           -} ->
-  OverrideMatcher CJ.JVM w ()
-matchTerm' sc loc sym prepost real expect = do
-  mlp <- matchTerm sc sym prepost real expect
-  case labelWithSimError loc show <$> mlp of
-    Nothing -> return ()
-    Just (W4.LabeledPred p doc) -> addAssert p doc
-
-------------------------------------------------------------------------
-
 -- | Match the value of a function argument with a symbolic 'SetupValue'.
 matchArg ::
   Options          {- ^ saw script print out opts -} ->
@@ -555,7 +539,7 @@ matchArg opts sc cc cs prepost actual expectedTy expected@(MS.SetupTerm expected
   = do sym <- getSymInterface
        failMsg  <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
        realTerm <- valueToSC sym (cs ^. MS.csLoc) failMsg tval actual
-       matchTerm' sc (cs ^. MS.csLoc) (cc^.jccBackend) prepost realTerm (ttTerm expectedTT)
+       matchTerm sc (cc^.jccBackend) (cs ^. MS.csLoc) prepost realTerm (ttTerm expectedTT)
 
 matchArg opts sc cc cs prepost actual@(RVal ref) expectedTy setupval =
   case setupval of

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/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 (toList, find)
+import           Data.Foldable (for_, toList, find)
 import           Data.Function
 import           Data.IORef
 import           Data.List
@@ -98,6 +98,7 @@ 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
@@ -848,23 +849,15 @@ verifyPoststate opts sc cc mspec env0 globals ret =
                                     (view (MS.csPostState . MS.csFreshVars) mspec))
      matchPost <- io $
           runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $
-           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)
+           do matchResult
               learnCond opts sc cc mspec PostState (mspec ^. MS.csPostState)
 
      st <- case matchPost of
              Left err      -> fail (show err)
              Right (_, st) -> return st
 
-     io $ mapM_ (Crucible.addAssertion sym) (st ^. omAsserts)
-     when (not (null (st ^. omArgAsserts))) $ fail "verifyPoststate: impossible"
+     io $ for_ (view omAsserts st) $ \(W4.LabeledPred p r) ->
+       Crucible.addAssertion sym (Crucible.LabeledPred p r)
 
      obligations <- io $ Crucible.getProofObligations sym
      io $ Crucible.clearProofObligations sym
@@ -884,7 +877,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 ()
 
 --------------------------------------------------------------------------------