|
| 1 | +{-# LANGUAGE GADTs #-} |
| 2 | +{-# LANGUAGE ScopedTypeVariables #-} |
| 3 | +{-# LANGUAGE TypeApplications #-} |
| 4 | +{-# LANGUAGE OverloadedStrings #-} |
| 5 | +{-# LANGUAGE TypeOperators #-} |
| 6 | +{-# LANGUAGE DataKinds #-} |
| 7 | +{-# LANGUAGE ViewPatterns #-} |
| 8 | + |
| 9 | +module Verifier.SAW.Heapster.LLVMGlobalConst ( |
| 10 | + permEnvAddGlobalConst |
| 11 | + ) where |
| 12 | + |
| 13 | +import Data.Bits |
| 14 | +import Data.List |
| 15 | +import Control.Monad.Reader |
| 16 | +import GHC.TypeLits |
| 17 | +import qualified Text.PrettyPrint.HughesPJ as PPHPJ |
| 18 | + |
| 19 | +import qualified Text.LLVM.AST as L |
| 20 | +import qualified Text.LLVM.PP as L |
| 21 | + |
| 22 | +import Data.Binding.Hobbits hiding (sym) |
| 23 | + |
| 24 | +import Data.Parameterized.NatRepr |
| 25 | +import Data.Parameterized.Some |
| 26 | + |
| 27 | +import Lang.Crucible.Types |
| 28 | +import Lang.Crucible.LLVM.MemModel |
| 29 | +import Verifier.SAW.OpenTerm |
| 30 | +import Verifier.SAW.Heapster.Permissions |
| 31 | + |
| 32 | +-- | Generate a SAW core term for a bitvector literal whose length is given by |
| 33 | +-- the first integer and whose value is given by the second |
| 34 | +bvLitOfIntOpenTerm :: Integer -> Integer -> OpenTerm |
| 35 | +bvLitOfIntOpenTerm n i = |
| 36 | + bvLitOpenTerm (map (testBit i) $ reverse [0..(fromIntegral n)-1]) |
| 37 | + |
| 38 | +-- | Helper function to build a SAW core term of type @BVVec w len a@, i.e., a |
| 39 | +-- bitvector-indexed vector, containing a given list of elements of type |
| 40 | +-- @a@. The roundabout way we do this currently requires a default element of |
| 41 | +-- type @a@, even though this value is never actually used. Also required is the |
| 42 | +-- bitvector width @w@. |
| 43 | +bvVecValueOpenTerm :: NatRepr w -> OpenTerm -> [OpenTerm] -> OpenTerm -> |
| 44 | + OpenTerm |
| 45 | +bvVecValueOpenTerm w tp ts def_tm = |
| 46 | + applyOpenTermMulti (globalOpenTerm "Prelude.genBVVecFromVec") |
| 47 | + [natOpenTerm (fromIntegral $ length ts), tp, arrayValueOpenTerm tp ts, |
| 48 | + def_tm, natOpenTerm (natValue w), |
| 49 | + bvLitOfIntOpenTerm (intValue w) (fromIntegral $ length ts)] |
| 50 | + |
| 51 | +-- | The monad for translating LLVM globals to Heapster |
| 52 | +type LLVMTransM = ReaderT (PermEnv, DebugLevel) Maybe |
| 53 | + |
| 54 | +-- | Run the 'LLVMTransM' monad |
| 55 | +runLLVMTransM :: LLVMTransM a -> (PermEnv, DebugLevel) -> Maybe a |
| 56 | +runLLVMTransM = runReaderT |
| 57 | + |
| 58 | +-- | Use 'debugTrace' to output a string message and then call 'mzero' |
| 59 | +traceAndZeroM :: String -> LLVMTransM a |
| 60 | +traceAndZeroM msg = |
| 61 | + do (_,dlevel) <- ask |
| 62 | + debugTrace dlevel msg mzero |
| 63 | + |
| 64 | +-- | Helper function to pretty-print the value of a global |
| 65 | +ppLLVMValue :: L.Value -> String |
| 66 | +ppLLVMValue val = |
| 67 | + L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppValue val) |
| 68 | + |
| 69 | +-- | Helper function to pretty-print an LLVM constant expression |
| 70 | +ppLLVMConstExpr :: L.ConstExpr -> String |
| 71 | +ppLLVMConstExpr ce = |
| 72 | + L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppConstExpr ce) |
| 73 | + |
| 74 | +-- | Translate a typed LLVM 'L.Value' to a Heapster permission + translation |
| 75 | +translateLLVMValue :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> L.Value -> |
| 76 | + LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) |
| 77 | +translateLLVMValue w tp@(L.PrimType (L.Integer n)) (L.ValInteger i) = |
| 78 | + translateLLVMType w tp >>= \(sh,_) -> |
| 79 | + return (sh, bvLitOfIntOpenTerm (fromIntegral n) i) |
| 80 | +translateLLVMValue w _ (L.ValSymbol sym) = |
| 81 | + do (env,_) <- ask |
| 82 | + -- (p, ts) <- lift (lookupGlobalSymbol env (GlobalSymbol sym) w) |
| 83 | + (p, t) <- case (lookupGlobalSymbol env (GlobalSymbol sym) w) of |
| 84 | + Just (p,[t]) -> return (p,t) |
| 85 | + Just (p,ts) -> return (p,tupleOpenTerm ts) |
| 86 | + Nothing -> traceAndZeroM ("Could not find symbol: " ++ show sym) |
| 87 | + return (PExpr_FieldShape (LLVMFieldShape p), t) |
| 88 | +translateLLVMValue w _ (L.ValArray tp elems) = |
| 89 | + do |
| 90 | + -- First, translate the elements |
| 91 | + ts <- map snd <$> mapM (translateLLVMValue w tp) elems |
| 92 | + |
| 93 | + -- Array shapes can only handle field shapes elements, so translate the |
| 94 | + -- element type to and ensure it returns a field shape; FIXME: this could |
| 95 | + -- actually handle sequences of field shapes if necessary |
| 96 | + (sh, saw_tp) <- translateLLVMType w tp |
| 97 | + fsh <- case sh of |
| 98 | + PExpr_FieldShape fsh -> return fsh |
| 99 | + _ -> mzero |
| 100 | + |
| 101 | + -- Compute the array stride as the length of the element shape |
| 102 | + sh_len_expr <- lift $ llvmShapeLength sh |
| 103 | + sh_len <- fromInteger <$> lift (bvMatchConstInt sh_len_expr) |
| 104 | + |
| 105 | + -- Generate a default element of type tp using the zero initializer; this is |
| 106 | + -- currently needed by bvVecValueOpenTerm |
| 107 | + def_v <- llvmZeroInitValue tp |
| 108 | + (_,def_tm) <- translateLLVMValue w tp def_v |
| 109 | + |
| 110 | + -- Finally, build our array shape and SAW core value |
| 111 | + return (PExpr_ArrayShape (bvInt $ fromIntegral $ length elems) sh_len [fsh], |
| 112 | + bvVecValueOpenTerm w saw_tp ts def_tm) |
| 113 | +translateLLVMValue w _ (L.ValPackedStruct elems) = |
| 114 | + mapM (translateLLVMTypedValue w) elems >>= \(unzip -> (shs,ts)) -> |
| 115 | + return (foldr PExpr_SeqShape PExpr_EmptyShape shs, tupleOpenTerm ts) |
| 116 | +translateLLVMValue w tp (L.ValString bytes) = |
| 117 | + translateLLVMValue w tp (L.ValArray |
| 118 | + (L.PrimType (L.Integer 8)) |
| 119 | + (map (L.ValInteger . toInteger) bytes)) |
| 120 | + {- |
| 121 | + return (PExpr_ArrayShape (bvInt $ fromIntegral $ length bytes) 1 |
| 122 | + [LLVMFieldShape (ValPerm_Exists $ nu $ \(bv :: Name (BVType 8)) -> |
| 123 | + ValPerm_Eq $ PExpr_LLVMWord $ PExpr_Var bv)], |
| 124 | + [arrayValueOpenTerm (bvTypeOpenTerm (8::Int)) $ |
| 125 | + map (\b -> bvLitOpenTerm $ map (testBit b) [7,6..0]) bytes]) |
| 126 | +-} |
| 127 | +translateLLVMValue w _ (L.ValConstExpr ce) = |
| 128 | + translateLLVMConstExpr w ce |
| 129 | +translateLLVMValue w tp L.ValZeroInit = |
| 130 | + llvmZeroInitValue tp >>= translateLLVMValue w tp |
| 131 | +translateLLVMValue _ _ v = |
| 132 | + traceAndZeroM ("translateLLVMValue does not yet handle:\n" ++ ppLLVMValue v) |
| 133 | + |
| 134 | +-- | Helper function for 'translateLLVMValue' |
| 135 | +translateLLVMTypedValue :: (1 <= w, KnownNat w) => NatRepr w -> L.Typed L.Value -> |
| 136 | + LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) |
| 137 | +translateLLVMTypedValue w (L.Typed tp v) = translateLLVMValue w tp v |
| 138 | + |
| 139 | +-- | Translate an LLVM type into a shape plus the SAW core type of elements of |
| 140 | +-- the translation of that shape |
| 141 | +translateLLVMType :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> |
| 142 | + LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) |
| 143 | +translateLLVMType _ (L.PrimType (L.Integer n)) |
| 144 | + | Just (Some (n_repr :: NatRepr n)) <- someNat n |
| 145 | + , Left leq_pf <- decideLeq (knownNat @1) n_repr = |
| 146 | + withKnownNat n_repr $ withLeqProof leq_pf $ |
| 147 | + return (PExpr_FieldShape (LLVMFieldShape $ ValPerm_Exists $ nu $ \bv -> |
| 148 | + ValPerm_Eq $ PExpr_LLVMWord $ |
| 149 | + PExpr_Var (bv :: Name (BVType n))), |
| 150 | + (bvTypeOpenTerm n)) |
| 151 | +translateLLVMType _ tp = |
| 152 | + traceAndZeroM ("translateLLVMType does not yet handle:\n" |
| 153 | + ++ show (L.ppType tp)) |
| 154 | + |
| 155 | +-- | Helper function for 'translateLLVMValue' applied to a constant expression |
| 156 | +translateLLVMConstExpr :: (1 <= w, KnownNat w) => NatRepr w -> L.ConstExpr -> |
| 157 | + LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) |
| 158 | +translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr : ixs)) = |
| 159 | + translateLLVMValue w tp ptr >>= \ptr_trans -> |
| 160 | + translateLLVMGEP w tp ptr_trans ixs |
| 161 | +translateLLVMConstExpr w (L.ConstConv L.BitCast |
| 162 | + (L.Typed tp@(L.PtrTo _) v) (L.PtrTo _)) = |
| 163 | + -- A bitcast from one LLVM pointer type to another is a no-op for us |
| 164 | + translateLLVMValue w tp v |
| 165 | +translateLLVMConstExpr _ ce = |
| 166 | + traceAndZeroM ("translateLLVMConstExpr does not yet handle:\n" |
| 167 | + ++ ppLLVMConstExpr ce) |
| 168 | + |
| 169 | +-- | Helper function for 'translateLLVMValue' applied to a @getelemptr@ |
| 170 | +-- expression |
| 171 | +translateLLVMGEP :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> |
| 172 | + (PermExpr (LLVMShapeType w), OpenTerm) -> |
| 173 | + [L.Typed L.Value] -> |
| 174 | + LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) |
| 175 | +translateLLVMGEP _ _ vtrans [] = return vtrans |
| 176 | +translateLLVMGEP w (L.Array _ tp) vtrans (L.Typed _ (L.ValInteger 0) : ixs) = |
| 177 | + translateLLVMGEP w tp vtrans ixs |
| 178 | +translateLLVMGEP w (L.PtrTo tp) vtrans (L.Typed _ (L.ValInteger 0) : ixs) = |
| 179 | + translateLLVMGEP w tp vtrans ixs |
| 180 | +translateLLVMGEP w (L.PackedStruct [tp]) vtrans (L.Typed |
| 181 | + _ (L.ValInteger 0) : ixs) = |
| 182 | + translateLLVMGEP w tp vtrans ixs |
| 183 | +translateLLVMGEP _ tp _ ixs = |
| 184 | + traceAndZeroM ("translateLLVMGEP cannot handle arguments:\n" ++ |
| 185 | + " " ++ intercalate "," (show tp : map show ixs)) |
| 186 | + |
| 187 | +-- | Build an LLVM value for a @zeroinitializer@ field of the supplied type |
| 188 | +llvmZeroInitValue :: L.Type -> LLVMTransM (L.Value) |
| 189 | +llvmZeroInitValue (L.PrimType (L.Integer _)) = return $ L.ValInteger 0 |
| 190 | +llvmZeroInitValue (L.Array len tp) = |
| 191 | + L.ValArray tp <$> replicate (fromIntegral len) <$> llvmZeroInitValue tp |
| 192 | +llvmZeroInitValue (L.PackedStruct tps) = |
| 193 | + L.ValPackedStruct <$> zipWith L.Typed tps <$> mapM llvmZeroInitValue tps |
| 194 | +llvmZeroInitValue tp = |
| 195 | + traceAndZeroM ("llvmZeroInitValue cannot handle type:\n" |
| 196 | + ++ show (L.ppType tp)) |
| 197 | + |
| 198 | +-- | Add an LLVM global constant to a 'PermEnv', if the global has a type and |
| 199 | +-- value we can translate to Heapster, otherwise silently ignore it |
| 200 | +permEnvAddGlobalConst :: (1 <= w, KnownNat w) => DebugLevel -> NatRepr w -> |
| 201 | + PermEnv -> L.Global -> PermEnv |
| 202 | +permEnvAddGlobalConst dlevel w env global = |
| 203 | + let sym = show (L.globalSym global) in |
| 204 | + debugTrace dlevel ("Global: " ++ sym ++ "; value =\n" ++ |
| 205 | + maybe "None" ppLLVMValue |
| 206 | + (L.globalValue global)) $ |
| 207 | + maybe env id $ |
| 208 | + (\x -> case x of |
| 209 | + Just _ -> debugTrace dlevel (sym ++ " translated") x |
| 210 | + Nothing -> debugTrace dlevel (sym ++ " not translated") x) $ |
| 211 | + flip runLLVMTransM (env,dlevel) $ |
| 212 | + do val <- lift $ L.globalValue global |
| 213 | + (sh, t) <- translateLLVMValue w (L.globalType global) val |
| 214 | + let p = ValPerm_LLVMBlock $ llvmReadBlockOfShape sh |
| 215 | + return $ permEnvAddGlobalSyms env |
| 216 | + [PermEnvGlobalEntry (GlobalSymbol $ L.globalSym global) p [t]] |
0 commit comments