Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Handle globals in x86 postconditons. #795

Merged
merged 1 commit into from
Jul 24, 2020
Merged

Handle globals in x86 postconditons. #795

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 18 additions & 7 deletions src/SAWScript/Crucible/LLVM/X86.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -544,12 +544,28 @@ assumePointsTo ::
assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do
when (isJust cond) $ throwX86 "unsupported x86_64 command: crucible_conditional_points_to"
tval <- checkConcreteSizePointsToValue tptval
sym <- use x86Sym
cc <- use x86CrucibleContext
mem <- use x86Mem
ptr <- resolvePtrSetupValue env tyenv tptr
val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval
storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval
mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val
x86Mem .= mem'

resolvePtrSetupValue ::
X86Constraints =>
Map MS.AllocIndex Ptr ->
Map MS.AllocIndex LLVMAllocSpec ->
MS.SetupValue LLVM ->
X86Sim Ptr
resolvePtrSetupValue env tyenv tptr = do
sym <- use x86Sym
cc <- use x86CrucibleContext
mem <- use x86Mem
elf <- use x86Elf
base <- use x86GlobalBase
ptr <- case tptr of
case tptr of
MS.SetupGlobal () nm -> case
(Vector.!? 0)
. Vector.filter (\e -> Elf.steName e == encodeUtf8 (Text.pack nm))
Expand All @@ -562,10 +578,6 @@ assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do
liftIO $ C.LLVM.doPtrAddOffset sym mem base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr)
_ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64)
=<< resolveSetupVal cc mem env tyenv Map.empty tptr
val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval
storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval
mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val
x86Mem .= mem'

checkConcreteSizePointsToValue :: LLVMPointsToValue LLVMArch -> X86Sim (MS.SetupValue LLVM)
checkConcreteSizePointsToValue = \case
Expand Down Expand Up @@ -700,8 +712,7 @@ assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptexpected) = do
cc <- use x86CrucibleContext
ms <- use x86MethodSpec
mem <- use x86Mem
ptr <- liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64)
=<< resolveSetupVal cc mem env tyenv Map.empty tptr
ptr <- resolvePtrSetupValue env tyenv tptr
memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv texpected
storTy <- liftIO $ C.LLVM.toStorableType memTy
actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment
Expand Down