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

Typed overrides #1136

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
96 changes: 42 additions & 54 deletions crucible-go/src/Lang/Crucible/Go/Overrides.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ as well as assuming and asserting boolean predicates.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Go.Overrides where
Expand Down Expand Up @@ -38,79 +39,74 @@ import Lang.Crucible.Types

import Lang.Crucible.Go.Types

import qualified Crux.Overrides as Crux
import qualified Crux.Types as Crux

data SomeOverride p sym ext where
SomeOverride :: Text -- ^ package name
-> CtxRepr args
-> TypeRepr ret
-> Override p sym ext args ret
-> FunctionName
-> C.TypedOverride p sym ext args ret
-> SomeOverride p sym ext

nameOfOverride :: Override p sym ext args ret -> Text
nameOfOverride (Override { overrideName = nm }) =
pack $ show nm

mkSomeOverride :: Text -> Text -> CtxRepr args -> TypeRepr ret ->
(forall r. C.OverrideSim p sym ext r args ret
(forall r args' ret'.
Assignment (C.RegValue' sym) args ->
C.OverrideSim p sym ext r args' ret'
(RegValue sym ret)) ->
SomeOverride p sym ext
mkSomeOverride pkg nm argsRepr retRepr overrideSim =
SomeOverride pkg argsRepr retRepr $
Override { overrideName = functionNameFromText nm
, overrideHandler = C.runOverrideSim retRepr overrideSim }

mkFresh :: IsSymInterface sym
=> String
-> BaseTypeRepr ty
-> Crux.OverM p sym ext (RegValue sym (BaseToType ty))
mkFresh nm ty =
do sym <- C.getSymInterface
liftIO $ W4.freshConstant sym (W4.safeSymbol nm) ty
SomeOverride pkg (functionNameFromText nm) $
C.TypedOverride
{ C.typedOverrideHandler = overrideSim
, C.typedOverrideArgs = argsRepr
, C.typedOverrideRet = retRepr
}

fresh_int :: (IsSymInterface sym, 1 <= w)
=> NatRepr w
-> Crux.OverM p sym ext (RegValue sym (BVType w))
fresh_int w = mkFresh "X" $ BaseBVRepr w
-> C.TypedOverride (p sym) sym ext Ctx.EmptyCtx (BVType w)
fresh_int w = Crux.baseFreshOverride' (W4.safeSymbol "X") (BaseBVRepr w)

fresh_int' :: (IsSymInterface sym, KnownNat w, 1 <= w)
=> Crux.OverM p sym ext (RegValue sym (BVType w))
fresh_int' :: (KnownNat w, 1 <= w, IsSymInterface sym)
=> C.TypedOverride (p sym) sym ext Ctx.EmptyCtx (BVType w)
fresh_int' = fresh_int knownNat

fresh_float :: IsSymInterface sym
=> FloatPrecisionRepr fp
-> Crux.OverM p sym ext
(RegValue sym (BaseToType (BaseFloatType fp)))
fresh_float fp = mkFresh "X" $ BaseFloatRepr fp
fresh_float fp = Crux.mkFresh (W4.safeSymbol "X") $ BaseFloatRepr fp

-- TODO: float, float32, float64

fresh_string :: IsSymInterface sym
=> StringInfoRepr si
-> Crux.OverM p sym ext
(RegValue sym (BaseToType (BaseStringType si)))
fresh_string si = mkFresh "X" $ BaseStringRepr si
fresh_string si = Crux.mkFresh (W4.safeSymbol "X") $ BaseStringRepr si

do_assume :: IsSymInterface sym
=> C.OverrideSim p sym ext gret
(EmptyCtx ::> StringType Unicode ::> StringType Unicode ::> BoolType)
(StructType EmptyCtx) (RegValue sym (StructType EmptyCtx))
do_assume = C.ovrWithBackend $ \bak -> do
=> Assignment (C.RegValue' sym) (EmptyCtx ::> StringType Unicode ::> StringType Unicode ::> BoolType)
-> C.OverrideSim p sym ext gret args ret (RegValue sym (StructType EmptyCtx))
do_assume args = C.ovrWithBackend $ \bak -> do
let sym = backendGetSym bak
RegMap (Empty :> mgs :> file :> b) <- C.getOverrideArgs
(Empty :> _mgs :> _file :> C.RV b) <- pure args
loc <- liftIO $ W4.getCurrentProgramLoc sym
liftIO $ addAssumption bak (GenericAssumption loc "assume" (regValue b))
liftIO $ addAssumption bak (GenericAssumption loc "assume" b)
return Ctx.empty

do_assert :: IsSymInterface sym
=> C.OverrideSim p sym ext gret
(EmptyCtx ::> StringType Unicode ::> StringType Unicode ::> BoolType)
(StructType EmptyCtx) (RegValue sym (StructType EmptyCtx))
do_assert = C.ovrWithBackend $ \bak -> do
=> Assignment (C.RegValue' sym) (EmptyCtx ::> StringType Unicode ::> StringType Unicode ::> BoolType)
-> C.OverrideSim p sym ext gret args ret (RegValue sym (StructType EmptyCtx))
do_assert args = C.ovrWithBackend $ \bak -> do
let sym = backendGetSym bak
RegMap (Empty :> mgs :> file :> b) <- C.getOverrideArgs
(Empty :> _mgs :> _file :> C.RV b) <- pure args
loc <- liftIO $ W4.getCurrentProgramLoc sym
liftIO $ addDurableAssertion bak (LabeledPred (regValue b)
liftIO $ addDurableAssertion bak (LabeledPred b
(C.SimError loc $ C.AssertFailureSimError
"assertion_failure" ""))
return Ctx.empty
Expand All @@ -119,26 +115,18 @@ go_overrides :: (IsSymInterface sym, 1 <= w)
=> NatRepr w
-> [SomeOverride (p sym) sym ext]
go_overrides w =
[ mkSomeOverride "crucible" "FreshInt" Ctx.empty (BVRepr w) (fresh_int w)
, mkSomeOverride "crucible" "FreshInt8" Ctx.empty
(BVRepr (knownNat :: NatRepr 8)) fresh_int'
, mkSomeOverride "crucible" "FreshInt16" Ctx.empty
(BVRepr (knownNat :: NatRepr 16)) fresh_int'
, mkSomeOverride "crucible" "FreshInt32" Ctx.empty
(BVRepr (knownNat :: NatRepr 32)) fresh_int'
, mkSomeOverride "crucible" "FreshInt64" Ctx.empty
(BVRepr (knownNat :: NatRepr 64)) fresh_int'
, mkSomeOverride "crucible" "FreshUint" Ctx.empty (BVRepr w) (fresh_int w)
, mkSomeOverride "crucible" "FreshUint8" Ctx.empty
(BVRepr (knownNat :: NatRepr 8)) fresh_int'
, mkSomeOverride "crucible" "FreshUint16" Ctx.empty
(BVRepr (knownNat :: NatRepr 16)) fresh_int'
, mkSomeOverride "crucible" "FreshUint32" Ctx.empty
(BVRepr (knownNat :: NatRepr 32)) fresh_int'
, mkSomeOverride "crucible" "FreshUint64" Ctx.empty
(BVRepr (knownNat :: NatRepr 64)) fresh_int'
[ SomeOverride "crucible" "FreshInt" (fresh_int w)
, SomeOverride "crucible" "FreshInt8" (fresh_int' @8)
, SomeOverride "crucible" "FreshInt16" (fresh_int' @16)
, SomeOverride "crucible" "FreshInt32" (fresh_int' @32)
, SomeOverride "crucible" "FreshInt64" (fresh_int' @64)
, SomeOverride "crucible" "FreshUint" (fresh_int w)
, SomeOverride "crucible" "FreshUint8" (fresh_int' @8)
, SomeOverride "crucible" "FreshUint16" (fresh_int' @16)
, SomeOverride "crucible" "FreshUint32" (fresh_int' @32)
, SomeOverride "crucible" "FreshUint64" (fresh_int' @64)
, mkSomeOverride "crucible" "FreshString" Ctx.empty
(StringRepr UnicodeRepr) $ fresh_string UnicodeRepr
(StringRepr UnicodeRepr) $ (\_args -> fresh_string UnicodeRepr)
, mkSomeOverride "crucible" "Assume"
(Ctx.Empty :> StringRepr UnicodeRepr :> StringRepr UnicodeRepr :> BoolRepr)
(StructRepr Ctx.empty) do_assume
Expand All @@ -152,8 +140,8 @@ lookupOverride :: Text
-> Maybe (SomeOverride p sym ext)
lookupOverride _pkgName _fName [] = Nothing
lookupOverride pkgName fName
(o@(SomeOverride pkg _argsRepr _retRepr override) : overrides) =
if pkgName == pkg && fName == overrideName override then
(o@(SomeOverride pkg ovrName typedOvr) : overrides) =
if pkgName == pkg && fName == ovrName then
Just o
else
lookupOverride pkgName fName overrides
Expand Down
4 changes: 2 additions & 2 deletions crucible-go/src/Lang/Crucible/Go/Simulate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -104,10 +104,10 @@ mkFunctionBindings :: forall sym p ext.
mkFunctionBindings _overrides [] = FnBindings emptyHandleMap
mkFunctionBindings overrides ((ident, AnyCFG cfg) : cfgs) =
let f = case lookupOverride' ident overrides of
Just (SomeOverride _pkg argsRepr retRepr override) ->
Just (SomeOverride _pkg fnm o@(C.TypedOverride override argsRepr retRepr)) ->
case (testEquality (cfgArgTypes cfg) argsRepr,
testEquality (cfgReturnType cfg) retRepr) of
(Just Refl, Just Refl) -> UseOverride override
(Just Refl, Just Refl) -> UseOverride (C.runTypedOverride fnm o)
_ -> panic "[Go simulator] mkFunctionBindings"
[ "Type mismatch for override of " ++ show ident
, " Expected: " ++ show (cfgArgTypes cfg) ++ " -> " ++ show (cfgReturnType cfg)
Expand Down
127 changes: 73 additions & 54 deletions crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Some
import Data.Parameterized.NatRepr as NR
import Data.Parameterized.TraversableFC (fmapFC)

-- crucible
import qualified Lang.Crucible.CFG.Core as C
Expand Down Expand Up @@ -149,12 +150,7 @@ data JVMOverride p sym = forall args ret.
{ jvmOverride_className :: J.ClassName
, jvmOverride_methodKey :: J.MethodKey
, jvmOverride_methodIsStatic :: Bool
, jvmOverride_args :: CtxRepr args
, jvmOverride_ret :: TypeRepr ret
, jvmOverride_def :: forall rtp args' ret'.
sym ->
Ctx.Assignment (C.RegEntry sym) args ->
C.OverrideSim p sym JVM rtp args' ret' (C.RegValue sym ret)
, jvmOverride_def :: C.TypedOverride p sym JVM args ret
}

newtype ArgTransformer p sym args args' =
Expand Down Expand Up @@ -217,15 +213,16 @@ build_jvm_override ::
TypeRepr ret ->
CtxRepr args' ->
TypeRepr ret' ->
(forall rtp' l' a'. Ctx.Assignment (C.RegEntry sym) args ->
(forall rtp' l' a'. Ctx.Assignment (C.RegValue' sym) args ->
C.OverrideSim p sym JVM rtp' l' a' (C.RegValue sym ret)) ->
C.OverrideSim p sym JVM rtp l a (C.Override p sym JVM args' ret')
build_jvm_override sym fnm args ret args' ret' llvmOverride =
build_jvm_override sym fnm args ret args' ret' jvmOverride =
do fargs <- transformJVMArgs sym args args' fnm
fret <- transformJVMRet sym ret ret'
return $ C.mkOverride' fnm ret' $
do C.RegMap xs <- C.getOverrideArgs
applyValTransformer fret =<< llvmOverride =<< applyArgTransformer fargs xs
fargs' <- applyArgTransformer fargs xs
applyValTransformer fret =<< jvmOverride (fmapFC (C.RV . C.regValue) fargs')

register_jvm_override :: forall p sym l a rtp
. (IsSymInterface sym)
Expand All @@ -234,9 +231,13 @@ register_jvm_override :: forall p sym l a rtp
register_jvm_override (JVMOverride { jvmOverride_className=cn
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=isStatic
, jvmOverride_args=overrideArgs
, jvmOverride_ret=overrideRet
, jvmOverride_def=def }) = do
, jvmOverride_def=
C.TypedOverride
{ C.typedOverrideHandler=def
, C.typedOverrideArgs=overrideArgs
, C.typedOverrideRet=overrideRet
}
}) = do
jvmctx <- get

let fnm = methodHandleName cn mk
Expand All @@ -245,7 +246,7 @@ register_jvm_override (JVMOverride { jvmOverride_className=cn


jvmToFunHandleRepr isStatic mk $ \derivedArgs derivedRet -> do
o <- lift $ build_jvm_override sym fnm overrideArgs overrideRet derivedArgs derivedRet (def sym)
o <- lift $ build_jvm_override sym fnm overrideArgs overrideRet derivedArgs derivedRet def
-- traceM $ "installing override for " ++ show fnm
case Map.lookup (cn,mk) (methodHandles jvmctx) of
Just (JVMHandleInfo _mkey h) -> do
Expand Down Expand Up @@ -284,10 +285,12 @@ gc_override =
JVMOverride { jvmOverride_className="java/lang/System"
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=isStatic
, jvmOverride_args=Ctx.Empty `Ctx.extend` refRepr
, jvmOverride_ret=UnitRepr
, jvmOverride_def=
\_sym _args -> return ()
C.TypedOverride
{ C.typedOverrideHandler= \_args -> return ()
, C.typedOverrideArgs=Ctx.Empty `Ctx.extend` refRepr
, C.typedOverrideRet=UnitRepr
}
}


Expand Down Expand Up @@ -593,13 +596,16 @@ printStreamUnit name showNewline =
JVMOverride { jvmOverride_className="java/io/PrintStream"
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=True
, jvmOverride_args=Ctx.Empty `Ctx.extend` refRepr
, jvmOverride_ret=UnitRepr
, jvmOverride_def=
\_sym args -> do
h <- C.printHandle <$> C.getContext
when showNewline (liftIO $ hPutStrLn h "")
liftIO $ hFlush h
C.TypedOverride
{ C.typedOverrideHandler=
\args -> do
h <- C.printHandle <$> C.getContext
when showNewline (liftIO $ hPutStrLn h "")
liftIO $ hFlush h
, C.typedOverrideArgs=Ctx.Empty `Ctx.extend` refRepr
, C.typedOverrideRet=UnitRepr
}
}

-- Should we print to the print handle in the simulation context?
Expand All @@ -625,15 +631,18 @@ printStream name showNewline descr t =
else JVMOverride { jvmOverride_className="java/io/PrintStream"
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=isStatic
, jvmOverride_args=Ctx.Empty `Ctx.extend` refRepr `Ctx.extend` t
, jvmOverride_ret=UnitRepr
, jvmOverride_def=
\_sym args -> do
let reg = C.regValue (Ctx.last args)
str <- showReg @sym (head (J.methodKeyParameterTypes mk)) t reg
h <- C.printHandle <$> C.getContext
liftIO $ (if showNewline then hPutStrLn else hPutStr) h str
liftIO $ hFlush h
C.TypedOverride
{ C.typedOverrideHandler=
\args -> do
let reg = C.unRV (Ctx.last args)
str <- showReg @sym (head (J.methodKeyParameterTypes mk)) t reg
h <- C.printHandle <$> C.getContext
liftIO $ (if showNewline then hPutStrLn else hPutStr) h str
liftIO $ hFlush h
, C.typedOverrideArgs=Ctx.Empty `Ctx.extend` refRepr `Ctx.extend` t
, C.typedOverrideRet=UnitRepr
}
}

flush_override :: (IsSymInterface sym) => JVMOverride p sym
Expand All @@ -643,12 +652,15 @@ flush_override =
JVMOverride { jvmOverride_className="java/io/BufferedOutputStream"
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=isStatic
, jvmOverride_args=Ctx.Empty `Ctx.extend` refRepr
, jvmOverride_ret=UnitRepr
, jvmOverride_def=
\_sym _args -> do
h <- C.printHandle <$> C.getContext
liftIO $ hFlush h
C.TypedOverride
{ C.typedOverrideHandler=
\_args -> do
h <- C.printHandle <$> C.getContext
liftIO $ hFlush h
, C.typedOverrideArgs=Ctx.Empty `Ctx.extend` refRepr
, C.typedOverrideRet=UnitRepr
}
}

-- java.lang.Throwable.fillInStackTrace (i.e. just returns this)
Expand All @@ -661,12 +673,15 @@ fillInStackTrace_override =
JVMOverride { jvmOverride_className="java/io/BufferedOutputStream"
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=isStatic
, jvmOverride_args=Ctx.Empty `Ctx.extend` refRepr
, jvmOverride_ret=refRepr
, jvmOverride_def=
\_sym args -> do
let reg = C.regValue (Ctx.last args)
return reg
C.TypedOverride
{ C.typedOverrideHandler=
\args -> do
let reg = C.unRV (Ctx.last args)
return reg
, C.typedOverrideArgs=Ctx.Empty `Ctx.extend` refRepr
, C.typedOverrideRet=refRepr
}
}

-- OMG This is difficult to define
Expand All @@ -677,23 +692,27 @@ isArray_override =
JVMOverride { jvmOverride_className="java/lang/Class"
, jvmOverride_methodKey=mk
, jvmOverride_methodIsStatic=isStatic
, jvmOverride_args=Ctx.Empty `Ctx.extend` refRepr
, jvmOverride_ret=intRepr
, jvmOverride_def=
\sym args -> do
let reg :: W4.PartExpr (W4.Pred sym) (C.MuxTree sym (RefCell JVMObjectType))
reg = C.regValue (Ctx.last args)
bvFalse <- liftIO $ return $ W4.bvLit sym knownRepr (BV.zero knownRepr)
C.TypedOverride
{ C.typedOverrideHandler=
\args -> C.ovrWithBackend $ \bak -> do
let sym = backendGetSym bak
let reg :: W4.PartExpr (W4.Pred sym) (C.MuxTree sym (RefCell JVMObjectType))
reg = C.unRV (Ctx.last args)
bvFalse <- liftIO $ return $ W4.bvLit sym knownRepr (BV.zero knownRepr)
{-
let k :: RefCell JVMObjectType -> IO (W4.SymBV sym 32)
k = undefined
let h :: W4.Pred sym -> (W4.SymBV sym 32) -> (W4.SymBV sym 32) -> IO (W4.SymBV sym 32)
h = undefined
let g :: (C.MuxTree sym (RefCell JVMObjectType)) -> IO (W4.SymBV sym 32)
-> IO (W4.SymBV sym 32)
g mux curr = undefined
let k :: RefCell JVMObjectType -> IO (W4.SymBV sym 32)
k = undefined
let h :: W4.Pred sym -> (W4.SymBV sym 32) -> (W4.SymBV sym 32) -> IO (W4.SymBV sym 32)
h = undefined
let g :: (C.MuxTree sym (RefCell JVMObjectType)) -> IO (W4.SymBV sym 32)
-> IO (W4.SymBV sym 32)
g mux curr = undefined
-}
liftIO $ foldr undefined bvFalse reg
liftIO $ foldr undefined bvFalse reg
, C.typedOverrideArgs=Ctx.Empty `Ctx.extend` refRepr
, C.typedOverrideRet=intRepr
}
}


Expand Down
Loading
Loading