[refinement] Add an unbounded memory allocation at the bottom of the allocation stack.

refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs

@@ -445,6 +445,7 @@ data RefinementContext arch t solver fp = RefinementContext
   , memVar :: C.GlobalVar LLVM.Mem
   , mem :: LLVM.MemImpl (C.OnlineBackend t solver fp)
   , memPtrTable :: MSM.MemPtrTable (C.OnlineBackend t solver fp) (MC.ArchAddrWidth arch)
+  , globalMappingFn :: MS.GlobalMap (C.OnlineBackend t solver fp) (MC.ArchAddrWidth arch)
   }
 
 withDefaultRefinementContext
@@ -459,39 +460,50 @@ withDefaultRefinementContext loaded_binary k = do
     C.withZ3OnlineBackend nonce_gen C.NoUnsatFeatures $ \sym ->
       case MS.archVals (Proxy @arch) of
         Just arch_vals -> do
-          -- path_setter <- W.getOptionSetting W.z3Path (W.getConfiguration sym)
-          -- _ <- W.setOpt path_setter "z3-tee"
 
           mem_var <- stToIO $ LLVM.mkMemVar handle_alloc
-          -- empty_mem <- LLVM.emptyMem LLVM.LittleEndian
-          -- let ?ptrWidth = W.knownNat
-          -- (base_ptr, allocated_mem) <- LLVM.doMallocUnbounded
-          --   sym
-          --   LLVM.GlobalAlloc
-          --   LLVM.Mutable
-          --   "flat memory"
-          --   empty_mem
-          --   LLVM.noAlignment
-          -- let Right mem_name = W.userSymbol "mem"
-          -- mem_array <- W.freshConstant sym mem_name W.knownRepr
-          -- initialized_mem <- LLVM.doArrayStoreUnbounded
-          --   sym
-          --   allocated_mem
-          --   base_ptr
-          --   LLVM.noAlignment
-          --   mem_array
+
           (mem, mem_ptr_table) <- MSM.newGlobalMemory
             (Proxy @arch)
             sym
             LLVM.LittleEndian
             MSM.ConcreteMutable
             (MBL.memoryImage loaded_binary)
+
+          let ?ptrWidth = W.knownNat
+          (base_ptr, allocated_mem) <- LLVM.doMallocUnbounded
+            sym
+            LLVM.GlobalAlloc
+            LLVM.Mutable
+            "flat memory"
+            mem
+            LLVM.noAlignment
+          let Right mem_name = W.userSymbol "mem"
+          mem_array <- W.freshConstant sym mem_name W.knownRepr
+          initialized_mem <- LLVM.doArrayStoreUnbounded
+            sym
+            allocated_mem
+            base_ptr
+            LLVM.noAlignment
+            mem_array
+
+          let global_mapping_fn = \sym' mem' base off -> do
+                flat_mem_ptr <- LLVM.ptrAdd sym' W.knownNat base_ptr off
+                MSM.mapRegionPointers
+                  mem_ptr_table
+                  flat_mem_ptr
+                  sym'
+                  mem'
+                  base
+                  off
+
           MS.withArchEval arch_vals sym $ \arch_eval_fns -> do
             let ext_impl = MS.macawExtensions
                   arch_eval_fns
                   mem_var
-                  (MSM.mapRegionPointers mem_ptr_table)
+                  global_mapping_fn
                   (MS.LookupFunctionHandle $ \_ _ _ -> undefined)
+
             k $ RefinementContext
               { symbolicBackend = sym
               , archVals = arch_vals
@@ -499,9 +511,9 @@ withDefaultRefinementContext loaded_binary k = do
               , nonceGenerator = nonce_gen
               , extensionImpl = ext_impl
               , memVar = mem_var
-              -- , mem = empty_mem
-              , mem = mem
+              , mem = initialized_mem
               , memPtrTable = mem_ptr_table
+              , globalMappingFn = global_mapping_fn
               }
         Nothing -> fail $ "unsupported architecture"
 
@@ -582,7 +594,7 @@ smtSolveTransfer RefinementContext{..} discovery_state blocks = do
   ip_off <- liftIO $ W.bvLit symbolicBackend W.knownNat $
     MC.memWordToUnsigned $ MC.addrOffset entry_addr
   entry_ip_val <- liftIO $ fromJust <$>
-    (MSM.mapRegionPointers memPtrTable) symbolicBackend mem2 ip_base ip_off
+    globalMappingFn symbolicBackend mem2 ip_base ip_off
 
   init_regs <- initRegs archVals symbolicBackend entry_ip_val init_sp_val
   some_cfg <- liftIO $ stToIO $ MS.mkBlockPathCFG

