GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-28 08:34:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/GaloisInc/macaw into HEAD

Browse Source
This commit is contained in:
Joey Dodds 2018-09-27 15:39:01 -07:00
commit 4f1f8656dd
18 changed files with 896 additions and 478 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
base/macaw-base.cabal
View File

@ -31,15 +31,16 @@ library
base >= 4,
ansi-wl-pprint,
binary,
binary-symbols,
binary-symbols >= 0.1.1,
bytestring,
containers >= 0.5.8.1,
elf-edit >= 0.29,
elf-edit >= 0.32,
galois-dwarf,
IntervalMap >= 0.5,
lens >= 4.7,
mtl,
parameterized-utils >= 1.0.1,
template-haskell,
text,
vector,
QuickCheck >= 2.7

4
base/src/Data/Macaw/CFG/Core.hs
View File

@ -707,8 +707,8 @@ ppStmt ppOff stmt =
where
ppAddr addr =
case asAbsoluteAddr addr of
Just absAddr -> ppOff absAddr
Nothing -> PP.braces (PP.int (addrBase addr)) PP.<> ppOff (addrOffset addr)
Just absAddr -> text (show absAddr)
Nothing -> PP.braces (PP.int (addrBase addr)) PP.<> text "+" PP.<> text (show (addrOffset addr))
prefix = text "#" <+> ppAddr a PP.<> text ": "
ppUpdate key val acc = text (showF key) <+> text "=>" <+> ppValue 0 val : acc

6
base/src/Data/Macaw/Discovery.hs
View File

@ -644,13 +644,15 @@ resolveAsAbsoluteAddr mem endianness l = addrWidthClass (memAddrWidth mem) $
[ByteRegion bs] -> do
absoluteAddr <$> addrRead endianness bs
[RelocationRegion r] -> do
let off = relocationOffset r
when (relocationIsRel r) $ Nothing
case relocationSym r of
SymbolRelocation{} -> Nothing
SectionIdentifier idx -> do
addr <- Map.lookup idx (memSectionAddrMap mem)
pure $ relativeSegmentAddr addr & incAddr (toInteger off)
pure $ relativeSegmentAddr addr & incAddr (toInteger (relocationOffset r))
SegmentBaseAddr idx -> do
addr <- Map.lookup idx (memSegmentAddrMap mem)
pure $ relativeSegmentAddr addr & incAddr (toInteger (relocationOffset r))
_ -> Nothing
-- This function resolves jump table entries.

166
base/src/Data/Macaw/Memory.hs
View File

