{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
-- | This module provides various default formatters for outputting
-- information in human readable form.  Alternative versions should be
-- used where appropriate.

module Crux.FormatOut
  (
    sayWhatResultStatus
  , sayWhatFailedGoals
  )
where

import qualified Data.BitVector.Sized as BV
import           Data.Foldable ( toList )
import           Data.Sequence (Seq)
import qualified Data.Text as Text (Text)
import           Prettyprinter ( (<+>) )
import qualified Prettyprinter as PP
import qualified Prettyprinter.Render.Text as PPR

import           What4.Expr (GroundValueWrapper(..), GroundValue)
import           What4.BaseTypes
import           What4.ProgramLoc

import           Lang.Crucible.Backend (CrucibleEvent(..))
import qualified Lang.Crucible.Simulator.SimError as CSE

import           Crux.Types

sayWhatResultStatus :: CruxSimulationResult -> SayWhat
sayWhatResultStatus :: CruxSimulationResult -> SayWhat
sayWhatResultStatus (CruxSimulationResult ProgramCompleteness
cmpl Seq (ProcessedGoals, ProvedGoals)
gls) =
  let tot :: Integer
tot        = Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (ProcessedGoals -> Integer
totalProcessedGoals (ProcessedGoals -> Integer)
-> ((ProcessedGoals, ProvedGoals) -> ProcessedGoals)
-> (ProcessedGoals, ProvedGoals)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProcessedGoals, ProvedGoals) -> ProcessedGoals
forall a b. (a, b) -> a
fst ((ProcessedGoals, ProvedGoals) -> Integer)
-> Seq (ProcessedGoals, ProvedGoals) -> Seq Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (ProcessedGoals, ProvedGoals)
gls)
      proved :: Integer
proved     = Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (ProcessedGoals -> Integer
provedGoals (ProcessedGoals -> Integer)
-> ((ProcessedGoals, ProvedGoals) -> ProcessedGoals)
-> (ProcessedGoals, ProvedGoals)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProcessedGoals, ProvedGoals) -> ProcessedGoals
forall a b. (a, b) -> a
fst ((ProcessedGoals, ProvedGoals) -> Integer)
-> Seq (ProcessedGoals, ProvedGoals) -> Seq Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (ProcessedGoals, ProvedGoals)
gls)
      disproved :: Integer
disproved  = Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (ProcessedGoals -> Integer
disprovedGoals (ProcessedGoals -> Integer)
-> ((ProcessedGoals, ProvedGoals) -> ProcessedGoals)
-> (ProcessedGoals, ProvedGoals)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProcessedGoals, ProvedGoals) -> ProcessedGoals
forall a b. (a, b) -> a
fst ((ProcessedGoals, ProvedGoals) -> Integer)
-> Seq (ProcessedGoals, ProvedGoals) -> Seq Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (ProcessedGoals, ProvedGoals)
gls)
      incomplete :: Integer
incomplete = Seq Integer -> Integer
forall a. Num a => Seq a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (ProcessedGoals -> Integer
incompleteGoals (ProcessedGoals -> Integer)
-> ((ProcessedGoals, ProvedGoals) -> ProcessedGoals)
-> (ProcessedGoals, ProvedGoals)
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProcessedGoals, ProvedGoals) -> ProcessedGoals
forall a b. (a, b) -> a
fst ((ProcessedGoals, ProvedGoals) -> Integer)
-> Seq (ProcessedGoals, ProvedGoals) -> Seq Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (ProcessedGoals, ProvedGoals)
gls)
      unknown :: Integer
unknown    = Integer
tot Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
proved Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
disproved Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
incomplete)
      goalSummary :: Doc Any
goalSummary = if Integer
tot Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then
                      Doc Any
"All goals discharged through internal simplification."
                    else
                      Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.nest Int
