Debug.hs

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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Debug
  ( debugger
  , bareDebuggerExt
  , bareDebugger
  , Inps.Inputs(..)
  , Inps.defaultDebuggerInputs
  , Inps.prepend
  , Outps.prettyOut
  , Outps.Outputs(..)
  , Outps.defaultDebuggerOutputs
  , Arg.Arg(..)
  , AType.ArgTypeRepr(..)
  , type AType.Breakpoint
  , type AType.Exactly
  , type AType.Function
  , type AType.Int
  , type AType.Path
  , type AType.Text
  , Cmd.Command(Base, Ext)
  , Cmd.CommandExt(..)
  , Cmd.voidExts
  , Cmds.execStateSimState
  , Ctxt.EvalResult(..)
  , Ctxt.Context(..)
  , Ctxt.CommandImpl(..)
  , Ctxt.ExtImpl(..)
  , Ctxt.voidImpl
  , Ctxt.DebuggerState(..)
  , Resp.Response(Ok, UserError, XResponse)
  , Resp.UserError(NotApplicable)
  , Resp.NotApplicable(DoneSimulating, NotYetSimulating)
  , Resp.ResponseExt
  , type Rgx.Regex
  , type Rgx.Empty
  , type Rgx.Lit
  , type (Rgx.:|)
  , type Rgx.Then
  , type Rgx.Star
  , Rgx.Match(..)
  , Rgx.RegexRepr(..)
  , Stmt.ParseError
  , Stmt.parse
  , Stmt.renderParseError
  , Trace.Trace
  , Trace.TraceEntry(..)
  , Trace.latest
  , IntrinsicPrinters(..)
  , Ctxt.initCtx
  , Pers.HasContext(..)
  , Ov.debuggerPrepend
  , Ov.debuggerQuit
  , Ov.debuggerStop
  , Ov.debugOverride
  , Ov.debugRunOverride
  ) where

import Control.Applicative qualified as Applicative
import Control.Lens qualified as Lens
import Control.Monad qualified as Monad
import Data.Function ((&))
import Data.Maybe qualified as Maybe
import Data.Parameterized.Map qualified as MapF
import Data.Parameterized.Nonce qualified as Nonce
import Data.Parameterized.Some (Some(Some))
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Void (Void)
import Lang.Crucible.Backend qualified as C
import Lang.Crucible.Backend.Simple qualified as C
import Lang.Crucible.CFG.Extension qualified as C
import Lang.Crucible.Debug.Arg qualified as Arg
import Lang.Crucible.Debug.Arg.Type qualified as AType
import Lang.Crucible.Debug.Breakpoint qualified as Break
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.Debug.Commands qualified as Cmds
import Lang.Crucible.Debug.Complete qualified as Complete
import Lang.Crucible.Debug.Complete (CompletionT)
import Lang.Crucible.Debug.Context (Context, DebuggerState)
import Lang.Crucible.Debug.Context qualified as Ctxt
import Lang.Crucible.Debug.Eval (EvalResult)
import Lang.Crucible.Debug.Eval qualified as Eval
import Lang.Crucible.Debug.Inputs (Inputs)
import Lang.Crucible.Debug.Inputs qualified as Inps
import Lang.Crucible.Debug.Outputs (Outputs)
import Lang.Crucible.Debug.Outputs qualified as Outps
import Lang.Crucible.Debug.Override qualified as Ov
import Lang.Crucible.Debug.Personality qualified as Pers
import Lang.Crucible.Debug.Regex qualified as Rgx
import Lang.Crucible.Debug.Response qualified as Resp
import Lang.Crucible.Debug.Response (Response)
import Lang.Crucible.Debug.Statement (Statement)
import Lang.Crucible.Debug.Statement qualified as Stmt
import Lang.Crucible.Debug.Style qualified as Style
import Lang.Crucible.Debug.Style (StyleT)
import Lang.Crucible.Debug.Trace qualified as Trace
import Lang.Crucible.FunctionHandle qualified as C
import Lang.Crucible.Pretty (IntrinsicPrinters(..))
import Lang.Crucible.Simulator.CallFrame qualified as C
import Lang.Crucible.Simulator.EvalStmt qualified as C
import Lang.Crucible.Simulator.ExecutionTree qualified as C
import Lang.Crucible.Simulator qualified as C
import Lang.Crucible.Syntax.Concrete qualified as C
import Lang.Crucible.Types qualified as C
import Prettyprinter qualified as PP
import Prettyprinter.Render.Text qualified as PP
import System.Exit qualified as Exit
import System.IO (stdout)
import What4.Expr qualified as W4
import What4.Interface qualified as W4