@ -39,18 +39,16 @@ module Data.Macaw.Memory
, Endianness(..)
, bytesToInteger
-- * MemSegment operations
, MemSegment
, MemSegment(..)
, RegionIndex
, AddrOffsetMap
, PresymbolData
, takePresymbolBytes
, RelocEntry(..)
, ResolveFn
, memSegment
, segmentBase
, segmentOffset
, segmentFlags
, segmentContents
, byteSegments
, SegmentContents
, contentsFromList
, contentsRanges
, ppMemSegment
, segmentSize
@ -95,7 +93,9 @@ module Data.Macaw.Memory
, SymbolUndefType(..)
-- * Section addresses
, memAddSectionAddr
, memAddSegmentAddr
, memSectionAddrMap
, memSegmentAddrMap
-- * General purposes addrs
, MemAddr(..)
, absoluteAddr
@ -159,6 +159,9 @@ import Data.Parameterized.NatRepr
import qualified Data.Macaw.Memory.Permissions as Perm
-- | Maps an address to the symbol that it is associated for.
type AddrOffsetMap w v = Map (MemWord w) v
------------------------------------------------------------------------
-- AddrWidthRepr
@ -611,10 +614,16 @@ contentsRanges :: SegmentContents w -> [(MemWord w, SegmentRange w)]
contentsRanges = Map.toList . segContentsMap
------------------------------------------------------------------------
-- Code for injecting relocations into segments.
-- Presymbol data
-- | Contents of segment/section before symbol folded in.
data PresymbolData = PresymbolData !L.ByteString !Int64
data PresymbolData = PresymbolData { preBytes :: !L.ByteString
, preBSS :: !Int64
}
-- | Return number of presymbol bytes remaining
presymbolBytesLeft :: PresymbolData -> Integer
presymbolBytesLeft p = toInteger (L.length (preBytes p)) + toInteger (preBSS p)
mkPresymbolData :: L.ByteString -> Int64 -> PresymbolData
mkPresymbolData contents0 sz
@ -652,46 +661,61 @@ dropSegment cnt (PresymbolData contents bssSize)
-- | Return the given bytes
takePresymbolBytes :: Int64 -> PresymbolData -> Maybe BS.ByteString
takePresymbolBytes cnt (PresymbolData contents bssSize)
| toInteger (L.length contents) + toInteger bssSize > toInteger cnt =
Just $ L.toStrict (L.take cnt contents)
<> BS.replicate (fromIntegral cnt - fromIntegral (L.length contents)) 0
| otherwise = Nothing
takePresymbolBytes cnt p
| toInteger cnt <= presymbolBytesLeft p =
Just $ L.toStrict (L.take cnt (preBytes p))
<> BS.replicate (fromIntegral cnt - fromIntegral (L.length (preBytes p))) 0
| otherwise =
Nothing
-- | Maps an address to the symbol that it is associated for.
type AddrOffsetMap w v = Map (MemWord w) v
type ResolveFn v m w = v -> PresymbolData -> m (Maybe (Relocation w, MemWord w))
------------------------------------------------------------------------
-- Relocation processing
-- | Function for resolving the new contents of a relocation entry given an optional
-- index for the current segment and the existing contents.
--
-- The segment index is used for dynamic relocations and set to
-- `Nothing` for static relocations.
type ResolveFn m w = Maybe SegmentIndex -> BS.ByteString -> m (Maybe (Relocation w))
-- | Information about a relocation sufficient to know how many bytes
-- are affected, and how to replaces the existing bytes.
data RelocEntry m w = RelocEntry { relocEntrySize :: !(MemWord w)
-- ^ Number of bytes in relocation
, applyReloc :: !(ResolveFn m w)
}
-- | This takes a list of symbols and an address and coerces into a memory contents.
--
-- If the size is different from the length of file contents, then the file content
-- buffer is truncated or zero-extended as in a BSS.
byteSegments :: forall v m w
byteSegments :: forall m w
. (Monad m, MemWidth w)
=> ResolveFn v m w
-> AddrOffsetMap w v -- ^ Map from addresses to symbolis
-> MemWord w -- ^ Base address for segment
=> Map (MemWord w) (RelocEntry m w) -- ^ Map from segment offset to relocation
-> Maybe SegmentIndex
-- ^ Index of segment for relocation purposes if this is a dynamic address
-> MemWord w -- ^ Base address for segment at link time.
-> L.ByteString -- ^ File contents for segment.
-> Int64 -- ^ Expected size
-> m [SegmentRange w]
byteSegments resolver relocMap initBase contents0 regionSize
| end <= initBase =
byteSegments relocMap msegIdx linkBaseOff contents0 regionSize
| end <= linkBaseOff =
error $ "regionSize should be a positive number that does not overflow address space."
| otherwise =
bytesToSegmentsAscending [] symbolPairs initBase (mkPresymbolData contents0 regionSize)
bytesToSegmentsAscending [] symbolPairs linkBaseOff (mkPresymbolData contents0 regionSize)
where -- Parse the map to get a list of symbols starting at base0.
symbolPairs :: [(MemWord w, v)]
symbolPairs :: [(MemWord w, RelocEntry m w)]
symbolPairs
= Map.toList
$ Map.dropWhileAntitone (< initBase) relocMap
$ Map.dropWhileAntitone (< linkBaseOff) relocMap
end :: MemWord w
end = initBase + fromIntegral regionSize
end = linkBaseOff + fromIntegral regionSize
-- Traverse the list of symbols that we should parse.
bytesToSegmentsAscending :: [SegmentRange w]
-> [(MemWord w, v)]
-> [(MemWord w, RelocEntry m w)]
-- ^ List of relocations to process in order.
-> MemWord w
-- ^ Address we are currently at
@ -702,26 +726,31 @@ byteSegments resolver relocMap initBase contents0 regionSize
-> m [SegmentRange w]
bytesToSegmentsAscending pre ((addr,v):rest) ioff contents
-- We only consider relocations that are in the range of this segment,
-- so we require the difference between the address and initBase is
-- so we require the difference between the address and linkBaseOff is
-- less than regionSize
| addr < end = do
when (addr < ioff) $ do
error "Encountered overlapping relocations."
mr <- resolver v contents
case mr of
Just (r,rsz) -> do
when (rsz < 1 || ioff + rsz > end) $ do
error $ "Region size " ++ show rsz ++ " is out of range."
-- Get number of bytes between this address offset and the current offset."
let addrDiff = addr - ioff
let post = dropSegment (fromIntegral (addrDiff + rsz)) contents
let pre' = [RelocationRegion r]
++ reverse (takeSegment (fromIntegral addrDiff) contents)
++ pre
bytesToSegmentsAscending pre' rest (addr + rsz) post
_ -> do
-- Skipping relocation
bytesToSegmentsAscending pre rest ioff contents
let rsz = relocEntrySize v
case takePresymbolBytes (fromIntegral rsz) contents of
Nothing -> do
error $ "Relocation at " ++ show addr ++ " needs "
++ show rsz ++ " bytes, but only " ++ show (presymbolBytesLeft contents)
++ " bytes remaining."
Just bytes -> do
mr <- applyReloc v msegIdx bytes
case mr of
Just r -> do
-- Get number of bytes between this address offset and the current offset."
let addrDiff = addr - ioff
let post = dropSegment (fromIntegral (addrDiff + rsz)) contents
let pre' = [RelocationRegion r]
++ reverse (takeSegment (fromIntegral addrDiff) contents)
++ pre
bytesToSegmentsAscending pre' rest (addr + rsz) post
Nothing -> do
-- Skipping relocation
bytesToSegmentsAscending pre rest ioff contents
bytesToSegmentsAscending pre _ _ contents =
pure $ reverse pre ++ allSymbolData contents
@ -750,40 +779,6 @@ data MemSegment w
-- the segment.
}
-- | This creates a memory segment.
memSegment :: forall v m w
. (Monad m, MemWidth w)
=> ResolveFn v m w
-- ^ Function for resolving relocation entries.
-> RegionIndex
-- ^ Index of base (0=absolute address)
-> AddrOffsetMap w v
-- ^ Relocations we may need to apply when creating the
-- segment. These are all relative to the given region.
-> MemWord w
-- ^ Offset of segment
-> Perm.Flags
-- ^ Flags if defined
-> L.ByteString
-- ^ File contents for segment.
-> Int64
-- ^ Expected size (must be positive)
-> m (MemSegment w)
memSegment resolve base allSymbols off flags bytes sz
-- Return nothing if size is not positive
| not (sz > 0) = error $ "Memory segments must have a positive size."
-- Check for overflow in contents end
| toInteger off + toInteger sz > toInteger (maxBound :: MemWord w) =
error "Contents two large for base."
| otherwise = do
contents <- byteSegments resolve allSymbols off bytes sz
pure $
MemSegment { segmentBase = base
, segmentOffset = off
, segmentFlags = flags
, segmentContents = contentsFromList contents
}
instance Eq (MemSegment w) where
x == y = segmentBase x == segmentBase y
&& segmentOffset x == segmentOffset y
@ -822,6 +817,8 @@ data Memory w = Memory { memAddrWidth :: !(AddrWidthRepr w)
-- ^ Segment map
, memSectionAddrMap :: !(Map SectionIndex (MemSegmentOff w))
-- ^ Map from section indices to addresses.
, memSegmentAddrMap :: !(Map SegmentIndex (MemSegmentOff w))
-- ^ Map from segment indices to addresses.
}
-- | Get memory segments.
@ -840,14 +837,23 @@ memAddSectionAddr idx addr mem
| otherwise =
mem { memSectionAddrMap = Map.insert idx addr (memSectionAddrMap mem) }
-- | Add a new segment index to address binding
memAddSegmentAddr :: SegmentIndex -> MemSegmentOff w -> Memory w -> Memory w
memAddSegmentAddr idx addr mem
| Map.member idx (memSegmentAddrMap mem) =
error $ "memAddSegmentAddr: duplicate index " ++ show idx
| otherwise =
mem { memSegmentAddrMap = Map.insert idx addr (memSegmentAddrMap mem) }
instance MemWidth w => Show (Memory w) where
show = show . memSegments
-- | A memory with no segments.
emptyMemory :: AddrWidthRepr w -> Memory w
emptyMemory w = Memory { memAddrWidth = w
, memSegmentMap = Map.empty
emptyMemory w = Memory { memAddrWidth = w
, memSegmentMap = Map.empty
, memSectionAddrMap = Map.empty
, memSegmentAddrMap = Map.empty
}
-- | Get executable segments.
@ -1451,7 +1457,7 @@ findByteStringMatches pat curIndex segs@((relOffset, chunk) : rest)
matchPrefix :: MemWidth w => BS.ByteString -> [SegmentRange w] -> Bool
matchPrefix _ [] = False
matchPrefix _ (BSSRegion _ : _) = False
matchPrefix pat (rel@(RelocationRegion r) : rest)
matchPrefix pat (rel@(RelocationRegion _r) : rest)
-- When pattern is greater than size of the relocation, skip
-- relocation bytes in the pattern and look for match in beginning
-- of the next range.

529
base/src/Data/Macaw/Memory/ElfLoader.hs
View File

@ -1,5 +1,5 @@
{-|
Copyright : Galois Inc, 2016
Copyright : Galois Inc, 2016-18
Maintainer : jhendrix@galois.com
Operations for creating a view of memory from an elf file.
@ -39,6 +39,7 @@ import qualified Data.ByteString.Lazy as L
import Data.Either
import Data.ElfEdit
( ElfWordType
, ElfIntType
, Elf
, elfSections
, elfLayout
@ -73,6 +74,7 @@ import qualified Data.Set as Set
import qualified Data.Vector as V
import Data.Word
import Numeric (showHex)
import Data.Int
import Data.Macaw.Memory
import Data.Macaw.Memory.LoadCommon
@ -119,6 +121,34 @@ flagsForSectionFlags f =
where flagIf :: ElfSectionFlags w -> Perm.Flags -> Perm.Flags
flagIf ef pf = if f `Elf.hasPermissions` ef then pf else Perm.none
------------------------------------------------------------------------
-- RelocationError
data RelocationError
= RelocationZeroSymbol
-- ^ A relocation refers to the symbol index 0.
| RelocationBadSymbolIndex !Int
-- ^ A relocation entry referenced a bad symbol index.
| RelocationUnsupportedType !String
-- ^ We do not support this type of relocation.
| RelocationFileUnsupported
-- ^ We do not allow relocations to refer to the "file" as in Elf.
| RelocationInvalidAddend !String !Integer
-- ^ The relocation type given does not allow the adddend with the given value.
instance Show RelocationError where
show RelocationZeroSymbol =
"A relocation entry referred to invalid 0 symbol index."
show (RelocationBadSymbolIndex idx) =
"A relocation entry referred to invalid symbol index " ++ show idx ++ "."
show (RelocationUnsupportedType tp) =
"Do not yet support relocation type " ++ tp ++ "."
show RelocationFileUnsupported =
"Do not support relocations referring to file entry."
show (RelocationInvalidAddend tp v) =
"Do not support addend of " ++ show v ++ " with relocation type " ++ tp ++ "."
------------------------------------------------------------------------
-- MemLoader
@ -133,8 +163,8 @@ data MemLoadWarning
| DynamicRelaAndRelPresent
-- ^ Issued if the dynamic section contains table for DT_REL and
-- DT_RELA.
| DuplicateRelocationSections !B.ByteString
-- ^ @DuplicateRelocationSections nm@ is issued if we encounter
| SectionRelaAndRelPresent !B.ByteString
-- ^ @SectionRelaAndRelPresent nm@ is issued if we encounter
-- both section ".rela$nm" and ".rel$nm".
| UnsupportedSection !SectionName
| UnknownDefinedSymbolBinding !SymbolName Elf.ElfSymbolBinding
@ -163,9 +193,9 @@ instance Show MemLoadWarning where
show (RelocationParseFailure msg) =
"Error parsing relocations: " ++ msg
show DynamicRelaAndRelPresent =
"Dynamic section contains contain offsets for both DT_REL and DT_RELA relocation tables; "
"PT_DYNAMIC segment contains contain offsets for both DT_REL and DT_RELA relocation tables; "
++ " Using only DT_RELA relocations."
show (DuplicateRelocationSections (BSC.unpack -> nm)) =
show (SectionRelaAndRelPresent (BSC.unpack -> nm)) =
"File contains both .rela" ++ nm ++ " and .rel" ++ nm
++ " sections; Using only .rela" ++ nm ++ " sections."
show (UnsupportedSection nm) =
@ -212,26 +242,6 @@ addWarning w = modify $ \s -> s { mlsWarnings = w : mlsWarnings s }
type MemLoader w = StateT (MemLoaderState w) (Except (LoadError w))
data RelocationError
= RelocationZeroSymbol
-- ^ A relocation refers to the symbol index 0.
| RelocationBadSymbolIndex !Int
-- ^ A relocation entry referenced a bad symbol index.
| RelocationUnsupportedType !String
-- ^ We do not support relocations with this architecture.
| RelocationFileUnsupported
-- ^ We do not allow relocations to refer to the "file" as in Elf.
instance Show RelocationError where
show RelocationZeroSymbol =
"A relocation entry referred to invalid 0 symbol index."
show (RelocationBadSymbolIndex idx) =
"A relocation entry referred to invalid symbol index " ++ show idx ++ "."
show (RelocationUnsupportedType tp) =
"Do not yet support relocation type " ++ tp ++ "."
show RelocationFileUnsupported =
"Do not support relocations referring to file entry."
data LoadError w
= LoadInsertError !String !(InsertError w)
-- ^ Error occurred in inserting a segment into memory.
@ -285,36 +295,22 @@ type ElfFileSectionMap v = IntervalMap v (ElfSection v)
-- | Map from symbol indices to the associated resolved symbol.
--
-- This drops the first symbol in Elf since that refers to no symbol
newtype SymbolVector = SymbolVector (V.Vector SymbolInfo)
newtype SymbolTable = SymbolTable (V.Vector SymbolInfo)
-- | Monad to use for reporting relocation failures.
type RelocResolver = Either RelocationError
relocError :: RelocationError -> RelocResolver a
relocError = Left
-- | A function that resolves the architecture-specific relocation-type
-- into a symbol reference. The input
type RelocationResolver tp
= SymbolVector
-> Elf.RelEntry tp
-> MemWord (Elf.RelocationWidth tp)
-- ^ Offset
-> RelocResolver (Relocation (Elf.RelocationWidth tp))
data SomeRelocationResolver w
= forall tp
. (Elf.IsRelocationType tp, w ~ Elf.RelocationWidth tp)
=> SomeRelocationResolver (RelocationResolver tp)
-- | Attempts to resolve a relocation entry into a specific target.
resolveSymbol :: SymbolVector
resolveSymbol :: SymbolTable
-- ^ A vector mapping symbol indices to the
-- associated symbol information.
-> Word32
-- ^ Offset of symbol
-> RelocResolver SymbolInfo
resolveSymbol (SymbolVector symtab) symIdx = do
resolveSymbol (SymbolTable symtab) symIdx = do
when (symIdx == 0) $
relocError RelocationZeroSymbol
case symtab V.!? fromIntegral (symIdx - 1) of
@ -322,9 +318,25 @@ resolveSymbol (SymbolVector symtab) symIdx = do
relocError $ RelocationBadSymbolIndex $ fromIntegral symIdx
Just sym -> pure sym
-- | A function that resolves the architecture-specific relocation-type
-- into a symbol reference. The input
type RelocationResolver tp
= Maybe SegmentIndex
-- ^ Index of segment index if this is a dynamic relocation.
-> SymbolTable
-> Elf.RelEntry tp
-> MemWord (Elf.RelocationWidth tp)
-- ^ Addend to add to symbol.
-> RelocResolver (Relocation (Elf.RelocationWidth tp))
data SomeRelocationResolver w
= forall tp
. (Elf.IsRelocationType tp, w ~ Elf.RelocationWidth tp)
=> SomeRelocationResolver (RelocationResolver tp)
-- | This attempts to resolve an index in the symbol table to the
-- identifier information needed to resolve its loaded address.
resolveRelocationSym :: SymbolVector
resolveRelocationSym :: SymbolTable
-- ^ A vector mapping symbol indices to the
-- associated symbol information.
-> Word32
@ -343,12 +355,13 @@ resolveRelocationSym symtab symIdx = do
pure $ SymbolRelocation (symbolName sym) (symbolVersion sym)
-- | Attempt to resolve an X86_64 specific symbol.
relaTargetX86_64 :: SymbolVector
relaTargetX86_64 :: Maybe SegmentIndex
-> SymbolTable
-> Elf.RelEntry Elf.X86_64_RelocationType
-> MemWord 64
-- ^ Offset of symbol
-- ^ Addend to add to symbol.
-> RelocResolver (Relocation 64)
relaTargetX86_64 symtab rel off =
relaTargetX86_64 _ symtab rel off =
case Elf.relType rel of
Elf.R_X86_64_JUMP_SLOT -> do
sym <- resolveRelocationSym symtab (Elf.relSym rel)
@ -416,30 +429,70 @@ relaTargetX86_64 symtab rel off =
tp -> relocError $ RelocationUnsupportedType (show tp)
-- | Attempt to resolve an X86_64 specific symbol.
relaTargetARM :: SymbolVector
-> Elf.RelEntry Elf.ARM_RelocationType
relaTargetARM :: Endianness
-- ^ Endianness of relocations
-> Maybe SegmentIndex
-- ^ Index of segment for dynamic relocations
-> SymbolTable -- ^ Symbol table
-> Elf.RelEntry Elf.ARM_RelocationType -- ^ Relocaiton entry
-> MemWord 32
-- ^ Offset of symbol
-- ^ Addend of symbol
-> RelocResolver (Relocation 32)
relaTargetARM _ rel _ =
relocError $ RelocationUnsupportedType (show (Elf.relType rel))
{-
This has been diabled until we get actual ARM support.
-- | Attempt to resolve an ARM specific symbol.
relaTargetARM :: SomeRelocationResolver 32
relaTargetARM = SomeRelocationResolver $ \_symtab rel _maddend ->
relaTargetARM end msegIndex symtab rel addend =
case Elf.relType rel of
-- Elf.R_ARM_GLOB_DAT -> do
-- checkZeroAddend rel
-- TargetSymbol <$> resolveSymbol symtab rel
-- Elf.R_ARM_COPY -> pure $ TargetCopy
-- Elf.R_ARM_JUMP_SLOT -> do
-- checkZeroAddend rel
-- TargetSymbol <$> resolveSymbol symtab rel
tp -> relocError $ RelocationUnsupportedType (show tp)
-}
Elf.R_ARM_GLOB_DAT -> do
sym <- resolveRelocationSym symtab (Elf.relSym rel)
-- Check that addend is 0 so that we do not change thumb bit of symbol
when (addend `testBit` 0) $ do
relocError $RelocationInvalidAddend (show (Elf.relType rel)) (toInteger addend)
pure $! Relocation { relocationSym = sym
, relocationOffset = addend
, relocationIsRel = False
, relocationSize = 4
, relocationIsSigned = False
, relocationEndianness = end
}
Elf.R_ARM_RELATIVE -> do
-- This relocation has the value B(S) + A where
-- - A is the addend for the relocation, and
-- - B(S) with S ≠ 0 resolves to the difference between the
-- address at which the segment defining the symbol S was
-- loaded and the address at which it was linked.
-- - B(S) with S = 0 resolves to the difference between the
-- address at which the segment being relocated was loaded
-- and the address at which it was linked.
--
-- Since the address at which it was linked is a constant, we
-- create a non-relative address but subtract the link address
-- from the offset.
-- Get the address at which it was linked so we can subtract from offset.
let linktimeAddr = Elf.relAddr rel
-- Resolve the symbol using the index in the relocation.
sym <-
if Elf.relSym rel == 0 then do
case msegIndex of
Nothing -> do
relocError $ RelocationZeroSymbol
Just idx ->
pure $! SegmentBaseAddr idx
else do
resolveRelocationSym symtab (Elf.relSym rel)
pure $! Relocation { relocationSym = sym
, relocationOffset = addend - fromIntegral linktimeAddr
, relocationIsRel = False
, relocationSize = 4
, relocationIsSigned = False
, relocationEndianness = end
}
tp -> do
relocError $ RelocationUnsupportedType (show tp)
toEndianness :: Elf.ElfData -> Endianness
toEndianness Elf.ELFDATA2LSB = LittleEndian
toEndianness Elf.ELFDATA2MSB = BigEndian
-- | Creates a relocation map from the contents of a dynamic section.
getRelocationResolver
@ -448,14 +501,13 @@ getRelocationResolver
-> MemLoader w (SomeRelocationResolver w)
getRelocationResolver hdr =
case (Elf.headerClass hdr, Elf.headerMachine hdr) of
(Elf.ELFCLASS64, Elf.EM_X86_64) -> pure (SomeRelocationResolver relaTargetX86_64)
(Elf.ELFCLASS32, Elf.EM_ARM) -> pure (SomeRelocationResolver relaTargetARM)
(Elf.ELFCLASS64, Elf.EM_X86_64) ->
pure $ SomeRelocationResolver relaTargetX86_64
(Elf.ELFCLASS32, Elf.EM_ARM) -> do
let end = toEndianness (Elf.headerData hdr)
pure $ SomeRelocationResolver $ relaTargetARM end
(_,mach) -> throwError $ UnsupportedArchitecture (show mach)
data RelocMap w v = RelocMap !(AddrOffsetMap w v) !(ResolveFn v (MemLoader w) w)
emptyRelocMap :: RelocMap w ()
emptyRelocMap = RelocMap Map.empty (\_ _ -> pure Nothing)
-- | This checks a computation that returns a dynamic error or succeeds.
runDynamic :: Either Elf.DynamicError a -> MemLoader w a
@ -468,88 +520,120 @@ resolveRela :: ( MemWidth w
, Elf.IsRelocationType tp
, Integral (Elf.ElfIntType w)
)
=> SymbolVector
=> SymbolTable
-> RelocationResolver tp
-> ResolveFn (Elf.RelaEntry tp) (MemLoader w) w
resolveRela symtab resolver rela _presym =
case resolver symtab (Elf.relaToRel rela) (fromIntegral (Elf.relaAddend rela)) of
-> Elf.RelaEntry tp
-> ResolveFn (MemLoader w) w
resolveRela symtab resolver rela msegIdx _ =
case resolver msegIdx symtab (Elf.relaToRel rela) (fromIntegral (Elf.relaAddend rela)) of
Left e -> do
addWarning (IgnoreRelocation e)
pure Nothing
Right r -> do
let tp = Elf.relaType rela
let cnt = Elf.relocTargetBits tp
pure $ Just (r, fromIntegral $ (cnt + 7) `shiftR` 3)
pure $ Just r
resolveRel :: ( MemWidth w
, Elf.RelocationWidth tp ~ w
, Elf.IsRelocationType tp
)
=> Endianness -- ^ Endianness of Elf file
-> SymbolVector
-> SymbolTable -- ^ Symbol table
-> RelocationResolver tp
-> ResolveFn (Elf.RelEntry tp) (MemLoader w) w
resolveRel end symtab resolver rel presym = do
-- Get the number of bytes being relocated.
let tp = Elf.relType rel
let bits = Elf.relocTargetBits tp
let cnt = (bits + 7) `shiftR` 3
-- Get the bytes that we will be overwriting.
case takePresymbolBytes (fromIntegral cnt) presym of
Nothing ->
pure Nothing
Just bytes -> do
-- Update the resolver.
let mask = (1 `shiftL` (bits - 1)) - 1
let uaddend = bytesToInteger end bytes .&. mask
let saddend | uaddend `testBit` (bits - 1) =
uaddend - (1 `shiftL` bits)
| otherwise =
uaddend
case resolver symtab rel (fromInteger saddend) of
Left e -> do
addWarning (IgnoreRelocation e)
pure Nothing
Right r -> do
pure $ Just (r, fromIntegral cnt)
-> Elf.RelEntry tp
-> ResolveFn (MemLoader w) w
resolveRel end symtab resolver rel msegIdx bytes = do
-- Get the number of bits in the addend
let bits = Elf.relocTargetBits (Elf.relType rel)
-- Compute the addended by masking off the low order bits, and
-- then sign extending them.
let mask = (1 `shiftL` (bits - 1)) - 1
let uaddend = bytesToInteger end bytes .&. mask
-- Convert uaddend as signed by looking at most-significant bit.
let saddend | uaddend `testBit` (bits - 1) =
uaddend - (1 `shiftL` bits)
| otherwise =
uaddend
-- Update the resolver.
case resolver msegIdx symtab rel (fromInteger saddend) of
Left e -> do
addWarning (IgnoreRelocation e)
pure Nothing
Right r -> do
pure $ Just r
relocTargetBytes :: (Elf.IsRelocationType tp, MemWidth (Elf.RelocationWidth tp))
=> tp
-> MemWord (Elf.RelocationWidth tp)
relocTargetBytes tp = fromIntegral $ (Elf.relocTargetBits tp + 7) `shiftR` 3
relocFromRela :: ( Elf.IsRelocationType tp
, w ~ Elf.RelocationWidth tp
, MemWidth w
, Integral (ElfIntType w)
, Integral (ElfWordType w)
)
=> SymbolTable
-> RelocationResolver tp
-> Elf.RelaEntry tp
-> (MemWord w, RelocEntry (MemLoader w) w)
relocFromRela symtab resolver r =
( fromIntegral (Elf.relaAddr r)
, RelocEntry { relocEntrySize = relocTargetBytes (Elf.relaType r)
, applyReloc = resolveRela symtab resolver r
}
)
relocFromRel :: ( Elf.IsRelocationType tp
, w ~ Elf.RelocationWidth tp
, MemWidth w
, Integral (ElfWordType w)
)
=> Endianness
-> SymbolTable
-> RelocationResolver tp
-> Elf.RelEntry tp
-> (MemWord w, RelocEntry (MemLoader w) w)
relocFromRel end symtab resolver r =
( fromIntegral (Elf.relAddr r)
, RelocEntry { relocEntrySize = relocTargetBytes (Elf.relType r)
, applyReloc = resolveRel end symtab resolver r
}
)
relocMapFromRelAndRela :: (Elf.IsRelocationType tp, w ~ Elf.RelocationWidth tp)
=> Elf.ElfData
-- ^ Endianness
-> RelocationResolver tp
-> SymbolTable
-- ^ Map from symbol indices to associated symbol
-> Maybe L.ByteString
-- ^ Buffer containing relocation entries in Rel format
-> Maybe L.ByteString
-- ^ Buffer containing relocation entries in Rela format
-> MemLoader w (Map (MemWord w) (RelocEntry (MemLoader w) w))
relocMapFromRelAndRela _dta _resolver _symtab Nothing Nothing = do
pure Map.empty
relocMapFromRelAndRela dta resolver symtab _ (Just relaBuffer) = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
case Elf.elfRelaEntries dta relaBuffer of
Left msg -> do
addWarning (RelocationParseFailure msg)
pure Map.empty
Right entries -> do
pure $ Map.fromList $ relocFromRela symtab resolver <$> entries
relocMapFromRelAndRela dta resolver symtab (Just relBuffer) Nothing = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
case Elf.elfRelEntries dta relBuffer of
Left msg -> do
addWarning (RelocationParseFailure msg)
pure Map.empty
Right entries -> do
pure $ Map.fromList $ relocFromRel (toEndianness dta) symtab resolver <$> entries
mkRelocMap :: Elf.ElfData
-> Elf.ElfHeader w
-- ^ format for Elf file
-> SymbolVector
-- ^ Map from symbol indices to associated symbol
-> Maybe L.ByteString
-- ^ Buffer containing relocation entries in Rel format
-> Maybe L.ByteString
-- ^ Buffer containing relocation entries in Rela format
-> MemLoader w (Some (RelocMap w))
mkRelocMap _dta _hdr _symtab Nothing Nothing = do
pure $! Some emptyRelocMap
mkRelocMap dta hdr symtab _mrelBuffer (Just relaBuffer) = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
SomeRelocationResolver resolver <- getRelocationResolver hdr
case Elf.elfRelaEntries dta relaBuffer of
Left msg -> do
addWarning (RelocationParseFailure msg)
pure $ Some emptyRelocMap
Right relocs -> do
-- Create the relocation map using the above information
let m = Map.fromList [ (fromIntegral (Elf.relaOffset r), r) | r <- relocs ]
pure $ Some $ RelocMap m (resolveRela symtab resolver)
mkRelocMap dta hdr symtab (Just relBuffer) Nothing = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
SomeRelocationResolver resolver <- getRelocationResolver hdr
case Elf.elfRelEntries dta relBuffer of
Left msg -> do
addWarning (RelocationParseFailure msg)
pure $ Some emptyRelocMap
Right relocs -> do
-- Create the relocation map using the above information
let m = Map.fromList [ (fromIntegral (Elf.relOffset r), r) | r <- relocs ]
end <- gets mlsEndianness
pure $ Some $ RelocMap m (resolveRel end symtab resolver)
resolveUndefinedSymbolReq :: SymbolName
-> Elf.ElfSymbolBinding
@ -674,10 +758,10 @@ mkDynamicSymbolRef (sym, mverId) = do
dynamicRelocationMap :: Elf.ElfHeader w
-> [Elf.Phdr w]
-> L.ByteString
-> MemLoader w (Some (RelocMap w))
-> MemLoader w (Map (MemWord w) (RelocEntry (MemLoader w) w))
dynamicRelocationMap hdr ph contents =
case filter (\p -> Elf.phdrSegmentType p == Elf.PT_DYNAMIC) ph of
[] -> pure $ Some emptyRelocMap
[] -> pure $ Map.empty
dynPhdr:dynRest -> do
when (not (null dynRest)) $
addWarning MultipleDynamicSegments
@ -686,7 +770,7 @@ dynamicRelocationMap hdr ph contents =
case Elf.virtAddrMap contents ph of
Nothing -> do
addWarning OverlappingLoadableSegments
pure $! Some emptyRelocMap
pure Map.empty
Just virtMap -> do
let dynContents = sliceL (Elf.phdrFileRange dynPhdr) contents
-- Find th dynamic section from the contents.
@ -694,12 +778,27 @@ dynamicRelocationMap hdr ph contents =
Elf.dynamicEntries (Elf.headerData hdr) (Elf.headerClass hdr) virtMap dynContents
symentries <- runDynamic (Elf.dynSymTable dynSection)
symtab <-
SymbolVector <$> traverse mkDynamicSymbolRef (V.drop 1 symentries)
SymbolTable <$> traverse mkDynamicSymbolRef (V.drop 1 symentries)
mRelBuffer <- runDynamic $ Elf.dynRelBuffer dynSection
mRelaBuffer <- runDynamic $ Elf.dynRelaBuffer dynSection
when (isJust mRelBuffer && isJust mRelaBuffer) $
addWarning DynamicRelaAndRelPresent
mkRelocMap (Elf.headerData hdr) hdr symtab mRelBuffer mRelaBuffer
SomeRelocationResolver resolver <- getRelocationResolver hdr
when (isJust mRelBuffer && isJust mRelaBuffer) $ do
addWarning $ DynamicRelaAndRelPresent
let dta = Elf.headerData hdr
loadtimeRelocs <-
relocMapFromRelAndRela dta resolver symtab mRelBuffer mRelaBuffer
pltRelocs <-
case Elf.dynPLTRel dynSection of
Left e -> do
addWarning $ RelocationParseFailure (show e)
pure $! Map.empty
Right Elf.PLTEmpty -> do
pure $! Map.empty
Right (Elf.PLTRel entries) -> do
pure $! Map.fromList $ relocFromRel (toEndianness dta) symtab resolver <$> entries
Right (Elf.PLTRela entries) -> do
pure $! Map.fromList $ relocFromRela symtab resolver <$> entries
pure $ Map.union loadtimeRelocs pltRelocs
------------------------------------------------------------------------
-- Elf segment loading
@ -714,45 +813,70 @@ reprConstraints :: AddrWidthRepr w
reprConstraints Addr32 x = x
reprConstraints Addr64 x = x
-- let f r contents = pure $ Just (r, relocSize r)
-- | Return a memory segment for elf segment if it loadable.
memSegmentForElfSegment :: (MemWidth w, Monad m, Integral (ElfWordType w))
=> ResolveFn v m w
-> MemAddr w
-- ^ Base address to use for segments.
-> L.ByteString
-- ^ Complete contents of Elf file.
-> AddrOffsetMap w v
-- ^ Relocation map
-> Elf.Phdr w
-- ^ Program header entry
-> m (MemSegment w)
memSegmentForElfSegment resolver base contents relocMap phdr =
memSegment resolver (addrBase base) relocMap off flags dta sz
where off = addrOffset base + fromIntegral (Elf.phdrSegmentVirtAddr phdr)
dta = sliceL (Elf.phdrFileRange phdr) contents
sz = fromIntegral $ Elf.phdrMemSize phdr
flags = flagsForSegmentFlags (Elf.phdrSegmentFlags phdr)
-- | This creates a memory segment.
memSegment :: forall m w
. (Monad m, MemWidth w)
=> Map (MemWord w) (RelocEntry m w)
-- ^ Map from region offset to relocation entry for segment.
-> RegionIndex
-- ^ Index of base (0=absolute address)
-> Integer
-- ^ Offset to add to linktime address for this segment (defaults to 0)
-> Maybe SegmentIndex
-- ^ Identifier for this segment in relocation if this is created from so/exe.
-> MemWord w
-- ^ Linktime address of segment.
-> Perm.Flags
-- ^ Flags if defined
-> L.ByteString
-- ^ File contents for segment.
-> Int64
-- ^ Expected size (must be positive)
-> m (MemSegment w)
memSegment relocMap regionIndex regionOff msegIdx linkBaseOff flags bytes sz
-- Return nothing if size is not positive
| not (sz > 0) = error $ "Memory segments must have a positive size."
-- Check for overflow in contents end
| regionOff + toInteger linkBaseOff + toInteger sz > toInteger (maxBound :: MemWord w) =
error "Contents two large for base."
| otherwise = do
contents <- byteSegments relocMap msegIdx linkBaseOff bytes sz
pure $
MemSegment { segmentBase = regionIndex
, segmentOffset = fromInteger regionOff + linkBaseOff
, segmentFlags = flags
, segmentContents = contentsFromList contents
}
-- | Load an elf file into memory.
insertElfSegment :: MemAddr w
-- ^ Base address to use for loading program header.
insertElfSegment :: RegionIndex
-- ^ Region for elf segment
-> Integer
-- ^ Amount to add to linktime virtual address for thsi memory.
-> ElfFileSectionMap (ElfWordType w)
-> L.ByteString
-> RelocMap w v
-- ^ Relocations to apply in loading section.
-> Map (MemWord w) (RelocEntry (MemLoader w) w)
-- ^ Relocations to apply when inserting segment.
-> Elf.Phdr w
-> MemLoader w ()
insertElfSegment base shdrMap contents (RelocMap relocMap resolver) phdr = do
insertElfSegment regIdx addrOff shdrMap contents relocMap phdr = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
when (Elf.phdrMemSize phdr > 0) $ do
seg <- memSegmentForElfSegment resolver base contents relocMap phdr
let seg_idx = Elf.phdrSegmentIndex phdr
loadMemSegment ("Segment " ++ show seg_idx) seg
let segIdx = Elf.phdrSegmentIndex phdr
seg <- do
let linkBaseOff = fromIntegral (Elf.phdrSegmentVirtAddr phdr)
let flags = flagsForSegmentFlags (Elf.phdrSegmentFlags phdr)
let dta = sliceL (Elf.phdrFileRange phdr) contents
let sz = fromIntegral $ Elf.phdrMemSize phdr
memSegment relocMap regIdx addrOff (Just segIdx) linkBaseOff flags dta sz
loadMemSegment ("Segment " ++ show segIdx) seg
let phdr_offset = Elf.fromFileOffset (Elf.phdrFileStart phdr)
let phdr_end = phdr_offset + Elf.phdrFileSize phdr
-- Add segment index to address mapping to memory object.
do let Just segAddr = resolveSegmentOff seg 0
mlsMemory %= memAddSegmentAddr segIdx segAddr
-- Iterative through sections
let l = IMap.toList $ IMap.intersecting shdrMap (IntervalCO phdr_offset phdr_end)
forM_ l $ \(i, sec) -> do
case i of
@ -769,12 +893,15 @@ insertElfSegment base shdrMap contents (RelocMap relocMap resolver) phdr = do
-- | Load an elf file into memory by parsing segments.
memoryForElfSegments
:: forall w
. MemAddr w
. RegionIndex
-- ^ This is used as the base address to load Elf segments at (the virtual
-- address is treated as relative to this.
-> Integer
-- ^ This is used as the base address to load Elf segments at (the virtual
-- address is treated as relative to this.
-> Elf w
-> MemLoader w ()
memoryForElfSegments base e = do
memoryForElfSegments regIndex addrOff e = do
let l = elfLayout e
let hdr = Elf.elfLayoutHeader l
let w = elfAddrWidth (elfClass e)
@ -782,8 +909,7 @@ memoryForElfSegments base e = do
let ph = Elf.allPhdrs l
let contents = elfLayoutBytes l
-- Create relocation map
Some relocMap <-
dynamicRelocationMap hdr ph contents
relocMap <- dynamicRelocationMap hdr ph contents
let intervals :: ElfFileSectionMap (ElfWordType w)
intervals = IMap.fromList
@ -793,7 +919,7 @@ memoryForElfSegments base e = do
, let sec = shdr^._1
, let end = start + elfSectionFileSize sec
]
mapM_ (insertElfSegment base intervals contents relocMap)
mapM_ (insertElfSegment regIndex addrOff intervals contents relocMap)
(filter (\p -> Elf.phdrSegmentType p == Elf.PT_LOAD) ph)
------------------------------------------------------------------------
@ -846,8 +972,9 @@ findSection sectionMap nm =
addWarning $ MultipleSectionsWithName nm
pure (Just sec)
-- | Add a section to the current memory
insertAllocatedSection :: Elf.ElfHeader w
-> SymbolVector
-> SymbolTable
-> SectionNameMap w
-> RegionIndex
-> SectionName
@ -865,7 +992,7 @@ insertAllocatedSection hdr symtab sectionMap regIdx nm = do
findSection sectionMap (".rela" <> nm)
-- Build relocation map
-- Get size of section
let secSize = fromIntegral (Elf.elfSectionSize sec)
let secSize = Elf.elfSectionSize sec
-- Check if we should load section
when (not (elfSectionFlags sec `Elf.hasPermissions` Elf.shf_alloc)) $ do
addWarning $ SectionNotAlloc nm
@ -877,12 +1004,13 @@ insertAllocatedSection hdr symtab sectionMap regIdx nm = do
-- Get bytes as a lazy bytesize
let bytes = L.fromStrict (elfSectionData sec)
-- Create memory segment
SomeRelocationResolver resolver <- getRelocationResolver hdr
when (isJust mRelBuffer && isJust mRelaBuffer) $ do
addWarning $ DuplicateRelocationSections nm
Some (RelocMap relocMap resolver) <-
mkRelocMap (Elf.headerData hdr) hdr symtab mRelBuffer mRelaBuffer
addWarning $ SectionRelaAndRelPresent nm
relocMap <-
relocMapFromRelAndRela (Elf.headerData hdr) resolver symtab mRelBuffer mRelaBuffer
seg <-
memSegment resolver regIdx relocMap (fromIntegral base) flags bytes secSize
memSegment relocMap regIdx 0 Nothing (fromIntegral base) flags bytes (fromIntegral secSize)
-- Load memory segment.
loadMemSegment ("Section " ++ BSC.unpack (elfSectionName sec)) seg
-- Add entry to map elf section index to start in segment.
@ -892,17 +1020,17 @@ insertAllocatedSection hdr symtab sectionMap regIdx nm = do
mlsIndexMap %= Map.insert elfIdx (addr, sec)
-- | Create the symbol vector from
symtabSymbolVector :: forall w . Elf w -> MemLoader w SymbolVector
symtabSymbolVector e =
symtabSymbolTable :: forall w . Elf w -> MemLoader w SymbolTable
symtabSymbolTable e =
case Elf.elfSymtab e of
[] ->
pure $ SymbolVector V.empty
pure $ SymbolTable V.empty
elfSymTab:_rest -> do
-- when (not (null rest)) $ addWarning $ MultipleSymbolTables
let entries = Elf.elfSymbolTableEntries elfSymTab
-- let lclCnt = fromIntegral $ Elf.elfSymbolTableLocalEntries elfSymTab
-- Create an unversioned symbol from symbol table.
SymbolVector <$> traverse (`mkSymbolRef` ObjectSymbol) (V.drop 1 entries)
SymbolTable <$> traverse (`mkSymbolRef` ObjectSymbol) (V.drop 1 entries)
-- | Load allocated Elf sections into memory.
--
@ -917,8 +1045,8 @@ memoryForElfSections e = do
let sectionMap :: SectionNameMap w
sectionMap = foldlOf elfSections insSec Map.empty e
where insSec m sec = Map.insertWith (\new old -> old ++ new) (elfSectionName sec) [sec] m
symtab <- symtabSymbolVector e
forM_ (zip [1..] allocatedSectionInfo) $ \(idx, (nm,_)) ->
symtab <- symtabSymbolTable e
forM_ (zip [1..] allocatedSectionInfo) $ \(idx, (nm,_)) -> do
insertAllocatedSection hdr symtab sectionMap idx nm
-- TODO: Figure out what to do about .tdata and .tbss
-- Check for other section names that we do not support."
@ -957,19 +1085,16 @@ memoryForElf' :: ( Memory w
, [SymbolResolutionError]
)
memoryForElf' resolver opt e = reprConstraints (elfAddrWidth (elfClass e)) $ do
let end = case Elf.elfData e of
Elf.ELFDATA2LSB -> LittleEndian
Elf.ELFDATA2MSB -> BigEndian
let end = toEndianness (Elf.elfData e)
(secMap, mem, warnings) <-
runMemLoader end (emptyMemory (elfAddrWidth (elfClass e))) $
case Elf.elfType e of
Elf.ET_REL ->
memoryForElfSections e
_ -> do
let base = MemAddr { addrBase = adjustedLoadRegionIndex e opt
, addrOffset = fromInteger (loadRegionBaseOffset opt)
}
memoryForElfSegments base e
let regIdx = adjustedLoadRegionIndex e opt
let addrOff = loadRegionBaseOffset opt
memoryForElfSegments regIdx addrOff e
let (symErrs, funcSymbols) = resolver mem secMap e
pure (mem, funcSymbols, warnings, symErrs)

247
base/src/Data/Macaw/Types.hs
View File

@ -6,15 +6,20 @@ The type of machine words, including bit vectors and floating point
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.Types
@ -27,8 +32,10 @@ module Data.Macaw.Types
import Data.Parameterized.Classes
import qualified Data.Parameterized.List as P
import Data.Parameterized.NatRepr
import Data.Parameterized.TH.GADT
import Data.Parameterized.TraversableFC
import GHC.TypeLits
import qualified Language.Haskell.TH.Syntax as TH
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
-- FIXME: move
@ -68,16 +75,8 @@ n256 = knownNat
data Type
= -- | A bitvector with the given number of bits.
BVType Nat
-- | 64 bit binary IEE754
| DoubleFloat
-- | 32 bit binary IEE754
| SingleFloat
-- | X86 80-bit extended floats
| X86_80Float
-- | 128 bit binary IEE754
| QuadFloat
-- | 16 bit binary IEE754
| HalfFloat
-- | A floating point in the given format.
| FloatType FloatInfo
-- | A Boolean value
| BoolType
-- | A tuple of types
@ -86,29 +85,21 @@ data Type
-- Return number of bytes in the type.
type family TypeBytes (tp :: Type) :: Nat where
TypeBytes (BVType 8) = 1
TypeBytes (BVType 16) = 2
TypeBytes (BVType 32) = 4
TypeBytes (BVType 64) = 8
TypeBytes HalfFloat = 2
TypeBytes SingleFloat = 4
TypeBytes DoubleFloat = 8
TypeBytes QuadFloat = 16
TypeBytes X86_80Float = 10
TypeBytes (BVType 8) = 1
TypeBytes (BVType 16) = 2
TypeBytes (BVType 32) = 4
TypeBytes (BVType 64) = 8
TypeBytes (FloatType fi) = FloatInfoBytes fi
-- Return number of bits in the type.
type family TypeBits (tp :: Type) :: Nat where
TypeBits (BVType n) = n
TypeBits HalfFloat = 16
TypeBits SingleFloat = 32
TypeBits DoubleFloat = 64
TypeBits QuadFloat = 128
TypeBits X86_80Float = 80
type FloatType tp = BVType (8 * TypeBytes tp)
TypeBits (BVType n) = n
TypeBits (FloatType fi) = 8 * FloatInfoBytes fi
type BVType = 'BVType
type FloatType = 'FloatType
type BoolType = 'BoolType
type TupleType = 'TupleType
@ -117,33 +108,16 @@ type TupleType = 'TupleType
data TypeRepr (tp :: Type) where
BoolTypeRepr :: TypeRepr BoolType
BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
type_width :: TypeRepr (BVType n) -> NatRepr n
type_width (BVTypeRepr n) = n
instance TestEquality TypeRepr where
testEquality BoolTypeRepr BoolTypeRepr = do
return Refl
testEquality (BVTypeRepr m) (BVTypeRepr n) = do
Refl <- testEquality m n
return Refl
testEquality _ _ = Nothing
instance OrdF TypeRepr where
compareF BoolTypeRepr BoolTypeRepr = EQF
compareF BoolTypeRepr _ = LTF
compareF _ BoolTypeRepr = GTF
compareF (BVTypeRepr m) (BVTypeRepr n) = do
lexCompareF m n EQF
compareF BVTypeRepr{} _ = LTF
compareF _ BVTypeRepr{} = GTF
compareF (TupleTypeRepr x) (TupleTypeRepr y) =
lexCompareF x y EQF
instance Show (TypeRepr tp) where
show BoolTypeRepr = "bool"
show (BVTypeRepr w) = "[" ++ show w ++ "]"
show (FloatTypeRepr fi) = show fi ++ "_float"
show (TupleTypeRepr P.Nil) = "()"
show (TupleTypeRepr (h P.:< z)) =
"(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
@ -154,96 +128,123 @@ instance KnownRepr TypeRepr BoolType where
instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
knownRepr = BVTypeRepr knownNat
instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
knownRepr = FloatTypeRepr knownRepr
instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr (TupleType l) where
knownRepr = TupleTypeRepr knownRepr
------------------------------------------------------------------------
-- Floating point sizes
data FloatInfo
= HalfFloat -- ^ 16 bit binary IEE754
| SingleFloat -- ^ 32 bit binary IEE754
| DoubleFloat -- ^ 64 bit binary IEE754
| QuadFloat -- ^ 128 bit binary IEE754
| X86_80Float -- ^ X86 80-bit extended floats
type HalfFloat = 'HalfFloat
type SingleFloat = 'SingleFloat
type DoubleFloat = 'DoubleFloat
type X86_80Float = 'X86_80Float
type QuadFloat = 'QuadFloat
type HalfFloat = 'HalfFloat
type X86_80Float = 'X86_80Float
data FloatInfoRepr (flt::Type) where
DoubleFloatRepr :: FloatInfoRepr DoubleFloat
SingleFloatRepr :: FloatInfoRepr SingleFloat
X86_80FloatRepr :: FloatInfoRepr X86_80Float
QuadFloatRepr :: FloatInfoRepr QuadFloat
data FloatInfoRepr (fi :: FloatInfo) where
HalfFloatRepr :: FloatInfoRepr HalfFloat
SingleFloatRepr :: FloatInfoRepr SingleFloat
DoubleFloatRepr :: FloatInfoRepr DoubleFloat
QuadFloatRepr :: FloatInfoRepr QuadFloat
X86_80FloatRepr :: FloatInfoRepr X86_80Float
deriving instance Show (FloatInfoRepr tp)
instance KnownRepr FloatInfoRepr HalfFloat where
knownRepr = HalfFloatRepr
instance KnownRepr FloatInfoRepr SingleFloat where
knownRepr = SingleFloatRepr
instance KnownRepr FloatInfoRepr DoubleFloat where
knownRepr = DoubleFloatRepr
instance KnownRepr FloatInfoRepr QuadFloat where
knownRepr = QuadFloatRepr
instance KnownRepr FloatInfoRepr X86_80Float where
knownRepr = X86_80FloatRepr
instance Show (FloatInfoRepr fi) where
show HalfFloatRepr = "half"
show SingleFloatRepr = "single"
show DoubleFloatRepr = "double"
show QuadFloatRepr = "quad"
show X86_80FloatRepr = "x87_80"
instance Pretty (FloatInfoRepr fi) where
pretty = text . show
deriving instance TH.Lift (FloatInfoRepr fi)
type family FloatInfoBytes (fi :: FloatInfo) :: Nat where
FloatInfoBytes HalfFloat = 2
FloatInfoBytes SingleFloat = 4
FloatInfoBytes DoubleFloat = 8
FloatInfoBytes QuadFloat = 16
FloatInfoBytes X86_80Float = 10
floatInfoBytes :: FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
floatInfoBytes = \case
HalfFloatRepr -> knownNat
SingleFloatRepr -> knownNat
DoubleFloatRepr -> knownNat
QuadFloatRepr -> knownNat
X86_80FloatRepr -> knownNat
floatInfoBytesIsPos :: FloatInfoRepr fi -> LeqProof 1 (FloatInfoBytes fi)
floatInfoBytesIsPos = \case
HalfFloatRepr -> LeqProof
SingleFloatRepr -> LeqProof
DoubleFloatRepr -> LeqProof
QuadFloatRepr -> LeqProof
X86_80FloatRepr -> LeqProof
type FloatInfoBits (fi :: FloatInfo) = 8 * FloatInfoBytes fi
floatInfoBits :: FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBits = natMultiply (knownNat @8) . floatInfoBytes
floatInfoBitsIsPos :: FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
floatInfoBitsIsPos = \case
HalfFloatRepr -> LeqProof
SingleFloatRepr -> LeqProof
DoubleFloatRepr -> LeqProof
QuadFloatRepr -> LeqProof
X86_80FloatRepr -> LeqProof
-- | The bitvector associted with the given floating-point format.
type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi)
floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
floatBVTypeRepr fi | LeqProof <- floatInfoBitsIsPos fi =
BVTypeRepr $ floatInfoBits fi
$(return [])
instance TestEquality TypeRepr where
testEquality = $(structuralTypeEquality [t|TypeRepr|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
, ( ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType
, [|testEquality|]
)
])
instance OrdF TypeRepr where
compareF = $(structuralTypeOrd [t|TypeRepr|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType, [|compareF|])
])
instance TestEquality FloatInfoRepr where
testEquality x y = orderingF_refl (compareF x y)
testEquality = $(structuralTypeEquality [t|FloatInfoRepr|] [])
instance OrdF FloatInfoRepr where
compareF DoubleFloatRepr DoubleFloatRepr = EQF
compareF DoubleFloatRepr _ = LTF
compareF _ DoubleFloatRepr = GTF
compareF SingleFloatRepr SingleFloatRepr = EQF
compareF SingleFloatRepr _ = LTF
compareF _ SingleFloatRepr = GTF
compareF X86_80FloatRepr X86_80FloatRepr = EQF
compareF X86_80FloatRepr _ = LTF
compareF _ X86_80FloatRepr = GTF
compareF QuadFloatRepr QuadFloatRepr = EQF
compareF QuadFloatRepr _ = LTF
compareF _ QuadFloatRepr = GTF
compareF HalfFloatRepr HalfFloatRepr = EQF
instance Pretty (FloatInfoRepr flt) where
pretty DoubleFloatRepr = text "double"
pretty SingleFloatRepr = text "single"
pretty X86_80FloatRepr = text "x87_80"
pretty QuadFloatRepr = text "quad"
pretty HalfFloatRepr = text "half"
floatInfoBytes :: FloatInfoRepr flt -> NatRepr (TypeBytes flt)
floatInfoBytes fir =
case fir of
HalfFloatRepr -> knownNat
SingleFloatRepr -> knownNat
DoubleFloatRepr -> knownNat
QuadFloatRepr -> knownNat
X86_80FloatRepr -> knownNat
floatInfoBytesIsPos :: FloatInfoRepr flt -> LeqProof 1 (TypeBytes flt)
floatInfoBytesIsPos fir =
case fir of
HalfFloatRepr -> LeqProof
SingleFloatRepr -> LeqProof
DoubleFloatRepr -> LeqProof
QuadFloatRepr -> LeqProof
X86_80FloatRepr -> LeqProof
floatInfoBits :: FloatInfoRepr flt -> NatRepr (8 * TypeBytes flt)
floatInfoBits fir = natMultiply (knownNat :: NatRepr 8) (floatInfoBytes fir)
floatTypeRepr :: FloatInfoRepr flt -> TypeRepr (BVType (8 * TypeBytes flt))
floatTypeRepr fir =
case fir of
HalfFloatRepr -> knownRepr
SingleFloatRepr -> knownRepr
DoubleFloatRepr -> knownRepr
QuadFloatRepr -> knownRepr
X86_80FloatRepr -> knownRepr
floatInfoBitsIsPos :: FloatInfoRepr flt -> LeqProof 1 (8 * TypeBytes flt)
floatInfoBitsIsPos fir =
case fir of
HalfFloatRepr -> LeqProof
SingleFloatRepr -> LeqProof
DoubleFloatRepr -> LeqProof
QuadFloatRepr -> LeqProof
X86_80FloatRepr -> LeqProof
compareF = $(structuralTypeOrd [t|FloatInfoRepr|] [])
------------------------------------------------------------------------
--

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit df334c354b4208e5f7a43149569442f5536084b4
Subproject commit 459ae2a3dfc033eb7f8129f3068859e73dc40cb3

2
deps/elf-edit vendored

@ -1 +1 @@
Subproject commit 78ca989cb31058968c5dc4e01009ee705eaeea09
Subproject commit afa3dcf45afc5429139cae09f8584a722a737946

2
deps/flexdis86 vendored

@ -1 +1 @@
Subproject commit 71c367e2269f84dcdfda21612288109312ba3fc6
Subproject commit e53a3359b51ad1a91758144a85d8a8eb635d91d9

2
deps/llvm-pretty vendored

@ -1 +1 @@
Subproject commit d2fb5fc1e6bf0f40a8a55a63672970cdbc6070b6
Subproject commit 6cc6990017c4d875311a52a6d3988fb7a962ed7a

2
deps/parameterized-utils vendored

@ -1 +1 @@
Subproject commit a30e12292371bc9abe6ccc631a0409df059449d9
Subproject commit fa6085733f507d07c7c417d238e1a6c575944680

134
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -21,11 +21,14 @@ module Data.Macaw.Symbolic
, macawExtensions
, runCodeBlock
-- , runBlocks
, mkBlocksCFG
, mkParsedBlockCFG
, mkFunCFG
, mkBlocksCFG, mkBlocksRegCFG
, mkParsedBlockCFG, mkParsedBlockRegCFG
, mkFunCFG, mkFunRegCFG
, toCoreCFG
, Data.Macaw.Symbolic.PersistentState.ArchRegContext
, Data.Macaw.Symbolic.PersistentState.ToCrucibleType
, Data.Macaw.Symbolic.PersistentState.ToCrucibleFloatInfo
, Data.Macaw.Symbolic.PersistentState.floatInfoToCrucible
, Data.Macaw.Symbolic.PersistentState.macawAssignToCrucM
, Data.Macaw.Symbolic.CrucGen.ArchRegStruct
, Data.Macaw.Symbolic.CrucGen.MacawCrucibleRegTypes
@ -52,6 +55,7 @@ import Data.Parameterized.Context as Ctx
import Data.Word
import qualified What4.FunctionName as C
import What4.InterpretedFloatingPoint
import What4.Interface
import qualified What4.ProgramLoc as C
import What4.Symbol (userSymbol)
@ -108,8 +112,12 @@ mkMemBaseVarMap halloc mem = do
Map.fromList <$> traverse (mkMemSegmentBinding halloc (M.memWidth mem)) (Set.toList baseIndices)
-}
-- | Create a Crucible CFG from a list of blocks
mkCrucCFG :: forall s arch ids
-- | Create a Crucible registerized CFG from a list of blocks
--
-- Useful as an alternative to 'mkCrucCFG' if post-processing is
-- desired (as this is easier to do with the registerized form); use
-- 'toCoreCFG' to finish.
mkCrucRegCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Crucible architecture-specific functions.
-> C.HandleAllocator s
@ -118,8 +126,8 @@ mkCrucCFG :: forall s arch ids
-- ^ Name of function for pretty print purposes.
-> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
-- ^ Action to run
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkCrucCFG archFns halloc nm action = do
-> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkCrucRegCFG archFns halloc nm action = do
let crucRegTypes = crucArchRegTypes archFns
let macawStructRepr = C.StructRepr crucRegTypes
let argTypes = Empty :> macawStructRepr
@ -137,8 +145,20 @@ mkCrucCFG archFns halloc nm action = do
, CR.cfgNextValue = valueCount finalSt
, CR.cfgNextLabel = length blks
}
crucGenArchConstraints archFns $
pure $ C.toSSA rg
pure $ CR.SomeCFG rg
where
-- Unlike valueCount, we don't keep this handy, so just compute it
nextLabel blks = 1 + maximum (map (blockIDInt . CR.blockID) blks)
blockIDInt (CR.LabelID l) = CR.labelInt l
blockIDInt (CR.LambdaID l) = CR.lambdaInt l
-- | Generate the final SSA CFG from a registerized CFG. Offered
-- separately in case post-processing on the registerized CFG is
-- desired.
toCoreCFG :: MacawSymbolicArchFunctions arch
-> CR.SomeCFG (MacawExt arch) init ret
-> C.SomeCFG (MacawExt arch) init ret
toCoreCFG archFns (CR.SomeCFG cfg) = crucGenArchConstraints archFns $ C.toSSA cfg
-- | Create a Crucible CFG from a list of blocks
addBlocksCFG :: forall s arch ids
@ -160,6 +180,25 @@ addBlocksCFG archFns baseAddrMap posFn macawBlocks = do
forM macawBlocks $ \b -> do
addMacawBlock archFns baseAddrMap blockLabelMap posFn b
-- | Create a registerized Crucible CFG from a list of blocks
mkBlocksRegCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Crucible specific functions.
-> C.HandleAllocator s
-- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> (M.ArchAddrWord arch -> C.Position)
-- ^ Function that maps offsets from start of block to Crucible position.
-> [M.Block arch ids]
-- ^ List of blocks for this region.
-> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkBlocksRegCFG archFns halloc memBaseVarMap nm posFn macawBlocks = do
mkCrucRegCFG archFns halloc nm $ do
addBlocksCFG archFns memBaseVarMap posFn macawBlocks
-- | Create a Crucible CFG from a list of blocks
mkBlocksCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
@ -175,9 +214,9 @@ mkBlocksCFG :: forall s arch ids
-> [M.Block arch ids]
-- ^ List of blocks for this region.
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks = do
mkCrucCFG archFns halloc nm $ do
addBlocksCFG archFns memBaseVarMap posFn macawBlocks
mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks =
toCoreCFG archFns <$>
mkBlocksRegCFG archFns halloc memBaseVarMap nm posFn macawBlocks
-- | Create a map from Macaw @(address, index)@ pairs to Crucible labels
mkBlockLabelMap :: [M.ParsedBlock arch ids] -> BlockLabelMap arch s
@ -219,9 +258,14 @@ termStmtToReturn sl = sl { M.stmtsTerm = tm }
M.ParsedIte b l r -> M.ParsedIte b (termStmtToReturn l) (termStmtToReturn r)
tm0 -> tm0
-- | This create a Crucible CFG from a Macaw block. Note that the
-- term statement of the block is updated to make it a return.
mkParsedBlockCFG :: forall s arch ids
-- | This create a registerized Crucible CFG from a Macaw block. Note
-- that the term statement of the block is updated to make it a
-- return.
--
-- Useful as an alternative to 'mkParsedBlockCFG' if post-processing
-- is desired (as this is easier on the registerized form). Use
-- 'toCoreCFG' to finish by translating the registerized CFG to SSA.
mkParsedBlockRegCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions.
-> C.HandleAllocator s
@ -232,9 +276,9 @@ mkParsedBlockCFG :: forall s arch ids
-- ^ Function that maps function address to Crucible position
-> M.ParsedBlock arch ids
-- ^ Block to translate
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkParsedBlockCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints archFns $ do
mkCrucCFG archFns halloc "" $ do
-> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints archFns $ do
mkCrucRegCFG archFns halloc "" $ do
let strippedBlock = b { M.blockStatementList = termStmtToReturn (M.blockStatementList b) }
let entryAddr = M.pblockAddr strippedBlock
@ -278,8 +322,30 @@ mkParsedBlockCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints a
-- Return initialization block followed by actual blocks.
pure (initCrucibleBlock : crucibleBlock)
-- | This create a Crucible CFG from a Macaw `DiscoveryFunInfo` value.
mkFunCFG :: forall s arch ids
-- | This create a Crucible CFG from a Macaw block. Note that the
-- term statement of the block is updated to make it a return.
mkParsedBlockCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions.
-> C.HandleAllocator s
-- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address
-> (M.ArchSegmentOff arch -> C.Position)
-- ^ Function that maps function address to Crucible position
-> M.ParsedBlock arch ids
-- ^ Block to translate
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkParsedBlockCFG archFns halloc memBaseVarMap posFn b =
toCoreCFG archFns <$> mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b
-- | This create a registerized Crucible CFG from a Macaw
-- `DiscoveryFunInfo` value.
--
-- Useful as an alternative to 'mkFunCFG' if post-processing
-- is desired (as this is easier on the registerized form). Use
-- 'toCoreCFG' to finish by translating the registerized CFG to SSA.
mkFunRegCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions.
-> C.HandleAllocator s
@ -292,9 +358,9 @@ mkFunCFG :: forall s arch ids
-- ^ Function that maps function address to Crucible position
-> M.DiscoveryFunInfo arch ids
-- ^ List of blocks for this region.
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkFunCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints archFns $ do
mkCrucCFG archFns halloc nm $ do
-> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints archFns $ do
mkCrucRegCFG archFns halloc nm $ do
-- Get entry point address for function
let entryAddr = M.discoveredFunAddr fn
-- Get list of blocks
@ -332,6 +398,24 @@ mkFunCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints archF
-- Return initialization block followed by actual blocks.
pure (initCrucibleBlock : concat restCrucibleBlocks)
-- | This create a Crucible CFG from a Macaw `DiscoveryFunInfo` value.
mkFunCFG :: forall s arch ids
. MacawSymbolicArchFunctions arch
-- ^ Architecture specific functions.
-> C.HandleAllocator s
-- ^ Handle allocator to make the blocks
-> MemSegmentMap (M.ArchAddrWidth arch)
-- ^ Map from region indices to their address
-> C.FunctionName
-- ^ Name of function for pretty print purposes.
-> (M.ArchSegmentOff arch -> C.Position)
-- ^ Function that maps function address to Crucible position
-> M.DiscoveryFunInfo arch ids
-- ^ List of blocks for this region.
-> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
mkFunCFG archFns halloc memBaseVarMap nm posFn fn =
toCoreCFG archFns <$> mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn
evalMacawExprExtension :: IsSymInterface sym
=> sym
-> C.IntrinsicTypes sym
@ -459,6 +543,10 @@ freshValue sym str w ty =
offs <- freshConstant sym nm (C.BaseBVRepr y)
return (MM.LLVMPointer base offs)
M.FloatTypeRepr fi -> do
nm <- symName str
freshFloatConstant sym nm $ floatInfoToCrucible fi
M.BoolTypeRepr ->
do nm <- symName str
freshConstant sym nm C.BaseBoolRepr

