GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-24 08:53:12 +03:00
Code Issues Projects Releases Wiki Activity
5b93187d5b
macaw/refinement/macaw-refinement.cabal

136 lines
4.3 KiB
Plaintext
Raw Normal View History

Add refinement library. 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.
2019-01-08 01:16:03 +03:00
name: macaw-refinement
version: 0.0.1
Add README and Changelog and update cabal synopsis/description.
2019-01-08 02:13:50 +03:00
synopsis: Additional refinement operations for binary code discovery to improve coverage
Add refinement library. 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.
2019-01-08 01:16:03 +03:00
author: Galois, Inc.
maintainer: kquick@galois.com
Add README and Changelog and update cabal synopsis/description.
2019-01-08 02:13:50 +03:00
homepage: https://github.com/GaloisInc/macaw/refinement
Add refinement library. 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.
2019-01-08 01:16:03 +03:00
license: BSD3
license-file: LICENSE
Add README and Changelog and update cabal synopsis/description.
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
Add refinement library. 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.
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
[refinement] updates for merge of Some removal and updateDiscovery.
2019-02-07 04:58:21 +03:00
, macaw-loader
Add refinement library. 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.
2019-01-08 01:16:03 +03:00
, macaw-symbolic
, mtl
, parameterized-utils
[refinement] Add pretty printer for FuncBlockPath.
2019-01-29 02:04:21 +03:00
, prettyprinter
Add refinement library. 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.
2019-01-08 01:16:03 +03:00
, text
, what4 >= 0.4.0
hs-source-dirs: src
[refinement] Add initial refinement framework.
2019-01-25 01:48:55 +03:00
exposed-modules: Data.Macaw.Refinement
[refinement] Split out modules for Path handling, Function/Block utilities.
2019-01-28 21:50:35 +03:00
other-modules: Data.Macaw.Refinement.FuncBlockUtils
Data.Macaw.Refinement.Path
Data.Macaw.Refinement.Target
[refinement] Add initial refinement framework.
2019-01-25 01:48:55 +03:00
Data.Macaw.Refinement.UnknownTransfer
Add refinement library. 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.
2019-01-08 01:16:03 +03:00
Add README and Changelog and update cabal synopsis/description.
2019-01-08 02:13:50 +03:00
default-language: Haskell2010
Enable warnings for future compatibility issues.
2019-01-11 01:41:44 +03:00
ghc-options: -Wall -Wcompat
Add refinement library. 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.
2019-01-08 01:16:03 +03:00
ghc-prof-options: -O2 -fprof-auto-top
Add run-refinement tool for cmdline dumping of exe file info. This tool is similar to run-refurbish but it is intended to dump information about additional refinements provided by this library.
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
[refinement] update run-refinement tool for changes in library. Additional constraints and the refinement operations are now run in a MonadIO context.
2019-02-01 01:55:26 +03:00
, macaw-x86-symbolic
Add run-refinement --unrefined flag to show pre- and post- refinement.
2019-01-11 04:25:12 +03:00
, optparse-applicative
Add run-refinement tool for cmdline dumping of exe file info. This tool is similar to run-refurbish but it is intended to dump information about additional refinements provided by this library.
2019-01-11 01:53:12 +03:00
, parameterized-utils
, semmc-ppc
[refinement] Add test framework to compare output to expected output.
2019-01-23 07:04:26 +03:00
, 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
[refinement] update test generation and add refinement tests.
2019-01-23 23:04:41 +03:00
, macaw-refinement
Fixes.
2019-01-30 03:29:54 +03:00
, macaw-symbolic
[refinement] Add test framework to compare output to expected output.
2019-01-23 07:04:26 +03:00
, macaw-x86
Fixes.
2019-01-30 03:29:54 +03:00
, macaw-x86-symbolic
[refinement] Add test framework to compare output to expected output.
2019-01-23 07:04:26 +03:00
, optparse-applicative >= 0.13 && < 0.15
, parameterized-utils
, QuickCheck >= 2.7
, semmc-ppc
, tagged
, tasty
, tasty-hspec
, tasty-hunit
Reference in New Issue Copy Permalink