{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Copilot.Verifier
  ( verify
  , verifyWithOptions
  , VerifierOptions(..)
  , defaultVerifierOptions
  , sideCondVerifierOptions
  , Verbosity(..)
  ) where

import Control.Lens (view, (^.), to)
import Control.Monad (foldM, forM_, unless, when)
import Control.Monad.IO.Class (liftIO)
import Control.Monad.State (execStateT, lift, StateT(..))
import Data.Aeson (ToJSON)
import Data.Foldable (traverse_)
import Data.Functor (void)
import qualified Data.Text as Text
import qualified Data.Map.Strict as Map
import Data.IORef (newIORef, modifyIORef', readIORef, IORef)
import qualified Text.LLVM.AST as L
import Data.List (genericLength, sort)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NE
import qualified Data.Vector as V
import qualified Data.BitVector.Sized as BV
import GHC.Generics (Generic)
import qualified Prettyprinter as PP
import System.Exit (exitFailure)
import System.FilePath ((</>), (<.>))

import Copilot.Compile.C99 (CSettings(..), compileWith)
import Copilot.Core
import qualified Copilot.Core.Type as CT

import qualified Copilot.Theorem.What4 as CW4

import qualified Copilot.Verifier.FloatMode as FloatMode
import qualified Copilot.Verifier.Log as Log
import qualified Copilot.Verifier.Solver as Solver

import Data.Parameterized.Ctx (EmptyCtx)
import Data.Parameterized.Context (pattern Empty)
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr (intValue, natValue, testEquality, knownNat, type (<=) )
import Data.Parameterized.Nonce (globalNonceGenerator)
import Data.Parameterized.Some (Some(..))
import Data.Parameterized.TraversableFC (toListFC)
import Data.Parameterized.TraversableFC.WithIndex (ifoldlMFC)
import qualified Data.Parameterized.Vector as PVec

import Lang.Crucible.Backend
  ( IsSymInterface, Goals(..), Assumptions, Assertion
  , pushAssumptionFrame, popUntilAssumptionFrame
  , getProofObligations, clearProofObligations
  , LabeledPred(..), abortExecBecause, AbortExecReason(..), addAssumption
  , addDurableAssertion, addDurableProofObligation
  , CrucibleAssumption(..), ppAbortExecReason
  , IsSymBackend(..), HasSymInterface(..)
  , labeledPred, labeledPredMsg
  -- , ProofObligations, proofGoal, goalsToList, labeledPredMsg
  )
import Lang.Crucible.Backend.Simple (SimpleBackend, newSimpleBackend)
import Lang.Crucible.CFG.Core (AnyCFG(..), cfgArgTypes, cfgReturnType)
import Lang.Crucible.CFG.Common ( freshGlobalVar )
import Lang.Crucible.FunctionHandle (HandleAllocator, newHandleAllocator)
import Lang.Crucible.Simulator
  ( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..)
  , defaultAbortHandler, runOverrideSim, partialValue, gpValue
  , GlobalVar, executeCrucible, OverrideSim, ovrWithBackend, regValue
  , readGlobal, modifyGlobal, callCFG, emptyRegMap, RegEntry(..)
  , AbortedResult(..)
  )
import Lang.Crucible.Simulator.ExecutionTree ( withBackend )
import Lang.Crucible.Simulator.GlobalState ( insertGlobal )
import Lang.Crucible.Simulator.RegValue (RegValue, RegValue'(..))
import Lang.Crucible.Simulator.SimError (SimError(..), SimErrorReason(..)) -- ppSimError
import Lang.Crucible.Types
  ( TypeRepr(..), (:~:)(..), KnownRepr(..), NatType )

import Lang.Crucible.LLVM (llvmGlobals, registerLazyModule, register_llvm_overrides)
import Lang.Crucible.LLVM.Bytes (bitsToBytes)
import Lang.Crucible.LLVM.DataLayout (Alignment, DataLayout)
import Lang.Crucible.LLVM.Errors (BadBehavior)
import Lang.Crucible.LLVM.Extension (LLVM, ArchWidth)
import Lang.Crucible.LLVM.Globals (initializeAllMemory, populateAllGlobals)
import Lang.Crucible.LLVM.Intrinsics
  ( IntrinsicsOptions, OverrideTemplate, basic_llvm_override, LLVMOverride(..) )

import Lang.Crucible.LLVM.MemType
  ( MemType(..), SymType(..)
  , i1, i8, i16, i32, i64
  , memTypeSize, memTypeAlign
  , mkStructInfo
  )
import Lang.Crucible.LLVM.MemModel
  ( mkMemVar, withPtrWidth, HasLLVMAnn, LLVMAnnMap, MemImpl
  , HasPtrWidth, doResolveGlobal, doStore
  , LLVMPtr, LLVMVal, MemOptions, PartLLVMVal(..), StorageType, bitvectorType
  , ptrAdd, toStorableType, projectLLVM_bv
  , pattern LLVMPointerRepr, pattern PtrRepr, loadRaw, llvmPointer_bv
  , memRepr, Mem, unpackMemValue
  )
import Lang.Crucible.LLVM.MemModel.CallStack (CallStack)
import Lang.Crucible.LLVM.MemModel.Partial (BoolAnn(..))
import Lang.Crucible.LLVM.PrettyPrint (ppSymbol)
import Lang.Crucible.LLVM.Translation
  ( LLVMTranslationWarning(..), ModuleTranslation
  , getTranslatedCFG, translateModule, globalInitMap
  , transContext, llvmPtrWidth, llvmTypeCtx, llvmTypeAsRepr
  )
import Lang.Crucible.LLVM.TypeContext (TypeContext, llvmDataLayout)

import Crux (defaultOutputConfig)
import Crux.Config (cfgJoin, Config(..))
import Crux.Config.Load (fromFile, fromEnv)
import Crux.Config.Common
  ( cruxOptions, CruxOptions(..), postprocessOptions, outputOptions
  , OutputOptions(..)
  )
import Crux.Goal (proveGoalsOffline, provedGoalsTree)
import qualified Crux.Log as Log
import Crux.Types (SimCtxt, Crux, ProcessedGoals(..), ProofResult(..))

import Crux.LLVM.Config (llvmCruxConfig, LLVMOptions(..))
import Crux.LLVM.Compile (genBitCode)
import qualified Crux.LLVM.Log as Log
import Crux.LLVM.Simulate (setupSimCtxt, parseLLVM, explainFailure)
import CruxLLVMMain (processLLVMOptions)

import What4.Config
  (extendConfig)
import What4.Interface
  ( Pred, bvLit, bvAdd, bvUrem, bvMul, bvIsNonzero, bvEq, isEq
  , getConfiguration, freshBoundedBV, predToBV
  , getCurrentProgramLoc, printSymExpr
  , truePred, falsePred, andPred, annotateTerm, backendPred
  , getAnnotation, natAdd, natEq, natIte, natLit
  )
import What4.Expr.Builder
  ( Flags, ExprBuilder, BoolExpr, startCaching
  , newExprBuilder
  )
import What4.FunctionName (functionName)
import What4.InterpretedFloatingPoint
  ( FloatInfoRepr(..), IsInterpretedFloatExprBuilder(..)
  , SingleFloat, DoubleFloat
  )
import What4.ProgramLoc (ProgramLoc, mkProgramLoc, plFunction, Position(..))
import What4.Solver.Adapter (SolverAdapter(..))
import What4.Symbol (safeSymbol)

-- | @'verify' csettings props prefix spec@ verifies the Copilot specification
-- @spec@ under the assumptions @props@ matches the behavior of the C program
-- compiled with @csettings@ within a directory prefixed by @prefix@.
verify :: CSettings -> [String] -> String -> Spec -> IO ()
verify :: CSettings -> [String] -> String -> Spec -> IO ()
verify = VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
defaultVerifierOptions

-- | Options for configuring the behavior of the verifier.
data VerifierOptions = VerifierOptions
  { VerifierOptions -> Verbosity
verbosity :: Verbosity
    -- ^ How much output the verifier should produce.
  , VerifierOptions -> Bool
assumePartialSideConds :: Bool
    -- ^ If 'True', the verifier will determine the conditions under which
    --   a Copilot specification's partial operations are well defined and
    --   add these side conditions as assumptions. As a result, even if the
    --   generated C code performs a partial operation, the verification will
    --   succeed if this partial operation coincides with a corresponding
    --   operation on the Copilot side.
    --
    --   If 'False', the verifier will not assume any side conditions related
    --   to partial operations in the Copilot specification. As a result, any
    --   use of a partial operation in the generated C code will cause
    --   verification to fail unless the user adds their own assumptions.
  , VerifierOptions -> Bool
logSmtInteractions :: Bool
    -- ^ If 'True', create log files corresponding to the SMT solver
    -- interactions used to discharge each proof goal. The file will be named
    -- @<step>-<goal number>-<solver>.smt2@, where:
    --
    -- * @<step>@ will be either @initial-step@ or @transition-step@, depending
    --   on which step of the proof the goal corresponds to.
    --
    -- * @<goal number>@ will be the number of the goal, starting at 0 and
    --   counting up. Note that each step of the proof has its own goal
    --   numbers. This means that there can be both an
    --   @initial-step-0-<solver>.smt2@ and a @transition-step-0-<solver>.smt2@,
    --   and similarly for other numbers.
    --
    -- * @<solver>@ is the name of the SMT solver used to discharge the proof
    --   goal. Currently, this will always be @z3@, although we might make this
    --   configurable in the future.
  , VerifierOptions -> Solver
smtSolver :: Solver.Solver
    -- ^ Which SMT solver to use when solving proof goals.
  , VerifierOptions -> FloatMode
smtFloatMode :: FloatMode.FloatMode
    -- ^ How the verifier should interpret floating-point operations when
    -- translating them to SMT.
    --
    -- By default, the verifier will treat all floating-point operations as
    -- uninterpreted functions ('FloatMode.FloatUninterpreted'). This allows the
    -- verifier to perform some limited reasoning about floating-point
    -- operations that SMT solvers do not have built-in operations for (@sin@,
    -- @cos@, @tan@, etc.), but at the expense of not being able to verify C
    -- code in which the compiler optimizes floating-point expressions. One can
    -- also opt into an alternative mode where floating-point values are treated
    -- as IEEE-754 floats ('FloatMode.FloatIEEE'), but this comes with the
    -- drawback that the verifier will not be able to perform /any/ reasoning
    -- about @sin@, @cos@, @tan@, etc.
  } deriving stock Int -> VerifierOptions -> ShowS
[VerifierOptions] -> ShowS
VerifierOptions -> String
(Int -> VerifierOptions -> ShowS)
-> (VerifierOptions -> String)
-> ([VerifierOptions] -> ShowS)
-> Show VerifierOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VerifierOptions -> ShowS
showsPrec :: Int -> VerifierOptions -> ShowS
$cshow :: VerifierOptions -> String
show :: VerifierOptions -> String
$cshowList :: [VerifierOptions] -> ShowS
showList :: [VerifierOptions] -> ShowS
Show

-- | The default 'VerifierOptions':
--
-- * Produce a reasonable amount of diagnostics as verification proceeds
--   ('Default').
--
-- * Do not assume any side conditions related to partial operations.
--
-- * Do not log any SMT solver interactions.
--
-- * Use the Z3 SMT solver.
--
-- * Treat all floating-point operations as uninterpreted functions when
--   translating to SMT.
defaultVerifierOptions :: VerifierOptions
defaultVerifierOptions :: VerifierOptions
defaultVerifierOptions = VerifierOptions
  { verbosity :: Verbosity
verbosity = Verbosity
Default
  , assumePartialSideConds :: Bool
assumePartialSideConds = Bool
False
  , logSmtInteractions :: Bool
logSmtInteractions = Bool
False
  , smtSolver :: Solver
smtSolver = Solver
Solver.Z3
  , smtFloatMode :: FloatMode
smtFloatMode = FloatMode
FloatMode.FloatUninterpreted
  }

-- | Like 'defaultVerifierOptions', except that the verifier will assume side
-- conditions related to partial operations used in the Copilot spec.
sideCondVerifierOptions :: VerifierOptions
sideCondVerifierOptions :: VerifierOptions
sideCondVerifierOptions = VerifierOptions
defaultVerifierOptions
  { assumePartialSideConds = True
  }

-- | How much output should verification produce?
--
-- The data constructors are listed in increasing order of how many diagnostics
-- they produce.
data Verbosity
  = Quiet   -- ^ Don't produce any diagnostics.
  | Default -- ^ Produce a reasonable amount of diagnostics as verification proceeds.
  | Noisy   -- ^ Produce as many diagnostics as possible.
  deriving stock (Verbosity -> Verbosity -> Bool
(Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool) -> Eq Verbosity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Verbosity -> Verbosity -> Bool
== :: Verbosity -> Verbosity -> Bool
$c/= :: Verbosity -> Verbosity -> Bool
/= :: Verbosity -> Verbosity -> Bool
Eq, Eq Verbosity
Eq Verbosity =>
(Verbosity -> Verbosity -> Ordering)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Bool)
-> (Verbosity -> Verbosity -> Verbosity)
-> (Verbosity -> Verbosity -> Verbosity)
-> Ord Verbosity
Verbosity -> Verbosity -> Bool
Verbosity -> Verbosity -> Ordering
Verbosity -> Verbosity -> Verbosity
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Verbosity -> Verbosity -> Ordering
compare :: Verbosity -> Verbosity -> Ordering
$c< :: Verbosity -> Verbosity -> Bool
< :: Verbosity -> Verbosity -> Bool
$c<= :: Verbosity -> Verbosity -> Bool
<= :: Verbosity -> Verbosity -> Bool
$c> :: Verbosity -> Verbosity -> Bool
> :: Verbosity -> Verbosity -> Bool
$c>= :: Verbosity -> Verbosity -> Bool
>= :: Verbosity -> Verbosity -> Bool
$cmax :: Verbosity -> Verbosity -> Verbosity
max :: Verbosity -> Verbosity -> Verbosity
$cmin :: Verbosity -> Verbosity -> Verbosity
min :: Verbosity -> Verbosity -> Verbosity
Ord, Int -> Verbosity -> ShowS
[Verbosity] -> ShowS
Verbosity -> String
(Int -> Verbosity -> ShowS)
-> (Verbosity -> String)
-> ([Verbosity] -> ShowS)
-> Show Verbosity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Verbosity -> ShowS
showsPrec :: Int -> Verbosity -> ShowS
$cshow :: Verbosity -> String
show :: Verbosity -> String
$cshowList :: [Verbosity] -> ShowS
showList :: [Verbosity] -> ShowS
Show)

-- | Like 'verify', but with 'VerifierOptions' to more finely control the
-- verifier's behavior.
verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions VerifierOptions
opts CSettings
csettings0 [String]
properties String
prefix Spec
spec =
  ((SupportsCruxLogMessage CopilotLogging,
  SupportsCruxLLVMLogMessage CopilotLogging,
  SupportsCopilotLogMessage CopilotLogging) =>
 IO ())
-> IO ()
forall computation.
((SupportsCruxLogMessage CopilotLogging,
  SupportsCruxLLVMLogMessage CopilotLogging,
  SupportsCopilotLogMessage CopilotLogging) =>
 computation)
-> computation
withCopilotLogging (((SupportsCruxLogMessage CopilotLogging,
   SupportsCruxLLVMLogMessage CopilotLogging,
   SupportsCopilotLogMessage CopilotLogging) =>
  IO ())
 -> IO ())
-> ((SupportsCruxLogMessage CopilotLogging,
     SupportsCruxLLVMLogMessage CopilotLogging,
     SupportsCopilotLogMessage CopilotLogging) =>
    IO ())
-> IO ()
forall a b. (a -> b) -> a -> b
$
  do -- munge options structures into the necessary forms
     (OutputConfig CopilotLogging
ocfg, CruxOptions
cruxOpts, LLVMOptions
llvmOpts, CSettings
csettings, String
csrc) <- SupportsCruxLogMessage CopilotLogging =>
VerifierOptions
-> CSettings
-> String
-> IO
     (OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings,
      String)
VerifierOptions
-> CSettings
-> String
-> IO
     (OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings,
      String)
computeConfiguration VerifierOptions
opts CSettings
csettings0 String
prefix
     let ?outputConfig = ?outputConfig::OutputConfig CopilotLogging
OutputConfig CopilotLogging
ocfg

     -- Compile the Copilot spec into C source code, using
     -- preexisting Copilot library calls.
     CSettings -> String -> Spec -> IO ()
compileWith CSettings
csettings String
prefix Spec
spec
     CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> CopilotLogMessage
Log.GeneratedCFile String
csrc

     -- Compile the C source into LLVM bitcode, using preexisting
     -- Crux library calls.
     String
bcFile <- CruxOptions -> LLVMOptions -> IO String
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions -> LLVMOptions -> IO String
genBitCode CruxOptions
cruxOpts LLVMOptions
llvmOpts
     CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> CopilotLogMessage
Log.CompiledBitcodeFile String
prefix String
bcFile

     -- Run the main verification procedure
     VerifierOptions
-> CSettings
-> [String]
-> Spec
-> CruxOptions
-> LLVMOptions
-> String
-> String
-> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCruxLLVMLogMessage msgs, SupportsCopilotLogMessage msgs) =>
VerifierOptions
-> CSettings
-> [String]
-> Spec
-> CruxOptions
-> LLVMOptions
-> String
-> String
-> IO ()
verifyBitcode VerifierOptions
opts CSettings
csettings [String]
properties Spec
spec CruxOptions
cruxOpts LLVMOptions
llvmOpts String
csrc String
bcFile


-- | Do the (surprisingly large amount) of options munging necessary to set up
--   the crucible/crux environment.
computeConfiguration ::
  Log.SupportsCruxLogMessage CopilotLogging =>
  VerifierOptions -> CSettings -> FilePath ->
  IO (Log.OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings, FilePath)
computeConfiguration :: SupportsCruxLogMessage CopilotLogging =>
VerifierOptions
-> CSettings
-> String
-> IO
     (OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings,
      String)
computeConfiguration VerifierOptions
opts CSettings
csettings0 String
prefix =
  do Maybe OutputOptions -> OutputConfig CopilotLogging
ocfg1 <- (CopilotLogging -> SayWhat)
-> IO (Maybe OutputOptions -> OutputConfig CopilotLogging)
forall msgs.
ToJSON msgs =>
(msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs)
defaultOutputConfig CopilotLogging -> SayWhat
copilotLoggingToSayWhat
     let quiet :: Bool
quiet = VerifierOptions -> Verbosity
verbosity VerifierOptions
opts Verbosity -> Verbosity -> Bool
forall a. Eq a => a -> a -> Bool
== Verbosity
Quiet
     let ocfg2 :: Maybe OutputOptions -> OutputConfig CopilotLogging
ocfg2 Maybe OutputOptions
mbOutputOpts = (Maybe OutputOptions -> OutputConfig CopilotLogging
ocfg1 Maybe OutputOptions
mbOutputOpts) { Log._quiet = quiet }
     Config LLVMOptions
llvmcfg <- IO (Config LLVMOptions)
llvmCruxConfig
     let cfg :: Config (CruxOptions, LLVMOptions)
cfg = Config CruxOptions
-> Config LLVMOptions -> Config (CruxOptions, LLVMOptions)
forall a b. Config a -> Config b -> Config (a, b)
cfgJoin Config CruxOptions
cruxOptions Config LLVMOptions
llvmcfg
     -- TODO, load from an actual configuration file?
     (CruxOptions, LLVMOptions)
fileOpts <- Text
-> Config (CruxOptions, LLVMOptions)
-> Maybe String
-> IO (CruxOptions, LLVMOptions)
forall opts. Text -> Config opts -> Maybe String -> IO opts
fromFile Text
"copilot-verifier" Config (CruxOptions, LLVMOptions)
cfg Maybe String
forall a. Maybe a
Nothing
     (CruxOptions
cruxOpts0, LLVMOptions
llvmOpts0) <- ((CruxOptions, LLVMOptions)
 -> EnvDescr (CruxOptions, LLVMOptions)
 -> IO (CruxOptions, LLVMOptions))
-> (CruxOptions, LLVMOptions)
-> [EnvDescr (CruxOptions, LLVMOptions)]
-> IO (CruxOptions, LLVMOptions)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (CruxOptions, LLVMOptions)
-> EnvDescr (CruxOptions, LLVMOptions)
-> IO (CruxOptions, LLVMOptions)
forall opts. opts -> EnvDescr opts -> IO opts
fromEnv (CruxOptions, LLVMOptions)
fileOpts (Config (CruxOptions, LLVMOptions)
-> [EnvDescr (CruxOptions, LLVMOptions)]
forall opts. Config opts -> [EnvDescr opts]
cfgEnv Config (CruxOptions, LLVMOptions)
cfg)
     let odir0 :: String
odir0 = CSettings -> String
cSettingsOutputDirectory CSettings
csettings0
     let odir :: String
odir = -- A bit grimy, but this corresponds to how crux-llvm sets
                -- its output directory.
                if String
odir0 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"."
                  then String
"results" String -> ShowS
</> String
prefix
                  else String
odir0
     let csettings :: CSettings
csettings = CSettings
csettings0{ cSettingsOutputDirectory = odir }
     let csrc :: String
csrc = String
odir String -> ShowS
</> String
prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".c"
     let cruxOpts1 :: CruxOptions
cruxOpts1 = CruxOptions
cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc]
                              , outputOptions =
                                  (outputOptions cruxOpts0)
                                    { quietMode = quiet
                                    , simVerbose = if verbosity opts > Default
                                                   then 2
                                                   else 0
                                    }
                              }
     let ?outputConfig = Maybe OutputOptions -> OutputConfig CopilotLogging
ocfg2 (OutputOptions -> Maybe OutputOptions
forall a. a -> Maybe a
Just (CruxOptions -> OutputOptions
outputOptions CruxOptions
cruxOpts1))
     CruxOptions
cruxOpts2 <- CruxOptions -> IO CruxOptions
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
postprocessOptions CruxOptions
cruxOpts1

     -- Tweak the options passed to Clang:
     --
     -- - Fix the optimization level to -O0.
     --
     -- - Pass -ffp-contract=off to prevent sequences of floating-point
     --   multiplications/additions from being optimized to llvm.fmuladd
     --   intrinsics, which makes floating-point verification fragile.
     let llvmOpts1 :: LLVMOptions
llvmOpts1 = LLVMOptions
llvmOpts0
                       { optLevel = 0
                       , clangOpts = "-ffp-contract=off" : clangOpts llvmOpts0
                       }
     (CruxOptions
cruxOpts3, LLVMOptions
llvmOpts2) <- (CruxOptions, LLVMOptions) -> IO (CruxOptions, LLVMOptions)
processLLVMOptions (CruxOptions
cruxOpts2, LLVMOptions
llvmOpts1)

     let ocfg3 :: OutputConfig CopilotLogging
ocfg3 = Maybe OutputOptions -> OutputConfig CopilotLogging
ocfg2 (OutputOptions -> Maybe OutputOptions
forall a. a -> Maybe a
Just (CruxOptions -> OutputOptions
outputOptions CruxOptions
cruxOpts3))
     (OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings,
 String)
-> IO
     (OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings,
      String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConfig CopilotLogging
ocfg3, CruxOptions
cruxOpts3, LLVMOptions
llvmOpts2, CSettings
csettings, String
csrc)