symbolic/src/Data/Macaw/Symbolic/Memory.hs

@@ -342,10 +342,11 @@ mapRegionPointers :: ( MC.MemWidth w
                      , CB.IsSymInterface sym
                      )
                   => MemPtrTable sym w
+                  -> CL.LLVMPtr sym w
                   -> MS.GlobalMap sym w
-mapRegionPointers mpt = \sym mem regionNum offsetVal ->
+mapRegionPointers mpt default_ptr = \sym mem regionNum offsetVal ->
   case WI.asNat regionNum of
-    Just 0 -> mapBitvectorToLLVMPointer mpt sym mem offsetVal
+    Just 0 -> mapBitvectorToLLVMPointer mpt sym mem offsetVal default_ptr
     Just _ ->
       -- This is the case where the region number is concrete and non-zero,
       -- meaning that it is already an LLVM pointer
@@ -354,7 +355,7 @@ mapRegionPointers mpt = \sym mem regionNum offsetVal ->
       -- In this case, the region number is symbolic, so we need to be very
       -- careful to handle the possibility that it is zero (and thus must be
       -- conditionally mapped to one or all of our statically-allocated regions.
-      mapSymbolicRegionPointer mpt sym mem regionNum offsetVal
+      mapSymbolicRegionPointer mpt sym mem regionNum offsetVal default_ptr
 
 -- | This is a relatively simple case where we know that the region number is
 -- zero.  This means that the bitvector we have needs to be mapped to a pointer.
@@ -366,8 +367,9 @@ mapBitvectorToLLVMPointer :: ( MC.MemWidth w
                           -> sym
                           -> CS.RegValue sym CL.Mem
                           -> CS.RegValue sym (CT.BVType w)
+                          -> CL.LLVMPtr sym w
                           -> IO (Maybe (CL.LLVMPtr sym w))
-mapBitvectorToLLVMPointer mpt@(MemPtrTable im _) sym mem offsetVal =
+mapBitvectorToLLVMPointer mpt@(MemPtrTable im _) sym mem offsetVal default_ptr =
   case WI.asUnsignedBV offsetVal of
     Just concreteOffset -> do
       -- This is the simplest case where the bitvector is concretely known.  We
@@ -399,7 +401,7 @@ mapBitvectorToLLVMPointer mpt@(MemPtrTable im _) sym mem offsetVal =
       --
       -- We will handle this by creating a mux tree that allows the pointer to
       -- be in *any* of our statically-allocated regions.
-      Just <$> staticRegionMuxTree mpt sym mem offsetVal
+      Just <$> staticRegionMuxTree mpt sym mem offsetVal default_ptr
 
 -- | Create a mux tree that maps the input bitvector (which is the offset in a
 -- LLVMPointer with region == 0) to one of the regions that are statically
@@ -420,11 +422,10 @@ staticRegionMuxTree :: ( CB.IsSymInterface sym
                     -> sym
                     -> CL.MemImpl sym
                     -> WI.SymExpr sym (WI.BaseBVType w)
+                    -> CL.LLVMPtr sym w
                     -> IO (CL.LLVMPtr sym w)
-staticRegionMuxTree (MemPtrTable im _) sym mem offsetVal = do
-  let rep = WI.bvWidth offsetVal
-  np <- CL.mkNullPointer sym rep
-  F.foldlM addMuxForRegion np (IM.toList im)
+staticRegionMuxTree (MemPtrTable im _) sym mem offsetVal default_ptr =
+  F.foldlM addMuxForRegion default_ptr (IM.toList im)
   where
     handleCase f alloc start end greater less = do
       let rep = WI.bvWidth offsetVal
@@ -457,10 +458,11 @@ mapSymbolicRegionPointer :: ( MC.MemWidth w
                          -> CS.RegValue sym CL.Mem
                          -> CS.RegValue sym CT.NatType
                          -> CS.RegValue sym (CT.BVType w)
+                         -> CL.LLVMPtr sym w
                          -> IO (Maybe (CL.LLVMPtr sym w))
-mapSymbolicRegionPointer mpt sym mem regionNum offsetVal = do
+mapSymbolicRegionPointer mpt sym mem regionNum offsetVal default_ptr = do
   zeroNat <- WI.natLit sym 0
-  staticRegion <- staticRegionMuxTree mpt sym mem offsetVal
+  staticRegion <- staticRegionMuxTree mpt sym mem offsetVal default_ptr
   isZeroRegion <- WI.natEq sym zeroNat regionNum
   let nonZeroPtr = CL.LLVMPointer regionNum offsetVal
   Just <$> CL.muxLLVMPtr sym isZeroRegion staticRegion nonZeroPtr