{-|
Copyright        : (c) Galois, Inc. 2025
Maintainer       : Langston Barrett <langston@galois.com>
-}

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Lang.Crucible.Debug.Response
  ( NotApplicable(..)
  , UserError(..)
  , ResponseExt
  , ProofResult(..)
  , Response(..)
  ) where

import Control.Exception (IOException)
import Data.Foldable qualified as Foldable
import Data.Kind (Type)
import Data.Sequence qualified as Seq
import Data.Text qualified as Text
import Data.Text (Text)
import Data.Void (Void, absurd)
import Lang.Crucible.Debug.Arg (ArgParseError)
import Lang.Crucible.Debug.Command.Base qualified as BCmd
import Lang.Crucible.Debug.Command (Command)
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.Debug.Regex (MatchError)
import Lang.Crucible.Debug.Statement (ParseError)
import Lang.Crucible.Debug.Statement qualified as Stmt
import Lang.Crucible.Debug.Style (Styled)
import Prettyprinter qualified as PP
import Text.Megaparsec.Error qualified as MP
import What4.FunctionName (FunctionName)
import What4.FunctionName qualified as W4
import What4.ProgramLoc qualified as W4

-- | The command was not applicable in this state
data NotApplicable
  = DoneSimulating
  | NoCfg
  | NoFrame
  | NotDone
  | NotYetSimulating
  deriving Int -> NotApplicable -> ShowS
[NotApplicable] -> ShowS
NotApplicable -> String
(Int -> NotApplicable -> ShowS)
-> (NotApplicable -> String)
-> ([NotApplicable] -> ShowS)
-> Show NotApplicable
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotApplicable -> ShowS
showsPrec :: Int -> NotApplicable -> ShowS
$cshow :: NotApplicable -> String
show :: NotApplicable -> String
$cshowList :: [NotApplicable] -> ShowS
showList :: [NotApplicable] -> ShowS
Show

instance PP.Pretty NotApplicable where
  pretty :: forall ann. NotApplicable -> Doc ann
pretty =
    \case
      NotApplicable
DoneSimulating -> Doc ann
"The simulator is no longer running"
      NotApplicable
NoCfg -> Doc ann
"Not executing a CFG"
      NotApplicable
NoFrame -> Doc ann
"Not in a call frame"
      NotApplicable
NotDone -> Doc ann
"Execution is not finished"
      NotApplicable
NotYetSimulating -> Doc ann
"The simulator is not yet running"

-- | The command could not be completed successfully for some reason the user
-- should have anticipated.
data UserError cExt
  = ArgError (Command cExt) (MatchError Text ArgParseError)
  | BadArgNumber Text
  | FnNotFound FunctionName [FunctionName]
  | LoadParseError (MP.ParseErrorBundle Text Void)
  | LoadSyntaxError (PP.Doc Void)
  | NoHelp [Text]
  | NoSuchArgument Int
  | NotACfg W4.FunctionName
  | NotApplicable NotApplicable
  | SourceParseError ParseError
  deriving Int -> UserError cExt -> ShowS
[UserError cExt] -> ShowS
UserError cExt -> String
(Int -> UserError cExt -> ShowS)
-> (UserError cExt -> String)
-> ([UserError cExt] -> ShowS)
-> Show (UserError cExt)
forall cExt. Show cExt => Int -> UserError cExt -> ShowS
forall cExt. Show cExt => [UserError cExt] -> ShowS
forall cExt. Show cExt => UserError cExt -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall cExt. Show cExt => Int -> UserError cExt -> ShowS
showsPrec :: Int -> UserError cExt -> ShowS
$cshow :: forall cExt. Show cExt => UserError cExt -> String
show :: UserError cExt -> String
$cshowList :: forall cExt. Show cExt => [UserError cExt] -> ShowS
showList :: [UserError cExt] -> ShowS
Show