data CopilotVerifierData t = CopilotVerifierData


-- | Main entry point for the verifier.
verifyBitcode ::
  Log.Logs msgs =>
  Log.SupportsCruxLogMessage msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  VerifierOptions {- ^ Verifier-specific settings -} ->
  CSettings   {- ^ Settings used to compile the Copilot spec. Used to find the names of functions and variables. -} ->
  [String]    {- ^ Names of properties to assume during verification. -} ->
  Spec        {- ^ The input Copilot specification -} ->
  CruxOptions {- ^ Crux options -} ->
  LLVMOptions {- ^ CruxLLVM options -} ->
  FilePath    {- ^ Path to the generated C file (for logging purposes only) -} ->
  FilePath    {- ^ Path to the bitcode file to verify -} ->
  IO ()
verifyBitcode :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCruxLLVMLogMessage msgs, SupportsCopilotLogMessage msgs) =>
VerifierOptions
-> CSettings
-> [String]
-> Spec
-> CruxOptions
-> LLVMOptions
-> String
-> String
-> IO ()
verifyBitcode VerifierOptions
opts CSettings
csettings [String]
properties Spec
spec CruxOptions
cruxOpts LLVMOptions
llvmOpts String
cFile String
bcFile =
  FloatMode
-> (forall {fm :: FloatMode}. FloatModeRepr fm -> IO ()) -> IO ()
forall r.
FloatMode -> (forall (fm :: FloatMode). FloatModeRepr fm -> r) -> r
FloatMode.withFloatMode (VerifierOptions -> FloatMode
smtFloatMode VerifierOptions
opts) ((forall {fm :: FloatMode}. FloatModeRepr fm -> IO ()) -> IO ())
-> (forall {fm :: FloatMode}. FloatModeRepr fm -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FloatModeRepr fm
fm ->
  do -- Set up the expression builder and symbolic backend
     HandleAllocator
halloc <- IO HandleAllocator
newHandleAllocator
     ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
sym <- FloatModeRepr fm
-> CopilotVerifierData GlobalNonceGenerator
-> NonceGenerator IO GlobalNonceGenerator
-> IO
     (ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
newExprBuilder FloatModeRepr fm
fm CopilotVerifierData GlobalNonceGenerator
forall t. CopilotVerifierData t
CopilotVerifierData NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
     SimpleBackend GlobalNonceGenerator CopilotVerifierData (Flags fm)
bak <- ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
-> IO
     (SimpleBackend GlobalNonceGenerator CopilotVerifierData (Flags fm))
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> IO (SimpleBackend t st fs)
newSimpleBackend ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
sym
     -- turn on hash-consing
     ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
-> IO ()
forall t (st :: * -> *) fs. ExprBuilder t st fs -> IO ()
startCaching ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
sym

     ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
-> FloatModeRepr fm
-> (IsInterpretedFloatExprBuilder
      (ExprBuilder
         GlobalNonceGenerator CopilotVerifierData (Flags fm)) =>
    IO ())
-> IO ()
forall t (st :: * -> *) (fm :: FloatMode) r.
ExprBuilder t st (Flags fm)
-> FloatModeRepr fm
-> (IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) =>
    r)
-> r
FloatMode.withInterpretedFloatExprBuilder ExprBuilder GlobalNonceGenerator CopilotVerifierData (Flags fm)
sym FloatModeRepr fm
fm ((IsInterpretedFloatExprBuilder
    (ExprBuilder
       GlobalNonceGenerator CopilotVerifierData (Flags fm)) =>
  IO ())
 -> IO ())
-> (IsInterpretedFloatExprBuilder
      (ExprBuilder
         GlobalNonceGenerator CopilotVerifierData (Flags fm)) =>
    IO ())
-> IO ()
forall a b. (a -> b) -> a -> b
$
       SimpleBackend GlobalNonceGenerator CopilotVerifierData (Flags fm)
-> HandleAllocator -> IO ()
forall t (st :: * -> *) (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) =>
SimpleBackend t st (Flags fm) -> HandleAllocator -> IO ()
verifyWithSymBackend SimpleBackend GlobalNonceGenerator CopilotVerifierData (Flags fm)
bak HandleAllocator
halloc
  where
    verifyWithSymBackend ::
      forall t st fm.
      IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) =>
      SimpleBackend t st (Flags fm) ->
      HandleAllocator ->
      IO ()
    verifyWithSymBackend :: forall t (st :: * -> *) (fm :: FloatMode).
IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) =>
SimpleBackend t st (Flags fm) -> HandleAllocator -> IO ()
verifyWithSymBackend SimpleBackend t st (Flags fm)
bak HandleAllocator
halloc = do
      let sym :: ExprBuilder t st (Flags fm)
sym = SimpleBackend t st (Flags fm) -> ExprBuilder t st (Flags fm)
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym SimpleBackend t st (Flags fm)
bak
      -- capture LLVM side-condition information for use in error reporting
      CopilotLogRefs (ExprBuilder t st (Flags fm))
clRefs <- IO (CopilotLogRefs (ExprBuilder t st (Flags fm)))
forall sym. IsSymInterface sym => IO (CopilotLogRefs sym)
newCopilotLogRefs
      let ?recordLLVMAnnotation = CopilotLogRefs (ExprBuilder t st (Flags fm))
-> CallStack
-> BoolAnn (ExprBuilder t st (Flags fm))
-> BadBehavior (ExprBuilder t st (Flags fm))
-> IO ()
forall sym.
IsSymInterface sym =>
CopilotLogRefs sym
-> CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()
recordLLVMAnnotation CopilotLogRefs (ExprBuilder t st (Flags fm))
clRefs

      -- Set up the solver to use for verification.
      let adapter :: SolverAdapter st
          adapter :: SolverAdapter st
adapter = Solver -> SolverAdapter st
forall (st :: * -> *). Solver -> SolverAdapter st
Solver.solverAdapter (VerifierOptions -> Solver
smtSolver VerifierOptions
opts)
      [ConfigDesc] -> Config -> IO ()
extendConfig (SolverAdapter st -> [ConfigDesc]
forall (st :: * -> *). SolverAdapter st -> [ConfigDesc]
solver_adapter_config_options SolverAdapter st
adapter) (ExprBuilder t st (Flags fm) -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st (Flags fm)
sym)

      -- Set up the Crucible/LLVM simulation context
      GlobalVar Mem
memVar <- Text -> HandleAllocator -> IO (GlobalVar Mem)
mkMemVar Text
"llvm_memory" HandleAllocator
halloc
      let simctx :: SimContext
  (Crux (ExprBuilder t st (Flags fm)))
  (ExprBuilder t st (Flags fm))
  LLVM
simctx = (HandleAllocator
-> SimpleBackend t st (Flags fm)
-> MemOptions
-> GlobalVar Mem
-> SimContext
     (Crux (ExprBuilder t st (Flags fm)))
     (ExprBuilder t st (Flags fm))
     LLVM
forall sym bak.
(IsSymBackend sym bak, HasLLVMAnn sym) =>
HandleAllocator
-> bak -> MemOptions -> GlobalVar Mem -> SimCtxt Crux sym LLVM
setupSimCtxt HandleAllocator
halloc SimpleBackend t st (Flags fm)
bak (LLVMOptions -> MemOptions
memOpts LLVMOptions
llvmOpts) GlobalVar Mem
memVar)
                   { printHandle = view Log.outputHandle ?outputConfig }

      -- Load and translate the input LLVM module
      Module
llvmMod <- String -> IO Module
parseLLVM String
bcFile
      Some ModuleTranslation x
trans <-
         let ?transOpts = LLVMOptions -> TranslationOptions
transOpts LLVMOptions
llvmOpts
          in (?transOpts::TranslationOptions) =>
HandleAllocator
-> GlobalVar Mem -> Module -> IO (Some ModuleTranslation)
HandleAllocator
-> GlobalVar Mem -> Module -> IO (Some ModuleTranslation)
translateModule HandleAllocator
halloc GlobalVar Mem
memVar Module
llvmMod

      CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot CopilotLogMessage
Log.TranslatedToCrucible

      -- Grab some metadata from the bitcode file and options;
      -- make the available via implicit arguments to the places
      -- that expect them.
      let llvmCtxt :: LLVMContext x
llvmCtxt = ModuleTranslation x
trans ModuleTranslation x
-> Getting (LLVMContext x) (ModuleTranslation x) (LLVMContext x)
-> LLVMContext x
forall s a. s -> Getting a s a -> a
^. Getting (LLVMContext x) (ModuleTranslation x) (LLVMContext x)
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext
      let ?lc = LLVMContext x
llvmCtxt LLVMContext x
-> Getting TypeContext (LLVMContext x) TypeContext -> TypeContext
forall s a. s -> Getting a s a -> a
^. Getting TypeContext (LLVMContext x) TypeContext
forall (arch :: LLVMArch) (f :: * -> *).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
      let ?memOpts = LLVMOptions -> MemOptions
memOpts LLVMOptions
llvmOpts
      let ?intrinsicsOpts = LLVMOptions -> IntrinsicsOptions
intrinsicsOpts LLVMOptions
llvmOpts

      LLVMContext x
