content: {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  module Grease.ErrorDescription (
    ErrorDescription (..),
    concretizeErrorDescription,
    ppMacawError,
    ppErrorDesc,
  ) where
  
  import Data.List qualified as List
  import Data.Macaw.Symbolic.Memory (MacawError (UnmappedGlobalMemoryAccess))
  import Data.Macaw.Symbolic.Memory qualified as MSM
  import Lang.Crucible.LLVM.Errors qualified as CLM
  import Lang.Crucible.LLVM.MemModel qualified as CLM
  import Lang.Crucible.LLVM.MemModel.CallStack qualified as CLM
  import Lang.Crucible.LLVM.MemModel.CallStack qualified as LLCS
  import Prettyprinter qualified as PP
  import What4.Expr qualified as W4
  import What4.Interface qualified as WI
  
  concretizeErrorDescription ::
    (WI.IsExprBuilder sym, sym ~ W4.ExprBuilder t st fs) =>
    sym ->
    W4.GroundEvalFn t ->
    ErrorDescription sym ->
    IO (ErrorDescription sym)
  concretizeErrorDescription
    sym
    (W4.GroundEvalFn gFn) =
      \case
        CrucibleLLVMError bb cs -> do
          bb' <- CLM.concBadBehavior sym gFn bb
          pure (CrucibleLLVMError bb' cs)
        (MacawMemError (UnmappedGlobalMemoryAccess ptrVal)) -> do
          cptr <- CLM.concPtr sym gFn ptrVal
          pure $ MacawMemError (UnmappedGlobalMemoryAccess cptr)
  
  -- | An error either from the underlying LLVM memory model or
  -- from Macaw.
  data ErrorDescription sym
    = CrucibleLLVMError (CLM.BadBehavior sym) LLCS.CallStack
    | MacawMemError (MSM.MacawError sym)
  
  -- | Pretty print a 'MSM.MacawError'
  -- TODO(#310) Pretty print macaw error using a macaw implementation
  ppMacawError :: WI.IsExpr (WI.SymExpr sym) => MSM.MacawError sym -> PP.Doc a
  ppMacawError (MSM.UnmappedGlobalMemoryAccess ptrVal) = "Read or write of an unmapped pointer:" PP.<+> CLM.ppPtr ptrVal
  
  ppErrorDesc :: WI.IsExpr (WI.SymExpr sym) => ErrorDescription sym -> PP.Doc a
  ppErrorDesc =
    \case
      MacawMemError mmErr -> ppMacawError mmErr
      CrucibleLLVMError bb callStack ->
        let ppCs = CLM.ppCallStack callStack
         in PP.vcat $
              [PP.indent 4 (CLM.ppBB bb)]
                List.++ if CLM.null callStack
                  then []
                  else ["in context:", PP.indent 2 ppCs]
  
  instance WI.IsExpr (WI.SymExpr sym) => PP.Pretty (ErrorDescription sym) where
    pretty :: WI.IsExpr (WI.SymExpr sym) => ErrorDescription sym -> PP.Doc ann
    pretty = ppErrorDesc
  