instance PP.Pretty cExt => PP.Pretty (UserError cExt) where
  pretty :: forall ann. UserError cExt -> Doc ann
pretty =
    \case
      ArgError Command cExt
cmd MatchError Text ArgParseError
e ->
        [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep
        [ Doc ann
"Bad arguments for command" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Command cExt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Command cExt -> Doc ann
PP.pretty Command cExt
cmd Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
":"
        , MatchError Text ArgParseError -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MatchError Text ArgParseError -> Doc ann
PP.pretty MatchError Text ArgParseError
e
        ]
      BadArgNumber Text
txt ->
        Doc ann
"Bad argument number:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
txt
      FnNotFound FunctionName
nm [FunctionName]
nms ->
        [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
        [ Doc ann
"No such function:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty FunctionName
nm
        , if [FunctionName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunctionName]
nms
          then Doc ann
forall a. Monoid a => a
mempty
          else
            [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
            [ Doc ann
"Known functions:"
            , [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat ((FunctionName -> Doc ann) -> [FunctionName] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Text -> Doc ann)
-> (FunctionName -> Text) -> FunctionName -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctionName -> Text
W4.functionName) [FunctionName]
nms)
            ]
        ]
      LoadParseError ParseErrorBundle Text Void
err -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (ParseErrorBundle Text Void -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
MP.errorBundlePretty ParseErrorBundle Text Void
err)
      LoadSyntaxError Doc Void
err -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
err
      NoHelp [Text]
args -> Doc ann
"Can't help with" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Text -> [Text] -> Text
Text.intercalate Text
" " [Text]
args)
      NoSuchArgument Int
i -> Doc ann
"No such argument:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
i
      NotACfg FunctionName
fNm -> Doc ann
"Not a CFG:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (FunctionName -> Text
W4.functionName FunctionName
fNm)
      NotApplicable NotApplicable
err -> NotApplicable -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. NotApplicable -> Doc ann
PP.pretty NotApplicable
err
      SourceParseError ParseError
err ->
        Doc ann
"Parse error during" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+>
        Command Void -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Command Void -> Doc ann
PP.pretty (forall cExt. BaseCommand -> Command cExt
Cmd.Base @Void BaseCommand
BCmd.Source) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<>
        Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+>
        Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (ParseError -> Text
Stmt.renderParseError ParseError
err)

type ResponseExt :: Type -> Type
type family ResponseExt cExt :: Type
type instance ResponseExt Void = Void

data ProofResult
  = Proved
  | Disproved
  | Unknown
  deriving Int -> ProofResult -> ShowS
[ProofResult] -> ShowS
ProofResult -> String
(Int -> ProofResult -> ShowS)
-> (ProofResult -> String)
-> ([ProofResult] -> ShowS)
-> Show ProofResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProofResult -> ShowS
showsPrec :: Int -> ProofResult -> ShowS
$cshow :: ProofResult -> String
show :: ProofResult -> String
$cshowList :: [ProofResult] -> ShowS
showList :: [ProofResult] -> ShowS
Show

instance PP.Pretty ProofResult where
  pretty :: forall ann. ProofResult -> Doc ann
pretty =
    \case
      ProofResult
Proved -> Doc ann
"proved"
      ProofResult
Disproved -> Doc ann
"disproved"
      ProofResult
Unknown -> Doc ann
"unknown"

data Response cExt
  = Arg (PP.Doc Void)
  | Backtrace (PP.Doc Void)
  | Block (PP.Doc Void)
  | Cfg (PP.Doc Void)
  | Clear Int
  | Complete (PP.Doc Void)
  | Delete W4.FunctionName Bool
  | Frame (PP.Doc Void)
  | Help (PP.Doc Void)
  | IOError IOException
  | Load FilePath Int
  | Location W4.ProgramLoc
  | Obligation [PP.Doc Void]
  | PathCondition (PP.Doc Void)
  | Prove (Seq.Seq (PP.Doc Void, ProofResult))
  | ProveTimeout
  | Ok
  | Style [Styled]
  | Trace [PP.Doc Void]
  | Usage (PP.Doc Void)
  | UserError (UserError cExt)
  | XResponse (ResponseExt cExt)

