{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
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"
, 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
]
[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 []
[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
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