mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-27 12:52:52 +03:00
Merge branch 'master' of gitlab-ext.galois.com:macaw/macaw-semmc
This commit is contained in:
commit
399cd4ab6c
@ -18,6 +18,7 @@ cabal-version: >=1.10
|
||||
library
|
||||
exposed-modules: Data.Macaw.PPC
|
||||
Data.Macaw.PPC.Arch
|
||||
Data.Macaw.PPC.BinaryFormat.ELF
|
||||
Data.Macaw.PPC.Disassemble
|
||||
Data.Macaw.PPC.Eval
|
||||
Data.Macaw.PPC.Generator
|
||||
@ -44,8 +45,10 @@ library
|
||||
lens,
|
||||
macaw-base,
|
||||
ansi-wl-pprint,
|
||||
cereal,
|
||||
mtl,
|
||||
parameterized-utils,
|
||||
elf-edit,
|
||||
template-haskell,
|
||||
text
|
||||
hs-source-dirs: src
|
||||
|
@ -7,16 +7,21 @@
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
|
||||
module Data.Macaw.PPC (
|
||||
-- * Macaw configurations
|
||||
ppc32_linux_info,
|
||||
ppc64_linux_info
|
||||
ppc64_linux_info,
|
||||
-- * ELF support
|
||||
tocBaseForELF
|
||||
) where
|
||||
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
|
||||
import qualified Data.Macaw.AbsDomain.AbsState as MA
|
||||
import qualified Data.Macaw.Architecture.Info as MI
|
||||
import Data.Macaw.CFG
|
||||
import qualified Data.Macaw.CFG.DemandSet as MDS
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Macaw.Types ( BVType )
|
||||
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
@ -38,6 +43,7 @@ import Data.Macaw.PPC.Arch ( rewriteTermStmt,
|
||||
ppcPrimFnHasSideEffects,
|
||||
PPCArchConstraints
|
||||
)
|
||||
import Data.Macaw.PPC.BinaryFormat.ELF ( tocBaseForELF )
|
||||
import qualified Data.Macaw.PPC.Semantics.PPC32 as PPC32
|
||||
import qualified Data.Macaw.PPC.Semantics.PPC64 as PPC64
|
||||
|
||||
@ -52,14 +58,14 @@ archDemandContext _ =
|
||||
jumpTableEntrySize :: (PPCArchConstraints ppc) => proxy ppc -> MM.MemWord (ArchAddrWidth ppc)
|
||||
jumpTableEntrySize _ = 4
|
||||
|
||||
ppc64_linux_info :: MI.ArchitectureInfo PPC64.PPC
|
||||
ppc64_linux_info =
|
||||
ppc64_linux_info :: (ArchSegmentOff PPC64.PPC -> Maybe (MA.AbsValue 64 (BVType 64))) -> MI.ArchitectureInfo PPC64.PPC
|
||||
ppc64_linux_info tocMap =
|
||||
MI.ArchitectureInfo { MI.withArchConstraints = \x -> x
|
||||
, MI.archAddrWidth = MM.Addr64
|
||||
, MI.archEndianness = MM.BigEndian
|
||||
, MI.jumpTableEntrySize = jumpTableEntrySize proxy
|
||||
, MI.disassembleFn = disassembleFn proxy PPC64.execInstruction
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy tocMap
|
||||
, MI.absEvalArchFn = absEvalArchFn proxy
|
||||
, MI.absEvalArchStmt = absEvalArchStmt proxy
|
||||
, MI.postCallAbsState = postCallAbsState proxy
|
||||
@ -74,14 +80,14 @@ ppc64_linux_info =
|
||||
where
|
||||
proxy = Proxy @PPC64.PPC
|
||||
|
||||
ppc32_linux_info :: MI.ArchitectureInfo PPC32.PPC
|
||||
ppc32_linux_info =
|
||||
ppc32_linux_info :: (ArchSegmentOff PPC32.PPC -> Maybe (MA.AbsValue 32 (BVType 32))) -> MI.ArchitectureInfo PPC32.PPC
|
||||
ppc32_linux_info tocMap =
|
||||
MI.ArchitectureInfo { MI.withArchConstraints = \x -> x
|
||||
, MI.archAddrWidth = MM.Addr32
|
||||
, MI.archEndianness = MM.BigEndian
|
||||
, MI.jumpTableEntrySize = jumpTableEntrySize proxy
|
||||
, MI.disassembleFn = disassembleFn proxy PPC32.execInstruction
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy tocMap
|
||||
, MI.absEvalArchFn = absEvalArchFn proxy
|
||||
, MI.absEvalArchStmt = absEvalArchStmt proxy
|
||||
, MI.postCallAbsState = postCallAbsState proxy
|
||||
|
80
macaw-ppc/src/Data/Macaw/PPC/BinaryFormat/ELF.hs
Normal file
80
macaw-ppc/src/Data/Macaw/PPC/BinaryFormat/ELF.hs
Normal file
@ -0,0 +1,80 @@
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
module Data.Macaw.PPC.BinaryFormat.ELF (
|
||||
tocBaseForELF
|
||||
) where
|
||||
|
||||
import GHC.TypeLits ( KnownNat, natVal )
|
||||
|
||||
import Control.Monad ( replicateM, unless )
|
||||
import qualified Data.ByteString.Char8 as C8
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.Serialize.Get as G
|
||||
import qualified Data.Set as S
|
||||
import Text.Printf ( printf, PrintfArg )
|
||||
|
||||
import qualified Data.ElfEdit as E
|
||||
import qualified Data.Macaw.AbsDomain.AbsState as MA
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Macaw.Types ( BVType )
|
||||
|
||||
-- | Given an ELF file, extract a mapping from function entry points to the
|
||||
-- value of the TOC pointer (which is to be stored in r2) for that function.
|
||||
--
|
||||
-- The generated function is called from 'mkInitialAbsState' to set up the value
|
||||
-- of r2 at the entry point to each function, which will allow macaw to discover
|
||||
-- the values of loaded function pointers.
|
||||
--
|
||||
-- In the v1 PowerPC ABI (at least as generated by gcc), the entries are all
|
||||
-- stored in the @.opd@ section. Each entry is three pointers, where the first
|
||||
-- entry is the function address and the second is the value of the TOC. The
|
||||
-- third entry is unused in C programs (it is meant for Pascal).
|
||||
tocBaseForELF :: forall ppc proxy
|
||||
. (KnownNat (MC.RegAddrWidth (MC.ArchReg ppc)), MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc)))
|
||||
=> proxy ppc
|
||||
-> E.Elf (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||
-> MM.Memory (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||
-> MC.ArchSegmentOff ppc
|
||||
-> Maybe (MA.AbsValue (MC.RegAddrWidth (MC.ArchReg ppc)) (BVType (MC.RegAddrWidth (MC.ArchReg ppc))))
|
||||
tocBaseForELF proxy e mem =
|
||||
case E.findSectionByName (C8.pack ".opd") e of
|
||||
[sec] ->
|
||||
case G.runGet (parseFunctionDescriptors proxy mem (fromIntegral ptrSize)) (E.elfSectionData sec) of
|
||||
Left err -> error ("Error parsing .opd section: " ++ err)
|
||||
Right res -> \entryAddr -> M.lookup entryAddr res
|
||||
_ -> error "Could not find .opd section"
|
||||
where
|
||||
ptrSize = natVal (Proxy @(MC.RegAddrWidth (MC.ArchReg ppc)))
|
||||
|
||||
parseFunctionDescriptors :: (MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc)))
|
||||
=> proxy ppc
|
||||
-> MM.Memory (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||
-> Int
|
||||
-> G.Get (M.Map (MC.ArchSegmentOff ppc) (MA.AbsValue (MC.RegAddrWidth (MC.ArchReg ppc)) (BVType (MC.RegAddrWidth (MC.ArchReg ppc)))))
|
||||
parseFunctionDescriptors _ mem ptrSize = do
|
||||
let recordBytes = (3 * ptrSize) `div` 8
|
||||
let recordParser =
|
||||
case ptrSize of
|
||||
32 -> getFunctionDescriptor mem G.getWord32be
|
||||
64 -> getFunctionDescriptor mem G.getWord64be
|
||||
_ -> error ("Invalid pointer size: " ++ show ptrSize)
|
||||
totalBytes <- G.remaining
|
||||
unless (totalBytes `mod` recordBytes == 0) $ do
|
||||
fail "The .opd section is not divisible by the record size"
|
||||
funcDescs <- replicateM (totalBytes `div` recordBytes) recordParser
|
||||
return (M.fromList funcDescs)
|
||||
|
||||
getFunctionDescriptor :: (Integral a, PrintfArg a, MM.MemWidth w)
|
||||
=> MM.Memory w
|
||||
-> G.Get a
|
||||
-> G.Get (MM.MemSegmentOff w, MA.AbsValue w (BVType w))
|
||||
getFunctionDescriptor mem ptrParser = do
|
||||
entryAddr <- ptrParser
|
||||
tocAddr <- ptrParser
|
||||
_ <- ptrParser
|
||||
case MM.resolveAbsoluteAddr mem (fromIntegral entryAddr) of
|
||||
Nothing -> error (printf "Invalid function entry point: 0x%x" entryAddr)
|
||||
Just mso -> return (mso, MA.FinSet (S.singleton (fromIntegral tocAddr)))
|
@ -19,9 +19,12 @@ import qualified Data.Set as S
|
||||
|
||||
import Data.Macaw.AbsDomain.AbsState as MA
|
||||
import Data.Macaw.CFG
|
||||
import Data.Macaw.Types ( BVType )
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import Data.Parameterized.Some ( Some(..) )
|
||||
|
||||
import qualified Dismantle.PPC as D
|
||||
|
||||
import Data.Macaw.PPC.Arch
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Simplify ( simplifyValue )
|
||||
@ -66,12 +69,17 @@ postPPCTermStmtAbsState preservePred mem s0 regState stmt =
|
||||
-- abstract return value.
|
||||
mkInitialAbsState :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> (ArchSegmentOff ppc -> Maybe (MA.AbsValue (RegAddrWidth (ArchReg ppc)) (BVType (RegAddrWidth (ArchReg ppc)))))
|
||||
-> MM.Memory (RegAddrWidth (ArchReg ppc))
|
||||
-> ArchSegmentOff ppc
|
||||
-> MA.AbsBlockState (ArchReg ppc)
|
||||
mkInitialAbsState _ _mem startAddr =
|
||||
MA.top & MA.setAbsIP startAddr
|
||||
& MA.absRegState . boundValue PPC_LNK .~ MA.ReturnAddr
|
||||
mkInitialAbsState _ tocMap _mem startAddr =
|
||||
case tocMap startAddr of
|
||||
Just tocAddr -> s0 & MA.absRegState . boundValue (PPC_GP (D.GPR 2)) .~ tocAddr
|
||||
Nothing -> s0
|
||||
where
|
||||
s0 = MA.top & MA.setAbsIP startAddr
|
||||
& MA.absRegState . boundValue PPC_LNK .~ MA.ReturnAddr
|
||||
|
||||
absEvalArchFn :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
|
@ -1,4 +1,5 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
module PPC64InstructionCoverage (
|
||||
ppc64InstructionCoverageTests
|
||||
) where
|
||||
@ -6,6 +7,7 @@ module PPC64InstructionCoverage (
|
||||
import Control.Lens ( (^.) )
|
||||
import qualified Data.Map as M
|
||||
import Data.Maybe ( fromJust )
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.Set as S
|
||||
import Data.Word ( Word64 )
|
||||
import qualified Test.Tasty as T
|
||||
@ -17,6 +19,7 @@ import qualified Data.Parameterized.Some as PU
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import qualified Data.Macaw.Discovery as MD
|
||||
import qualified Data.Macaw.PPC as RO
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
|
||||
import Shared
|
||||
|
||||
@ -30,7 +33,8 @@ testMacaw :: E.Elf 64 -> IO ()
|
||||
testMacaw elf =
|
||||
withMemory MM.Addr64 elf $ \mem -> do
|
||||
let Just entryPoint = MM.asSegmentOff mem (findEntryPoint64 elf mem)
|
||||
let di = MD.cfgFromAddrs RO.ppc64_linux_info mem MD.emptySymbolAddrMap [entryPoint] []
|
||||
let tocBase = RO.tocBaseForELF (Proxy @PPC64.PPC) elf mem
|
||||
let di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem MD.emptySymbolAddrMap [entryPoint] []
|
||||
let allFoundBlockAddrs :: S.Set Word64
|
||||
allFoundBlockAddrs =
|
||||
S.fromList [ fromIntegral (fromJust (MM.asAbsoluteAddr (MM.relativeSegmentAddr (MD.pblockAddr pbr))))
|
||||
|
@ -1,8 +1,9 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE DeriveDataTypeable #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
module PPC64Tests (
|
||||
ppcAsmTests
|
||||
) where
|
||||
@ -11,6 +12,7 @@ import Control.Lens ( (^.) )
|
||||
import qualified Data.Foldable as F
|
||||
import qualified Data.Map as M
|
||||
import Data.Maybe ( fromJust )
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.Set as S
|
||||
import Data.Word ( Word64 )
|
||||
import System.FilePath ( dropExtension, replaceExtension )
|
||||
@ -26,6 +28,7 @@ import qualified Data.Macaw.Memory as MM
|
||||
import qualified Data.Macaw.Discovery as MD
|
||||
import qualified Data.Macaw.Discovery.State as MD
|
||||
import qualified Data.Macaw.PPC as RO
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
|
||||
import Data.List (intercalate)
|
||||
import Debug.Trace (trace)
|
||||
@ -76,7 +79,8 @@ testDiscovery expectedFilename elf =
|
||||
let Just entryPoint = trace (showSegments mem) $ MM.asSegmentOff mem (findEntryPoint64 elf mem)
|
||||
-- TODO: For some reason asSegmentOff is returning Nothing. Need to investigate.
|
||||
-- Above: Just need to convert the entry point from E.elfEntry elf to an ArchSegmentOff.
|
||||
di = MD.cfgFromAddrs RO.ppc64_linux_info mem MD.emptySymbolAddrMap [entryPoint] []
|
||||
tocBase = RO.tocBaseForELF (Proxy @PPC64.PPC) elf mem
|
||||
di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem MD.emptySymbolAddrMap [entryPoint] []
|
||||
expectedString <- readFile expectedFilename
|
||||
case readMaybe expectedString of
|
||||
-- Above: Read in the ExpectedResult from the contents of the file
|
||||
|
29
macaw-ppc/tests/ppc/test-indirect-calls.c
Normal file
29
macaw-ppc/tests/ppc/test-indirect-calls.c
Normal file
@ -0,0 +1,29 @@
|
||||
#include "util.h"
|
||||
|
||||
int g1;
|
||||
int g2;
|
||||
int g3;
|
||||
int g4;
|
||||
|
||||
int f2(long l1) {
|
||||
return (int)&g2;
|
||||
}
|
||||
|
||||
int f1(long l1) {
|
||||
long i1 = (long)&g1;
|
||||
i1 = l1 + i1;
|
||||
return (int)i1;
|
||||
}
|
||||
|
||||
void _start() {
|
||||
long i1 = (long)&g1;
|
||||
long i2 = (long)&g2;
|
||||
long i3 = (long)&g3;
|
||||
int (*fptr)(long) = &f1;
|
||||
if(i1 > i2)
|
||||
fptr = &f2;
|
||||
|
||||
g1 = fptr(i3 + i2);
|
||||
EXIT();
|
||||
}
|
||||
|
BIN
macaw-ppc/tests/ppc/test-indirect-calls.exe
Executable file
BIN
macaw-ppc/tests/ppc/test-indirect-calls.exe
Executable file
Binary file not shown.
139
macaw-ppc/tests/ppc/test-indirect-calls.s
Normal file
139
macaw-ppc/tests/ppc/test-indirect-calls.s
Normal file
@ -0,0 +1,139 @@
|
||||
.file "test-indirect-calls.c"
|
||||
.comm g1,4,4
|
||||
.comm g2,4,4
|
||||
.comm g3,4,4
|
||||
.comm g4,4,4
|
||||
.section ".toc","aw"
|
||||
.align 3
|
||||
.LC0:
|
||||
.quad g2
|
||||
.section ".text"
|
||||
.align 2
|
||||
.globl f2
|
||||
.section ".opd","aw"
|
||||
.align 3
|
||||
f2:
|
||||
.quad .L.f2,.TOC.@tocbase,0
|
||||
.previous
|
||||
.type f2, @function
|
||||
.L.f2:
|
||||
std 31,-8(1)
|
||||
stdu 1,-64(1)
|
||||
mr 31,1
|
||||
std 3,112(31)
|
||||
addis 9,2,.LC0@toc@ha
|
||||
ld 9,.LC0@toc@l(9)
|
||||
extsw 9,9
|
||||
mr 3,9
|
||||
addi 1,31,64
|
||||
ld 31,-8(1)
|
||||
blr
|
||||
.long 0
|
||||
.byte 0,0,0,0,128,1,0,1
|
||||
.size f2,.-.L.f2
|
||||
.section ".toc","aw"
|
||||
.LC1:
|
||||
.quad g1
|
||||
.section ".text"
|
||||
.align 2
|
||||
.globl f1
|
||||
.section ".opd","aw"
|
||||
.align 3
|
||||
f1:
|
||||
.quad .L.f1,.TOC.@tocbase,0
|
||||
.previous
|
||||
.type f1, @function
|
||||
.L.f1:
|
||||
std 31,-8(1)
|
||||
stdu 1,-80(1)
|
||||
mr 31,1
|
||||
std 3,128(31)
|
||||
addis 9,2,.LC1@toc@ha
|
||||
ld 9,.LC1@toc@l(9)
|
||||
std 9,48(31)
|
||||
ld 10,48(31)
|
||||
ld 9,128(31)
|
||||
add 9,10,9
|
||||
std 9,48(31)
|
||||
ld 9,48(31)
|
||||
extsw 9,9
|
||||
mr 3,9
|
||||
addi 1,31,80
|
||||
ld 31,-8(1)
|
||||
blr
|
||||
.long 0
|
||||
.byte 0,0,0,0,128,1,0,1
|
||||
.size f1,.-.L.f1
|
||||
.section ".toc","aw"
|
||||
.set .LC2,.LC1
|
||||
.set .LC3,.LC0
|
||||
.LC4:
|
||||
.quad g3
|
||||
.section ".text"
|
||||
.align 2
|
||||
.globl _start
|
||||
.section ".opd","aw"
|
||||
.align 3
|
||||
_start:
|
||||
.quad .L._start,.TOC.@tocbase,0
|
||||
.previous
|
||||
.type _start, @function
|
||||
.L._start:
|
||||
mflr 0
|
||||
std 0,16(1)
|
||||
std 31,-8(1)
|
||||
stdu 1,-160(1)
|
||||
mr 31,1
|
||||
addis 9,2,.LC2@toc@ha
|
||||
ld 9,.LC2@toc@l(9)
|
||||
std 9,120(31)
|
||||
addis 9,2,.LC3@toc@ha
|
||||
ld 9,.LC3@toc@l(9)
|
||||
std 9,128(31)
|
||||
addis 9,2,.LC4@toc@ha
|
||||
ld 9,.LC4@toc@l(9)
|
||||
std 9,136(31)
|
||||
addis 9,2,f1@toc@ha
|
||||
addi 9,9,f1@toc@l
|
||||
std 9,112(31)
|
||||
ld 10,120(31)
|
||||
ld 9,128(31)
|
||||
cmpd 7,10,9
|
||||
ble 7,.L6
|
||||
addis 9,2,f2@toc@ha
|
||||
addi 9,9,f2@toc@l
|
||||
std 9,112(31)
|
||||
.L6:
|
||||
ld 10,136(31)
|
||||
ld 9,128(31)
|
||||
add 10,10,9
|
||||
ld 9,112(31)
|
||||
mr 3,10
|
||||
std 2,40(1)
|
||||
ld 10,0(9)
|
||||
ld 11,16(9)
|
||||
mtctr 10
|
||||
ld 2,8(9)
|
||||
bctrl
|
||||
ld 2,40(1)
|
||||
mr 9,3
|
||||
mr 10,9
|
||||
addis 9,2,.LC2@toc@ha
|
||||
ld 9,.LC2@toc@l(9)
|
||||
stw 10,0(9)
|
||||
#APP
|
||||
# 27 "test-indirect-calls.c" 1
|
||||
li 0,1
|
||||
sc
|
||||
# 0 "" 2
|
||||
#NO_APP
|
||||
nop
|
||||
addi 1,31,160
|
||||
ld 0,16(1)
|
||||
mtlr 0
|
||||
ld 31,-8(1)
|
||||
blr
|
||||
.long 0
|
||||
.byte 0,0,0,1,128,1,0,1
|
||||
.size _start,.-.L._start
|
||||
.ident "GCC: (Ubuntu 7.2.0-6ubuntu1) 7.2.0"
|
12
macaw-ppc/tests/ppc/test-indirect-calls.s.expected
Normal file
12
macaw-ppc/tests/ppc/test-indirect-calls.s.expected
Normal file
@ -0,0 +1,12 @@
|
||||
R { funcs = [ (0x100001d0, [ (0x100001d0, 84)
|
||||
, (0x10000224, 56)
|
||||
, (0x10000230, 44)
|
||||
, (0x1000025c, 32)
|
||||
])
|
||||
, (0x10000180, [ (0x10000180, 68)
|
||||
])
|
||||
, (0x10000148, [ (0x10000148, 44)
|
||||
])
|
||||
]
|
||||
, ignoreBlocks = [0x1000027c]
|
||||
}
|
Loading…
Reference in New Issue
Block a user