deriving instance (Show (ResponseExt cExt), Show cExt) => Show (Response cExt)

instance (PP.Pretty (ResponseExt cExt), PP.Pretty cExt) => PP.Pretty (Response cExt) where
  pretty :: forall ann. Response cExt -> Doc ann
pretty =
    \case
      Arg Doc Void
a -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
a
      Backtrace Doc Void
bt -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
bt
      Block Doc Void
b -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
b
      Cfg Doc Void
c -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
c
      Complete Doc Void
c -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
c
      Clear Int
0 -> Doc ann
"No proof obligations to clear"
      Clear Int
1 -> Doc ann
"Cleared 1 proof obligation"
      Clear Int
n -> Doc ann
"Cleared" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"proof obligations"
      Delete FunctionName
nm Bool
True -> Doc ann
"Deleted breakpoint at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (FunctionName -> Text
W4.functionName FunctionName
nm)
      Delete FunctionName
nm Bool
False -> Doc ann
"No breakpoint at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (FunctionName -> Text
W4.functionName FunctionName
nm)
      Frame Doc Void
f -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
f
      Help Doc Void
h -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
h
      Style [Styled]
styles -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.hsep ((Styled -> Doc ann) -> [Styled] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Styled -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Styled -> Doc ann
PP.pretty [Styled]
styles)
      Load String
p Int
i -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.hsep [Doc ann
"Loaded", Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Int
i, Doc ann
"CFGs from", String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
p]
      IOError IOException
e -> IOException -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow IOException
e
      Location ProgramLoc
l -> FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty (ProgramLoc -> FunctionName
W4.plFunction ProgramLoc
l) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Position -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (ProgramLoc -> Position
W4.plSourceLoc ProgramLoc
l)
      Obligation [Doc Void]
obls ->
        if [Doc Void] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc Void]
obls
        then Doc ann
"No proof obligations"
        else [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep ((Doc Void -> Doc ann) -> [Doc Void] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map ((Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd) [Doc Void]
obls)
      PathCondition Doc Void
p -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
p
      Prove Seq (Doc Void, ProofResult)
results ->
        if Seq (Doc Void, ProofResult) -> Bool
forall a. Seq a -> Bool
Seq.null Seq (Doc Void, ProofResult)
results
        then Doc ann
"No obligations to prove"
        else
          [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
            ((Doc Void, ProofResult) -> Doc ann)
-> [(Doc Void, ProofResult)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map
              (\(Doc Void
goal, ProofResult
result) -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat [(Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
goal, ProofResult -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ProofResult -> Doc ann
PP.pretty ProofResult
result])
              (Seq (Doc Void, ProofResult) -> [(Doc Void, ProofResult)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Seq (Doc Void, ProofResult)
results)
      Response cExt
ProveTimeout -> Doc ann
"Proof timed out!"
      Response cExt
Ok -> Doc ann
"Ok"
      Trace [Doc Void]
t -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
PP.punctuate Doc ann
forall ann. Doc ann
PP.line ((Doc Void -> Doc ann) -> [Doc Void] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map ((Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd) [Doc Void]
t))
      Usage Doc Void
u -> (Void -> ann) -> Doc Void -> Doc ann
forall a b. (a -> b) -> Doc a -> Doc b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Void -> ann
forall a. Void -> a
absurd Doc Void
u
      UserError UserError cExt
e -> UserError cExt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. UserError cExt -> Doc ann
PP.pretty UserError cExt
e
      XResponse ResponseExt cExt
rExt -> ResponseExt cExt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. ResponseExt cExt -> Doc ann
PP.pretty ResponseExt cExt
rExt