{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# 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_, 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)
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.Log as Log
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
, addDurableProofObligation, assert, CrucibleAssumption(..), ppAbortExecReason
, IsSymBackend(..), HasSymInterface(..)
, labeledPred, labeledPredMsg
-- , ProofObligations, proofGoal, goalsToList, labeledPredMsg
)
import Lang.Crucible.Backend.Simple (newSimpleBackend)
import Lang.Crucible.CFG.Core (AnyCFG(..), cfgArgTypes, cfgReturnType)
import Lang.Crucible.CFG.Common ( freshGlobalVar )
import Lang.Crucible.FunctionHandle (newHandleAllocator)
import Lang.Crucible.Simulator
( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..)
, defaultAbortHandler, runOverrideSim, partialValue, gpValue
, GlobalVar, executeCrucible, OverrideSim, 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
( FloatModeRepr(..), 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.Solver.Z3 (z3Adapter)
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 = verifyWithOptions defaultVerifierOptions
-- | Options for configuring the behavior of the verifier.
data VerifierOptions = VerifierOptions
{ verbosity :: Verbosity
-- ^ How much output the verifier should produce.
, 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.
, 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.
} deriving stock 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.
defaultVerifierOptions :: VerifierOptions
defaultVerifierOptions = VerifierOptions
{ verbosity = Default
, assumePartialSideConds = False
, logSmtInteractions = False
}
-- | Like 'defaultVerifierOptions', except that the verifier will assume side
-- conditions related to partial operations used in the Copilot spec.
sideCondVerifierOptions :: VerifierOptions
sideCondVerifierOptions = 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 (Eq, Ord, Show)
-- | Like 'verify', but with 'VerifierOptions' to more finely control the
-- verifier's behavior.
verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()
verifyWithOptions opts csettings0 properties prefix spec =
withCopilotLogging $
do -- munge options structures into the necessary forms
(ocfg, cruxOpts, llvmOpts, csettings, csrc) <- computeConfiguration opts csettings0 prefix
let ?outputConfig = ocfg
-- Compile the Copilot spec into C source code, using
-- preexisting Copilot library calls.
compileWith csettings prefix spec
Log.sayCopilot $ Log.GeneratedCFile csrc
-- Compile the C source into LLVM bitcode, using preexisting
-- Crux library calls.
bcFile <- genBitCode cruxOpts llvmOpts
Log.sayCopilot $ Log.CompiledBitcodeFile prefix bcFile
-- Run the main verification procedure
verifyBitcode opts csettings properties spec cruxOpts llvmOpts csrc 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 opts csettings0 prefix =
do ocfg1 <- defaultOutputConfig copilotLoggingToSayWhat
let quiet = verbosity opts == Quiet
let ocfg2 mbOutputOpts = (ocfg1 mbOutputOpts) { Log._quiet = quiet }
llvmcfg <- llvmCruxConfig
let cfg = cfgJoin cruxOptions llvmcfg
-- TODO, load from an actual configuration file?
fileOpts <- fromFile "copilot-verifier" cfg Nothing
(cruxOpts0, llvmOpts0) <- foldM fromEnv fileOpts (cfgEnv cfg)
let odir0 = cSettingsOutputDirectory csettings0
let odir = -- A bit grimy, but this corresponds to how crux-llvm sets
-- its output directory.
if odir0 == "."
then "results" </> prefix
else odir0
let csettings = csettings0{ cSettingsOutputDirectory = odir }
let csrc = odir </> prefix ++ ".c"
let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc]
, outputOptions =
(outputOptions cruxOpts0)
{ quietMode = quiet
, simVerbose = if verbosity opts > Default
then 2
else 0
}
}
let ?outputConfig = ocfg2 (Just (outputOptions cruxOpts1))
cruxOpts2 <- postprocessOptions 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 = llvmOpts0
{ optLevel = 0
, clangOpts = "-ffp-contract=off" : clangOpts llvmOpts0
}
(cruxOpts3, llvmOpts2) <- processLLVMOptions (cruxOpts2, llvmOpts1)
let ocfg3 = ocfg2 (Just (outputOptions cruxOpts3))
return (ocfg3, cruxOpts3, llvmOpts2, csettings, 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 opts csettings properties spec cruxOpts llvmOpts cFile bcFile =
do -- Set up the expression builder and symbolic backend
halloc <- newHandleAllocator
sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator
bak <- newSimpleBackend sym
-- turn on hash-consing
startCaching sym
-- capture LLVM side-condition information for use in error reporting
clRefs <- newCopilotLogRefs
let ?recordLLVMAnnotation = recordLLVMAnnotation clRefs
-- Set up the solver to use for verification. Right now we hard-code this to Z3.
let adapters = [z3Adapter] -- TODO? configurable
extendConfig (solver_adapter_config_options z3Adapter) (getConfiguration sym)
-- Set up the Crucible/LLVM simulation context
memVar <- mkMemVar "llvm_memory" halloc
let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)
{ printHandle = view Log.outputHandle ?outputConfig }
-- Load and translate the input LLVM module
llvmMod <- parseLLVM bcFile
Some trans <-
let ?transOpts = transOpts llvmOpts
in translateModule halloc memVar llvmMod
Log.sayCopilot 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 = trans ^. transContext
let ?lc = llvmCtxt ^. llvmTypeCtx
let ?memOpts = memOpts llvmOpts
let ?intrinsicsOpts = intrinsicsOpts llvmOpts
llvmPtrWidth llvmCtxt $ \ptrW ->
withPtrWidth ptrW $
do -- Compute the LLVM memory state with global variables allocated
-- but not initialized
emptyMem <- initializeAllMemory bak llvmCtxt llvmMod
-- Compute the LLVM memory state with global variables initialized
-- to their initial values.
initialMem <- populateAllGlobals bak (trans ^. globalInitMap) emptyMem
-- Use the Copilot spec directly to compute the symbolic states
-- necessary to carry out the states of the bisimulation proof.
Log.sayCopilot Log.GeneratingProofState
proofStateBundle <- CW4.computeBisimulationProofBundle sym properties spec
-- First check that the initial state of the program matches the starting
-- segment of the associated Copilot streams.
let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts
initGoals <-
verifyInitialState cruxOptsInit adapters clRefs simctx initialMem
(CW4.initialStreamState proofStateBundle)
-- Now, the real meat. Carry out the bisimulation step of the proof.
let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts
bisimGoals <-
verifyStepBisimulation opts cruxOptsTrans adapters csettings
clRefs simctx llvmMod trans memVar initialMem proofStateBundle
Log.sayCopilot $ Log.SuccessfulProofSummary cFile initGoals 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.
when (verbosity opts < Noisy) $
Log.sayCopilot Log.NoisyVerbositySuggestion
where
-- 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 template cruxOpts'
| logSmtInteractions opts
= cruxOpts'
{ offlineSolverOutput = Just $ outDir cruxOpts' </> template <.> "smt2" }
| otherwise
= cruxOpts'
-- | Capture LLVM side-condition information for use in error reporting.
recordLLVMAnnotation ::
IsSymInterface sym =>
CopilotLogRefs sym ->
CallStack ->
BoolAnn sym ->
BadBehavior sym ->
IO ()
recordLLVMAnnotation clRefs stk bann bb =
modifyIORef' (llvmAnnMapRef clRefs) (Map.insert bann (stk, 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 cruxOpts adapters clRefs simctx mem initialState =
withBackend simctx $ \bak ->
do Log.sayCopilot $ Log.ComputingConditions Log.InitialState
frm <- pushAssumptionFrame bak
assertStateRelation bak clRefs mem initialState
popUntilAssumptionFrame bak frm
Log.sayCopilot $ Log.ProvingConditions Log.InitialState
proveObls cruxOpts adapters clRefs Log.InitialState 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 opts cruxOpts adapters csettings clRefs simctx llvmMod modTrans memVar mem prfbundle =
withBackend simctx $ \bak ->
do Log.sayCopilot $ Log.ComputingConditions Log.StepBisimulation
frm <- pushAssumptionFrame bak
do -- set up the memory image
mem' <- setupPrestate bak mem prfbundle
-- sanity check, verify that we set up the memory in the expected relation
assertStateRelation bak clRefs mem' (CW4.preStreamState prfbundle)
-- set up trigger guard global variables
let halloc = simHandleAllocator simctx
-- See Note [Global variables for trigger functions]
let prepTrigger (nm, guard, _) =
do gv <- freshGlobalVar halloc (Text.pack (nm ++ "_called")) NatRepr
return (nm, gv, guard)
triggerGlobals <- mapM prepTrigger (CW4.triggerState prfbundle)
-- execute the step function
let overrides = zipWith (triggerOverride clRefs) triggerGlobals (CW4.triggerState prfbundle)
mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle)
-- assert the poststate is in the relation
assertStateRelation bak clRefs mem'' (CW4.postStreamState prfbundle)
popUntilAssumptionFrame bak frm
Log.sayCopilot $ Log.ProvingConditions Log.StepBisimulation
proveObls cruxOpts adapters clRefs Log.StepBisimulation 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 arch (RegEntry sym Mem) EmptyCtx Mem
triggerOverride clRefs (_,triggerGlobal,_) (nm, _guard, args) =
let args' = map toTypeRepr args in
case Ctx.fromList args' of
Some argCtx ->
basic_llvm_override $
LLVMOverride decl argCtx UnitRepr $
\memOps bak calledArgs ->
do let sym = backendGetSym bak
modifyGlobal triggerGlobal $ \count -> do
-- See Note [Global variables for trigger functions]
countPlusOne <- liftIO $ do
one <- natLit sym 1
natAdd sym count one
pure ((), countPlusOne)
mem <- readGlobal memOps
liftIO $ checkArgs bak mem (toListFC Some calledArgs) args
return ()
where
decl = L.Declare
{ L.decLinkage = Nothing
, L.decVisibility = Nothing
, L.decRetType = L.PrimType L.Void
, L.decName = L.Symbol nm
, L.decArgs = map llvmArgTy args
, L.decVarArgs = False
, L.decAttrs = []
, L.decComdat = 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 ctp, _) = llvmTypeAsRepr (copilotTypeToMemTypeCompositePtr (llvmDataLayout ?lc) ctp) Some
llvmArgTy (Some ctp, _) = copilotTypeToLLVMTypeCompositePtr ctp
checkArgs :: forall bak. IsSymBackend sym bak =>
bak -> MemImpl sym -> [Some (RegEntry sym)] -> [(Some Type, CW4.XExpr sym)] -> IO ()
checkArgs bak mem = loop (0::Integer)
where
loop i (x:xs) ((ctp,v):vs) = checkArg bak mem i x ctp v >> loop (i+1) xs vs
loop _ [] [] = return ()
loop _ _ _ = fail $ "Argument list mismatch in " ++ nm
checkArg :: forall bak. IsSymBackend sym bak =>
bak -> MemImpl sym -> Integer -> Some (RegEntry sym) -> Some Type -> CW4.XExpr sym -> IO ()
checkArg bak mem i (Some (RegEntry tp v)) (Some ctp) x =
do let sym = backendGetSym bak
eq <- computeEqualVals bak clRefs mem ctp x tp v
(ann, eq') <- annotateTerm sym eq
let shortmsg = "Trigger " ++ show nm ++ " argument " ++ show i
let longmsg = show (printSymExpr eq')
let rsn = AssertFailureSimError shortmsg longmsg
loc <- getCurrentProgramLoc sym
modifyIORef' (verifierAssertionMapRef clRefs)
$ Map.insert (BoolAnn ann)
$ Log.TriggerArgumentEqualityAssertion
$ Log.SomeSome
$ Log.TriggerArgumentEquality sym loc nm i ctp x tp v
addDurableProofObligation bak (LabeledPred eq' (SimError loc 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 arch (RegEntry sym Mem) EmptyCtx Mem] ->
[Pred sym] {- User-provided property assumptions -} ->
[Pred sym] {- Side conditions related to partial operations -} ->
IO (MemImpl sym)
executeStep opts csettings clRefs simctx memVar mem llvmmod modTrans triggerGlobals triggerOverrides assums sideConds =
do globSt <- foldM setupTrigger (llvmGlobals memVar mem) triggerGlobals
let initSt = InitialState simctx globSt defaultAbortHandler memRepr $
runOverrideSim memRepr runStep
res <- executeCrucible [] initSt
case res of
FinishedResult _ pr -> return (pr^.partialValue.gpValue.to regValue)
AbortedResult _ abortRes -> fail $ show $ ppAbortedResult abortRes
TimeoutResult{} -> fail "simulation timed out!"
where
-- See Note [Global variables for trigger functions]
setupTrigger gs (_,gv,_) = do
zero <- liftIO $ natLit sym 0
pure $ insertGlobal gv zero gs
llvm_ctx = modTrans ^. transContext
stepName = cSettingsStepFunctionName csettings
sym = simctx^.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 = mkProgramLoc "<>" InternalPos
assumeProperty b =
withBackend simctx $ \bak ->
addAssumption bak (GenericAssumption dummyLoc "Property assumption" b)
assumeSideCond b =
withBackend simctx $ \bak ->
addAssumption bak (GenericAssumption dummyLoc "Side condition for partial operation" b)
ppAbortedResult :: AbortedResult sym ext -> PP.Doc ann
ppAbortedResult abortRes =
case gatherReasons abortRes of
reason :| [] -> reason
reasons -> PP.vcat $ "Simulation aborted for multiple reasons."
: NE.toList reasons
gatherReasons :: AbortedResult sym ext -> NonEmpty (PP.Doc ann)
gatherReasons (AbortedExec rsn _) =
PP.vcat ["Simulation aborted!", ppAbortExecReason rsn] :| []
gatherReasons (AbortedExit ec) =
PP.vcat ["Simulation called exit!", PP.viaShow ec] :| []
gatherReasons (AbortedBranch _ _ t f) =
gatherReasons t <> gatherReasons f
-- Simulator entry point
runStep :: OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)
runStep =
do -- set up built-in functions and trigger overrides
register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx
-- set up functions defined in the module
registerLazyModule sayTranslationWarning modTrans
-- make any property assumptions
liftIO (mapM_ assumeProperty assums)
-- assume side conditions related to partial operations
when (assumePartialSideConds opts) $ liftIO $
mapM_ assumeSideCond sideConds
-- look up and call the step function
mbCfg <- liftIO $ getTranslatedCFG modTrans (L.Symbol stepName)
() <- case mbCfg of
Just (_, AnyCFG anyCfg, warns) -> do
liftIO $ mapM_ sayTranslationWarning warns
case (cfgArgTypes anyCfg, cfgReturnType anyCfg) of
(Empty, UnitRepr) -> regValue <$> callCFG anyCfg emptyRegMap
_ -> fail $ unwords [show stepName, "should take no arguments and return void"]
Nothing -> fail $ unwords ["Could not find step function named", show stepName]
-- Assert that the trigger functions were called exactly once iff the
-- associated guard condition was true.
-- See Note [Global variables for trigger functions].
forM_ triggerGlobals $ \(nm, gv, guard) ->
do expectedCount <- liftIO $ do
one <- natLit sym 1
zero <- natLit sym 0
natIte sym guard one zero
actualCount <- readGlobal gv
eq <- liftIO $ natEq sym expectedCount actualCount
(ann, eq') <- liftIO $ annotateTerm sym eq
let shortmsg = "Trigger guard equality condition: " ++ show nm
let longmsg = show (printSymExpr eq')
let rsn = AssertFailureSimError shortmsg longmsg
liftIO
$ modifyIORef' (verifierAssertionMapRef clRefs)
$ Map.insert (BoolAnn ann)
$ Log.TriggersInvokedCorrespondinglyAssertion
$ Log.TriggersInvokedCorrespondingly dummyLoc nm expectedCount actualCount
withBackend simctx $ \bak ->
liftIO $ addDurableProofObligation bak (LabeledPred eq' (SimError dummyLoc rsn))
-- return the final state of the memory
readGlobal 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 bak mem0 prfbundle =
do mem' <- foldM setupStreamState mem0 (CW4.streamState (CW4.preStreamState prfbundle))
foldM setupExternalInput mem' (CW4.externalInputs prfbundle)
where
sym = backendGetSym bak
sizeTStorage :: StorageType
sizeTStorage = bitvectorType (bitsToBytes (intValue ?ptrWidth))
setupExternalInput mem (nm, Some ctp, v) =
do -- Compute LLVM/Crucible type information from the Copilot type
let memTy = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
let typeAlign = memTypeAlign (llvmDataLayout ?lc) memTy
stType <- toStorableType memTy
Some typeRepr <- return (llvmTypeAsRepr memTy Some)
-- resolve the global variable to a pointers
ptrVal <- doResolveGlobal bak mem (L.Symbol nm)
-- write the value into the global
regVal <- copilotExprToRegValue sym v typeRepr
doStore bak mem ptrVal typeRepr stType typeAlign regVal
setupStreamState mem (nm, Some ctp, vs) =
do -- TODO, should get these from somewhere inside copilot instead of building these names directly
let idxName = "s" ++ show nm ++ "_idx"
let bufName = "s" ++ show nm
let buflen = genericLength vs :: Integer
-- Compute LLVM/Crucible type information from the Copilot type
let memTy = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
let typeLen = memTypeSize (llvmDataLayout ?lc) memTy
let typeAlign = memTypeAlign (llvmDataLayout ?lc) memTy
stType <- toStorableType memTy
Some typeRepr <- return (llvmTypeAsRepr memTy Some)
-- Resolve the global names into base pointers
idxPtr <- doResolveGlobal bak mem (L.Symbol idxName)
bufPtr <- doResolveGlobal bak mem (L.Symbol bufName)
-- Create a fresh index value in the proper range
idxVal <- freshBoundedBV sym (safeSymbol idxName) ?ptrWidth
(Just 0) (Just (fromIntegral (buflen - 1)))
idxVal' <- llvmPointer_bv sym idxVal
-- store the index value in the correct location
let sizeTAlign = memTypeAlign (llvmDataLayout ?lc) (IntType (natValue ?ptrWidth))
mem' <- doStore bak mem idxPtr (LLVMPointerRepr ?ptrWidth) sizeTStorage sizeTAlign idxVal'
buflen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)
typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))
-- Write each value of the stream ring buffer into its correct location
flip execStateT mem' $
forM_ (zip vs [0 ..]) $ \(v,i) ->
do ptrVal <- lift $
do x1 <- bvAdd sym idxVal =<< bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i)
x2 <- bvUrem sym x1 buflen'
x3 <- bvMul sym x2 typeLen'
ptrAdd sym ?ptrWidth bufPtr x3
regVal <- lift $ copilotExprToRegValue sym v typeRepr
StateT $ \m ->
do m' <- doStore bak m ptrVal typeRepr stType typeAlign regVal
return ((),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 ->
CW4.BisimulationProofState sym ->
IO ()
assertStateRelation bak clRefs mem prfst =
-- For each stream in the proof state, assert that the
-- generated ring buffer global contains the corresponding
-- values.
forM_ (CW4.streamState prfst) assertStreamState
where
sym = backendGetSym bak
sizeTStorage :: StorageType
sizeTStorage = bitvectorType (bitsToBytes (intValue ?ptrWidth))
assertStreamState (nm, Some ctp, vs) =
do -- TODO, should get these from somewhere inside copilot instead of building these names directly
let idxName = "s" ++ show nm ++ "_idx"
let bufName = "s" ++ show nm
let buflen = genericLength vs :: Integer
-- Compute LLVM/Crucible type information from the Copilot type
let memTy = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
let typeLen = memTypeSize (llvmDataLayout ?lc) memTy
let typeAlign = memTypeAlign (llvmDataLayout ?lc) memTy
stType <- toStorableType memTy
Some typeRepr <- return (llvmTypeAsRepr memTy Some)
-- Resolve the global names into base pointers
idxPtr <- doResolveGlobal bak mem (L.Symbol idxName)
bufPtr <- doResolveGlobal bak mem (L.Symbol bufName)
-- read the value of the ring buffer index
let sizeTAlign = memTypeAlign (llvmDataLayout ?lc) (IntType (natValue ?ptrWidth))
(bannIdxVal, pIdxVal, idxVal) <-
doLoadWithAnn bak mem idxPtr sizeTStorage (LLVMPointerRepr ?ptrWidth) sizeTAlign
idxVal' <- projectLLVM_bv bak idxVal
locIdxVal <- getCurrentProgramLoc sym
modifyIORef' (verifierAssertionMapRef clRefs)
$ Map.insert bannIdxVal
$ Log.RingBufferIndexLoadAssertion
$ Log.RingBufferIndexLoad sym locIdxVal (Text.pack idxName) pIdxVal
buflen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)
typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))
-- For each value in the stream description, read a corresponding value from
-- memory and assert that they are equal.
forM_ (zip vs [0 ..]) $ \(v,i) ->
do ptrVal <-
do x1 <- bvAdd sym idxVal' =<< bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i)
x2 <- bvUrem sym x1 buflen'
x3 <- bvMul sym x2 typeLen'
ptrAdd sym ?ptrWidth bufPtr x3
(bannv', pv', v') <- doLoadWithAnn bak mem ptrVal stType typeRepr typeAlign
locv' <- getCurrentProgramLoc sym
let bufNameT = Text.pack bufName
modifyIORef' (verifierAssertionMapRef clRefs)
$ Map.insert bannv'
$ Log.RingBufferLoadAssertion
$ Log.SomeSome
$ Log.RingBufferLoad sym locv' bufNameT i buflen ctp typeRepr pv'
eq <- computeEqualVals bak clRefs mem ctp v typeRepr v'
(ann, eq') <- annotateTerm sym eq
let shortmsg = "State equality condition: " ++ show nm ++ " index value " ++ show i
let longmsg = show (printSymExpr eq')
let rsn = AssertFailureSimError shortmsg longmsg
let loc = mkProgramLoc "<>" InternalPos
modifyIORef' (verifierAssertionMapRef clRefs)
$ Map.insert (BoolAnn ann)
$ Log.StreamValueEqualityAssertion
$ Log.SomeSome
$ Log.StreamValueEquality sym loc bufNameT i buflen ctp v typeRepr v'
addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn))
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 sym = loop
where
loop :: forall tp'. CW4.XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')
loop (CW4.XBool b) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @1) =
llvmPointer_bv sym =<< predToBV sym b knownRepr
loop (CW4.XBool b) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =
llvmPointer_bv sym =<< predToBV sym b knownRepr
loop (CW4.XInt8 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =
llvmPointer_bv sym x
loop (CW4.XInt16 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @16) =
llvmPointer_bv sym x
loop (CW4.XInt32 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @32) =
llvmPointer_bv sym x
loop (CW4.XInt64 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @64) =
llvmPointer_bv sym x
loop (CW4.XWord8 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =
llvmPointer_bv sym x
loop (CW4.XWord16 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @16) =
llvmPointer_bv sym x
loop (CW4.XWord32 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @32) =
llvmPointer_bv sym x
loop (CW4.XWord64 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @64) =
llvmPointer_bv sym x
loop (CW4.XFloat x) (FloatRepr SingleFloatRepr) = return x
loop (CW4.XDouble x) (FloatRepr DoubleFloatRepr) = return x
loop CW4.XEmptyArray (VectorRepr _tpr) =
pure V.empty
loop (CW4.XArray xs) (VectorRepr tpr) =
V.generateM (PVec.lengthInt xs) (\i -> loop (PVec.elemAtUnsafe i xs) tpr)
loop (CW4.XStruct xs) (StructRepr ctx) =
Ctx.traverseWithIndex
(\i tpr -> RV <$> loop (xs !! Ctx.indexVal i) tpr)
ctx
loop x tpr =
fail $ unlines ["Mismatch between Copilot value and crucible value", show x, show 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 bak clRefs mem = loop
where
sym = backendGetSym bak
loop :: forall tp' a'. Type a' -> CW4.XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)
loop Bool (CW4.XBool b) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @1) =
isEq sym b =<< bvIsNonzero sym =<< projectLLVM_bv bak v
loop Bool (CW4.XBool b) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =
isEq sym b =<< bvIsNonzero sym =<< projectLLVM_bv bak v
loop Int8 (CW4.XInt8 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =
bvEq sym x =<< projectLLVM_bv bak v
loop Int16 (CW4.XInt16 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @16) =
bvEq sym x =<< projectLLVM_bv bak v
loop Int32 (CW4.XInt32 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @32) =
bvEq sym x =<< projectLLVM_bv bak v
loop Int64 (CW4.XInt64 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @64) =
bvEq sym x =<< projectLLVM_bv bak v
loop Word8 (CW4.XWord8 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =
bvEq sym x =<< projectLLVM_bv bak v
loop Word16 (CW4.XWord16 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @16) =
bvEq sym x =<< projectLLVM_bv bak v
loop Word32 (CW4.XWord32 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @32) =
bvEq sym x =<< projectLLVM_bv bak v
loop Word64 (CW4.XWord64 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @64) =
bvEq sym x =<< projectLLVM_bv bak v
loop Float (CW4.XFloat x) (FloatRepr SingleFloatRepr) v = iFloatEq @_ @SingleFloat sym x v
loop Double (CW4.XDouble x) (FloatRepr DoubleFloatRepr) v = iFloatEq @_ @DoubleFloat sym x v
loop (Array _ctp) CW4.XEmptyArray (VectorRepr _tpr) vs =
pure $ backendPred sym $ V.null vs
loop (Array ctp) (CW4.XArray xs) (VectorRepr tpr) vs
| PVec.lengthInt xs == V.length vs
= V.ifoldM (\pAcc i v -> andPred sym pAcc =<< loop ctp (PVec.elemAtUnsafe i xs) tpr v)
(truePred sym) vs
| otherwise
= pure (falsePred sym)
loop (Struct struct) (CW4.XStruct xs) (StructRepr ctx) vs
| length copilotVals == Ctx.sizeInt (Ctx.size vs)
= ifoldlMFC (\i pAcc tpr ->
case copilotVals !! Ctx.indexVal i of
(Value ctp _, x) ->
andPred sym pAcc =<< loop ctp x tpr (unRV (vs Ctx.! i)))
(truePred sym) ctx
| otherwise
= pure (falsePred sym)
where
copilotVals :: [(Value a', CW4.XExpr sym)]
copilotVals = zip (toValues struct) 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 ctp x PtrRepr v =
do let memTy = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp
typeAlign = memTypeAlign (llvmDataLayout ?lc) memTy
stp <- toStorableType memTy
llvmTypeAsRepr memTy $ \tpr ->
do loc <- getCurrentProgramLoc sym
(bann, p, regVal) <- doLoadWithAnn bak mem v stp tpr typeAlign
modifyIORef' (verifierAssertionMapRef clRefs)
$ Map.insert bann
$ Log.PointerArgumentLoadAssertion
$ Log.SomeSome
$ Log.PointerArgumentLoad sym loc ctp tpr p
loop ctp x tpr regVal
loop _ctp x tpr _v =
fail $ unlines ["Mismatch between Copilot value and crucible value", show x, show 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 dl = loop
where
loop :: forall t. CT.Type t -> MemType
loop CT.Bool = i1
loop CT.Int8 = i8
loop CT.Int16 = i16
loop CT.Int32 = i32
loop CT.Int64 = i64
loop CT.Word8 = i8
loop CT.Word16 = i16
loop CT.Word32 = i32
loop CT.Word64 = i64
loop CT.Float = FloatType
loop CT.Double = DoubleType
loop t0@(CT.Array tp) =
let len = fromIntegral (typeLength t0) in
ArrayType len (copilotTypeToMemTypeBool8 dl tp)
loop (CT.Struct v) =
StructType (mkStructInfo dl False (map val (CT.toValues v)))
val :: forall t. CT.Value t -> MemType
val (CT.Value tp _) = copilotTypeToMemTypeBool8 dl 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 _dl CT.Bool = i8
copilotTypeToMemTypeBool8 dl tp = copilotTypeToMemType dl 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 dl (CT.Array tp) =
PtrType (MemType (copilotTypeToMemTypeBool8 dl tp))
copilotTypeToMemTypeCompositePtr _dl (CT.Struct struct) =
PtrType (Alias (copilotStructIdent struct))
copilotTypeToMemTypeCompositePtr dl tp = copilotTypeToMemType dl 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 = loop
where
loop :: forall t. CT.Type t -> L.Type
loop CT.Bool = L.PrimType (L.Integer 1)
loop CT.Int8 = L.PrimType (L.Integer 8)
loop CT.Int16 = L.PrimType (L.Integer 16)
loop CT.Int32 = L.PrimType (L.Integer 32)
loop CT.Int64 = L.PrimType (L.Integer 64)
loop CT.Word8 = L.PrimType (L.Integer 8)
loop CT.Word16 = L.PrimType (L.Integer 16)
loop CT.Word32 = L.PrimType (L.Integer 32)
loop CT.Word64 = L.PrimType (L.Integer 64)
loop CT.Float = L.PrimType (L.FloatType L.Float)
loop CT.Double = L.PrimType (L.FloatType L.Double)
loop t0@(CT.Array tp) =
let len = fromIntegral (typeLength t0) in
L.Array len (copilotTypeToLLVMTypeBool8 tp)
loop (CT.Struct 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.
L.Alias (copilotStructIdent 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 CT.Bool = L.PrimType (L.Integer 8)
copilotTypeToLLVMTypeBool8 tp = copilotTypeToLLVMType 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 (CT.Array tp) =
L.PtrTo (copilotTypeToLLVMTypeBool8 tp)
copilotTypeToLLVMTypeCompositePtr (CT.Struct struct) =
L.PtrTo (L.Alias (copilotStructIdent struct))
copilotTypeToLLVMTypeCompositePtr tp = copilotTypeToLLVMType tp
-- | Given a struct @s@, construct the name @struct.s@ as an LLVM identifier.
copilotStructIdent :: Struct a => a -> L.Ident
copilotStructIdent struct = L.Ident $ "struct." ++ typeName 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 also returning the 'BoolAnn' and
-- 'Pred' asserting the validity of the load.
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 bak mem ptr valType tpr alignment = do
partLLVMVal <- loadRaw sym mem ptr valType alignment
(bann, p, llvmVal) <- assertSafeWithAnn bak partLLVMVal
regVal <- unpackMemValue sym tpr llvmVal
pure (bann, p, regVal)
where
sym = backendGetSym bak
-- | Like @crucible-llvm@'s @assertSafe@, but also returning the 'BoolAnn' and
-- 'Pred' corresponding the assertion.
assertSafeWithAnn ::
IsSymBackend sym bak =>
bak ->
PartLLVMVal sym ->
IO (BoolAnn sym, Pred sym, LLVMVal sym)
assertSafeWithAnn bak partVal =
case partVal of
NoErr p v -> do
(ann, p') <- annotateTerm sym p
assert bak p' rsn
return (BoolAnn ann, p', v)
Err p -> do
loc <- getCurrentProgramLoc sym
let err = SimError loc rsn
(_ann, p') <- annotateTerm sym p
addProofObligation bak (LabeledPred p' err)
abortExecBecause (AssertionFailure err)
where
rsn = AssertFailureSimError "Error during memory load" ""
sym = backendGetSym 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 cruxOpts adapters clRefs step simctx =
withBackend simctx $ \bak ->
do let sym = backendGetSym bak
obls <- getProofObligations bak
clearProofObligations bak
-- mapM_ (print . ppSimError) (summarizeObls sym obls)
vaMap <- readIORef $ verifierAssertionMapRef clRefs
let laMapRef = llvmAnnMapRef clRefs
laMap <- readIORef laMapRef
results <- proveGoalsOffline adapters cruxOpts simctx (explainFailure sym laMapRef) obls
presentResults sym vaMap laMap step 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 sym vaMap laMap step (num, goals)
| numTotalGoals == 0
= do Log.sayCopilot Log.AllGoalsProved
pure 0
-- All goals were proven
| numProvedGoals == numTotalGoals
= do traverse_ (logVerifierAssertions sym vaMap laMap step num) goals
printGoals
pure numProvedGoals
-- There were some unproved goals, so fail with exit code 1
| otherwise
= do printGoals
exitFailure
where
numTotalGoals = totalProcessedGoals num
numProvedGoals = provedGoals num
printGoals =
do Log.sayCopilot $ Log.OnlySomeGoalsProved numProvedGoals numTotalGoals
goals' <- provedGoalsTree sym goals
case goals' of
Just g -> Log.logGoal g
Nothing -> 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 sym vaMap laMap step num goals = void $ go 0 goals
where
numTotalGoals = totalProcessedGoals num
go :: Integer ->
Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->
IO Integer
go goalIdx gs =
case gs of
Assuming _ gs' ->
go goalIdx gs'
Prove (gl, locs, _) -> do
let p = gl^.labeledPred
nearestLoc = nearestProgramLoc locs
-- First, obtain the verifier assertion.
va <- case getAnnotation sym p of
-- If the assertion has a BoolAnn, look it up in the assertion maps
-- that we have accumulated during verification.
Just ann
| Just va <- Map.lookup (BoolAnn ann) vaMap
-> pure va
| Just (stk, bb) <- Map.lookup (BoolAnn ann) laMap
-> pure $ Log.LLVMBadBehaviorCheckAssertion
$ Log.LLVMBadBehaviorCheck sym nearestLoc stk bb p
| otherwise
-> fail $ unlines
[ "Cannot find BoolAnn for assertion"
, show $ gl^.labeledPredMsg
, show $ printSymExpr p
]
-- If the assertion does not have a BoolAnn, fall back to using
-- heuristics to guess what kind of assertion it is.
Nothing -> pure $ verifierAssertionHeuristics sym nearestLoc p
-- Log the assertion.
case va of
Log.StreamValueEqualityAssertion (Log.SomeSome a) ->
Log.sayCopilot $
Log.StreamValueEqualityProofGoal step goalIdx numTotalGoals a
Log.TriggersInvokedCorrespondinglyAssertion a ->
Log.sayCopilot $
Log.TriggersInvokedCorrespondinglyProofGoal step goalIdx numTotalGoals a
Log.TriggerArgumentEqualityAssertion (Log.SomeSome a) ->
Log.sayCopilot $
Log.TriggerArgumentEqualityProofGoal step goalIdx numTotalGoals a
Log.RingBufferLoadAssertion (Log.SomeSome a) ->
Log.sayCopilot $
Log.RingBufferLoadProofGoal step goalIdx numTotalGoals a
Log.RingBufferIndexLoadAssertion a ->
Log.sayCopilot $
Log.RingBufferIndexLoadProofGoal step goalIdx numTotalGoals a
Log.PointerArgumentLoadAssertion (Log.SomeSome a) ->
Log.sayCopilot $
Log.PointerArgumentLoadProofGoal step goalIdx numTotalGoals a
Log.AccessorFunctionLoadAssertion a ->
Log.sayCopilot $
Log.AccessorFunctionLoadProofGoal step goalIdx numTotalGoals a
Log.GuardFunctionLoadAssertion a ->
Log.sayCopilot $
Log.GuardFunctionLoadProofGoal step goalIdx numTotalGoals a
Log.UnknownFunctionLoadAssertion a ->
Log.sayCopilot $
Log.UnknownFunctionLoadProofGoal step goalIdx numTotalGoals a
Log.LLVMBadBehaviorCheckAssertion a ->
Log.sayCopilot $
Log.LLVMBadBehaviorCheckProofGoal step goalIdx numTotalGoals a
-- Finally, return the current goal index.
pure goalIdx
ProveConj gs1 gs2 -> do
goalIdx' <- go goalIdx gs1
go (goalIdx' + 1) 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 sym loc p
| "_get" `Text.isSuffixOf` functionName funName
= Log.AccessorFunctionLoadAssertion $
Log.AccessorFunctionLoad sym loc funName p
| "_guard" `Text.isSuffixOf` functionName funName
= Log.GuardFunctionLoadAssertion $
Log.GuardFunctionLoad sym loc funName p
| otherwise
= Log.UnknownFunctionLoadAssertion $
Log.UnknownFunctionLoad sym loc funName p
where
funName = plFunction 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 locs =
case locs of
loc:_ -> loc
_ -> mkProgramLoc "<>" 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
{ verifierAssertionMapRef :: !(IORef (Map.Map (BoolAnn sym) (Log.VerifierAssertion sym)))
-- ^ A map of 'BoolAnn's (i.e., unique numbers) to 'Log.VerifierAssertions'.
, 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 = do
vaMapRef <- newIORef mempty
laMapRef <- newIORef mempty
pure $ CopilotLogRefs
{ verifierAssertionMapRef = vaMapRef
, llvmAnnMapRef = laMapRef
}
data CopilotLogging
= LoggingCrux Log.CruxLogMessage
| LoggingCruxLLVM Log.CruxLLVMLogMessage
| LoggingCopilot Log.CopilotLogMessage
deriving stock Generic
deriving anyclass ToJSON
copilotLoggingToSayWhat :: CopilotLogging -> Log.SayWhat
copilotLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
copilotLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
copilotLoggingToSayWhat (LoggingCopilot msg) = Log.copilotLogMessageToSayWhat msg
withCopilotLogging ::
( ( Log.SupportsCruxLogMessage CopilotLogging
, Log.SupportsCruxLLVMLogMessage CopilotLogging
, Log.SupportsCopilotLogMessage CopilotLogging
) => computation ) ->
computation
withCopilotLogging computation = do
let ?injectCruxLogMessage = LoggingCrux
?injectCruxLLVMLogMessage = LoggingCruxLLVM
?injectCopilotLogMessage = LoggingCopilot
in computation
sayTranslationWarning ::
Log.Logs msgs =>
Log.SupportsCruxLLVMLogMessage msgs =>
LLVMTranslationWarning -> IO ()
sayTranslationWarning = Log.sayCruxLLVM . f
where
f (LLVMTranslationWarning s p msg) =
Log.TranslationWarning (Text.pack (show (ppSymbol s))) (Text.pack (show p)) msg