2 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$
                      [Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
PP.vcat [ Doc Any
"Goal status:"
                              , Doc Any
"Total:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc Any
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
tot
                              , Doc Any
"Proved:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc Any
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
proved
                              , Doc Any
"Disproved:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc Any
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
disproved
                              , Doc Any
"Incomplete:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc Any
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
incomplete
                              , Doc Any
"Unknown:" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc Any
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Integer
unknown
                              ]
  in SayWhat -> SayWhat -> SayWhat
SayMore
     (SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
"Crux" (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ Doc Any -> Text
forall ann. Doc ann -> Text
ppToText Doc Any
goalSummary)
     (SayWhat -> SayWhat) -> SayWhat -> SayWhat
forall a b. (a -> b) -> a -> b
$ if | Integer
disproved Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 ->
              SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Fail Text
"Crux" Text
"Overall status: Invalid."
          | Integer
incomplete Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 Bool -> Bool -> Bool
|| ProgramCompleteness
cmpl ProgramCompleteness -> ProgramCompleteness -> Bool
forall a. Eq a => a -> a -> Bool
== ProgramCompleteness
ProgramIncomplete ->
              SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Warn Text
"Crux" Text
"Overall status: Unknown (incomplete)."
          | Integer
unknown Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Warn Text
"Crux" Text
"Overall status: Unknown."
          | Integer
proved Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
tot -> SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
OK Text
"Crux" Text
"Overall status: Valid."
          | Bool
otherwise ->
              SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Fail Text
"Crux" Text
"Internal error computing overall status."

sayWhatFailedGoals :: Bool -> Bool -> Seq ProvedGoals -> SayWhat
sayWhatFailedGoals :: Bool -> Bool -> Seq ProvedGoals -> SayWhat
sayWhatFailedGoals Bool
skipIncompl Bool
showVars Seq ProvedGoals
allGls =
  if [Doc Void] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc Void]
allDocs
     then SayWhat
SayNothing
     else SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Fail Text
"Crux" (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ Doc Void -> Text
forall ann. Doc ann -> Text
ppToText (Doc Void -> Text) -> Doc Void -> Text
forall a b. (a -> b) -> a -> b
$ [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vsep [Doc Void]
allDocs
 where
  failedDoc :: ProvedGoals -> [Doc Void]
failedDoc = \case
    Branch ProvedGoals
gls1 ProvedGoals
gls2 -> ProvedGoals -> [Doc Void]
failedDoc ProvedGoals
gls1 [Doc Void] -> [Doc Void] -> [Doc Void]
forall a. Semigroup a => a -> a -> a
<> ProvedGoals -> [Doc Void]
failedDoc ProvedGoals
gls2
    ProvedGoal{} -> []
    NotProvedGoal [CrucibleAssumption (Const ())]
_asmps SimError
err Doc Void
ex [ProgramLoc]
_locs Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
mdl [String]
s ->
      if | Bool
skipIncompl, CSE.SimError ProgramLoc
_ (CSE.ResourceExhausted String
_) <- SimError
err -> []
         | Just (ModelView
_m,[CrucibleEvent GroundValueWrapper]
evs) <- Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
mdl ->
             [ Int -> Doc Void -> Doc Void
forall ann. Int -> Doc ann -> Doc ann
PP.nest Int
2 (Doc Void -> Doc Void) -> Doc Void -> Doc Void
forall a b. (a -> b) -> a -> b
$ [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat (
               [ Doc Void
"Found counterexample for verification goal"
               -- n.b. prefer the prepared pretty explanation, but
               -- if not available, use the NotProved information.
               -- Don't show both: they tend to be duplications.
               , if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Doc Void -> String
forall a. Show a => a -> String
show Doc Void
ex) then SimError -> Doc Void
forall a ann. Show a => a -> Doc ann
PP.viaShow SimError
err else Doc Void
ex
               ] -- if `showVars` is set, print the sequence of symbolic
                 -- variable events that led to this failure
                 [Doc Void] -> [Doc Void] -> [Doc Void]
forall a. [a] -> [a] -> [a]
++ if Bool
showVars then
                      [Doc Void
"Symbolic variables:", Int -> Doc Void -> Doc Void
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 ([Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat ([CrucibleEvent GroundValueWrapper] -> [Doc Void]
forall {m :: * -> *} {ann}.
MonadFail m =>
m (CrucibleEvent GroundValueWrapper) -> m (Doc ann)
ppVars [CrucibleEvent GroundValueWrapper]
evs))]
                    else []
                 -- print abducts, if any
                 [Doc Void] -> [Doc Void] -> [Doc Void]
forall a. [a] -> [a] -> [a]
++ if [String]
s [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] then
                      let numFacts :: Int
numFacts = [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
s
                          -- NB: If you update the contents of this error
                          -- message, make sure to update the corresponding
                          -- regexes that check for this in
                          -- crux-llvm/test/Test.hs.
                          herald :: Doc Void
herald = Doc Void -> Doc Void -> Int -> Doc Void
forall amount doc.
(Num amount, Eq amount) =>
doc -> doc -> amount -> doc
PP.plural
                                     Doc Void
"The following fact"
                                     (Doc Void
"One of the following"
                                        Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Int -> Doc Void
forall a ann. Show a => a -> Doc ann
PP.viaShow Int
numFacts
                                        Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc Void
"facts")
                                     Int
numFacts Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc Void
"would entail the goal" in
                      Doc Void
herald Doc Void -> [Doc Void] -> [Doc Void]
forall a. a -> [a] -> [a]
: ((String -> Doc Void) -> [String] -> [Doc Void]
forall a b. (a -> b) -> [a] -> [b]
map (\String
x -> String -> Doc Void
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Char
'*' Char -> String -> String
forall a. a -> [a] -> [a]
: Char
' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
x)) [String]
s)
                    else [])]
         | Bool
otherwise ->
           [ Int -> Doc Void -> Doc Void
forall ann. Int -> Doc ann -> Doc ann
PP.nest Int
2 (Doc Void -> Doc Void) -> Doc Void -> Doc Void
forall a b. (a -> b) -> a -> b
$ [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat [ Doc Void
"Failed to prove verification goal", Doc Void
ex ] ]

  ppVars :: m (CrucibleEvent GroundValueWrapper) -> m (Doc ann)
ppVars m (CrucibleEvent GroundValueWrapper)
evs =
    do CreateVariableEvent ProgramLoc
loc String
nm BaseTypeRepr tp
tpr (GVW GroundValue tp
v) <- m (CrucibleEvent GroundValueWrapper)
evs
       Doc ann -> m (Doc ann)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProgramLoc
-> String -> BaseTypeRepr tp -> GroundValue tp -> Doc ann
forall {a} {tp :: BaseType} {ann}.
Pretty a =>
ProgramLoc -> a -> BaseTypeRepr tp -> GroundValue tp -> Doc ann
ppVarEvent ProgramLoc
loc String
nm BaseTypeRepr tp
tpr GroundValue tp
v)

  ppVarEvent :: ProgramLoc -> a -> BaseTypeRepr tp -> GroundValue tp -> Doc ann
ppVarEvent ProgramLoc
loc a
nm BaseTypeRepr tp
tpr GroundValue tp
v =
    a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty a
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> BaseTypeRepr tp -> GroundValue tp -> Doc ann
forall (tp :: BaseType) ann.
BaseTypeRepr tp -> GroundValue tp -> Doc ann
ppVal BaseTypeRepr tp
tpr GroundValue tp
v Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc ann
forall ann. Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc)

  ppVal :: BaseTypeRepr tp -> GroundValue tp -> PP.Doc ann
  ppVal :: forall (tp :: BaseType) ann.
BaseTypeRepr tp -> GroundValue tp -> Doc ann
ppVal BaseTypeRepr tp
tpr GroundValue tp
v = case BaseTypeRepr tp
tpr of
    BaseBVRepr NatRepr w
_w -> Integer -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (BV w -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV w
GroundValue tp
v)
    BaseFloatRepr FloatPrecisionRepr fpp
_fpp -> BigFloat -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow BigFloat
GroundValue tp
v
    BaseTypeRepr tp
BaseRealRepr -> Rational -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow Rational
GroundValue tp
v
    BaseTypeRepr tp
_ -> Doc ann
"<unknown>" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> BaseTypeRepr tp -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow BaseTypeRepr tp
tpr

  allDocs :: [Doc Void]
allDocs = [[Doc Void]] -> [Doc Void]
forall a. Monoid a => [a] -> a
mconcat (ProvedGoals -> [Doc Void]
failedDoc (ProvedGoals -> [Doc Void]) -> [ProvedGoals] -> [[Doc Void]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq ProvedGoals -> [ProvedGoals]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq ProvedGoals
allGls)



ppToText :: PP.Doc ann -> Text.Text
ppToText :: forall ann. Doc ann -> Text
ppToText = SimpleDocStream ann -> Text
forall ann. SimpleDocStream ann -> Text
PPR.renderStrict (SimpleDocStream ann -> Text)
-> (Doc ann -> SimpleDocStream ann) -> Doc ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc ann -> SimpleDocStream ann
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
PP.layoutPretty LayoutOptions
PP.defaultLayoutOptions