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.

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

Check for poison values in fptosi and fptoui #137

Open
langston-barrett opened this issue Jan 10, 2019 · 1 comment
Open

Check for poison values in fptosi and fptoui #137

langston-barrett opened this issue Jan 10, 2019 · 1 comment
Labels
llvm poison Issues touching on the LLVM concept of poison unsoundness Potential for incorrect proofs exists

Comments

@langston-barrett
Copy link
Contributor

langston-barrett commented Jan 10, 2019

The LLVM language reference says:

The ‘fptoui’ instruction converts its floating-point operand into the nearest (rounding towards zero) unsigned integer value. If the value cannot fit in ty2, the result is a poison value.

and

The ‘fptosi’ instruction converts its floating-point operand into the nearest (rounding towards zero) signed integer value. If the value cannot fit in ty2, the result is a poison value.

However, it doesn't appear that we're currently checking for poison values there by adding side conditions:

L.FpToUi -> do
outty' <- liftMemType' outty
x' <- transTypedValue x
let demoteToInt :: (1 <= w) => NatRepr w -> Expr (LLVM arch) s (FloatType fi) -> LLVMExpr s arch
demoteToInt w v = BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w $ App $ FloatToBV w RNE v)
llvmTypeAsRepr outty' $ \outty'' ->
case (asScalar x', outty'') of
(Scalar (FloatRepr _) x'', LLVMPointerRepr w) -> return $ demoteToInt w x''
_ -> fail (unlines [unwords ["Invalid fptoui:", show op, show x, show outty], showI])
L.FpToSi -> do
outty' <- liftMemType' outty
x' <- transTypedValue x
let demoteToInt :: (1 <= w) => NatRepr w -> Expr (LLVM arch) s (FloatType fi) -> LLVMExpr s arch
demoteToInt w v = BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w $ App $ FloatToSBV w RNE v)
llvmTypeAsRepr outty' $ \outty'' ->
case (asScalar x', outty'') of
(Scalar (FloatRepr _) x'', LLVMPointerRepr w) -> return $ demoteToInt w x''
_ -> fail (unlines [unwords ["Invalid fptosi:", show op, show x, show outty], showI])

@atomb
Copy link
Contributor

atomb commented Mar 26, 2021

This is related to #366.

@robdockins robdockins added the poison Issues touching on the LLVM concept of poison label Mar 26, 2021
@langston-barrett langston-barrett added the unsoundness Potential for incorrect proofs exists label May 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
llvm poison Issues touching on the LLVM concept of poison unsoundness Potential for incorrect proofs exists
Projects
None yet
Development

No branches or pull requests

3 participants