GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-29 21:44:11 +03:00
Code Issues Projects Releases Wiki Activity
12daa3a17b
macaw/symbolic/macaw-symbolic.cabal

40 lines
763 B
Plaintext
Raw Normal View History

Refactor to support Boolean type; start mapping to Crucible.
2017-07-08 00:18:35 +03:00
name: macaw-symbolic
version: 0.0.1
author: Galois, Inc.
maintainer: jhendrix@galois.com
build-type: Simple
cabal-version: >= 1.9.2
Update license information.
2017-09-28 01:59:06 +03:00
license: BSD3
license-file: LICENSE
Refactor to support Boolean type; start mapping to Crucible.
2017-07-08 00:18:35 +03:00
library
build-depends:
Refactor X86 semantics types; add tuples to Macaw.
2017-12-02 00:58:20 +03:00
base >= 4,
Port to use crucible syntax extensions.
2018-01-09 21:40:14 +03:00
ansi-wl-pprint,
Refactor X86 semantics types; add tuples to Macaw.
2017-12-02 00:58:20 +03:00
containers,
Clean up and document the macaw-symbolic API This cleanup consolidates the interface to macaw symbolic into two (and a half) modules: - Data.Macaw.Symbolic for clients who just need to symbolically simulate machine code - Data.Macaw.Symbolic.Backend for clients that need to implement new architectures - Data.Macaw.Symbolic.Memory provides a reusable example implementation of machine pointer to LLVM memory model pointer mapping Most functions are now documented and are grouped by use case. There are two worked (compiling) examples in the haddocks that show how to translate Macaw into Crucible and then symbolically simulate the results (including setting up all aspects of Crucible). The examples are included in the symbolic/examples directory and can be loaded with GHCi to type check them. The Data.Macaw.Symbolic.Memory module still needs a worked example. There were very few changes to actual code as part of this overhaul, but there are a few places where complicated functions were hidden behind newtypes, as users never need to construct the values themselves (e.g., MacawArchEvalFn and MacawSymbolicArchFunctions). There was also a slight consolidation of constraint synonyms to reduce duplication. All callers will have to be updated. There is also now a README for macaw-symbolic that explains its purpose and includes pointers to the new haddocks. This commit also fixes up the (minor) breakage in the macaw-x86-symbolic implementation from the API changes.
2019-01-11 05:10:30 +03:00
IntervalMap >= 0.6 && < 0.7,
Updates to Macaw.
2018-06-06 21:48:45 +03:00
crucible >= 0.4,
crucible-llvm,
Refactor X86 semantics types; add tuples to Macaw.
2017-12-02 00:58:20 +03:00
lens,
macaw-base,
mtl,
parameterized-utils,
Get started on integrating the LLVM memory model.
2018-02-07 03:47:13 +03:00
text,
Clean up and document the macaw-symbolic API This cleanup consolidates the interface to macaw symbolic into two (and a half) modules: - Data.Macaw.Symbolic for clients who just need to symbolically simulate machine code - Data.Macaw.Symbolic.Backend for clients that need to implement new architectures - Data.Macaw.Symbolic.Memory provides a reusable example implementation of machine pointer to LLVM memory model pointer mapping Most functions are now documented and are grouped by use case. There are two worked (compiling) examples in the haddocks that show how to translate Macaw into Crucible and then symbolically simulate the results (including setting up all aspects of Crucible). The examples are included in the symbolic/examples directory and can be loaded with GHCi to type check them. The Data.Macaw.Symbolic.Memory module still needs a worked example. There were very few changes to actual code as part of this overhaul, but there are a few places where complicated functions were hidden behind newtypes, as users never need to construct the values themselves (e.g., MacawArchEvalFn and MacawSymbolicArchFunctions). There was also a slight consolidation of constraint synonyms to reduce duplication. All callers will have to be updated. There is also now a README for macaw-symbolic that explains its purpose and includes pointers to the new haddocks. This commit also fixes up the (minor) breakage in the macaw-x86-symbolic implementation from the API changes.
2019-01-11 05:10:30 +03:00
vector,
bytestring,
Updates to Macaw.
2018-06-06 21:48:45 +03:00
what4 >= 0.4.0
Refactor to support Boolean type; start mapping to Crucible.
2017-07-08 00:18:35 +03:00
hs-source-dirs: src
exposed-modules:
Clean up and document the macaw-symbolic API This cleanup consolidates the interface to macaw symbolic into two (and a half) modules: - Data.Macaw.Symbolic for clients who just need to symbolically simulate machine code - Data.Macaw.Symbolic.Backend for clients that need to implement new architectures - Data.Macaw.Symbolic.Memory provides a reusable example implementation of machine pointer to LLVM memory model pointer mapping Most functions are now documented and are grouped by use case. There are two worked (compiling) examples in the haddocks that show how to translate Macaw into Crucible and then symbolically simulate the results (including setting up all aspects of Crucible). The examples are included in the symbolic/examples directory and can be loaded with GHCi to type check them. The Data.Macaw.Symbolic.Memory module still needs a worked example. There were very few changes to actual code as part of this overhaul, but there are a few places where complicated functions were hidden behind newtypes, as users never need to construct the values themselves (e.g., MacawArchEvalFn and MacawSymbolicArchFunctions). There was also a slight consolidation of constraint synonyms to reduce duplication. All callers will have to be updated. There is also now a README for macaw-symbolic that explains its purpose and includes pointers to the new haddocks. This commit also fixes up the (minor) breakage in the macaw-x86-symbolic implementation from the API changes.
2019-01-11 05:10:30 +03:00
Data.Macaw.Symbolic
Data.Macaw.Symbolic.Backend
Data.Macaw.Symbolic.Memory
other-modules:
Update for parameterized-utils compat.
2018-01-03 04:31:42 +03:00
Data.Macaw.Symbolic.CrucGen
Remove generic quot/rem ops, and BoolMux; Refactor macaw-symbolic.
2017-10-03 00:40:14 +03:00
Data.Macaw.Symbolic.PersistentState
Cleanup pointer manipulation operations.
2018-02-09 22:41:39 +03:00
Data.Macaw.Symbolic.MemOps
Refactor to support Boolean type; start mapping to Crucible.
2017-07-08 00:18:35 +03:00
Added -Wcompat for warnings about future compatibility.
2019-01-11 00:43:27 +03:00
ghc-options: -Wall -Wcompat
Get started on integrating the LLVM memory model.
2018-02-07 03:47:13 +03:00
ghc-prof-options: -O2 -fprof-auto-top
Reference in New Issue Copy Permalink