15
symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
View File

@ -71,9 +71,11 @@ import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Parameterized.Classes
import Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.List as P
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import qualified Data.Parameterized.TH.GADT as U
import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC
@ -655,6 +657,7 @@ appToCrucible app = do
Just Refl -> evalMacawStmt (PtrEq rW xv yv)
Nothing ->
appAtom =<< C.BVEq n <$> toBits n xv <*> toBits n yv
M.FloatTypeRepr _ -> appAtom $ C.FloatEq xv yv
M.TupleTypeRepr _ -> fail "XXX: Equality on tuples not yet done."
@ -670,11 +673,19 @@ appToCrucible app = do
Just Refl -> evalMacawStmt (PtrMux rW cond tv fv)
Nothing -> appBVAtom n =<<
C.BVIte cond n <$> toBits n tv <*> toBits n fv
M.FloatTypeRepr fi ->
appAtom $ C.FloatIte (floatInfoToCrucible fi) cond tv fv
M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done."
M.TupleField tps x i ->
undefined tps x i -- TODO: Fix this
M.TupleField tps x i -> do
let tps' = typeListToCrucible tps
tp' = typeToCrucible $ tps P.!! i
x' <- v2c x
case Ctx.intIndex (fromIntegral $ P.indexValue i) (Ctx.size tps') of
Just (Some i') | Just Refl <- testEquality tp' (tps' Ctx.! i') ->
appAtom $ C.GetStruct x' i' tp'
_ -> fail ""
-- Booleans

41
symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
View File

@ -8,6 +8,7 @@ This defines the monad used to map Reopt blocks to Crucible.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
@ -22,10 +23,15 @@ module Data.Macaw.Symbolic.PersistentState
, initCrucPersistentState
-- * Types
, ToCrucibleType
, ToCrucibleFloatInfo
, FromCrucibleFloatInfo
, CtxToCrucibleType
, ArchRegContext
, typeToCrucible
, floatInfoToCrucible
, floatInfoFromCrucible
, typeCtxToCrucible
, typeListToCrucible
, macawAssignToCrucM
, memReprToCrucible
-- * Register index map
@ -59,9 +65,23 @@ type family ToCrucibleTypeList (l :: [M.Type]) :: Ctx C.CrucibleType where
type family ToCrucibleType (tp :: M.Type) :: C.CrucibleType where
ToCrucibleType (M.BVType w) = MM.LLVMPointerType w
ToCrucibleType (M.FloatType fi) = C.FloatType (ToCrucibleFloatInfo fi)
ToCrucibleType ('M.TupleType l) = C.StructType (ToCrucibleTypeList l)
ToCrucibleType M.BoolType = C.BaseToType C.BaseBoolType
type family ToCrucibleFloatInfo (fi :: M.FloatInfo) :: C.FloatInfo where
ToCrucibleFloatInfo M.HalfFloat = C.HalfFloat
ToCrucibleFloatInfo M.SingleFloat = C.SingleFloat
ToCrucibleFloatInfo M.DoubleFloat = C.DoubleFloat
ToCrucibleFloatInfo M.QuadFloat = C.QuadFloat
ToCrucibleFloatInfo M.X86_80Float = C.X86_80Float
type family FromCrucibleFloatInfo (fi :: C.FloatInfo) :: M.FloatInfo where
FromCrucibleFloatInfo C.HalfFloat = M.HalfFloat
FromCrucibleFloatInfo C.SingleFloat = M.SingleFloat
FromCrucibleFloatInfo C.DoubleFloat = M.DoubleFloat
FromCrucibleFloatInfo C.QuadFloat = M.QuadFloat
FromCrucibleFloatInfo C.X86_80Float = M.X86_80Float
type family CtxToCrucibleType (mtp :: Ctx M.Type) :: Ctx C.CrucibleType where
CtxToCrucibleType EmptyCtx = EmptyCtx
@ -92,8 +112,29 @@ typeToCrucible tp =
case tp of
M.BoolTypeRepr -> C.BoolRepr
M.BVTypeRepr w -> MM.LLVMPointerRepr w
M.FloatTypeRepr fi -> C.FloatRepr $ floatInfoToCrucible fi
M.TupleTypeRepr a -> C.StructRepr (typeListToCrucible a)
floatInfoToCrucible
:: M.FloatInfoRepr fi -> C.FloatInfoRepr (ToCrucibleFloatInfo fi)
floatInfoToCrucible = \case
M.HalfFloatRepr -> knownRepr
M.SingleFloatRepr -> knownRepr
M.DoubleFloatRepr -> knownRepr
M.QuadFloatRepr -> knownRepr
M.X86_80FloatRepr -> knownRepr
floatInfoFromCrucible
:: C.FloatInfoRepr fi -> M.FloatInfoRepr (FromCrucibleFloatInfo fi)
floatInfoFromCrucible = \case
C.HalfFloatRepr -> knownRepr
C.SingleFloatRepr -> knownRepr
C.DoubleFloatRepr -> knownRepr
C.QuadFloatRepr -> knownRepr
C.X86_80FloatRepr -> knownRepr
fi ->
error $ "Unsupported Crucible floating-point format in Macaw: " ++ show fi
typeListToCrucible ::
P.List M.TypeRepr ctx ->
Assignment C.TypeRepr (ToCrucibleTypeList ctx)

34
x86/src/Data/Macaw/X86/ArchTypes.hs
View File

@ -17,7 +17,7 @@ module Data.Macaw.X86.ArchTypes
, X86PrimFn(..)
, X87_FloatType(..)
, SSE_FloatType(..)
, SSE_Cmp
, SSE_Cmp(..)
, lookupSSECmp
, SSE_Op(..)
, AVXPointWiseOp2(..)
@ -210,8 +210,8 @@ sseOpName f =
-- | A single or double value for floating-point restricted to this types.
data SSE_FloatType tp where
SSE_Single :: SSE_FloatType (FloatType SingleFloat)
SSE_Double :: SSE_FloatType (FloatType DoubleFloat)
SSE_Single :: SSE_FloatType (FloatBVType SingleFloat)
SSE_Double :: SSE_FloatType (FloatBVType DoubleFloat)
instance Show (SSE_FloatType tp) where
show SSE_Single = "single"
@ -225,9 +225,9 @@ instance HasRepr SSE_FloatType TypeRepr where
-- X87 declarations
data X87_FloatType tp where
X87_Single :: X87_FloatType (BVType 32)
X87_Double :: X87_FloatType (BVType 64)
X87_ExtDouble :: X87_FloatType (BVType 80)
X87_Single :: X87_FloatType (FloatBVType SingleFloat)
X87_Double :: X87_FloatType (FloatBVType DoubleFloat)
X87_ExtDouble :: X87_FloatType (FloatBVType X86_80Float)
instance Show (X87_FloatType tp) where
show X87_Single = "single"
@ -513,7 +513,7 @@ data X86PrimFn f tp where
-- Guaranteed to not throw exception or have side effects.
X87_Extend :: !(SSE_FloatType tp)
-> !(f tp)
-> X86PrimFn f (BVType 80)
-> X86PrimFn f (FloatBVType X86_80Float)
-- | This performs an 80-bit floating point add.
--
@ -529,9 +529,9 @@ data X86PrimFn f tp where
-- * @#U@ Result is too small for destination format.
-- * @#O@ Result is too large for destination format.
-- * @#P@ Value cannot be represented exactly in destination format.
X87_FAdd :: !(f (FloatType X86_80Float))
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
X87_FAdd :: !(f (FloatBVType X86_80Float))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
-- | This performs an 80-bit floating point subtraction.
--
@ -547,9 +547,9 @@ data X86PrimFn f tp where
-- * @#U@ Result is too small for destination format.
-- * @#O@ Result is too large for destination format.
-- * @#P@ Value cannot be represented exactly in destination format.
X87_FSub :: !(f (FloatType X86_80Float))
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
X87_FSub :: !(f (FloatBVType X86_80Float))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
-- | This performs an 80-bit floating point multiply.
--
@ -565,9 +565,9 @@ data X86PrimFn f tp where
-- * @#U@ Result is too small for destination format.
-- * @#O@ Result is too large for destination format.
-- * @#P@ Value cannot be represented exactly in destination format.
X87_FMul :: !(f (FloatType X86_80Float))
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
X87_FMul :: !(f (FloatBVType X86_80Float))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
-- | This rounds a floating number to single or double precision.
--
@ -583,7 +583,7 @@ data X86PrimFn f tp where
-- In the #P case, the C1 register will be set 1 if rounding up,
-- and 0 otherwise.
X87_FST :: !(SSE_FloatType tp)
-> !(f (BVType 80))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f tp
-- | Unary operation on a vector. Should have no side effects.

15
x86/src/Data/Macaw/X86/Monad.hs
View File

@ -519,7 +519,7 @@ data Location addr (tp :: Type) where
-- top, so X87Register 0 is the top, X87Register 1 is the second,
-- and so forth.
X87StackRegister :: !Int
-> Location addr (FloatType X86_80Float)
-> Location addr (FloatBVType X86_80Float)
------------------------------------------------------------------------
-- Location
@ -743,14 +743,13 @@ c2_loc = fullRegister R.X87_C2
c3_loc = fullRegister R.X87_C3
-- | Maps float info repr to associated MemRepr.
floatMemRepr :: FloatInfoRepr flt -> MemRepr (FloatType flt)
floatMemRepr fir =
case floatInfoBytesIsPos fir of
LeqProof -> BVMemRepr (floatInfoBytes fir) LittleEndian
floatMemRepr :: FloatInfoRepr fi -> MemRepr (FloatBVType fi)
floatMemRepr fi | LeqProof <- floatInfoBytesIsPos fi =
BVMemRepr (floatInfoBytes fi) LittleEndian
-- | Tuen an address into a location of size @n
mkFPAddr :: FloatInfoRepr flt -> addr -> Location addr (FloatType flt)
mkFPAddr fir addr = MemoryAddr addr (floatMemRepr fir)
mkFPAddr :: FloatInfoRepr fi -> addr -> Location addr (FloatBVType fi)
mkFPAddr fi addr = MemoryAddr addr (floatMemRepr fi)
-- | Return MMX register corresponding to x87 register.
--
@ -1629,7 +1628,7 @@ getSegmentBase seg =
-- | X87 support --- these both affect the register stack for the
-- x87 state.
x87Push :: Expr ids (FloatType X86_80Float) -> X86Generator st ids ()
x87Push :: Expr ids (FloatBVType X86_80Float) -> X86Generator st ids ()
x87Push e = do
v <- eval e
topv <- getX87Top

6
x86/src/Data/Macaw/X86/Semantics.hs
View File

@ -1549,9 +1549,9 @@ def_fstX mnem doPop = defUnary mnem $ \_ val -> do
type X87BinOp
= forall f
. f (FloatType X86_80Float)
-> f (FloatType X86_80Float)
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
. f (FloatBVType X86_80Float)
-> f (FloatBVType X86_80Float)
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
execX87BinOp :: X87BinOp
-> Location (Addr ids) (BVType 80)

162
x86_symbolic/src/Data/Macaw/X86/Crucible.hs
View File

@ -1,6 +1,7 @@
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language LambdaCase #-}
{-# Language DataKinds #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
@ -41,6 +42,7 @@ import Data.Word (Word8)
import GHC.TypeLits (KnownNat)
import What4.Interface hiding (IsExpr)
import What4.InterpretedFloatingPoint
import What4.Symbol (userSymbol)
import Lang.Crucible.Backend (IsSymInterface)
@ -138,7 +140,8 @@ pureSem :: (IsSymInterface sym) =>
Sym sym {- ^ Handle to the simulator -} ->
M.X86PrimFn (AtomWrapper (RegEntry sym)) mt {- ^ Instruction -} ->
IO (RegValue sym (ToCrucibleType mt)) -- ^ Resulting value
pureSem sym fn =
pureSem sym fn = do
let symi = (symIface sym)
case fn of
M.CMPXCHG8B{} -> error "CMPXCHG8B"
M.XGetBV {} -> error "XGetBV"
@ -155,13 +158,6 @@ pureSem sym fn =
M.X86IRem {} -> error "X86IRem"
M.X86Div {} -> error "X86Div"
M.X86Rem {} -> error "X86Rem"
M.SSE_VectorOp {} -> error "SSE_VectorOp"
M.SSE_CMPSX {} -> error "SSE_CMPSX"
M.SSE_UCOMIS {} -> error "SSE_UCOMIS"
M.SSE_CVTSS2SD{} -> error "SSE_CVTSS2SD"
M.SSE_CVTSD2SS{} -> error "SSE_CVTSD2SS"
M.SSE_CVTSI2SX {} -> error "SSE_CVTSI2SX"
M.SSE_CVTTSX2SI {} -> error "SSE_CVTTSX2SI"
M.X87_Extend{} -> error "X87_Extend"
M.X87_FAdd{} -> error "X87_FAdd"
M.X87_FSub{} -> error "X87_FSub"
@ -169,7 +165,78 @@ pureSem sym fn =
M.X87_FST {} -> error "X87_FST"
M.VExtractF128 {} -> error "VExtractF128"
M.SSE_VectorOp op n (tp :: M.SSE_FloatType (M.BVType w)) x y -> do
let w = M.typeWidth tp
vecOp2M sym BigEndian (natMultiply n w) w x y $ V.zipWithM $ \x' y' -> do
x'' <- toValFloat' sym tp x'
y'' <- toValFloat' sym tp y'
fromValFloat' symi tp =<< case op of
M.SSE_Add ->
iFloatAdd @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Sub ->
iFloatSub @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Mul ->
iFloatMul @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Div ->
iFloatDiv @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_CMPSX op (tp :: M.SSE_FloatType tp) x y -> do
x' <- toValFloat symi tp x
y' <- toValFloat symi tp y
res <- case op of
M.EQ_OQ -> iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
M.LT_OS -> iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
M.LE_OS -> iFloatLe @_ @(FloatInfoFromSSEType tp) symi x' y'
M.UNORD_Q -> do
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
orPred symi x_is_nan y_is_nan
M.NEQ_UQ ->
notPred symi =<< iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
M.NLT_US ->
notPred symi =<< iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
M.NLE_US ->
notPred symi =<< iFloatLe @_ @(FloatInfoFromSSEType tp) symi x' y'
M.ORD_Q -> do
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
notPred symi =<< orPred symi x_is_nan y_is_nan
case tp of
M.SSE_Single -> do
zeros <- minUnsignedBV symi knownNat
ones <- maxUnsignedBV symi knownNat
llvmPointer_bv symi =<< bvIte symi res ones zeros
M.SSE_Double -> do
zeros <- minUnsignedBV symi knownNat
ones <- maxUnsignedBV symi knownNat
llvmPointer_bv symi =<< bvIte symi res ones zeros
M.SSE_UCOMIS (tp :: M.SSE_FloatType tp) x y -> do
x' <- toValFloat symi tp x
y' <- toValFloat symi tp y
is_eq <- iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
is_lt <- iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
is_unord <- orPred symi x_is_nan y_is_nan
zf <- orPred symi is_eq is_unord
cf <- orPred symi is_lt is_unord
let pf = is_unord
return $ empty `extend` (RV zf) `extend` (RV pf) `extend` (RV cf)
M.SSE_CVTSS2SD x ->
fromValFloat symi M.SSE_Double
=<< iFloatCast @_ @DoubleFloat @SingleFloat symi knownRepr RNE
=<< toValFloat symi M.SSE_Single x
M.SSE_CVTSD2SS x ->
fromValFloat symi M.SSE_Single
=<< iFloatCast @_ @SingleFloat @DoubleFloat symi knownRepr RNE
=<< toValFloat symi M.SSE_Double x
M.SSE_CVTSI2SX tp _ x ->
fromValFloat symi tp
=<< iSBVToFloat symi (floatInfoFromSSEType tp) RNE
=<< toValBV symi x
M.SSE_CVTTSX2SI w (tp :: M.SSE_FloatType tp) x ->
llvmPointer_bv symi
=<< iFloatToSBV @_ @_ @(FloatInfoFromSSEType tp) symi w RTZ
=<< toValFloat symi tp x
M.EvenParity x0 ->
do x <- getBitVal (symIface sym) x0
@ -354,6 +421,26 @@ vecOp2 sym endian totLen elLen x y f =
unpack2 (symIface sym) endian totLen elLen x y $ \u v ->
llvmPointer_bv (symIface sym) =<< evalE sym (V.toBV endian elLen (f u v))
vecOp2M
:: (IsSymInterface sym, 1 <= c)
=> Sym sym {- ^ Simulator -}
-> Endian {- ^ How to split-up the bit-vector -}
-> NatRepr w {- ^ Total width of the bit-vector -}
-> NatRepr c {- ^ Width of individual elements -}
-> AtomWrapper (RegEntry sym) (M.BVType w) {- ^ Input value 1 -}
-> AtomWrapper (RegEntry sym) (M.BVType w) {- ^ Input value 2 -}
-> ( forall n
. (1 <= n, (n * c) ~ w)
=> V.Vector n (E sym (BVType c))
-> V.Vector n (E sym (BVType c))
-> IO (V.Vector n (E sym (BVType c)))
) {- ^ Definition of operation -}
-> IO (RegValue sym (LLVMPointerType w)) -- ^ The final result.
vecOp2M sym endian totLen elLen x y f =
unpack2 (symIface sym) endian totLen elLen x y $ \u v ->
llvmPointer_bv (symIface sym)
=<< evalE sym
=<< (V.toBV endian elLen <$> f u v)
bitOp2 :: (IsSymInterface sym) =>
Sym sym {- ^ The simulator -} ->
@ -429,6 +516,63 @@ toValBV ::
IO (RegValue sym (BVType w))
toValBV sym (AtomWrapper x) = projectLLVM_bv sym (regValue x)
type family FloatInfoFromSSEType (tp :: M.Type) :: FloatInfo where
FloatInfoFromSSEType (M.BVType 32) = SingleFloat
FloatInfoFromSSEType (M.BVType 64) = DoubleFloat
floatInfoFromSSEType
:: M.SSE_FloatType tp -> FloatInfoRepr (FloatInfoFromSSEType tp)
floatInfoFromSSEType = \case
M.SSE_Single -> knownRepr
M.SSE_Double -> knownRepr
toValFloat
:: IsSymInterface sym
=> sym
-> M.SSE_FloatType tp
-> AtomWrapper (RegEntry sym) tp
-> IO (RegValue sym (FloatType (FloatInfoFromSSEType tp)))
toValFloat sym tp (AtomWrapper x) =
case tp of
M.SSE_Single ->
iFloatFromBinary sym SingleFloatRepr =<< projectLLVM_bv sym (regValue x)
M.SSE_Double ->
iFloatFromBinary sym DoubleFloatRepr =<< projectLLVM_bv sym (regValue x)
toValFloat'
:: IsSymInterface sym
=> Sym sym
-> M.SSE_FloatType (M.BVType w)
-> E sym (BVType w)
-> IO (RegValue sym (FloatType (FloatInfoFromSSEType (M.BVType w))))
toValFloat' sym tp x =
case tp of
M.SSE_Single ->
iFloatFromBinary (symIface sym) SingleFloatRepr =<< evalE sym x
M.SSE_Double ->
iFloatFromBinary (symIface sym) DoubleFloatRepr =<< evalE sym x
fromValFloat
:: IsSymInterface sym
=> sym
-> M.SSE_FloatType tp
-> RegValue sym (FloatType (FloatInfoFromSSEType tp))
-> IO (RegValue sym (ToCrucibleType tp))
fromValFloat sym tp x =
case tp of
M.SSE_Single -> llvmPointer_bv sym =<< iFloatToBinary sym SingleFloatRepr x
M.SSE_Double -> llvmPointer_bv sym =<< iFloatToBinary sym DoubleFloatRepr x
fromValFloat'
:: IsSymInterface sym
=> sym
-> M.SSE_FloatType (M.BVType w)
-> RegValue sym (FloatType (FloatInfoFromSSEType (M.BVType w)))
-> IO (E sym (BVType w))
fromValFloat' sym tp x =
case tp of
M.SSE_Single -> ValBV knownNat <$> iFloatToBinary sym SingleFloatRepr x
M.SSE_Double -> ValBV knownNat <$> iFloatToBinary sym DoubleFloatRepr x
--------------------------------------------------------------------------------