-> forall a.
   ((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> a) -> a
forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
   ((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth LLVMContext x
llvmCtxt (((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> IO ()) -> IO ())
-> ((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \NatRepr (ArchWidth x)
ptrW ->
        NatRepr (ArchWidth x)
-> (HasPtrWidth (ArchWidth x) => IO ()) -> IO ()
forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth x)
ptrW ((HasPtrWidth (ArchWidth x) => IO ()) -> IO ())
-> (HasPtrWidth (ArchWidth x) => IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$

        do -- Compute the LLVM memory state with global variables allocated
           -- but not initialized
           MemImpl (ExprBuilder t st (Flags fm))
emptyMem   <- SimpleBackend t st (Flags fm)
-> LLVMContext x
-> Module
-> IO (MemImpl (ExprBuilder t st (Flags fm)))
forall sym bak (wptr :: Natural) (arch :: LLVMArch).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak -> LLVMContext arch -> Module -> IO (MemImpl sym)
initializeAllMemory SimpleBackend t st (Flags fm)
bak LLVMContext x
llvmCtxt Module
llvmMod

           -- Compute the LLVM memory state with global variables initialized
           -- to their initial values.
           MemImpl (ExprBuilder t st (Flags fm))
initialMem <- SimpleBackend t st (Flags fm)
-> GlobalInitializerMap
-> MemImpl (ExprBuilder t st (Flags fm))
-> IO (MemImpl (ExprBuilder t st (Flags fm)))
forall (wptr :: Natural) sym bak.
(?lc::TypeContext, ?memOpts::MemOptions, 16 <= wptr,
 HasPtrWidth wptr, HasLLVMAnn sym, IsSymBackend sym bak) =>
bak -> GlobalInitializerMap -> MemImpl sym -> IO (MemImpl sym)
populateAllGlobals SimpleBackend t st (Flags fm)
bak (ModuleTranslation x
trans ModuleTranslation x
-> Getting
     GlobalInitializerMap (ModuleTranslation x) GlobalInitializerMap
-> GlobalInitializerMap
forall s a. s -> Getting a s a -> a
^. Getting
  GlobalInitializerMap (ModuleTranslation x) GlobalInitializerMap
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(GlobalInitializerMap -> f GlobalInitializerMap)
-> ModuleTranslation arch -> f (ModuleTranslation arch)
globalInitMap) MemImpl (ExprBuilder t st (Flags fm))
emptyMem

           -- Use the Copilot spec directly to compute the symbolic states
           -- necessary to carry out the states of the bisimulation proof.
           CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot CopilotLogMessage
Log.GeneratingProofState
           BisimulationProofBundle (ExprBuilder t st (Flags fm))
proofStateBundle <- ExprBuilder t st (Flags fm)
-> [String]
-> Spec
-> IO (BisimulationProofBundle (ExprBuilder t st (Flags fm)))
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> [String] -> Spec -> IO (BisimulationProofBundle sym)
CW4.computeBisimulationProofBundle ExprBuilder t st (Flags fm)
sym [String]
properties Spec
spec

           -- First check that the initial state of the program matches the starting
           -- segment of the associated Copilot streams.
           let cruxOptsInit :: CruxOptions
cruxOptsInit = String -> CruxOptions -> CruxOptions
setCruxOfflineSolverOutput String
"initial-step" CruxOptions
cruxOpts
           Integer
initGoals <-
             CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs (ExprBuilder t st (Flags fm))
-> SimContext
     (Crux (ExprBuilder t st (Flags fm)))
     (ExprBuilder t st (Flags fm))
     LLVM
-> MemImpl (ExprBuilder t st (Flags fm))
-> BisimulationProofState (ExprBuilder t st (Flags fm))
-> IO Integer
forall sym msgs t (st :: * -> *) fs (wptr :: Natural).
(IsSymInterface sym, Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCopilotLogMessage msgs, sym ~ ExprBuilder t st fs,
 HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts::MemOptions,
 ?lc::TypeContext) =>
CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> MemImpl sym
-> BisimulationProofState sym
-> IO Integer
verifyInitialState CruxOptions
cruxOptsInit [SolverAdapter st
adapter] CopilotLogRefs (ExprBuilder t st (Flags fm))
clRefs SimContext
  (Crux (ExprBuilder t st (Flags fm)))
  (ExprBuilder t st (Flags fm))
  LLVM
simctx MemImpl (ExprBuilder t st (Flags fm))
initialMem
               (BisimulationProofBundle (ExprBuilder t st (Flags fm))
-> BisimulationProofState (ExprBuilder t st (Flags fm))
forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
CW4.initialStreamState BisimulationProofBundle (ExprBuilder t st (Flags fm))
proofStateBundle)

           -- Now, the real meat. Carry out the bisimulation step of the proof.
           let cruxOptsTrans :: CruxOptions
cruxOptsTrans = String -> CruxOptions -> CruxOptions
setCruxOfflineSolverOutput String
"transition-step" CruxOptions
cruxOpts
           Integer
bisimGoals <-
             VerifierOptions
-> CruxOptions
-> [SolverAdapter st]
-> CSettings
-> CopilotLogRefs (ExprBuilder t st (Flags fm))
-> SimContext
     (Crux (ExprBuilder t st (Flags fm)))
     (ExprBuilder t st (Flags fm))
     LLVM
-> Module
-> ModuleTranslation x
-> GlobalVar Mem
-> MemImpl (ExprBuilder t st (Flags fm))
-> BisimulationProofBundle (ExprBuilder t st (Flags fm))
-> IO Integer
forall sym msgs t (st :: * -> *) fs (wptr :: Natural)
       (arch :: LLVMArch).
(IsSymInterface sym, Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCruxLLVMLogMessage msgs, SupportsCopilotLogMessage msgs,
 sym ~ ExprBuilder t st fs, HasPtrWidth wptr, HasLLVMAnn sym,
 1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
 ?memOpts::MemOptions, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions) =>
VerifierOptions
-> CruxOptions
-> [SolverAdapter st]
-> CSettings
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> Module
-> ModuleTranslation arch
-> GlobalVar Mem
-> MemImpl sym
-> BisimulationProofBundle sym
-> IO Integer
verifyStepBisimulation VerifierOptions
opts CruxOptions
cruxOptsTrans [SolverAdapter st
adapter] CSettings
csettings
               CopilotLogRefs (ExprBuilder t st (Flags fm))
clRefs SimContext
  (Crux (ExprBuilder t st (Flags fm)))
  (ExprBuilder t st (Flags fm))
  LLVM
simctx Module
llvmMod ModuleTranslation x
trans GlobalVar Mem
memVar MemImpl (ExprBuilder t st (Flags fm))
initialMem BisimulationProofBundle (ExprBuilder t st (Flags fm))
proofStateBundle

           CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Integer -> Integer -> CopilotLogMessage
Log.SuccessfulProofSummary String
cFile Integer
initGoals Integer
bisimGoals
           -- We only want to inform users about Noisy if the verbosity level is
           -- sufficiently low. Crux's logging framework isn't particularly
           -- suited to doing this, as it assumes that all log messages enabled
           -- for low verbosity levels should also be enabled for higher
           -- verbosity levels. That is a reasonable assumption most of the time,
           -- but not here.
           --
           -- To compensate, we hack around the issue by manually checking the
           -- verbosity level before logging the message.
           Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VerifierOptions -> Verbosity
verbosity VerifierOptions
opts Verbosity -> Verbosity -> Bool
forall a. Ord a => a -> a -> Bool
< Verbosity
Noisy) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
             CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot CopilotLogMessage
Log.NoisyVerbositySuggestion

    -- If @logSmtInteractions@ is enabled, enable offline solver output in the
    -- supplied 'CruxOptions' with the supplied file template. Otherwise, return
    -- the supplied 'CruxOptions' unaltered.
    setCruxOfflineSolverOutput :: FilePath -> CruxOptions -> CruxOptions
    setCruxOfflineSolverOutput :: String -> CruxOptions -> CruxOptions
setCruxOfflineSolverOutput String
template CruxOptions
cruxOpts'
      | VerifierOptions -> Bool
logSmtInteractions VerifierOptions
opts
      = CruxOptions
cruxOpts'
          { offlineSolverOutput = Just $ outDir cruxOpts' </> template <.> "smt2" }
      | Bool
otherwise
      = CruxOptions
cruxOpts'

-- | Capture LLVM side-condition information for use in error reporting.
recordLLVMAnnotation ::
  IsSymInterface sym =>
  CopilotLogRefs sym ->
  CallStack ->
  BoolAnn sym ->
  BadBehavior sym ->
  IO ()
recordLLVMAnnotation :: forall sym.
IsSymInterface sym =>
CopilotLogRefs sym
-> CallStack -> BoolAnn sym -> BadBehavior sym -> IO ()
recordLLVMAnnotation CopilotLogRefs sym
clRefs CallStack
stk BoolAnn sym
bann BadBehavior sym
bb =
  IORef (LLVMAnnMap sym)
-> (LLVMAnnMap sym -> LLVMAnnMap sym) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym -> IORef (LLVMAnnMap sym)
forall sym. CopilotLogRefs sym -> IORef (LLVMAnnMap sym)
llvmAnnMapRef CopilotLogRefs sym
clRefs) (BoolAnn sym
-> (CallStack, BadBehavior sym) -> LLVMAnnMap sym -> LLVMAnnMap sym
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BoolAnn sym
bann (CallStack
stk, BadBehavior sym
bb))

-- | Prove that the state of the global variables at program startup
--   matches the expected initial segments of the associated Copilot
--   streams.
verifyInitialState ::
  IsSymInterface sym =>
  Log.Logs msgs =>
  Log.SupportsCruxLogMessage msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  sym ~ ExprBuilder t st fs =>
  HasPtrWidth wptr =>
  HasLLVMAnn sym =>
  (?memOpts :: MemOptions) =>
  (?lc :: TypeContext) =>

  CruxOptions ->
  [SolverAdapter st] ->
  CopilotLogRefs sym ->
  SimCtxt Crux sym LLVM ->
  MemImpl sym ->
  CW4.BisimulationProofState sym ->
  IO Integer
verifyInitialState :: forall sym msgs t (st :: * -> *) fs (wptr :: Natural).
(IsSymInterface sym, Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCopilotLogMessage msgs, sym ~ ExprBuilder t st fs,
 HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts::MemOptions,
 ?lc::TypeContext) =>
CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> MemImpl sym
-> BisimulationProofState sym
-> IO Integer
verifyInitialState CruxOptions
cruxOpts [SolverAdapter st]
adapters CopilotLogRefs sym
clRefs SimCtxt Crux sym LLVM
simctx MemImpl sym
mem BisimulationProofState sym
initialState =
  SimCtxt Crux sym LLVM
-> (forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
-> IO Integer
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimCtxt Crux sym LLVM
simctx ((forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
 -> IO Integer)
-> (forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
-> IO Integer
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
  do CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ VerificationStep -> CopilotLogMessage
Log.ComputingConditions VerificationStep
Log.InitialState
     FrameIdentifier
frm <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
pushAssumptionFrame bak
bak

     bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
forall sym bak msgs (wptr :: Natural).
(IsSymBackend sym bak, Logs msgs, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, ?lc::TypeContext) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
assertStateRelation bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem
       StateRelationStep
Log.InitialStateRelation BisimulationProofState sym
initialState

     bak -> FrameIdentifier -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> FrameIdentifier -> IO ()
popUntilAssumptionFrame bak
bak FrameIdentifier
frm

     CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ VerificationStep -> CopilotLogMessage
Log.ProvingConditions VerificationStep
Log.InitialState
     CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> VerificationStep
-> SimCtxt Crux sym LLVM
-> IO Integer
forall sym t (st :: * -> *) fs msgs.
(IsSymInterface sym, sym ~ ExprBuilder t st fs, Logs msgs,
 SupportsCruxLogMessage msgs, SupportsCopilotLogMessage msgs) =>
CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> VerificationStep
-> SimCtxt Crux sym LLVM
-> IO Integer
proveObls CruxOptions
cruxOpts [SolverAdapter st]
adapters CopilotLogRefs sym
clRefs VerificationStep
Log.InitialState SimCtxt Crux sym LLVM
simctx


verifyStepBisimulation ::
  IsSymInterface sym =>
  Log.Logs msgs =>
  Log.SupportsCruxLogMessage msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  sym ~ ExprBuilder t st fs =>
  HasPtrWidth wptr =>
  HasLLVMAnn sym =>
  (1 <= ArchWidth arch) =>
  HasPtrWidth (ArchWidth arch) =>
  (?memOpts :: MemOptions) =>
  (?lc :: TypeContext) =>
  (?intrinsicsOpts :: IntrinsicsOptions) =>

  VerifierOptions ->
  CruxOptions ->
  [SolverAdapter st] ->
  CSettings ->
  CopilotLogRefs sym ->
  SimCtxt Crux sym LLVM ->
  L.Module ->
  ModuleTranslation arch ->
  GlobalVar Mem ->
  MemImpl sym ->
  CW4.BisimulationProofBundle sym ->
  IO Integer
verifyStepBisimulation :: forall sym msgs t (st :: * -> *) fs (wptr :: Natural)
       (arch :: LLVMArch).
(IsSymInterface sym, Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCruxLLVMLogMessage msgs, SupportsCopilotLogMessage msgs,
 sym ~ ExprBuilder t st fs, HasPtrWidth wptr, HasLLVMAnn sym,
 1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
 ?memOpts::MemOptions, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions) =>
VerifierOptions
-> CruxOptions
-> [SolverAdapter st]
-> CSettings
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> Module
-> ModuleTranslation arch
-> GlobalVar Mem
-> MemImpl sym
-> BisimulationProofBundle sym
-> IO Integer
verifyStepBisimulation VerifierOptions
opts CruxOptions
cruxOpts [SolverAdapter st]
adapters CSettings
csettings CopilotLogRefs sym
clRefs SimCtxt Crux sym LLVM
simctx Module
llvmMod ModuleTranslation arch
modTrans GlobalVar Mem
memVar MemImpl sym
mem BisimulationProofBundle sym
prfbundle =
  SimCtxt Crux sym LLVM
-> (forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
-> IO Integer
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimCtxt Crux sym LLVM
simctx ((forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
 -> IO Integer)
-> (forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
-> IO Integer
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
  do CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ VerificationStep -> CopilotLogMessage
Log.ComputingConditions VerificationStep
Log.StepBisimulation

     FrameIdentifier
frm <- bak -> IO FrameIdentifier
forall sym bak. IsSymBackend sym bak => bak -> IO FrameIdentifier
pushAssumptionFrame bak
bak

     do -- set up the memory image
        MemImpl sym
mem' <- bak
-> MemImpl sym -> BisimulationProofBundle sym -> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, ?lc::TypeContext) =>
bak
-> MemImpl sym -> BisimulationProofBundle sym -> IO (MemImpl sym)
setupPrestate bak
bak MemImpl sym
mem BisimulationProofBundle sym
prfbundle

        -- sanity check, verify that we set up the memory in the expected relation
        bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
forall sym bak msgs (wptr :: Natural).
(IsSymBackend sym bak, Logs msgs, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, ?lc::TypeContext) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
assertStateRelation bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem'
          StateRelationStep
Log.PreStepStateRelation (BisimulationProofBundle sym -> BisimulationProofState sym
forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
CW4.preStreamState BisimulationProofBundle sym
prfbundle)

        -- set up trigger guard global variables
        let halloc :: HandleAllocator
halloc = SimCtxt Crux sym LLVM -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
simHandleAllocator SimCtxt Crux sym LLVM
simctx
        -- See Note [Global variables for trigger functions]
        let prepTrigger :: (String, Expr t BaseBoolType, [(Some Type, XExpr sym)])
-> IO (String, GlobalVar 'NatType, Expr t BaseBoolType)
prepTrigger (String
nm, Expr t BaseBoolType
guard, [(Some Type, XExpr sym)]
_) =
              do GlobalVar 'NatType
gv <- HandleAllocator
-> Text -> TypeRepr 'NatType -> IO (GlobalVar 'NatType)
forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
freshGlobalVar HandleAllocator
halloc (String -> Text
Text.pack (String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_called")) TypeRepr 'NatType
NatRepr
                 (String, GlobalVar 'NatType, Expr t BaseBoolType)
-> IO (String, GlobalVar 'NatType, Expr t BaseBoolType)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, GlobalVar 'NatType
gv, Expr t BaseBoolType
guard)

            checkDuplicateTriggerNames :: [Name] -> IO ()
            checkDuplicateTriggerNames :: [String] -> IO ()
checkDuplicateTriggerNames [String]
triggers =
              (NonEmpty String -> IO ()) -> [NonEmpty String] -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ NonEmpty String -> IO ()
checkDuplicateTriggerName ([NonEmpty String] -> IO ()) -> [NonEmpty String] -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> [NonEmpty String]
forall (f :: * -> *) a. (Foldable f, Eq a) => f a -> [NonEmpty a]
NE.group ([String] -> [NonEmpty String]) -> [String] -> [NonEmpty String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. Ord a => [a] -> [a]
sort [String]
triggers

            checkDuplicateTriggerName :: NonEmpty Name -> IO ()
            checkDuplicateTriggerName :: NonEmpty String -> IO ()
checkDuplicateTriggerName (String
trig :| [String]
dupTrigs) =
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dupTrigs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                  [ String
"The specification invokes the `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
trig String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    String
"` trigger function multiple times,"
                  , String
"which copilot-verifier does not currently support."
                  , String
"See https://github.com/Copilot-Language/copilot-verifier/issues/74."
                  ]
        let triggerState :: [(String, Pred sym, [(Some Type, XExpr sym)])]
triggerState = BisimulationProofBundle sym
-> [(String, Pred sym, [(Some Type, XExpr sym)])]
forall sym.
BisimulationProofBundle sym
-> [(String, Pred sym, [(Some Type, XExpr sym)])]
CW4.triggerState BisimulationProofBundle sym
prfbundle
        [String] -> IO ()
checkDuplicateTriggerNames ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ ((String, Expr t BaseBoolType, [(Some Type, XExpr sym)]) -> String)
-> [(String, Expr t BaseBoolType, [(Some Type, XExpr sym)])]
-> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
nm,Expr t BaseBoolType
_,[(Some Type, XExpr sym)]
_) -> String
nm) [(String, Expr t BaseBoolType, [(Some Type, XExpr sym)])]
[(String, Pred sym, [(Some Type, XExpr sym)])]
triggerState
        [(String, GlobalVar 'NatType, Expr t BaseBoolType)]
triggerGlobals <- ((String, Expr t BaseBoolType, [(Some Type, XExpr sym)])
 -> IO (String, GlobalVar 'NatType, Expr t BaseBoolType))
-> [(String, Expr t BaseBoolType, [(Some Type, XExpr sym)])]
-> IO [(String, GlobalVar 'NatType, Expr t BaseBoolType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (String, Expr t BaseBoolType, [(Some Type, XExpr sym)])
-> IO (String, GlobalVar 'NatType, Expr t BaseBoolType)
prepTrigger [(String, Expr t BaseBoolType, [(Some Type, XExpr sym)])]
[(String, Pred sym, [(Some Type, XExpr sym)])]
triggerState

        -- execute the step function
        let overrides :: [OverrideTemplate (Crux sym) sym LLVM arch]
overrides = ((String, GlobalVar 'NatType, Expr t BaseBoolType)
 -> (String, Expr t BaseBoolType, [(Some Type, XExpr sym)])
 -> OverrideTemplate (Crux sym) sym LLVM arch)
-> [(String, GlobalVar 'NatType, Expr t BaseBoolType)]
-> [(String, Expr t BaseBoolType, [(Some Type, XExpr sym)])]
-> [OverrideTemplate (Crux sym) sym LLVM arch]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (CopilotLogRefs sym
-> (String, GlobalVar 'NatType, Pred sym)
-> (String, Expr t BaseBoolType, [(Some Type, XExpr sym)])
-> OverrideTemplate (Crux sym) sym LLVM arch
forall sym t (arch :: LLVMArch) msgs.
(IsSymInterface sym, Logs msgs, SupportsCopilotLogMessage msgs,
 ?memOpts::MemOptions, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions, 1 <= ArchWidth arch,
 HasPtrWidth (ArchWidth arch), HasLLVMAnn sym) =>
CopilotLogRefs sym
-> (String, GlobalVar 'NatType, Pred sym)
-> (String, BoolExpr t, [(Some Type, XExpr sym)])
-> OverrideTemplate (Crux sym) sym LLVM arch
triggerOverride CopilotLogRefs sym
clRefs) [(String, GlobalVar 'NatType, Expr t BaseBoolType)]
triggerGlobals [(String, Expr t BaseBoolType, [(Some Type, XExpr sym)])]
[(String, Pred sym, [(Some Type, XExpr sym)])]
triggerState
        MemImpl sym
mem'' <- VerifierOptions
-> CSettings
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> GlobalVar Mem
-> MemImpl sym
-> Module
-> ModuleTranslation arch
-> [(String, GlobalVar 'NatType, Pred sym)]
-> [OverrideTemplate (Crux sym) sym LLVM arch]
-> [Pred sym]
-> [Pred sym]
-> IO (MemImpl sym)
forall sym (arch :: LLVMArch) msgs.
(IsSymInterface sym, Logs msgs, SupportsCruxLLVMLogMessage msgs,
 SupportsCopilotLogMessage msgs, ?memOpts::MemOptions,
 ?lc::TypeContext, ?intrinsicsOpts::IntrinsicsOptions,
 1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
 HasLLVMAnn sym) =>
VerifierOptions
-> CSettings
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> GlobalVar Mem
-> MemImpl sym
-> Module
-> ModuleTranslation arch
-> [(String, GlobalVar 'NatType, Pred sym)]
-> [OverrideTemplate (Crux sym) sym LLVM arch]
-> [Pred sym]
-> [Pred sym]
-> IO (MemImpl sym)
executeStep VerifierOptions
opts CSettings
csettings CopilotLogRefs sym
clRefs SimCtxt Crux sym LLVM
simctx GlobalVar Mem
memVar MemImpl sym
mem' Module
llvmMod ModuleTranslation arch
modTrans [(String, GlobalVar 'NatType, Expr t BaseBoolType)]
[(String, GlobalVar 'NatType, Pred sym)]
triggerGlobals [OverrideTemplate (Crux sym) sym LLVM arch]
overrides (BisimulationProofBundle sym -> [Pred sym]
forall sym. BisimulationProofBundle sym -> [Pred sym]
CW4.assumptions BisimulationProofBundle sym
prfbundle) (BisimulationProofBundle sym -> [Pred sym]
forall sym. BisimulationProofBundle sym -> [Pred sym]
CW4.sideConds BisimulationProofBundle sym
prfbundle)

        -- assert the poststate is in the relation
        bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
forall sym bak msgs (wptr :: Natural).
(IsSymBackend sym bak, Logs msgs, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, ?lc::TypeContext) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
assertStateRelation bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem''
          StateRelationStep
Log.PostStepStateRelation (BisimulationProofBundle sym -> BisimulationProofState sym
forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
CW4.postStreamState BisimulationProofBundle sym
prfbundle)

     bak -> FrameIdentifier -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> FrameIdentifier -> IO ()
popUntilAssumptionFrame bak
bak FrameIdentifier
frm

     CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ VerificationStep -> CopilotLogMessage
Log.ProvingConditions VerificationStep
Log.StepBisimulation
     CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> VerificationStep
-> SimCtxt Crux sym LLVM
-> IO Integer
forall sym t (st :: * -> *) fs msgs.
(IsSymInterface sym, sym ~ ExprBuilder t st fs, Logs msgs,
 SupportsCruxLogMessage msgs, SupportsCopilotLogMessage msgs) =>
CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> VerificationStep
-> SimCtxt Crux sym LLVM
-> IO Integer
proveObls CruxOptions
cruxOpts [SolverAdapter st]
adapters CopilotLogRefs sym
clRefs VerificationStep
Log.StepBisimulation SimCtxt Crux sym LLVM
simctx


-- | Set up the "trigger override" functions.  These dummy functions
--   take the place of the external functions called by the Copilot
--   monitor when a guarded condition occurs.
--
--   Each trigger statement has a corresponding global variable that
--   is used to record if the trigger function was called; initially
--   the global is false, and is set to true when the trigger function
--   is called.  At the end of verification, we check that the value
--   of this global variable is true iff the corresponding trigger guard
--   condition is true.
--
--   The other function of the trigger overrides is to check that, when called,
--   the functions are given the expected argument values.
--
--   Otherwise, the override functions have no effects, which corresponds
--   to the assumption that the external environment makes no changes to the
--   program state that are observable to the Copilot monitor.
triggerOverride :: forall sym t arch msgs.
  IsSymInterface sym =>
  Log.Logs msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  (?memOpts :: MemOptions) =>
  (?lc :: TypeContext) =>
  (?intrinsicsOpts :: IntrinsicsOptions) =>
  (1 <= ArchWidth arch) =>
  HasPtrWidth (ArchWidth arch) =>
  HasLLVMAnn sym =>

  CopilotLogRefs sym ->
  (Name, GlobalVar NatType, Pred sym) ->
  (Name, BoolExpr t, [(Some Type, CW4.XExpr sym)]) ->
  OverrideTemplate (Crux sym) sym LLVM arch
triggerOverride :: forall sym t (arch :: LLVMArch) msgs.
(IsSymInterface sym, Logs msgs, SupportsCopilotLogMessage msgs,
 ?memOpts::MemOptions, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions, 1 <= ArchWidth arch,
 HasPtrWidth (ArchWidth arch), HasLLVMAnn sym) =>
CopilotLogRefs sym
-> (String, GlobalVar 'NatType, Pred sym)
-> (String, BoolExpr t, [(Some Type, XExpr sym)])
-> OverrideTemplate (Crux sym) sym LLVM arch
triggerOverride CopilotLogRefs sym
clRefs (String
_,GlobalVar 'NatType
triggerGlobal,Pred sym
_) (String
nm, BoolExpr t
_guard, [(Some Type, XExpr sym)]
args) =
   let args' :: [Some TypeRepr]
args' = ((Some Type, XExpr sym) -> Some TypeRepr)
-> [(Some Type, XExpr sym)] -> [Some TypeRepr]
forall a b. (a -> b) -> [a] -> [b]
map (Some Type, XExpr sym) -> Some TypeRepr
forall {wptr :: Natural} {b}.
(Assert
   (OrdCond (CmpNat 1 wptr) 'True 'True 'False) (TypeError ...),
 Assert
   (OrdCond (CmpNat 16 wptr) 'True 'True 'False) (TypeError ...),
 ?ptrWidth::NatRepr wptr, ?lc::TypeContext) =>
(Some Type, b) -> Some TypeRepr
toTypeRepr [(Some Type, XExpr sym)]
args in
   case [Some TypeRepr] -> Some (Assignment TypeRepr)
forall {k} (f :: k -> *). [Some f] -> Some (Assignment f)
Ctx.fromList [Some TypeRepr]
args' of
     Some Assignment TypeRepr x
argCtx ->
      LLVMOverride (Crux sym) sym LLVM x 'UnitType
-> OverrideTemplate (Crux sym) sym LLVM arch
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext args ret -> OverrideTemplate p sym ext arch
basic_llvm_override (LLVMOverride (Crux sym) sym LLVM x 'UnitType
 -> OverrideTemplate (Crux sym) sym LLVM arch)
-> LLVMOverride (Crux sym) sym LLVM x 'UnitType
-> OverrideTemplate (Crux sym) sym LLVM arch
forall a b. (a -> b) -> a -> b
$
      Declare
-> Assignment TypeRepr x
-> TypeRepr 'UnitType
-> (IsSymInterface sym =>
    GlobalVar Mem
    -> Assignment (RegEntry sym) x
    -> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
       OverrideSim
         (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
-> LLVMOverride (Crux sym) sym LLVM x 'UnitType
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare
-> CtxRepr args
-> TypeRepr ret
-> (IsSymInterface sym =>
    GlobalVar Mem
    -> Assignment (RegEntry sym) args
    -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
       OverrideSim p sym ext rtp args' ret' (RegValue sym ret))
-> LLVMOverride p sym ext args ret
LLVMOverride Declare
decl Assignment TypeRepr x
argCtx TypeRepr 'UnitType
UnitRepr ((IsSymInterface sym =>
  GlobalVar Mem
  -> Assignment (RegEntry sym) x
  -> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
     OverrideSim
       (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
 -> LLVMOverride (Crux sym) sym LLVM x 'UnitType)
-> (IsSymInterface sym =>
    GlobalVar Mem
    -> Assignment (RegEntry sym) x
    -> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
       OverrideSim
         (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
-> LLVMOverride (Crux sym) sym LLVM x 'UnitType
forall a b. (a -> b) -> a -> b
$
        \GlobalVar Mem
memOps Assignment (RegEntry sym) x
calledArgs ->
          (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
-> OverrideSim
     (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
 -> OverrideSim
      (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType))
-> OverrideSim
     (Crux sym) sym LLVM rtp args' ret' (RegValue sym 'UnitType)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
          do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
             GlobalVar 'NatType
-> (RegValue sym 'NatType
    -> OverrideSim
         (Crux sym) sym LLVM rtp args' ret' ((), RegValue sym 'NatType))
-> OverrideSim (Crux sym) sym LLVM rtp args' ret' ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar 'NatType
triggerGlobal ((RegValue sym 'NatType
  -> OverrideSim
       (Crux sym) sym LLVM rtp args' ret' ((), RegValue sym 'NatType))
 -> OverrideSim (Crux sym) sym LLVM rtp args' ret' ())
-> (RegValue sym 'NatType
    -> OverrideSim
         (Crux sym) sym LLVM rtp args' ret' ((), RegValue sym 'NatType))
-> OverrideSim (Crux sym) sym LLVM rtp args' ret' ()
forall a b. (a -> b) -> a -> b
$ \RegValue sym 'NatType
count -> do
               -- See Note [Global variables for trigger functions]
               SymNat sym
countPlusOne <- IO (SymNat sym)
-> OverrideSim (Crux sym) sym LLVM rtp args' ret' (SymNat sym)
forall a. IO a -> OverrideSim (Crux sym) sym LLVM rtp args' ret' a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymNat sym)
 -> OverrideSim (Crux sym) sym LLVM rtp args' ret' (SymNat sym))
-> IO (SymNat sym)
-> OverrideSim (Crux sym) sym LLVM rtp args' ret' (SymNat sym)
forall a b. (a -> b) -> a -> b
$ do
                 SymNat sym
one <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
1
                 sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd sym
sym RegValue sym 'NatType
SymNat sym
count SymNat sym
one
               ((), SymNat sym)
-> OverrideSim (Crux sym) sym LLVM rtp args' ret' ((), SymNat sym)
forall a. a -> OverrideSim (Crux sym) sym LLVM rtp args' ret' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((), SymNat sym
countPlusOne)
             MemImpl sym
mem <- GlobalVar Mem
-> OverrideSim
     (Crux sym) sym LLVM rtp args' ret' (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
memOps
             IO () -> OverrideSim (Crux sym) sym LLVM rtp args' ret' ()
forall a. IO a -> OverrideSim (Crux sym) sym LLVM rtp args' ret' a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim (Crux sym) sym LLVM rtp args' ret' ())
-> IO () -> OverrideSim (Crux sym) sym LLVM rtp args' ret' ()
forall a b. (a -> b) -> a -> b
$ bak
-> MemImpl sym
-> [Some (RegEntry sym)]
-> [(Some Type, XExpr sym)]
-> IO ()
forall bak.
IsSymBackend sym bak =>
bak
-> MemImpl sym
-> [Some (RegEntry sym)]
-> [(Some Type, XExpr sym)]
-> IO ()
checkArgs bak
bak MemImpl sym
mem ((forall (x :: CrucibleType). RegEntry sym x -> Some (RegEntry sym))
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> [Some (RegEntry sym)]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> *) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC RegEntry sym x -> Some (RegEntry sym)
forall k (f :: k -> *) (x :: k). f x -> Some f
forall (x :: CrucibleType). RegEntry sym x -> Some (RegEntry sym)
Some Assignment (RegEntry sym) x
calledArgs) [(Some Type, XExpr sym)]
args
             () -> OverrideSim (Crux sym) sym LLVM rtp args' ret' ()
forall a. a -> OverrideSim (Crux sym) sym LLVM rtp args' ret' a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

 where
  decl :: Declare
decl = L.Declare
         { decLinkage :: Maybe Linkage
L.decLinkage = Maybe Linkage
forall a. Maybe a
Nothing
         , decVisibility :: Maybe Visibility
L.decVisibility = Maybe Visibility
forall a. Maybe a
Nothing
         , decRetType :: Type
L.decRetType = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType PrimType
L.Void
         , decName :: Symbol
L.decName = String -> Symbol
L.Symbol String
nm
         , decArgs :: [Type]
L.decArgs = ((Some Type, XExpr sym) -> Type)
-> [(Some Type, XExpr sym)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Some Type, XExpr sym) -> Type
forall {b}. (Some Type, b) -> Type
llvmArgTy [(Some Type, XExpr sym)]
args
         , decVarArgs :: Bool
L.decVarArgs = Bool
False
         , decAttrs :: [FunAttr]
L.decAttrs = []
         , decComdat :: Maybe String
L.decComdat = Maybe String
forall a. Maybe a
Nothing
         }

  -- Use the `-CompositePtr` functions here to ensure that arguments with array
  -- or struct types are treated as pointers. See Note [Arrays and structs].
  toTypeRepr :: (Some Type, b) -> Some TypeRepr
toTypeRepr (Some Type x
ctp, b
_) = MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr (DataLayout -> Type x -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeCompositePtr (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) Type x
ctp) TypeRepr tp -> Some TypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr
Some
  llvmArgTy :: (Some Type, b) -> Type
llvmArgTy (Some Type x
ctp, b
_) = Type x -> Type
forall a. Type a -> Type
copilotTypeToLLVMTypeCompositePtr Type x
ctp

  checkArgs :: forall bak. IsSymBackend sym bak =>
    bak -> MemImpl sym -> [Some (RegEntry sym)] -> [(Some Type, CW4.XExpr sym)] -> IO ()
  checkArgs :: forall bak.
IsSymBackend sym bak =>
bak
-> MemImpl sym
-> [Some (RegEntry sym)]
-> [(Some Type, XExpr sym)]
-> IO ()
checkArgs bak
bak MemImpl sym
mem = Integer
-> [Some (RegEntry sym)] -> [(Some Type, XExpr sym)] -> IO ()
loop (Integer
0::Integer)
    where
    loop :: Integer
-> [Some (RegEntry sym)] -> [(Some Type, XExpr sym)] -> IO ()
loop Integer
i (Some (RegEntry sym)
x:[Some (RegEntry sym)]
xs) ((Some Type
ctp,XExpr sym
v):[(Some Type, XExpr sym)]
vs) = bak
-> MemImpl sym
-> Integer
-> Some (RegEntry sym)
-> Some Type
-> XExpr sym
-> IO ()
forall bak.
IsSymBackend sym bak =>
bak
-> MemImpl sym
-> Integer
-> Some (RegEntry sym)
-> Some Type
-> XExpr sym
-> IO ()
checkArg bak
bak MemImpl sym
mem Integer
i Some (RegEntry sym)
x Some Type
ctp XExpr sym
v IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Integer
-> [Some (RegEntry sym)] -> [(Some Type, XExpr sym)] -> IO ()
loop (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) [Some (RegEntry sym)]
xs [(Some Type, XExpr sym)]
vs
    loop Integer
_ [] [] = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    loop Integer
_ [Some (RegEntry sym)]
_ [(Some Type, XExpr sym)]
_ = String -> IO ()
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Argument list mismatch in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm

  checkArg :: forall bak. IsSymBackend sym bak =>
    bak -> MemImpl sym -> Integer -> Some (RegEntry sym) -> Some Type -> CW4.XExpr sym -> IO ()
  checkArg :: forall bak.
IsSymBackend sym bak =>
bak
-> MemImpl sym
-> Integer
-> Some (RegEntry sym)
-> Some Type
-> XExpr sym
-> IO ()
checkArg bak
bak MemImpl sym
mem Integer
i (Some (RegEntry TypeRepr x
tp RegValue sym x
v)) (Some Type x
ctp) XExpr sym
x =
    do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
       Pred sym
eq <- bak
-> CopilotLogRefs sym
-> MemImpl sym
-> Type x
-> XExpr sym
-> TypeRepr x
-> RegValue sym x
-> IO (Pred sym)
forall sym bak (tp :: CrucibleType) a (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> Type a
-> XExpr sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (Pred sym)
computeEqualVals bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem Type x
ctp XExpr sym
x TypeRepr x
tp RegValue sym x
v
       (SymAnnotation sym BaseBoolType
ann, Pred sym
eq') <- sym -> Pred sym -> IO (SymAnnotation sym BaseBoolType, Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym Pred sym
eq
       let shortmsg :: String
shortmsg = String
"Trigger " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" argument " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
       let longmsg :: String
longmsg  = Doc Any -> String
forall a. Show a => a -> String
show (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
printSymExpr Pred sym
eq')
       let rsn :: SimErrorReason
rsn      = String -> String -> SimErrorReason
AssertFailureSimError String
shortmsg String
longmsg
       ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
       IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs)
         ((Map (BoolAnn sym) (VerifierAssertion sym)
  -> Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO ())
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a b. (a -> b) -> a -> b
$ BoolAnn sym
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
ann)
         (VerifierAssertion sym
 -> Map (BoolAnn sym) (VerifierAssertion sym)
 -> Map (BoolAnn sym) (VerifierAssertion sym))
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ SomeSome (TriggerArgumentEquality sym) -> VerifierAssertion sym
forall sym.
SomeSome (TriggerArgumentEquality sym) -> VerifierAssertion sym
Log.TriggerArgumentEqualityAssertion
         (SomeSome (TriggerArgumentEquality sym) -> VerifierAssertion sym)
-> SomeSome (TriggerArgumentEquality sym) -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ TriggerArgumentEquality sym x x
-> SomeSome (TriggerArgumentEquality sym)
forall {j} {k} (f :: j -> k -> *) (x :: j) (y :: k).
f x y -> SomeSome f
Log.SomeSome
         (TriggerArgumentEquality sym x x
 -> SomeSome (TriggerArgumentEquality sym))
-> TriggerArgumentEquality sym x x
-> SomeSome (TriggerArgumentEquality sym)
forall a b. (a -> b) -> a -> b
$ sym
-> ProgramLoc
-> String
-> Integer
-> Type x
-> XExpr sym
-> TypeRepr x
-> RegValue sym x
-> TriggerArgumentEquality sym x x
forall sym copilotType (crucibleType :: CrucibleType).
sym
-> ProgramLoc
-> String
-> Integer
-> Type copilotType
-> XExpr sym
-> TypeRepr crucibleType
-> RegValue sym crucibleType
-> TriggerArgumentEquality sym copilotType crucibleType
Log.TriggerArgumentEquality sym
sym ProgramLoc
loc String
nm Integer
i Type x
ctp XExpr sym
x TypeRepr x
tp RegValue sym x
v
       bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
eq' (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
rsn))


-- | Actually execute the Crucible simulator on the generated "step" function.
--   This will record proof side-conditions into the symbolic backend, and
--   return the memory state corresponding to the function post-state.
--
--   This function will record side-conditions that arise from the semantics
--   of C itself (e.g., memory is accessed in bounds and signed arithmetic
--   doesn't overflow) as well as the conditions related to trigger functions.
executeStep :: forall sym arch msgs.
  IsSymInterface sym =>
  Log.Logs msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  (?memOpts :: MemOptions) =>
  (?lc :: TypeContext) =>
  (?intrinsicsOpts :: IntrinsicsOptions) =>
  (1 <= ArchWidth arch) =>
  HasPtrWidth (ArchWidth arch) =>
  HasLLVMAnn sym =>

  VerifierOptions ->
  CSettings ->
  CopilotLogRefs sym ->
  SimCtxt Crux sym LLVM ->
  GlobalVar Mem ->
  MemImpl sym ->
  L.Module ->
  ModuleTranslation arch ->
  [(Name, GlobalVar NatType, Pred sym)] ->
  [OverrideTemplate (Crux sym) sym LLVM arch] ->
  [Pred sym] {- User-provided property assumptions -} ->
  [Pred sym] {- Side conditions related to partial operations -} ->
  IO (MemImpl sym)
executeStep :: forall sym (arch :: LLVMArch) msgs.
(IsSymInterface sym, Logs msgs, SupportsCruxLLVMLogMessage msgs,
 SupportsCopilotLogMessage msgs, ?memOpts::MemOptions,
 ?lc::TypeContext, ?intrinsicsOpts::IntrinsicsOptions,
 1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
 HasLLVMAnn sym) =>
VerifierOptions
-> CSettings
-> CopilotLogRefs sym
-> SimCtxt Crux sym LLVM
-> GlobalVar Mem
-> MemImpl sym
-> Module
-> ModuleTranslation arch
-> [(String, GlobalVar 'NatType, Pred sym)]
-> [OverrideTemplate (Crux sym) sym LLVM arch]
-> [Pred sym]
-> [Pred sym]
-> IO (MemImpl sym)
executeStep VerifierOptions
opts CSettings
csettings CopilotLogRefs sym
clRefs SimCtxt Crux sym LLVM
simctx GlobalVar Mem
memVar MemImpl sym
mem Module
llvmmod ModuleTranslation arch
modTrans [(String, GlobalVar 'NatType, Pred sym)]
triggerGlobals [OverrideTemplate (Crux sym) sym LLVM arch]
triggerOverrides [Pred sym]
assums [Pred sym]
sideConds =
  do SymGlobalState sym
globSt <- (SymGlobalState sym
 -> (String, GlobalVar 'NatType, Pred sym)
 -> IO (SymGlobalState sym))
-> SymGlobalState sym
-> [(String, GlobalVar 'NatType, Pred sym)]
-> IO (SymGlobalState sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM SymGlobalState sym
-> (String, GlobalVar 'NatType, Pred sym)
-> IO (SymGlobalState sym)
setupTrigger (GlobalVar Mem -> MemImpl sym -> SymGlobalState sym
forall sym. GlobalVar Mem -> MemImpl sym -> SymGlobalState sym
llvmGlobals GlobalVar Mem
memVar MemImpl sym
mem) [(String, GlobalVar 'NatType, Pred sym)]
triggerGlobals
     let initSt :: ExecState (Crux sym) sym LLVM (RegEntry sym Mem)
initSt = SimCtxt Crux sym LLVM
-> SymGlobalState sym
-> AbortHandler (Crux sym) sym LLVM (RegEntry sym Mem)
-> TypeRepr Mem
-> ExecCont
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     (OverrideLang Mem)
     ('Just EmptyCtx)
-> ExecState (Crux sym) sym LLVM (RegEntry sym Mem)
forall p sym ext rtp (ret :: CrucibleType).
(rtp ~ RegEntry sym ret) =>
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
InitialState SimCtxt Crux sym LLVM
simctx SymGlobalState sym
globSt AbortHandler (Crux sym) sym LLVM (RegEntry sym Mem)
forall sym p ext rtp.
IsSymInterface sym =>
AbortHandler p sym ext rtp
defaultAbortHandler TypeRepr Mem
memRepr (ExecCont
   (Crux sym)
   sym
   LLVM
   (RegEntry sym Mem)
   (OverrideLang Mem)
   ('Just EmptyCtx)
 -> ExecState (Crux sym) sym LLVM (RegEntry sym Mem))
-> ExecCont
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     (OverrideLang Mem)
     ('Just EmptyCtx)
-> ExecState (Crux sym) sym LLVM (RegEntry sym Mem)
forall a b. (a -> b) -> a -> b
$
                    TypeRepr Mem
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (RegValue sym Mem)
-> ExecCont
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     (OverrideLang Mem)
     ('Just EmptyCtx)
forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType).
TypeRepr tp
-> OverrideSim p sym ext rtp args tp (RegValue sym tp)
-> ExecCont p sym ext rtp (OverrideLang tp) ('Just args)
runOverrideSim TypeRepr Mem
memRepr OverrideSim
  (Crux sym)
  sym
  LLVM
  (RegEntry sym Mem)
  EmptyCtx
  Mem
  (RegValue sym Mem)
OverrideSim
  (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)
runStep
     ExecResult (Crux sym) sym LLVM (RegEntry sym Mem)
res <- [ExecutionFeature (Crux sym) sym LLVM (RegEntry sym Mem)]
-> ExecState (Crux sym) sym LLVM (RegEntry sym Mem)
-> IO (ExecResult (Crux sym) sym LLVM (RegEntry sym Mem))
forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
executeCrucible [] ExecState (Crux sym) sym LLVM (RegEntry sym Mem)
initSt
     case ExecResult (Crux sym) sym LLVM (RegEntry sym Mem)
res of
       FinishedResult SimCtxt Crux sym LLVM
_ PartialResult sym LLVM (RegEntry sym Mem)
pr -> MemImpl sym -> IO (MemImpl sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (PartialResult sym LLVM (RegEntry sym Mem)
prPartialResult sym LLVM (RegEntry sym Mem)
-> Getting
     (MemImpl sym)
     (PartialResult sym LLVM (RegEntry sym Mem))
     (MemImpl sym)
-> MemImpl sym
forall s a. s -> Getting a s a -> a
^.(GlobalPair sym (RegEntry sym Mem)
 -> Const (MemImpl sym) (GlobalPair sym (RegEntry sym Mem)))
-> PartialResult sym LLVM (RegEntry sym Mem)
-> Const (MemImpl sym) (PartialResult sym LLVM (RegEntry sym Mem))
forall sym ext u v (f :: * -> *).
Functor f =>
(GlobalPair sym u -> f (GlobalPair sym v))
-> PartialResult sym ext u -> f (PartialResult sym ext v)
partialValue((GlobalPair sym (RegEntry sym Mem)
  -> Const (MemImpl sym) (GlobalPair sym (RegEntry sym Mem)))
 -> PartialResult sym LLVM (RegEntry sym Mem)
 -> Const (MemImpl sym) (PartialResult sym LLVM (RegEntry sym Mem)))
-> ((MemImpl sym -> Const (MemImpl sym) (MemImpl sym))
    -> GlobalPair sym (RegEntry sym Mem)
    -> Const (MemImpl sym) (GlobalPair sym (RegEntry sym Mem)))
-> Getting
     (MemImpl sym)
     (PartialResult sym LLVM (RegEntry sym Mem))
     (MemImpl sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegEntry sym Mem -> Const (MemImpl sym) (RegEntry sym Mem))
-> GlobalPair sym (RegEntry sym Mem)
-> Const (MemImpl sym) (GlobalPair sym (RegEntry sym Mem))
forall sym u v (f :: * -> *).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
gpValue((RegEntry sym Mem -> Const (MemImpl sym) (RegEntry sym Mem))
 -> GlobalPair sym (RegEntry sym Mem)
 -> Const (MemImpl sym) (GlobalPair sym (RegEntry sym Mem)))
-> ((MemImpl sym -> Const (MemImpl sym) (MemImpl sym))
    -> RegEntry sym Mem -> Const (MemImpl sym) (RegEntry sym Mem))
-> (MemImpl sym -> Const (MemImpl sym) (MemImpl sym))
-> GlobalPair sym (RegEntry sym Mem)
-> Const (MemImpl sym) (GlobalPair sym (RegEntry sym Mem))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(RegEntry sym Mem -> MemImpl sym)
-> (MemImpl sym -> Const (MemImpl sym) (MemImpl sym))
-> RegEntry sym Mem
-> Const (MemImpl sym) (RegEntry sym Mem)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to RegEntry sym Mem -> RegValue sym Mem
RegEntry sym Mem -> MemImpl sym
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue)
       AbortedResult SimCtxt Crux sym LLVM
_ AbortedResult sym LLVM
abortRes -> String -> IO (MemImpl sym)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (MemImpl sym)) -> String -> IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ AbortedResult sym LLVM -> Doc Any
forall ext ann. AbortedResult sym ext -> Doc ann
ppAbortedResult AbortedResult sym LLVM
abortRes
       TimeoutResult{} -> String -> IO (MemImpl sym)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"simulation timed out!"

 where
  -- See Note [Global variables for trigger functions]
  setupTrigger :: SymGlobalState sym
-> (String, GlobalVar 'NatType, Pred sym)
-> IO (SymGlobalState sym)
setupTrigger SymGlobalState sym
gs (String
_,GlobalVar 'NatType
gv,Pred sym
_) = do
    SymNat sym
zero <- IO (SymNat sym) -> IO (SymNat sym)
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymNat sym) -> IO (SymNat sym))
-> IO (SymNat sym) -> IO (SymNat sym)
forall a b. (a -> b) -> a -> b
$ sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0
    SymGlobalState sym -> IO (SymGlobalState sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SymGlobalState sym -> IO (SymGlobalState sym))
-> SymGlobalState sym -> IO (SymGlobalState sym)
forall a b. (a -> b) -> a -> b
$ GlobalVar 'NatType
-> RegValue sym 'NatType
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal GlobalVar 'NatType
gv RegValue sym 'NatType
SymNat sym
zero SymGlobalState sym
gs
  llvm_ctx :: LLVMContext arch
llvm_ctx = ModuleTranslation arch
modTrans ModuleTranslation arch
-> Getting
     (LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
-> LLVMContext arch
forall s a. s -> Getting a s a -> a
^. Getting
  (LLVMContext arch) (ModuleTranslation arch) (LLVMContext arch)
forall (arch :: LLVMArch) (f :: * -> *).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext
  stepName :: String
stepName = CSettings -> String
cSettingsStepFunctionName CSettings
csettings
  sym :: sym
sym = SimCtxt Crux sym LLVM
simctxSimCtxt Crux sym LLVM
-> Getting sym (SimCtxt Crux sym LLVM) sym -> sym
forall s a. s -> Getting a s a -> a
^.Getting sym (SimCtxt Crux sym LLVM) sym
forall p sym ext (f :: * -> *).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
ctxSymInterface

  -- TODO, would be lovely to be able to do better than dummy positions for all these things
  -- so we can correspond assumptions and asserts back to the parts of the original spec that
  -- gave rise to them.
  dummyLoc :: ProgramLoc
dummyLoc = FunctionName -> Position -> ProgramLoc
mkProgramLoc FunctionName
"<>" Position
InternalPos

  assumeProperty :: Pred sym -> IO ()
assumeProperty Pred sym
b =
    SimCtxt Crux sym LLVM
-> (forall bak. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimCtxt Crux sym LLVM
simctx ((forall bak. IsSymBackend sym bak => bak -> IO ()) -> IO ())
-> (forall bak. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> String -> Pred sym -> Assumption sym
forall (e :: BaseType -> *).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
GenericAssumption ProgramLoc
dummyLoc String
"Property assumption" Pred sym
b)

  assumeSideCond :: Pred sym -> IO ()
assumeSideCond Pred sym
b =
    SimCtxt Crux sym LLVM
-> (forall bak. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimCtxt Crux sym LLVM
simctx ((forall bak. IsSymBackend sym bak => bak -> IO ()) -> IO ())
-> (forall bak. IsSymBackend sym bak => bak -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
      bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (ProgramLoc -> String -> Pred sym -> Assumption sym
forall (e :: BaseType -> *).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
GenericAssumption ProgramLoc
dummyLoc String
"Side condition for partial operation" Pred sym
b)

  ppAbortedResult :: AbortedResult sym ext -> PP.Doc ann
  ppAbortedResult :: forall ext ann. AbortedResult sym ext -> Doc ann
ppAbortedResult AbortedResult sym ext
abortRes =
    case AbortedResult sym ext -> NonEmpty (Doc ann)
forall ext ann. AbortedResult sym ext -> NonEmpty (Doc ann)
gatherReasons AbortedResult sym ext
abortRes of
      Doc ann
reason :| [] -> Doc ann
reason
      NonEmpty (Doc ann)
reasons      -> [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 ann
"Simulation aborted for multiple reasons."
                              Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: NonEmpty (Doc ann) -> [Doc ann]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Doc ann)
reasons

  gatherReasons :: AbortedResult sym ext -> NonEmpty (PP.Doc ann)
  gatherReasons :: forall ext ann. AbortedResult sym ext -> NonEmpty (Doc ann)
gatherReasons (AbortedExec AbortExecReason
rsn GlobalPair sym (SimFrame sym ext l args)
_) =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat [Doc ann
"Simulation aborted!", AbortExecReason -> Doc ann
forall ann. AbortExecReason -> Doc ann
ppAbortExecReason AbortExecReason
rsn] Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| []
  gatherReasons (AbortedExit ExitCode
ec) =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat [Doc ann
"Simulation called exit!", ExitCode -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow ExitCode
ec] Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| []
  gatherReasons (AbortedBranch ProgramLoc
_ Pred sym
_ AbortedResult sym ext
t AbortedResult sym ext
f) =
    AbortedResult sym ext -> NonEmpty (Doc ann)
forall ext ann. AbortedResult sym ext -> NonEmpty (Doc ann)
gatherReasons AbortedResult sym ext
t NonEmpty (Doc ann) -> NonEmpty (Doc ann) -> NonEmpty (Doc ann)
forall a. Semigroup a => a -> a -> a
<> AbortedResult sym ext -> NonEmpty (Doc ann)
forall ext ann. AbortedResult sym ext -> NonEmpty (Doc ann)
gatherReasons AbortedResult sym ext
f

  -- Simulator entry point
  runStep :: OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)
  runStep :: OverrideSim
  (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)
runStep =
    do -- set up built-in functions and trigger overrides
       ([SomeLLVMOverride (Crux sym) sym LLVM],
 [SomeLLVMOverride (Crux sym) sym LLVM])
_ <- Module
-> [OverrideTemplate (Crux sym) sym LLVM arch]
-> [OverrideTemplate (Crux sym) sym LLVM arch]
-> LLVMContext arch
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     ([SomeLLVMOverride (Crux sym) sym LLVM],
      [SomeLLVMOverride (Crux sym) sym LLVM])
forall sym (wptr :: Natural) (arch :: LLVMArch) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
Module
-> [OverrideTemplate p sym LLVM arch]
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim
     p
     sym
     LLVM
     rtp
     l
     a
     ([SomeLLVMOverride p sym LLVM], [SomeLLVMOverride p sym LLVM])
register_llvm_overrides Module
llvmmod [] [OverrideTemplate (Crux sym) sym LLVM arch]
triggerOverrides LLVMContext arch
llvm_ctx
       -- set up functions defined in the module
       (LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall (arch :: LLVMArch) sym p rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch),
 IsSymInterface sym) =>
(LLVMTranslationWarning -> IO ())
-> ModuleTranslation arch -> OverrideSim p sym LLVM rtp l a ()
registerLazyModule LLVMTranslationWarning -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning ModuleTranslation arch
modTrans

       -- make any property assumptions
       IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((Pred sym -> IO ()) -> [Pred sym] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Pred sym -> IO ()
assumeProperty [Pred sym]
assums)

       -- assume side conditions related to partial operations
       Bool
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (VerifierOptions -> Bool
assumePartialSideConds VerifierOptions
opts) (OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$
         (Pred sym -> IO ()) -> [Pred sym] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Pred sym -> IO ()
assumeSideCond [Pred sym]
sideConds

       -- look up and call the step function
       Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
mbCfg <- IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
 -> OverrideSim
      (Crux sym)
      sym
      LLVM
      (RegEntry sym Mem)
      EmptyCtx
      Mem
      (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a b. (a -> b) -> a -> b
$ ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
getTranslatedCFG ModuleTranslation arch
modTrans (String -> Symbol
L.Symbol String
stepName)
       () <- case Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
mbCfg of
         Just (Declare
_, AnyCFG CFG LLVM blocks init ret
anyCfg, [LLVMTranslationWarning]
warns) -> do
           IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ (LLVMTranslationWarning -> IO ())
-> [LLVMTranslationWarning] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ LLVMTranslationWarning -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning [LLVMTranslationWarning]
warns
           case (CFG LLVM blocks init ret -> CtxRepr init
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> CtxRepr init
cfgArgTypes CFG LLVM blocks init ret
anyCfg, CFG LLVM blocks init ret -> TypeRepr ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> TypeRepr ret
cfgReturnType CFG LLVM blocks init ret
anyCfg) of
             (CtxRepr init
Empty, TypeRepr ret
UnitRepr) -> RegEntry sym ret -> ()
RegEntry sym ret -> RegValue sym ret
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue (RegEntry sym ret -> ())
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (RegEntry sym ret)
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CFG LLVM blocks init ret
-> RegMap sym init
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (RegEntry sym ret)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) sym p rtp
       (a :: Ctx CrucibleType) (r :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> RegMap sym init
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
callCFG CFG LLVM blocks init ret
anyCfg RegMap sym init
RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap
             (CtxRepr init, TypeRepr ret)
_ -> String
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
String
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> String
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ShowS
forall a. Show a => a -> String
show String
stepName, String
"should take no arguments and return void"]
         Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
Nothing -> String
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
String
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> String
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"Could not find step function named", ShowS
forall a. Show a => a -> String
show String
stepName]

       -- Assert that the trigger functions were called exactly once iff the
       -- associated guard condition was true.
       -- See Note [Global variables for trigger functions].
       [(String, GlobalVar 'NatType, Pred sym)]
-> ((String, GlobalVar 'NatType, Pred sym)
    -> OverrideSim
         (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(String, GlobalVar 'NatType, Pred sym)]
triggerGlobals (((String, GlobalVar 'NatType, Pred sym)
  -> OverrideSim
       (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> ((String, GlobalVar 'NatType, Pred sym)
    -> OverrideSim
         (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ \(String
nm, GlobalVar 'NatType
gv, Pred sym
guard) ->
         do SymNat sym
expectedCount <- IO (SymNat sym)
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (SymNat sym)
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymNat sym)
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (SymNat sym))
-> IO (SymNat sym)
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (SymNat sym)
forall a b. (a -> b) -> a -> b
$ do
              SymNat sym
one  <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
1
              SymNat sym
zero <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0
              sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym Pred sym
guard SymNat sym
one SymNat sym
zero
            SymNat sym
actualCount <- GlobalVar 'NatType
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (RegValue sym 'NatType)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar 'NatType
gv
            Pred sym
eq <- IO (Pred sym)
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (Pred sym)
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Pred sym)
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (Pred sym))
-> IO (Pred sym)
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
expectedCount SymNat sym
actualCount
            (SymAnnotation sym BaseBoolType
ann, Pred sym
eq') <- IO (SymAnnotation sym BaseBoolType, Pred sym)
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (SymAnnotation sym BaseBoolType, Pred sym)
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SymAnnotation sym BaseBoolType, Pred sym)
 -> OverrideSim
      (Crux sym)
      sym
      LLVM
      (RegEntry sym Mem)
      EmptyCtx
      Mem
      (SymAnnotation sym BaseBoolType, Pred sym))
-> IO (SymAnnotation sym BaseBoolType, Pred sym)
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (SymAnnotation sym BaseBoolType, Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> IO (SymAnnotation sym BaseBoolType, Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym Pred sym
eq
            let shortmsg :: String
shortmsg = String
"Trigger guard equality condition: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm
            let longmsg :: String
longmsg  = Doc Any -> String
forall a. Show a => a -> String
show (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
printSymExpr Pred sym
eq')
            let rsn :: SimErrorReason
rsn      = String -> String -> SimErrorReason
AssertFailureSimError String
shortmsg String
longmsg
            IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
              (IO ()
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs)
              ((Map (BoolAnn sym) (VerifierAssertion sym)
  -> Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO ())
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a b. (a -> b) -> a -> b
$ BoolAnn sym
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
ann)
              (VerifierAssertion sym
 -> Map (BoolAnn sym) (VerifierAssertion sym)
 -> Map (BoolAnn sym) (VerifierAssertion sym))
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ TriggersInvokedCorrespondingly sym -> VerifierAssertion sym
forall sym.
TriggersInvokedCorrespondingly sym -> VerifierAssertion sym
Log.TriggersInvokedCorrespondinglyAssertion
              (TriggersInvokedCorrespondingly sym -> VerifierAssertion sym)
-> TriggersInvokedCorrespondingly sym -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ ProgramLoc
-> String
-> SymNat sym
-> SymNat sym
-> TriggersInvokedCorrespondingly sym
forall sym.
ProgramLoc
-> String
-> SymNat sym
-> SymNat sym
-> TriggersInvokedCorrespondingly sym
Log.TriggersInvokedCorrespondingly ProgramLoc
dummyLoc String
nm SymNat sym
expectedCount SymNat sym
actualCount
            SimCtxt Crux sym LLVM
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimCtxt Crux sym LLVM
simctx ((forall {bak}.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
              IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a.
IO a
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ()
 -> OverrideSim
      (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ())
-> IO ()
-> OverrideSim
     (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem ()
forall a b. (a -> b) -> a -> b
$ bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
eq' (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
dummyLoc SimErrorReason
rsn))

       -- return the final state of the memory
       GlobalVar Mem
-> OverrideSim
     (Crux sym)
     sym
     LLVM
     (RegEntry sym Mem)
     EmptyCtx
     Mem
     (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
memVar

-- | Given a bisimulation proof bundle and an empty initial state,
--   populate the global ring-buffer variables with abstract state
--   values, and write the abstract values of the external stream
--   values into their proper locations.
setupPrestate ::
  IsSymBackend sym bak =>
  HasPtrWidth wptr =>
  HasLLVMAnn sym =>
  (?memOpts :: MemOptions) =>
  (?lc :: TypeContext) =>

  bak ->
  MemImpl sym ->
  CW4.BisimulationProofBundle sym ->
  IO (MemImpl sym)
setupPrestate :: forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, ?lc::TypeContext) =>
bak
-> MemImpl sym -> BisimulationProofBundle sym -> IO (MemImpl sym)
setupPrestate bak
bak MemImpl sym
mem0 BisimulationProofBundle sym
prfbundle =
  do MemImpl sym
mem' <- (MemImpl sym -> (Int, Some Type, [XExpr sym]) -> IO (MemImpl sym))
-> MemImpl sym
-> [(Int, Some Type, [XExpr sym])]
-> IO (MemImpl sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM MemImpl sym -> (Int, Some Type, [XExpr sym]) -> IO (MemImpl sym)
setupStreamState MemImpl sym
mem0 (BisimulationProofState sym -> [(Int, Some Type, [XExpr sym])]
forall sym.
BisimulationProofState sym -> [(Int, Some Type, [XExpr sym])]
CW4.streamState (BisimulationProofBundle sym -> BisimulationProofState sym
forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
CW4.preStreamState BisimulationProofBundle sym
prfbundle))
     (MemImpl sym -> (String, Some Type, XExpr sym) -> IO (MemImpl sym))
-> MemImpl sym
-> [(String, Some Type, XExpr sym)]
-> IO (MemImpl sym)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM MemImpl sym -> (String, Some Type, XExpr sym) -> IO (MemImpl sym)
setupExternalInput MemImpl sym
mem' (BisimulationProofBundle sym -> [(String, Some Type, XExpr sym)]
forall sym.
BisimulationProofBundle sym -> [(String, Some Type, XExpr sym)]
CW4.externalInputs BisimulationProofBundle sym
prfbundle)

 where
   sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak

   sizeTStorage :: StorageType
   sizeTStorage :: StorageType
sizeTStorage = Bytes -> StorageType
bitvectorType (Integer -> Bytes
forall a. Integral a => a -> Bytes
bitsToBytes (NatRepr wptr -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth))

   setupExternalInput :: MemImpl sym -> (String, Some Type, XExpr sym) -> IO (MemImpl sym)
setupExternalInput MemImpl sym
mem (String
nm, Some Type x
ctp, XExpr sym
v) =
     do -- Compute LLVM/Crucible type information from the Copilot type
        let memTy :: MemType
memTy      = DataLayout -> Type x -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) Type x
ctp
        let typeAlign :: Alignment
typeAlign  = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memTy
        StorageType
stType <- MemType -> IO StorageType
forall (m :: * -> *) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
memTy
        Some TypeRepr x
typeRepr <- Some TypeRepr -> IO (Some TypeRepr)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
memTy TypeRepr tp -> Some TypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr
Some)

        -- resolve the global variable to a pointers
        LLVMPointer sym wptr
ptrVal <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (String -> Symbol
L.Symbol String
nm)

        -- write the value into the global
        RegValue sym x
regVal <- sym -> XExpr sym -> TypeRepr x -> IO (RegValue sym x)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> XExpr sym -> TypeRepr tp -> IO (RegValue sym tp)
copilotExprToRegValue sym
sym XExpr sym
v TypeRepr x
typeRepr
        bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr x
-> StorageType
-> Alignment
-> RegValue sym x
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
ptrVal TypeRepr x
typeRepr StorageType
stType Alignment
typeAlign RegValue sym x
regVal

   setupStreamState :: MemImpl sym -> (Int, Some Type, [XExpr sym]) -> IO (MemImpl sym)
setupStreamState MemImpl sym
mem (Int
nm, Some Type x
ctp, [XExpr sym]
vs) =
     do -- TODO, should get these from somewhere inside copilot instead of building these names directly
        let idxName :: String
idxName = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_idx"
        let bufName :: String
bufName = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nm
        let buflen :: Integer
buflen  = [XExpr sym] -> Integer
forall i a. Num i => [a] -> i
genericLength [XExpr sym]
vs :: Integer

        -- Compute LLVM/Crucible type information from the Copilot type
        let memTy :: MemType
memTy      = DataLayout -> Type x -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) Type x
ctp
        let typeLen :: Bytes
typeLen    = DataLayout -> MemType -> Bytes
memTypeSize (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memTy
        let typeAlign :: Alignment
typeAlign  = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memTy
        StorageType
stType <- MemType -> IO StorageType
forall (m :: * -> *) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
memTy
        Some TypeRepr x
typeRepr <- Some TypeRepr -> IO (Some TypeRepr)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
memTy TypeRepr tp -> Some TypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr
Some)

        -- Resolve the global names into base pointers
        LLVMPointer sym wptr
idxPtr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (String -> Symbol
L.Symbol String
idxName)
        LLVMPointer sym wptr
bufPtr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (String -> Symbol
L.Symbol String
bufName)

        -- Create a fresh index value in the proper range
        SymExpr sym (BaseBVType wptr)
idxVal <- sym
-> SolverSymbol
-> NatRepr wptr
-> Maybe Natural
-> Maybe Natural
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym
-> SolverSymbol
-> NatRepr w
-> Maybe Natural
-> Maybe Natural
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsSymExprBuilder sym, 1 <= w) =>
sym
-> SolverSymbol
-> NatRepr w
-> Maybe Natural
-> Maybe Natural
-> IO (SymBV sym w)
freshBoundedBV sym
sym (String -> SolverSymbol
safeSymbol String
idxName) ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth
                     (Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
0) (Natural -> Maybe Natural
forall a. a -> Maybe a
Just (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
buflen Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))
        LLVMPointer sym wptr
idxVal' <- sym -> SymExpr sym (BaseBVType wptr) -> IO (LLVMPtr sym wptr)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType wptr)
idxVal

        -- store the index value in the correct location
        let sizeTAlign :: Alignment
sizeTAlign = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) (Natural -> MemType
IntType (NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth))
        MemImpl sym
mem' <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr (LLVMPointerType wptr)
-> StorageType
-> Alignment
-> LLVMPtr sym wptr
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
idxPtr (NatRepr wptr -> TypeRepr (LLVMPointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth) StorageType
sizeTStorage Alignment
sizeTAlign LLVMPtr sym wptr
LLVMPointer sym wptr
idxVal'

        SymExpr sym (BaseBVType wptr)
buflen'  <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth Integer
buflen)
        SymExpr sym (BaseBVType wptr)
typeLen' <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger Bytes
typeLen))

        -- Write each value of the stream ring buffer into its correct location
        (StateT (MemImpl sym) IO () -> MemImpl sym -> IO (MemImpl sym))
-> MemImpl sym -> StateT (MemImpl sym) IO () -> IO (MemImpl sym)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (MemImpl sym) IO () -> MemImpl sym -> IO (MemImpl sym)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT MemImpl sym
mem' (StateT (MemImpl sym) IO () -> IO (MemImpl sym))
-> StateT (MemImpl sym) IO () -> IO (MemImpl sym)
forall a b. (a -> b) -> a -> b
$
          [(XExpr sym, Integer)]
-> ((XExpr sym, Integer) -> StateT (MemImpl sym) IO ())
-> StateT (MemImpl sym) IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([XExpr sym] -> [Integer] -> [(XExpr sym, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [XExpr sym]
vs [Integer
0 ..]) (((XExpr sym, Integer) -> StateT (MemImpl sym) IO ())
 -> StateT (MemImpl sym) IO ())
-> ((XExpr sym, Integer) -> StateT (MemImpl sym) IO ())
-> StateT (MemImpl sym) IO ()
forall a b. (a -> b) -> a -> b
$ \(XExpr sym
v,Integer
i) ->
            do LLVMPointer sym wptr
ptrVal <- IO (LLVMPointer sym wptr)
-> StateT (MemImpl sym) IO (LLVMPointer sym wptr)
forall (m :: * -> *) a. Monad m => m a -> StateT (MemImpl sym) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (LLVMPointer sym wptr)
 -> StateT (MemImpl sym) IO (LLVMPointer sym wptr))
-> IO (LLVMPointer sym wptr)
-> StateT (MemImpl sym) IO (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$
                 do SymExpr sym (BaseBVType wptr)
x1 <- sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymExpr sym (BaseBVType wptr)
idxVal (SymExpr sym (BaseBVType wptr)
 -> IO (SymExpr sym (BaseBVType wptr)))
-> IO (SymExpr sym (BaseBVType wptr))
-> IO (SymExpr sym (BaseBVType wptr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth Integer
i)
                    SymExpr sym (BaseBVType wptr)
x2 <- sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvUrem sym
sym SymExpr sym (BaseBVType wptr)
x1 SymExpr sym (BaseBVType wptr)
buflen'
                    SymExpr sym (BaseBVType wptr)
x3 <- sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType wptr)
x2 SymExpr sym (BaseBVType wptr)
typeLen'
                    sym
-> NatRepr wptr
-> LLVMPtr sym wptr
-> SymExpr sym (BaseBVType wptr)
-> IO (LLVMPtr sym wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
ptrAdd sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth LLVMPtr sym wptr
LLVMPointer sym wptr
bufPtr SymExpr sym (BaseBVType wptr)
x3

               RegValue sym x
regVal <- IO (RegValue sym x) -> StateT (MemImpl sym) IO (RegValue sym x)
forall (m :: * -> *) a. Monad m => m a -> StateT (MemImpl sym) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (RegValue sym x) -> StateT (MemImpl sym) IO (RegValue sym x))
-> IO (RegValue sym x) -> StateT (MemImpl sym) IO (RegValue sym x)
forall a b. (a -> b) -> a -> b
$ sym -> XExpr sym -> TypeRepr x -> IO (RegValue sym x)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> XExpr sym -> TypeRepr tp -> IO (RegValue sym tp)
copilotExprToRegValue sym
sym XExpr sym
v TypeRepr x
typeRepr
               (MemImpl sym -> IO ((), MemImpl sym)) -> StateT (MemImpl sym) IO ()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((MemImpl sym -> IO ((), MemImpl sym))
 -> StateT (MemImpl sym) IO ())
-> (MemImpl sym -> IO ((), MemImpl sym))
-> StateT (MemImpl sym) IO ()
forall a b. (a -> b) -> a -> b
$ \MemImpl sym
m ->
                 do MemImpl sym
m' <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr x
-> StorageType
-> Alignment
-> RegValue sym x
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> TypeRepr tp
-> StorageType
-> Alignment
-> RegValue sym tp
-> IO (MemImpl sym)
doStore bak
bak MemImpl sym
m LLVMPtr sym wptr
LLVMPointer sym wptr
ptrVal TypeRepr x
typeRepr StorageType
stType Alignment
typeAlign RegValue sym x
regVal
                    ((), MemImpl sym) -> IO ((), MemImpl sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((),MemImpl sym
m')

-- | Given a memory image and a "proof state", assert that the global values
--   for each stream ring buffer have values that correspond to the given
--   stream state. This collection of assertions defines the bisimulation
--   relation.
assertStateRelation ::
  IsSymBackend sym bak =>
  Log.Logs msgs =>
  HasPtrWidth wptr =>
  HasLLVMAnn sym =>
  (?memOpts :: MemOptions) =>
  (?lc :: TypeContext) =>
  bak ->
  CopilotLogRefs sym ->
  MemImpl sym ->
  Log.StateRelationStep ->
  CW4.BisimulationProofState sym ->
  IO ()
assertStateRelation :: forall sym bak msgs (wptr :: Natural).
(IsSymBackend sym bak, Logs msgs, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions, ?lc::TypeContext) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> StateRelationStep
-> BisimulationProofState sym
-> IO ()
assertStateRelation bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem StateRelationStep
stateRelStep BisimulationProofState sym
prfst =
  -- For each stream in the proof state, assert that the
  -- generated ring buffer global contains the corresponding
  -- values.
  [(Int, Some Type, [XExpr sym])]
-> ((Int, Some Type, [XExpr sym]) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (BisimulationProofState sym -> [(Int, Some Type, [XExpr sym])]
forall sym.
BisimulationProofState sym -> [(Int, Some Type, [XExpr sym])]
CW4.streamState BisimulationProofState sym
prfst) (Int, Some Type, [XExpr sym]) -> IO ()
assertStreamState

 where
   sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak

   sizeTStorage :: StorageType
   sizeTStorage :: StorageType
sizeTStorage = Bytes -> StorageType
bitvectorType (Integer -> Bytes
forall a. Integral a => a -> Bytes
bitsToBytes (NatRepr wptr -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth))

   assertStreamState :: (Int, Some Type, [XExpr sym]) -> IO ()
assertStreamState (Int
nm, Some Type x
ctp, [XExpr sym]
vs) =
     do -- TODO, should get these from somewhere inside copilot instead of building these names directly
        let idxName :: String
idxName = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_idx"
        let bufName :: String
bufName = String
"s" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nm
        let buflen :: Integer
buflen  = [XExpr sym] -> Integer
forall i a. Num i => [a] -> i
genericLength [XExpr sym]
vs :: Integer

        -- Compute LLVM/Crucible type information from the Copilot type
        let memTy :: MemType
memTy      = DataLayout -> Type x -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) Type x
ctp
        let typeLen :: Bytes
typeLen    = DataLayout -> MemType -> Bytes
memTypeSize (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memTy
        let typeAlign :: Alignment
typeAlign  = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memTy
        StorageType
stType <- MemType -> IO StorageType
forall (m :: * -> *) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
memTy
        Some TypeRepr x
typeRepr <- Some TypeRepr -> IO (Some TypeRepr)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
memTy TypeRepr tp -> Some TypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr
Some)

        -- Resolve the global names into base pointers
        LLVMPointer sym wptr
idxPtr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (String -> Symbol
L.Symbol String
idxName)
        LLVMPointer sym wptr
bufPtr <- bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasCallStack) =>
bak -> MemImpl sym -> Symbol -> IO (LLVMPtr sym wptr)
doResolveGlobal bak
bak MemImpl sym
mem (String -> Symbol
L.Symbol String
bufName)

        -- read the value of the ring buffer index
        let sizeTAlign :: Alignment
sizeTAlign = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) (Natural -> MemType
IntType (NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth))
        (BoolAnn sym
bannIdxVal, SymExpr sym BaseBoolType
pIdxVal, LLVMPtr sym wptr
idxVal) <-
          bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr (LLVMPointerType wptr)
-> Alignment
-> IO (BoolAnn sym, SymExpr sym BaseBoolType, LLVMPtr sym wptr)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (BoolAnn sym, Pred sym, RegValue sym tp)
doLoadWithAnn bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
idxPtr StorageType
sizeTStorage (NatRepr wptr -> TypeRepr (LLVMPointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth) Alignment
sizeTAlign
        SymExpr sym (BaseBVType wptr)
idxVal' <- bak -> LLVMPtr sym wptr -> IO (SymExpr sym (BaseBVType wptr))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak LLVMPtr sym wptr
idxVal
        ProgramLoc
locIdxVal <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
        IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs)
          ((Map (BoolAnn sym) (VerifierAssertion sym)
  -> Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO ())
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a b. (a -> b) -> a -> b
$ BoolAnn sym
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BoolAnn sym
bannIdxVal
          (VerifierAssertion sym
 -> Map (BoolAnn sym) (VerifierAssertion sym)
 -> Map (BoolAnn sym) (VerifierAssertion sym))
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ RingBufferIndexLoad sym -> VerifierAssertion sym
forall sym. RingBufferIndexLoad sym -> VerifierAssertion sym
Log.RingBufferIndexLoadAssertion
          (RingBufferIndexLoad sym -> VerifierAssertion sym)
-> RingBufferIndexLoad sym -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ sym
-> StateRelationStep
-> ProgramLoc
-> Text
-> SymExpr sym BaseBoolType
-> RingBufferIndexLoad sym
forall sym.
sym
-> StateRelationStep
-> ProgramLoc
-> Text
-> Pred sym
-> RingBufferIndexLoad sym
Log.RingBufferIndexLoad sym
sym StateRelationStep
stateRelStep ProgramLoc
locIdxVal (String -> Text
Text.pack String
idxName) SymExpr sym BaseBoolType
pIdxVal

        SymExpr sym (BaseBVType wptr)
buflen'  <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth Integer
buflen)
        SymExpr sym (BaseBVType wptr)
typeLen' <- sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger Bytes
typeLen))

        -- For each value in the stream description, read a corresponding value from
        -- memory and assert that they are equal.
        [(XExpr sym, Integer)] -> ((XExpr sym, Integer) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([XExpr sym] -> [Integer] -> [(XExpr sym, Integer)]
forall a b. [a] -> [b] -> [(a, b)]
zip [XExpr sym]
vs [Integer
0 ..]) (((XExpr sym, Integer) -> IO ()) -> IO ())
-> ((XExpr sym, Integer) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(XExpr sym
v,Integer
i) ->
          do LLVMPointer sym wptr
ptrVal <-
               do SymExpr sym (BaseBVType wptr)
x1 <- sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymExpr sym (BaseBVType wptr)
idxVal' (SymExpr sym (BaseBVType wptr)
 -> IO (SymExpr sym (BaseBVType wptr)))
-> IO (SymExpr sym (BaseBVType wptr))
-> IO (SymExpr sym (BaseBVType wptr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr wptr -> BV wptr -> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth (NatRepr wptr -> Integer -> BV wptr
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth Integer
i)
                  SymExpr sym (BaseBVType wptr)
x2 <- sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvUrem sym
sym SymExpr sym (BaseBVType wptr)
x1 SymExpr sym (BaseBVType wptr)
buflen'
                  SymExpr sym (BaseBVType wptr)
x3 <- sym
-> SymExpr sym (BaseBVType wptr)
-> SymExpr sym (BaseBVType wptr)
-> IO (SymExpr sym (BaseBVType wptr))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMul sym
sym SymExpr sym (BaseBVType wptr)
x2 SymExpr sym (BaseBVType wptr)
typeLen'
                  sym
-> NatRepr wptr
-> LLVMPtr sym wptr
-> SymExpr sym (BaseBVType wptr)
-> IO (LLVMPtr sym wptr)
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
ptrAdd sym
sym ?ptrWidth::NatRepr wptr
NatRepr wptr
?ptrWidth LLVMPtr sym wptr
LLVMPointer sym wptr
bufPtr SymExpr sym (BaseBVType wptr)
x3

             (BoolAnn sym
bannv', SymExpr sym BaseBoolType
pv', RegValue sym x
v') <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr x
-> Alignment
-> IO (BoolAnn sym, SymExpr sym BaseBoolType, RegValue sym x)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (BoolAnn sym, Pred sym, RegValue sym tp)
doLoadWithAnn bak
bak MemImpl sym
mem LLVMPtr sym wptr
LLVMPointer sym wptr
ptrVal StorageType
stType TypeRepr x
typeRepr Alignment
typeAlign
             ProgramLoc
locv' <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
             let bufNameT :: Text
bufNameT = String -> Text
Text.pack String
bufName
             IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs)
               ((Map (BoolAnn sym) (VerifierAssertion sym)
  -> Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO ())
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a b. (a -> b) -> a -> b
$ BoolAnn sym
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BoolAnn sym
bannv'
               (VerifierAssertion sym
 -> Map (BoolAnn sym) (VerifierAssertion sym)
 -> Map (BoolAnn sym) (VerifierAssertion sym))
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ SomeSome (RingBufferLoad sym) -> VerifierAssertion sym
forall sym. SomeSome (RingBufferLoad sym) -> VerifierAssertion sym
Log.RingBufferLoadAssertion
               (SomeSome (RingBufferLoad sym) -> VerifierAssertion sym)
-> SomeSome (RingBufferLoad sym) -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ RingBufferLoad sym x x -> SomeSome (RingBufferLoad sym)
forall {j} {k} (f :: j -> k -> *) (x :: j) (y :: k).
f x y -> SomeSome f
Log.SomeSome
               (RingBufferLoad sym x x -> SomeSome (RingBufferLoad sym))
-> RingBufferLoad sym x x -> SomeSome (RingBufferLoad sym)
forall a b. (a -> b) -> a -> b
$ sym
-> StateRelationStep
-> ProgramLoc
-> Text
-> Integer
-> Integer
-> Type x
-> TypeRepr x
-> SymExpr sym BaseBoolType
-> RingBufferLoad sym x x
forall sym copilotType (crucibleType :: CrucibleType).
sym
-> StateRelationStep
-> ProgramLoc
-> Text
-> Integer
-> Integer
-> Type copilotType
-> TypeRepr crucibleType
-> Pred sym
-> RingBufferLoad sym copilotType crucibleType
Log.RingBufferLoad sym
sym StateRelationStep
stateRelStep ProgramLoc
locv' Text
bufNameT Integer
i Integer
buflen Type x
ctp TypeRepr x
typeRepr SymExpr sym BaseBoolType
pv'
             SymExpr sym BaseBoolType
eq <- bak
-> CopilotLogRefs sym
-> MemImpl sym
-> Type x
-> XExpr sym
-> TypeRepr x
-> RegValue sym x
-> IO (SymExpr sym BaseBoolType)
forall sym bak (tp :: CrucibleType) a (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> Type a
-> XExpr sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (Pred sym)
computeEqualVals bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem Type x
ctp XExpr sym
v TypeRepr x
typeRepr RegValue sym x
v'
             (SymAnnotation sym BaseBoolType
ann, SymExpr sym BaseBoolType
eq') <- sym
-> SymExpr sym BaseBoolType
-> IO (SymAnnotation sym BaseBoolType, SymExpr sym BaseBoolType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym SymExpr sym BaseBoolType
eq
             let shortmsg :: String
shortmsg = String
"State equality condition: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" index value " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
             let longmsg :: String
longmsg  = Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym BaseBoolType -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym BaseBoolType
eq')
             let rsn :: SimErrorReason
rsn      = String -> String -> SimErrorReason
AssertFailureSimError String
shortmsg String
longmsg
             let loc :: ProgramLoc
loc      = FunctionName -> Position -> ProgramLoc
mkProgramLoc FunctionName
"<>" Position
InternalPos
             IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs)
               ((Map (BoolAnn sym) (VerifierAssertion sym)
  -> Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO ())
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a b. (a -> b) -> a -> b
$ BoolAnn sym
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
ann)
               (VerifierAssertion sym
 -> Map (BoolAnn sym) (VerifierAssertion sym)
 -> Map (BoolAnn sym) (VerifierAssertion sym))
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ SomeSome (StreamValueEquality sym) -> VerifierAssertion sym
forall sym.
SomeSome (StreamValueEquality sym) -> VerifierAssertion sym
Log.StreamValueEqualityAssertion
               (SomeSome (StreamValueEquality sym) -> VerifierAssertion sym)
-> SomeSome (StreamValueEquality sym) -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ StreamValueEquality sym x x -> SomeSome (StreamValueEquality sym)
forall {j} {k} (f :: j -> k -> *) (x :: j) (y :: k).
f x y -> SomeSome f
Log.SomeSome
               (StreamValueEquality sym x x -> SomeSome (StreamValueEquality sym))
-> StreamValueEquality sym x x
-> SomeSome (StreamValueEquality sym)
forall a b. (a -> b) -> a -> b
$ sym
-> StateRelationStep
-> ProgramLoc
-> Text
-> Integer
-> Integer
-> Type x
-> XExpr sym
-> TypeRepr x
-> RegValue sym x
-> StreamValueEquality sym x x
forall sym copilotType (crucibleType :: CrucibleType).
sym
-> StateRelationStep
-> ProgramLoc
-> Text
-> Integer
-> Integer
-> Type copilotType
-> XExpr sym
-> TypeRepr crucibleType
-> RegValue sym crucibleType
-> StreamValueEquality sym copilotType crucibleType
Log.StreamValueEquality sym
sym StateRelationStep
stateRelStep ProgramLoc
loc Text
bufNameT Integer
i Integer
buflen Type x
ctp XExpr sym
v TypeRepr x
typeRepr RegValue sym x
v'
             bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred SymExpr sym BaseBoolType
eq' (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
rsn))

        () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Translate the @XExpr@ values from the "Copilot.Theorem.What4" module into
--   Crucible @RegValue@s suitable for injection into the Crucible simulator.
copilotExprToRegValue :: forall sym tp.
  IsSymInterface sym =>
  sym ->
  CW4.XExpr sym ->
  TypeRepr tp ->
  IO (RegValue sym tp)
copilotExprToRegValue :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> XExpr sym -> TypeRepr tp -> IO (RegValue sym tp)
copilotExprToRegValue sym
sym = XExpr sym -> TypeRepr tp -> IO (RegValue sym tp)
forall (tp' :: CrucibleType).
XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')
loop
  where
    loop :: forall tp'. CW4.XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')

    loop :: forall (tp' :: CrucibleType).
XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')
loop (CW4.XBool SymExpr sym BaseBoolType
b) (LLVMPointerRepr NatRepr w
w) | Just w :~: 1
Refl <- NatRepr w -> NatRepr 1 -> Maybe (w :~: 1)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) =
      sym -> SymExpr sym (BaseBVType 1) -> IO (LLVMPtr sym 1)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym (BaseBVType 1) -> IO (LLVMPointer sym 1))
-> IO (SymExpr sym (BaseBVType 1)) -> IO (LLVMPointer sym 1)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym BaseBoolType
-> NatRepr 1
-> IO (SymExpr sym (BaseBVType 1))
forall (w :: Natural).
(1 <= w) =>
sym -> SymExpr sym BaseBoolType -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
predToBV sym
sym SymExpr sym BaseBoolType
b NatRepr 1
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    loop (CW4.XBool SymExpr sym BaseBoolType
b) (LLVMPointerRepr NatRepr w
w) | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) =
      sym -> SymExpr sym (BaseBVType 8) -> IO (LLVMPtr sym 8)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym (BaseBVType 8) -> IO (LLVMPointer sym 8))
-> IO (SymExpr sym (BaseBVType 8)) -> IO (LLVMPointer sym 8)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym BaseBoolType
-> NatRepr 8
-> IO (SymExpr sym (BaseBVType 8))
forall (w :: Natural).
(1 <= w) =>
sym -> SymExpr sym BaseBoolType -> NatRepr w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
predToBV sym
sym SymExpr sym BaseBoolType
b NatRepr 8
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    loop (CW4.XInt8 SymExpr sym (BaseBVType 8)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) =
      sym -> SymExpr sym (BaseBVType 8) -> IO (LLVMPtr sym 8)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 8)
x
    loop (CW4.XInt16 SymExpr sym (BaseBVType 16)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 16
Refl <- NatRepr w -> NatRepr 16 -> Maybe (w :~: 16)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16) =
      sym -> SymExpr sym (BaseBVType 16) -> IO (LLVMPtr sym 16)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 16)
x
    loop (CW4.XInt32 SymExpr sym (BaseBVType 32)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 32
Refl <- NatRepr w -> NatRepr 32 -> Maybe (w :~: 32)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32) =
      sym -> SymExpr sym (BaseBVType 32) -> IO (LLVMPtr sym 32)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 32)
x
    loop (CW4.XInt64 SymExpr sym (BaseBVType 64)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 64
Refl <- NatRepr w -> NatRepr 64 -> Maybe (w :~: 64)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64) =
      sym -> SymExpr sym (BaseBVType 64) -> IO (LLVMPtr sym 64)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 64)
x
    loop (CW4.XWord8 SymExpr sym (BaseBVType 8)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) =
      sym -> SymExpr sym (BaseBVType 8) -> IO (LLVMPtr sym 8)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 8)
x
    loop (CW4.XWord16 SymExpr sym (BaseBVType 16)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 16
Refl <- NatRepr w -> NatRepr 16 -> Maybe (w :~: 16)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16) =
      sym -> SymExpr sym (BaseBVType 16) -> IO (LLVMPtr sym 16)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 16)
x
    loop (CW4.XWord32 SymExpr sym (BaseBVType 32)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 32
Refl <- NatRepr w -> NatRepr 32 -> Maybe (w :~: 32)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32) =
      sym -> SymExpr sym (BaseBVType 32) -> IO (LLVMPtr sym 32)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 32)
x
    loop (CW4.XWord64 SymExpr sym (BaseBVType 64)
x) (LLVMPointerRepr NatRepr w
w) | Just w :~: 64
Refl <- NatRepr w -> NatRepr 64 -> Maybe (w :~: 64)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64) =
      sym -> SymExpr sym (BaseBVType 64) -> IO (LLVMPtr sym 64)
forall sym (w :: Natural).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymExpr sym (BaseBVType 64)
x

    loop (CW4.XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
x)  (FloatRepr FloatInfoRepr flt
SingleFloatRepr) = SymExpr sym (SymInterpretedFloatType sym SingleFloat)
-> IO (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym (SymInterpretedFloatType sym SingleFloat)
x
    loop (CW4.XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
x) (FloatRepr FloatInfoRepr flt
DoubleFloatRepr) = SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
-> IO (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
x

    loop (CW4.XEmptyArray Type t
_ctp) (VectorRepr TypeRepr tp1
_tpr) =
      Vector (RegValue sym tp1) -> IO (Vector (RegValue sym tp1))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Vector (RegValue sym tp1)
forall a. Vector a
V.empty
    loop (CW4.XArray Vector n (XExpr sym)
xs) (VectorRepr TypeRepr tp1
tpr) =
      Int
-> (Int -> IO (RegValue sym tp1)) -> IO (Vector (RegValue sym tp1))
forall (m :: * -> *) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM (Vector n (XExpr sym) -> Int
forall (n :: Natural) a. Vector n a -> Int
PVec.lengthInt Vector n (XExpr sym)
xs) (\Int
i -> XExpr sym -> TypeRepr tp1 -> IO (RegValue sym tp1)
forall (tp' :: CrucibleType).
XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')
loop (Int -> Vector n (XExpr sym) -> XExpr sym
forall (n :: Natural) a. Int -> Vector n a -> a
PVec.elemAtUnsafe Int
i Vector n (XExpr sym)
xs) TypeRepr tp1
tpr)
    loop (CW4.XStruct [XExpr sym]
xs) (StructRepr CtxRepr ctx
ctx) =
      (forall (tp :: CrucibleType).
 Index ctx tp -> TypeRepr tp -> IO (RegValue' sym tp))
-> CtxRepr ctx -> IO (Assignment (RegValue' sym) ctx)
forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *)
       (g :: k -> *).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
Ctx.traverseWithIndex
        (\Index ctx tp
i TypeRepr tp
tpr -> RegValue sym tp -> RegValue' sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (RegValue sym tp -> RegValue' sym tp)
-> IO (RegValue sym tp) -> IO (RegValue' sym tp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> XExpr sym -> TypeRepr tp -> IO (RegValue sym tp)
forall (tp' :: CrucibleType).
XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')
loop ([XExpr sym]
xs [XExpr sym] -> Int -> XExpr sym
forall a. HasCallStack => [a] -> Int -> a
!! Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index ctx tp
i) TypeRepr tp
tpr)
        CtxRepr ctx
ctx

    loop XExpr sym
x TypeRepr tp'
tpr =
      String -> IO (RegValue sym tp')
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (RegValue sym tp'))
-> String -> IO (RegValue sym tp')
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
"Mismatch between Copilot value and crucible value", XExpr sym -> String
forall a. Show a => a -> String
show XExpr sym
x, TypeRepr tp' -> String
forall a. Show a => a -> String
show TypeRepr tp'
tpr]


-- | Given an @XExpr@ from from the "Copilot.Theorem.What4" module, and
--   a Crucible @RegValue@ which is expected to match, compute an equality
--   predicate between the values.  The Crucible values may be pointers,
--   requiring us to resolve the indirection through memory; this is necessary
--   for array and struct values, but would also work for scalars.
computeEqualVals :: forall sym bak tp a wptr.
  IsSymBackend sym bak =>
  HasPtrWidth wptr =>
  HasLLVMAnn sym =>
  (?lc :: TypeContext) =>
  (?memOpts :: MemOptions) =>
  bak ->
  CopilotLogRefs sym ->
  MemImpl sym ->
  Type a ->
  CW4.XExpr sym ->
  TypeRepr tp ->
  RegValue sym tp ->
  IO (Pred sym)
computeEqualVals :: forall sym bak (tp :: CrucibleType) a (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
bak
-> CopilotLogRefs sym
-> MemImpl sym
-> Type a
-> XExpr sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (Pred sym)
computeEqualVals bak
bak CopilotLogRefs sym
clRefs MemImpl sym
mem = Type a
-> XExpr sym -> TypeRepr tp -> RegValue sym tp -> IO (Pred sym)
forall (tp' :: CrucibleType) a'.
Type a'
-> XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
loop
  where
    sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak

    loop :: forall tp' a'. Type a' -> CW4.XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
    loop :: forall (tp' :: CrucibleType) a'.
Type a'
-> XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
loop Type a'
Bool (CW4.XBool Pred sym
b) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 1
Refl <- NatRepr w -> NatRepr 1 -> Maybe (w :~: 1)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) =
      sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym
sym Pred sym
b (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymExpr sym (BaseBVType 1) -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym (SymExpr sym (BaseBVType 1) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 1)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 1 -> IO (SymExpr sym (BaseBVType 1))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 1
v
    loop Type a'
Bool (CW4.XBool Pred sym
b) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) =
      sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym
sym Pred sym
b (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymExpr sym (BaseBVType 8) -> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym (SymExpr sym (BaseBVType 8) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 8)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 8 -> IO (SymExpr sym (BaseBVType 8))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 8
v
    loop Type a'
Int8 (CW4.XInt8 SymExpr sym (BaseBVType 8)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) =
      sym
-> SymExpr sym (BaseBVType 8)
-> SymExpr sym (BaseBVType 8)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 8)
x (SymExpr sym (BaseBVType 8) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 8)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 8 -> IO (SymExpr sym (BaseBVType 8))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 8
v
    loop Type a'
Int16 (CW4.XInt16 SymExpr sym (BaseBVType 16)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 16
Refl <- NatRepr w -> NatRepr 16 -> Maybe (w :~: 16)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16) =
      sym
-> SymExpr sym (BaseBVType 16)
-> SymExpr sym (BaseBVType 16)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 16)
x (SymExpr sym (BaseBVType 16) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 16)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 16 -> IO (SymExpr sym (BaseBVType 16))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 16
v
    loop Type a'
Int32 (CW4.XInt32 SymExpr sym (BaseBVType 32)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 32
Refl <- NatRepr w -> NatRepr 32 -> Maybe (w :~: 32)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32) =
      sym
-> SymExpr sym (BaseBVType 32)
-> SymExpr sym (BaseBVType 32)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 32)
x (SymExpr sym (BaseBVType 32) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 32)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 32 -> IO (SymExpr sym (BaseBVType 32))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 32
v
    loop Type a'
Int64 (CW4.XInt64 SymExpr sym (BaseBVType 64)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 64
Refl <- NatRepr w -> NatRepr 64 -> Maybe (w :~: 64)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64) =
      sym
-> SymExpr sym (BaseBVType 64)
-> SymExpr sym (BaseBVType 64)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 64)
x (SymExpr sym (BaseBVType 64) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 64)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 64 -> IO (SymExpr sym (BaseBVType 64))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 64
v
    loop Type a'
Word8 (CW4.XWord8 SymExpr sym (BaseBVType 8)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 8
Refl <- NatRepr w -> NatRepr 8 -> Maybe (w :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) =
      sym
-> SymExpr sym (BaseBVType 8)
-> SymExpr sym (BaseBVType 8)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 8)
x (SymExpr sym (BaseBVType 8) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 8)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 8 -> IO (SymExpr sym (BaseBVType 8))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 8
v
    loop Type a'
Word16 (CW4.XWord16 SymExpr sym (BaseBVType 16)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 16
Refl <- NatRepr w -> NatRepr 16 -> Maybe (w :~: 16)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16) =
      sym
-> SymExpr sym (BaseBVType 16)
-> SymExpr sym (BaseBVType 16)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 16)
x (SymExpr sym (BaseBVType 16) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 16)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 16 -> IO (SymExpr sym (BaseBVType 16))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 16
v
    loop Type a'
Word32 (CW4.XWord32 SymExpr sym (BaseBVType 32)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 32
Refl <- NatRepr w -> NatRepr 32 -> Maybe (w :~: 32)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32) =
      sym
-> SymExpr sym (BaseBVType 32)
-> SymExpr sym (BaseBVType 32)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 32)
x (SymExpr sym (BaseBVType 32) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 32)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 32 -> IO (SymExpr sym (BaseBVType 32))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 32
v
    loop Type a'
Word64 (CW4.XWord64 SymExpr sym (BaseBVType 64)
x) (LLVMPointerRepr NatRepr w
w) RegValue sym tp'
v | Just w :~: 64
Refl <- NatRepr w -> NatRepr 64 -> Maybe (w :~: 64)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64) =
      sym
-> SymExpr sym (BaseBVType 64)
-> SymExpr sym (BaseBVType 64)
-> IO (Pred sym)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymExpr sym (BaseBVType 64)
x (SymExpr sym (BaseBVType 64) -> IO (Pred sym))
-> IO (SymExpr sym (BaseBVType 64)) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak -> LLVMPtr sym 64 -> IO (SymExpr sym (BaseBVType 64))
forall sym bak (w :: Natural).
IsSymBackend sym bak =>
bak -> LLVMPtr sym w -> IO (SymBV sym w)
projectLLVM_bv bak
bak RegValue sym tp'
LLVMPtr sym 64
v

    loop Type a'
Float (CW4.XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
x)  (FloatRepr FloatInfoRepr flt
SingleFloatRepr) RegValue sym tp'
v = forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatEq @_ @SingleFloat sym
sym SymExpr sym (SymInterpretedFloatType sym SingleFloat)
x RegValue sym tp'
SymExpr sym (SymInterpretedFloatType sym SingleFloat)
v
    loop Type a'
Double (CW4.XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
x) (FloatRepr FloatInfoRepr flt
DoubleFloatRepr) RegValue sym tp'
v = forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (Pred sym)
iFloatEq @_ @DoubleFloat sym
sym SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
x RegValue sym tp'
SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
v

    loop (Array Type t
_ctp) (CW4.XEmptyArray Type t
_ctp2) (VectorRepr TypeRepr tp1
_tpr) RegValue sym tp'
vs =
      Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pred sym -> IO (Pred sym)) -> Pred sym -> IO (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> Bool -> Pred sym
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred sym
sym (Bool -> Pred sym) -> Bool -> Pred sym
forall a b. (a -> b) -> a -> b
$ Vector (RegValue sym tp1) -> Bool
forall a. Vector a -> Bool
V.null Vector (RegValue sym tp1)
RegValue sym tp'
vs
    loop (Array Type t
ctp) (CW4.XArray Vector n (XExpr sym)
xs) (VectorRepr TypeRepr tp1
tpr) RegValue sym tp'
vs
      | Vector n (XExpr sym) -> Int
forall (n :: Natural) a. Vector n a -> Int
PVec.lengthInt Vector n (XExpr sym)
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector (RegValue sym tp1) -> Int
forall a. Vector a -> Int
V.length Vector (RegValue sym tp1)
RegValue sym tp'
vs
      = (Pred sym -> Int -> RegValue sym tp1 -> IO (Pred sym))
-> Pred sym -> Vector (RegValue sym tp1) -> IO (Pred sym)
forall (m :: * -> *) a b.
Monad m =>
(a -> Int -> b -> m a) -> a -> Vector b -> m a
V.ifoldM (\Pred sym
pAcc Int
i RegValue sym tp1
v -> sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
pAcc (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type t
-> XExpr sym -> TypeRepr tp1 -> RegValue sym tp1 -> IO (Pred sym)
forall (tp' :: CrucibleType) a'.
Type a'
-> XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
loop Type t
ctp (Int -> Vector n (XExpr sym) -> XExpr sym
forall (n :: Natural) a. Int -> Vector n a -> a
PVec.elemAtUnsafe Int
i Vector n (XExpr sym)
xs) TypeRepr tp1
tpr RegValue sym tp1
v)
                 (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) Vector (RegValue sym tp1)
RegValue sym tp'
vs
      | Bool
otherwise
      = Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
    loop (Struct a'
struct) (CW4.XStruct [XExpr sym]
xs) (StructRepr CtxRepr ctx
ctx) RegValue sym tp'
vs
      | [(Value a', XExpr sym)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Value a', XExpr sym)]
copilotVals Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Size ctx -> Int
forall {k} (ctx :: Ctx k). Size ctx -> Int
Ctx.sizeInt (Assignment (RegValue' sym) ctx -> Size ctx
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size RegValue sym tp'
Assignment (RegValue' sym) ctx
vs)
      = (forall (x :: CrucibleType).
 IndexF (CtxRepr ctx) x -> Pred sym -> TypeRepr x -> IO (Pred sym))
-> Pred sym -> CtxRepr ctx -> IO (Pred sym)
forall {k} {l} (t :: (k -> *) -> l -> *) (m :: * -> *)
       (f :: k -> *) (z :: l) b.
(FoldableFCWithIndex t, Monad m) =>
(forall (x :: k). IndexF (t f z) x -> b -> f x -> m b)
-> b -> t f z -> m b
ifoldlMFC (\IndexF (CtxRepr ctx) x
i Pred sym
pAcc TypeRepr x
tpr ->
                    case [(Value a', XExpr sym)]
copilotVals [(Value a', XExpr sym)] -> Int -> (Value a', XExpr sym)
forall a. HasCallStack => [a] -> Int -> a
!! Index ctx x -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal IndexF (CtxRepr ctx) x
Index ctx x
i of
                      (Value Type t
ctp Field s t
_, XExpr sym
x) ->
                        sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
pAcc (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type t
-> XExpr sym -> TypeRepr x -> RegValue sym x -> IO (Pred sym)
forall (tp' :: CrucibleType) a'.
Type a'
-> XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
loop Type t
ctp XExpr sym
x TypeRepr x
tpr (RegValue' sym x -> RegValue sym x
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV (RegValue sym tp'
Assignment (RegValue' sym) ctx
vs Assignment (RegValue' sym) ctx -> Index ctx x -> RegValue' sym x
forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! IndexF (CtxRepr ctx) x
Index ctx x
i)))
                  (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) CtxRepr ctx
ctx
      | Bool
otherwise
      = Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym)
      where
        copilotVals :: [(Value a', CW4.XExpr sym)]
        copilotVals :: [(Value a', XExpr sym)]
copilotVals = [Value a'] -> [XExpr sym] -> [(Value a', XExpr sym)]
forall a b. [a] -> [b] -> [(a, b)]
zip (a' -> [Value a']
forall a. Struct a => a -> [Value a]
toValues a'
struct) [XExpr sym]
xs

    -- If we encounter a pointer, read the memory that it points to and recurse,
    -- using the Copilot type as a guide for how much memory to read. This is
    -- needed to make array- or struct-typed arguments work (see
    -- Note [Arrays and structs]), although there is nothing about this code
    -- that is array- or struct-specific. In fact, this code could also work
    -- for pointer arguments of any other type.
    loop Type a'
ctp XExpr sym
x TypeRepr tp'
PtrRepr RegValue sym tp'
v =
      do let memTy :: MemType
memTy = DataLayout -> Type a' -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) Type a'
ctp
             typeAlign :: Alignment
typeAlign = DataLayout -> MemType -> Alignment
memTypeAlign (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) MemType
memTy
         StorageType
stp <- MemType -> IO StorageType
forall (m :: * -> *) (wptr :: Natural).
(MonadFail m, HasPtrWidth wptr) =>
MemType -> m StorageType
toStorableType MemType
memTy
         MemType
-> (forall {tp :: CrucibleType}. TypeRepr tp -> IO (Pred sym))
-> IO (Pred sym)
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
memTy ((forall {tp :: CrucibleType}. TypeRepr tp -> IO (Pred sym))
 -> IO (Pred sym))
-> (forall {tp :: CrucibleType}. TypeRepr tp -> IO (Pred sym))
-> IO (Pred sym)
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr ->
           do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
              (BoolAnn sym
bann, Pred sym
p, RegValue sym tp
regVal) <- bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (BoolAnn sym, Pred sym, RegValue sym tp)
forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (BoolAnn sym, Pred sym, RegValue sym tp)
doLoadWithAnn bak
bak MemImpl sym
mem RegValue sym tp'
LLVMPtr sym wptr
v StorageType
stp TypeRepr tp
tpr Alignment
typeAlign
              IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs)
                ((Map (BoolAnn sym) (VerifierAssertion sym)
  -> Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO ())
-> (Map (BoolAnn sym) (VerifierAssertion sym)
    -> Map (BoolAnn sym) (VerifierAssertion sym))
-> IO ()
forall a b. (a -> b) -> a -> b
$ BoolAnn sym
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BoolAnn sym
bann
                (VerifierAssertion sym
 -> Map (BoolAnn sym) (VerifierAssertion sym)
 -> Map (BoolAnn sym) (VerifierAssertion sym))
-> VerifierAssertion sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Map (BoolAnn sym) (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ SomeSome (PointerArgumentLoad sym) -> VerifierAssertion sym
forall sym.
SomeSome (PointerArgumentLoad sym) -> VerifierAssertion sym
Log.PointerArgumentLoadAssertion
                (SomeSome (PointerArgumentLoad sym) -> VerifierAssertion sym)
-> SomeSome (PointerArgumentLoad sym) -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ PointerArgumentLoad sym a' tp -> SomeSome (PointerArgumentLoad sym)
forall {j} {k} (f :: j -> k -> *) (x :: j) (y :: k).
f x y -> SomeSome f
Log.SomeSome
                (PointerArgumentLoad sym a' tp
 -> SomeSome (PointerArgumentLoad sym))
-> PointerArgumentLoad sym a' tp
-> SomeSome (PointerArgumentLoad sym)
forall a b. (a -> b) -> a -> b
$ sym
-> ProgramLoc
-> Type a'
-> TypeRepr tp
-> Pred sym
-> PointerArgumentLoad sym a' tp
forall sym copilotType (crucibleType :: CrucibleType).
sym
-> ProgramLoc
-> Type copilotType
-> TypeRepr crucibleType
-> Pred sym
-> PointerArgumentLoad sym copilotType crucibleType
Log.PointerArgumentLoad sym
sym ProgramLoc
loc Type a'
ctp TypeRepr tp
tpr Pred sym
p
              Type a'
-> XExpr sym -> TypeRepr tp -> RegValue sym tp -> IO (Pred sym)
forall (tp' :: CrucibleType) a'.
Type a'
-> XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
loop Type a'
ctp XExpr sym
x TypeRepr tp
tpr RegValue sym tp
regVal

    loop Type a'
_ctp XExpr sym
x TypeRepr tp'
tpr RegValue sym tp'
_v =
      String -> IO (Pred sym)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (Pred sym)) -> String -> IO (Pred sym)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
"Mismatch between Copilot value and crucible value", XExpr sym -> String
forall a. Show a => a -> String
show XExpr sym
x, TypeRepr tp' -> String
forall a. Show a => a -> String
show TypeRepr tp'
tpr]

-- | Convert a Copilot 'CT.Type' to a Crucible 'MemType'. 'CT.Bool's are
-- assumed to be one bit in size. See @Note [How LLVM represents bool]@.
copilotTypeToMemType ::
  DataLayout ->
  CT.Type a ->
  MemType
copilotTypeToMemType :: forall a. DataLayout -> Type a -> MemType
copilotTypeToMemType DataLayout
dl = Type a -> MemType
forall t. Type t -> MemType
loop
  where
    loop :: forall t. CT.Type t -> MemType
    loop :: forall t. Type t -> MemType
loop Type t
CT.Bool   = MemType
i1
    loop Type t
CT.Int8   = MemType
i8
    loop Type t
CT.Int16  = MemType
i16
    loop Type t
CT.Int32  = MemType
i32
    loop Type t
CT.Int64  = MemType
i64
    loop Type t
CT.Word8  = MemType
i8
    loop Type t
CT.Word16 = MemType
i16
    loop Type t
CT.Word32 = MemType
i32
    loop Type t
CT.Word64 = MemType
i64
    loop Type t
CT.Float  = MemType
FloatType
    loop Type t
CT.Double = MemType
DoubleType
    loop t0 :: Type t
t0@(CT.Array Type t
tp) =
      let len :: Natural
len = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Type (Array n t) -> Int
forall (n :: Natural) t. KnownNat n => Type (Array n t) -> Int
typeLength Type t
Type (Array n t)
t0) in
      Natural -> MemType -> MemType
ArrayType Natural
len (DataLayout -> Type t -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 DataLayout
dl Type t
tp)
    loop (CT.Struct t
v) =
      StructInfo -> MemType
StructType (DataLayout -> Bool -> [MemType] -> StructInfo
mkStructInfo DataLayout
dl Bool
False ((Value t -> MemType) -> [Value t] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map Value t -> MemType
forall t. Value t -> MemType
val (t -> [Value t]
forall a. Struct a => a -> [Value a]
CT.toValues t
v)))

    val :: forall t. CT.Value t -> MemType
    val :: forall t. Value t -> MemType
val (CT.Value Type t
tp Field s t
_) = DataLayout -> Type t -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 DataLayout
dl Type t
tp

-- | Like 'copilotTypeToMemType', except that 'CT.Bool's are assumed to be
-- eight bits, not one bit. See @Note [How LLVM represents bool]@.
copilotTypeToMemTypeBool8 ::
  DataLayout ->
  CT.Type a ->
  MemType
copilotTypeToMemTypeBool8 :: forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 DataLayout
_dl Type a
CT.Bool = MemType
i8
copilotTypeToMemTypeBool8 DataLayout
dl Type a
tp = DataLayout -> Type a -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemType DataLayout
dl Type a
tp

-- | Like 'copilotTypeToMemType', except that composite types (i.e.,
-- 'CT.Array's and 'CT.Struct's) are converted to 'PtrType's instead of direct
-- 'ArrayType's or 'StructType's. See @Note [Arrays and structs]@.
copilotTypeToMemTypeCompositePtr ::
  DataLayout ->
  CT.Type a ->
  MemType
copilotTypeToMemTypeCompositePtr :: forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeCompositePtr DataLayout
dl (CT.Array Type t
tp) =
  SymType -> MemType
PtrType (MemType -> SymType
MemType (DataLayout -> Type t -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemTypeBool8 DataLayout
dl Type t
tp))
copilotTypeToMemTypeCompositePtr DataLayout
_dl (CT.Struct a
struct) =
  SymType -> MemType
PtrType (Ident -> SymType
Alias (a -> Ident
forall a. Struct a => a -> Ident
copilotStructIdent a
struct))
copilotTypeToMemTypeCompositePtr DataLayout
dl Type a
tp = DataLayout -> Type a -> MemType
forall a. DataLayout -> Type a -> MemType
copilotTypeToMemType DataLayout
dl Type a
tp

-- | Convert a Copilot 'CT.Type' to an LLVM 'L.Type'. 'CT.Bool's are
-- assumed to be one bit in size. See @Note [How LLVM represents bool]@.
copilotTypeToLLVMType ::
  CT.Type a ->
  L.Type
copilotTypeToLLVMType :: forall a. Type a -> Type
copilotTypeToLLVMType = Type a -> Type
forall a. Type a -> Type
loop
  where
    loop :: forall t. CT.Type t -> L.Type
    loop :: forall a. Type a -> Type
loop Type t
CT.Bool   = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
1)
    loop Type t
CT.Int8   = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
8)
    loop Type t
CT.Int16  = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
16)
    loop Type t
CT.Int32  = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
32)
    loop Type t
CT.Int64  = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
64)
    loop Type t
CT.Word8  = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
8)
    loop Type t
CT.Word16 = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
16)
    loop Type t
CT.Word32 = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
32)
    loop Type t
CT.Word64 = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
64)
    loop Type t
CT.Float  = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (FloatType -> PrimType
L.FloatType FloatType
L.Float)
    loop Type t
CT.Double = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (FloatType -> PrimType
L.FloatType FloatType
L.Double)
    loop t0 :: Type t
t0@(CT.Array Type t
tp) =
      let len :: Word64
len = Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Type (Array n t) -> Int
forall (n :: Natural) t. KnownNat n => Type (Array n t) -> Int
typeLength Type t
Type (Array n t)
t0) in
      Word64 -> Type -> Type
forall ident. Word64 -> Type' ident -> Type' ident
L.Array Word64
len (Type t -> Type
forall a. Type a -> Type
copilotTypeToLLVMTypeBool8 Type t
tp)
    loop (CT.Struct t
v) =
      -- NB: Don't use L.Struct here. That represents a literal, unnamed
      -- struct, but all of the structs used in a copilot-c99 program are
      -- named structs. As such, we must identify the struct by its alias.
      Ident -> Type
forall ident. ident -> Type' ident
L.Alias (t -> Ident
forall a. Struct a => a -> Ident
copilotStructIdent t
v)

-- | Like 'copilotTypeToLLVMType', except that 'CT.Bool's are assumed to be
-- eight bits, not one bit. See @Note [How LLVM represents bool]@.
copilotTypeToLLVMTypeBool8 ::
  CT.Type a ->
  L.Type
copilotTypeToLLVMTypeBool8 :: forall a. Type a -> Type
copilotTypeToLLVMTypeBool8 Type a
CT.Bool = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (Word32 -> PrimType
L.Integer Word32
8)
copilotTypeToLLVMTypeBool8 Type a
tp = Type a -> Type
forall a. Type a -> Type
copilotTypeToLLVMType Type a
tp

-- | Like 'copilotTypeToLLVMType', except that composite types (i.e.,
-- 'CT.Array's and 'CT.Struct's) are given special treatment involving
-- pointers. See @Note [Arrays and structs]@.
copilotTypeToLLVMTypeCompositePtr ::
  CT.Type a ->
  L.Type
copilotTypeToLLVMTypeCompositePtr :: forall a. Type a -> Type
copilotTypeToLLVMTypeCompositePtr (CT.Array Type t
tp) =
  Type -> Type
forall ident. Type' ident -> Type' ident
L.PtrTo (Type t -> Type
forall a. Type a -> Type
copilotTypeToLLVMTypeBool8 Type t
tp)
copilotTypeToLLVMTypeCompositePtr (CT.Struct a
struct) =
  Type -> Type
forall ident. Type' ident -> Type' ident
L.PtrTo (Ident -> Type
forall ident. ident -> Type' ident
L.Alias (a -> Ident
forall a. Struct a => a -> Ident
copilotStructIdent a
struct))
copilotTypeToLLVMTypeCompositePtr Type a
tp = Type a -> Type
forall a. Type a -> Type
copilotTypeToLLVMType Type a
tp

-- | Given a struct @s@, construct the name @struct.s@ as an LLVM identifier.
copilotStructIdent :: Struct a => a -> L.Ident
copilotStructIdent :: forall a. Struct a => a -> Ident
copilotStructIdent a
struct = String -> Ident
L.Ident (String -> Ident) -> String -> Ident
forall a b. (a -> b) -> a -> b
$ String
"struct." String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Struct a => a -> String
typeName a
struct

{-
Note [How LLVM represents bool]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
How are C values of type `bool` represented in LLVM? It depends. If it's being
stored directly a `bool`, it's represented with `i1` (i.e., a single bit). If
a `bool` is a member of some composite type, such as a pointer, array, or
struct, however, it's representing with `i8` (i.e., eight bits). This means
that we have to be careful when converting Bool-typed Copilot values, as they
can become `i1` or `i8` depending on the context.

copilot-verifier handles this by having both `copilotTypeToLLVMType` and
`copilotTypeToLLVMTypeBool8` functions. The former function treats `bool`s as
`i1`, whereas the latter treats `bool`s as `i8`. The former is used when
converting "top-level" types (e.g., the argument types in a trigger override),
whereas the latter is used when converting types that are part of a larger
composite type (e.g., the element type in an array).

The story for the `copilotTypeToMemType` and `copilotTypeToMemTypeBool8`
functions is similar.

Note [Arrays and structs]
~~~~~~~~~~~~~~~~~~~~~~~~~
When Clang compiles a function with an array argument, such as this trigger
function:

  void func(int32_t func_arg0[2]) { ... }

It will produce the following LLVM code:

  declare void @func(i32*) { ... }

Note that the argument is an i32*, not a [2 x i32]. As a result, we can't
translate Copilot array types directly to LLVM array types when they're used as
arguments to a function. This impedance mismatch is handled in two places:

1. The `copilotTypeToMemTypeCompositePtr`/`copilotTypeToLLVMTypeCompositePtr`
   functions special-case Copilot arrays such that they are translated to
   pointers. These functions are used when declaring the argument types of an
   override for a trigger function (see `triggerOverride`).
2. The `computeEqualVals` function has a special case for pointer
   arguments—see the case that matches on `PtrRepr`. When a `PtrRepr` is
   encountered, the underlying array values that it points to are read from
   memory. Because `PtrRepr` doesn't record the type of the thing being pointed
   to, `computeEqualVals` uses the corresponding Copilot type as a guide to
   determine how much memory to read and at what type the memory should be
   used. After this, `computeEqualVals` reads from the read array
   element-by-element—see the `VectorRepr` cases.

   Note that unlike `computeEqualVals`, `copilotExprToRegValue` does not need
   a `PtrRepr` case. This is because `copilotExprToRegValue` is ultimately used
   in service of calling writing elements of streams to memory, and streams do
   not store pointer values (at least, not in today's Copilot).

There is a very similar story for structs. Copilot passes structs by reference
in trigger functions (e.g., `void trigger(struct s *ss)`), so we must also load
from a `PtrRepr` in `computeEqualVals` to handle structs.

See Note [Global variables for trigger functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As part of verifying that the behavior of a Copilot specification's trigger
functions behave the same way as the trigger functions in the corresponding C
program, we check that each trigger function in the C program is invoked the
appropriate number of times. That is, if the guard condition for a trigger is
true, the C trigger function should be invoked exactly once, and if the guard
condition is false, then the trigger function should not be invoked at all.

To check this, we create a Nat-valued global variable for each trigger function
and initialize it to zero. Whenever we simulate a trigger function, we increment
the value of the corresponding global variable. At the end of simulation, we
check that the value in each global variable is equal to
`if guard_cond then 1 else 0`.
-}

-- | Like @crucible-llvm@'s @doLoad@, but with the following differences:
--
-- * This function returns the 'BoolAnn' and 'Pred' asserting the validity of
--   the load, which the verifier needs for logging purposes.
--
-- * This always generates a durable proof goal so that Crucible will always
--   record it, even if it is trivial.
doLoadWithAnn ::
  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
  , ?memOpts :: MemOptions ) =>
  bak ->
  MemImpl sym ->
  LLVMPtr sym wptr {- ^ pointer to load from      -} ->
  StorageType      {- ^ type of value to load     -} ->
  TypeRepr tp      {- ^ crucible type of the result -} ->
  Alignment        {- ^ assumed pointer alignment -} ->
  IO (BoolAnn sym, Pred sym, RegValue sym tp)
doLoadWithAnn :: forall sym bak (wptr :: Natural) (tp :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> TypeRepr tp
-> Alignment
-> IO (BoolAnn sym, Pred sym, RegValue sym tp)
doLoadWithAnn bak
bak MemImpl sym
mem LLVMPtr sym wptr
ptr StorageType
valType TypeRepr tp
tpr Alignment
alignment = do
    PartLLVMVal sym
partLLVMVal <- sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> IO (PartLLVMVal sym)
forall sym (wptr :: Natural).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> IO (PartLLVMVal sym)
loadRaw sym
sym MemImpl sym
mem LLVMPtr sym wptr
ptr StorageType
valType Alignment
alignment
    (BoolAnn sym
bann, Pred sym
p, LLVMVal sym
llvmVal) <- bak -> PartLLVMVal sym -> IO (BoolAnn sym, Pred sym, LLVMVal sym)
forall sym bak.
IsSymBackend sym bak =>
bak -> PartLLVMVal sym -> IO (BoolAnn sym, Pred sym, LLVMVal sym)
assertSafeWithAnn bak
bak PartLLVMVal sym
partLLVMVal
    RegValue sym tp
regVal <- sym -> TypeRepr tp -> LLVMVal sym -> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
(HasCallStack, IsSymInterface sym) =>
sym -> TypeRepr tp -> LLVMVal sym -> IO (RegValue sym tp)
unpackMemValue sym
sym TypeRepr tp
tpr LLVMVal sym
llvmVal
    (BoolAnn sym, Pred sym, RegValue sym tp)
-> IO (BoolAnn sym, Pred sym, RegValue sym tp)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BoolAnn sym
bann, Pred sym
p, RegValue sym tp
regVal)
  where
    sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak

-- | Like @crucible-llvm@'s @assertSafe@, but with the following differences:
--
-- * This function returns the 'BoolAnn' and 'Pred' corresponding to the
--   assertion, which the verifier needs for logging purposes.
--
-- * This generates a durable assertion so that Crucible will always record it,
--   even if it is trivial.
assertSafeWithAnn ::
  IsSymBackend sym bak =>
  bak ->
  PartLLVMVal sym ->
  IO (BoolAnn sym, Pred sym, LLVMVal sym)
assertSafeWithAnn :: forall sym bak.
IsSymBackend sym bak =>
bak -> PartLLVMVal sym -> IO (BoolAnn sym, Pred sym, LLVMVal sym)
assertSafeWithAnn bak
bak PartLLVMVal sym
partVal = do
  ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
  let err :: SimError
err = ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
rsn
  case PartLLVMVal sym
partVal of
    NoErr Pred sym
p LLVMVal sym
v -> do
      (SymAnnotation sym BaseBoolType
ann, Pred sym
p') <- sym -> Pred sym -> IO (SymAnnotation sym BaseBoolType, Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym Pred sym
p
      bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableAssertion bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
p' SimError
err)
      (BoolAnn sym, Pred sym, LLVMVal sym)
-> IO (BoolAnn sym, Pred sym, LLVMVal sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
ann, Pred sym
p', LLVMVal sym
v)
    Err Pred sym
p -> do
      (SymAnnotation sym BaseBoolType
_ann, Pred sym
p') <- sym -> Pred sym -> IO (SymAnnotation sym BaseBoolType, Pred sym)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym Pred sym
p
      bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
p' SimError
err)
      AbortExecReason -> IO (BoolAnn sym, Pred sym, LLVMVal sym)
forall a. AbortExecReason -> IO a
abortExecBecause (SimError -> AbortExecReason
AssertionFailure SimError
err)
  where
    rsn :: SimErrorReason
rsn = String -> String -> SimErrorReason
AssertFailureSimError String
"Error during memory load" String
""
    sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak

-- | Given a simulator state, extract any collected proof obligations,
--   attempt to prove them, and present the results to the user.
--
--   Afterward, the simulator state will be cleared of any proof obligations,
--   regardless of if they could all be proved.
proveObls ::
  IsSymInterface sym =>
  sym ~ ExprBuilder t st fs =>
  Log.Logs msgs =>
  Log.SupportsCruxLogMessage msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  CruxOptions ->
  [SolverAdapter st] ->
  CopilotLogRefs sym ->
  Log.VerificationStep ->
  SimCtxt Crux sym LLVM ->
  IO Integer
proveObls :: forall sym t (st :: * -> *) fs msgs.
(IsSymInterface sym, sym ~ ExprBuilder t st fs, Logs msgs,
 SupportsCruxLogMessage msgs, SupportsCopilotLogMessage msgs) =>
CruxOptions
-> [SolverAdapter st]
-> CopilotLogRefs sym
-> VerificationStep
-> SimCtxt Crux sym LLVM
-> IO Integer
proveObls CruxOptions
cruxOpts [SolverAdapter st]
adapters CopilotLogRefs sym
clRefs VerificationStep
step SimCtxt Crux sym LLVM
simctx =
  SimCtxt Crux sym LLVM
-> (forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
-> IO Integer
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
withBackend SimCtxt Crux sym LLVM
simctx ((forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
 -> IO Integer)
-> (forall {bak}. IsSymBackend sym bak => bak -> IO Integer)
-> IO Integer
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
obls <- bak
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
           (LabeledPred
              (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
getProofObligations bak
bak
     bak -> IO ()
forall sym bak. IsSymBackend sym bak => bak -> IO ()
clearProofObligations bak
bak

--     mapM_ (print . ppSimError) (summarizeObls sym obls)

     Map (BoolAnn sym) (VerifierAssertion sym)
vaMap <- IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> IO (Map (BoolAnn sym) (VerifierAssertion sym))
forall a. IORef a -> IO a
readIORef (IORef (Map (BoolAnn sym) (VerifierAssertion sym))
 -> IO (Map (BoolAnn sym) (VerifierAssertion sym)))
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
-> IO (Map (BoolAnn sym) (VerifierAssertion sym))
forall a b. (a -> b) -> a -> b
$ CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef CopilotLogRefs sym
clRefs
     let laMapRef :: IORef (LLVMAnnMap sym)
laMapRef = CopilotLogRefs sym -> IORef (LLVMAnnMap sym)
forall sym. CopilotLogRefs sym -> IORef (LLVMAnnMap sym)
llvmAnnMapRef CopilotLogRefs sym
clRefs
     LLVMAnnMap sym
laMap <- IORef (LLVMAnnMap sym) -> IO (LLVMAnnMap sym)
forall a. IORef a -> IO a
readIORef IORef (LLVMAnnMap sym)
laMapRef
     (ProcessedGoals,
 Maybe
   (Goals
      (CrucibleAssumptions (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
       ProofResult (ExprBuilder t st fs))))
results <- [SolverAdapter st]
-> CruxOptions
-> SimCtxt Crux sym LLVM
-> (Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void))
-> Maybe (Goals (Assumptions sym) (Assertion sym))
-> IO
     (ProcessedGoals,
      Maybe
        (Goals
           (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
forall (st :: * -> *) sym p t fs (personality :: * -> *) msgs.
(sym ~ ExprBuilder t st fs, Logs msgs,
 SupportsCruxLogMessage msgs) =>
[SolverAdapter st]
-> CruxOptions
-> SimCtxt personality sym p
-> (Maybe (GroundEvalFn t) -> Assertion sym -> IO (Doc Void))
-> Maybe (Goals (Assumptions sym) (Assertion sym))
-> IO
     (ProcessedGoals,
      Maybe
        (Goals
           (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
proveGoalsOffline [SolverAdapter st]
adapters CruxOptions
cruxOpts SimCtxt Crux sym LLVM
simctx (sym
-> IORef (LLVMAnnMap sym)
-> Maybe (GroundEvalFn t)
-> Assertion sym
-> IO (Doc Void)
forall sym t (st :: * -> *) fs ann.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
sym -> IORef (LLVMAnnMap sym) -> Explainer sym t ann
explainFailure sym
sym IORef (LLVMAnnMap sym)
laMapRef) Maybe (Goals (Assumptions sym) (Assertion sym))
Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder t st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder t st fs) BaseBoolType) SimError))
obls
     sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> LLVMAnnMap sym
-> VerificationStep
-> (ProcessedGoals,
    Maybe
      (Goals
         (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
-> IO Integer
forall msgs sym.
(Logs msgs, SupportsCopilotLogMessage msgs, IsSymInterface sym) =>
sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> LLVMAnnMap sym
-> VerificationStep
-> (ProcessedGoals,
    Maybe
      (Goals
         (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
-> IO Integer
presentResults sym
sym Map (BoolAnn sym) (VerifierAssertion sym)
vaMap LLVMAnnMap sym
laMap VerificationStep
step (ProcessedGoals,
 Maybe
   (Goals
      (CrucibleAssumptions (Expr t))
      (LabeledPred (Expr t BaseBoolType) SimError, [ProgramLoc],
       ProofResult (ExprBuilder t st fs))))
(ProcessedGoals,
 Maybe
   (Goals
      (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
results

{-
summarizeObls :: sym -> ProofObligations sym -> [SimError]
summarizeObls _ Nothing = []
summarizeObls _ (Just obls) = map (view labeledPredMsg . proofGoal) (goalsToList obls)
-}

-- | Compute the number of goals that were proven during verification, logging
-- the goals as they are proven. If all goals are proven successfully, return
-- the number of goals. Otherwise, log the failing proof goals and abort.
presentResults ::
  Log.Logs msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  IsSymInterface sym =>
  sym ->
  Map.Map (BoolAnn sym) (Log.VerifierAssertion sym) ->
  LLVMAnnMap sym ->
  Log.VerificationStep ->
  (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) ->
  IO Integer
presentResults :: forall msgs sym.
(Logs msgs, SupportsCopilotLogMessage msgs, IsSymInterface sym) =>
sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> LLVMAnnMap sym
-> VerificationStep
-> (ProcessedGoals,
    Maybe
      (Goals
         (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)))
-> IO Integer
presentResults sym
sym Map (BoolAnn sym) (VerifierAssertion sym)
vaMap LLVMAnnMap sym
laMap VerificationStep
step (ProcessedGoals
num, Maybe
  (Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
goals)
  | Integer
numTotalGoals Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
  = do CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot CopilotLogMessage
Log.AllGoalsProved
       Integer -> IO Integer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0

    -- All goals were proven
  | Integer
numProvedGoals Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
numTotalGoals
  = do (Goals
   (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
 -> IO ())
-> Maybe
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
-> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> LLVMAnnMap sym
-> VerificationStep
-> ProcessedGoals
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO ()
forall sym msgs.
(IsSymInterface sym, Logs msgs, SupportsCopilotLogMessage msgs) =>
sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> LLVMAnnMap sym
-> VerificationStep
-> ProcessedGoals
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO ()
logVerifierAssertions sym
sym Map (BoolAnn sym) (VerifierAssertion sym)
vaMap LLVMAnnMap sym
laMap VerificationStep
step ProcessedGoals
num) Maybe
  (Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
goals
       IO ()
printGoals
       Integer -> IO Integer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
numProvedGoals

    -- There were some unproved goals, so fail with exit code 1
  | Bool
otherwise
  = do IO ()
printGoals
       IO Integer
forall a. IO a
exitFailure
  where
    numTotalGoals :: Integer
numTotalGoals  = ProcessedGoals -> Integer
totalProcessedGoals ProcessedGoals
num
    numProvedGoals :: Integer
numProvedGoals = ProcessedGoals -> Integer
provedGoals ProcessedGoals
num

    printGoals :: IO ()
printGoals =
      do CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> CopilotLogMessage
Log.OnlySomeGoalsProved Integer
numProvedGoals Integer
numTotalGoals
         Maybe ProvedGoals
goals' <- sym
-> Maybe
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
-> IO (Maybe ProvedGoals)
forall sym.
IsSymInterface sym =>
sym
-> Maybe
     (Goals
        (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
-> IO (Maybe ProvedGoals)
provedGoalsTree sym
sym Maybe
  (Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))
goals
         case Maybe ProvedGoals
goals' of
           Just ProvedGoals
g -> ProvedGoals -> IO ()
forall msgs. Logs msgs => ProvedGoals -> IO ()
Log.logGoal ProvedGoals
g
           Maybe ProvedGoals
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Upon a successful verification, log the various assertions that the
-- verifier makes. These assertions will be visible in the output if the
-- 'verbosity' is set to 'Noisy'.
logVerifierAssertions ::
  forall sym msgs.
  IsSymInterface sym =>
  Log.Logs msgs =>
  Log.SupportsCopilotLogMessage msgs =>
  sym ->
  Map.Map (BoolAnn sym) (Log.VerifierAssertion sym) ->
  LLVMAnnMap sym ->
  Log.VerificationStep ->
  ProcessedGoals ->
  Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->
  IO ()
logVerifierAssertions :: forall sym msgs.
(IsSymInterface sym, Logs msgs, SupportsCopilotLogMessage msgs) =>
sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> LLVMAnnMap sym
-> VerificationStep
-> ProcessedGoals
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO ()
logVerifierAssertions sym
sym Map (BoolAnn sym) (VerifierAssertion sym)
vaMap LLVMAnnMap sym
laMap VerificationStep
step ProcessedGoals
num Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
goals = IO Integer -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Integer -> IO ()) -> IO Integer -> IO ()
forall a b. (a -> b) -> a -> b
$ Integer
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO Integer
go Integer
0 Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
goals
  where
    numTotalGoals :: Integer
numTotalGoals = ProcessedGoals -> Integer
totalProcessedGoals ProcessedGoals
num

    go :: Integer ->
          Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->
          IO Integer
    go :: Integer
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO Integer
go Integer
goalIdx Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs =
      case Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs of
        Assuming Assumptions sym
_ Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs' ->
          Integer
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO Integer
go Integer
goalIdx Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs'

        Prove (Assertion sym
gl, [ProgramLoc]
locs, ProofResult sym
_) -> do
          let p :: SymExpr sym BaseBoolType
p = Assertion sym
glAssertion sym
-> Getting
     (SymExpr sym BaseBoolType)
     (Assertion sym)
     (SymExpr sym BaseBoolType)
-> SymExpr sym BaseBoolType
forall s a. s -> Getting a s a -> a
^.Getting
  (SymExpr sym BaseBoolType)
  (Assertion sym)
  (SymExpr sym BaseBoolType)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred
              nearestLoc :: ProgramLoc
nearestLoc = [ProgramLoc] -> ProgramLoc
nearestProgramLoc [ProgramLoc]
locs

          -- First, obtain the verifier assertion.
          VerifierAssertion sym
va <- case sym
-> SymExpr sym BaseBoolType
-> Maybe (SymAnnotation sym BaseBoolType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
getAnnotation sym
sym SymExpr sym BaseBoolType
p of
            -- If the assertion has a BoolAnn, look it up in the assertion maps
            -- that we have accumulated during verification.
            Just SymAnnotation sym BaseBoolType
ann
              |  Just VerifierAssertion sym
va <- BoolAnn sym
-> Map (BoolAnn sym) (VerifierAssertion sym)
-> Maybe (VerifierAssertion sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
ann) Map (BoolAnn sym) (VerifierAssertion sym)
vaMap
              -> VerifierAssertion sym -> IO (VerifierAssertion sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VerifierAssertion sym
va
              |  Just (CallStack
stk, BadBehavior sym
bb) <- BoolAnn sym -> LLVMAnnMap sym -> Maybe (CallStack, BadBehavior sym)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SymAnnotation sym BaseBoolType -> BoolAnn sym
forall sym. SymAnnotation sym BaseBoolType -> BoolAnn sym
BoolAnn SymAnnotation sym BaseBoolType
ann) LLVMAnnMap sym
laMap
              -> VerifierAssertion sym -> IO (VerifierAssertion sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VerifierAssertion sym -> IO (VerifierAssertion sym))
-> VerifierAssertion sym -> IO (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ LLVMBadBehaviorCheck sym -> VerifierAssertion sym
forall sym. LLVMBadBehaviorCheck sym -> VerifierAssertion sym
Log.LLVMBadBehaviorCheckAssertion
                      (LLVMBadBehaviorCheck sym -> VerifierAssertion sym)
-> LLVMBadBehaviorCheck sym -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$ sym
-> ProgramLoc
-> CallStack
-> BadBehavior sym
-> SymExpr sym BaseBoolType
-> LLVMBadBehaviorCheck sym
forall sym.
sym
-> ProgramLoc
-> CallStack
-> BadBehavior sym
-> Pred sym
-> LLVMBadBehaviorCheck sym
Log.LLVMBadBehaviorCheck sym
sym ProgramLoc
nearestLoc CallStack
stk BadBehavior sym
bb SymExpr sym BaseBoolType
p
              |  Bool
otherwise
              -> String -> IO (VerifierAssertion sym)
forall a. String -> IO a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> IO (VerifierAssertion sym))
-> String -> IO (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                   [ String
"Cannot find BoolAnn for assertion"
                   , SimError -> String
forall a. Show a => a -> String
show (SimError -> String) -> SimError -> String
forall a b. (a -> b) -> a -> b
$ Assertion sym
glAssertion sym
-> Getting SimError (Assertion sym) SimError -> SimError
forall s a. s -> Getting a s a -> a
^.Getting SimError (Assertion sym) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg
                   , Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SymExpr sym BaseBoolType -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymExpr sym BaseBoolType
p
                   ]
            -- If the assertion does not have a BoolAnn, fall back to using
            -- heuristics to guess what kind of assertion it is.
            Maybe (SymAnnotation sym BaseBoolType)
Nothing -> VerifierAssertion sym -> IO (VerifierAssertion sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VerifierAssertion sym -> IO (VerifierAssertion sym))
-> VerifierAssertion sym -> IO (VerifierAssertion sym)
forall a b. (a -> b) -> a -> b
$ sym
-> ProgramLoc -> SymExpr sym BaseBoolType -> VerifierAssertion sym
forall sym.
IsSymInterface sym =>
sym -> ProgramLoc -> Pred sym -> VerifierAssertion sym
verifierAssertionHeuristics sym
sym ProgramLoc
nearestLoc SymExpr sym BaseBoolType
p

          -- Log the assertion.
          case VerifierAssertion sym
va of
            Log.StreamValueEqualityAssertion (Log.SomeSome StreamValueEquality sym x y
a) ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> StreamValueEquality sym x y
-> CopilotLogMessage
forall sym copilotType (crucibleType :: CrucibleType).
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> StreamValueEquality sym copilotType crucibleType
-> CopilotLogMessage
Log.StreamValueEqualityProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals StreamValueEquality sym x y
a
            Log.TriggersInvokedCorrespondinglyAssertion TriggersInvokedCorrespondingly sym
a ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> TriggersInvokedCorrespondingly sym
-> CopilotLogMessage
forall sym.
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> TriggersInvokedCorrespondingly sym
-> CopilotLogMessage
Log.TriggersInvokedCorrespondinglyProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals TriggersInvokedCorrespondingly sym
a
            Log.TriggerArgumentEqualityAssertion (Log.SomeSome TriggerArgumentEquality sym x y
a) ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> TriggerArgumentEquality sym x y
-> CopilotLogMessage
forall sym copilotType (crucibleType :: CrucibleType).
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> TriggerArgumentEquality sym copilotType crucibleType
-> CopilotLogMessage
Log.TriggerArgumentEqualityProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals TriggerArgumentEquality sym x y
a
            Log.RingBufferLoadAssertion (Log.SomeSome RingBufferLoad sym x y
a) ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> RingBufferLoad sym x y
-> CopilotLogMessage
forall sym copilotType (crucibleType :: CrucibleType).
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> RingBufferLoad sym copilotType crucibleType
-> CopilotLogMessage
Log.RingBufferLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals RingBufferLoad sym x y
a
            Log.RingBufferIndexLoadAssertion RingBufferIndexLoad sym
a ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> RingBufferIndexLoad sym
-> CopilotLogMessage
forall sym.
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> RingBufferIndexLoad sym
-> CopilotLogMessage
Log.RingBufferIndexLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals RingBufferIndexLoad sym
a
            Log.PointerArgumentLoadAssertion (Log.SomeSome PointerArgumentLoad sym x y
a) ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> PointerArgumentLoad sym x y
-> CopilotLogMessage
forall sym copilotType (crucibleType :: CrucibleType).
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> PointerArgumentLoad sym copilotType crucibleType
-> CopilotLogMessage
Log.PointerArgumentLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals PointerArgumentLoad sym x y
a
            Log.AccessorFunctionLoadAssertion AccessorFunctionLoad sym
a ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> AccessorFunctionLoad sym
-> CopilotLogMessage
forall sym.
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> AccessorFunctionLoad sym
-> CopilotLogMessage
Log.AccessorFunctionLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals AccessorFunctionLoad sym
a
            Log.GuardFunctionLoadAssertion GuardFunctionLoad sym
a ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer -> Integer -> GuardFunctionLoad sym -> CopilotLogMessage
forall sym.
IsSymExprBuilder sym =>
VerificationStep
-> Integer -> Integer -> GuardFunctionLoad sym -> CopilotLogMessage
Log.GuardFunctionLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals GuardFunctionLoad sym
a
            Log.UnknownFunctionLoadAssertion UnknownFunctionLoad sym
a ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> UnknownFunctionLoad sym
-> CopilotLogMessage
forall sym.
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> UnknownFunctionLoad sym
-> CopilotLogMessage
Log.UnknownFunctionLoadProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals UnknownFunctionLoad sym
a
            Log.LLVMBadBehaviorCheckAssertion LLVMBadBehaviorCheck sym
a ->
              CopilotLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCopilotLogMessage msgs) =>
CopilotLogMessage -> IO ()
Log.sayCopilot (CopilotLogMessage -> IO ()) -> CopilotLogMessage -> IO ()
forall a b. (a -> b) -> a -> b
$
              VerificationStep
-> Integer
-> Integer
-> LLVMBadBehaviorCheck sym
-> CopilotLogMessage
forall sym.
IsSymExprBuilder sym =>
VerificationStep
-> Integer
-> Integer
-> LLVMBadBehaviorCheck sym
-> CopilotLogMessage
Log.LLVMBadBehaviorCheckProofGoal VerificationStep
step Integer
goalIdx Integer
numTotalGoals LLVMBadBehaviorCheck sym
a

          -- Finally, return the current goal index.
          Integer -> IO Integer
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
goalIdx

        ProveConj Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs1 Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs2 -> do
          Integer
goalIdx' <- Integer
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO Integer
go Integer
goalIdx Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs1
          Integer
-> Goals
     (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
-> IO Integer
go (Integer
goalIdx' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Goals
  (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym)
gs2

-- | If a verifier assertion does not have a corresponding 'BoolAnn', then we
-- must use heuristics to guess what kind of assertion it is. These heuristics
-- are not perfect, and we fall back to 'Log.UnknownFunctionLoad' in the event
-- that we cannot figure out a more obvious cause for the assertion.
verifierAssertionHeuristics ::
  IsSymInterface sym =>
  sym ->
  ProgramLoc ->
  Pred sym ->
  Log.VerifierAssertion sym
verifierAssertionHeuristics :: forall sym.
IsSymInterface sym =>
sym -> ProgramLoc -> Pred sym -> VerifierAssertion sym
verifierAssertionHeuristics sym
sym ProgramLoc
loc Pred sym
p
  | Text
"_get" Text -> Text -> Bool
`Text.isSuffixOf` FunctionName -> Text
functionName FunctionName
funName
  = AccessorFunctionLoad sym -> VerifierAssertion sym
forall sym. AccessorFunctionLoad sym -> VerifierAssertion sym
Log.AccessorFunctionLoadAssertion (AccessorFunctionLoad sym -> VerifierAssertion sym)
-> AccessorFunctionLoad sym -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$
    sym
-> ProgramLoc
-> FunctionName
-> Pred sym
-> AccessorFunctionLoad sym
forall sym.
sym
-> ProgramLoc
-> FunctionName
-> Pred sym
-> AccessorFunctionLoad sym
Log.AccessorFunctionLoad sym
sym ProgramLoc
loc FunctionName
funName Pred sym
p

  | Text
"_guard" Text -> Text -> Bool
`Text.isSuffixOf` FunctionName -> Text
functionName FunctionName
funName
  = GuardFunctionLoad sym -> VerifierAssertion sym
forall sym. GuardFunctionLoad sym -> VerifierAssertion sym
Log.GuardFunctionLoadAssertion (GuardFunctionLoad sym -> VerifierAssertion sym)
-> GuardFunctionLoad sym -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$
    sym
-> ProgramLoc -> FunctionName -> Pred sym -> GuardFunctionLoad sym
forall sym.
sym
-> ProgramLoc -> FunctionName -> Pred sym -> GuardFunctionLoad sym
Log.GuardFunctionLoad sym
sym ProgramLoc
loc FunctionName
funName Pred sym
p

  | Bool
otherwise
  = UnknownFunctionLoad sym -> VerifierAssertion sym
forall sym. UnknownFunctionLoad sym -> VerifierAssertion sym
Log.UnknownFunctionLoadAssertion (UnknownFunctionLoad sym -> VerifierAssertion sym)
-> UnknownFunctionLoad sym -> VerifierAssertion sym
forall a b. (a -> b) -> a -> b
$
    sym
-> ProgramLoc
-> FunctionName
-> Pred sym
-> UnknownFunctionLoad sym
forall sym.
sym
-> ProgramLoc
-> FunctionName
-> Pred sym
-> UnknownFunctionLoad sym
Log.UnknownFunctionLoad sym
sym ProgramLoc
loc FunctionName
funName Pred sym
p
  where
    funName :: FunctionName
funName = ProgramLoc -> FunctionName
plFunction ProgramLoc
loc

-- | Pick the most recent 'ProgramLoc' in a trace of locations. If there are
-- no locations available, return a dummy location.
nearestProgramLoc :: [ProgramLoc] -> ProgramLoc
nearestProgramLoc :: [ProgramLoc] -> ProgramLoc
nearestProgramLoc [ProgramLoc]
locs =
  case [ProgramLoc]
locs of
    ProgramLoc
loc:[ProgramLoc]
_ -> ProgramLoc
loc
    [ProgramLoc]
_     -> FunctionName -> Position -> ProgramLoc
mkProgramLoc FunctionName
"<>" Position
InternalPos

-- | A collection of 'IORef's used to accumulate log messages that the verifier
-- may display at the end of verification.
data CopilotLogRefs sym = CopilotLogRefs
  { forall sym.
CopilotLogRefs sym
-> IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef :: !(IORef (Map.Map (BoolAnn sym) (Log.VerifierAssertion sym)))
    -- ^ A map of 'BoolAnn's (i.e., unique numbers) to 'Log.VerifierAssertions'.
  , forall sym. CopilotLogRefs sym -> IORef (LLVMAnnMap sym)
llvmAnnMapRef :: !(IORef (LLVMAnnMap sym))
    -- ^ A map of 'BoolAnn's (i.e., unique numbers) to assertions about checks
    -- for bad behavior in LLVM.

    -- This is kept in a separate 'IORef' for technical reasons, as
    -- @crucible-llvm@'s 'explainFailure' function expects this 'IORef' as an
    -- argument. We could put everything into 'verifierAssertionMapRef', but
    -- that would require some tiresome 'IORef' massaging to make work.
  }

-- | Create a new 'CopilotLogRefs' value.
newCopilotLogRefs :: IsSymInterface sym => IO (CopilotLogRefs sym)
newCopilotLogRefs :: forall sym. IsSymInterface sym => IO (CopilotLogRefs sym)
newCopilotLogRefs = do
  IORef (Map (BoolAnn sym) (VerifierAssertion sym))
vaMapRef <- Map (BoolAnn sym) (VerifierAssertion sym)
-> IO (IORef (Map (BoolAnn sym) (VerifierAssertion sym)))
forall a. a -> IO (IORef a)
newIORef Map (BoolAnn sym) (VerifierAssertion sym)
forall a. Monoid a => a
mempty
  IORef (LLVMAnnMap sym)
laMapRef <- LLVMAnnMap sym -> IO (IORef (LLVMAnnMap sym))
forall a. a -> IO (IORef a)
newIORef LLVMAnnMap sym
forall a. Monoid a => a
mempty
  CopilotLogRefs sym -> IO (CopilotLogRefs sym)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CopilotLogRefs sym -> IO (CopilotLogRefs sym))
-> CopilotLogRefs sym -> IO (CopilotLogRefs sym)
forall a b. (a -> b) -> a -> b
$ CopilotLogRefs
    { verifierAssertionMapRef :: IORef (Map (BoolAnn sym) (VerifierAssertion sym))
verifierAssertionMapRef = IORef (Map (BoolAnn sym) (VerifierAssertion sym))
vaMapRef
    , llvmAnnMapRef :: IORef (LLVMAnnMap sym)
llvmAnnMapRef = IORef (LLVMAnnMap sym)
laMapRef
    }

data CopilotLogging
  = LoggingCrux Log.CruxLogMessage
  | LoggingCruxLLVM Log.CruxLLVMLogMessage
  | LoggingCopilot Log.CopilotLogMessage
  deriving stock (forall x. CopilotLogging -> Rep CopilotLogging x)
-> (forall x. Rep CopilotLogging x -> CopilotLogging)
-> Generic CopilotLogging
forall x. Rep CopilotLogging x -> CopilotLogging
forall x. CopilotLogging -> Rep CopilotLogging x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CopilotLogging -> Rep CopilotLogging x
from :: forall x. CopilotLogging -> Rep CopilotLogging x
$cto :: forall x. Rep CopilotLogging x -> CopilotLogging
to :: forall x. Rep CopilotLogging x -> CopilotLogging
Generic
  deriving anyclass [CopilotLogging] -> Value
[CopilotLogging] -> Encoding
CopilotLogging -> Bool
CopilotLogging -> Value
CopilotLogging -> Encoding
(CopilotLogging -> Value)
-> (CopilotLogging -> Encoding)
-> ([CopilotLogging] -> Value)
-> ([CopilotLogging] -> Encoding)
-> (CopilotLogging -> Bool)
-> ToJSON CopilotLogging
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: CopilotLogging -> Value
toJSON :: CopilotLogging -> Value
$ctoEncoding :: CopilotLogging -> Encoding
toEncoding :: CopilotLogging -> Encoding
$ctoJSONList :: [CopilotLogging] -> Value
toJSONList :: [CopilotLogging] -> Value
$ctoEncodingList :: [CopilotLogging] -> Encoding
toEncodingList :: [CopilotLogging] -> Encoding
$comitField :: CopilotLogging -> Bool
omitField :: CopilotLogging -> Bool
ToJSON

copilotLoggingToSayWhat :: CopilotLogging -> Log.SayWhat
copilotLoggingToSayWhat :: CopilotLogging -> SayWhat
copilotLoggingToSayWhat (LoggingCrux CruxLogMessage
msg) = CruxLogMessage -> SayWhat
Log.cruxLogMessageToSayWhat CruxLogMessage
msg
copilotLoggingToSayWhat (LoggingCruxLLVM CruxLLVMLogMessage
msg) = CruxLLVMLogMessage -> SayWhat
Log.cruxLLVMLogMessageToSayWhat CruxLLVMLogMessage
msg
copilotLoggingToSayWhat (LoggingCopilot CopilotLogMessage
msg) = CopilotLogMessage -> SayWhat
Log.copilotLogMessageToSayWhat CopilotLogMessage
msg

withCopilotLogging ::
  ( ( Log.SupportsCruxLogMessage CopilotLogging
    , Log.SupportsCruxLLVMLogMessage CopilotLogging
    , Log.SupportsCopilotLogMessage CopilotLogging
    ) => computation ) ->
  computation
withCopilotLogging :: forall computation.
((SupportsCruxLogMessage CopilotLogging,
  SupportsCruxLLVMLogMessage CopilotLogging,
  SupportsCopilotLogMessage CopilotLogging) =>
 computation)
-> computation
withCopilotLogging (SupportsCruxLogMessage CopilotLogging,
 SupportsCruxLLVMLogMessage CopilotLogging,
 SupportsCopilotLogMessage CopilotLogging) =>
computation
computation = do
  let ?injectCruxLogMessage = SupportsCruxLogMessage CopilotLogging
CruxLogMessage -> CopilotLogging
LoggingCrux
      ?injectCruxLLVMLogMessage = SupportsCruxLLVMLogMessage CopilotLogging
CruxLLVMLogMessage -> CopilotLogging
LoggingCruxLLVM
      ?injectCopilotLogMessage = SupportsCopilotLogMessage CopilotLogging
CopilotLogMessage -> CopilotLogging
LoggingCopilot
    in computation
(SupportsCruxLogMessage CopilotLogging,
 SupportsCruxLLVMLogMessage CopilotLogging,
 SupportsCopilotLogMessage CopilotLogging) =>
computation
computation

sayTranslationWarning ::
  Log.Logs msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  LLVMTranslationWarning -> IO ()
sayTranslationWarning :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning = CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM (CruxLLVMLogMessage -> IO ())
-> (LLVMTranslationWarning -> CruxLLVMLogMessage)
-> LLVMTranslationWarning
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMTranslationWarning -> CruxLLVMLogMessage
f
  where
    f :: LLVMTranslationWarning -> CruxLLVMLogMessage
f (LLVMTranslationWarning Symbol
s Position
p Text
msg) =
        Text -> Text -> Text -> CruxLLVMLogMessage
Log.TranslationWarning (String -> Text
Text.pack (Doc -> String
forall a. Show a => a -> String
show (Symbol -> Doc
ppSymbol Symbol
s))) (String -> Text
Text.pack (Position -> String
forall a. Show a => a -> String
show Position
p)) Text
msg