-- Useful for debugging
_printState :: C.ExecState p sym ext rtp -> Text
_printState =
  \case
    C.AbortState {} -> "AbortState"
    C.CallState {} -> "CallState"
    C.TailCallState {} -> "TailCallState"
    C.ReturnState {} -> "ReturnState"
    C.ResultState {} -> "ResultState"
    C.InitialState {} -> "InitialState"
    C.OverrideState {} -> "OverrideState"
    C.RunningState {} -> "RunningState"
    C.SymbolicBranchState {} -> "SymbolicBranchState"
    C.BranchMergeState {} -> "BranchMergeState"
    C.ControlTransferState {} -> "ControlTransferState"
    C.UnwindCallState {} -> "UnwindCallState"

stepState ::
  Context cExt sym ext t ->
  C.ExecState p sym ext rtp ->
  IO DebuggerState
stepState ctx =
  \case
    C.AbortState {} ->
      if Ctxt.dbgStopOnAbort ctx
      then pure Ctxt.Stopped
      else pure initState
    C.CallState _retHandler frm _st -> do
      C.SomeHandle hdl <- pure (C.resolvedCallHandle frm)
      stepCall hdl
    C.TailCallState _vfv frm _st -> do
      C.SomeHandle hdl <- pure (C.resolvedCallHandle frm)
      stepCall hdl
    C.ReturnState _fnm _vfv _ret _st ->
      case initState of
        Ctxt.Running Ctxt.Finish -> pure Ctxt.Stopped
        _ -> pure initState
    C.RunningState (C.RunBlockEnd _) simState -> do
      let fr = simState Lens.^. C.stateCrucibleFrame
      C.CallFrame { C._frameCFG = cfg, C._frameBlockID = blkId } <- pure fr
      let ent = Trace.TraceEntry cfg blkId
      Trace.append (Ctxt.dbgTrace ctx) ent
      pure initState

    -- Nothing to do for these...
    C.InitialState {} -> pure initState
    C.OverrideState {} -> pure initState
    C.ResultState {} -> pure initState
    C.RunningState {} -> pure initState
    C.SymbolicBranchState {} -> pure initState

    -- These are mostly implementation details...
    C.BranchMergeState {} -> pure initState
    C.ControlTransferState {} -> pure initState
    C.UnwindCallState {} -> pure initState
  where
    initState = Ctxt.dbgState ctx

    stepCall :: C.FnHandle args ret ->  IO DebuggerState
    stepCall hdl = do
      let b = Break.BreakFunction (C.handleName hdl)
      if Set.member b (Ctxt.dbgBreakpoints ctx)
      then pure Ctxt.Stopped
      else pure initState

mergeResults ::
  C.ExecutionFeatureResult p sym ext ret ->
  C.ExecutionFeatureResult p sym ext ret ->
  C.ExecutionFeatureResult p sym ext ret
mergeResults old new =
  case old of
    C.ExecutionFeatureNoChange -> new
    _ ->
      case new of
        C.ExecutionFeatureNoChange -> old
        _ -> new

resultState ::
  C.ExecutionFeatureResult p sym ext ret ->
  Maybe (C.ExecState p sym ext ret)
resultState =
  \case
    C.ExecutionFeatureNoChange -> Nothing
    C.ExecutionFeatureModifiedState s -> Just s
    C.ExecutionFeatureNewState s -> Just s

stopped ::
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  W4.IsExpr (W4.SymExpr sym) =>
  Context cExt sym ext t ->
  Ctxt.ExtImpl cExt p sym ext t ->
  C.ExecState p sym ext (C.RegEntry sym t) ->
  IO (EvalResult cExt p sym ext t)
stopped ctx0 ext execState0 = go ctx0 execState0 C.ExecutionFeatureNoChange
  where
    go c0 s0 r = do
      let cEnv = Ctxt.toCompletionEnv c0 s0
      let sEnv = Ctxt.toStyleEnv c0 s0
      stmt <- Style.runStyleM sEnv (Complete.runCompletionM cEnv (Inps.recv (Ctxt.dbgInputs c0)))
      result0 <- Eval.eval c0 ext s0 stmt
      let featResult = mergeResults r (Eval.evalFeatureResult result0)
      let result = result0 { Eval.evalFeatureResult = featResult }
      let s = Maybe.fromMaybe s0 (resultState featResult)
      let c = Eval.evalCtx result
      Outps.send (Ctxt.dbgOutputs c) (Eval.evalResp result)
      case Ctxt.dbgState c of
        Ctxt.Quit -> pure result
        Ctxt.Running {} -> pure result
        Ctxt.Stopped -> go c s featResult

dispatch ::
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  W4.IsExpr (W4.SymExpr sym) =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Context cExt sym ext t ->
  Ctxt.ExtImpl cExt p sym ext t ->
  C.ExecState p sym ext (C.RegEntry sym t) ->
  IO (Context cExt sym ext t, C.ExecutionFeatureResult p sym ext (C.RegEntry sym t))
