{-|
Module      : Lang.Crucible.Backend
Copyright   : (c) Galois, Inc 2014-2022
License     : BSD3
Maintainer  : Joe Hendrix <jhendrix@galois.com>

This module provides an interface that symbolic backends must provide
for interacting with the symbolic simulator.

Compared to the solver connections provided by What4, Crucible backends provide
a facility for managing an /assumption stack/ (see 'AS.AssumptionStack').  Note
that these backends are layered on top of the 'What4.Expr.Builder.ExprBuilder';
the solver choice is still up to the user.  The
'Lang.Crucible.Backend.Simple.SimpleBackend' is designed to be used with an
offline solver connection, while the
'Lang.Crucible.Backend.Online.OnlineBackend' is designed to be used with an
online solver.

The backend tracks the assumptions that are in scope for each assertion,
accounting for the branching and merging structure of programs. After
symbolic simulation completes, the caller should traverse the collected
'ProofObligations'  (via 'getProofObligations') to discharge the resulting proof
obligations with a solver backend. See also "Lang.Crucible.Backend.Prove".
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.Backend
  ( IsSymBackend(..)
  , IsSymInterface
  , HasSymInterface(..)
  , Assertion
  , SomeBackend(..)
  , ProofObligation
  , ProofObligations
  , AssumptionState
  , assert
  , impossibleAssumption

    -- ** Reexports
  , module Lang.Crucible.Backend.Assumptions
  , LabeledPred(..)
  , labeledPred
  , labeledPredMsg
  , AS.AssumptionStack
  , AS.FrameIdentifier
  , PG.ProofGoal(..)
  , PG.Goals(..)
  , PG.goalsToList

    -- ** Aborting execution
  , AbortExecReason(..)
  , abortExecBecause
  , ppAbortExecReason

    -- * Utilities
  , throwUnsupported

  , addAssertion
  , addDurableAssertion
  , addAssertionM
  , addFailedAssertion
  , assertIsInteger
  , readPartExpr
  , runCHC
  , proofObligationsAsImplications
  , convertProofObligationsAsImplications
  , proofObligationsUninterpConstants
  , pathConditionUninterpConstants
  , ppProofObligation
  , backendOptions
  , assertThenAssumeConfigOption
  ) where

import           Control.Exception(Exception(..), throwIO)
import           Control.Lens ((^.))
import           Control.Monad
import           Control.Monad.IO.Class
import           Data.Foldable (toList)
import           Data.Set (Set)
import qualified Prettyprinter as PP
import           GHC.Stack

import           Data.Parameterized.Map (MapF)

import           What4.Concrete
import           What4.Config
import           What4.Expr.Builder
import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.LabeledPred
import           What4.Partial
import           What4.ProgramLoc

import           What4.Solver
import qualified What4.Solver.Z3 as Z3

import           Lang.Crucible.Backend.Assumptions
import qualified Lang.Crucible.Backend.AssumptionStack as AS
import qualified Lang.Crucible.Backend.ProofGoals as PG
import           Lang.Crucible.Simulator.SimError

type Assertion sym = LabeledPred (Pred sym) SimError
type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym)
type ProofObligations sym = Maybe (AS.Goals (Assumptions sym) (Assertion sym))
type AssumptionState sym = PG.GoalCollector (Assumptions sym) (Assertion sym)

-- | This is used to signal that current execution path is infeasible.
data AbortExecReason =
    InfeasibleBranch ProgramLoc
    -- ^ We have discovered that the currently-executing
    --   branch is infeasible. The given program location
    --   describes the point at which infeasibility was discovered.

  | AssertionFailure SimError
    -- ^ An assertion concretely failed.

  | VariantOptionsExhausted ProgramLoc
    -- ^ We tried all possible cases for a variant, and now we should
    -- do something else.

  | EarlyExit ProgramLoc
    -- ^ We invoked a function which ends the current thread of execution
    --   (e.g., @abort()@ or @exit(1)@).

    deriving Int -> AbortExecReason -> ShowS
