Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

use demangler to decode C++ symbols #351

Merged
merged 6 commits into from
Nov 15, 2023
Merged

use demangler to decode C++ symbols #351

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e84d8d1
demangle C++ symbols
danmatichuk Nov 15, 2023
adb3d97
avoid infinite recursion in node ancestry
danmatichuk Nov 15, 2023
47f0653
reverse polarity when refining domains for "cells"
danmatichuk Nov 15, 2023
a91b619
add return status for plt stubs
danmatichuk Nov 15, 2023
ceffc84
bump freeze file
danmatichuk Nov 15, 2023
1ad6a88
add demangler submodule
danmatichuk Nov 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,3 +55,6 @@
[submodule "tools/pate/static/cytoscape.js-dagre"]
path = tools/pate/static/cytoscape.js-dagre
url = [email protected]:cytoscape/cytoscape.js-dagre.git
[submodule "submodules/demangler"]
path = submodules/demangler
url = [email protected]:GaloisInc/demangler.git
124 changes: 65 additions & 59 deletions arch/Pate/AArch32.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,66 +239,72 @@ argumentMapping =
}

stubOverrides :: PA.ArchStubOverrides SA.AArch32
stubOverrides = PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r0 ) $
Map.fromList $ map (\(nm,v) -> (BSC.pack nm, v)) $
[ ("malloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for calloc
, ("calloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for reallolc
, ("realloc", PA.mkMallocOverride r0 r0)
, ("clock", PA.mkClockOverride r0)
, ("write", PA.mkWriteOverride "write" r0 r1 r2 r0)
-- FIXME: fixup arguments for fwrite (len = size * nmemb)
, ("fwrite", PA.mkWriteOverride "fwrite" r3 r0 r1 r0)
, ("printf", PA.mkObservableOverride "printf" r0 r1)
, ("puts", PA.mkObservableOverride "puts" r0 r0)
-- fixme: double check this
, ("ceilf", PA.mkDefaultStubOverrideArg "ceilf" [Some v0] r0)
-- FIXME: check abi for args
, ("fread", PA.mkDefaultStubOverrideArg "fread" [Some r0, Some r1, Some r2, Some r4] r0)
-- FIXME: default stubs below here
] ++
(map mkDefault $
[ "memcpy" -- FIXME: needs implementation
, "memset" -- FIXME: needs implementation
, "gettimeofday" -- FIXME: needs implementation
, "getopt"
, "fprintf"
, "open"
, "atoi"
, "openat"
, "__errno_location"
, "ioctl"
, "fopen"
, "ERR_print_errors_fp"
, "RAND_bytes"
, "close"
, "fclose"
, "lseek"
, "strcpy"
, "sleep"
, "socket"
, "setsockopt"
, "bind"
, "select"
, "free"
, "sigfillset"
, "sigaction"
, "setitimer"
, "read"
-- PLT Stubs
, "EVP_CIPHER_CTX_new"
, "EVP_DecryptInit_ex"
, "EVP_DecryptUpdate"
, "EVP_DecryptFinal_ex"
, "EVP_EncryptInit_ex"
, "EVP_EncryptUpdate"
, "EVP_EncryptFinal_ex"
, "EVP_CIPHER_CTX_free"
, "EVP_aes_256_cbc"
, "BIO_dump_fp"
])
stubOverrides =
PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r0 ) $ \fs ->
case PB.fnSymBase fs of
-- FIXME: multiple variants of this constructor
"basic_string" -> Just $ PA.mkDefaultStubOverride "basic_string" r0
"print" -> Just $ PA.mkObservableOverride "print" r0 r1
_ -> lookup (PB.fnSymBase fs) override_list
where
override_list =
[ ("malloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for calloc
, ("calloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for reallolc
, ("realloc", PA.mkMallocOverride r0 r0)
, ("clock", PA.mkClockOverride r0)
, ("write", PA.mkWriteOverride "write" r0 r1 r2 r0)
-- FIXME: fixup arguments for fwrite (len = size * nmemb)
, ("fwrite", PA.mkWriteOverride "fwrite" r3 r0 r1 r0)
, ("printf", PA.mkObservableOverride "printf" r0 r1)
, ("puts", PA.mkObservableOverride "puts" r0 r0)
-- fixme: double check this
, ("ceilf", PA.mkDefaultStubOverrideArg "ceilf" [Some v0] r0)
-- FIXME: check abi for args
, ("fread", PA.mkDefaultStubOverrideArg "fread" [Some r0, Some r1, Some r2, Some r4] r0)
-- FIXME: default stubs below here
] ++
(map mkDefault $
[ "memcpy" -- FIXME: needs implementation
, "memset" -- FIXME: needs implementation
, "gettimeofday" -- FIXME: needs implementation
, "getopt"
, "fprintf"
, "open"
, "atoi"
, "openat"
, "__errno_location"
, "ioctl"
, "fopen"
, "ERR_print_errors_fp"
, "RAND_bytes"
, "close"
, "fclose"
, "lseek"
, "strcpy"
, "sleep"
, "socket"
, "setsockopt"
, "bind"
, "select"
, "free"
, "sigfillset"
, "sigaction"
, "setitimer"
, "read"
-- PLT Stubs
, "EVP_CIPHER_CTX_new"
, "EVP_DecryptInit_ex"
, "EVP_DecryptUpdate"
, "EVP_DecryptFinal_ex"
, "EVP_EncryptInit_ex"
, "EVP_EncryptUpdate"
, "EVP_EncryptFinal_ex"
, "EVP_CIPHER_CTX_free"
, "EVP_aes_256_cbc"
, "BIO_dump_fp"
])
mkDefault nm = (nm, PA.mkDefaultStubOverride nm r0)

r0 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R0")
Expand Down
116 changes: 59 additions & 57 deletions arch/Pate/PPC.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,64 +247,66 @@ argumentMapping = undefined

-- FIXME: clagged directly from ARM, registers may not be correct
stubOverrides :: (MS.SymArchConstraints (PPC.AnyPPC v), 1 <= SP.AddrWidth v, 16 <= SP.AddrWidth v) => PA.ArchStubOverrides (PPC.AnyPPC v)
stubOverrides = PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r0 ) $
Map.fromList $ map (\(nm,v) -> (BSC.pack nm, v)) $
[ ("malloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for calloc
, ("calloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for reallolc
, ("realloc", PA.mkMallocOverride r0 r0)
, ("clock", PA.mkClockOverride r0)
, ("write", PA.mkWriteOverride "write" r0 r1 r2 r0)
-- FIXME: fixup arguments for fwrite
, ("fwrite", PA.mkWriteOverride "fwrite" r0 r1 r2 r0)
, ("printf", PA.mkObservableOverride "printf" r0 r1)
-- FIXME: default stubs below here
] ++
(map mkDefault $
[ "getopt"
, "fprintf"
, "open"
, "atoi"
, "openat"
, "__errno_location"
, "ioctl"
, "fopen"
, "ERR_print_errors_fp"
, "RAND_bytes"
, "close"
, "fclose"
, "puts"
, "lseek"
, "strcpy"
, "sleep"
, "socket"
, "setsockopt"
, "bind"
, "select"
, "free"
, "sigfillset"
, "sigaction"
, "setitimer"
, "read"
, "memcpy" -- FIXME: needs implementation
, "__floatsidf" -- FIXME: lets us ignore float operations
, "__extendsfdf2" -- FIXME: lets us ignore float operations
, "__gtdf2" -- FIXME: lets us ignore float operations
, "ceil" -- FIXME: more floating point hacks
, "FLEXCAN_DRV_Send" -- FIXME: IO stub
]
) ++
(map mkNOPStub $ [
"console_debugln"
, "console_debugf"
, "console_printf" -- FIXME: observable?
, "console_printf_data" -- FIXME: observable?
, "console_println" -- FIXME: observable?
, "console_error" -- FIXME: observable?
, "console_print" -- FIXME: observable?
])
stubOverrides = PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r0 ) $ \fs ->
lookup (PBl.fnSymBase fs) override_list
where
override_list =
[ ("malloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for calloc
, ("calloc", PA.mkMallocOverride r0 r0)
-- FIXME: arguments are interpreted differently for reallolc
, ("realloc", PA.mkMallocOverride r0 r0)
, ("clock", PA.mkClockOverride r0)
, ("write", PA.mkWriteOverride "write" r0 r1 r2 r0)
-- FIXME: fixup arguments for fwrite
, ("fwrite", PA.mkWriteOverride "fwrite" r0 r1 r2 r0)
, ("printf", PA.mkObservableOverride "printf" r0 r1)
-- FIXME: default stubs below here
] ++
(map mkDefault $
[ "getopt"
, "fprintf"
, "open"
, "atoi"
, "openat"
, "__errno_location"
, "ioctl"
, "fopen"
, "ERR_print_errors_fp"
, "RAND_bytes"
, "close"
, "fclose"
, "puts"
, "lseek"
, "strcpy"
, "sleep"
, "socket"
, "setsockopt"
, "bind"
, "select"
, "free"
, "sigfillset"
, "sigaction"
, "setitimer"
, "read"
, "memcpy" -- FIXME: needs implementation
, "__floatsidf" -- FIXME: lets us ignore float operations
, "__extendsfdf2" -- FIXME: lets us ignore float operations
, "__gtdf2" -- FIXME: lets us ignore float operations
, "ceil" -- FIXME: more floating point hacks
, "FLEXCAN_DRV_Send" -- FIXME: IO stub
]
) ++
(map mkNOPStub $ [
"console_debugln"
, "console_debugf"
, "console_printf" -- FIXME: observable?
, "console_printf_data" -- FIXME: observable?
, "console_println" -- FIXME: observable?
, "console_error" -- FIXME: observable?
, "console_print" -- FIXME: observable?
])

mkNOPStub nm = (nm, PA.mkNOPStub nm)
mkDefault nm = (nm, PA.mkDefaultStubOverride nm r0)

Expand Down
8 changes: 4 additions & 4 deletions cabal.GHC-9.2.8.freeze
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ constraints: any.BoundedChan ==1.0.3.0,
lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy,
any.libBF ==0.6.6,
libBF -system-libbf,
any.lifted-async ==0.10.2.4,
any.lifted-async ==0.10.2.5,
any.lifted-base ==0.2.3.12,
any.llvm-pretty-bc-parser ==0.4.0.0,
llvm-pretty-bc-parser -fuzz,
Expand All @@ -167,7 +167,7 @@ constraints: any.BoundedChan ==1.0.3.0,
any.lumberjack ==1.0.3.0,
any.math-functions ==0.3.4.3,
math-functions +system-erf +system-expm1,
any.megaparsec ==9.6.0,
any.megaparsec ==9.6.1,
megaparsec -dev,
any.microlens ==0.4.13.1,
any.microlens-th ==0.4.3.14,
Expand Down Expand Up @@ -215,7 +215,7 @@ constraints: any.BoundedChan ==1.0.3.0,
any.s-cargot-letbind ==0.2.4.0,
any.safe ==0.3.19,
any.safe-exceptions ==0.1.7.4,
any.sayable ==1.2.3.0,
any.sayable ==1.2.3.1,
any.scientific ==0.3.7.0,
scientific -bytestring-builder -integer-simple,
any.selective ==0.7,
Expand Down Expand Up @@ -317,4 +317,4 @@ constraints: any.BoundedChan ==1.0.3.0,
any.zlib ==0.6.3.0,
zlib -bundled-c-zlib -non-blocking-ffi -pkg-config,
any.zlib-bindings ==0.1.1.5
index-state: hackage.haskell.org 2023-11-01T19:52:38Z
index-state: hackage.haskell.org 2023-11-15T12:42:10Z
1 change: 1 addition & 0 deletions cabal.project.dist
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ packages: .
submodules/asl-translator
submodules/elf-edit
submodules/dwarf
submodules/demangler
submodules/flexdis86
submodules/flexdis86/binary-symbols
submodules/dismantle/dismantle-tablegen
Expand Down
3 changes: 2 additions & 1 deletion pate.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,9 @@ common shared
unliftio >= 0.2 && < 0.3,
unordered-containers,
ordered-containers,
itanium-abi,
demangler >= 1.3.0.0,
semmc,
sayable,
text >= 1 && < 1.3,
tomland >= 1.3 && < 1.4,
transformers,
Expand Down
6 changes: 3 additions & 3 deletions src/Pate/Arch.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,12 +260,12 @@ withStubOverride sym wsolver (StubOverride ov) f = do


data ArchStubOverrides arch =
ArchStubOverrides (StubOverride arch) (Map.Map BS.ByteString (StubOverride arch))
ArchStubOverrides (StubOverride arch) (PB.FunctionSymbol -> Maybe (StubOverride arch))

lookupStubOverride ::
ValidArchData arch -> BS.ByteString -> Maybe (StubOverride arch)
ValidArchData arch -> PB.FunctionSymbol -> Maybe (StubOverride arch)
lookupStubOverride va nm = let ArchStubOverrides _ ov = validArchStubOverrides va in
Map.lookup nm ov
ov nm

defaultStubOverride ::
ValidArchData arch -> StubOverride arch
Expand Down
Loading
Loading