Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace many calls to fail with other exceptions #685

Merged
merged 9 commits into from
Apr 27, 2020
17 changes: 14 additions & 3 deletions src/SAWScript/Crucible/Common/Override.hs
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ module SAWScript.Crucible.Common.Override
, ppOverrideFailure
--
, OverrideMatcher(..)
, throwOverrideMatcher
, runOverrideMatcher
, RO
, RW
Expand All @@ -54,7 +55,8 @@ import Control.Lens
import Control.Monad.Trans.State hiding (get, put)
import Control.Monad.State.Class (MonadState(..))
import Control.Monad.Error.Class (MonadError)
import Control.Monad.Fail (MonadFail)
import Control.Monad.Catch (MonadThrow)
import Control.Monad.Fail (MonadFail(..))
import Control.Monad.Trans.Except
import Control.Monad.Trans.Class
import Control.Monad.IO.Class
Expand All @@ -81,6 +83,7 @@ import qualified What4.Interface as W4
import qualified What4.LabeledPred as W4
import qualified What4.ProgramLoc as W4

import SAWScript.Exceptions
import SAWScript.Crucible.Common (Sym)
import SAWScript.Crucible.Common.MethodSpec as MS

Expand Down Expand Up @@ -252,13 +255,21 @@ data RW
-- and side-conditions needed to proceed.
newtype OverrideMatcher ext rorw a =
OM (StateT (OverrideState ext) (ExceptT (OverrideFailure ext) IO) a)
deriving (Applicative, Functor, Generic, Generic1, Monad, MonadIO, MonadFail)
deriving (Applicative, Functor, Generic, Generic1, Monad, MonadIO, MonadThrow)

instance Wrapped (OverrideMatcher ext rorw a) where

deriving instance MonadState (OverrideState ext) (OverrideMatcher ext rorw)
deriving instance MonadError (OverrideFailure ext) (OverrideMatcher ext rorw)

throwOverrideMatcher :: String -> OverrideMatcher ext rorw a
throwOverrideMatcher msg = do
loc <- use osLocation
X.throw $ OverrideMatcherException loc msg

instance MonadFail (OverrideMatcher ext rorw) where
fail = throwOverrideMatcher

-- | "Run" function for OverrideMatcher. The final result and state
-- are returned. The state will contain the updated globals and substitutions
runOverrideMatcher ::
Expand Down Expand Up @@ -291,7 +302,7 @@ readGlobal ::
readGlobal k =
do mb <- OM (uses overrideGlobals (Crucible.lookupGlobal k))
case mb of
Nothing -> fail ("No such global: " ++ show k)
Nothing -> throwOverrideMatcher ("No such global: " ++ show k)
Just v -> return v

writeGlobal ::
Expand Down
13 changes: 4 additions & 9 deletions src/SAWScript/Crucible/Common/Setup/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ module SAWScript.Crucible.Common.Setup.Builtins where
import Control.Lens
import Control.Monad (when)
import Control.Monad.State (get)
import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map

import qualified What4.ProgramLoc as W4
Expand All @@ -32,45 +31,41 @@ import SAWScript.Crucible.Common.Setup.Type
-- TODO: crucible_fresh_var?

crucible_precond ::
Fail.MonadFail m =>
W4.ProgramLoc ->
TypedTerm ->
CrucibleSetupT ext m ()
CrucibleSetup ext ()
crucible_precond loc p = do
st <- get
when (st ^. csPrePost == MS.PostState) $
fail "attempt to use `crucible_precond` in post state"
addCondition (MS.SetupCond_Pred loc p)

crucible_postcond ::
Fail.MonadFail m =>
W4.ProgramLoc ->
TypedTerm ->
CrucibleSetupT ext m ()
CrucibleSetup ext ()
crucible_postcond loc p = do
st <- get
when (st ^. csPrePost == MS.PreState) $
fail "attempt to use `crucible_postcond` in pre state"
addCondition (MS.SetupCond_Pred loc p)

crucible_return ::
Fail.MonadFail m =>
BuiltinContext ->
Options ->
MS.SetupValue ext ->
CrucibleSetupT ext m ()
CrucibleSetup ext ()
crucible_return _bic _opt retval = do
ret <- use (csMethodSpec . MS.csRetValue)
case ret of
Just _ -> fail "crucible_return: duplicate return value specification"
Nothing -> csMethodSpec . MS.csRetValue .= Just retval

crucible_execute_func ::
Monad m =>
BuiltinContext ->
Options ->
[MS.SetupValue ext] ->
CrucibleSetupT ext m ()
CrucibleSetup ext ()
crucible_execute_func _bic _opt args = do
tps <- use (csMethodSpec . MS.csArgs)
csPrePost .= MS.PostState
Expand Down
Loading