Refactor the way :prove counterexamples are represented and printed.

This allows us to distinguish cases where counterexamples find inputs
that violate safety conditions from cases where inputs cause the
predicate to be false.

src/Cryptol/Prelude.hs

@@ -32,3 +32,4 @@ arrayContents = B.pack [there|lib/Array.cry|]
 
 cryptolTcContents :: String
 cryptolTcContents = [there|lib/CryptolTC.z3|]
+

src/Cryptol/REPL/Command.hs

@@ -80,7 +80,10 @@ import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)
 import qualified Cryptol.Parser.AST as P
 import qualified Cryptol.Transform.Specialize as S
-import Cryptol.Symbolic (ProverCommand(..), QueryType(..), SatNum(..),ProverStats,ProverResult(..))
+import Cryptol.Symbolic
+  ( ProverCommand(..), QueryType(..), SatNum(..)
+  , ProverStats,ProverResult(..),CounterExampleType(..)
+  )
 import qualified Cryptol.Symbolic.SBV as SBV
 import qualified Cryptol.Symbolic.What4 as W4
 
@@ -308,13 +311,23 @@ evalCmd str = do
       -- be generalized if mono-binds is enabled
       replEvalDecl decl
 
-printCounterexample :: Bool -> P.Expr P.PName -> [Concrete.Value] -> REPL ()
-printCounterexample isSat pexpr vs =
+printCounterexample :: CounterExampleType -> P.Expr P.PName -> [Concrete.Value] -> REPL ()
+printCounterexample cexTy pexpr vs =
   do ppOpts <- getPPValOpts
      docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs
      let doc = ppPrec 3 pexpr -- function application has precedence 3
      rPrint $ hang doc 2 (sep docs) <+>
-       text (if isSat then "= True" else "= False")
+       case cexTy of
+         SafetyViolation -> text "= <<error>>"
+         PredicateFalsified -> text "= False"
+
+printSatisfyingModel :: P.Expr P.PName -> [Concrete.Value] -> REPL ()
+printSatisfyingModel pexpr vs =
+  do ppOpts <- getPPValOpts
+     docs <- mapM (rEval . E.ppValue Concrete ppOpts) vs
+     let doc = ppPrec 3 pexpr -- function application has precedence 3
+     rPrint $ hang doc 2 (sep docs) <+> text ("= True")
+
 
 dumpTestsCmd :: FilePath -> String -> REPL ()
 dumpTestsCmd outFile str =
@@ -459,8 +472,7 @@ qcCmd qcMode str =
     opts <- getPPValOpts
     case failure of
       FailFalse vs -> do
-        let isSat = False
-        printCounterexample isSat pexpr vs
+        printCounterexample PredicateFalsified pexpr vs
         case (tys,vs) of
           ([t],[v]) -> bindItVariableVal t v
           _ -> let fs = [ M.packIdent ("arg" ++ show (i::Int)) | i <- [ 1 .. ] ]
@@ -568,13 +580,29 @@ cmdProveSat isSat str = do
         case result of
           EmptyResult         ->
             panic "REPL.Command" [ "got EmptyResult for online prover query" ]
+
           ProverError msg     -> rPutStrLn msg
+
           ThmResult ts        -> do
             rPutStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
             (t, e) <- mkSolverResult cexStr (not isSat) (Left ts)
             bindItVariable t e
+
+          CounterExample cexType tevs -> do
+            rPutStrLn "Counterexample"
+            let tes = map ( \(t,e,_) -> (t,e)) tevs
+                vs  = map ( \(_,_,v) -> v)     tevs
+
+            (t,e) <- mkSolverResult cexStr isSat (Right tes)
+            pexpr <- replParseExpr str
+
+            ~(EnvBool yes) <- getUser "show-examples"
+            when yes $ printCounterexample cexType pexpr vs
+
+            bindItVariable t e
+
           AllSatResult tevss -> do
-            rPutStrLn (if isSat then "Satisfiable" else "Counterexample")
+            rPutStrLn "Satisfiable"
             let tess = map (map $ \(t,e,_) -> (t,e)) tevss
                 vss  = map (map $ \(_,_,v) -> v)     tevss
             resultRecs <- mapM (mkSolverResult cexStr isSat . Right) tess
@@ -594,7 +622,7 @@ cmdProveSat isSat str = do
             pexpr <- replParseExpr str
 
             ~(EnvBool yes) <- getUser "show-examples"
-            when yes $ forM_ vss (printCounterexample isSat pexpr)
+            when yes $ forM_ vss (printSatisfyingModel pexpr)
 
             case (ty, exprs) of
               (t, [e]) -> bindItVariable t e

src/Cryptol/Symbolic.hs

@@ -22,6 +22,7 @@ module Cryptol.Symbolic
  , SatNum(..)
  , ProverResult(..)
  , ProverStats
+ , CounterExampleType(..)
    -- * FinType
  , FinType(..)
  , finType
