------------------------------------------------------------------------
-- |
-- Module      : Lang.Crucible.Backend.Simple
-- Description : The "simple" solver backend
-- Copyright   : (c) Galois, Inc 2015-2016
-- License     : BSD3
-- Maintainer  : Rob Dockins <rdockins@galois.com>
-- Stability   : provisional
--
-- An "offline" backend for communicating with solvers.  This backend
-- does not maintain a persistent connection to a solver, and does
-- not perform satisfiability checks at symbolic branch points.
------------------------------------------------------------------------

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Lang.Crucible.Backend.Simple
  ( -- * SimpleBackend
    SimpleBackend
  , newSimpleBackend
    -- * Re-exports
  , B.FloatMode
  , B.FloatModeRepr(..)
  , B.FloatIEEE
  , B.FloatUninterpreted
  , B.FloatReal
  , B.Flags
  ) where

import           Control.Lens ( (^.) )
import           Control.Monad (void)

import           What4.Config
import           What4.Interface
import qualified What4.Expr.Builder as B

import qualified Lang.Crucible.Backend.AssumptionStack as AS
import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator.SimError

------------------------------------------------------------------------
-- SimpleBackendState

-- | This represents the state of the backend along a given execution.
-- It contains the current assertion stack.

type AS t =
     AssumptionStack (CrucibleAssumptions (B.Expr t))
                     (LabeledPred (B.BoolExpr t) SimError)

data SimpleBackend t st fs =
  SimpleBackend
  { forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack :: AS t
  , forall t (st :: Type -> Type) fs.
SimpleBackend t st fs -> ExprBuilder t st fs
sbExprBuilder :: B.ExprBuilder t st fs
  }

newSimpleBackend ::
  B.ExprBuilder t st fs ->
  IO (SimpleBackend t st fs)
newSimpleBackend :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SimpleBackend t st fs)
newSimpleBackend ExprBuilder t st fs
sym =
  do AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
as <- NonceGenerator IO t
-> IO
     (AssumptionStack
        (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError))
forall t asmp ast.
NonceGenerator IO t -> IO (AssumptionStack asmp ast)
AS.initAssumptionStack (ExprBuilder t st fs
sym ExprBuilder t st fs
-> Getting
     (NonceGenerator IO t) (ExprBuilder t st fs) (NonceGenerator IO t)
-> NonceGenerator IO t
forall s a. s -> Getting a s a -> a
^. Getting
  (NonceGenerator IO t) (ExprBuilder t st fs) (NonceGenerator IO t)
forall t (st :: Type -> Type) fs (f :: Type -> Type).
(Contravariant f, Functor f) =>
(NonceGenerator IO t -> f (NonceGenerator IO t))
-> ExprBuilder t st fs -> f (ExprBuilder t st fs)
B.exprCounter)
     [ConfigDesc] -> Config -> IO ()
tryExtendConfig [ConfigDesc]
backendOptions (ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym)
     SimpleBackend t st fs -> IO (SimpleBackend t st fs)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SimpleBackend
            { sbAssumptionStack :: AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
sbAssumptionStack = AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
as
            , sbExprBuilder :: ExprBuilder t st fs
sbExprBuilder = ExprBuilder t st fs
sym
            }

instance HasSymInterface (B.ExprBuilder t st fs) (SimpleBackend t st fs) where
  backendGetSym :: SimpleBackend t st fs -> ExprBuilder t st fs
backendGetSym = SimpleBackend t st fs -> ExprBuilder t st fs
forall t (st :: Type -> Type) fs.
SimpleBackend t st fs -> ExprBuilder t st fs
sbExprBuilder  

instance IsSymInterface (B.ExprBuilder t st fs) =>
  IsSymBackend (B.ExprBuilder t st fs) (SimpleBackend t st fs) where

  addDurableProofObligation :: SimpleBackend t st fs -> Assertion (ExprBuilder t st fs) -> IO ()
