Add support for x86 64 bit integer stack arguments. #2007
Conversation
andreistefanescu
force-pushed
the
x86-stack-args
branch
from
a68689e
to
a3ff26c
Compare
andreistefanescu
force-pushed
the
x86-stack-args
branch
from
a3ff26c
to
9b2a33a
Compare
| finalMem <- liftIO $ C.LLVM.doStore bak mem' ptr | ||
| rsp <- getReg Macaw.RSP regs | ||
| ptr <- liftIO $ C.LLVM.doPtrAddOffset bak mem rsp =<< W4.bvLit sym knownNat (BV.mkBV knownNat (-8)) | ||
| let writeAlign = C.LLVM.noAlignment |
There was a problem hiding this comment.
Why the change from integerToAlignment defaultStackBaseAlign to noAlignment?
There was a problem hiding this comment.
nice catch! Actually, this reveals a bug. The stack needs to be 16 byte aligned before the call instruction is executed, that is, before the return address has been pushed. The existing check is on %rsp after the return address has been pushed.
| liftIO $ exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case | ||
| C.LLVM.PtrType _ -> pure () | ||
| C.LLVM.IntType 64 -> pure () | ||
| _ -> fail "Stack argument is not a 64 bit integer." |
There was a problem hiding this comment.
Are we only handling 64-bit arguments at this point? If test_llvm_x86_08 changed argument h from unsigned long to unsigned char, does clang promote it to a ulong argument or do we fail here?
Also, what are the expected semantics of fail here? Do we have a MonadFail instance with special handling, or should this use panic as on line 1061?
There was a problem hiding this comment.
Longer term, it might be interesting to look at the abide library and utilize the functionality from there in this effort to consolidate and centralize our ABI handling. That said, I think that would be a future effort and not part of this utilitarian PR.
There was a problem hiding this comment.
yes, this only handles 64-bit arguments. I didn't investigate what clang does, I think it doesn't promote it. The semantics if fail, since this can happen, and it's just not handled. Also, this doesn't handle float/doable, and other non-integer types.
|
|
||
| regs' <- use x86Regs | ||
| rsp <- getReg Macaw.RSP regs' | ||
| rsp' <- liftIO $ C.LLVM.doPtrAddOffset bak mem rsp =<< W4.bvLit sym knownNat (BV.mkBV knownNat (-8)) |
There was a problem hiding this comment.
Where do we detect/handle stack overflow? Is that just normal SAW detection of addressing memory not valid for the allocation in 969+970?
There was a problem hiding this comment.
yes, it's just standard detection.
No description provided.