diff --git a/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs b/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs index 53fe5879..823c19f1 100644 --- a/refinement/src/Data/Macaw/Refinement/UnknownTransfer.hs +++ b/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 diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index 0dd1f46c..4285c5fa 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/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