[AbortExecReason] -> ShowS
AbortExecReason -> String
(Int -> AbortExecReason -> ShowS)
-> (AbortExecReason -> String)
-> ([AbortExecReason] -> ShowS)
-> Show AbortExecReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbortExecReason -> ShowS
showsPrec :: Int -> AbortExecReason -> ShowS
$cshow :: AbortExecReason -> String
show :: AbortExecReason -> String
$cshowList :: [AbortExecReason] -> ShowS
showList :: [AbortExecReason] -> ShowS
Show

instance Exception AbortExecReason


-- | If an assumption is clearly impossible, return an abort reason
--   that can be used to unwind the execution of this branch.
impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason
impossibleAssumption :: forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Maybe AbortExecReason
impossibleAssumption (AssumingNoError SimError
err e BaseBoolType
p)
  | Just Bool
False <- e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
p = AbortExecReason -> Maybe AbortExecReason
forall a. a -> Maybe a
Just (SimError -> AbortExecReason
AssertionFailure SimError
err)
impossibleAssumption (BranchCondition ProgramLoc
loc Maybe ProgramLoc
_ e BaseBoolType
p)
  | Just Bool
False <- e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
p = AbortExecReason -> Maybe AbortExecReason
forall a. a -> Maybe a
Just (ProgramLoc -> AbortExecReason
InfeasibleBranch ProgramLoc
loc)
impossibleAssumption (GenericAssumption ProgramLoc
loc String
_ e BaseBoolType
p)
  | Just Bool
False <- e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
p = AbortExecReason -> Maybe AbortExecReason
forall a. a -> Maybe a
Just (ProgramLoc -> AbortExecReason
InfeasibleBranch ProgramLoc
loc)
impossibleAssumption CrucibleAssumption e
_ = Maybe AbortExecReason
forall a. Maybe a
Nothing

ppAbortExecReason :: AbortExecReason -> PP.Doc ann
ppAbortExecReason :: forall ann. AbortExecReason -> Doc ann
ppAbortExecReason AbortExecReason
e =
  case AbortExecReason
e of
    InfeasibleBranch ProgramLoc
l -> ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
"Executing branch was discovered to be infeasible."
    AssertionFailure SimError
err ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ Doc ann
"Abort due to assertion failure:"
      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (SimError -> Doc ann
forall ann. SimError -> Doc ann
ppSimError SimError
err)
      ]
    VariantOptionsExhausted ProgramLoc
l -> ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
"Variant options exhausted."
    EarlyExit ProgramLoc
l -> ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
"Program exited early."
  where
    ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann
    ppLocated :: forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
x = Doc ann
"in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppFn ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
x

    ppFn :: ProgramLoc -> PP.Doc ann
    ppFn :: forall ann. ProgramLoc -> Doc ann
ppFn ProgramLoc
l = FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty (ProgramLoc -> FunctionName
plFunction ProgramLoc
l)

    ppLoc :: ProgramLoc -> PP.Doc ann
    ppLoc :: forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
l = Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
l)

throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a
throwUnsupported :: forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m, HasCallStack) =>
sym -> String -> m a
throwUnsupported sym
sym String
msg = IO a -> m a
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$
  do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     SimError -> IO a
forall e a. Exception e => e -> IO a
throwIO (SimError -> IO a) -> SimError -> IO a
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc (SimErrorReason -> SimError) -> SimErrorReason -> SimError
forall a b. (a -> b) -> a -> b
$ CallStack -> String -> SimErrorReason
Unsupported CallStack
HasCallStack => CallStack
callStack String
msg

type IsSymInterface sym =
  ( IsSymExprBuilder sym
  , IsInterpretedFloatSymExprBuilder sym
  )

data SomeBackend sym =
  forall bak. IsSymBackend sym bak => SomeBackend bak


-- | Class for backend type that can retrieve sym values.
--
--   This is separate from `IsSymBackend` specifically to avoid
--   the need for additional class constraints on the `backendGetSym`
--   operation, which is occasionally useful.
class HasSymInterface sym bak | bak -> sym where
  -- | Retrive the symbolic expression builder corresponding to this
  --   simulator backend.
  backendGetSym :: bak -> sym


