From d978319707bc8e2d3ae20e47509c305b1c27c433 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Jul 2024 15:34:03 -0400 Subject: [PATCH] Review comments --- .../Stubs/FunctionOverride/AArch32/Linux.hs | 2 + .../src/Stubs/FunctionOverride/PPC/Linux.hs | 4 +- .../Stubs/FunctionOverride/X86_64/Linux.hs | 2 + .../src/Stubs/Memory/AArch32/Linux.hs | 24 +++++---- stubs-common/src/Stubs/Memory/PPC/Linux.hs | 12 +++-- stubs-common/src/Stubs/Memory/X86_64/Linux.hs | 14 ++++-- .../src/Stubs/Syscall/Names/AArch32/Linux.hs | 6 +-- .../src/Stubs/Syscall/Names/PPC32/Linux.hs | 6 +-- .../src/Stubs/Syscall/Names/PPC64/Linux.hs | 6 +-- .../src/Stubs/Syscall/Names/X86_64/Linux.hs | 6 +-- stubs-translator/src/Stubs/Arch/AArch32.hs | 50 +++++++++---------- stubs-translator/src/Stubs/Arch/PPC32.hs | 18 +++---- stubs-translator/src/Stubs/Arch/PPC64.hs | 19 +++---- stubs-translator/src/Stubs/Arch/X86.hs | 29 +++++------ 14 files changed, 109 insertions(+), 89 deletions(-) diff --git a/stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs b/stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs index bb41701..abba1a7 100644 --- a/stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs +++ b/stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs @@ -85,6 +85,8 @@ aarch32LinuxIntegerArguments bak archVals argTypes regFile mem = do let ?ptrWidth = ptrWidth let stackArgList = map (AFS.loadIntegerStackArgument bak archVals regFile mem) [0..] + -- NB: `regArgList` below only has four elements, so the cost of using (++) + -- below (which is O(n) in the size of the first list n) is negligible. let argList = regArgList ++ stackArgList AO.buildArgumentAssignment bak argTypes argList where diff --git a/stubs-common/src/Stubs/FunctionOverride/PPC/Linux.hs b/stubs-common/src/Stubs/FunctionOverride/PPC/Linux.hs index 506f302..8d41588 100644 --- a/stubs-common/src/Stubs/FunctionOverride/PPC/Linux.hs +++ b/stubs-common/src/Stubs/FunctionOverride/PPC/Linux.hs @@ -68,7 +68,7 @@ ppcLinuxIntegerArguments ) => bak -> DMS.GenArchVals mem (DMP.AnyPPC v) - -- ^ ARM-specific architecture information + -- ^ PPC-specific architecture information -> LCT.CtxRepr atps -- ^ The argument types -> Ctx.Assignment (LCS.RegValue' sym) (DMS.MacawCrucibleRegTypes (DMP.AnyPPC v)) @@ -84,6 +84,8 @@ ppcLinuxIntegerArguments bak archVals argTypes regs mem = do -- not 0, as the first stack argument is located at @8(r1)@ -- instead of @0(r1)@ (which is where the back chain resides). [1..] + -- NB: `regArgList` below only has eight elements, so the cost of using (++) + -- below (which is O(n) in the size of the first list n) is negligible. let argList = regArgList ++ stackArgList AO.buildArgumentAssignment bak argTypes argList where diff --git a/stubs-common/src/Stubs/FunctionOverride/X86_64/Linux.hs b/stubs-common/src/Stubs/FunctionOverride/X86_64/Linux.hs index 7a13e98..d98734a 100644 --- a/stubs-common/src/Stubs/FunctionOverride/X86_64/Linux.hs +++ b/stubs-common/src/Stubs/FunctionOverride/X86_64/Linux.hs @@ -87,6 +87,8 @@ x86_64LinuxIntegerArguments bak archVals argTypes regs mem = do -- instead of @0(%rsp)@ (which is where the return address -- resides). [1..] + -- NB: `regArgList` below only has six elements, so the cost of using (++) + -- below (which is O(n) in the size of the first list n) is negligible. let argList = regArgList ++ stackArgList AO.buildArgumentAssignment bak argTypes argList where diff --git a/stubs-common/src/Stubs/Memory/AArch32/Linux.hs b/stubs-common/src/Stubs/Memory/AArch32/Linux.hs index 1cbcb5e..52a9172 100644 --- a/stubs-common/src/Stubs/Memory/AArch32/Linux.hs +++ b/stubs-common/src/Stubs/Memory/AArch32/Linux.hs @@ -6,6 +6,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -Wno-orphans #-} {-| Description: IsStubsMemoryModel instance for LLVMMemory with AArch32 @@ -50,7 +51,7 @@ import qualified Data.Macaw.Architecture.Info as DMA import qualified Data.Parameterized.NatRepr as PN import qualified Stubs.Memory as SM import qualified SemMC.Architecture.AArch32 as SAA -import Control.Monad.IO.Class (liftIO) +import Control.Monad.IO.Class (MonadIO(..)) import Data.Macaw.AArch32.Symbolic () import qualified Stubs.Extensions as SE import qualified Data.Macaw.Symbolic.MemOps as DMSMO @@ -59,18 +60,21 @@ import qualified Data.Macaw.BinaryLoader as DMB import qualified Stubs.Loader.BinaryConfig as SLB import qualified Stubs.Memory.Common as SMC -instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where +instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where type instance PtrType DMS.LLVMMemory SAA.AArch32 = LCLM.LLVMPointerType (DMC.ArchAddrWidth SAA.AArch32) type instance MemType DMS.LLVMMemory SAA.AArch32 = LCLM.Mem type instance BVToPtrTy w DMS.LLVMMemory SAA.AArch32 = LCLM.LLVMPointerType w type instance MemTable sym DMS.LLVMMemory SAA.AArch32 = AEM.MemPtrTable sym SAA.AArch32 type instance MemMap sym SAA.AArch32 = DMSMO.GlobalMap sym LCLM.Mem (DMC.ArchAddrWidth SAA.AArch32) - type instance VerifierState sym DMS.LLVMMemory SAA.AArch32 = (SE.AmbientSimulatorState sym SAA.AArch32) + type instance VerifierState sym DMS.LLVMMemory SAA.AArch32 = (SE.AmbientSimulatorState sym SAA.AArch32) - bvToPtr :: LCT.TypeRepr tp-> LCT.TypeRepr (SM.ToPtrTy tp DMS.LLVMMemory SAA.AArch32) - bvToPtr (LCT.BVRepr n) = LCLM.LLVMPointerRepr n - bvToPtr ty = case ty of + bvToPtr :: LCT.TypeRepr tp -> LCT.TypeRepr (SM.ToPtrTy tp DMS.LLVMMemory SAA.AArch32) + bvToPtr ty = case ty of + -- Map BVRepr to LLVMPointerRepr... + LCT.BVRepr n -> LCLM.LLVMPointerRepr n + + -- ...and map all other TypeReprs to themselves. LCT.AnyRepr -> LCT.AnyRepr LCT.UnitRepr -> LCT.UnitRepr LCT.BoolRepr -> LCT.BoolRepr @@ -99,11 +103,13 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where memPtrSize :: PN.NatRepr (DMC.ArchAddrWidth SAA.AArch32) memPtrSize = WI.knownRepr + genStackPtr :: (Monad m, MonadIO m) => LCLM.LLVMPtr sym 32 -> WI.SymBV sym 32 -> SC.Sym sym -> m (LCLM.LLVMPtr sym 32) genStackPtr baseptr offset (SC.Sym sym _) = liftIO $ LCLM.ptrAdd sym WI.knownRepr baseptr offset - initMem (SC.Sym sym bak) archInfo stackSize binConf halloc = do + initMem :: SC.Sym sym -> DMA.ArchitectureInfo SAA.AArch32 -> Integer -> SLB.BinaryConfig SAA.AArch32 binfmt -> LCF.HandleAllocator -> (Monad m, MonadIO m) => m (SM.InitialMemory sym DMS.LLVMMemory SAA.AArch32) + initMem (SC.Sym sym bak) archInfo stackSize binConf halloc = do let endian = DMSM.toCrucibleEndian (DMA.archEndianness archInfo) - + let mems = fmap (DMB.memoryImage . SLB.lbpBinary) (SLB.bcBinaries binConf) let ?ptrWidth = SM.memPtrSize @DMS.LLVMMemory @SAA.AArch32 (recordFn, _) <- liftIO SM.buildRecordLLVMAnnotation @@ -119,7 +125,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory SAA.AArch32 where mem2 <- liftIO $ LCLM.doArrayStore bak mem1 stackBasePtr LCLD.noAlignment stackArrayStorage stackSizeBV (mem3, globals0) <- liftIO $ aarch32LinuxInitGlobals tlsvar (SC.Sym sym bak) mem2 - memVar <- liftIO $ LCLM.mkMemVar (DT.pack "ambient-verifier::memory") halloc + memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc let globals1 = LCSG.insertGlobal memVar mem3 globals0 let globalMap = AEM.mapRegionPointers memPtrTbl diff --git a/stubs-common/src/Stubs/Memory/PPC/Linux.hs b/stubs-common/src/Stubs/Memory/PPC/Linux.hs index 966a021..14e4521 100644 --- a/stubs-common/src/Stubs/Memory/PPC/Linux.hs +++ b/stubs-common/src/Stubs/Memory/PPC/Linux.hs @@ -30,6 +30,7 @@ import qualified What4.Symbol as WSym import qualified Stubs.Memory as AM import qualified Stubs.Common as SC +import qualified Lang.Crucible.FunctionHandle as LCF import qualified Lang.Crucible.Types as LCT import qualified Data.Macaw.Symbolic.Memory as DMSM import qualified Data.Macaw.Architecture.Info as DMA @@ -56,9 +57,12 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) => type instance VerifierState sym DMS.LLVMMemory (DMP.AnyPPC v) = SE.AmbientSimulatorState sym (DMP.AnyPPC v) - bvToPtr :: LCT.TypeRepr tp-> LCT.TypeRepr (SM.ToPtrTy tp DMS.LLVMMemory (DMP.AnyPPC v)) - bvToPtr (LCT.BVRepr n) = LCLM.LLVMPointerRepr n + bvToPtr :: LCT.TypeRepr tp -> LCT.TypeRepr (SM.ToPtrTy tp DMS.LLVMMemory (DMP.AnyPPC v)) bvToPtr ty = case ty of + -- Map BVRepr to LLVMPointerRepr... + LCT.BVRepr n -> LCLM.LLVMPointerRepr n + + -- ...and map all other TypeReprs to themselves. LCT.AnyRepr -> LCT.AnyRepr LCT.UnitRepr -> LCT.UnitRepr LCT.BoolRepr -> LCT.BoolRepr @@ -87,8 +91,10 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) => memPtrSize :: PN.NatRepr (SAP.AddrWidth v) memPtrSize = WI.knownRepr + genStackPtr :: (Monad m, MonadIO m) => LCLM.LLVMPtr sym (SAP.AddrWidth v) -> WI.SymBV sym (SAP.AddrWidth v) -> SC.Sym sym -> m (LCLM.LLVMPtr sym (SAP.AddrWidth v)) genStackPtr baseptr offset (SC.Sym sym _) = liftIO $ LCLM.ptrAdd sym WI.knownRepr baseptr offset + initMem :: SC.Sym sym -> DMA.ArchitectureInfo (DMP.AnyPPC v) -> Integer -> SLB.BinaryConfig (DMP.AnyPPC v) binfmt -> LCF.HandleAllocator -> (Monad m, MonadIO m) => m (SM.InitialMemory sym DMS.LLVMMemory (DMP.AnyPPC v)) initMem (SC.Sym sym bak) archInfo stackSize binConf halloc = do let endian = DMSM.toCrucibleEndian (DMA.archEndianness archInfo) @@ -105,7 +111,7 @@ instance (DMS.SymArchConstraints (DMP.AnyPPC v), 16 WI.<= SAP.AddrWidth v) => stackArrayStorage <- liftIO $ WI.freshConstant sym (WSym.safeSymbol "stack_array") WI.knownRepr mem2 <- liftIO $ LCLM.doArrayStore bak mem1 stackBasePtr LCLD.noAlignment stackArrayStorage stackSizeBV - memVar <- liftIO $ LCLM.mkMemVar (DT.pack "ambient-verifier::memory") halloc + memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc let globals = LCSG.insertGlobal memVar mem2 LCSG.emptyGlobals let globalMap = AEM.mapRegionPointers memPtrTbl diff --git a/stubs-common/src/Stubs/Memory/X86_64/Linux.hs b/stubs-common/src/Stubs/Memory/X86_64/Linux.hs index 1f1ec2d..f20d166 100644 --- a/stubs-common/src/Stubs/Memory/X86_64/Linux.hs +++ b/stubs-common/src/Stubs/Memory/X86_64/Linux.hs @@ -124,9 +124,12 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where } return $ SE.ambientExtensions @sym @DMX.X86_64 bak f initialMem mmConf mempty - bvToPtr :: LCT.TypeRepr tp-> LCT.TypeRepr (SM.ToPtrTy tp DMS.LLVMMemory DMX.X86_64) - bvToPtr (LCT.BVRepr n) = LCLM.LLVMPointerRepr n + bvToPtr :: LCT.TypeRepr tp -> LCT.TypeRepr (SM.ToPtrTy tp DMS.LLVMMemory DMX.X86_64) bvToPtr ty = case ty of + -- Map BVRepr to LLVMPointerRepr... + LCT.BVRepr n -> LCLM.LLVMPointerRepr n + + -- ...and map all other TypeReprs to themselves. LCT.AnyRepr -> LCT.AnyRepr LCT.UnitRepr -> LCT.UnitRepr LCT.BoolRepr -> LCT.BoolRepr @@ -152,12 +155,17 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where LCT.SymbolicStructRepr r -> LCT.SymbolicStructRepr r LCT.ReferenceRepr r -> LCT.ReferenceRepr r + genStackPtr :: (Monad m, MonadIO m) => LCLM.LLVMPtr sym 64 -> WI.SymBV sym 64 -> SC.Sym sym -> m (LCLM.LLVMPtr sym 64) genStackPtr baseptr offset (SC.Sym sym _) = liftIO $ LCLM.ptrAdd sym WI.knownRepr baseptr offset + + insertStackPtr :: (WI.IsExprBuilder sym, LCB.IsSymInterface sym) => DMS.GenArchVals DMS.LLVMMemory DMX.X86_64 -> LCLM.LLVMPtr sym 64 -> LCS.RegEntry sym (LCT.StructType (DMS.CtxToCrucibleType (DMS.ArchRegContext DMX.X86_64))) -> LCS.RegEntry sym (LCT.StructType (DMS.CtxToCrucibleType (DMS.ArchRegContext DMX.X86_64))) insertStackPtr archVals sp initialRegsEntry= DMS.updateReg archVals initialRegsEntry DMC.sp_reg sp memPtrSize :: PN.NatRepr (DMC.ArchAddrWidth DMX.X86_64) memPtrSize = WI.knownRepr + + initMem :: SC.Sym sym -> DMA.ArchitectureInfo DMX.X86_64 -> Integer -> SLB.BinaryConfig DMX.X86_64 binfmt -> LCF.HandleAllocator -> (Monad m, MonadIO m) => m (SM.InitialMemory sym DMS.LLVMMemory DMX.X86_64) initMem (SC.Sym sym bak) archInfo stackSize binConf halloc = do let mems = fmap (DMB.memoryImage . SLB.lbpBinary) (SLB.bcBinaries binConf) @@ -177,7 +185,7 @@ instance SM.IsStubsMemoryModel DMS.LLVMMemory DMX.X86_64 where stackArrayStorage <- liftIO $ WI.freshConstant sym (WSym.safeSymbol "stack_array") WI.knownRepr mem2 <- liftIO $ LCLM.doArrayStore bak mem1 stackBasePtr LCLD.noAlignment stackArrayStorage stackSizeBV (mem3, globals0) <- liftIO $ x86_64LinuxInitGlobals fsvar gsvar (SC.Sym sym bak) mem2 - memVar <- liftIO $ LCLM.mkMemVar (DT.pack "ambient-verifier::memory") halloc + memVar <- liftIO $ LCLM.mkMemVar (DT.pack "stubs::memory") halloc let globals1 = LCSG.insertGlobal memVar mem3 globals0 let globalMap = AEM.mapRegionPointers memPtrTbl diff --git a/stubs-common/src/Stubs/Syscall/Names/AArch32/Linux.hs b/stubs-common/src/Stubs/Syscall/Names/AArch32/Linux.hs index dc917f7..c764b43 100644 --- a/stubs-common/src/Stubs/Syscall/Names/AArch32/Linux.hs +++ b/stubs-common/src/Stubs/Syscall/Names/AArch32/Linux.hs @@ -7,10 +7,8 @@ -- the information that's contained within -- syscalls_arm.tbl. module Stubs.Syscall.Names.AArch32.Linux - ( - syscallMap - ) - where + ( syscallMap + ) where import qualified Data.IntMap.Strict as IM import qualified Data.Text as DT diff --git a/stubs-common/src/Stubs/Syscall/Names/PPC32/Linux.hs b/stubs-common/src/Stubs/Syscall/Names/PPC32/Linux.hs index 81452b5..9823170 100644 --- a/stubs-common/src/Stubs/Syscall/Names/PPC32/Linux.hs +++ b/stubs-common/src/Stubs/Syscall/Names/PPC32/Linux.hs @@ -7,10 +7,8 @@ -- the information that's contained within -- syscalls_powerpc.tbl. module Stubs.Syscall.Names.PPC32.Linux - ( - syscallMap - ) - where + ( syscallMap + ) where import qualified Data.IntMap.Strict as IM import qualified Data.Text as DT diff --git a/stubs-common/src/Stubs/Syscall/Names/PPC64/Linux.hs b/stubs-common/src/Stubs/Syscall/Names/PPC64/Linux.hs index 1b3d3d2..89fe4a4 100644 --- a/stubs-common/src/Stubs/Syscall/Names/PPC64/Linux.hs +++ b/stubs-common/src/Stubs/Syscall/Names/PPC64/Linux.hs @@ -7,10 +7,8 @@ -- the information that's contained within -- syscalls_powerpc.tbl. module Stubs.Syscall.Names.PPC64.Linux - ( - syscallMap - ) - where + ( syscallMap + ) where import qualified Data.IntMap.Strict as IM import qualified Data.Text as DT diff --git a/stubs-common/src/Stubs/Syscall/Names/X86_64/Linux.hs b/stubs-common/src/Stubs/Syscall/Names/X86_64/Linux.hs index efca7bd..5865491 100644 --- a/stubs-common/src/Stubs/Syscall/Names/X86_64/Linux.hs +++ b/stubs-common/src/Stubs/Syscall/Names/X86_64/Linux.hs @@ -7,10 +7,8 @@ -- the information that's contained within -- syscalls_x86_64.tbl. module Stubs.Syscall.Names.X86_64.Linux - ( - syscallMap - ) - where + ( syscallMap + ) where import qualified Data.IntMap.Strict as IM import qualified Data.Text as DT diff --git a/stubs-translator/src/Stubs/Arch/AArch32.hs b/stubs-translator/src/Stubs/Arch/AArch32.hs index 76ada44..7ef0953 100644 --- a/stubs-translator/src/Stubs/Arch/AArch32.hs +++ b/stubs-translator/src/Stubs/Arch/AArch32.hs @@ -1,19 +1,19 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-orphans #-} -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wno-orphans #-} {-| -Description: Preamble Instance for AArch32 +Description: 'SPR.Preamble' Instance for AArch32 -} module Stubs.Arch.AArch32() where import qualified Stubs.AST as SA @@ -33,12 +33,12 @@ import qualified Data.Parameterized.Map as MapF import qualified Stubs.Translate.Intrinsic as STI import qualified Lang.Crucible.LLVM.MemModel as LCLM -instance STC.StubsArch SAA.AArch32 where +instance STC.StubsArch SAA.AArch32 where type instance ArchIntSize SAA.AArch32 = 32 type instance ArchShortSize SAA.AArch32 =16 type instance ArchLongSize SAA.AArch32 = 64 - + toCrucibleTy tyrepr = do case tyrepr of SA.StubsIntRepr -> return $ LCT.BVRepr (PN.knownNat @32) @@ -52,28 +52,28 @@ instance STC.StubsArch SAA.AArch32 where SA.StubsUShortRepr -> return $ LCT.BVRepr (PN.knownNat @16) SA.StubsCharRepr -> pure $ LCT.BVRepr (PN.knownNat @8) SA.StubsUCharRepr -> pure $ LCT.BVRepr (PN.knownNat @8) - SA.StubsAliasRepr s -> do - env <- STC.getStubEnv + SA.StubsAliasRepr s -> do + env <- STC.getStubEnv let tymap = STC.stTyMap env - case MapF.lookup s tymap of + case MapF.lookup s tymap of Just (STC.WrappedStubsTypeAliasRepr _ t) -> STC.toCrucibleTy t Nothing -> error $ "missing type alias: " ++ show s - SA.StubsIntrinsicRepr s -> do - env <- STC.getStubEnv - let intrinsicMap = STC.stIntrinsicMap env - case MapF.lookup s intrinsicMap of - Just (STC.WrappedIntrinsicRepr _ t) -> return t + SA.StubsIntrinsicRepr s -> do + env <- STC.getStubEnv + let intrinsicMap = STC.stIntrinsicMap env + case MapF.lookup s intrinsicMap of + Just (STC.WrappedIntrinsicRepr _ t) -> return t Nothing -> error $ "Missing intrinsic: " ++ show s - SA.StubsTupleRepr t -> do + SA.StubsTupleRepr t -> do internal <- STC.toCrucibleTyCtx @_ @SAA.AArch32 t return (LCT.StructRepr internal) - translateLit lit = do + translateLit lit = do let n = PN.knownNat @32 let ln = PN.knownNat @64 let sn = PN.knownNat @16 let sc = PN.knownNat @8 - case lit of + case lit of SA.BoolLit b -> LCCR.App $ LCCE.BoolLit b SA.UnitLit -> LCCR.App LCCE.EmptyApp SA.IntLit i -> LCCR.App (LCCE.IntegerToBV n $ LCCR.App $ LCCE.IntLit i) @@ -101,10 +101,10 @@ instance SPR.Preamble SAA.AArch32 where preambleMap SA.StubsSignature{SA.sigFnName="ushort",SA.sigFnArgTys=(Ctx.Empty Ctx.:> SA.StubsShortRepr), SA.sigFnRetTy=SA.StubsUShortRepr} = bvIdOverride @SAA.AArch32 "ushort" preambleMap SA.StubsSignature{SA.sigFnName="long",SA.sigFnArgTys=(Ctx.Empty Ctx.:> SA.StubsULongRepr), SA.sigFnRetTy=SA.StubsLongRepr} = bvIdOverride @SAA.AArch32 "long" preambleMap SA.StubsSignature{SA.sigFnName="ulong",SA.sigFnArgTys=(Ctx.Empty Ctx.:> SA.StubsLongRepr), SA.sigFnRetTy=SA.StubsULongRepr} = bvIdOverride @SAA.AArch32 "ulong" - preambleMap SA.StubsSignature{SA.sigFnName="uint_s",SA.sigFnArgTys=(Ctx.Empty Ctx.:> SA.StubsUShortRepr), SA.sigFnRetTy=SA.StubsUIntRepr} = bvExtendOverride @SAA.AArch32 "uint_s" False + preambleMap SA.StubsSignature{SA.sigFnName="uint_s",SA.sigFnArgTys=(Ctx.Empty Ctx.:> SA.StubsUShortRepr), SA.sigFnRetTy=SA.StubsUIntRepr} = bvExtendOverride @SAA.AArch32 "uint_s" False preambleMap SA.StubsSignature{SA.sigFnName="ulong_i",SA.sigFnArgTys=(Ctx.Empty Ctx.:> SA.StubsUIntRepr), SA.sigFnRetTy=SA.StubsULongRepr} = bvExtendOverride @SAA.AArch32 "ulong_i" False preambleMap sig = error ("Missing implementation for preamble function:"++SA.sigFnName sig) -instance STI.OverrideArch SAA.AArch32 where +instance STI.OverrideArch SAA.AArch32 where buildOverrides = pure [] - \ No newline at end of file + diff --git a/stubs-translator/src/Stubs/Arch/PPC32.hs b/stubs-translator/src/Stubs/Arch/PPC32.hs index 08f5f9d..de49a90 100644 --- a/stubs-translator/src/Stubs/Arch/PPC32.hs +++ b/stubs-translator/src/Stubs/Arch/PPC32.hs @@ -1,19 +1,19 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-orphans #-} -{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wno-orphans #-} {-| -Description: Preamble Instance for PPC32 +Description: 'SPR.Preamble' Instance for PPC32 -} module Stubs.Arch.PPC32() where import qualified Stubs.AST as SA diff --git a/stubs-translator/src/Stubs/Arch/PPC64.hs b/stubs-translator/src/Stubs/Arch/PPC64.hs index e8ef82e..2ccffd2 100644 --- a/stubs-translator/src/Stubs/Arch/PPC64.hs +++ b/stubs-translator/src/Stubs/Arch/PPC64.hs @@ -1,18 +1,19 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DataKinds #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wno-orphans #-} + {-| -Description: Preamble Instance for PPC64 +Description: 'SPR.Preamble' Instance for PPC64 -} module Stubs.Arch.PPC64() where import qualified Stubs.AST as SA diff --git a/stubs-translator/src/Stubs/Arch/X86.hs b/stubs-translator/src/Stubs/Arch/X86.hs index 77adb6e..1c4bea4 100644 --- a/stubs-translator/src/Stubs/Arch/X86.hs +++ b/stubs-translator/src/Stubs/Arch/X86.hs @@ -1,18 +1,19 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DataKinds #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# OPTIONS_GHC -Wno-orphans #-} + {-| -Description: Preamble Instance for X86_64 +Description: 'SPR.Preamble' Instance for X86_64 -} module Stubs.Arch.X86() where import qualified Stubs.AST as SA @@ -32,7 +33,7 @@ import GHC.Natural (naturalToInteger) import qualified Data.Parameterized.Map as MapF import qualified Stubs.Translate.Intrinsic as STI import qualified Data.Parameterized as P -import qualified Stubs.Common as SC +import qualified Stubs.Common as SC import qualified Lang.Crucible.Simulator as LCS import Control.Monad.IO.Class (MonadIO) import qualified Lang.Crucible.LLVM.MemModel as LCLM @@ -69,7 +70,7 @@ instance STC.StubsArch DMX.X86_64 where Just (STC.WrappedIntrinsicRepr _ t) -> return t Nothing -> error $ "Missing intrinsic: " ++ show s - SA.StubsTupleRepr t -> do + SA.StubsTupleRepr t -> do internal <- STC.toCrucibleTyCtx @_ @DMX.X86_64 t return (LCT.StructRepr internal) @@ -111,7 +112,7 @@ instance SPR.Preamble DMX.X86_64 where preambleMap sig = error ("Missing implementation for preamble function:"++SA.sigFnName sig) instance STI.OverrideArch DMX.X86_64 where - buildOverrides = do + buildOverrides = do allocModule <- mallocOv @DMX.X86_64 return [allocModule] @@ -124,6 +125,6 @@ mallocStub ptr = STI.SomeStubsOverride (STI.StubsOverride (\(SC.Sym sym _)-> do )) (Ctx.extend Ctx.empty (LCT.BVRepr @32 WI.knownRepr)) LCT.BoolRepr) (SA.StubsSignature "malloc" (Ctx.extend Ctx.empty SA.StubsIntRepr) (SA.StubsIntrinsicRepr ptr)) mallocOv :: (STC.StubsArch arch, MonadIO m) => m (STI.OverrideModule arch) -mallocOv = do +mallocOv = do P.Some ptr <- return $ P.someSymbol "Pointer" - return $ STI.OverrideModule "alloc" [mallocStub ptr] [STI.SomeIntrinsicTyDecl (STI.IntrinsicTyDecl ptr LCT.BoolRepr)] [] \ No newline at end of file + return $ STI.OverrideModule "alloc" [mallocStub ptr] [STI.SomeIntrinsicTyDecl (STI.IntrinsicTyDecl ptr LCT.BoolRepr)] []