{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
module Copilot.Verifier.Log
  ( SupportsCopilotLogMessage
  , CopilotLogMessage(..)
  , VerificationStep(..)
  , StateRelationStep(..)
  , VerifierAssertion(..)
  , SomeSome(..)
  , StreamValueEquality(..)
  , TriggersInvokedCorrespondingly(..)
  , TriggerArgumentEquality(..)
  , RingBufferLoad(..)
  , RingBufferIndexLoad(..)
  , PointerArgumentLoad(..)
  , AccessorFunctionLoad(..)
  , GuardFunctionLoad(..)
  , UnknownFunctionLoad(..)
  , LLVMBadBehaviorCheck(..)
  , sayCopilot
  , copilotLogMessageToSayWhat
  ) where

import Crux (SayLevel (..), SayWhat (..))
import qualified Crux.Log as Log
import Data.Aeson (ToJSON (..), Value (..))
import Data.Aeson.TH (defaultOptions, deriveToJSON)
import Data.Kind (Type)
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Vector as PV
import qualified Data.Parameterized.TraversableFC.WithIndex as PWI
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Vector as V
import GHC.Generics (Generic)
import qualified Prettyprinter as PP
import qualified Prettyprinter.Render.Text as PP

import qualified Copilot.Core.Expr as CE
import qualified Copilot.Core.Type as CT
import qualified Copilot.Theorem.What4 as CW4

import qualified Lang.Crucible.Simulator as LCS
import qualified Lang.Crucible.Types as LCT
import qualified Lang.Crucible.LLVM.Errors as LCLE
import qualified Lang.Crucible.LLVM.Errors.MemoryError as LCLEME
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as LCLEUB
import qualified Lang.Crucible.LLVM.MemModel as LCLM
import qualified Lang.Crucible.LLVM.MemModel.CallStack as LCLMCS
import qualified What4.FunctionName as WF
import qualified What4.Interface as WI
import qualified What4.ProgramLoc as WPL

data CopilotLogMessage where
  GeneratedCFile ::
       FilePath
       -- ^ The path of the generated C File
    -> CopilotLogMessage
  CompiledBitcodeFile ::
       String
       -- ^ The prefix to use in the compiled bitcode's directory
    -> FilePath
       -- ^ The name of the generated LLVM bitcode file
    -> CopilotLogMessage
  TranslatedToCrucible :: CopilotLogMessage
  GeneratingProofState :: CopilotLogMessage
  ComputingConditions :: VerificationStep -> CopilotLogMessage
  ProvingConditions :: VerificationStep -> CopilotLogMessage
  AllGoalsProved :: CopilotLogMessage
  OnlySomeGoalsProved ::
       Integer
       -- ^ Number of goals proved
    -> Integer
       -- ^ Number of total goals
    -> CopilotLogMessage
  SuccessfulProofSummary ::
       FilePath
       -- ^ Name of the generated C file.
    -> Integer
       -- ^ Number of goals proven during for the initial state of the proof.
    -> Integer
       -- ^ Number of goals proven during the bisimulation step of the proof.
    -> CopilotLogMessage
  NoisyVerbositySuggestion :: CopilotLogMessage

  -----
  -- Types of proof goals the verifier emits
  --
  -- The first three arguments to each constructor are:
  --
  -- * Which step of the verifier we are on
  -- * The current goal number (zero-indexed)
  -- * The total number of goals
  -----

  StreamValueEqualityProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> StreamValueEquality sym copilotType crucibleType
    -> CopilotLogMessage

  TriggersInvokedCorrespondinglyProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> TriggersInvokedCorrespondingly sym
    -> CopilotLogMessage

  TriggerArgumentEqualityProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> TriggerArgumentEquality sym copilotType crucibleType
    -> CopilotLogMessage

  RingBufferLoadProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> RingBufferLoad sym copilotType crucibleType
    -> CopilotLogMessage

  RingBufferIndexLoadProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> RingBufferIndexLoad sym
    -> CopilotLogMessage

  PointerArgumentLoadProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> PointerArgumentLoad sym copilotType crucibleType
    -> CopilotLogMessage

  AccessorFunctionLoadProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> AccessorFunctionLoad sym
    -> CopilotLogMessage

  GuardFunctionLoadProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> GuardFunctionLoad sym
    -> CopilotLogMessage

  UnknownFunctionLoadProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> UnknownFunctionLoad sym
    -> CopilotLogMessage

  LLVMBadBehaviorCheckProofGoal ::
       WI.IsSymExprBuilder sym
    => VerificationStep
    -> Integer
    -> Integer
    -> LLVMBadBehaviorCheck sym
    -> CopilotLogMessage

data VerificationStep
  = InitialState
  | StepBisimulation
  deriving stock (forall x. VerificationStep -> Rep VerificationStep x)
-> (forall x. Rep VerificationStep x -> VerificationStep)
-> Generic VerificationStep
forall x. Rep VerificationStep x -> VerificationStep
forall x. VerificationStep -> Rep VerificationStep x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. VerificationStep -> Rep VerificationStep x
from :: forall x. VerificationStep -> Rep VerificationStep x
$cto :: forall x. Rep VerificationStep x -> VerificationStep
to :: forall x. Rep VerificationStep x -> VerificationStep
Generic
  deriving anyclass [VerificationStep] -> Value
[VerificationStep] -> Encoding
VerificationStep -> Bool
VerificationStep -> Value
VerificationStep -> Encoding
(VerificationStep -> Value)
-> (VerificationStep -> Encoding)
-> ([VerificationStep] -> Value)
-> ([VerificationStep] -> Encoding)
-> (VerificationStep -> Bool)
-> ToJSON VerificationStep
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: VerificationStep -> Value
toJSON :: VerificationStep -> Value
$ctoEncoding :: VerificationStep -> Encoding
toEncoding :: VerificationStep -> Encoding
$ctoJSONList :: [VerificationStep] -> Value
toJSONList :: [VerificationStep] -> Value
$ctoEncodingList :: [VerificationStep] -> Encoding
toEncodingList :: [VerificationStep] -> Encoding
$comitField :: VerificationStep -> Bool
omitField :: VerificationStep -> Bool
ToJSON

-- | The provenance of an assertion.
data AssertionProvenance
  = VerifierProvenance
    -- ^ Assertions that the verifier directly makes to check the correspondence
    -- between the Copilot specification and the generated C code. Because these
    -- assertions are core to the proof that the verifier is computing, these
    -- assertions' proof goals are always logged, even if they are trivial.
  | StepExecutionProvenance
    -- ^ Assertions that arise during symbolic execution of the @step()@
    -- function as part of proving the memory safety of the generated C code.
    -- These assertions' proof goals are only logged if they are non-trivial,
    -- as there would be an excessive number of these proof goals otherwise.

-- | At what step of the proof are we checking the state relation? We record
-- this so that we can better distinguish between transition step–related
-- proof goals that arise before or after calling the @step()@ function.
data StateRelationStep
  = InitialStateRelation
    -- ^ Check the state relation for the initial state.
  | PreStepStateRelation
    -- ^ During the transition step of the proof, check the state relation
    -- before calling the @step()@ function.
  | PostStepStateRelation
    -- ^ During the transition step of the proof, check the state relation
    -- after calling the @step()@ function.
  deriving stock (forall x. StateRelationStep -> Rep StateRelationStep x)
-> (forall x. Rep StateRelationStep x -> StateRelationStep)
-> Generic StateRelationStep
forall x. Rep StateRelationStep x -> StateRelationStep
forall x. StateRelationStep -> Rep StateRelationStep x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. StateRelationStep -> Rep StateRelationStep x
from :: forall x. StateRelationStep -> Rep StateRelationStep x
$cto :: forall x. Rep StateRelationStep x -> StateRelationStep
to :: forall x. Rep StateRelationStep x -> StateRelationStep
Generic
  deriving anyclass [StateRelationStep] -> Value
[StateRelationStep] -> Encoding
StateRelationStep -> Bool
StateRelationStep -> Value
StateRelationStep -> Encoding
(StateRelationStep -> Value)
-> (StateRelationStep -> Encoding)
-> ([StateRelationStep] -> Value)
-> ([StateRelationStep] -> Encoding)
-> (StateRelationStep -> Bool)
-> ToJSON StateRelationStep
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: StateRelationStep -> Value
toJSON :: StateRelationStep -> Value
$ctoEncoding :: StateRelationStep -> Encoding
toEncoding :: StateRelationStep -> Encoding
$ctoJSONList :: [StateRelationStep] -> Value
toJSONList :: [StateRelationStep] -> Value
$ctoEncodingList :: [StateRelationStep] -> Encoding
toEncodingList :: [StateRelationStep] -> Encoding
$comitField :: StateRelationStep -> Bool
omitField :: StateRelationStep -> Bool
ToJSON

-- | Types of assertions that the verifier can make, which will count towards
-- the total number of proof goals.
data VerifierAssertion sym
  = StreamValueEqualityAssertion (SomeSome (StreamValueEquality sym))
  | TriggersInvokedCorrespondinglyAssertion (TriggersInvokedCorrespondingly sym)
  | TriggerArgumentEqualityAssertion (SomeSome (TriggerArgumentEquality sym))
  | RingBufferLoadAssertion (SomeSome (RingBufferLoad sym))
  | RingBufferIndexLoadAssertion (RingBufferIndexLoad sym)
  | PointerArgumentLoadAssertion (SomeSome (PointerArgumentLoad sym))
  | AccessorFunctionLoadAssertion (AccessorFunctionLoad sym)
  | GuardFunctionLoadAssertion (GuardFunctionLoad sym)
  | UnknownFunctionLoadAssertion (UnknownFunctionLoad sym)
  | LLVMBadBehaviorCheckAssertion (LLVMBadBehaviorCheck sym)

-- | Like @Some@ in @parameterized-utils@, but existentially closing over two
-- type parameters instead of just one.
data SomeSome (f :: j -> k -> Type) where
  SomeSome :: f x y -> SomeSome f

-- | An assertion that an element in a Copilot stream is equal to the
-- corresponding element in a C ring buffer.
data StreamValueEquality sym copilotType crucibleType where
  StreamValueEquality ::
       sym
    -> StateRelationStep
       -- ^ When the values are checked for equality
    -> WPL.ProgramLoc
       -- ^ The locations of the values
    -> Text
       -- ^ The name of the buffer
    -> Integer
       -- ^ The offset from the buffer's index, which is used to compute the
       -- element of the buffer to load
    -> Integer
       -- ^ The number of elements in the buffer
    -> CT.Type copilotType
       -- ^ The Copilot type
    -> CW4.XExpr sym
       -- ^ The Copilot value
    -> LCT.TypeRepr crucibleType
       -- ^ The Crucible type
    -> LCS.RegValue sym crucibleType
       -- ^ The Crucible value
    -> StreamValueEquality sym copilotType crucibleType

-- | An assertion that, given a Copilot trigger stream and its corresponding C
-- trigger function on a particular time step, either both fired at the same
-- time or both did not fire at all.
data TriggersInvokedCorrespondingly sym where
  TriggersInvokedCorrespondingly ::
       WPL.ProgramLoc
       -- ^ The location of the trigger
    -> CE.Name
       -- ^ The trigger name
    -> WI.SymNat sym
       -- ^ The expected number of times the trigger was fired this step
       -- (should be either 1 or 0).
    -> WI.SymNat sym
       -- ^ The actual number of times the trigger was fired this step.
    -> TriggersInvokedCorrespondingly sym

-- | An assertion that an argument to a Copilot trigger is equal to the
-- corresponding argument to a C trigger function.
data TriggerArgumentEquality sym copilotType crucibleType where
  TriggerArgumentEquality ::
       sym
    -> WPL.ProgramLoc
       -- ^ The locations of the arguments
    -> CE.Name
       -- ^ The trigger name
    -> Integer
       -- ^ The number of the argument (starting from 0)
    -> CT.Type copilotType
       -- ^ The Copilot type
    -> CW4.XExpr sym
       -- ^ The Copilot value
    -> LCT.TypeRepr crucibleType
       -- ^ The Crucible type
    -> LCS.RegValue sym crucibleType
       -- ^ The Crucible value
    -> TriggerArgumentEquality sym copilotType crucibleType

-- | An assertion that a load from a ring buffer in C is valid.
data RingBufferLoad sym copilotType crucibleType where
  RingBufferLoad ::
       sym
    -> StateRelationStep
       -- ^ When the ring buffer is loaded from
    -> WPL.ProgramLoc
       -- ^ The location of the buffer
    -> Text
       -- ^ The name of the buffer
    -> Integer
       -- ^ The offset from the buffer's index, which is used to compute the
       -- element of the buffer to load
    -> Integer
       -- ^ The number of elements in the buffer
    -> CT.Type copilotType
       -- ^ The Copilot type of the elements of the array
    -> LCT.TypeRepr crucibleType
       -- ^ The Crucible type of the elements of the array
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this load to be valid
    -> RingBufferLoad sym copilotType crucibleType

-- | An assertion that a load from a global variable representing a ring
-- buffer's index in C is valid.
data RingBufferIndexLoad sym where
  RingBufferIndexLoad ::
       sym
    -> StateRelationStep
       -- ^ When the index's global variable is loaded from
    -> WPL.ProgramLoc
       -- ^ The location of the global index
    -> Text
       -- ^ The name of the global index
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this load to be valid
    -> RingBufferIndexLoad sym

-- | An assertion that a load from a pointer argument to a trigger function in C
-- is valid.
data PointerArgumentLoad sym copilotType crucibleType where
  PointerArgumentLoad ::
       sym
    -> WPL.ProgramLoc
       -- ^ The location of the pointer
    -> CT.Type copilotType
       -- ^ The Copilot type of the underlying memory
    -> LCT.TypeRepr crucibleType
       -- ^ The Crucible type of the underlying memory
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this load to be valid
    -> PointerArgumentLoad sym copilotType crucibleType

-- | An assertion that a load occurring from somewhere in a stream accessor
-- function in C (e.g., @s0_get@) is valid. This is a somewhat imprecise
-- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it
-- happens because of an array index.)
data AccessorFunctionLoad sym where
  AccessorFunctionLoad ::
       sym
    -> WPL.ProgramLoc
       -- ^ The location of the accessor function
    -> WF.FunctionName
       -- ^ The name of the accessor function
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this load to be valid
    -> AccessorFunctionLoad sym

