Concretize the argument to @fresh-bytes

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 ->

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)

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

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

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