-- | This class provides operations that interact with the symbolic simulator.
--   It allows for logical assumptions/assertions to be added to the current
--   path condition, and allows queries to be asked about branch conditions.
--
--   The @bak@ type contains all the datastructures necessary to
--   maintain the current program path conditions, and keep track of
--   assumptions and assertions made during program execution.  The @sym@
--   type is expected to satisfy the `IsSymInterface` constraints, which
--   provide access to the What4 expression language. A @sym@ is uniquely
--   determined by a @bak@.
--
--
--   == Note [Pushes and pops]
--
--   This class provides methods for pushing ('pushAssumptionFrame')
--   and popping ('popAssumptionFrame', 'popUntilAssumptionFrame',
--   'popAssumptionFrameAndObligations') frames. Pushes and pops must be
--   well-bracketed. In particular, @popAssumptionFrame*@ are required to throw
--   an exception if the provided frame identifier does not match the top of
--   the stack.
--
--   It is relatively easy to end up with ill-bracketed pushes and pops in the
--   presence of exceptions. When diagnosing such issues, consider popping
--   frames using methods such as 'Control.Exception.try'.
class (IsSymInterface sym, HasSymInterface sym bak) => IsSymBackend sym bak | bak -> sym where

  ----------------------------------------------------------------------
  -- Branch manipulations

  -- | Push a new assumption frame onto the stack.  Assumptions and assertions
  --   made will now be associated with this frame on the stack until a new
  --   frame is pushed onto the stack, or until this one is popped.
  pushAssumptionFrame :: bak -> IO AS.FrameIdentifier

  -- | Pop an assumption frame from the stack.  The collected assumptions
  --   in this frame are returned.
  --
  --   This may throw an exception, see Note [Pushes and pops].
  popAssumptionFrame :: bak -> AS.FrameIdentifier -> IO (Assumptions sym)

  -- | Pop all assumption frames up to and including the frame with the given
  --   frame identifier.  This operation will panic if the named frame does
  --   not exist on the stack.
  popUntilAssumptionFrame :: bak -> AS.FrameIdentifier -> IO ()

  -- | Pop an assumption frame from the stack.  The collected assummptions
  --   in this frame are returned, along with any proof obligations that were
  --   incurred while the frame was active.
  --
  --   Note that the returned 'ProofObligation's only include assumptions from
  --   the popped frame, not all frames above it.
  --
  --   This may throw an exception, see Note [Pushes and pops].
  popAssumptionFrameAndObligations ::
    bak -> AS.FrameIdentifier -> IO (Assumptions sym, ProofObligations sym)

  ----------------------------------------------------------------------
  -- Assertions

  -- | Add an assumption to the current state.
  addAssumption :: bak -> Assumption sym -> IO ()

  -- | Add a collection of assumptions to the current state.
  addAssumptions :: bak -> Assumptions sym -> IO ()

  -- | Get the current path condition as a predicate.  This consists of the conjunction
  --   of all the assumptions currently in scope.
  getPathCondition :: bak -> IO (Pred sym)
  getPathCondition bak
bak = do
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
    CrucibleAssumptions (SymExpr sym)
ps <- bak -> IO (CrucibleAssumptions (SymExpr sym))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (CrucibleAssumptions (SymExpr sym))
collectAssumptions bak
bak
    sym -> CrucibleAssumptions (SymExpr sym) -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym CrucibleAssumptions (SymExpr sym)
ps

  -- | Collect all the assumptions currently in scope
  collectAssumptions :: bak -> IO (Assumptions sym)

  -- | Add a new proof obligation to the system.
  -- The proof may use the current path condition and assumptions. Note
  -- that this *DOES NOT* add the goal as an assumption. See also
  -- 'addAssertion'. Also note that predicates that concretely evaluate
  -- to True will be silently discarded. See 'addDurableProofObligation'
  -- to avoid discarding goals.
  addProofObligation :: bak -> Assertion sym -> IO ()
  addProofObligation bak