-- | An assertion that a load occurring from somewhere in a trigger guard
-- function in C (e.g., @even_guard@) is valid. This is a somewhat imprecise
-- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it
-- happens because of an array index.)
data GuardFunctionLoad sym where
  GuardFunctionLoad ::
       sym
    -> WPL.ProgramLoc
       -- ^ The location of the guard function
    -> WF.FunctionName
       -- ^ The name of the guard function
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this load to be valid
    -> GuardFunctionLoad sym

-- | An assertion that a load occurring in some function is valid. If you
-- see this assertion, it is because the heuristics used to identify where
-- load-related assertions come from could not identify a more precise cause
-- for a load.
data UnknownFunctionLoad sym where
  UnknownFunctionLoad ::
       sym
    -> WPL.ProgramLoc
       -- ^ The location of the function
    -> WF.FunctionName
       -- ^ The name of the function
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this load to be valid
    -> UnknownFunctionLoad sym

-- | An assertion that checks that some form of bad behavior in LLVM does not
-- occur. Bad behavior includes both undefined behavior and memory unsafety.
data LLVMBadBehaviorCheck sym where
  LLVMBadBehaviorCheck ::
       sym
    -> WPL.ProgramLoc
       -- ^ The location of the check
    -> LCLMCS.CallStack
       -- ^ A call stack for the check, if one exists
    -> LCLE.BadBehavior sym
       -- ^ What type of LLVM bad behavior is being checked for
    -> WI.Pred sym
       -- ^ The assertion that must hold in order for this check to succeed
    -> LLVMBadBehaviorCheck sym