addDurableProofObligation SimpleBackend t st fs
bak Assertion (ExprBuilder t st fs)
a =
     LabeledPred (BoolExpr t) SimError
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO ()
forall ast asmp. ast -> AssumptionStack asmp ast -> IO ()
AS.addProofObligation Assertion (ExprBuilder t st fs)
LabeledPred (BoolExpr t) SimError
a (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  addAssumption :: SimpleBackend t st fs -> Assumption (ExprBuilder t st fs) -> IO ()
addAssumption SimpleBackend t st fs
bak Assumption (ExprBuilder t st fs)
a =
    case CrucibleAssumption (Expr t) -> Maybe AbortExecReason
forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Maybe AbortExecReason
impossibleAssumption Assumption (ExprBuilder t st fs)
CrucibleAssumption (Expr t)
a of
      Just AbortExecReason
rsn -> AbortExecReason -> IO ()
forall a. AbortExecReason -> IO a
abortExecBecause AbortExecReason
rsn
      Maybe AbortExecReason
Nothing  -> CrucibleAssumptions (Expr t)
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO ()
forall asmp ast.
Monoid asmp =>
asmp -> AssumptionStack asmp ast -> IO ()
AS.appendAssumptions (CrucibleAssumption (Expr t) -> CrucibleAssumptions (Expr t)
forall (e :: BaseType -> Type).
CrucibleAssumption e -> CrucibleAssumptions e
singleAssumption Assumption (ExprBuilder t st fs)
CrucibleAssumption (Expr t)
a) (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  addAssumptions :: SimpleBackend t st fs -> Assumptions (ExprBuilder t st fs) -> IO ()
addAssumptions SimpleBackend t st fs
bak Assumptions (ExprBuilder t st fs)
ps = do
    CrucibleAssumptions (Expr t)
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO ()
forall asmp ast.
Monoid asmp =>
asmp -> AssumptionStack asmp ast -> IO ()
AS.appendAssumptions Assumptions (ExprBuilder t st fs)
CrucibleAssumptions (Expr t)
ps (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  collectAssumptions :: SimpleBackend t st fs -> IO (Assumptions (ExprBuilder t st fs))
collectAssumptions SimpleBackend t st fs
bak =
    AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO (CrucibleAssumptions (Expr t))
forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO asmp
AS.collectAssumptions (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  getProofObligations :: SimpleBackend t st fs
-> IO (ProofObligations (ExprBuilder t st fs))
getProofObligations SimpleBackend t st fs
bak = do
    AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (Expr t))
           (LabeledPred (BoolExpr t) SimError)))
forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (Maybe (Goals asmp ast))
AS.getProofObligations (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  clearProofObligations :: SimpleBackend t st fs -> IO ()
clearProofObligations SimpleBackend t st fs
bak = do
    AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO ()
forall asmp ast. Monoid asmp => AssumptionStack asmp ast -> IO ()
AS.clearProofObligations (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  pushAssumptionFrame :: SimpleBackend t st fs -> IO FrameIdentifier
pushAssumptionFrame SimpleBackend t st fs
bak = do
    AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO FrameIdentifier
forall asmp ast. AssumptionStack asmp ast -> IO FrameIdentifier
AS.pushFrame (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  popAssumptionFrame :: SimpleBackend t st fs
-> FrameIdentifier -> IO (Assumptions (ExprBuilder t st fs))
popAssumptionFrame SimpleBackend t st fs
bak FrameIdentifier
ident = do
    FrameIdentifier
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO (CrucibleAssumptions (Expr t))
forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
AS.popFrame FrameIdentifier
ident (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  popAssumptionFrameAndObligations :: SimpleBackend t st fs
-> FrameIdentifier
-> IO
     (Assumptions (ExprBuilder t st fs),
      ProofObligations (ExprBuilder t st fs))
popAssumptionFrameAndObligations SimpleBackend t st fs
bak FrameIdentifier
ident = do
    FrameIdentifier
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO
     (CrucibleAssumptions (Expr t),
      Maybe
        (Goals
           (CrucibleAssumptions (Expr t))
           (LabeledPred (BoolExpr t) SimError)))
forall asmp ast.
Monoid asmp =>
FrameIdentifier
-> AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast))
AS.popFrameAndGoals FrameIdentifier
ident (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  popUntilAssumptionFrame :: SimpleBackend t st fs -> FrameIdentifier -> IO ()
popUntilAssumptionFrame SimpleBackend t st fs
bak FrameIdentifier
ident = do
    IO Int -> IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (IO Int -> IO ()) -> IO Int -> IO ()
forall a b. (a -> b) -> a -> b
$ FrameIdentifier
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO Int
forall asmp ast.
Monoid asmp =>
FrameIdentifier -> AssumptionStack asmp ast -> IO Int
AS.popFramesUntil FrameIdentifier
ident (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  saveAssumptionState :: SimpleBackend t st fs -> IO (AssumptionState (ExprBuilder t st fs))
saveAssumptionState SimpleBackend t st fs
bak = do
    AssumptionStack
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO
     (GoalCollector
        (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError))
forall asmp ast.
Monoid asmp =>
AssumptionStack asmp ast -> IO (GoalCollector asmp ast)
AS.saveAssumptionStack (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)

  restoreAssumptionState :: SimpleBackend t st fs
-> AssumptionState (ExprBuilder t st fs) -> IO ()
restoreAssumptionState SimpleBackend t st fs
bak AssumptionState (ExprBuilder t st fs)
newstk = do
    GoalCollector
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
-> IO ()
forall asmp ast.
Monoid asmp =>
GoalCollector asmp ast -> AssumptionStack asmp ast -> IO ()
AS.restoreAssumptionStack AssumptionState (ExprBuilder t st fs)
GoalCollector
  (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
newstk (SimpleBackend t st fs
-> AssumptionStack
     (CrucibleAssumptions (Expr t)) (LabeledPred (BoolExpr t) SimError)
forall t (st :: Type -> Type) fs. SimpleBackend t st fs -> AS t
sbAssumptionStack SimpleBackend t st fs
bak)