crucible-llvm-0.7: src/Lang/Crucible/LLVM/Translation/Instruction.hs
-----------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.LLVM.Translation.Instruction
-- Description : Translation of LLVM instructions
-- Copyright : (c) Galois, Inc 2018
-- License : BSD3
-- Maintainer : Rob Dockins <rdockins@galois.com>
-- Stability : provisional
--
-- This module represents the workhorse of the LLVM translation. It
-- is responsible for interpreting the LLVM instruction set into
-- corresponding crucible statements.
-----------------------------------------------------------------------
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.LLVM.Translation.Instruction
( instrResultType
, generateInstr
, definePhiBlock
, assignLLVMReg
, callOrdinaryFunction
) where
import Prelude hiding (exp, pred)
import Control.Lens hiding (op, (:>) )
import Control.Monad (MonadPlus(..), forM, unless)
import Control.Monad.Except (MonadError(..), runExceptT)
import Control.Monad.State.Strict (MonadState(..))
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.Maybe
import Data.Foldable (for_, toList)
import Data.Functor (void)
import Data.Int
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty((:|)))
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.String
import qualified Data.Text as Text
import qualified Data.Vector as V
import Numeric.Natural
import Prettyprinter (pretty)
import GHC.Exts ( Proxy#, proxy# )
import qualified Text.LLVM.AST as L
import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr as NatRepr
import Data.Parameterized.Some
import What4.Utils.StringLiteral
import Lang.Crucible.CFG.Expr
import Lang.Crucible.CFG.Generator
import qualified Lang.Crucible.LLVM.Bytes as G
import Lang.Crucible.LLVM.DataLayout
import qualified Lang.Crucible.LLVM.Errors.Poison as Poison
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
import Lang.Crucible.LLVM.Extension
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.MemType
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
import Lang.Crucible.LLVM.Translation.Constant
import Lang.Crucible.LLVM.Translation.Expr
import Lang.Crucible.LLVM.Translation.Monad
import Lang.Crucible.LLVM.Translation.Options
import Lang.Crucible.LLVM.Translation.Types
import Lang.Crucible.LLVM.TypeContext
import Lang.Crucible.Syntax hiding (IsExpr)
import Lang.Crucible.Types
--------------------------------------------------------------------------------
-- Assertions
-- | Add a bunch of side conditions to a value.
--
-- Allows for effectful computation of the predicates and expressions.
sideConditionsA :: forall f ty s. Applicative f
=> GlobalVar Mem
-> TypeRepr ty
-> Expr LLVM s ty
-- ^ Expression with side-condition
-> [( Bool
, f (Expr LLVM s BoolType)
, UB.UndefinedBehavior (Expr LLVM s)
)]
-- ^ Conditions to (conditionally) assert
-> f (Expr LLVM s ty)
sideConditionsA mvar tyRepr expr conds =
let middle :: Applicative g => (a, g b, c) -> g (a, b, c)
middle (a, fb, c) = (,,) <$> pure a <*> fb <*> pure c
fmapMaybe :: Functor g => g [a] -> (a -> Maybe b) -> g [b]
fmapMaybe gs h = fmap (mapMaybe h) gs
conds' :: f [LLVMSideCondition (Expr LLVM s)]
conds' = fmapMaybe (traverse middle conds) $ \(b, pred, classifier) ->
(if b then Just else const Nothing) $
LLVMSideCondition pred classifier
in flip fmap conds' $
\case
[] -> expr -- No assertions left, nothing to do.
(x:xs) -> App $ ExtensionApp $ LLVM_SideConditions mvar tyRepr (x :| xs) expr
-- | Assert that evaluation doesn't result in a poison value
poisonSideCondition :: GlobalVar Mem
-> TypeRepr ty
-> Poison.Poison (Expr LLVM s)
-> Expr LLVM s ty
-- ^ Expression with side-condition
-> Expr LLVM s BoolType
-- ^ Condition to assert
-> Expr LLVM s ty
poisonSideCondition mvar tyRepr poison expr cond =
runIdentity $ sideConditionsA mvar tyRepr expr [(True, pure cond, UB.PoisonValueCreated poison)]
--------------------------------------------------------------------------------
-- Translation
-- | Get the return type of an LLVM instruction
-- See <https://llvm.org/docs/LangRef.html#instruction-reference the language reference>.
instrResultType ::
(?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
L.Instr ->
m MemType
instrResultType instr =
case instr of
L.Arith _ x _ -> liftMemType (L.typedType x)
L.UnaryArith _ x -> liftMemType (L.typedType x)
L.Bit _ x _ -> liftMemType (L.typedType x)
L.Conv _ _ ty -> liftMemType ty
L.Call _ (L.FunTy ty _ _) _ _ -> liftMemType ty
L.Call _ ty _ _ -> throwError $ unwords ["unexpected non-function type in call:", show ty]
L.Invoke (L.FunTy ty _ _) _ _ _ _ -> liftMemType ty
L.Invoke ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in invoke:", show ty]
L.CallBr (L.FunTy ty _ _) _ _ _ _ -> liftMemType ty
L.CallBr ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in callbr:", show ty]
L.Alloca ty _ _ -> liftMemType (L.PtrTo ty)
L.Load tp _ _ _ -> liftMemType tp
L.ICmp _op tv _ -> do
inpType <- liftMemType (L.typedType tv)
case inpType of
VecType len _ -> return (VecType len (IntType 1))
_ -> return (IntType 1)
L.FCmp _op tv _ -> do
inpType <- liftMemType (L.typedType tv)
case inpType of
VecType len _ -> return (VecType len (IntType 1))
_ -> return (IntType 1)
L.Phi tp _ -> liftMemType tp
L.GEP inbounds baseTy basePtr elts ->
do gepRes <- runExceptT (translateGEP inbounds baseTy basePtr elts)
case gepRes of
Left err -> throwError err
Right (GEPResult lanes tp _gep) ->
let n = natValue lanes in
if n == 1 then
return (PtrType (MemType tp))
else
return (VecType n (PtrType (MemType tp)))
L.Select _ x _ -> liftMemType (L.typedType x)
L.ExtractValue x idxes -> liftMemType (L.typedType x) >>= go idxes
where go [] tp = return tp
go (i:is) (ArrayType n tp')
| i < fromIntegral n = go is tp'
| otherwise = throwError $ unwords ["invalid index into array type", showInstr instr]
go (i:is) (StructType si) =
case siFields si V.!? (fromIntegral i) of
Just fi -> go is (fiType fi)
Nothing -> throwError $ unwords ["invalid index into struct type", showInstr instr]
go _ _ = throwError $ unwords ["invalid type in extract value instruction", showInstr instr]
L.InsertValue x _ _ -> liftMemType (L.typedType x)
L.ExtractElt x _ ->
do tp <- liftMemType (L.typedType x)
case tp of
VecType _n tp' -> return tp'
_ -> throwError $ unwords ["extract element of non-vector type", showInstr instr]
L.InsertElt x _ _ -> liftMemType (L.typedType x)
L.ShuffleVector x _ i ->
do xtp <- liftMemType (L.typedType x)
itp <- liftMemType (L.typedType i)
case (xtp, itp) of
(VecType _n ty, VecType m _) -> return (VecType m ty)
_ -> throwError $ unwords ["invalid shufflevector:", showInstr instr]
L.LandingPad x _ _ _ -> liftMemType x
-- LLVM Language Reference: "The original value at the location is returned."
L.AtomicRW _ _ _ v _ _ -> liftMemType (L.typedType v)
L.CmpXchg _weak _volatile _ptr _old new _ _ _ ->
do let dl = llvmDataLayout ?lc
tp <- liftMemType (L.typedType new)
return (StructType (mkStructInfo dl False [tp, i1]))
L.Freeze x -> liftMemType (L.typedType x)
_ -> throwError $ unwords ["instrResultType, unsupported instruction:", showInstr instr]
-- | Given an LLVM expression of vector type, select out the ith element.
extractElt
:: forall s arch ret.
L.Instr
-> MemType -- ^ type contained in the vector
-> Integer -- ^ size of the vector
-> LLVMExpr s arch -- ^ vector expression
-> LLVMExpr s arch -- ^ index expression
-> LLVMGenerator s arch ret (LLVMExpr s arch)
extractElt _instr ty _n (UndefExpr _) _i =
return $ UndefExpr ty
extractElt _instr ty _n (ZeroExpr _) _i =
return $ ZeroExpr ty
extractElt _ ty _ _ (UndefExpr _) =
return $ UndefExpr ty
extractElt instr ty n v (ZeroExpr zty) =
let ?err = fail in
zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> extractElt instr ty n v (BaseExpr tyr ex)
extractElt instr _ n (VecExpr _ vs) i
| Scalar _archProxy (LLVMPointerRepr _) (BitvectorAsPointerExpr _ x) <- asScalar i
, App (BVLit _ x') <- x
= constantExtract (BV.asUnsigned x')
where
constantExtract :: Integer -> LLVMGenerator s arch ret (LLVMExpr s arch)
constantExtract idx =
if (fromInteger idx < Seq.length vs) && (fromInteger idx < n)
then return $ Seq.index vs (fromInteger idx)
else fail (unlines ["invalid extractelement instruction (index out of bounds)", showInstr instr])
extractElt instr ty n (VecExpr _ vs) i = do
let ?err = fail
llvmTypeAsRepr ty $ \tyr -> unpackVec (proxy# :: Proxy# arch) tyr (toList vs) $
\ex -> extractElt instr ty n (BaseExpr (VectorRepr tyr) ex) i
extractElt instr _ n (BaseExpr (VectorRepr tyr) v) i =
do mvar <- getMemVar
idx <- case asScalar i of
Scalar _archProxy (LLVMPointerRepr w) x ->
do bv <- pointerAsBitvectorExpr w x
-- The value is poisoned if the index is out of bounds.
let poison = Poison.ExtractElementIndex bv
return $ poisonSideCondition
mvar
NatRepr
poison
-- returned expression
(App (BvToNat w bv))
-- assertion condition
(App (BVUlt w bv (App (BVLit w (BV.mkBV w n)))))
_ ->
fail (unlines ["invalid extractelement instruction", showInstr instr])
return $ BaseExpr tyr (App (VectorGetEntry tyr v idx))
extractElt instr _ _ _ _ = fail (unlines ["invalid extractelement instruction", showInstr instr])
-- | Given an LLVM expression of vector type, insert a new element at location ith element.
insertElt :: forall s arch ret.
L.Instr -- ^ Actual instruction
-> MemType -- ^ type contained in the vector
-> Integer -- ^ size of the vector
-> LLVMExpr s arch -- ^ vector expression
-> LLVMExpr s arch -- ^ element to insert
-> LLVMExpr s arch -- ^ index expression
-> LLVMGenerator s arch ret (LLVMExpr s arch)
insertElt _ ty _ _ _ (UndefExpr _) = do
return $ UndefExpr ty
insertElt instr ty n v a (ZeroExpr zty) = do
let ?err = fail
zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> insertElt instr ty n v a (BaseExpr tyr ex)
insertElt instr ty n (UndefExpr _) a i = do
insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (UndefExpr ty))) a i
insertElt instr ty n (ZeroExpr _) a i = do
insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (ZeroExpr ty))) a i
insertElt instr _ n (VecExpr ty vs) a i
| Scalar _archProxy (LLVMPointerRepr _) (BitvectorAsPointerExpr _ x) <- asScalar i
, App (BVLit _ x') <- x
= constantInsert (BV.asUnsigned x')
where
constantInsert :: Integer -> LLVMGenerator s arch ret (LLVMExpr s arch)
constantInsert idx =
if (fromInteger idx < Seq.length vs) && (fromInteger idx < n)
then return $ VecExpr ty $ Seq.adjust (\_ -> a) (fromIntegral idx) vs
else fail (unlines ["invalid insertelement instruction (index out of bounds)", showInstr instr])
insertElt instr ty n (VecExpr _ vs) a i = do
let ?err = fail
llvmTypeAsRepr ty $ \tyr -> unpackVec (proxy# :: Proxy# arch) tyr (toList vs) $
\ex -> insertElt instr ty n (BaseExpr (VectorRepr tyr) ex) a i
insertElt instr _ n (BaseExpr (VectorRepr tyr) v) a i =
do mvar <- getMemVar
(idx :: Expr LLVM s NatType)
<- case asScalar i of
Scalar _archProxy (LLVMPointerRepr w) x ->
do bv <- pointerAsBitvectorExpr w x
-- The value is poisoned if the index is out of bounds.
let poison = Poison.InsertElementIndex bv
return $
poisonSideCondition
mvar
NatRepr
poison
-- returned expression
(App (BvToNat w bv))
-- assertion condition
(App (BVUlt w bv (App (BVLit w (BV.mkBV w n)))))
_ ->
fail (unlines ["invalid insertelement instruction", showInstr instr, show i])
let ?err = fail
unpackOne a $ \_archProxy tyra a' ->
case testEquality tyr tyra of
Just Refl ->
return $ BaseExpr (VectorRepr tyr) (App (VectorSetEntry tyr v idx a'))
Nothing -> fail (unlines ["type mismatch in insertelement instruction", showInstr instr])
insertElt instr _tp n v a i = fail (unlines ["invalid insertelement instruction", showInstr instr, show n, show v, show a, show i])
-- Given an LLVM expression of vector or structure type, select out the
-- element indicated by the sequence of given concrete indices.
extractValue
:: LLVMExpr s arch -- ^ aggregate expression
-> [Int32] -- ^ sequence of indices
-> LLVMGenerator s arch ret (LLVMExpr s arch)
extractValue v [] = return v
extractValue (UndefExpr (StructType si)) is =
extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, UndefExpr tp)) tps) is
where tps = map fiType $ toList $ siFields si
extractValue (UndefExpr (ArrayType n tp)) is =
extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) is
extractValue (ZeroExpr (StructType si)) is =
extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) is
where tps = map fiType $ toList $ siFields si
extractValue (ZeroExpr (ArrayType n tp)) is =
extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (ZeroExpr tp)) is
extractValue (StructExpr vs) (i:is)
| fromIntegral i < Seq.length vs = extractValue (snd $ Seq.index vs $ fromIntegral i) is
extractValue (VecExpr _ vs) (i:is)
| fromIntegral i < Seq.length vs = extractValue (Seq.index vs $ fromIntegral i) is
extractValue (BaseExpr (StructRepr ctx) x) (i:is)
| Just (Some idx) <- Ctx.intIndex (fromIntegral i) (Ctx.size ctx) = do
let tpr = ctx Ctx.! idx
extractValue (BaseExpr tpr (getStruct idx x)) is
extractValue (BaseExpr (VectorRepr elTp) x) (i:is)
| i >= 0 =
do let n = fromIntegral i :: Natural
extractValue (BaseExpr elTp (app (VectorGetEntry elTp x (litExpr n)))) is
extractValue _ _ = fail "invalid extractValue instruction"
-- Given an LLVM expression of vector or structure type, insert a new element in the posistion
-- given by the concrete indices.
insertValue
:: LLVMExpr s arch -- ^ aggregate expression
-> LLVMExpr s arch -- ^ element to insert
-> [Int32] -- ^ sequence of concrete indices
-> LLVMGenerator s arch ret (LLVMExpr s arch)
insertValue _ v [] = return v
insertValue (UndefExpr (StructType si)) v is =
insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, UndefExpr tp)) tps) v is
where tps = map fiType $ toList $ siFields si
insertValue (UndefExpr (ArrayType n tp)) v is =
insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) v is
insertValue (ZeroExpr (StructType si)) v is =
insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) v is
where tps = map fiType $ toList $ siFields si
insertValue (ZeroExpr (ArrayType n tp)) v is =
insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (ZeroExpr tp)) v is
insertValue (StructExpr vs) v (i:is)
| fromIntegral i < Seq.length vs = do
let (xtp, x) = Seq.index vs (fromIntegral i)
x' <- insertValue x v is
return (StructExpr (Seq.adjust (\_ -> (xtp,x')) (fromIntegral i) vs))
insertValue (VecExpr tp vs) v (i:is)
| fromIntegral i < Seq.length vs = do
let x = Seq.index vs (fromIntegral i)
x' <- insertValue x v is
return (VecExpr tp (Seq.adjust (\_ -> x') (fromIntegral i) vs))
insertValue (BaseExpr (StructRepr ctx) x) v (i:is)
| Just (Some idx) <- Ctx.intIndex (fromIntegral i) (Ctx.size ctx) = do
let tpr = ctx Ctx.! idx
x' <- insertValue (BaseExpr tpr (getStruct idx x)) v is
let ?err = fail
unpackOne x' $ \_px tpr' x'' ->
case testEquality tpr tpr' of
Just Refl -> return $ BaseExpr (StructRepr ctx) (setStruct ctx x idx x'')
Nothing -> fail "insertValue was expected to return base value of same type (struct case)"
insertValue (BaseExpr (VectorRepr elTp) x) v (i:is)
| i >= 0 =
do let n = fromIntegral i :: Natural
x' <- insertValue (BaseExpr elTp (app (VectorGetEntry elTp x (litExpr n)))) v is
let ?err = fail
unpackOne x' $ \_px tpr' x'' ->
case testEquality elTp tpr' of
Just Refl -> return $ BaseExpr (VectorRepr elTp) (app (VectorSetEntry elTp x (litExpr n) x''))
Nothing -> fail "insertValue was expected to return base value of same type (vector case)"
insertValue _ _ _ = fail "invalid insertValue instruction"
evalGEP :: forall s arch ret wptr.
wptr ~ ArchWidth arch =>
L.Instr ->
GEPResult (LLVMExpr s arch) ->
LLVMGenerator s arch ret (LLVMExpr s arch)
evalGEP instr (GEPResult _lanes finalMemType gep0) = finish =<< go gep0
where
finish xs =
case Seq.viewl xs of
x Seq.:< (Seq.null -> True) -> return (BaseExpr PtrRepr x)
_ -> return (VecExpr (PtrType (MemType finalMemType)) (fmap (BaseExpr PtrRepr) xs))
badGEP :: LLVMGenerator s arch ret a
badGEP = fail $ unlines ["Unexpected failure when evaluating GEP", showInstr instr]
asPtr :: LLVMExpr s arch -> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
asPtr x =
case asScalar x of
Scalar _archProxy PtrRepr p -> return p
_ -> badGEP
go :: GEP n (LLVMExpr s arch) -> LLVMGenerator s arch ret (Seq (Expr LLVM s (LLVMPointerType wptr)))
go (GEP_scalar_base x) =
do p <- asPtr x
return (Seq.singleton p)
go (GEP_vector_base n x) =
do xs <- maybe badGEP (traverse (\y -> asPtr y)) (asVector x)
unless (fromIntegral (Seq.length xs) == natValue n) badGEP
return xs
go (GEP_scatter n gep) =
do xs <- go gep
unless (Seq.length xs == 1) badGEP
return (Seq.cycleTaking (widthVal n) xs)
go (GEP_field fi gep) =
do xs <- go gep
traverse (\x -> calcGEP_struct fi x) xs
go (GEP_index_each mt' gep idx) =
do xs <- go gep
traverse (\x -> calcGEP_array mt' x idx) xs
go (GEP_index_vector mt' gep idx) =
do xs <- go gep
idxs <- maybe badGEP return (asVector idx)
unless (Seq.length idxs == Seq.length xs) badGEP
traverse (\(x,i) -> calcGEP_array mt' x i) (Seq.zip xs idxs)
calcGEP_array :: forall wptr s arch ret.
wptr ~ ArchWidth arch =>
MemType {- ^ Type of the array elements -} ->
Expr LLVM s (LLVMPointerType wptr) {- ^ Base pointer -} ->
LLVMExpr s arch {- ^ index value -} ->
LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
calcGEP_array _typ base (ZeroExpr _) = return base
-- If the array index is the concrete number 0, then return the base
-- pointer unchanged.
calcGEP_array typ base idx =
do -- sign-extend the index value if necessary to make it
-- the same width as a pointer
(idx' :: Expr LLVM s (BVType wptr))
<- case asScalar idx of
Scalar _archProxy (LLVMPointerRepr w) x
| Just Refl <- testEquality w PtrWidth ->
pointerAsBitvectorExpr PtrWidth x
| Just LeqProof <- testLeq (incNat w) PtrWidth ->
do x' <- pointerAsBitvectorExpr w x
return $ app (BVSext PtrWidth w x')
_ -> fail $ unwords ["Invalid index value in GEP", show idx]
-- Calculate the size of the element memtype and check that it fits
-- in the pointer width
let dl = llvmDataLayout ?lc
let isz = G.bytesToInteger $ memTypeSize dl typ
unless (isz <= maxSigned PtrWidth)
(fail $ unwords ["Type size too large for pointer width:", show typ])
-- Perform the multiply
mvar <- getMemVar
off0 <- AtomExpr <$> (mkAtom $ app $ BVMul PtrWidth (app $ BVLit PtrWidth (BV.mkBV PtrWidth isz)) idx')
let off =
if isz == 0
then off0
else
let
-- Compute safe upper and lower bounds for the index value to
-- prevent multiplication overflow. Note that `minidx <= idx <=
-- maxidx` iff `MININT <= (isz * idx) <= MAXINT` when `isz` and
-- `idx` are considered as infinite precision integers. This
-- property holds only if we use `quot` (which rounds toward 0)
-- for the divisions in the following definitions.
-- maximum and minimum indices to prevent multiplication overflow
maxidx = maxSigned PtrWidth `quot` (max isz 1)
minidx = minSigned PtrWidth `quot` (max isz 1)
poison = Poison.GEPOutOfBounds base idx'
cond =
(app $ BVSle PtrWidth (app $ BVLit PtrWidth (BV.mkBV PtrWidth minidx)) idx') .&&
(app $ BVSle PtrWidth idx' (app $ BVLit PtrWidth (BV.mkBV PtrWidth maxidx)))
in
-- Multiplication overflow will result in a pointer which is not "in
-- bounds" for the given allocation. We translate all GEP
-- instructions as if they had the `inbounds` flag set, so the
-- result would be a poison value.
poisonSideCondition mvar (BVRepr PtrWidth) poison off0 cond
-- Perform the pointer offset arithmetic
callPtrAddOffset base off
calcGEP_struct ::
wptr ~ ArchWidth arch =>
FieldInfo ->
Expr LLVM s (LLVMPointerType wptr) ->
LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
calcGEP_struct fi base =
do -- Get the field offset and check that it fits
-- in the pointer width
let ioff = G.bytesToInteger $ fiOffset fi
unless (ioff <= maxSigned PtrWidth)
(fail $ unwords ["Field offset too large for pointer width in structure:", show ioff])
let off = app $ BVLit PtrWidth $ BV.mkBV PtrWidth ioff
-- Perform the pointer arithmetic and continue
-- Skip pointer arithmetic when offset is 0
if ioff == 0 then return base else callPtrAddOffset base off
translateConversion :: (?transOpts :: TranslationOptions) =>
L.Instr ->
L.ConvOp ->
MemType {- Input type -} ->
LLVMExpr s arch {- Value to convert -} ->
MemType {- Output type -} ->
LLVMGenerator s arch ret (LLVMExpr s arch)
-- Bitcast is a bit of a special case, handle separately
translateConversion _instr L.BitCast inty x outty = bitCast inty x outty
-- Perform translations pointwise on vectors
translateConversion instr op (VecType n inty) (explodeVector n -> Just xs) (VecType m outty)
| n == m = VecExpr outty <$> traverse (\x -> translateConversion instr op inty x outty) xs
-- Otherwise, assume scalar values and do the basic conversions
translateConversion instr op _inty x outty =
let showI = showInstr instr in
case op of
L.IntToPtr -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) _, LLVMPointerRepr w')
| Just Refl <- testEquality w PtrWidth
, Just Refl <- testEquality w' PtrWidth -> return x
(Scalar _ t v, a) ->
fail (unlines ["integer-to-pointer conversion failed: "
, showI
, show v ++ " : " ++ show (pretty t) ++ " -to- " ++ show (pretty a)
])
(NotScalar, _) -> fail (unlines ["integer-to-pointer conversion failed: non scalar", showI])
L.PtrToInt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) _, LLVMPointerRepr w')
| Just Refl <- testEquality w PtrWidth
, Just Refl <- testEquality w' PtrWidth -> return x
_ -> fail (unlines ["pointer-to-integer conversion failed", showI])
L.Trunc -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
| Just LeqProof <- isPosNat w'
, Just LeqProof <- testLeq (incNat w') w ->
do x_bv <- pointerAsBitvectorExpr w x'
let bv' = App (BVTrunc w' w x_bv)
return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
_ -> fail (unlines [unwords ["invalid truncation:", show x, show outty], showI])
L.ZExt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
| Just LeqProof <- isPosNat w
, Just LeqProof <- testLeq (incNat w) w' ->
do x_bv <- pointerAsBitvectorExpr w x'
let bv' = App (BVZext w' w x_bv)
return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
_ -> fail (unlines [unwords ["invalid zero extension:", show x, show outty], showI])
L.SExt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
| Just LeqProof <- isPosNat w
, Just LeqProof <- testLeq (incNat w) w' -> do
do x_bv <- pointerAsBitvectorExpr w x'
let bv' = App (BVSext w' w x_bv)
return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
_ -> fail (unlines [unwords ["invalid sign extension", show x, show outty], showI])
#if __GLASGOW_HASKELL__ < 900
-- This is redundant, but GHC's pattern-match coverage checker is only
-- smart enough to realize this in 9.0 or later.
L.BitCast -> bitCast _inty x outty
#endif
L.UiToFp -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do
bv <- pointerAsBitvectorExpr w x'
return $ BaseExpr (FloatRepr fi) $ App $ FloatFromBV fi RNE bv
_ -> fail (unlines [unwords ["Invalid uitofp:", show op, show x, show outty], showI])
L.SiToFp -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do
bv <- pointerAsBitvectorExpr w x'
return $ BaseExpr (FloatRepr fi) $ App $ FloatFromSBV fi RNE bv
_ -> fail (unlines [unwords ["Invalid sitofp:", show op, show x, show outty], showI])
L.FpToUi -> do
let demoteToInt :: (1 <= w) => NatRepr w -> Expr LLVM 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 _archProxy (FloatRepr _) x', LLVMPointerRepr w) -> return $ demoteToInt w x'
_ -> fail (unlines [unwords ["Invalid fptoui:", show op, show x, show outty], showI])
L.FpToSi -> do
let demoteToInt :: (1 <= w) => NatRepr w -> Expr LLVM 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 _archProxy (FloatRepr _) x', LLVMPointerRepr w) -> return $ demoteToInt w x'
_ -> fail (unlines [unwords ["Invalid fptosi:", show op, show x, show outty], showI])
L.FpTrunc -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (FloatRepr _) x', FloatRepr fi) -> do
return $ BaseExpr (FloatRepr fi) $ App $ FloatCast fi RNE x'
_ -> fail (unlines [unwords ["Invalid fptrunc:", show op, show x, show outty], showI])
L.FpExt -> do
llvmTypeAsRepr outty $ \outty' ->
case (asScalar x, outty') of
(Scalar _archProxy (FloatRepr _) x', FloatRepr fi) -> do
return $ BaseExpr (FloatRepr fi) $ App $ FloatCast fi RNE x'
_ -> fail (unlines [unwords ["Invalid fpext:", show op, show x, show outty], showI])
--------------------------------------------------------------------------------
-- Bit Cast
bitCast :: (?lc::TypeContext,HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
MemType {- ^ starting type of the expression -} ->
LLVMExpr s arch {- ^ expression to cast -} ->
MemType {- ^ target type -} ->
LLVMGenerator s arch ret (LLVMExpr s arch)
bitCast _ (ZeroExpr _) tgtT = return (ZeroExpr tgtT)
bitCast _ (UndefExpr _) tgtT = return (UndefExpr tgtT)
-- pointer casts always succeed
bitCast (PtrType _) expr (PtrType _) = return expr
bitCast (PtrType _) expr PtrOpaqueType = return expr
bitCast PtrOpaqueType expr (PtrType _) = return expr
bitCast PtrOpaqueType expr PtrOpaqueType = return expr
-- casts between vectors of the same length can just be done pointwise
bitCast (VecType n srcT) (explodeVector n -> Just xs) (VecType n' tgtT)
| n == n' = VecExpr tgtT <$> traverse (\x -> bitCast srcT x tgtT) xs
-- otherwise, cast via an intermediate integer type of common width
bitCast srcT expr tgtT = mb =<< runMaybeT (
case (memTypeBitwidth srcT, memTypeBitwidth tgtT) of
(Just w1, Just w2) | w1 == w2 -> castToInt srcT expr >>= castFromInt tgtT w2
_ -> mzero)
where
mb = maybe (err [ "*** Invalid coercion of expression"
, indent (show expr)
, "of type"
, indent (show srcT)
, "to type"
, indent (show tgtT)
]) return
err msg = reportError $ fromString $ unlines ("[bitCast] Failed to perform cast:" : msg)
indent msg = " " ++ msg
castToInt :: (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch) =>
MemType {- ^ type of input expression -} ->
LLVMExpr s arch ->
MaybeT (LLVMGenerator' s arch ret) (LLVMExpr s arch)
castToInt (IntType w) (BaseExpr (LLVMPointerRepr wrepr) x)
| w == natValue wrepr
= lift (BaseExpr (BVRepr wrepr) <$> pointerAsBitvectorExpr wrepr x)
castToInt FloatType (BaseExpr (FloatRepr SingleFloatRepr) x)
= return (BaseExpr (BVRepr (knownNat @32)) (app (FloatToBinary SingleFloatRepr x)))
castToInt DoubleType (BaseExpr (FloatRepr DoubleFloatRepr) x)
= return (BaseExpr (BVRepr (knownNat @64)) (app (FloatToBinary DoubleFloatRepr x)))
castToInt X86_FP80Type (BaseExpr (FloatRepr X86_80FloatRepr) x)
= return (BaseExpr (BVRepr (knownNat @80)) (app (FloatToBinary X86_80FloatRepr x)))
castToInt (VecType n tp) (explodeVector n -> Just xs) =
do xs' <- traverse (castToInt tp) (toList xs)
MaybeT (return (vecJoin xs'))
castToInt _ _ = mzero
castFromInt :: (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch) =>
MemType {- ^ target type -} ->
Natural {- ^ bitvector width in bits -} ->
LLVMExpr s arch -> MaybeT (LLVMGenerator' s arch ret) (LLVMExpr s arch)
castFromInt (IntType w1) w2 (BaseExpr (BVRepr w) x)
| w1 == w2, w1 == natValue w
= return (BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w x))
castFromInt FloatType 32 (BaseExpr (BVRepr w) x)
| Just Refl <- testEquality w (knownNat @32)
= return (BaseExpr (FloatRepr SingleFloatRepr) (app (FloatFromBinary SingleFloatRepr x)))
castFromInt DoubleType 64 (BaseExpr (BVRepr w) x)
| Just Refl <- testEquality w (knownNat @64)
= return (BaseExpr (FloatRepr DoubleFloatRepr) (app (FloatFromBinary DoubleFloatRepr x)))
castFromInt X86_FP80Type 80 (BaseExpr (BVRepr w) x)
| Just Refl <- testEquality w (knownNat @80)
= return (BaseExpr (FloatRepr X86_80FloatRepr) (app (FloatFromBinary X86_80FloatRepr x)))
castFromInt (VecType n tp) w expr
| n > 0
, (w',0) <- w `divMod` n
, Some wrepr' <- mkNatRepr w'
, Just LeqProof <- isPosNat wrepr'
= do xs <- MaybeT (return (vecSplit wrepr' expr))
VecExpr tp . Seq.fromList <$> traverse (castFromInt tp w') xs
castFromInt _ _ _ = mzero
-- | Join the elements of a vector into a single bit-vector value.
-- The resulting bit-vector would be of length at least one.
vecJoin :: (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch) =>
[LLVMExpr s arch] {- ^ Join these vector elements -} ->
Maybe (LLVMExpr s arch)
vecJoin exprs =
do (a,ys) <- List.uncons exprs
Scalar _archProxy (BVRepr (n :: NatRepr n)) e1 <- return (asScalar a)
if null ys
then do LeqProof <- testLeq (knownNat @1) n
return (BaseExpr (BVRepr n) e1)
else do BaseExpr (BVRepr m) e2 <- vecJoin ys
let p1 = leqZero @n
p2 = leqProof (knownNat @1) m
(LeqProof,LeqProof) <- return (leqAdd2 p1 p2, leqAdd2 p2 p1)
let bits u v x y = bitVal (addNat u v) (BVConcat u v x y)
return $! case llvmDataLayout ?lc ^. intLayout of
LittleEndian -> bits m n e2 e1
BigEndian -> bits n m e1 e2
bitVal ::
(1 <= n) =>
NatRepr n ->
App LLVM (Expr LLVM s) (BVType n) ->
LLVMExpr s arch
bitVal n e = BaseExpr (BVRepr n) (App e)
-- | Split a single bit-vector value into a vector of value of the given width.
vecSplit :: forall s n w arch. (?lc::TypeContext,HasPtrWidth w, w ~ ArchWidth arch, 1 <= n) =>
NatRepr n {- ^ Length of a single element -} ->
LLVMExpr s arch {- ^ Bit-vector value -} ->
Maybe [ LLVMExpr s arch ]
vecSplit elLen expr =
do Scalar _archProxy (BVRepr totLen) e <- return (asScalar expr)
let getEl :: NatRepr offset -> Maybe [ LLVMExpr s arch ]
getEl offset = let end = addNat offset elLen
in case testLeq end totLen of
Just LeqProof ->
do rest <- getEl end
let x = bitVal elLen
(BVSelect offset elLen totLen e)
return (x : rest)
Nothing ->
do Refl <- testEquality offset totLen
return []
els <- getEl (knownNat @0)
-- in `els` the least significant chunk is first
return $! case lay ^. intLayout of
LittleEndian -> els
BigEndian -> reverse els
where
lay = llvmDataLayout ?lc
bitop :: (?transOpts :: TranslationOptions) =>
L.BitOp ->
MemType ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
bitop op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
VecExpr tp <$> sequence (Seq.zipWith (\x y -> bitop op tp x y) xs ys)
bitop op _ x y =
case (asScalar x, asScalar y) of
(Scalar _archProxy (LLVMPointerRepr w) x',
Scalar _archPrxy' (LLVMPointerRepr w') y')
| Just Refl <- testEquality w w'
, Just LeqProof <- isPosNat w -> do
xbv <- pointerAsBitvectorExpr w x'
ybv <- pointerAsBitvectorExpr w y'
ex <- raw_bitop op w xbv ybv
return (BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w ex))
_ -> fail $ unwords ["bitwise operation on unsupported values", show x, show y]
raw_bitop :: (?transOpts :: TranslationOptions, 1 <= w) =>
L.BitOp ->
NatRepr w ->
Expr LLVM s (BVType w) ->
Expr LLVM s (BVType w) ->
LLVMGenerator s arch ret (Expr LLVM s (BVType w))
raw_bitop op w a b =
do mvar <- getMemVar
let withSideConds val lst = sideConditionsA mvar (BVRepr w) val lst
let noLaxArith = not (laxArith ?transOpts)
case op of
L.And -> return $ App (BVAnd w a b)
L.Or -> return $ App (BVOr w a b)
L.Xor -> return $ App (BVXor w a b)
L.Shl nuw nsw -> do
let wlit = App (BVLit w (BV.width w))
result <- AtomExpr <$> mkAtom (App (BVShl w a b))
withSideConds result
[ ( noLaxArith
, pure $ App (BVUlt w b wlit) -- TODO: is this the right condition?
, UB.PoisonValueCreated $ Poison.ShlOp2Big a b
)
, ( nuw && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVLshr w result b)))
, UB.PoisonValueCreated $ Poison.ShlNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVAshr w result b)))
, UB.PoisonValueCreated $ Poison.ShlNoSignedWrap a b
)
]
L.Lshr exact -> do
let wlit = App (BVLit w (BV.width w))
result <- AtomExpr <$> mkAtom (App (BVLshr w a b))
withSideConds result
[ ( noLaxArith
, pure $ App (BVUlt w b wlit)
, UB.PoisonValueCreated $ Poison.LshrOp2Big a b
)
, ( exact && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVShl w result b)))
, UB.PoisonValueCreated $ Poison.LshrExact a b
)
]
L.Ashr exact
| Just LeqProof <- isPosNat w -> do
let wlit = App (BVLit w (BV.width w))
result <- AtomExpr <$> mkAtom (App (BVAshr w a b))
withSideConds result
[ ( noLaxArith
, pure $ App (BVUlt w b wlit)
, UB.PoisonValueCreated $ Poison.AshrOp2Big a b
)
, ( exact && noLaxArith
, fmap (App . BVEq w a)
(AtomExpr <$> mkAtom (App (BVShl w result b)))
, UB.PoisonValueCreated $ Poison.AshrExact a b
)
]
| otherwise -> fail "cannot arithmetic right shift a 0-width integer"
-- | Translate an LLVM integer operation into a Crucible CFG expression.
--
-- Poison values can arise from such operations.
intop :: forall w s arch ret. (?transOpts :: TranslationOptions, 1 <= w)
=> L.ArithOp
-> NatRepr w
-> Expr LLVM s (BVType w)
-> Expr LLVM s (BVType w)
-> LLVMGenerator s arch ret (Expr LLVM s (BVType w))
intop op w a b =
do mvar <- getMemVar
let withSideConds val lst = sideConditionsA mvar (BVRepr w) val lst
let withPoison val xs =
do v <- AtomExpr <$> mkAtom val
withSideConds v $ map (\(d, e, c) -> (d, pure e, UB.PoisonValueCreated c)) xs
let z = App (BVLit w (BV.zero w))
let bNeqZero = \ub -> (True, pure (notExpr (App (BVEq w z b))), ub)
let neg1 = App (BVLit w (BV.mkBV w (-1)))
let minInt = App (BVLit w (BV.minSigned w))
let noLaxArith = not (laxArith ?transOpts)
case op of
L.Add nuw nsw -> withPoison (App (BVAdd w a b))
[ ( nuw && noLaxArith
, notExpr (App (BVCarry w a b))
, Poison.AddNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, notExpr (App (BVSCarry w a b))
, Poison.AddNoSignedWrap a b
)
]
L.Sub nuw nsw -> withPoison (App (BVSub w a b))
[ ( nuw && noLaxArith
, notExpr (App (BVUlt w a b))
, Poison.SubNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, notExpr (App (BVSBorrow w a b))
, Poison.SubNoSignedWrap a b
)
]
L.Mul nuw nsw -> do
let w' = addNat w w
Just LeqProof <- return $ isPosNat w'
Just LeqProof <- return $ testLeq (incNat w) w'
prod <- AtomExpr <$> mkAtom (App (BVMul w a b))
withSideConds prod
[ ( nuw && noLaxArith
, do
az <- AtomExpr <$> mkAtom (App (BVZext w' w a))
bz <- AtomExpr <$> mkAtom (App (BVZext w' w b))
wideprod <- AtomExpr <$> mkAtom (App (BVMul w' az bz))
prodz <- AtomExpr <$> mkAtom (App (BVZext w' w prod))
return (App (BVEq w' wideprod prodz))
, UB.PoisonValueCreated $ Poison.MulNoUnsignedWrap a b
)
, ( nsw && noLaxArith
, do
as <- AtomExpr <$> mkAtom (App (BVSext w' w a))
bs <- AtomExpr <$> mkAtom (App (BVSext w' w b))
wideprod <- AtomExpr <$> mkAtom (App (BVMul w' as bs))
prods <- AtomExpr <$> mkAtom (App (BVSext w' w prod))
return (App (BVEq w' wideprod prods))
, UB.PoisonValueCreated $ Poison.MulNoSignedWrap a b
)
]
L.UDiv exact -> do
q <- AtomExpr <$> mkAtom (App (BVUdiv w a b))
withSideConds q
[ ( exact && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVMul w q b)))
, UB.PoisonValueCreated $ Poison.UDivExact a b
)
, bNeqZero (UB.UDivByZero a b)
]
L.SDiv exact
| Just LeqProof <- isPosNat w -> do
q <- AtomExpr <$> mkAtom (App (BVSdiv w a b))
withSideConds q
[ ( exact && noLaxArith
, fmap (App . BVEq w a . AtomExpr)
(mkAtom (App (BVMul w q b)))
, UB.PoisonValueCreated $ Poison.SDivExact a b
)
, ( noLaxArith
, pure (notExpr (App (BVEq w neg1 b) .&& App (BVEq w minInt a)))
, UB.SDivOverflow a b
)
, bNeqZero (UB.SDivByZero a b)
]
| otherwise -> fail "cannot take the signed quotient of a 0-width bitvector"
L.URem -> withSideConds (App (BVUrem w a b)) [ bNeqZero (UB.URemByZero a b) ]
L.SRem
| Just LeqProof <- isPosNat w ->
do r <- AtomExpr <$> mkAtom (App (BVSrem w a b))
withSideConds r
[ ( noLaxArith
, pure (notExpr (App (BVEq w neg1 b) .&& App (BVEq w minInt a)))
, UB.SRemOverflow a b
)
, bNeqZero (UB.SRemByZero a b)
]
| otherwise -> fail "cannot take the signed remainder of a 0-width bitvector"
_ -> fail $ unwords ["unsupported integer arith operation", show op]
caseptr
:: (1 <= w)
=> NatRepr w
-> TypeRepr a
-> (Expr LLVM s (BVType w) ->
LLVMGenerator s arch ret (Expr LLVM s a))
-> (Expr LLVM s NatType -> Expr LLVM s (BVType w) ->
LLVMGenerator s arch ret (Expr LLVM s a))
-> Expr LLVM s (LLVMPointerType w)
-> LLVMGenerator s arch ret (Expr LLVM s a)
caseptr w tpr bvCase ptrCase x =
case x of
PointerExpr _ blk off ->
case asApp blk of
Just (NatLit 0) -> bvCase off
Just (NatLit _) -> ptrCase blk off
_ -> ptrSwitch blk off
_ -> do a_x <- forceEvaluation x
blk <- forceEvaluation (App (ExtensionApp (LLVM_PointerBlock w a_x)))
off <- forceEvaluation (App (ExtensionApp (LLVM_PointerOffset w a_x)))
ptrSwitch blk off
where
ptrSwitch blk off =
do let cond = (blk .== litExpr 0)
c_label <- newLambdaLabel' tpr
bv_label <- defineBlockLabel (bvCase off >>= jumpToLambda c_label)
ptr_label <- defineBlockLabel (ptrCase blk off >>= jumpToLambda c_label)
continueLambda c_label (branch cond bv_label ptr_label)
atomicRWOp ::
forall s arch ret.
L.AtomicRWOp ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
atomicRWOp op x y =
case (asScalar x, asScalar y) of
(Scalar _archProxy (LLVMPointerRepr (w :: NatRepr w)) x', Scalar _archProxy' (LLVMPointerRepr w') y')
| Just Refl <- testEquality w w'
-> do xbv <- pointerAsBitvectorExpr w x'
ybv <- pointerAsBitvectorExpr w y'
newval <- bvOp w xbv ybv
return $ BaseExpr (LLVMPointerRepr w) $ BitvectorAsPointerExpr w newval
(Scalar _archProxy (FloatRepr fi) xf, Scalar _archPrxy' (FloatRepr fi') yf)
| Just Refl <- testEquality fi fi'
-> do newval <- floatingOp fi xf yf
return $ BaseExpr (FloatRepr fi) newval
_ -> fail $ unlines [ "atomicRW operation on incompatible values"
, "Operation: " ++ show op
, "Value 1: " ++ show x
, "Value 2: " ++ show y
]
where
-- Translate an atomic operation over bitvector values, respecting the
-- semantics described in this part of the LLVM Language Reference Manual:
-- https://releases.llvm.org/16.0.0/docs/LangRef.html#id229
--
-- Note that `xbv` corresponds to `*ptr` and `ybv` corresponds to `val` in
-- the Reference Manual.
bvOp ::
forall w.
(1 <= w) =>
NatRepr w ->
Expr LLVM s (BVType w) ->
Expr LLVM s (BVType w) ->
LLVMGenerator s arch ret (Expr LLVM s (BVType w))
bvOp w xbv ybv =
case op of
L.AtomicXchg -> pure ybv
L.AtomicAdd -> pure $ app $ BVAdd w xbv ybv
L.AtomicSub -> pure $ app $ BVSub w xbv ybv
L.AtomicAnd -> pure $ app $ BVAnd w xbv ybv
L.AtomicNand -> pure $ app $ BVNot w $ app $ BVAnd w xbv ybv
L.AtomicOr -> pure $ app $ BVOr w xbv ybv
L.AtomicXor -> pure $ app $ BVXor w xbv ybv
L.AtomicMax -> pure $ app $ BVSMax w xbv ybv
L.AtomicMin -> pure $ app $ BVSMin w xbv ybv
L.AtomicUMax -> pure $ app $ BVUMax w xbv ybv
L.AtomicUMin -> pure $ app $ BVUMin w xbv ybv
L.AtomicUIncWrap ->
-- This is the same thing as
--
-- (*ptr u>= val) ? 0 : (*ptr + 1)
--
-- from the LLVM semantics, but with a double-negated condition to
-- account for the Crucible CFG language not having a BVUge operation
-- (only BVUlt).
let c = app $ Not $ app $ BVUlt w xbv ybv -- ~(*ptr u< val)
t = zero
f = app $ BVAdd w xbv one in
pure $ app $ BVIte c w t f
L.AtomicUDecWrap ->
-- This is the same thing as
--
-- ((*ptr == 0) || (*ptr u> val)) ? val : (*ptr - 1)
--
-- from the LLVM semantics, but with a double-negated condition to
-- account for the Crucible CFG language not having a BVUgt operation
-- (only BVUle).
let c1 = app $ BVEq w xbv zero
c2 = app $ Not $ app $ BVUle w xbv ybv -- ~(*ptr u<= val)
c = app $ Or c1 c2
t = xbv
f = app $ BVSub w xbv one in
pure $ app $ BVIte c w t f
L.AtomicFAdd -> nonBvError
L.AtomicFSub -> nonBvError
L.AtomicFMax -> nonBvError
L.AtomicFMin -> nonBvError
where
zero, one :: Expr LLVM s (BVType w)
zero = app $ BVLit w $ BV.zero w
one = app $ BVLit w $ BV.one w
nonBvError :: forall a. LLVMGenerator s arch ret a
nonBvError =
reportError $ fromString $ unwords
[ "Invalid atomic bitvector operation"
, "Operation: " ++ show op
, "Value 1: " ++ show xbv
, "Value 2: " ++ show ybv
]
-- Translate an atomic operation over floating-point values, respecting the
-- semantics described in this part of the LLVM Language Reference Manual:
-- https://releases.llvm.org/16.0.0/docs/LangRef.html#id229
--
-- Note that `xf` corresponds to `*ptr` and `yf` corresponds to `val` in the
-- Reference Manual.
floatingOp ::
forall fi.
FloatInfoRepr fi ->
Expr LLVM s (FloatType fi) ->
Expr LLVM s (FloatType fi) ->
LLVMGenerator s arch ret (Expr LLVM s (FloatType fi))
floatingOp fi xf yf =
case op of
L.AtomicXchg -> pure yf
L.AtomicFAdd -> pure $ app $ FloatAdd fi RNE xf yf
L.AtomicFSub -> pure $ app $ FloatSub fi RNE xf yf
L.AtomicFMax -> pure $ app $ FloatMax fi xf yf
L.AtomicFMin -> pure $ app $ FloatMin fi xf yf
L.AtomicAdd -> nonFloatingError
L.AtomicSub -> nonFloatingError
L.AtomicAnd -> nonFloatingError
L.AtomicNand -> nonFloatingError
L.AtomicOr -> nonFloatingError
L.AtomicXor -> nonFloatingError
L.AtomicMax -> nonFloatingError
L.AtomicMin -> nonFloatingError
L.AtomicUMax -> nonFloatingError
L.AtomicUMin -> nonFloatingError
L.AtomicUIncWrap -> nonFloatingError
L.AtomicUDecWrap -> nonFloatingError
where
nonFloatingError :: forall a. LLVMGenerator s arch ret a
nonFloatingError =
reportError $ fromString $ unwords
[ "Invalid atomic floating-point operation"
, "Operation: " ++ show op
, "Value 1: " ++ show xf
, "Value 2: " ++ show yf
]
floatingCompare ::
L.FCmpOp ->
MemType ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
floatingCompare op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> floatingCompare op tp x y) xs ys)
floatingCompare op _ x y =
do b <- scalarFloatingCompare op x y
return (BaseExpr (LLVMPointerRepr (knownNat :: NatRepr 1))
(BitvectorAsPointerExpr knownNat (App (BoolToBV knownNat b))))
scalarFloatingCompare ::
L.FCmpOp ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (Expr LLVM s BoolType)
scalarFloatingCompare op x y =
case (asScalar x, asScalar y) of
(Scalar _archProxy (FloatRepr fi) x',
Scalar _archPrxy' (FloatRepr fi') y')
| Just Refl <- testEquality fi fi' ->
return (floatcmp op x' y')
_ -> fail $ unwords ["Floating point comparison on incompatible values", show x, show y]
floatcmp ::
L.FCmpOp ->
Expr LLVM s (FloatType fi) ->
Expr LLVM s (FloatType fi) ->
Expr LLVM s BoolType
floatcmp op a b =
let isNaNCond = App . FloatIsNaN
-- True if a is NAN or b is NAN
unoCond = App $ Or (isNaNCond a) (isNaNCond b)
mkUno c = App $ Or c unoCond
in case op of
L.Ftrue -> App $ BoolLit True
L.Ffalse -> App $ BoolLit False
L.Foeq -> App $ FloatFpEq a b
L.Folt -> App $ FloatLt a b
L.Fole -> App $ FloatLe a b
L.Fogt -> App $ FloatGt a b
L.Foge -> App $ FloatGe a b
L.Fone -> App $ FloatFpApart a b
L.Fueq -> mkUno $ App $ FloatFpEq a b
L.Fult -> mkUno $ App $ FloatLt a b
L.Fule -> mkUno $ App $ FloatLe a b
L.Fugt -> mkUno $ App $ FloatGt a b
L.Fuge -> mkUno $ App $ FloatGe a b
L.Fune -> mkUno $ App $ FloatFpApart a b
L.Ford -> App $ And (App $ Not $ isNaNCond a) (App $ Not $ isNaNCond b)
L.Funo -> unoCond
integerCompare ::
L.ICmpOp ->
MemType ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
integerCompare op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare op tp x y) xs ys)
integerCompare op _ x y = do
b <- scalarIntegerCompare op x y
return (BaseExpr (LLVMPointerRepr (knownNat :: NatRepr 1))
(BitvectorAsPointerExpr knownNat (App (BoolToBV knownNat b))))
scalarIntegerCompare ::
L.ICmpOp ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (Expr LLVM s BoolType)
scalarIntegerCompare op x y =
case (asScalar x, asScalar y) of
(Scalar _archProxy (LLVMPointerRepr w) x'', Scalar _archProxy' (LLVMPointerRepr w') y'')
| Just Refl <- testEquality w w'
, Just Refl <- testEquality w PtrWidth
-> pointerCmp op x'' y''
| Just Refl <- testEquality w w'
-> do xbv <- pointerAsBitvectorExpr w x''
ybv <- pointerAsBitvectorExpr w y''
return (intcmp w op xbv ybv)
_ -> fail $ unlines [ "arithmetic comparison on incompatible values"
, "Comparison: " ++ show op
, "Value 1: " ++ show x
, "Value 2: " ++ show y
]
intcmp :: (1 <= w)
=> NatRepr w
-> L.ICmpOp
-> Expr LLVM s (BVType w)
-> Expr LLVM s (BVType w)
-> Expr LLVM s BoolType
intcmp w op a b =
case op of
L.Ieq -> App (BVEq w a b)
L.Ine -> App (Not (App (BVEq w a b)))
L.Iult -> App (BVUlt w a b)
L.Iule -> App (BVUle w a b)
L.Iugt -> App (BVUlt w b a)
L.Iuge -> App (BVUle w b a)
L.Islt -> App (BVSlt w a b)
L.Isle -> App (BVSle w a b)
L.Isgt -> App (BVSlt w b a)
L.Isge -> App (BVSle w b a)
pointerCmp
:: (wptr ~ ArchWidth arch)
=> L.ICmpOp
-> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s BoolType)
pointerCmp op x y =
caseptr PtrWidth knownRepr
(\x_bv ->
caseptr PtrWidth knownRepr
(\y_bv -> return $ intcmp PtrWidth op x_bv y_bv)
(\_ _ -> ptr_bv_compare x_bv y)
y)
(\_ _ ->
caseptr PtrWidth knownRepr
(\y_bv -> ptr_bv_compare y_bv x)
(\_ _ -> ptrOp)
y)
x
where
-- Special case: a pointer can be compared for equality with an integer, as long as
-- that integer is 0, representing the null pointer.
ptr_bv_compare bv ptr = do
-- TODO: We can't use assertUndefinedSym here since the type variable 'sym'
-- isn't in scope. How should this be fixed?
assertExpr
(App (BVEq PtrWidth bv (App (BVLit PtrWidth (BV.zero PtrWidth)))))
(litExpr "Undefined comparison between pointer and integer")
case op of
L.Ieq -> callIsNull PtrWidth ptr
L.Ine -> App . Not <$> callIsNull PtrWidth ptr
_ -> reportError $ litExpr $ Text.pack $ unlines $
[ "Arithmetic comparison on incompatible values"
, "Comparison operation: " ++ show op
, "Value 1: " ++ show x
, "Value 2: " ++ show y
]
ptrOp =
do memVar <- getMemVar
case op of
L.Ieq -> do
isEq <- extensionStmt (LLVM_PtrEq memVar x y)
return $ isEq
L.Ine -> do
isEq <- extensionStmt (LLVM_PtrEq memVar x y)
return $ App (Not isEq)
L.Iule -> do
isLe <- extensionStmt (LLVM_PtrLe memVar x y)
return $ isLe
L.Iult -> do
isGe <- extensionStmt (LLVM_PtrLe memVar y x)
return $ App (Not isGe)
L.Iuge -> do
isGe <- extensionStmt (LLVM_PtrLe memVar y x)
return $ isGe
L.Iugt -> do
isLe <- extensionStmt (LLVM_PtrLe memVar x y)
return $ App (Not isLe)
_ -> reportError $ litExpr $ Text.pack $ unlines $
[ "Signed comparison on pointer values"
, "Comparison operation: " ++ show op
, "Value 1:" ++ show x
, "Value 2" ++ show y
]
pointerOp
:: (wptr ~ ArchWidth arch, ?transOpts :: TranslationOptions)
=> L.ArithOp
-> Expr LLVM s (LLVMPointerType wptr)
-> Expr LLVM s (LLVMPointerType wptr)
-> LLVMGenerator s arch ret (Expr LLVM s (LLVMPointerType wptr))
pointerOp op x y =
caseptr PtrWidth PtrRepr
(\x_bv ->
caseptr PtrWidth PtrRepr
(\y_bv -> BitvectorAsPointerExpr PtrWidth <$>
intop op PtrWidth x_bv y_bv)
(\_ _ -> bv_ptr_op x_bv)
y)
(\_ _ ->
caseptr PtrWidth PtrRepr
(\y_bv -> ptr_bv_op y_bv)
(\_ _ -> ptr_ptr_op)
y)
x
where
ptr_bv_op y_bv =
case op of
L.Add _ _ ->
callPtrAddOffset x y_bv
L.Sub _ _ ->
do let off = App (BVSub PtrWidth (App $ BVLit PtrWidth (BV.zero PtrWidth)) y_bv)
callPtrAddOffset x off
_ -> err
bv_ptr_op x_bv =
case op of
L.Add _ _ -> callPtrAddOffset y x_bv
_ -> err
ptr_ptr_op =
case op of
L.Sub _ _ -> BitvectorAsPointerExpr PtrWidth <$> callPtrSubtract x y
_ -> err
err = reportError $ litExpr $ Text.pack $ unlines $
[ "Invalid pointer operation"
, "Operation: " ++ show op
, "Value 1: " ++ show x
, "Value 2: " ++ show y
]
baseSelect ::
(?lc :: TypeContext, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
LLVMExpr s arch {- ^ Selection expression -} ->
LLVMExpr s arch {- ^ true expression -} ->
LLVMExpr s arch {- ^ false expression -} ->
LLVMGenerator s arch ret (Maybe (LLVMExpr s arch))
baseSelect (asScalar -> Scalar _archProxy (LLVMPointerRepr wc) c) (asScalar -> Scalar _ xtp x) (asScalar -> Scalar _ ytp y)
| Just Refl <- testEquality xtp ytp
, LLVMPointerRepr w <- xtp
= do c' <- callIntToBool wc c
z <- forceEvaluation (App (ExtensionApp (LLVM_PointerIte w c' x y)))
return (Just (BaseExpr (LLVMPointerRepr w) z))
baseSelect (asScalar -> Scalar _archProxy (LLVMPointerRepr wc) c) (asScalar -> Scalar _ xtp x) (asScalar -> Scalar _ ytp y)
| Just Refl <- testEquality xtp ytp
, AsBaseType btp <- asBaseType xtp
= do c' <- callIntToBool wc c
z <- forceEvaluation (app (BaseIte btp c' x y))
return (Just (BaseExpr xtp z))
baseSelect _ _ _ = return Nothing
translateSelect ::
(?lc :: TypeContext, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
L.Instr {- ^ The instruction to translate -} ->
(LLVMExpr s arch -> LLVMGenerator s arch ret ())
{- ^ A continuation to assign the produced value of this instruction to a register -} ->
MemType {- ^ Type of the selector variable -} ->
LLVMExpr s arch {- ^ Selection expression -} ->
MemType {- ^ Type of the select branches -} ->
LLVMExpr s arch {- ^ true expression -} ->
LLVMExpr s arch {- ^ false expression -} ->
LLVMGenerator s arch ret ()
translateSelect instr assign_f
(VecType n _) (explodeVector n -> Just cs)
(VecType m eltp) (explodeVector n -> Just xs) (explodeVector n -> Just ys)
| n == m
= do zs <- forM [0..n-1] $ \i ->
do Just c <- return $ Seq.lookup (fromIntegral i) cs
Just x <- return $ Seq.lookup (fromIntegral i) xs
Just y <- return $ Seq.lookup (fromIntegral i) ys
mz <- baseSelect c x y
maybe (fail $ unlines ["invalid select operation", showInstr instr]) return mz
assign_f (VecExpr eltp (Seq.fromList zs))
translateSelect instr assign_f
_ctp c
(VecType n eltp) (explodeVector n -> Just xs) (explodeVector n -> Just ys)
= do zs <- forM [0..n-1] $ \i ->
do Just x <- return $ Seq.lookup (fromIntegral i) xs
Just y <- return $ Seq.lookup (fromIntegral i) ys
mz <- baseSelect c x y
maybe (fail $ unlines ["invalid select operation", showInstr instr]) return mz
assign_f (VecExpr eltp (Seq.fromList zs))
translateSelect _ assign_f _ctp c@(asScalar -> Scalar _archProxy (LLVMPointerRepr wc) c') _tp x y
= do mz <- baseSelect c x y
case mz of
Just z -> assign_f z
Nothing ->
do c'' <- callIntToBool wc c'
ifte_ c'' (assign_f x) (assign_f y)
translateSelect instr _ _ _ _ _ _ =
fail $ unlines ["invalid select operation", showInstr instr]
-- | Do the heavy lifting of translating LLVM instructions to crucible code.
generateInstr :: forall s arch ret a.
(?transOpts :: TranslationOptions) =>
TypeRepr ret {- ^ Type of the function return value -} ->
L.BlockLabel {- ^ The label of the current LLVM basic block -} ->
Set L.Ident {- ^ Set of usable identifiers -} ->
L.Instr {- ^ The instruction to translate -} ->
(LLVMExpr s arch -> LLVMGenerator s arch ret ())
{- ^ A continuation to assign the produced value of this instruction to a register -} ->
LLVMGenerator s arch ret a
{- ^ A continuation for translating the remaining statements in this function.
Straightline instructions should enter this continuation,
but block-terminating instructions should not. -} ->
LLVMGenerator s arch ret a
generateInstr retType lab defSet instr assign_f k =
case instr of
-- skip phi instructions, they are handled in definePhiBlock
L.Phi _ _ -> k
L.Comment _ -> k
L.Unreachable -> reportError "LLVM unreachable code"
L.ExtractValue x is -> do
x' <- transTypedValue x
v <- extractValue x' is
assign_f v
k
L.InsertValue x v is -> do
x' <- transTypedValue x
v' <- transTypedValue v
y <- insertValue x' v' is
assign_f y
k
L.ExtractElt x i ->
case x of
L.Typed (L.Vector n ty) x' -> do
ty' <- liftMemType' ty
x'' <- transValue (VecType (fromIntegral n) ty') x'
i' <- transValue (IntType 64) i -- FIXME? this is a bit of a hack, since the llvm-pretty
-- AST doesn't track the size of the index value
y <- extractElt instr ty' (fromIntegral n) x'' i'
assign_f y
k
_ -> fail $ unwords ["expected vector type in extractelement instruction:", show x]
L.InsertElt x v i ->
case x of
L.Typed (L.Vector n ty) x' -> do
ty' <- liftMemType' ty
x'' <- transValue (VecType (fromIntegral n) ty') x'
v' <- transTypedValue v
i' <- transValue (IntType 64) i -- FIXME? this is a bit of a hack, since the llvm-pretty
-- AST doesn't track the size of the index value
y <- insertElt instr ty' (fromIntegral n) x'' v' i'
assign_f y
k
_ -> fail $ unwords ["expected vector type in insertelement instruction:", show x]
L.ShuffleVector sV1 sV2 sIxes ->
case (L.typedType sV1, L.typedType sIxes) of
(L.Vector m ty, L.Vector n (L.PrimType (L.Integer 32))) ->
do elTy <- liftMemType' ty
let inL :: Num b => b
inL = fromIntegral m
inV = VecType inL elTy
outL :: Num b => b
outL = fromIntegral n
xv1 <- transValue inV (L.typedValue sV1)
xv2 <- transValue inV sV2
xis <- transValue (VecType outL (IntType 32)) (L.typedValue sIxes)
case (explodeVector inL xv1, explodeVector inL xv2, explodeVector outL xis) of
(Just v1, Just v2, Just is) ->
do let getV x =
case x of
UndefExpr _ -> return $ UndefExpr elTy
ZeroExpr _ -> return $ Seq.index v1 0
BaseExpr (LLVMPointerRepr _) (BitvectorAsPointerExpr _ (App (BVLit _ i)))
| BV.asUnsigned i < inL -> return $ Seq.index v1 (fromIntegral (BV.asUnsigned i))
| inL <= BV.asUnsigned i && BV.asUnsigned i < 2*inL ->
return $ Seq.index v2 (fromIntegral (BV.asUnsigned i - inL))
_ -> fail $ unwords ["[shuffle] Expected literal index values but got", show x]
is' <- traverse getV is
assign_f (VecExpr elTy is')
k
_ -> fail $ unlines ["[shuffle] unexpected values:"
, showInstr instr
, show xv1, show xv2, show xis]
(t1,t2) -> fail $ unlines ["[shuffle] Type error", show t1, show t2 ]
L.Alloca tp num align -> do
tp' <- liftMemType' tp
let dl = llvmDataLayout ?lc
let tp_sz = memTypeSize dl tp'
let tp_sz' = app $ BVLit PtrWidth $ G.bytesToBV PtrWidth tp_sz
sz <- case num of
Nothing -> return $ tp_sz'
Just num' -> do
n <- transTypedValue num'
case n of
ZeroExpr _ -> return $ app $ BVLit PtrWidth (BV.zero PtrWidth)
BaseExpr (LLVMPointerRepr w) x
| Just Refl <- testEquality w PtrWidth ->
do x' <- pointerAsBitvectorExpr w x
return $ app $ BVMul PtrWidth x' tp_sz'
_ -> fail $ "Invalid alloca argument: " ++ show num
-- LLVM documentation regarding `alloca` alignment:
--
-- If a constant alignment is specified, the value result of the
-- allocation is guaranteed to be aligned to at least that
-- boundary. The alignment may not be greater than 1 << 29. If
-- not specified, or if zero, the target can choose to align the
-- allocation on any convenient boundary compatible with the
-- type.
alignment <-
case align of
Just a | a > 0 ->
case toAlignment (G.toBytes a) of
Nothing -> fail $ "Invalid alignment value in alloca: " ++ show a
Just al -> return al
_ -> return (memTypeAlign dl tp')
p <- callAlloca sz alignment
assign_f (BaseExpr (LLVMPointerRepr PtrWidth) p)
k
-- We don't care if it's atomic, since the symbolic simulator is
-- effectively single-threaded.
L.Load tp ptr _atomic align -> do
resTy <- liftMemType' tp
ptr' <- transTypedValue ptr
llvmTypeAsRepr resTy $ \expectTy -> do
let a0 = memTypeAlign (llvmDataLayout ?lc) resTy
let align' = fromMaybe a0 (toAlignment . G.toBytes =<< align)
res <- callLoad resTy expectTy ptr' align'
assign_f res
k
-- We don't care if it's atomic, since the symbolic simulator is
-- effectively single-threaded.
L.Store v ptr _atomic align -> do
vTp <- liftMemType' (L.typedType v)
ptr' <- transTypedValue ptr
let a0 = memTypeAlign (llvmDataLayout ?lc) vTp
let align' = fromMaybe a0 (toAlignment . G.toBytes =<< align)
v' <- transValue vTp (L.typedValue v)
callStore vTp ptr' v' align'
k
-- NB We treat every GEP as though it has the "inbounds" flag set;
-- thus, the calculation of out-of-bounds pointers results in
-- a runtime error.
L.GEP inbounds baseTy basePtr elts -> do
runExceptT (translateGEP inbounds baseTy basePtr elts) >>= \case
Left err -> reportError $ fromString $ unlines ["Error translating GEP", err]
Right gep ->
do gep' <- traverse (\v -> transTypedValue v) gep
v <- evalGEP instr gep'
assign_f v
k
L.Conv op x outty -> do
do tp <- liftMemType' (L.typedType x)
x' <- transValue tp (L.typedValue x)
outty' <- liftMemType' outty
v <- translateConversion instr op tp x' outty'
assign_f v
k
L.Call tailcall fnTy fn args ->
callFunction defSet instr tailcall fnTy fn args assign_f >> k
L.Invoke fnTy fn args normLabel _unwindLabel -> do
do callFunction defSet instr False fnTy fn args assign_f
definePhiBlock lab normLabel
L.CallBr fnTy fn args normLabel otherLabels -> do
do callFunction defSet instr False fnTy fn args assign_f
for_ otherLabels $ \lab' -> void (definePhiBlock lab lab')
definePhiBlock lab normLabel
L.Bit op x y ->
do tp <- liftMemType' (L.typedType x)
x' <- transValue tp (L.typedValue x)
y' <- transValue tp y
v <- bitop op tp x' y'
assign_f v
k
L.Arith op x y ->
do tp <- liftMemType' (L.typedType x)
x' <- transValue tp (L.typedValue x)
y' <- transValue tp y
v <- arithOp op tp x' y'
assign_f v
k
L.UnaryArith op x ->
do tp <- liftMemType' (L.typedType x)
x' <- transValue tp (L.typedValue x)
v <- unaryArithOp op tp x'
assign_f v
k
L.FCmp op x y -> do
tp <- liftMemType' (L.typedType x)
x' <- transValue tp (L.typedValue x)
y' <- transValue tp y
cmp <- floatingCompare op tp x' y'
assign_f cmp
k
L.ICmp op x y -> do
tp <- liftMemType' (L.typedType x)
x' <- transTypedValue x
y' <- transTypedValue (L.Typed (L.typedType x) y)
cmp <- integerCompare op tp x' y'
assign_f cmp
k
L.Select c x y -> do
ctp <- liftMemType' (L.typedType c)
c' <- transValue ctp (L.typedValue c)
tp <- liftMemType' (L.typedType x)
x' <- transValue tp (L.typedValue x)
y' <- transValue tp y
translateSelect instr assign_f ctp c' tp x' y'
k
L.Jump l' -> definePhiBlock lab l'
L.Br v l1 l2 -> do
v' <- transTypedValue v
e' <- case asScalar v' of
Scalar _archProxy (LLVMPointerRepr w) e -> callIntToBool w e
_ -> fail "expected boolean condition on branch"
phi1 <- defineBlockLabel (definePhiBlock lab l1)
phi2 <- defineBlockLabel (definePhiBlock lab l2)
branch e' phi1 phi2
L.Switch x def branches -> do
x' <- transTypedValue x
case asScalar x' of
Scalar _archProxy (LLVMPointerRepr w) x'' ->
do bv <- pointerAsBitvectorExpr w x''
buildSwitch w bv lab def branches
_ -> fail $ unwords ["expected integer value in switch", showInstr instr]
L.Ret v -> do v' <- transTypedValue v
let ?err = fail
unpackOne v' $ \_archProxy retType' ex ->
case testEquality retType retType' of
Just Refl -> do
callPopFrame
returnFromFunction ex
Nothing -> fail $ unwords ["unexpected return type", show retType, show retType']
L.RetVoid -> case testEquality retType UnitRepr of
Just Refl -> do
callPopFrame
returnFromFunction (App EmptyApp)
Nothing -> fail $ unwords ["tried to void return from non-void function", show retType]
-- NB, the symbolic simulator is essentially single-threaded, so fence
-- instructions are no-ops
L.Fence{} -> k
-- NB, the symbolic simulator is essentially single-threaded, so cmpxchg
-- always succeeds if the expected value is found in memory.
L.CmpXchg _weak _volatile ptr compareValue newValue _syncScope _syncOrderSuccess _syncOrderFail ->
do resTy <- liftMemType' (L.typedType compareValue)
ptr' <- transTypedValue ptr
llvmTypeAsRepr resTy $ \expectTy ->
do cmpVal <- transValue resTy (L.typedValue compareValue)
newVal <- transValue resTy (L.typedValue newValue)
let a0 = memTypeAlign (llvmDataLayout ?lc) resTy
oldVal <- callLoad resTy expectTy ptr' a0
cmp <- scalarIntegerCompare L.Ieq oldVal cmpVal
let flag = BaseExpr (LLVMPointerRepr (knownNat @1))
(BitvectorAsPointerExpr knownNat
(App (BoolToBV knownNat cmp)))
ifte_ cmp
-- success case, write the new value
(callStore resTy ptr' newVal a0)
-- failure case, do nothing
(return ())
assign_f (StructExpr (Seq.fromList [(resTy,oldVal),(IntType 1,flag)]))
k
-- NB, the symbolic simulator is essentially single-threaded, so no special
-- actions need to be taken to make operations atomic. We simply execute
-- their straightforward load/modify/store semantics.
L.AtomicRW _volatile op ptr val _syncScope _ordering ->
do valTy <- liftMemType' (L.typedType val)
ptr' <- transTypedValue ptr
case valTy of
IntType _ -> pure ()
FloatType -> pure ()
DoubleType -> pure ()
X86_FP80Type -> pure ()
_ -> fail $ unwords
["Invalid argument type on atomicrw, expected integer type", show ptr]
llvmTypeAsRepr valTy $ \expectTy ->
do val' <- transValue valTy $ L.typedValue val
let a0 = memTypeAlign (llvmDataLayout ?lc) valTy
oldVal <- callLoad valTy expectTy ptr' a0
newVal <- atomicRWOp op oldVal val'
callStore valTy ptr' newVal a0
assign_f oldVal
k
-- We translate `freeze` instructions by simply passing the argument value
-- through unchanged. This doesn't quite adhere to LLVM's own semantics for
-- this instruction (https://releases.llvm.org/12.0.0/docs/LangRef.html#id323),
-- which state that if the argument is `undef` or `poison`, then `freeze`
-- should return an arbitrary value. We don't currently have the ability to
-- reliably determine whether a given value is `undef` or `poison`, however
-- (see https://github.com/GaloisInc/crucible/issues/366), so for now we
-- settle for a less accurate translation of `freeze`.
L.Freeze x -> do
tp' <- liftMemType' (L.typedType x)
x' <- transValue tp' (L.typedValue x)
assign_f x'
k
-- unwind, landingpad and resume are all exception-related, which we don't currently
-- support
L.Unwind{} -> unsupported
L.LandingPad{} -> unsupported
L.Resume{} -> unsupported
-- indirect branch could be supported, but requires some nontrivial work to deal
-- properly with mapping basic-block labels to pointer values.
L.IndirectBr{} -> unsupported
-- VaArg is uncommonly used and hard to support
L.VaArg{} -> unsupported
where
liftMemType' = either typeErr return . liftMemType
typeErr msg =
malformedLLVMModule "Invalid type when translating instruction"
[ fromString (showInstr instr)
, fromString msg
]
unsupported = reportError $ App $ StringLit $ UnicodeLiteral $ Text.pack $
unwords ["unsupported instruction", showInstr instr]
arithOp :: (?transOpts :: TranslationOptions) =>
L.ArithOp ->
MemType ->
LLVMExpr s arch ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
arithOp op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
VecExpr tp <$> sequence (Seq.zipWith (\x y -> arithOp op tp x y) xs ys)
arithOp op _ x y =
case (asScalar x, asScalar y) of
(Scalar _ ty@(LLVMPointerRepr w) x',
Scalar _ (LLVMPointerRepr w') y')
| Just Refl <- testEquality w PtrWidth
, Just Refl <- testEquality w w' ->
do z <- pointerOp op x' y'
return (BaseExpr ty z)
| Just Refl <- testEquality w w' ->
do xbv <- pointerAsBitvectorExpr w x'
ybv <- pointerAsBitvectorExpr w y'
z <- intop op w xbv ybv
return (BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w z))
(Scalar _archProxy (FloatRepr fi) x',
Scalar _archPrxy' (FloatRepr fi') y')
| Just Refl <- testEquality fi fi' ->
do ex <- fop fi x' y'
return (BaseExpr (FloatRepr fi) ex)
_ -> reportError
$ fromString
$ unwords ["binary arithmetic operation on unsupported values",
show x, show y]
where
fop :: FloatInfoRepr fi ->
Expr LLVM s (FloatType fi) ->
Expr LLVM s (FloatType fi) ->
LLVMGenerator s arch ret (Expr LLVM s (FloatType fi))
fop fi a b =
case op of
L.FAdd ->
return $ App $ FloatAdd fi RNE a b
L.FSub ->
return $ App $ FloatSub fi RNE a b
L.FMul ->
return $ App $ FloatMul fi RNE a b
L.FDiv ->
return $ App $ FloatDiv fi RNE a b
L.FRem -> do
return $ App $ FloatRem fi a b
_ -> reportError
$ fromString
$ unwords [ "unsupported floating-point arith operation"
, show op, show x, show y
]
unaryArithOp :: (?transOpts :: TranslationOptions) =>
L.UnaryArithOp ->
MemType ->
LLVMExpr s arch ->
LLVMGenerator s arch ret (LLVMExpr s arch)
unaryArithOp op (VecType n tp) (explodeVector n -> Just xs) =
VecExpr tp <$> sequence (fmap (\x -> unaryArithOp op tp x) xs)
unaryArithOp op _ x =
case asScalar x of
Scalar _archProxy (FloatRepr fi) x' ->
do ex <- fop fi x'
return (BaseExpr (FloatRepr fi) ex)
_ -> reportError
$ fromString
$ unwords ["unary arithmetic operation on unsupported value",
show x]
where
fop :: FloatInfoRepr fi ->
Expr LLVM s (FloatType fi) ->
LLVMGenerator s arch ret (Expr LLVM s (FloatType fi))
fop fi a =
case op of
L.FNeg ->
return $ App $ FloatNeg fi a
-- | Generate a call to an LLVM function, without any special
-- handling for debug intrinsics or breakpoints.
callOrdinaryFunction ::
Maybe L.Instr {- ^ The instruction causing this call -} ->
Bool {- ^ Is the function a tail call? -} ->
L.Type {- ^ type of the function to call -} ->
L.Value {- ^ function value to call -} ->
[L.Typed L.Value] {- ^ argument list -} ->
(LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ assignment continuation for return value -} ->
LLVMGenerator s arch ret ()
callOrdinaryFunction instr _tailCall fnTy@(L.FunTy lretTy _largTys _varargs) fn args assign_f = do
let err :: String -> a
err = \msg -> malformedLLVMModule "Invalid type in function call" $
[ fromString msg ]
++
maybe [] ((:[]) . fromString . showInstr) instr
fnTy' <- either err return $ liftMemType (L.PtrTo fnTy)
retTy' <- either err return $ liftRetType lretTy
fn' <- transValue fnTy' fn
args' <- mapM (\v -> transTypedValue v) args
let ?err = err
unpackArgs args' $ \_archProxy argTypes args'' ->
llvmRetTypeAsRepr retTy' $ \retTy ->
case asScalar fn' of
Scalar _ PtrRepr ptr -> do
memVar <- getMemVar
v <- extensionStmt (LLVM_LoadHandle memVar (Just fnTy) ptr argTypes retTy)
ret <- call v args''
assign_f (BaseExpr retTy ret)
_ -> fail $ unwords ["unsupported function value", show fn]
callOrdinaryFunction instr _tailCall fnTy _fn _args _assign_f =
reportError $ App $ StringLit $ UnicodeLiteral $ Text.pack $ unlines $
[ "[callFunction] Unsupported function type: " ++ show fnTy ]
++
maybe [] ( (:[]) . show) instr
-- | Generate a call to an LLVM function, generating special support
-- for debugging intrinsics and breakpoint functions.
callFunction :: forall s arch ret.
(?transOpts :: TranslationOptions) =>
Set L.Ident {- ^ Set of usable identifiers -} ->
L.Instr {- ^ Source instruction of the call -} ->
Bool {- ^ Is the function a tail call? -} ->
L.Type {- ^ type of the function to call -} ->
L.Value {- ^ function value to call -} ->
[L.Typed L.Value] {- ^ argument list -} ->
(LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ assignment continuation for return value -} ->
LLVMGenerator s arch ret ()
callFunction defSet instr tailCall_ fnTy fn args assign_f
-- Supports LLVM 4-12
| L.ValSymbol "llvm.dbg.declare" <- fn
, debugIntrinsics ?transOpts =
do mbArgs <- dbgArgs defSet args
case mbArgs of
Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->
do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Declare ptr lv di))
return ()
Left msg -> addWarning (Text.pack msg)
_ -> addWarning "Unexpected argument in llvm.dbg.declare"
-- Supports LLVM 6-12
| L.ValSymbol "llvm.dbg.addr" <- fn
, debugIntrinsics ?transOpts =
do mbArgs <- dbgArgs defSet args
case mbArgs of
Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->
do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Addr ptr lv di))
return ()
Left msg -> addWarning (Text.pack msg)
_ -> addWarning "Unexpected argument in llvm.dbg.addr"
-- Supports LLVM 6-12 (earlier versions had an extra argument)
| L.ValSymbol "llvm.dbg.value" <- fn
, debugIntrinsics ?transOpts =
do mbArgs <- dbgArgs defSet args
case mbArgs of
Right (asScalar -> Scalar _ repr val, lv, di) ->
do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr val lv di))
return ()
Left msg -> addWarning (Text.pack msg)
_ -> addWarning "Unexpected argument in llvm.dbg.value"
-- Skip calls to other debugging intrinsics.
| L.ValSymbol nm <- fn
, nm `elem` [ "llvm.dbg.label"
, "llvm.dbg.declare"
, "llvm.dbg.addr"
, "llvm.dbg.value"
, "llvm.dbg.assign" -- Added in LLVM 16
, "llvm.experimental.noalias.scope.decl" -- Added in LLVM 12
, "llvm.lifetime.start"
, "llvm.lifetime.start.p0"
, "llvm.lifetime.start.p0i8"
, "llvm.lifetime.end"
, "llvm.lifetime.end.p0"
, "llvm.lifetime.end.p0i8"
, "llvm.invariant.start"
, "llvm.invariant.start.p0i8"
, "llvm.invariant.start.p0"
, "llvm.invariant.end"
, "llvm.invariant.end.p0i8"
, "llvm.invariant.end.p0"
] = return ()
| L.ValSymbol (L.Symbol nm) <- fn
, testBreakpointFunction nm = do
some_val_args <- mapM (\tv -> typedValueAsCrucibleValue tv) args
case Ctx.fromList some_val_args of
Some val_args -> do
addBreakpointStmt (Text.pack nm) val_args
| otherwise = callOrdinaryFunction (Just instr) tailCall_ fnTy fn args assign_f
-- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@.
dbgArgs ::
Set L.Ident {- ^ Set of usable identifiers -} ->
[L.Typed L.Value] {- ^ debug call arguments -} ->
LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression))
dbgArgs defSet args =
case args of
[valArg, lvArg, diArg] ->
case valArg of
L.Typed _ (L.ValMd (L.ValMdValue val)) ->
case lvArg of
L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) ->
case diArg of
L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) ->
let unusableIdents = Set.difference (useTypedVal val) defSet
in if Set.null unusableIdents then
do v <- transTypedValue val
pure (Right (v, lv, di))
else
do let msg = unwords (["dbg intrinsic def/use violation for:"] ++
map (show . LPP.ppIdent) (Set.toList unusableIdents))
pure (Left msg)
_ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg))
_ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg))
_ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg))
_ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args)))
typedValueAsCrucibleValue ::
L.Typed L.Value ->
LLVMGenerator s arch ret (Some (Value s))
typedValueAsCrucibleValue tv = case L.typedValue tv of
L.ValIdent i -> do
m <- use identMap
case Map.lookup i m of
Just (Left (Some r)) ->return $ Some $ RegValue r
Just (Right (Some a)) -> return $ Some $ AtomValue a
Nothing -> reportError $ fromString $
"Could not find identifier " ++ show i ++ "."
v -> reportError $ fromString $
"Unsupported breakpoint parameter: " ++ show v ++ "."
-- | Build a switch statement by decomposing it into a linear sequence of branches.
-- FIXME? this could be more efficient if we sort the list and do binary search instead...
buildSwitch :: (1 <= w)
=> NatRepr w
-> Expr LLVM s (BVType w) -- ^ The expression to switch on
-> L.BlockLabel -- ^ The label of the current basic block
-> L.BlockLabel -- ^ The label of the default basic block if no other branch applies
-> [(Integer, L.BlockLabel)] -- ^ The switch labels
-> LLVMGenerator s arch ret a
buildSwitch _ _ curr_lab def [] =
definePhiBlock curr_lab def
buildSwitch w ex curr_lab def ((i,l):bs) = do
let test = App $ BVEq w ex $ App $ BVLit w (BV.mkBV w i)
t_id <- newLabel
f_id <- newLabel
defineBlock t_id (definePhiBlock curr_lab l)
defineBlock f_id (buildSwitch w ex curr_lab def bs)
branch test t_id f_id
-- | Implement the phi-functions along the edge from one LLVM Basic block to another.
definePhiBlock :: L.BlockLabel -- ^ The LLVM source basic block
-> L.BlockLabel -- ^ The LLVM target basic block
-> LLVMGenerator s arch ret a
definePhiBlock l l' = do
bim <- use blockInfoMap
case Map.lookup l' bim of
Nothing -> fail $ unwords ["label not found in label map:", show l']
Just bi' -> do
-- Collect all the relevant phi functions to evaluate
let phi_funcs = maybe [] toList $ Map.lookup l (block_phi_map bi')
-- NOTE: We evaluate all the right-hand sides of the phi nodes BEFORE
-- we assign the values to their associated registers. This preserves
-- the expected semantics that phi functions are evaluated in the context
-- of the previous basic block, and prevents unintended register shadowing.
-- Otherwise loop-carried dependencies will sometimes end up with the wrong
-- values.
phiVals <- mapM evalPhi phi_funcs
mapM_ assignPhi phiVals
-- Now jump to the target code block
jump (block_label bi')
where evalPhi (ident,tp,v) = do
t_v <- transTypedValue (L.Typed tp v)
return (ident,t_v)
assignPhi (ident,t_v) = do
assignLLVMReg ident t_v
-- | Assign a packed LLVM expression into the named LLVM register.
assignLLVMReg
:: L.Ident
-> LLVMExpr s arch
-> LLVMGenerator s arch ret ()
assignLLVMReg ident rhs = do
st <- get
let idMap = st^.identMap
case Map.lookup ident idMap of
Just (Left lhs) -> do
doAssign lhs rhs
Just (Right _) -> fail $ "internal: Value cannot be assigned to."
Nothing -> fail $ unwords ["register not found in register map:", show ident]
-- | Given a register and an expression shape, assign the expressions in the right-hand-side
-- into the register left-hand side.
doAssign :: forall s arch ret.
Some (Reg s)
-> LLVMExpr s arch -- ^ the RHS values to assign
-> LLVMGenerator s arch ret ()
doAssign (Some r) (BaseExpr tpr ex) =
case testEquality (typeOfReg r) tpr of
Just Refl -> assignReg r ex
Nothing -> reportError $ fromString $ unwords ["type mismatch when assigning register", show r, show (typeOfReg r) , show tpr]
doAssign (Some r) (StructExpr vs) = do
let ?err = fail
unpackArgs (map snd $ toList vs) $ \_archProxy ctx asgn ->
case testEquality (typeOfReg r) (StructRepr ctx) of
Just Refl -> assignReg r (mkStruct ctx asgn)
Nothing -> reportError $ fromString $ unwords ["type mismatch when assigning structure to register", show r, show (StructRepr ctx)]
doAssign (Some r) (ZeroExpr tp) = do
let ?err = fail
zeroExpand (proxy# :: Proxy# arch) tp $ \_archProxy (tpr :: TypeRepr t) (ex :: Expr LLVM s t) ->
case testEquality (typeOfReg r) tpr of
Just Refl -> assignReg r ex
Nothing -> reportError $ fromString $ "type mismatch when assigning zero value"
doAssign (Some r) (UndefExpr tp) = do
let ?err = fail
undefExpand (proxy# :: Proxy# arch) tp $ \_archProxy (tpr :: TypeRepr t) (ex :: Expr LLVM s t) ->
case testEquality (typeOfReg r) tpr of
Just Refl -> assignReg r ex
Nothing -> reportError $ fromString $ "type mismatch when assigning undef value"
doAssign (Some r) (VecExpr tp vs) = do
let ?err = fail
llvmTypeAsRepr tp $ \tpr ->
unpackVec (proxy# :: Proxy# arch) tpr (toList vs) $ \ex ->
case testEquality (typeOfReg r) (VectorRepr tpr) of
Just Refl -> assignReg r ex
Nothing -> reportError $ fromString $ "type mismatch when assigning vector value"