bak Assertion sym
a =
    case Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred (Assertion sym
a Assertion sym
-> Getting (Pred sym) (Assertion sym) (Pred sym) -> Pred sym
forall s a. s -> Getting a s a -> a
^. Getting (Pred sym) (Assertion sym) (Pred sym)
forall pred msg pred' (f :: Type -> Type).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred) of
      Just Bool
True -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
      Maybe Bool
_ -> bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak Assertion sym
a

  -- | Add a new proof obligation to the system which will persist
  -- throughout symbolic execution even if it is concretely valid.
  -- The proof may use the current path condition and assumptions. Note
  -- that this *DOES NOT* add the goal as an assumption. See also
  -- 'addDurableAssertion'.
  addDurableProofObligation :: bak -> Assertion sym -> IO ()

  -- | Get the collection of proof obligations.
  getProofObligations :: bak -> IO (ProofObligations sym)

  -- | Forget the current collection of proof obligations.
  -- Presumably, we've already used 'getProofObligations' to save them
  -- somewhere else.
  clearProofObligations :: bak -> IO ()

  -- | Create a snapshot of the current assumption state, that may later be restored.
  --   This is useful for supporting control-flow patterns that don't neatly fit into
  --   the stack push/pop model.
  saveAssumptionState :: bak -> IO (AssumptionState sym)

  -- | Restore the assumption state to a previous snapshot.
  restoreAssumptionState :: bak -> AssumptionState sym -> IO ()

  -- | Reset the assumption state to a fresh, blank state
  resetAssumptionState :: bak -> IO ()
  resetAssumptionState bak
bak = bak -> AssumptionState sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> AssumptionState sym -> IO ()
restoreAssumptionState bak
bak AssumptionState sym
forall asmp goal. GoalCollector asmp goal
PG.emptyGoalCollector

assertThenAssumeConfigOption :: ConfigOption BaseBoolType
assertThenAssumeConfigOption :: ConfigOption BaseBoolType
assertThenAssumeConfigOption = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"assertThenAssume"

assertThenAssumeOption :: ConfigDesc
assertThenAssumeOption :: ConfigDesc
assertThenAssumeOption = ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
  ConfigOption BaseBoolType
assertThenAssumeConfigOption
  OptionStyle BaseBoolType
boolOptSty
  (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Assume a predicate after asserting it.")
  (ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))

backendOptions :: [ConfigDesc]
backendOptions :: [ConfigDesc]
backendOptions = [ConfigDesc
assertThenAssumeOption]

-- | Add a proof obligation for the given predicate, and then assume it
-- (when the assertThenAssume option is true).
-- Note that assuming the prediate might cause the current execution
-- path to abort, if we happened to assume something that is obviously false.
addAssertion ::
  IsSymBackend sym bak =>
  bak -> Assertion sym -> IO ()
addAssertion :: forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion bak
bak Assertion sym
a =
  do bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addProofObligation bak
bak Assertion sym
a
     bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
assumeAssertion bak
bak Assertion sym
a

-- | Add a durable proof obligation for the given predicate, and then
-- assume it (when the assertThenAssume option is true).
-- Note that assuming the prediate might cause the current execution
-- path to abort, if we happened to assume something that is obviously false.
addDurableAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO ()
addDurableAssertion :: forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableAssertion bak
bak Assertion sym
a =
  do bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak Assertion sym
a
     bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
assumeAssertion bak
bak Assertion sym
a

-- | Assume assertion when the assertThenAssume option is true.
assumeAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO ()
assumeAssertion :: forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
assumeAssertion bak
bak (LabeledPred Pred sym
p SimError
msg) =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     Bool
assert_then_assume_opt <- OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt
       (OptionSetting BaseBoolType -> IO Bool)
-> IO (OptionSetting BaseBoolType) -> IO Bool
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
assertThenAssumeConfigOption (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration sym
sym)
     Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
assert_then_assume_opt (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
       bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (SimError -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
SimError -> e BaseBoolType -> CrucibleAssumption e
AssumingNoError SimError
msg Pred sym
p)

-- | Throw an exception, thus aborting the current execution path.
abortExecBecause :: AbortExecReason -> IO a
abortExecBecause :: forall a. AbortExecReason -> IO a
abortExecBecause AbortExecReason
err = AbortExecReason -> IO a
forall e a. Exception e => e -> IO a
throwIO AbortExecReason
err

-- | Add a proof obligation using the current program location.
--   Afterwards, assume the given fact.
assert ::
  IsSymBackend sym bak =>
  bak ->
  Pred sym ->
  SimErrorReason ->
  IO ()
assert :: forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak Pred sym
p SimErrorReason
msg =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
p (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
msg))

-- | Add a proof obligation for False. This always aborts execution
-- of the current path, because after asserting false, we get to assume it,
-- and so there is no need to check anything after.  This is why the resulting
-- IO computation can have the fully polymorphic type.
addFailedAssertion :: IsSymBackend sym bak => bak -> SimErrorReason -> IO a
addFailedAssertion :: forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
msg =
  do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     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
msg
     bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addProofObligation bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) SimError
