Skip to content

Commit

Permalink
crucible{,-go,-jvm}: Shared type for typed overrides
Browse files Browse the repository at this point in the history
  • Loading branch information
@langston-barrett
langston-barrett committed Nov 16, 2023
1 parent 0834003 commit e097fd6
Show file tree
Hide file tree
Showing 5 changed files with 151 additions and 88 deletions.
66 changes: 34 additions & 32 deletions crucible-go/src/Lang/Crucible/Go/Overrides.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,23 +42,27 @@ 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 }
SomeOverride pkg (functionNameFromText nm) $
C.TypedOverride
{ C.typedOverrideHandler = overrideSim
, C.typedOverrideArgs = argsRepr
, C.typedOverrideRet = retRepr
}

mkFresh :: IsSymInterface sym
=> String
Expand Down Expand Up @@ -92,25 +96,23 @@ fresh_string :: IsSymInterface sym
fresh_string si = mkFresh "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 +121,26 @@ 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" "FreshInt" Ctx.empty (BVRepr w) (\_args -> fresh_int w)
, mkSomeOverride "crucible" "FreshInt8" Ctx.empty
(BVRepr (knownNat :: NatRepr 8)) fresh_int'
(BVRepr (knownNat :: NatRepr 8)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshInt16" Ctx.empty
(BVRepr (knownNat :: NatRepr 16)) fresh_int'
(BVRepr (knownNat :: NatRepr 16)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshInt32" Ctx.empty
(BVRepr (knownNat :: NatRepr 32)) fresh_int'
(BVRepr (knownNat :: NatRepr 32)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshInt64" Ctx.empty
(BVRepr (knownNat :: NatRepr 64)) fresh_int'
, mkSomeOverride "crucible" "FreshUint" Ctx.empty (BVRepr w) (fresh_int w)
(BVRepr (knownNat :: NatRepr 64)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshUint" Ctx.empty (BVRepr w) (\_args -> fresh_int w)
, mkSomeOverride "crucible" "FreshUint8" Ctx.empty
(BVRepr (knownNat :: NatRepr 8)) fresh_int'
(BVRepr (knownNat :: NatRepr 8)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshUint16" Ctx.empty
(BVRepr (knownNat :: NatRepr 16)) fresh_int'
(BVRepr (knownNat :: NatRepr 16)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshUint32" Ctx.empty
(BVRepr (knownNat :: NatRepr 32)) fresh_int'
(BVRepr (knownNat :: NatRepr 32)) (\_args -> fresh_int')
, mkSomeOverride "crucible" "FreshUint64" Ctx.empty
(BVRepr (knownNat :: NatRepr 64)) fresh_int'
(BVRepr (knownNat :: NatRepr 64)) (\_args -> fresh_int')
, 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 +154,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
View file
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.mkTypedOverride fnm o)
_ -> panic "[Go simulator] mkFunctionBindings"
[ "Type mismatch for override of " ++ show ident
, " Expected: " ++ show (cfgArgTypes cfg) ++ " -> " ++ show (cfgReturnType cfg)
Expand Down
5 changes: 5 additions & 0 deletions crucible-jvm/Main.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
class Main {
public static void main(String args[]) {
System.out.println("Hello, world!");
}
}
127 changes: 73 additions & 54 deletions crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs
View file
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

0 comments on commit e097fd6

Please sign in to comment.