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

  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-x86
               , optparse-applicative >= 0.13 && < 0.15
               , parameterized-utils
               , QuickCheck >= 2.7
               , semmc-ppc
               , tagged
               , tasty
               , tasty-hspec
               , tasty-hunit