err)
     AbortExecReason -> IO a
forall a. AbortExecReason -> IO a
abortExecBecause (SimError -> AbortExecReason
AssertionFailure SimError
err)

-- | Run the given action to compute a predicate, and assert it.
addAssertionM ::
  IsSymBackend sym bak =>
  bak ->
  IO (Pred sym) ->
  SimErrorReason ->
  IO ()
addAssertionM :: forall sym bak.
IsSymBackend sym bak =>
bak -> IO (Pred sym) -> SimErrorReason -> IO ()
addAssertionM bak
bak IO (Pred sym)
pf SimErrorReason
msg = do
  Pred sym
p <- IO (Pred sym)
pf
  bak -> Pred sym -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak Pred sym
p SimErrorReason
msg

-- | Assert that the given real-valued expression is an integer.
assertIsInteger ::
  IsSymBackend sym bak =>
  bak ->
  SymReal sym ->
  SimErrorReason ->
  IO ()
assertIsInteger :: forall sym bak.
IsSymBackend sym bak =>
bak -> SymReal sym -> SimErrorReason -> IO ()
assertIsInteger bak
bak SymReal sym
v SimErrorReason
msg = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  bak -> IO (Pred sym) -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (Pred sym) -> SimErrorReason -> IO ()
addAssertionM bak
bak (sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
isInteger sym
sym SymReal sym
v) SimErrorReason
msg

-- | Given a partial expression, assert that it is defined
--   and return the underlying value.
readPartExpr ::
  IsSymBackend sym bak =>
  bak ->
  PartExpr (Pred sym) v ->
  SimErrorReason ->
  IO v
readPartExpr :: forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak PartExpr (SymExpr sym BaseBoolType) v
Unassigned SimErrorReason
msg = do
  bak -> SimErrorReason -> IO v
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
msg
readPartExpr bak
bak (PE SymExpr sym BaseBoolType
p v
v) SimErrorReason
msg = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
  bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred SymExpr sym BaseBoolType
p (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
msg))
  v -> IO v
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return v
v


-- | Run the CHC solver on the current proof obligations, and return the
-- solution as a substitution from the uninterpreted functions to their
-- definitions.
runCHC ::
  (IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) =>
  bak ->
  [SomeSymFn sym] ->
  m (MapF (SymFnWrapper sym) (SymFnWrapper sym))
runCHC :: forall sym bak t (st :: Type -> Type) fs (m :: Type -> Type).
(IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) =>
bak
-> [SomeSymFn sym]
-> m (MapF (SymFnWrapper sym) (SymFnWrapper sym))
runCHC bak
bak [SomeSymFn sym]
uninterp_inv_fns  = IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
-> m (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
 -> m (MapF (SymFnWrapper sym) (SymFnWrapper sym)))
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
-> m (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall a b. (a -> b) -> a -> b
$ do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak

  [BoolExpr t]
implications <- bak -> IO [Pred (ExprBuilder t st fs)]
forall sym bak. IsSymBackend sym bak => bak -> IO [Pred sym]
proofObligationsAsImplications bak
bak
  bak -> IO ()
forall sym bak. IsSymBackend sym bak => bak -> IO ()
clearProofObligations bak
bak

  -- log to stdout
  let logData :: LogData
logData = LogData
defaultLogData
        { logCallbackVerbose = \Int
_ -> String -> IO ()
putStrLn
        , logReason = "Crucible inv"
        }
  sym
-> Bool
-> LogData
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
forall sym t (st :: Type -> Type) fs.
(sym ~ ExprBuilder t st fs) =>
sym
-> Bool
-> LogData
-> [SomeSymFn sym]
-> [BoolExpr t]
-> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
Z3.runZ3Horn sym
sym Bool
True LogData
logData [SomeSymFn sym]
uninterp_inv_fns [BoolExpr t]
implications IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
-> (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
    -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)))
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Sat MapF (SymFnWrapper sym) (SymFnWrapper sym)
sub -> MapF (SymFnWrapper sym) (SymFnWrapper sym)
-> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MapF (SymFnWrapper sym) (SymFnWrapper sym)
sub
    Unsat{} -> String -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Prover returned Unsat"
    SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()