-- Silly ToJSON instances. Crux is only requiring a ToJSON constraint for
-- IDE-related functionality that we do not make use of, so the behavior of
-- these instances aren't very important.

instance ToJSON (StreamValueEquality sym copilotType crucibleType) where
  toJSON :: StreamValueEquality sym copilotType crucibleType -> Value
toJSON StreamValueEquality sym copilotType crucibleType
_ = Text -> Value
String Text
"StreamValueEquality"

instance ToJSON (TriggersInvokedCorrespondingly sym) where
  toJSON :: TriggersInvokedCorrespondingly sym -> Value
toJSON TriggersInvokedCorrespondingly sym
_ = Text -> Value
String Text
"TriggersInvokedCorrespondingly"

instance ToJSON (TriggerArgumentEquality sym copilotType crucibleType) where
  toJSON :: TriggerArgumentEquality sym copilotType crucibleType -> Value
toJSON TriggerArgumentEquality sym copilotType crucibleType
_ = Text -> Value
String Text
"TriggerArgumentEquality"

instance ToJSON (RingBufferLoad sym copilotType crucibleType) where
  toJSON :: RingBufferLoad sym copilotType crucibleType -> Value
toJSON RingBufferLoad sym copilotType crucibleType
_ = Text -> Value
String Text
"RingBufferLoad"

instance ToJSON (RingBufferIndexLoad sym) where
  toJSON :: RingBufferIndexLoad sym -> Value
toJSON RingBufferIndexLoad sym
_ = Text -> Value
String Text
"RingBufferIndexLoad"

instance ToJSON (PointerArgumentLoad sym copilotType crucibleType) where
  toJSON :: PointerArgumentLoad sym copilotType crucibleType -> Value
toJSON PointerArgumentLoad sym copilotType crucibleType
_ = Text -> Value
String Text
"PointerArgumentLoad"

