mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-04 06:36:29 +03:00
129 lines
4.1 KiB
Plaintext
129 lines
4.1 KiB
Plaintext
name: macaw-refinement
|
|
version: 0.0.1
|
|
synopsis: Additional refinement operations for binary code discovery to improve coverage
|
|
author: Galois, Inc.
|
|
maintainer: kquick@galois.com
|
|
homepage: https://github.com/GaloisInc/macaw/refinement
|
|
license: BSD3
|
|
license-file: LICENSE
|
|
|
|
build-type: Simple
|
|
cabal-version: >= 2.0
|
|
|
|
description:
|
|
The refinement library provides supplemental functionality for
|
|
discovery of elements that macaw-symbolic is not able to discover
|
|
via pattern matching. This library will use crucible symbolic
|
|
analysis to attempt to determine elements that could not be
|
|
identified by macaw-symbolic. The identification provided by
|
|
macaw-symbolic is incomplete, and so is the identification by this
|
|
macaw-refinement, but macaw-refinement attempts to additionally
|
|
"refine" the analysis to achieve even more information which can
|
|
then be provided back to the macaw analysis.
|
|
.
|
|
* Terminator effects for incomplete blocks. For example, the target
|
|
IP address by symbolic evaluation (e.g. of jump tables). If the
|
|
current block does not provide sufficient information to
|
|
symbolically identify the target, previous blocks can be added to
|
|
the analysis (back to the entry block or a loop point).
|
|
.
|
|
* Argument liveness (determining which registers and memory
|
|
locations are used/live by a block allows determination of ABI
|
|
compliance (for transformations) and specific block
|
|
requirements (which currently start with a full register state and
|
|
blank memory).
|
|
.
|
|
* Call graphs. Determination of targets of call instructions that
|
|
cannot be identified by pattern matching via symbolic evaluation,
|
|
using techniques similar to those for identifying incomplete blocks.
|
|
|
|
extra-source-files: Changelog.md
|
|
README.md
|
|
|
|
source-repository head
|
|
type: git
|
|
location: git://github.com/GaloisInc/macaw.git
|
|
|
|
|
|
library
|
|
build-depends: base >= 4
|
|
, ansi-wl-pprint
|
|
, containers
|
|
, crucible >= 0.4
|
|
, crucible-llvm
|
|
, lens
|
|
, macaw-base
|
|
, macaw-symbolic
|
|
, mtl
|
|
, parameterized-utils
|
|
, text
|
|
, what4 >= 0.4.0
|
|
|
|
hs-source-dirs: src
|
|
|
|
exposed-modules: Data.Macaw.Refinement
|
|
|
|
other-modules: Data.Macaw.Refinement.Target
|
|
Data.Macaw.Refinement.UnknownTransfer
|
|
|
|
default-language: Haskell2010
|
|
ghc-options: -Wall -Wcompat
|
|
ghc-prof-options: -O2 -fprof-auto-top
|
|
|
|
|
|
executable run-refinement
|
|
hs-source-dirs: tools
|
|
main-is: run-refinement.hs
|
|
default-language: Haskell2010
|
|
ghc-options: -Wall -Wcompat
|
|
build-depends: base >= 4
|
|
, bytestring
|
|
, containers
|
|
, elf-edit
|
|
, exceptions
|
|
, lens
|
|
, macaw-base
|
|
, macaw-loader
|
|
, macaw-loader-x86
|
|
, macaw-loader-ppc
|
|
, macaw-ppc
|
|
, macaw-refinement
|
|
, macaw-symbolic
|
|
, macaw-x86
|
|
, optparse-applicative
|
|
, parameterized-utils
|
|
, semmc-ppc
|
|
, text
|
|
|
|
test-suite test-refinements
|
|
type: exitcode-stdio-1.0
|
|
default-language: Haskell2010
|
|
GHC-options: -Wall -Werror -Wcompat
|
|
hs-source-dirs: tests
|
|
main-is: RefinementTests.hs
|
|
build-depends: base >= 4
|
|
, ansi-wl-pprint
|
|
, bytestring
|
|
, containers
|
|
, directory
|
|
, elf-edit
|
|
, exceptions
|
|
, filepath
|
|
, filemanip
|
|
, lens
|
|
, macaw-base
|
|
, macaw-loader
|
|
, macaw-loader-x86
|
|
, macaw-loader-ppc
|
|
, macaw-ppc
|
|
, macaw-refinement
|
|
, macaw-x86
|
|
, optparse-applicative >= 0.13 && < 0.15
|
|
, parameterized-utils
|
|
, QuickCheck >= 2.7
|
|
, semmc-ppc
|
|
, tagged
|
|
, tasty
|
|
, tasty-hspec
|
|
, tasty-hunit
|