dispatch ctx0 ext execState =
  case Ctxt.dbgState ctx0 of
    Ctxt.Quit ->
      pure (ctx0, C.ExecutionFeatureNoChange)
    Ctxt.Running {} | C.ResultState {} <- execState -> do
      let ctx = ctx0 { Ctxt.dbgState = Ctxt.Stopped }
      dispatch ctx ext execState
    Ctxt.Running (Ctxt.Step i) | i <= 1 -> do
      let ctx = ctx0 { Ctxt.dbgState = Ctxt.Stopped }
      dispatch ctx ext execState
    Ctxt.Running (Ctxt.Step i) -> do
      let ctx = ctx0 { Ctxt.dbgState = Ctxt.Running (Ctxt.Step (i - 1)) }
      state <- stepState ctx execState
      let ctx' = ctx0 { Ctxt.dbgState = state }
      pure (ctx', C.ExecutionFeatureNoChange)
    Ctxt.Running {} -> do
      state <- stepState ctx0 execState
      let ctx = ctx0 { Ctxt.dbgState = state }
      pure (ctx, C.ExecutionFeatureNoChange)
    Ctxt.Stopped -> do
      result <- stopped ctx0 ext execState
      pure (Eval.evalCtx result, Eval.evalFeatureResult result)

debugger ::
  Pers.HasContext p cExt sym ext t =>
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  W4.IsExpr (W4.SymExpr sym) =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Ctxt.ExtImpl cExt p sym ext t ->
  C.ExecutionFeature p sym ext (C.RegEntry sym t)
debugger ext =
  C.ExecutionFeature $ \execState -> do
    let simCtx = execState Lens.^. Lens.to C.execStateContext
    let ctx0 = simCtx Lens.^. C.cruciblePersonality . Pers.context
    (ctx, featResult) <- dispatch ctx0 ext execState
    let simCtx' = 
          case featResult of
            C.ExecutionFeatureNoChange -> simCtx
            C.ExecutionFeatureModifiedState execState' ->
              C.execStateContext execState'
            C.ExecutionFeatureNewState execState' ->
              C.execStateContext execState'
    let simCtx'' = simCtx' & C.cruciblePersonality . Pers.context Lens..~ ctx
    pure $
      case featResult of
        C.ExecutionFeatureNoChange ->
          C.ExecutionFeatureModifiedState
            (C.setExecStateContext simCtx'' execState)
        C.ExecutionFeatureModifiedState execState' ->
          C.ExecutionFeatureModifiedState
            (C.setExecStateContext simCtx'' execState')
        C.ExecutionFeatureNewState execState' ->
          C.ExecutionFeatureNewState
            (C.setExecStateContext simCtx'' execState')

-- | Like 'bareDebugger', but with a syntax extension
bareDebuggerExt ::
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Cmd.CommandExt cExt ->
  (forall p sym t. C.IsSymInterface sym => Ctxt.ExtImpl cExt p sym ext t) ->
  (forall p sym. C.IsSymInterface sym => C.ExtensionImpl p sym ext) ->
  Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) ->
  Outputs IO (Response cExt) ->
  (Text -> IO ()) ->
  IO ()
bareDebuggerExt cExts cEval extImpl inps outps logger = do
  Some nonceGen <- Nonce.newIONonceGenerator
  ha <- C.newHandleAllocator
  sym <- W4.newExprBuilder W4.FloatIEEERepr W4.EmptyExprBuilderState nonceGen
  bak <- C.newSimpleBackend sym
  let retType = C.UnitRepr
  let fns = C.FnBindings C.emptyHandleMap
  initCtx <- do
    let iFns = IntrinsicPrinters MapF.empty
    Ctxt.initCtx cExts iFns inps outps retType
  let simCtx = C.initSimContext bak C.emptyIntrinsicTypes ha stdout fns extImpl initCtx
  let ov = C.runOverrideSim retType $ return ()
  let simSt  = C.InitialState simCtx C.emptyGlobals C.defaultAbortHandler retType ov
  Monad.void $ C.executeCrucible [debugger cEval] simSt
  C.getProofObligations bak >>= \case
    Nothing -> pure ()
    Just obls -> do
      logger "There were unhandled proof obligations! Try `prove` and `clear`."
      let goals = C.goalsToList obls
      prettyGoals <- mapM (C.ppProofObligation sym) goals
      let render =  PP.renderStrict . PP.layoutSmart PP.defaultLayoutOptions
      logger (render (PP.vcat prettyGoals))
      Exit.exitFailure

-- | Start a debugger instance in an empty Crucible program.
--
-- The Crucible program simply returns the unit value. The idea is to use the
-- @Load@ and @Call@ commands to actually run some Crucible CFG(s).
--
-- Proves obligations using Z3.
bareDebugger ::
  Inputs (CompletionT Void (StyleT Void IO)) (Statement Void) ->
  Outputs IO (Response Void) ->
  (Text -> IO ()) ->
  IO ()
bareDebugger inps outps logger =
  let ?parserHooks = C.ParserHooks Applicative.empty Applicative.empty in
  bareDebuggerExt
    Cmd.voidExts
    Ctxt.voidImpl
    C.emptyExtensionImpl
    inps
    outps
    logger