instance ToJSON (AccessorFunctionLoad sym) where
  toJSON :: AccessorFunctionLoad sym -> Value
toJSON AccessorFunctionLoad sym
_ = Text -> Value
String Text
"AccessorFunctionLoad"

instance ToJSON (GuardFunctionLoad sym) where
  toJSON :: GuardFunctionLoad sym -> Value
toJSON GuardFunctionLoad sym
_ = Text -> Value
String Text
"GuardFunctionLoad"

instance ToJSON (UnknownFunctionLoad sym) where
  toJSON :: UnknownFunctionLoad sym -> Value
toJSON UnknownFunctionLoad sym
_ = Text -> Value
String Text
"UnknownFunctionLoad"

instance ToJSON (LLVMBadBehaviorCheck sym) where
  toJSON :: LLVMBadBehaviorCheck sym -> Value
toJSON LLVMBadBehaviorCheck sym
_ = Text -> Value
String Text
"LLVMBadBehaviorCheck"

type SupportsCopilotLogMessage msgs =
  (?injectCopilotLogMessage :: CopilotLogMessage -> msgs)

sayCopilot ::
  Log.Logs msgs =>
  SupportsCopilotLogMessage msgs =>
  CopilotLogMessage ->
  IO ()
sayCopilot :: forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
sayCopilot CopilotLogMessage
msg =
  let ?injectMessage = SupportsCopilotLogMessage msgs
?injectMessage::CopilotLogMessage -> msgs
CopilotLogMessage -> msgs
?injectCopilotLogMessage
   in CopilotLogMessage -> IO ()
forall msgs msg.
(Logs msgs, ?injectMessage::msg -> msgs) =>
msg -> IO ()
Log.say CopilotLogMessage
msg

copilotTag :: Text
copilotTag :: Text
copilotTag = Text
"copilot-verifier"

-- copilotFail :: Text -> SayWhat
-- copilotFail = SayWhat Fail copilotTag

copilotSimply :: Text -> SayWhat
copilotSimply :: Text -> SayWhat
copilotSimply = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
copilotTag

copilotNoisily :: Text -> SayWhat
copilotNoisily :: Text -> SayWhat
copilotNoisily = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Noisily Text
copilotTag

-- copilotWarn :: Text -> SayWhat
-- copilotWarn = SayWhat Warn copilotTag

copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat
copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat
copilotLogMessageToSayWhat (GeneratedCFile FilePath
csrc) =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ Text
"Generated " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
csrc)
copilotLogMessageToSayWhat (CompiledBitcodeFile FilePath
prefix FilePath
bcFile) =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ Text
"Compiled " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack FilePath
prefix Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" into " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack FilePath
bcFile
copilotLogMessageToSayWhat CopilotLogMessage
TranslatedToCrucible =
  Text -> SayWhat
copilotSimply Text
"Translated bitcode into Crucible"
copilotLogMessageToSayWhat CopilotLogMessage
GeneratingProofState =
  Text -> SayWhat
copilotSimply Text
"Generating proof state data"
copilotLogMessageToSayWhat (ComputingConditions VerificationStep
step) =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ Text
"Computing " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> VerificationStep -> Text
describeVerificationStep VerificationStep
step Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" verification conditions"
copilotLogMessageToSayWhat (ProvingConditions VerificationStep
step) =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ Text
"Proving " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> VerificationStep -> Text
describeVerificationStep VerificationStep
step Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" verification conditions"
copilotLogMessageToSayWhat CopilotLogMessage
AllGoalsProved =
  Text -> SayWhat
copilotSimply Text
"All obligations proved by concrete simplification"
copilotLogMessageToSayWhat (OnlySomeGoalsProved Integer
numProvedGoals Integer
numTotalGoals) =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unwords
    [ Text
"Proved", FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
numProvedGoals)
    , Text
"of"
    , FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
numTotalGoals), Text
"total goals"
    ]
copilotLogMessageToSayWhat (SuccessfulProofSummary FilePath
cFileName Integer
initGoals Integer
bisimGoals) =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
    [ Text
""
    , Text
"copilot-verifier has produced a mathematical proof that the behavior of"
    , Text
"the generated C program (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack FilePath
cFileName
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") precisely matches the behavior of"
    , Text
"the Copilot specification. This proof shows that the behaviors match for"
    , Text
"all possible moments in time, and in doing so, copilot-verifier examined"
    , Text
"how the programs behave at the start of execution (the \"initial state\")"
    , Text
"and at an arbitrary point of time in execution (the \"step bisimulation\")."
    , Text
"copilot-verifier decomposed the overall proof into smaller goals, the"
    , Text
"number of which depends on the size and complexity of the program. In this"
    , Text
"example, there are " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
initGoals) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" initial state goal(s)"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" and " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
bisimGoals) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" step bisimulation goal(s),"
    , Text
"and copilot-verifier was able to prove all of them."
    ]
copilotLogMessageToSayWhat CopilotLogMessage
NoisyVerbositySuggestion =
  Text -> SayWhat
copilotSimply (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
    [ Text
""
    , Text
"copilot-verifier is displaying an abridged summary of the verification results."
    , Text
"copilot-verifier also includes a \"noisy\" mode that prints detailed"
    , Text
"descriptions of each individual proof goal, including what type of goal it is,"
    , Text
"why it needs to be proven, and where in the Copilot specification and/or C code"
    , Text
"the proof goal originated from. To enable noisy mode, invoke the verifier with"
    , Text
"the following options:"
    , Text
""
    , Text
"```"
    , Text
"verifyWithOptions (defaultVerifierOptions { verbosity = Noisy }) ..."
    , Text
"```"
    ]
copilotLogMessageToSayWhat
    (StreamValueEqualityProofGoal VerificationStep
verifStep Integer
goalIdx Integer
numTotalGoals
      (StreamValueEquality
        sym
sym StateRelationStep
stateRelStep ProgramLoc
loc
        Text
bufName Integer
offset Integer
len
        Type copilotType
copilotTy XExpr sym
copilotVal
        TypeRepr crucibleType
crucibleTy RegValue sym crucibleType
crucibleVal)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> StateRelationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayStateRelationProofGoal
    VerificationStep
verifStep StateRelationStep
stateRelStep AssertionProvenance
VerifierProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the equality between two stream values"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Ring buffer name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
bufName
    , Text
"* Offset into buffer (from current index): " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
offset)
    , Text
"* Number of elements in buffer: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
len)
    , Text