Unknown -> String -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Prover returned Unknown"


-- | Get proof obligations as What4 implications.
proofObligationsAsImplications :: IsSymBackend sym bak => bak -> IO [Pred sym]
proofObligationsAsImplications :: forall sym bak. IsSymBackend sym bak => bak -> IO [Pred sym]
proofObligationsAsImplications bak
bak = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  sym
-> Maybe
     (Goals
        (CrucibleAssumptions (SymExpr sym))
        (LabeledPred (Pred sym) SimError))
-> IO [Pred sym]
forall sym.
IsSymInterface sym =>
sym -> ProofObligations sym -> IO [Pred sym]
convertProofObligationsAsImplications sym
sym (Maybe
   (Goals
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError))
 -> IO [Pred sym])
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr sym))
           (LabeledPred (Pred sym) SimError)))
-> IO [Pred sym]
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< bak
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr sym))
           (LabeledPred (Pred sym) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
getProofObligations bak
bak

-- | Convert proof obligations to What4 implications.
convertProofObligationsAsImplications :: IsSymInterface sym => sym -> ProofObligations sym -> IO [Pred sym]
convertProofObligationsAsImplications :: forall sym.
IsSymInterface sym =>
sym -> ProofObligations sym -> IO [Pred sym]
convertProofObligationsAsImplications sym
sym ProofObligations sym
goals = do
  let obligations :: [ProofGoal
   (CrucibleAssumptions (SymExpr sym))
   (LabeledPred (Pred sym) SimError)]
obligations = [ProofGoal
   (CrucibleAssumptions (SymExpr sym))
   (LabeledPred (Pred sym) SimError)]
-> (Goals
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError)
    -> [ProofGoal
          (CrucibleAssumptions (SymExpr sym))
          (LabeledPred (Pred sym) SimError)])
-> ProofObligations sym
-> [ProofGoal
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Goals
  (CrucibleAssumptions (SymExpr sym))
  (LabeledPred (Pred sym) SimError)
-> [ProofGoal
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError)]
forall asmp goal.
Monoid asmp =>
Goals asmp goal -> [ProofGoal asmp goal]
PG.goalsToList ProofObligations sym
goals
  [ProofGoal
   (CrucibleAssumptions (SymExpr sym))
   (LabeledPred (Pred sym) SimError)]
-> (ProofGoal
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError)
    -> IO (Pred sym))
-> IO [Pred sym]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ProofGoal
   (CrucibleAssumptions (SymExpr sym))
   (LabeledPred (Pred sym) SimError)]
obligations ((ProofGoal
    (CrucibleAssumptions (SymExpr sym))
    (LabeledPred (Pred sym) SimError)
  -> IO (Pred sym))
 -> IO [Pred sym])
-> (ProofGoal
      (CrucibleAssumptions (SymExpr sym))
      (LabeledPred (Pred sym) SimError)
    -> IO (Pred sym))
-> IO [Pred sym]
forall a b. (a -> b) -> a -> b
$ \(AS.ProofGoal CrucibleAssumptions (SymExpr sym)
hyps (LabeledPred Pred sym
concl SimError
_err)) -> do
    Pred sym
hyp <- sym -> CrucibleAssumptions (SymExpr sym) -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym CrucibleAssumptions (SymExpr sym)
hyps
    sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
impliesPred sym
sym Pred sym
hyp Pred sym
concl

