From 250c41d40b4eb5a05af8d35e4e134a28b9fcb42f Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 3 Jan 2018 13:18:13 -0800 Subject: [PATCH] Progrsss on symbolic and fixes to x86-support. --- base/src/Data/Macaw/Memory.hs | 3 + symbolic/src/Data/Macaw/Symbolic.hs | 18 +++-- symbolic/src/Data/Macaw/Symbolic/CrucGen.hs | 2 +- .../Data/Macaw/Symbolic/PersistentState.hs | 75 +++++++++++-------- x86/support/macaw-x86-support.cabal | 2 +- x86/support/make_bsd_syscalls/Main.hs | 4 +- 6 files changed, 59 insertions(+), 45 deletions(-) diff --git a/base/src/Data/Macaw/Memory.hs b/base/src/Data/Macaw/Memory.hs index f3994ad8..c4c0e106 100644 --- a/base/src/Data/Macaw/Memory.hs +++ b/base/src/Data/Macaw/Memory.hs @@ -219,6 +219,9 @@ instance Ord (MemWord w) where -- | Typeclass for legal memory widths class (1 <= w) => MemWidth w where + -- | Returns @AddrWidthRepr@ to identify width of pointer. + -- + -- The argument is ignored. addrWidthRepr :: p w -> AddrWidthRepr w -- | @addrWidthMod w@ returns @2^(8 * addrSize w - 1)@. diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 6a5dd9c3..1d979d1d 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -68,23 +68,27 @@ regVars sym nameFn a = _ -> error "internal: regVars encountered case non-exhaustive pattern" #endif +-- | An override that creates a fresh value with the given type. runFreshSymOverride :: M.TypeRepr tp -> C.OverrideSim MacawSimulatorState sym ret EmptyCtx (ToCrucibleType tp) (C.RegValue sym (ToCrucibleType tp)) -runFreshSymOverride = undefined +runFreshSymOverride tp = do + undefined tp -runReadMemOverride :: NatRepr w - -> M.MemRepr tp +-- | Run override that reads a value from memory. +runReadMemOverride :: M.AddrWidthRepr w -- ^ Width of the address. + -> M.MemRepr tp -- ^ Type of value to read. -> C.OverrideSim MacawSimulatorState sym ret (EmptyCtx ::> C.BVType w) (ToCrucibleType tp) (C.RegValue sym (ToCrucibleType tp)) runReadMemOverride = undefined -runWriteMemOverride :: NatRepr w - -> M.MemRepr tp +-- | Run override that writes a value to memory. +runWriteMemOverride :: M.AddrWidthRepr w -- ^ Width of a pointer + -> M.MemRepr tp -- ^ Type of value to write to memory. -> C.OverrideSim MacawSimulatorState sym ret (EmptyCtx ::> C.BVType w ::> ToCrucibleType tp) C.UnitType @@ -99,7 +103,6 @@ createHandleBinding ctx hid = MkFreshSymId repr -> runFreshSymOverride repr ReadMemId repr -> runReadMemOverride (archWidthRepr ctx) repr WriteMemId repr -> runWriteMemOverride (archWidthRepr ctx) repr - SyscallId -> undefined -- | This function identifies all the handles needed, and returns -- function bindings for each one. @@ -113,10 +116,9 @@ createHandleMap ctx = MapF.foldrWithKey go C.emptyHandleMap -> C.FunctionBindings MacawSimulatorState sym -> C.FunctionBindings MacawSimulatorState sym go hid (HandleVal h) b = - let o = C.mkOverride' (handleIdName hid) (handleIdRetType ctx hid) (createHandleBinding ctx hid) + let o = C.mkOverride' (handleIdName hid) (handleIdRetType hid) (createHandleBinding ctx hid) in C.insertHandleMap h (C.UseOverride o) b - mkMemSegmentBinding :: (1 <= w) => C.HandleAllocator s -> NatRepr w diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs index a31e41a3..f2c4f0fc 100644 --- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs +++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs @@ -368,7 +368,7 @@ mkHandleVal hid = do Nothing -> do ctx <- getCtx let argTypes = handleIdArgTypes ctx hid - let retType = handleIdRetType ctx hid + let retType = handleIdRetType hid hndl <- liftST $ C.mkHandle' (handleAlloc ctx) (handleIdName hid) argTypes retType crucPStateLens . handleMapLens %= MapF.insert hid (HandleVal hndl) pure $! hndl diff --git a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs index 37be2e68..be833c35 100644 --- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs +++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs @@ -59,6 +59,7 @@ module Data.Macaw.Symbolic.PersistentState ) where import Control.Lens hiding (Index, (:>), Empty) +import Data.List (intercalate) import qualified Data.Macaw.CFG as M import qualified Data.Macaw.Memory as M import qualified Data.Macaw.Types as M @@ -66,6 +67,7 @@ import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Parameterized.Classes import Data.Parameterized.Context +import qualified Data.Parameterized.List as P import Data.Parameterized.Map (MapF) import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr @@ -83,9 +85,18 @@ import qualified Lang.Crucible.Types as C ------------------------------------------------------------------------ -- Type mappings +type family ToCrucibleBaseTypeList (l :: [M.Type]) :: Ctx C.BaseType where + ToCrucibleBaseTypeList '[] = EmptyCtx + ToCrucibleBaseTypeList (h ': l) = ToCrucibleBaseTypeList l ::> ToCrucibleBaseType h + type family ToCrucibleBaseType (mtp :: M.Type) :: C.BaseType where - ToCrucibleBaseType (M.BVType w) = C.BaseBVType w ToCrucibleBaseType M.BoolType = C.BaseBoolType + ToCrucibleBaseType (M.BVType w) = C.BaseBVType w + ToCrucibleBaseType ('M.TupleType l) = C.BaseStructType (ToCrucibleBaseTypeList l) + +type family CtxToCrucibleBaseType (mtp :: Ctx M.Type) :: Ctx C.BaseType where + CtxToCrucibleBaseType EmptyCtx = EmptyCtx + CtxToCrucibleBaseType (c ::> tp) = CtxToCrucibleBaseType c ::> ToCrucibleBaseType tp type ToCrucibleType tp = C.BaseToType (ToCrucibleBaseType tp) @@ -129,7 +140,11 @@ typeToCrucibleBase tp = case tp of M.BoolTypeRepr -> C.BaseBoolRepr M.BVTypeRepr w -> C.BaseBVRepr w --- M.TupleTypeRepr a -> C.BaseStructRepr (macawAssignToCruc tpyeToCrucibleBase a) + M.TupleTypeRepr a -> C.BaseStructRepr (typeListToCrucibleBase a) + +typeListToCrucibleBase :: P.List M.TypeRepr ctx -> Assignment C.BaseTypeRepr (ToCrucibleBaseTypeList ctx) +typeListToCrucibleBase P.Nil = Empty +typeListToCrucibleBase (h P.:< r) = typeListToCrucibleBase r :> typeToCrucibleBase h typeToCrucible :: M.TypeRepr tp -> C.TypeRepr (ToCrucibleType tp) typeToCrucible = C.baseToType . typeToCrucibleBase @@ -161,10 +176,10 @@ mkRegIndexMap :: OrdF r => Assignment r ctx -> Size (CtxToCrucibleType ctx) -> MapF r (IndexPair ctx) -mkRegIndexMap r0 csz = - case (r0, viewSize csz) of - (Empty, _) -> MapF.empty - (a :> r, IncSize csz0) -> +mkRegIndexMap Empty _ = MapF.empty +mkRegIndexMap (a :> r) csz = + case viewSize csz of + IncSize csz0 -> let m = fmapF extendIndexPair (mkRegIndexMap a csz0) idx = IndexPair (nextIndex (size a)) (nextIndex csz0) in MapF.insert r idx m @@ -201,12 +216,8 @@ data CrucGenContext arch s -- variable storing the base address. } -archWidthRepr :: forall arch ids s . CrucGenContext arch s -> NatRepr (M.ArchAddrWidth arch) -archWidthRepr ctx = archConstraints ctx $ - let arepr :: M.AddrWidthRepr (M.ArchAddrWidth arch) - arepr = M.addrWidthRepr arepr - in M.addrWidthNatRepr arepr - +archWidthRepr :: forall arch s . CrucGenContext arch s -> M.AddrWidthRepr (M.ArchAddrWidth arch) +archWidthRepr ctx = archConstraints ctx $ M.addrWidthRepr (archWidthRepr ctx) regStructRepr :: CrucGenContext arch s -> C.TypeRepr (ArchRegStruct arch) regStructRepr ctx = archConstraints ctx $ @@ -229,7 +240,6 @@ data HandleId arch (ftp :: (Ctx C.CrucibleType, C.CrucibleType)) where '( EmptyCtx ::> ArchAddrCrucibleType arch ::> ToCrucibleType tp , C.UnitType ) - SyscallId :: HandleId arch '(EmptyCtx ::> ArchRegStruct arch, ArchRegStruct arch) instance TestEquality (HandleId arch) where testEquality x y = orderingF_refl (compareF x y) @@ -244,23 +254,27 @@ instance OrdF (HandleId arch) where compareF _ ReadMemId{} = GTF compareF (WriteMemId xr) (WriteMemId yr) = lexCompareF xr yr $ EQF - compareF WriteMemId{} _ = LTF - compareF _ WriteMemId{} = GTF +-- compareF WriteMemId{} _ = LTF +-- compareF _ WriteMemId{} = GTF - compareF SyscallId SyscallId = EQF +typeName :: M.TypeRepr tp -> String +typeName M.BoolTypeRepr = "Bool" +typeName (M.BVTypeRepr w) = "BV" ++ show w +typeName (M.TupleTypeRepr ctx) = "(" ++ intercalate "," (toListFC typeName ctx) ++ ")" + +endName :: M.Endianness -> String +endName M.LittleEndian = "le" +endName M.BigEndian = "be" handleIdName :: HandleId arch ftp -> C.FunctionName handleIdName h = case h of MkFreshSymId repr -> - case repr of - M.BoolTypeRepr -> "symbolicBool" - M.BVTypeRepr w -> fromString $ "symbolicBV" ++ show w - ReadMemId (M.BVMemRepr w _) -> - fromString $ "readMem" ++ show (8 * natValue w) - WriteMemId (M.BVMemRepr w _) -> - fromString $ "writeMem" ++ show (8 * natValue w) - SyscallId -> "syscall" + fromString $ "symbolic_" ++ typeName repr + ReadMemId (M.BVMemRepr w end) -> + fromString $ "readMem_" ++ show (8 * natValue w) ++ "_" ++ endName end + WriteMemId (M.BVMemRepr w end) -> + fromString $ "writeMem_" ++ show (8 * natValue w) ++ "_" ++ endName end handleIdArgTypes :: CrucGenContext arch s -> HandleId arch '(args, ret) @@ -269,23 +283,18 @@ handleIdArgTypes ctx h = case h of MkFreshSymId _repr -> empty ReadMemId _repr -> archConstraints ctx $ - empty :> C.BVRepr (archWidthRepr ctx) + empty :> C.BVRepr (M.addrWidthNatRepr (archWidthRepr ctx)) WriteMemId repr -> archConstraints ctx $ - empty :> C.BVRepr (archWidthRepr ctx) + empty :> C.BVRepr (M.addrWidthNatRepr (archWidthRepr ctx)) :> memReprToCrucible repr - SyscallId -> - empty :> regStructRepr ctx -handleIdRetType :: CrucGenContext arch s - -> HandleId arch '(args, ret) +handleIdRetType :: HandleId arch '(args, ret) -> C.TypeRepr ret -handleIdRetType ctx h = +handleIdRetType h = case h of MkFreshSymId repr -> typeToCrucible repr ReadMemId repr -> memReprToCrucible repr WriteMemId _ -> C.UnitRepr - SyscallId -> regStructRepr ctx - -- | A particular handle in the UsedHandleSet data HandleVal (ftp :: (Ctx C.CrucibleType, C.CrucibleType)) = diff --git a/x86/support/macaw-x86-support.cabal b/x86/support/macaw-x86-support.cabal index 630860ef..b1073611 100644 --- a/x86/support/macaw-x86-support.cabal +++ b/x86/support/macaw-x86-support.cabal @@ -10,7 +10,7 @@ executable make_bsd_syscalls build-depends: base >= 4, bytestring, - language-c >= 0.6, + language-c >= 0.7, lens, pretty, containers, diff --git a/x86/support/make_bsd_syscalls/Main.hs b/x86/support/make_bsd_syscalls/Main.hs index 9ded354e..86efaf15 100644 --- a/x86/support/make_bsd_syscalls/Main.hs +++ b/x86/support/make_bsd_syscalls/Main.hs @@ -81,7 +81,7 @@ syscallLine idents = parseDecl bytes = -- FIXME: we should maybe chain through newNameSupply? I don't think it is ever used ... - case execParser extDeclP bytes (position 0 "" 0 0) idents newNameSupply of + case execParser extDeclP bytes (position 0 "" 0 0 Nothing) idents newNameSupply of Left _err -> Nothing Right (cdecl, _unusedNames) -> Just cdecl @@ -248,7 +248,7 @@ main = do let (syscalls, split_headers) = splitFile (filter (not . BS.null) ls) headers = BS.intercalate "\n" split_headers - Right tunit = parseC headers (position 0 "" 0 0) + Right tunit = parseC headers (position 0 "" 0 0 Nothing) idents = translUnitToIdents tunit ms <- mapM (parseSyscallLine idents) (tail syscalls)