"* Copilot type: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Int -> Type copilotType -> FilePath -> FilePath
forall tp. Int -> Type tp -> FilePath -> FilePath
showsCopilotType Int
0 Type copilotType
copilotTy FilePath
"")
    , Text
"* Copilot value:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ XExpr sym -> Doc Any
forall sym a. IsSymExprBuilder sym => XExpr sym -> Doc a
ppCopilotValue XExpr sym
copilotVal
    , Text
"* Crucible value:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ sym
-> TypeRepr crucibleType -> RegValue sym crucibleType -> Doc Any
forall sym (tp :: CrucibleType) a.
IsSymExprBuilder sym =>
sym -> TypeRepr tp -> RegValue sym tp -> Doc a
ppCrucibleValue sym
sym TypeRepr crucibleType
crucibleTy RegValue sym crucibleType
crucibleVal
    ]
copilotLogMessageToSayWhat
    (TriggersInvokedCorrespondinglyProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (TriggersInvokedCorrespondingly ProgramLoc
loc FilePath
name SymNat sym
expected SymNat sym
actual)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
    VerificationStep
step AssertionProvenance
VerifierProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting triggers fired in corresponding ways"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Trigger name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack FilePath
name
    , Text
"* Expected number of times trigger was fired:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ SymNat sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => SymNat sym -> Doc ann
WI.printSymNat SymNat sym
expected
    , Text
"* Actual number of times trigger was fired:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ SymNat sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => SymNat sym -> Doc ann
WI.printSymNat SymNat sym
actual
    ]
copilotLogMessageToSayWhat
    (TriggerArgumentEqualityProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (TriggerArgumentEquality
        sym
sym ProgramLoc
loc
        FilePath
triggerName Integer
argNum
        Type copilotType
copilotTy XExpr sym
copilotVal
        TypeRepr crucibleType
crucibleTy RegValue sym crucibleType
crucibleVal)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
    VerificationStep
step AssertionProvenance
VerifierProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the equality between two trigger arguments"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Trigger name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack FilePath
triggerName
    , Text
"* Number of argument: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
argNum)
    , Text
"* Copilot type: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Int -> Type copilotType -> FilePath -> FilePath
forall tp. Int -> Type tp -> FilePath -> FilePath
showsCopilotType Int
0 Type copilotType
copilotTy FilePath
"")
    , Text
"* Copilot value:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ XExpr sym -> Doc Any
forall sym a. IsSymExprBuilder sym => XExpr sym -> Doc a
ppCopilotValue XExpr sym
copilotVal
    , Text
"* Crucible value:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ sym
-> TypeRepr crucibleType -> RegValue sym crucibleType -> Doc Any
forall sym (tp :: CrucibleType) a.
IsSymExprBuilder sym =>
sym -> TypeRepr tp -> RegValue sym tp -> Doc a
ppCrucibleValue sym
sym TypeRepr crucibleType
crucibleTy RegValue sym crucibleType
crucibleVal
    ]
copilotLogMessageToSayWhat
    (RingBufferLoadProofGoal VerificationStep
verifStep Integer
goalIdx Integer
numTotalGoals
      (RingBufferLoad
        sym
_sym StateRelationStep
stateRelStep ProgramLoc
loc Text
bufName Integer
offset Integer
len Type copilotType
copilotTy TypeRepr crucibleType
_crucibleTy Pred sym
p)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> StateRelationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayStateRelationProofGoal
    VerificationStep
verifStep StateRelationStep
stateRelStep AssertionProvenance
VerifierProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the validity of a memory load from a stream's ring buffer in C"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Ring buffer name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
bufName
    , Text
"* Offset into buffer (from current index): " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
offset)
    , Text
"* Number of elements in buffer: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
len)
    , Text
"* Copilot type of buffer elements:" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Int -> Type copilotType -> FilePath -> FilePath
forall tp. Int -> Type tp -> FilePath -> FilePath
showsCopilotType Int
0 Type copilotType
copilotTy FilePath
"")
    , Text
"* Validity predicate:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
    ]
copilotLogMessageToSayWhat
    (RingBufferIndexLoadProofGoal VerificationStep
verifStep Integer
goalIdx Integer
numTotalGoals
      (RingBufferIndexLoad sym
_sym StateRelationStep
stateRelStep ProgramLoc
loc Text
idxName Pred sym
p)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> StateRelationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayStateRelationProofGoal
    VerificationStep
verifStep StateRelationStep
stateRelStep AssertionProvenance
VerifierProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the validity of a memory load from the index to a stream's ring buffer in C"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Ring buffer index name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
idxName
    , Text
"* Validity predicate:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
    ]
copilotLogMessageToSayWhat
    (PointerArgumentLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (PointerArgumentLoad
        sym
_sym ProgramLoc
loc Type copilotType
copilotTy TypeRepr crucibleType
_crucibleTy Pred sym
p)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
    VerificationStep
step AssertionProvenance
VerifierProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the validity of a memory load from a pointer argument to a trigger"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Copilot type: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Int -> Type copilotType -> FilePath -> FilePath
forall tp. Int -> Type tp -> FilePath -> FilePath
showsCopilotType Int
0 Type copilotType
copilotTy FilePath
"")
    , Text
"* Validity predicate:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
    ]
copilotLogMessageToSayWhat
    (AccessorFunctionLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (AccessorFunctionLoad sym
_sym ProgramLoc
loc FunctionName
accessorName Pred sym
p)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
    VerificationStep
step AssertionProvenance
StepExecutionProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the validity of a memory load from a stream accessor function"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Accessor function name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FunctionName -> Text
WF.functionName FunctionName
accessorName
    , Text
"* Validity predicate:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
    ]
