{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Syntax.Overrides
  ( setupOverrides
  ) where

import Control.Lens hiding ((:>), Empty)
import Control.Monad.Except (runExceptT)
import Control.Monad.IO.Class
import System.IO

import Data.Parameterized.Context hiding (view)

import What4.Expr.Builder
import What4.ProgramLoc
import What4.Solver (LogData(..), defaultLogData)
import What4.Solver.Z3 (z3Adapter)

import Lang.Crucible.Backend
import qualified Lang.Crucible.Backend.Prove as CB
import Lang.Crucible.Types
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Simulator
import qualified Lang.Crucible.Utils.Seconds as Sec
import qualified Lang.Crucible.Utils.Timeout as CTO


setupOverrides ::
  (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
  sym -> HandleAllocator -> IO [(FnBinding p sym ext, Position)]
setupOverrides :: forall sym t (st :: * -> *) fs p ext.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
sym -> HandleAllocator -> IO [(FnBinding p sym ext, Position)]
setupOverrides sym
_ HandleAllocator
ha =
  do FnBinding p sym ext
f1 <- FnHandle EmptyCtx UnitType
-> FnState p sym ext EmptyCtx UnitType -> FnBinding p sym ext
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext.
FnHandle args ret
-> FnState p sym ext args ret -> FnBinding p sym ext
FnBinding (FnHandle EmptyCtx UnitType
 -> FnState p sym ext EmptyCtx UnitType -> FnBinding p sym ext)
-> IO (FnHandle EmptyCtx UnitType)
-> IO (FnState p sym ext EmptyCtx UnitType -> FnBinding p sym ext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HandleAllocator -> FunctionName -> IO (FnHandle EmptyCtx UnitType)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
(KnownCtx TypeRepr args, KnownRepr TypeRepr ret) =>
HandleAllocator -> FunctionName -> IO (FnHandle args ret)
mkHandle HandleAllocator
ha FunctionName
"proveObligations"
                     IO (FnState p sym ext EmptyCtx UnitType -> FnBinding p sym ext)
-> IO (FnState p sym ext EmptyCtx UnitType)
-> IO (FnBinding p sym ext)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FnState p sym ext EmptyCtx UnitType
-> IO (FnState p sym ext EmptyCtx UnitType)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Override p sym ext EmptyCtx UnitType
-> FnState p sym ext EmptyCtx UnitType
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FnState p sym ext args ret
UseOverride (FunctionName
-> (forall r.
    OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType))
-> Override p sym ext EmptyCtx UnitType
forall (ret :: CrucibleType) p sym ext (args :: Ctx CrucibleType).
KnownRepr TypeRepr ret =>
FunctionName
-> (forall r. OverrideSim p sym ext r args ret (RegValue sym ret))
-> Override p sym ext args ret
mkOverride FunctionName
"proveObligations" OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
forall r.
OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
forall sym t (st :: * -> *) fs p ext r.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
proveObligations))

     [(FnBinding p sym ext, Position)]
-> IO [(FnBinding p sym ext, Position)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(FnBinding p sym ext
f1, Position
InternalPos)]


proveObligations :: (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
  OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
proveObligations :: forall sym t (st :: * -> *) fs p ext r.
(IsSymInterface sym, sym ~ ExprBuilder t st fs) =>
OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
proveObligations =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r EmptyCtx UnitType (RegValue sym UnitType))
-> OverrideSim
     p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r EmptyCtx UnitType (RegValue sym UnitType))
 -> OverrideSim
      p sym ext r EmptyCtx UnitType (RegValue sym UnitType))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r EmptyCtx UnitType (RegValue sym UnitType))
-> OverrideSim
     p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
  do let sym :: ExprBuilder t st fs
sym = bak -> ExprBuilder t st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
     Handle
h <- SimContext p sym ext -> Handle
forall personality sym ext.
SimContext personality sym ext -> Handle
printHandle (SimContext p sym ext -> Handle)
-> OverrideSim p sym ext r EmptyCtx UnitType (SimContext p sym ext)
-> OverrideSim p sym ext r EmptyCtx UnitType Handle
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideSim p sym ext r EmptyCtx UnitType (SimContext p sym ext)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret (SimContext p sym ext)
getContext
     IO () -> OverrideSim p sym ext r EmptyCtx UnitType ()
forall a. IO a -> OverrideSim p sym ext r EmptyCtx UnitType a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext r EmptyCtx UnitType ())
-> IO () -> OverrideSim p sym ext r EmptyCtx UnitType ()
forall a b. (a -> b) -> a -> b
$ do
       Handle -> String -> IO ()
hPutStrLn Handle
h String
"Attempting to prove all outstanding obligations!\n"

       let logData :: LogData
logData = LogData
defaultLogData { logCallbackVerbose = \Int
_ -> Handle -> String -> IO ()
hPutStrLn Handle
h
                                    , logReason = "assertion proof" }
       let timeout :: Timeout