@@ -76,11 +77,17 @@ data ProverCommand = ProverCommand {
 
 type ProverStats = NominalDiffTime
 
+-- | A @:prove@ command can fail either because some
+--   input causes the predicate to violate a safety assertion,
+--   or because the predicate returns false for some input.
+data CounterExampleType = SafetyViolation | PredicateFalsified
+
 -- | A prover result is either an error message, an empty result (eg
 -- for the offline prover), a counterexample or a lazy list of
 -- satisfying assignments.
 data ProverResult = AllSatResult [SatResult] -- LAZY
                   | ThmResult    [Type]
+                  | CounterExample CounterExampleType SatResult
                   | EmptyResult
                   | ProverError  String
 

src/Cryptol/Symbolic/SBV.hs

@@ -32,6 +32,8 @@ import Data.Maybe (fromMaybe)
 import qualified Data.Map as Map
 import qualified Control.Exception as X
 
+import qualified Data.SBV as SBV (sObserve)
+import qualified Data.SBV.Internals as SBV (SBV(..))
 import qualified Data.SBV.Dynamic as SBV
 import           Data.SBV (Timing(SaveTiming))
 import           Data.SBV.Internals (showTDiff)
@@ -253,6 +255,11 @@ prepareQuery evo modEnv ProverCommand{..} =
                      do env <- Eval.evalDecls SBV extDgs mempty
                         v <- Eval.evalExpr SBV env pcExpr
                         Eval.fromVBit <$> foldM Eval.fromVFun v (map pure args)
+
+                 -- "observe" the value of the safety predicate.  This makes its value
+                 -- avaliable in the resulting model.
+                 SBV.sObserve "safety" (SBV.SBV safety :: SBV.SBV Bool)
+
                  return (foldr addAsm (SBV.svAnd safety b) asms))
 
 
@@ -274,21 +281,15 @@ processResults evo ProverCommand{..} ts results =
     case results of
        -- allSat can return more than one as long as
        -- they're satisfiable
-       (SBV.Satisfiable {} : _) -> do
-         tevss <- mapM mkTevs results
+       (SBV.Satisfiable {} : _) | isSat -> do
+         tevss <- map snd <$> mapM (mkTevs prims) results
          return $ AllSatResult tevss
-         where
-           mkTevs result = do
-             let Right (_, cvs) = SBV.getModelAssignment result
-                 (vs, _) = parseValues ts cvs
-                 sattys = unFinType <$> ts
-             satexprs <-
-               doEval evo (zipWithM (Concrete.toExpr prims) sattys vs)
-             case zip3 sattys <$> (sequence satexprs) <*> pure vs of
-               Nothing ->
-                 panic "Cryptol.Symbolic.sat"
-                   [ "unable to make assignment into expression" ]
-               Just tevs -> return $ tevs
+
+       -- prove should only have one counterexample
+       [r@SBV.Satisfiable{}] -> do
+         (safety, res) <- mkTevs prims r
+         let cexType = if safety then PredicateFalsified else SafetyViolation
+         return $ CounterExample cexType res
 
        -- prove returns only one
        [SBV.Unsatisfiable {}] ->
@@ -302,6 +303,23 @@ processResults evo ProverCommand{..} ts results =
               where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
                           | otherwise = show . SBV.ThmResult . head
 
+  where
+  mkTevs prims result = do
+    -- It's a bit fragile, but the value of the safety predicate seems
+    -- to always be the first value in the model assignment list.
+    let Right (_, (safetyCV : cvs)) = SBV.getModelAssignment result
+        safety = SBV.cvToBool safetyCV
+        (vs, _) = parseValues ts cvs
+        sattys = unFinType <$> ts
+    satexprs <-
+      doEval evo (zipWithM (Concrete.toExpr prims) sattys vs)
+    case zip3 sattys <$> (sequence satexprs) <*> pure vs of
+      Nothing ->
+        panic "Cryptol.Symbolic.sat"
+          [ "unable to make assignment into expression" ]
+      Just tevs -> return $ (safety, tevs)
+
+
 -- | Execute a symbolic ':prove' or ':sat' command.
 --
 --   This command returns a pair: the first element is the name of the

src/Cryptol/Symbolic/What4.hs

@@ -154,7 +154,7 @@ satProve ProverCommand {..} =
             result <- case pcQueryType of
               ProveQuery ->
                 do q <- W4.notPred sym =<< W4.andPred sym safety b
-                   singleQuery sym evo primMap pcProverName logData ts args q
+                   singleQuery sym evo primMap pcProverName logData ts args (Just safety) q
 
               SatQuery num ->
                 do q <- W4.andPred sym safety b
@@ -217,7 +217,7 @@ multiSATQuery ::
   SatNum ->
   IO (Maybe String, ProverResult)
 multiSATQuery sym evo primMap solverName logData ts args query (SomeSat n) | n <= 1 =
-  singleQuery sym evo primMap solverName logData ts args query
+  singleQuery sym evo primMap solverName logData ts args Nothing query
 
 multiSATQuery sym evo primMap solverName logData ts args query satNum0 =
   do adpt <- lookupProver solverName
@@ -273,13 +273,14 @@ singleQuery ::
   W4.LogData ->
   [FinType] ->
   [VarShape sym] ->
+  Maybe (W4.Pred sym) {- ^ optional safety predicate.  Nothing = SAT query -} ->
   W4.Pred sym ->
   IO (Maybe String, ProverResult)
 
 --singleQuery _sym _evo _primMap "all" _logData _ts _args _query =
 --  do fail "TODO portfolio solver!"
 
-singleQuery sym evo primMap solverName logData ts args query =
+singleQuery sym evo primMap solverName logData ts args msafe query =
   do adpt <- lookupProver solverName
      W4.extendConfig (W4.solver_adapter_config_options adpt) (W4.getConfiguration sym)
      pres <- W4.solver_adapter_check_sat adpt sym logData [query] $ \res ->
@@ -288,7 +289,12 @@ singleQuery sym evo primMap solverName logData ts args query =
            W4.Unsat _ -> return (ThmResult (map unFinType ts))
            W4.Sat (evalFn,_) ->
              do model <- computeModel evo primMap evalFn ts args
-                return (AllSatResult [ model ])
+                case msafe of
+                  Just s ->
+                    do s' <- W4.groundEval evalFn s
+                       let cexType = if s' then PredicateFalsified else SafetyViolation
+                       return (CounterExample cexType model)
+                  Nothing -> return (AllSatResult [ model ])
 
      return (Just (W4.solver_adapter_name adpt), pres)