-- | Get the set of uninterpreted constants that appear in the path condition.
pathConditionUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))
pathConditionUninterpConstants :: forall sym bak.
IsSymBackend sym bak =>
bak -> IO (Set (Some (BoundVar sym)))
pathConditionUninterpConstants bak
bak = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  sym -> SymExpr sym BaseBoolType -> Set (Some (BoundVar sym))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
exprUninterpConstants sym
sym (SymExpr sym BaseBoolType -> Set (Some (BoundVar sym)))
-> IO (SymExpr sym BaseBoolType) -> IO (Set (Some (BoundVar sym)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> bak -> IO (SymExpr sym BaseBoolType)
forall sym bak. IsSymBackend sym bak => bak -> IO (Pred sym)
getPathCondition bak
bak

-- | Get the set of uninterpreted constants that appear in the proof obligations.
proofObligationsUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))
proofObligationsUninterpConstants :: forall sym bak.
IsSymBackend sym bak =>
bak -> IO (Set (Some (BoundVar sym)))
proofObligationsUninterpConstants bak
bak = do
  let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
  (SymExpr sym BaseBoolType -> Set (Some (BoundVar sym)))
-> [SymExpr sym BaseBoolType] -> Set (Some (BoundVar sym))
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (sym -> SymExpr sym BaseBoolType -> Set (Some (BoundVar sym))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
forall (tp :: BaseType).
sym -> SymExpr sym tp -> Set (Some (BoundVar sym))
exprUninterpConstants sym
sym) ([SymExpr sym BaseBoolType] -> Set (Some (BoundVar sym)))
-> IO [SymExpr sym BaseBoolType] -> IO (Set (Some (BoundVar sym)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> bak -> IO [SymExpr sym BaseBoolType]
forall sym bak. IsSymBackend sym bak => bak -> IO [Pred sym]
proofObligationsAsImplications bak
bak


ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann)
ppProofObligation :: forall sym ann.
IsExprBuilder sym =>
sym -> ProofObligation sym -> IO (Doc ann)
ppProofObligation sym
sym (AS.ProofGoal Assumptions sym
asmps Assertion sym
gl) =
  do [CrucibleAssumption (SymExpr sym)]
as <- sym -> Assumptions sym -> IO [CrucibleAssumption (SymExpr sym)]
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions sym
sym Assumptions sym
asmps
     Doc ann -> IO (Doc ann)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Doc ann -> IO (Doc ann)) -> Doc ann -> IO (Doc ann)
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep
       [ if [CrucibleAssumption (SymExpr sym)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [CrucibleAssumption (SymExpr sym)]
as then Doc ann
forall a. Monoid a => a
mempty else
           [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat (Doc ann
"Assuming:" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (CrucibleAssumption (SymExpr sym) -> [Doc ann])
-> [CrucibleAssumption (SymExpr sym)] -> [Doc ann]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap CrucibleAssumption (SymExpr sym) -> [Doc ann]
forall {e :: BaseType -> Type} {ann}.
IsExpr e =>
CrucibleAssumption e -> [Doc ann]
ppAsm ([CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (SymExpr sym)]
forall a. [a] -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList [CrucibleAssumption (SymExpr sym)]
as))
       , Doc ann
"Prove:"
       , Doc ann
ppGl
       ]
 where
 ppAsm :: CrucibleAssumption e -> [Doc ann]
ppAsm CrucibleAssumption e
asm
   | Bool -> Bool
not (CrucibleAssumption e -> Bool
forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Bool
trivialAssumption CrucibleAssumption e
asm) = [Doc ann
"* " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.hang Int
2 ((forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
forall (e :: BaseType -> Type) ann.
(forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
ppAssumption e tp -> Doc ann
forall (tp :: BaseType). e tp -> Doc ann
forall (tp :: BaseType) ann. e tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr CrucibleAssumption e
asm)]
   | Bool
otherwise = []

 ppGl :: Doc ann
ppGl =
   Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
   [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep [SimError -> Doc ann
forall ann. SimError -> Doc ann
ppSimError (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 :: Type -> Type).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg), SymExpr sym BaseBoolType -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr (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 :: Type -> Type).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred)]