mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-02 10:54:04 +03:00
984f7cb368
This patch contains a handful of tweaks needed to make the libraries in the `macaw` repo build with GHC 9.6: * GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`, `Control.Monad.Trans`, and similar modules from `mtl`-related modules. To accommodate this, various imports have been made more explicit. * I have disambiguated a use of `Data.Parameterized.NatRepr.withKnownNat` in `macaw-aarch32` to avoid clashing with a newly exported function of the same name in `GHC.TypeNats`. * I have bumped various upper version bounds on `doctest`, `optparse-applicative`, and `what4` to allow building these libraries with GHC 9.6. * I have bumped the following submodules to bring in GHC 9.6–related changes: * `asl-translator`: GaloisInc/asl-translator#53 * `crucible`: GaloisInc/crucible#1102 * `dwarf`: GaloisInc/dwarf#6 * `elf-edit`: GaloisInc/elf-edit#38 * `flexdis86`: GaloisInc/flexdis86#54 * `grift`: GaloisInc/grift#9 * `llvm-pretty`: elliottt/llvm-pretty#112 * `llvm-pretty-bc-parser`: GaloisInc/llvm-pretty-bc-parser#225 * `semmc`: GaloisInc/semmc#80 * `what4`: GaloisInc/what4#235
168 lines
5.4 KiB
Plaintext
168 lines
5.4 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-base 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-base. The identification provided by
|
|
macaw-base 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
|
|
, bv-sized >= 1.0.0
|
|
, containers
|
|
, crucible >= 0.4
|
|
, crucible-llvm
|
|
, lens
|
|
, macaw-base
|
|
, macaw-loader
|
|
, macaw-loader-ppc
|
|
, macaw-loader-x86
|
|
, macaw-ppc
|
|
, macaw-symbolic
|
|
, macaw-ppc-symbolic
|
|
, mtl
|
|
, parameterized-utils
|
|
, prettyprinter >= 1.7
|
|
, text
|
|
, what4 >= 0.4.0
|
|
, scheduler >= 1.4 && < 1.6
|
|
, async
|
|
, lumberjack >= 0.1.0.2 && < 1.1
|
|
, unliftio-core >= 0.2 && < 0.3
|
|
, exceptions >= 0.10 && < 0.11
|
|
, haggle
|
|
|
|
hs-source-dirs: src
|
|
|
|
exposed-modules: Data.Macaw.Refinement
|
|
|
|
other-modules: Data.Macaw.Refinement.FuncBlockUtils
|
|
Data.Macaw.Refinement.Logging
|
|
Data.Macaw.Refinement.Path
|
|
Data.Macaw.Refinement.Solver
|
|
Data.Macaw.Refinement.Target
|
|
Data.Macaw.Refinement.SymbolicExecution
|
|
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
|
|
other-modules: Summary, Options, Initialization
|
|
default-language: Haskell2010
|
|
ghc-options: -Wall -Wcompat -rtsopts -threaded
|
|
build-depends: base >= 4
|
|
, bytestring
|
|
, containers
|
|
, elf-edit
|
|
, exceptions
|
|
, lens
|
|
, macaw-base
|
|
, macaw-loader
|
|
, macaw-loader-x86
|
|
, macaw-loader-ppc
|
|
, macaw-ppc
|
|
, macaw-ppc-symbolic
|
|
, macaw-refinement
|
|
, macaw-symbolic
|
|
, macaw-x86
|
|
, macaw-x86-symbolic
|
|
, optparse-applicative
|
|
, parameterized-utils
|
|
, prettyprinter
|
|
, semmc-ppc
|
|
, text
|
|
, what4
|
|
, crucible
|
|
, crucible-llvm
|
|
, mtl
|
|
, lumberjack
|
|
, unliftio-core
|
|
|
|
test-suite test-refinements
|
|
type: exitcode-stdio-1.0
|
|
buildable: True
|
|
default-language: Haskell2010
|
|
GHC-options: -Wall -Wcompat
|
|
hs-source-dirs: tests, tools
|
|
main-is: RefinementTests.hs
|
|
other-modules: Summary, Initialization, Options
|
|
build-depends: base >= 4
|
|
, bytestring
|
|
, containers
|
|
, directory
|
|
, elf-edit
|
|
, exceptions
|
|
, filepath
|
|
, filemanip
|
|
, lens
|
|
, macaw-base
|
|
, macaw-loader
|
|
, macaw-loader-x86
|
|
, macaw-loader-ppc
|
|
, macaw-ppc
|
|
, macaw-ppc-symbolic
|
|
, macaw-refinement
|
|
, macaw-symbolic
|
|
, macaw-x86
|
|
, macaw-x86-symbolic
|
|
, crucible
|
|
, crucible-llvm
|
|
, what4
|
|
, optparse-applicative >= 0.13 && < 0.19
|
|
, parameterized-utils
|
|
, QuickCheck >= 2.7
|
|
, semmc-ppc
|
|
, text
|
|
, tagged
|
|
, tasty
|
|
, tasty-hspec
|
|
, tasty-hunit
|
|
, prettyprinter
|
|
, mtl
|
|
, lumberjack
|
|
, unliftio-core
|