2019-01-08 01:16:03 +03:00
|
|
|
name: macaw-refinement
|
|
|
|
|
version: 0.0.1
|
2019-01-08 02:13:50 +03:00
|
|
|
synopsis: Additional refinement operations for binary code discovery to improve coverage
|
2019-01-08 01:16:03 +03:00
|
|
|
author: Galois, Inc.
|
|
|
|
|
maintainer: kquick@galois.com
|
2019-01-08 02:13:50 +03:00
|
|
|
homepage: https://github.com/GaloisInc/macaw/refinement
|
2019-01-08 01:16:03 +03:00
|
|
|
license: BSD3
|
|
|
|
|
license-file: LICENSE
|
|
|
|
|
|
2019-01-08 02:13:50 +03:00
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
2019-01-08 01:16:03 +03:00
|
|
|
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
|
|
|
|
|
|
2019-01-08 02:13:50 +03:00
|
|
|
default-language: Haskell2010
|
2019-01-11 01:41:44 +03:00
|
|
|
ghc-options: -Wall -Wcompat
|
2019-01-08 01:16:03 +03:00
|
|
|
ghc-prof-options: -O2 -fprof-auto-top
|
2019-01-11 01:53:12 +03:00
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
2019-01-11 04:25:12 +03:00
|
|
|
, optparse-applicative
|
2019-01-11 01:53:12 +03:00
|
|
|
, parameterized-utils
|
|
|
|
|
, semmc-ppc
|
