FormatOut.hs

{-# 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
import Lang.Crucible.Simulator.SimError (ppProgramStack, simErrorContext)

sayWhatResultStatus :: CruxSimulationResult -> SayWhat
sayWhatResultStatus (CruxSimulationResult cmpl gls) =
  let tot        = sum (totalProcessedGoals . fst <$> gls)
      proved     = sum (provedGoals . fst <$> gls)
      disproved  = sum (disprovedGoals . fst <$> gls)
      incomplete = sum (incompleteGoals . fst <$> gls)
      unknown    = tot - (proved + disproved + incomplete)
      goalSummary = if tot == 0 then
                      "All goals discharged through internal simplification."
                    else
                      PP.nest 2 $
                      PP.vcat [ "Goal status:"
                              , "Total:" <+> PP.pretty tot
                              , "Proved:" <+> PP.pretty proved
                              , "Disproved:" <+> PP.pretty disproved
                              , "Incomplete:" <+> PP.pretty incomplete
                              , "Unknown:" <+> PP.pretty unknown
                              ]
  in SayMore
     (SayWhat Simply "Crux" $ ppToText goalSummary)
     $ if | disproved > 0 ->
              SayWhat Fail "Crux" "Overall status: Invalid."
          | incomplete > 0 || cmpl == ProgramIncomplete ->
              SayWhat Warn "Crux" "Overall status: Unknown (incomplete)."
          | unknown > 0 -> SayWhat Warn "Crux" "Overall status: Unknown."
          | proved == tot -> SayWhat OK "Crux" "Overall status: Valid."
          | otherwise ->
              SayWhat Fail "Crux" "Internal error computing overall status."

sayWhatFailedGoals :: Bool -> Bool -> Seq ProvedGoals -> SayWhat
sayWhatFailedGoals skipIncompl showVars allGls =
  if null allDocs
     then SayNothing
     else SayWhat Fail "Crux" $ ppToText $ PP.vsep allDocs
 where
  failedDoc = \case
    Branch gls1 gls2 -> failedDoc gls1 <> failedDoc gls2
    ProvedGoal{} -> []
    NotProvedGoal _asmps err ex _locs mdl s ->
      if | skipIncompl, CSE.SimError _ (CSE.ResourceExhausted _) <- err -> []
         | Just (_m,evs) <- mdl ->
             [ PP.nest 2 $ PP.vcat (
               [ "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.
               ] ++ case (show ex, simErrorContext err) of
                      ([], _) ->  [  PP.viaShow err ] 
                      (_, Nothing) -> [ex]
                      (_, Just ctx) ->
                        [ex, "Context:", PP.indent 2 (ppProgramStack ctx)]
                 -- if `showVars` is set, print the sequence of symbolic
                 -- variable events that led to this failure
                 ++ if showVars then
                      ["Symbolic variables:", PP.indent 2 (PP.vcat (ppVars evs))]
                    else []
                 -- print abducts, if any
                 ++ if s /= [] then
                      let numFacts = length 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 = PP.plural
                                     "The following fact"
                                     ("One of the following"
                                        PP.<+> PP.viaShow numFacts
                                        PP.<+> "facts")
                                     numFacts PP.<+> "would entail the goal" in
                      herald : (map (\x -> PP.pretty ('*' : ' ' : x)) s)
                    else [])]
         | otherwise ->
           [ PP.nest 2 $ PP.vcat [ "Failed to prove verification goal", ex ] ]

  ppVars evs =
    do CreateVariableEvent loc nm tpr (GVW v) <- evs
       pure (ppVarEvent loc nm tpr v)

  ppVarEvent loc nm tpr v =
    PP.pretty nm PP.<+> "=" PP.<+> ppVal tpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc)

  ppVal :: BaseTypeRepr tp -> GroundValue tp -> PP.Doc ann
  ppVal tpr v = case tpr of
    BaseBVRepr _w -> PP.viaShow (BV.asUnsigned v)
    BaseFloatRepr _fpp -> PP.viaShow v
    BaseRealRepr -> PP.viaShow v
    _ -> "<unknown>" PP.<+> PP.viaShow tpr

  allDocs = mconcat (failedDoc <$> toList allGls)



ppToText :: PP.Doc ann -> Text.Text
ppToText = PPR.renderStrict . PP.layoutPretty PP.defaultLayoutOptions