timeout = Seconds -> Timeout
CTO.Timeout (Int -> Seconds
Sec.secondsFromInt Int
5)
       let prover :: Prover (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
prover = Timeout
-> IsSymExprBuilder (ExprBuilder t st fs) =>
   ExprBuilder t st fs
   -> LogData
   -> SolverAdapter st
   -> Prover (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
forall (m :: * -> *) sym t (st :: * -> *) fs r.
(MonadError TimedOut m, MonadIO m, sym ~ ExprBuilder t st fs) =>
Timeout
-> IsSymExprBuilder sym =>
   sym -> LogData -> SolverAdapter st -> Prover sym m t r
CB.offlineProver Timeout
timeout ExprBuilder t st fs
sym LogData
logData SolverAdapter st
forall (st :: * -> *). SolverAdapter st
z3Adapter
       let strat :: ProofStrategy (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
strat = Prover (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
-> Combiner (ExceptT TimedOut IO) ()
-> ProofStrategy (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
forall sym (m :: * -> *) t r.
Prover sym m t r -> Combiner m r -> ProofStrategy sym m t r
CB.ProofStrategy Prover (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
prover Combiner (ExceptT TimedOut IO) ()
forall (m :: * -> *) r. (Monad m, Semigroup r) => Combiner m r
CB.keepGoing
       let ppResult :: ProofGoal asmp (LabeledPred pred SimError)
-> ProofResult sym t -> String
ppResult ProofGoal asmp (LabeledPred pred SimError)
o =
             \case
               CB.Proved {}  -> [String] -> String
unlines [String
"Proof Succeeded!", Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SimError -> Doc Any
forall ann. SimError -> Doc ann
ppSimError (SimError -> Doc Any) -> SimError -> Doc Any
forall a b. (a -> b) -> a -> b
$ (ProofGoal asmp (LabeledPred pred SimError)
-> LabeledPred pred SimError
forall asmp goal. ProofGoal asmp goal -> goal
proofGoal ProofGoal asmp (LabeledPred pred SimError)
o)LabeledPred pred SimError
-> Getting SimError (LabeledPred pred SimError) SimError
-> SimError
forall s a. s -> Getting a s a -> a
^.Getting SimError (LabeledPred pred SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg]
               CB.Disproved {} -> [String] -> String
unlines [String
"Proof failed!", Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SimError -> Doc Any
forall ann. SimError -> Doc ann
ppSimError (SimError -> Doc Any) -> SimError -> Doc Any
forall a b. (a -> b) -> a -> b
$ (ProofGoal asmp (LabeledPred pred SimError)
-> LabeledPred pred SimError
forall asmp goal. ProofGoal asmp goal -> goal
proofGoal ProofGoal asmp (LabeledPred pred SimError)
o)LabeledPred pred SimError
-> Getting SimError (LabeledPred pred SimError) SimError
-> SimError
forall s a. s -> Getting a s a -> a
^.Getting SimError (LabeledPred pred SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg]
               CB.Unknown {} -> [String] -> String
unlines [String
"Proof inconclusive!", Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SimError -> Doc Any
forall ann. SimError -> Doc ann
ppSimError (SimError -> Doc Any) -> SimError -> Doc Any
forall a b. (a -> b) -> a -> b
$ (ProofGoal asmp (LabeledPred pred SimError)
-> LabeledPred pred SimError
forall asmp goal. ProofGoal asmp goal -> goal
proofGoal ProofGoal asmp (LabeledPred pred SimError)
o)LabeledPred pred SimError
-> Getting SimError (LabeledPred pred SimError) SimError
-> SimError
forall s a. s -> Getting a s a -> a
^.Getting SimError (LabeledPred pred SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg]
       let printer :: ProofConsumer (ExprBuilder t st fs) t ()
printer = (ProofObligation (ExprBuilder t st fs)
 -> ProofResult (ExprBuilder t st fs) t -> IO ())
-> ProofConsumer (ExprBuilder t st fs) t ()
forall sym t r.
(ProofObligation sym -> ProofResult sym t -> IO r)
-> ProofConsumer sym t r
CB.ProofConsumer ((ProofObligation (ExprBuilder t st fs)
  -> ProofResult (ExprBuilder t st fs) t -> IO ())
 -> ProofConsumer (ExprBuilder t st fs) t ())
-> (ProofObligation (ExprBuilder t st fs)
    -> ProofResult (ExprBuilder t st fs) t -> IO ())
-> ProofConsumer (ExprBuilder t st fs) t ()
forall a b. (a -> b) -> a -> b
$ \ProofObligation (ExprBuilder t st fs)
o ProofResult (ExprBuilder t st fs) t
r -> Handle -> String -> IO ()
hPutStrLn Handle
h (ProofGoal
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError)
-> ProofResult (ExprBuilder t st fs) t -> String
forall {asmp} {pred} {sym} {t}.
ProofGoal asmp (LabeledPred pred SimError)
-> ProofResult sym t -> String
ppResult ProofGoal
  (CrucibleAssumptions (Expr t))
  (LabeledPred (Expr t BaseBoolType) SimError)
ProofObligation (ExprBuilder t st fs)
o ProofResult (ExprBuilder t st fs) t
r)
       ExceptT TimedOut IO () -> IO (Either TimedOut ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (bak
-> ProofStrategy (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
-> ProofConsumer (ExprBuilder t st fs) t ()
-> ExceptT TimedOut IO ()
forall (m :: * -> *) r sym t (st :: * -> *) fs bak.
(MonadIO m, Monoid r, sym ~ ExprBuilder t st fs,
 IsSymBackend sym bak) =>
bak -> ProofStrategy sym m t r -> ProofConsumer sym t r -> m r
CB.proveCurrentObligations bak
bak ProofStrategy (ExprBuilder t st fs) (ExceptT TimedOut IO) t ()
strat ProofConsumer (ExprBuilder t st fs) t ()
printer) IO (Either TimedOut ()) -> (Either TimedOut () -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
         \case
           Left TimedOut
CTO.TimedOut -> Handle -> String -> IO ()
hPutStrLn Handle
h String
"Proof timed out!"
           Right () -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

       bak -> IO ()
forall sym bak. IsSymBackend sym bak => bak -> IO ()
clearProofObligations bak
bak