From 2bcc1fceeb8ed33c4d7d6ec34ebf155e4c374094 Mon Sep 17 00:00:00 2001 From: 2over12 Date: Thu, 18 Sep 2025 18:23:03 -0400 Subject: [PATCH] expose enough to concretize fresh bytes --- grease/src/Grease/LLVM.hs | 6 +++- grease/src/Grease/LLVM/Overrides.hs | 46 +++++++++++++++++++++------ grease/src/Grease/LLVM/SetupHook.hs | 14 +++++--- grease/src/Grease/Macaw/Overrides.hs | 3 +- grease/src/Grease/Syntax/Overrides.hs | 34 +++++++++++++++----- 5 files changed, 79 insertions(+), 24 deletions(-) diff --git a/grease/src/Grease/LLVM.hs b/grease/src/Grease/LLVM.hs index bc85024a..f46fd1cf 100644 --- a/grease/src/Grease/LLVM.hs +++ b/grease/src/Grease/LLVM.hs @@ -34,9 +34,11 @@ import Lang.Crucible.LLVM.TypeContext qualified as TCtx import Lang.Crucible.Simulator qualified as C import Lang.Crucible.Simulator.GlobalState qualified as C import What4.Expr qualified as W4 +import Lang.Crucible.Backend.Online qualified as C +import What4.Protocol.Online qualified as W4 initState :: - forall p sym bak arch m t st fs argTys retTy. + forall p sym bak arch m t st fs argTys retTy solver. ( MonadIO m , MonadThrow m , C.IsSymBackend sym bak @@ -47,6 +49,8 @@ initState :: , Mem.HasLLVMAnn sym , HasToConcretize p , ?memOpts :: Mem.MemOptions + , bak ~ C.OnlineBackend solver t st fs + , W4.OnlineSolver solver ) => bak -> GreaseLogAction -> diff --git a/grease/src/Grease/LLVM/Overrides.hs b/grease/src/Grease/LLVM/Overrides.hs index 0ac33095..5bf0ab27 100644 --- a/grease/src/Grease/LLVM/Overrides.hs +++ b/grease/src/Grease/LLVM/Overrides.hs @@ -50,6 +50,9 @@ import Lang.Crucible.Syntax.Concrete qualified as CSyn import Lumberjack qualified as LJ import Text.LLVM.AST qualified as L import What4.FunctionName qualified as W4 +import What4.Expr qualified as W4 +import Lang.Crucible.Backend.Online qualified as C +import What4.Protocol.Online qualified as W4 doLog :: MonadIO m => GreaseLogAction -> Diag.Diagnostic -> m () doLog la diag = LJ.writeLog la (LLVMOverridesDiagnostic diag) @@ -110,12 +113,16 @@ forwardDeclDecls m = -- -- * User-defined overrides from S-expressions (see 'loadOverrides') registerLLVMOverrides :: - forall sym bak arch p rtp as r. + forall sym bak arch p rtp as r solver scope st fs. ( C.IsSymBackend sym bak , Mem.HasLLVMAnn sym , Mem.HasPtrWidth 64 , ToConc.HasToConcretize p , ?lc :: TypeContext + , C.IsSymBackend sym bak + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver , ?memOpts :: Mem.MemOptions ) => GreaseLogAction -> @@ -182,7 +189,7 @@ registerLLVMOverrides la builtinOvs userOvs bak llvmCtx fs decls = do -- overrides. We only do this after registering all of the public functions -- so as to ensure that we get the dependencies correct. Foldable.for_ userOvs $ \(_, lso) -> - registerLLVMOvForwardDeclarations mvar allOvs $ + registerLLVMOvForwardDeclarations bak mvar allOvs $ lsoForwardDeclarations lso pure allOvs where @@ -201,13 +208,16 @@ registerLLVMOverrides la builtinOvs userOvs bak llvmCtx fs decls = do -- -- * User-defined overrides from S-expressions (see 'loadOverrides') registerLLVMSexpOverrides :: - forall sym bak arch p rtp as r. + forall sym bak arch p rtp as r solver scope st fs. ( C.IsSymBackend sym bak , Mem.HasLLVMAnn sym , Mem.HasPtrWidth 64 , ToConc.HasToConcretize p , ?lc :: TypeContext , ?memOpts :: Mem.MemOptions + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver ) => GreaseLogAction -> Seq.Seq (CLLVM.OverrideTemplate p sym CLLVM.LLVM arch) -> @@ -233,13 +243,16 @@ registerLLVMSexpOverrides la builtinOvs sexpOvs bak llvmCtx fs prog = do -- -- * User-defined overrides from S-expressions (see 'loadOverrides') registerLLVMModuleOverrides :: - forall sym bak arch p rtp as r. + forall sym bak arch p rtp as r solver scope st fs. ( C.IsSymBackend sym bak , Mem.HasLLVMAnn sym , Mem.HasPtrWidth 64 , ToConc.HasToConcretize p , ?lc :: TypeContext , ?memOpts :: Mem.MemOptions + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver ) => GreaseLogAction -> Seq.Seq (CLLVM.OverrideTemplate p sym CLLVM.LLVM arch) -> @@ -265,7 +278,11 @@ registerLLVMSexpProgForwardDeclarations :: , Mem.HasPtrWidth 64 , ToConc.HasToConcretize p , ?memOpts :: Mem.MemOptions + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver ) => + bak -> GreaseLogAction -> CLLVM.DataLayout -> C.GlobalVar Mem.Mem -> @@ -274,8 +291,8 @@ registerLLVMSexpProgForwardDeclarations :: -- | The map of forward declaration names to their handles. Map.Map W4.FunctionName C.SomeHandle -> C.OverrideSim p sym CLLVM.LLVM rtp as r () -registerLLVMSexpProgForwardDeclarations la dl mvar funOvs = - registerLLVMForwardDeclarations mvar funOvs $ +registerLLVMSexpProgForwardDeclarations bak la dl mvar funOvs = + registerLLVMForwardDeclarations bak mvar funOvs $ registerSkipOverride la dl mvar -- | Redirect handles for forward declarations in an LLVM S-expression override @@ -287,15 +304,19 @@ registerLLVMOvForwardDeclarations :: , Mem.HasLLVMAnn sym , ToConc.HasToConcretize p , ?memOpts :: Mem.MemOptions + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver ) => + bak -> C.GlobalVar Mem.Mem -> -- | The map of public function names to their overrides. Map.Map W4.FunctionName (CLLVM.SomeLLVMOverride p sym CLLVM.LLVM) -> -- | The map of forward declaration names to their handles. Map.Map W4.FunctionName C.SomeHandle -> C.OverrideSim p sym CLLVM.LLVM rtp as r () -registerLLVMOvForwardDeclarations mvar funOvs = - registerLLVMForwardDeclarations mvar funOvs $ \fwdDecName _ -> +registerLLVMOvForwardDeclarations bak mvar funOvs = + registerLLVMForwardDeclarations bak mvar funOvs $ \fwdDecName _ -> declaredFunNotFound fwdDecName -- | Redirect handles for forward declarations in an S-expression file to @@ -307,7 +328,12 @@ registerLLVMForwardDeclarations :: , Mem.HasLLVMAnn sym , ToConc.HasToConcretize p , ?memOpts :: Mem.MemOptions + , C.IsSymBackend sym bak + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver ) => + bak -> C.GlobalVar Mem.Mem -> -- | The map of public function names to their overrides. Map.Map W4.FunctionName (CLLVM.SomeLLVMOverride p sym CLLVM.LLVM) -> @@ -320,7 +346,7 @@ registerLLVMForwardDeclarations :: -- | The map of forward declaration names to their handles. Map.Map W4.FunctionName C.SomeHandle -> C.OverrideSim p sym CLLVM.LLVM rtp as r () -registerLLVMForwardDeclarations mvar funOvs cannotResolve fwdDecs = +registerLLVMForwardDeclarations bak mvar funOvs cannotResolve fwdDecs = Foldable.for_ (Map.toList fwdDecs) $ \(fwdDecName, C.SomeHandle hdl) -> case Map.lookup fwdDecName funOvs of Just (CLLVM.SomeLLVMOverride llvmOverride) -> @@ -330,7 +356,7 @@ registerLLVMForwardDeclarations mvar funOvs cannotResolve fwdDecs = -- S-expression files with forward-declarations of them. case fwdDecName of "fresh-bytes" -> do - ok <- tryBindTypedOverride hdl (freshBytesOverride ?ptrWidth) + ok <- tryBindTypedOverride hdl (freshBytesOverride bak ?ptrWidth) unless ok (cannotResolve fwdDecName hdl) "read-bytes" -> do ok <- tryBindTypedOverride hdl (StrOv.readBytesOverride mvar) diff --git a/grease/src/Grease/LLVM/SetupHook.hs b/grease/src/Grease/LLVM/SetupHook.hs index 3097e33e..33303c24 100644 --- a/grease/src/Grease/LLVM/SetupHook.hs +++ b/grease/src/Grease/LLVM/SetupHook.hs @@ -40,6 +40,9 @@ import Lang.Crucible.Simulator qualified as C import Lang.Crucible.Syntax.Concrete qualified as CSyn import Lumberjack qualified as LJ import What4.FunctionName qualified as W4 +import What4.Expr qualified as W4 +import Lang.Crucible.Backend.Online qualified as C +import What4.Protocol.Online qualified as W4 doLog :: MonadIO m => GreaseLogAction -> Diag.Diagnostic -> m () doLog la diag = LJ.writeLog la (LLVMSetupHookDiagnostic diag) @@ -52,7 +55,7 @@ doLog la diag = LJ.writeLog la (LLVMSetupHookDiagnostic diag) -- c.f. 'Grease.Macaw.SetupHook.SetupHook' newtype SetupHook sym arch = SetupHook - ( forall p bak rtp a r. + ( forall p bak rtp a r solver scope st fs. ( C.IsSymBackend sym bak , ArchWidth arch ~ 64 , Mem.HasPtrWidth (ArchWidth arch) @@ -61,6 +64,9 @@ newtype SetupHook sym arch , ?lc :: TCtx.TypeContext , ?memOpts :: Mem.MemOptions , ?intrinsicsOpts :: CLLVM.IntrinsicsOptions + , sym ~ W4.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , W4.OnlineSolver solver ) => bak -> C.HandleAllocator -> @@ -89,14 +95,14 @@ syntaxSetupHook la ovs prog cfgs = -- In addition to binding function handles for the user overrides, -- we must also redirect function handles resulting from parsing -- forward declarations (`declare`) to actually call the overrides. - GLO.registerLLVMSexpProgForwardDeclarations la dl mvar funOvs (CSyn.parsedProgForwardDecs prog) + GLO.registerLLVMSexpProgForwardDeclarations bak la dl mvar funOvs (CSyn.parsedProgForwardDecs prog) -- If a startup override exists and it contains forward declarations, -- then we redirect the function handles to actually call the respective -- overrides. Monad.forM_ (Map.elems cfgs) $ \entrypointCfgs -> Monad.forM_ (GE.startupOvForwardDecs <$> GE.entrypointStartupOv entrypointCfgs) $ \startupOvFwdDecs -> - GLO.registerLLVMSexpProgForwardDeclarations la dl mvar funOvs startupOvFwdDecs + GLO.registerLLVMSexpProgForwardDeclarations bak la dl mvar funOvs startupOvFwdDecs -- Register defined functions. If there is a user override of the same -- name, use the override's definition instead so that it takes @@ -141,4 +147,4 @@ moduleSetupHook la ovs trans cfgs = -- overrides. Monad.forM_ (Map.elems cfgs) $ \entrypointCfgs -> Monad.forM_ (GE.startupOvForwardDecs <$> GE.entrypointStartupOv entrypointCfgs) $ \startupOvFwdDecs -> - GLO.registerLLVMSexpProgForwardDeclarations la dl mvar funOvs startupOvFwdDecs + GLO.registerLLVMSexpProgForwardDeclarations bak la dl mvar funOvs startupOvFwdDecs diff --git a/grease/src/Grease/Macaw/Overrides.hs b/grease/src/Grease/Macaw/Overrides.hs index 503e5cab..cca2c06b 100644 --- a/grease/src/Grease/Macaw/Overrides.hs +++ b/grease/src/Grease/Macaw/Overrides.hs @@ -352,7 +352,8 @@ lookupMacawForwardDeclarationOverride bak funOvs decName hdl = -- forward-declarations of them. case decName of "fresh-bytes" -> do - let ov = SExp.freshBytesOverride @_ @p @sym @(Symbolic.MacawExt arch) ?ptrWidth + -- p sym ext w scope st fs solver bak + let ov = SExp.freshBytesOverride @p @sym @(Symbolic.MacawExt arch) bak ?ptrWidth (C.Refl, C.Refl) <- SExp.checkTypedOverrideHandleCompat hdl ov Just (C.runTypedOverride (C.handleName hdl) ov) _ -> Nothing diff --git a/grease/src/Grease/Syntax/Overrides.hs b/grease/src/Grease/Syntax/Overrides.hs index 515248d3..cd45ebef 100644 --- a/grease/src/Grease/Syntax/Overrides.hs +++ b/grease/src/Grease/Syntax/Overrides.hs @@ -27,6 +27,11 @@ import Lang.Crucible.FunctionHandle qualified as LCF import Lang.Crucible.Simulator qualified as LCS import Lang.Crucible.Types qualified as LCT import What4.Interface qualified as WI +import Data.Macaw.Symbolic.Concretize qualified as MSC +import GHC.TypeNats qualified as PT +import Lang.Crucible.Backend.Online qualified as C +import What4.Expr.Builder qualified as WE +import What4.Protocol.Online qualified as WPO -- | Check if a 'LCS.TypedOverride' is compatible with a 'LCF.FnHandle' checkTypedOverrideHandleCompat :: @@ -58,15 +63,20 @@ tryBindTypedOverride hdl ov = -- The number of bytes must be concrete. If a symbolic number is passed this -- function will generate an assertion failure. freshBytesOverride :: + forall p sym ext w scope st fs solver bak. ( 1 <= w , ToConc.HasToConcretize p , LCB.IsSymInterface sym + , sym ~ WE.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver ) => + bak -> NatRepr.NatRepr w -> LCS.TypedOverride p sym ext (Ctx.EmptyCtx Ctx.::> LCT.StringType WI.Unicode Ctx.::> LCT.BVType w) (LCT.VectorType (LCT.BVType 8)) -freshBytesOverride w = +freshBytesOverride bak w = WI.withKnownNat w $ - LCS.typedOverride (Ctx.uncurryAssignment freshBytes) + LCS.typedOverride (Ctx.uncurryAssignment $ freshBytes bak) -- | Implementation of @fresh-bytes@ override. -- @@ -79,21 +89,29 @@ freshBytes :: ( 1 <= w , ToConc.HasToConcretize p , LCB.IsSymInterface sym + , PT.KnownNat w + , LCB.IsSymInterface sym + , sym ~ WE.ExprBuilder scope st fs + , bak ~ C.OnlineBackend solver scope st fs + , WPO.OnlineSolver solver ) => + bak -> LCS.RegValue' sym (LCT.StringType WI.Unicode) -> LCS.RegValue' sym (LCT.BVType w) -> LCS.OverrideSim p sym ext r args ret (LCS.RegValue sym (LCT.VectorType (LCT.BVType 8))) -freshBytes name0 bv0 = +freshBytes bak name0 bv0 = case WI.asString (LCS.unRV name0) of Nothing -> LCS.overrideError $ LCS.AssertFailureSimError "Call to @fresh-bytes with symbolic name" "" Just (WI.UnicodeLiteral name) -> - case WI.asBV (LCS.unRV bv0) of - Nothing -> - LCS.overrideError $ - LCS.AssertFailureSimError "Call to @fresh-bytes with symbolic length" "" - Just bv -> doFreshBytes name (BV.asUnsigned bv) + do + x <- liftIO $ MSC.resolveSymBV bak WI.knownNat (LCS.unRV bv0) + case WI.asBV x of + Nothing -> do + LCS.overrideError $ + LCS.AssertFailureSimError "Call to @fresh-bytes with symbolic length" "" + Just bv -> doFreshBytes name (BV.asUnsigned bv) doFreshBytes :: ( ToConc.HasToConcretize p