copilotLogMessageToSayWhat
    (GuardFunctionLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (GuardFunctionLoad sym
_sym ProgramLoc
loc FunctionName
accessorName Pred sym
p)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
  VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
    VerificationStep
step AssertionProvenance
StepExecutionProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the validity of a memory load from a trigger guard function"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Guard function name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FunctionName -> Text
WF.functionName FunctionName
accessorName
    , Text
"* Validity predicate:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
    ]
copilotLogMessageToSayWhat
    (UnknownFunctionLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (UnknownFunctionLoad sym
_sym ProgramLoc
loc FunctionName
accessorName Pred sym
p)) =
  Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
    VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
    VerificationStep
step AssertionProvenance
StepExecutionProvenance Integer
goalIdx Integer
numTotalGoals
    Text
"asserting the validity of a memory load from an unknown function"
    [ Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
    , Text
"* Function name: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FunctionName -> Text
WF.functionName FunctionName
accessorName
    , Text
"* Validity predicate:"
    , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
    ]
copilotLogMessageToSayWhat
    (LLVMBadBehaviorCheckProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals
      (LLVMBadBehaviorCheck sym
_sym ProgramLoc
loc CallStack
stk BadBehavior sym
bb Pred sym
p)) =
  let ppLoc :: Text
ppLoc = Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> Doc Any
forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
loc
      ppCallStackLines :: [Text]
ppCallStackLines =
        [ Text
"* Call stack:"
        , Text
"    " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> CallStack -> Text
renderCallStack CallStack
stk
        ]
      ppValidPredLines :: [Text]
ppValidPredLines =
        [ Text
"* Validity predicate:"
        , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ Pred sym -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr Pred sym
p
        ] in
  case BadBehavior sym
bb of
    LCLE.BBUndefinedBehavior UndefinedBehavior (RegValue' sym)
ub ->
      Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
      VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
        VerificationStep
step AssertionProvenance
StepExecutionProvenance Integer
goalIdx Integer
numTotalGoals
        Text
"asserting that LLVM undefined behavior does not occur"
        ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text
ppLoc Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
ppCallStackLines [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++
        [ Text
"* Undefined behavior description:"
        , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ UndefinedBehavior (RegValue' sym) -> Doc Any
forall sym ann.
IsExpr (SymExpr sym) =>
UndefinedBehavior (RegValue' sym) -> Doc ann
LCLEUB.ppDetails UndefinedBehavior (RegValue' sym)
ub
        ] [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
ppValidPredLines
    LCLE.BBMemoryError MemoryError sym
me ->
      Text -> SayWhat
copilotNoisily (Text -> SayWhat) -> Text -> SayWhat
forall a b. (a -> b) -> a -> b
$
      VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal
        VerificationStep
step AssertionProvenance
StepExecutionProvenance Integer
goalIdx Integer
numTotalGoals
        Text
"asserting that LLVM memory unsafety does not occur"
        ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text
ppLoc Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
ppCallStackLines [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++
        [ Text
"* Memory unsafety description:"
        , Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Doc Any -> Doc Any
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
4 (Doc Any -> Doc Any) -> Doc Any -> Doc Any
forall a b. (a -> b) -> a -> b
$ MemoryError sym -> Doc Any
forall sym ann. IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
LCLEME.explain MemoryError sym
me
        ] [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
ppValidPredLines

describeVerificationStep :: VerificationStep -> Text
describeVerificationStep :: VerificationStep -> Text
describeVerificationStep VerificationStep
InitialState     = Text
"initial state"
describeVerificationStep VerificationStep
StepBisimulation = Text
"step bisimulation"

-- | Display information about an emitted proof goal.
displayProofGoal ::
     VerificationStep
  -> AssertionProvenance
  -> Integer
  -> Integer
  -> Text
  -> [Text]
  -> Text
displayProofGoal :: VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal VerificationStep
step AssertionProvenance
assertProv Integer
goalIdx Integer
numTotalGoals Text
why [Text]
ls = [Text] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$
  [ Text
banner
  , Text
"Emitted a proof goal (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
why Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
  , Text
"  During the " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
displayStep
  , Text
"  Required for proving the " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
displayAssertProv
  , Text
"  Proof goal " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
goalIdx)
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ("
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
T.pack (Integer -> FilePath
forall a. Show a => a -> FilePath
show Integer
numTotalGoals)
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" total)"
  , Text
""
  ]
  [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text]
ls [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [Text
banner]
  where
    banner :: Text
banner = Text
"====="
    displayStep :: Text
displayStep =
      case VerificationStep
step of
        VerificationStep
InitialState ->
          Text
"initial bisimulation state step"
        VerificationStep
StepBisimulation ->
          Text
"transition step of bisimulation"
    displayAssertProv :: Text
displayAssertProv =
      case AssertionProvenance
assertProv of
        AssertionProvenance
VerifierProvenance ->
          Text
"correspondence between the spec and C code"
        AssertionProvenance
StepExecutionProvenance ->
          Text
"memory safety of the generated step() function"

-- | Display information about an emitted proof goal that involves checking the
-- state relation.
displayStateRelationProofGoal ::
     VerificationStep
  -> StateRelationStep
  -> AssertionProvenance
  -> Integer
  -> Integer
  -> Text
  -> [Text]
  -> Text
displayStateRelationProofGoal :: VerificationStep
-> StateRelationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayStateRelationProofGoal VerificationStep
verifStep StateRelationStep
stateRelStep AssertionProvenance
assertProv Integer
goalIdx Integer
numTotalGoals Text
why =
    VerificationStep
-> AssertionProvenance
-> Integer
-> Integer
-> Text
-> [Text]
-> Text
displayProofGoal VerificationStep
verifStep AssertionProvenance
assertProv Integer
goalIdx Integer
numTotalGoals Text
why'
  where
    why' :: Text
    why' :: Text
why' =
      case StateRelationStep
stateRelStep of
        StateRelationStep
PreStepStateRelation  -> Text
why Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" before calling step()"
        StateRelationStep
PostStepStateRelation -> Text
why Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" after calling step()"
        -- `displayProofGoal` already makes a note of the fact that we're
        -- checking the initial state, so no need to do so again here.
        StateRelationStep
InitialStateRelation -> Text
why

ppProgramLoc :: WPL.ProgramLoc -> PP.Doc a
ppProgramLoc :: forall a. ProgramLoc -> Doc a
ppProgramLoc ProgramLoc
pl = [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
PP.vcat
  [ Doc a
"* Function:" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc a
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty (ProgramLoc -> FunctionName
WPL.plFunction ProgramLoc
pl)
  , Doc a
"  Position:" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc a
forall ann. Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (ProgramLoc -> Position
WPL.plSourceLoc ProgramLoc
pl)
  ]

renderCallStack :: LCLMCS.CallStack -> Text
renderCallStack :: CallStack -> Text
renderCallStack CallStack
cs
  | Text -> Bool
T.null Text
ppText
  = Text
"<no call stack available>"
  | Bool
otherwise
  = Text
ppText
  where
    ppText :: Text
ppText = Doc Any -> Text
forall a. Doc a -> Text
renderStrict (Doc Any -> Text) -> Doc Any -> Text
forall a b. (a -> b) -> a -> b
$ CallStack -> Doc Any
forall ann. CallStack -> Doc ann
LCLMCS.ppCallStack CallStack
cs

showsCopilotType :: Int -> CT.Type tp -> ShowS
showsCopilotType :: forall tp. Int -> Type tp -> FilePath -> FilePath
showsCopilotType Int
prec Type tp
tp =
  case Type tp
tp of
    Type tp
CT.Bool     -> FilePath -> FilePath -> FilePath
showString FilePath
"Bool"
    Type tp
CT.Int8     -> FilePath -> FilePath -> FilePath
showString FilePath
"Int8"
    Type tp
CT.Int16    -> FilePath -> FilePath -> FilePath
showString FilePath
"Int16"
    Type tp
CT.Int32    -> FilePath -> FilePath -> FilePath
showString FilePath
"Int32"
    Type tp
CT.Int64    -> FilePath -> FilePath -> FilePath
showString FilePath
"Int64"
    Type tp
CT.Word8    -> FilePath -> FilePath -> FilePath
showString FilePath
"Word8"
    Type tp
CT.Word16   -> FilePath -> FilePath -> FilePath
showString FilePath
"Word16"
    Type tp
CT.Word32   -> FilePath -> FilePath -> FilePath
showString FilePath
"Word32"
    Type tp
CT.Word64   -> FilePath -> FilePath -> FilePath
showString FilePath
"Word64"
    Type tp
CT.Float    -> FilePath -> FilePath -> FilePath
showString FilePath
"Float"
    Type tp
CT.Double   -> FilePath -> FilePath -> FilePath
showString FilePath
"Double"
    CT.Array Type t
t  -> Bool -> (FilePath -> FilePath) -> FilePath -> FilePath
showParen (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) ((FilePath -> FilePath) -> FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$
                     FilePath -> FilePath -> FilePath
showString FilePath
"Array" (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                     Int -> Int -> FilePath -> FilePath
forall a. Show a => Int -> a -> FilePath -> FilePath
showsPrec Int
11 (Type (Array n t) -> Int
forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
CT.typeSize Type tp
Type (Array n t)
tp) (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                     Int -> Type t -> FilePath -> FilePath
forall tp. Int -> Type tp -> FilePath -> FilePath
showsCopilotType Int
11 Type t
t
    CT.Struct tp
x -> FilePath -> FilePath -> FilePath
showString (FilePath -> FilePath -> FilePath)
-> FilePath -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ tp -> FilePath
forall a. Struct a => a -> FilePath
CT.typeName tp
x

ppCopilotValue :: WI.IsSymExprBuilder sym => CW4.XExpr sym -> PP.Doc a
ppCopilotValue :: forall sym a. IsSymExprBuilder sym => XExpr sym -> Doc a
ppCopilotValue XExpr sym
val =
  case XExpr sym
val of
    CW4.XBool   SymExpr sym BaseBoolType
b -> SymExpr sym BaseBoolType -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym BaseBoolType
b
    CW4.XInt8   SymExpr sym (BaseBVType 8)
i -> SymExpr sym (BaseBVType 8) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 8)
i
    CW4.XInt16  SymExpr sym (BaseBVType 16)
i -> SymExpr sym (BaseBVType 16) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 16)
i
    CW4.XInt32  SymExpr sym (BaseBVType 32)
i -> SymExpr sym (BaseBVType 32) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 32)
i
    CW4.XInt64  SymExpr sym (BaseBVType 64)
i -> SymExpr sym (BaseBVType 64) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 64)
i
    CW4.XWord8  SymExpr sym (BaseBVType 8)
w -> SymExpr sym (BaseBVType 8) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 8)
w
    CW4.XWord16 SymExpr sym (BaseBVType 16)
w -> SymExpr sym (BaseBVType 16) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 16)
w
    CW4.XWord32 SymExpr sym (BaseBVType 32)
w -> SymExpr sym (BaseBVType 32) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 32)
w
    CW4.XWord64 SymExpr sym (BaseBVType 64)
w -> SymExpr sym (BaseBVType 64) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (BaseBVType 64)
w
    CW4.XFloat  SymExpr sym (SymInterpretedFloatType sym SingleFloat)
f -> SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
f
    CW4.XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
d -> SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
d
    CW4.XEmptyArray {} -> Doc a
"[]"
    CW4.XArray  Vector n (XExpr sym)
a   -> (XExpr sym -> Doc a) -> [XExpr sym] -> Doc a
forall a b. (a -> Doc b) -> [a] -> Doc b
ppBracesWith XExpr sym -> Doc a
forall sym a. IsSymExprBuilder sym => XExpr sym -> Doc a
ppCopilotValue (Vector n (XExpr sym) -> [XExpr sym]
forall (n :: Nat) a. Vector n a -> [a]
PV.toList Vector n (XExpr sym)
a)
    CW4.XStruct [XExpr sym]
s   -> (XExpr sym -> Doc a) -> [XExpr sym] -> Doc a
forall a b. (a -> Doc b) -> [a] -> Doc b
ppBracketsWith XExpr sym -> Doc a
forall sym a. IsSymExprBuilder sym => XExpr sym -> Doc a
ppCopilotValue [XExpr sym]
s

ppCrucibleValue :: WI.IsSymExprBuilder sym
                => sym
                -> LCT.TypeRepr tp
                -> LCS.RegValue sym tp
                -> PP.Doc a
ppCrucibleValue :: forall sym (tp :: CrucibleType) a.
IsSymExprBuilder sym =>
sym -> TypeRepr tp -> RegValue sym tp -> Doc a
ppCrucibleValue sym
sym TypeRepr tp
tp RegValue sym tp
val =
  case TypeRepr tp
tp of
    LCLM.LLVMPointerRepr NatRepr w
_ -> LLVMPtr sym w -> Doc a
forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
LCLM.ppPtr RegValue sym tp
LLVMPtr sym w
val
    LCT.FloatRepr FloatInfoRepr flt
_        -> SymExpr sym (SymInterpretedFloatType sym flt) -> Doc a
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
WI.printSymExpr RegValue sym tp
SymExpr sym (SymInterpretedFloatType sym flt)
val
    LCT.VectorRepr TypeRepr tp1
tpr     -> (RegValue sym tp1 -> Doc a) -> [RegValue sym tp1] -> Doc a
forall a b. (a -> Doc b) -> [a] -> Doc b
ppBracketsWith (sym -> TypeRepr tp1 -> RegValue sym tp1 -> Doc a
forall sym (tp :: CrucibleType) a.
IsSymExprBuilder sym =>
sym -> TypeRepr tp -> RegValue sym tp -> Doc a
ppCrucibleValue sym
sym TypeRepr tp1
tpr) (Vector (RegValue sym tp1) -> [RegValue sym tp1]
forall a. Vector a -> [a]
V.toList Vector (RegValue sym tp1)
RegValue sym tp
val)
    LCT.StructRepr CtxRepr ctx
ctx     -> [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
withBraces ([Doc a] -> Doc a) -> [Doc a] -> Doc a
forall a b. (a -> b) -> a -> b
$
                              (forall (x :: CrucibleType).
 IndexF (Assignment (RegValue' sym) ctx) x
 -> RegValue' sym x -> Doc a)
-> Assignment (RegValue' sym) ctx -> [Doc a]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a (z :: l).
FoldableFCWithIndex t =>
(forall (x :: k). IndexF (t f z) x -> f x -> a) -> t f z -> [a]
forall (f :: CrucibleType -> *) a (z :: Ctx CrucibleType).
(forall (x :: CrucibleType). IndexF (Assignment f z) x -> f x -> a)
-> Assignment f z -> [a]
PWI.itoListFC (\IndexF (Assignment (RegValue' sym) ctx) x
i (LCS.RV RegValue sym x
v) -> sym -> TypeRepr x -> RegValue sym x -> Doc a
forall sym (tp :: CrucibleType) a.
IsSymExprBuilder sym =>
sym -> TypeRepr tp -> RegValue sym tp -> Doc a
ppCrucibleValue sym
sym (CtxRepr ctx
ctx CtxRepr ctx -> Index ctx x -> TypeRepr x
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! IndexF (Assignment (RegValue' sym) ctx) x
Index ctx x
i) RegValue sym x
v) RegValue sym tp
Assignment (RegValue' sym) ctx
val
    TypeRepr tp
_ -> FilePath -> Doc a
forall a. HasCallStack => FilePath -> a
error (FilePath -> Doc a) -> FilePath -> Doc a
forall a b. (a -> b) -> a -> b
$ FilePath
"ppCrucibleValue: Unsupported type: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ TypeRepr tp -> FilePath
forall a. Show a => a -> FilePath
show TypeRepr tp
tp

renderStrict :: PP.Doc a ->  Text
renderStrict :: forall a. Doc a -> Text
renderStrict = SimpleDocStream a -> Text
forall ann. SimpleDocStream ann -> Text
PP.renderStrict (SimpleDocStream a -> Text)
-> (Doc a -> SimpleDocStream a) -> Doc a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc a -> SimpleDocStream a
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
PP.layoutPretty LayoutOptions
PP.defaultLayoutOptions

ppBracketsWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b
ppBracketsWith :: forall a b. (a -> Doc b) -> [a] -> Doc b
ppBracketsWith a -> Doc b
f = Doc b -> Doc b
forall ann. Doc ann -> Doc ann
PP.align (Doc b -> Doc b) -> ([a] -> Doc b) -> [a] -> Doc b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc b] -> Doc b
forall ann. [Doc ann] -> Doc ann
PP.list ([Doc b] -> Doc b) -> ([a] -> [Doc b]) -> [a] -> Doc b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc b) -> [a] -> [Doc b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc b
f

ppBracesWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b
ppBracesWith :: forall a b. (a -> Doc b) -> [a] -> Doc b
ppBracesWith a -> Doc b
f = [Doc b] -> Doc b
forall ann. [Doc ann] -> Doc ann
withBraces ([Doc b] -> Doc b) -> ([a] -> [Doc b]) -> [a] -> Doc b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc b) -> [a] -> [Doc b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc b
f

withBraces :: [PP.Doc a] -> PP.Doc a
withBraces :: forall ann. [Doc ann] -> Doc ann
withBraces =
    Doc a -> Doc a
forall ann. Doc ann -> Doc ann
PP.align
  (Doc a -> Doc a) -> ([Doc a] -> Doc a) -> [Doc a] -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc a -> Doc a -> Doc a -> [Doc a] -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
PP.encloseSep (Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
PP.flatAlt Doc a
"{ " Doc a
"{") (Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
PP.flatAlt Doc a
" }" Doc a
"}") Doc a
", "

$(deriveToJSON defaultOptions ''CopilotLogMessage)