libriscv: A versatile, flexible and executable formal model for the RISC-V architecture.
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
A formal model for the RISC-V Instruction Set Architecture (ISA). Contrary to other Haskell RISC-V ISA models, like GRIFT or riscv-semantics, LibRISCV is specifically tailored to the creation of custom ISA interpreters. To this end, it is designed for flexibility, allowing a versatile representation of instruction operands. For example, instruction operands can be SMT expressions for symbolic execution of binary code.
LibRISCV abstractly describes instruction semantics using an Embedded Domain Specific Language
(EDSL) with free(r) monads. This Haskell library
is intended to build custom interpreters for this free monad. The entry point for this purpose is
the LibRISCV.Semantics.buildAST
function which obtains the free monad AST based on an entry address.
The entry address can be obtained from a provided ELF loader implementation, this Loader module
is also responsible for loading binary instructions into a provided memory implementation. Refer to
provided example interpreters in the GitHub repository
for practical usage instruction. More detailed information on LibRISCV and its concepts is also
available in a TFP'23 publication.
Properties
Versions | 0.1.0.0, 0.1.0.0 |
---|---|
Change log | None available |
Dependencies | array (>=0.5.4.0 && <0.6), base (>=4.15.0.0 && <4.20.0.0), bv (>=0.5 && <0.6), bytestring (>=0.10.10 && <0.12), containers (>=0.6.5.1 && <0.7), exceptions (>=0.10.4 && <0.11), extra (>=1.7.0 && <1.8), file-embed (>=0.0.10 && <0.1), filepath (>=1.4.2.1 && <1.5), freer-simple (>=1.2.1.2 && <1.3), libriscv, melf (>=1.3.0 && <1.4), optparse-applicative (>=0.16.1 && <0.19), parameterized-utils (>=2.1.6.0 && <2.2), template-haskell (>=2.18.0 && <2.22), transformers (>=0.5.6.0 && <0.7), yaml (>=0.11.8.0 && <0.12) [details] |
License | MIT |
Copyright | (c) 2022-2024 University of Bremen |
Author | Sören Tempel, Tobias Brandt, and Christoph Lüth |
Maintainer | Group of Computer Architecture <riscv@informatik.uni-bremen.de> |
Category | Formal Languages |
Home page | https://github.com/agra-uni-bremen/libriscv |
Bug tracker | https://github.com/agra-uni-bremen/libriscv/issues |
Source repo | head: git clone https://github.com/agra-uni-bremen/libriscv.git |
Uploaded | by nmeum at 2024-07-08T15:31:57Z |
Modules
[Index] [Quick Jump]
- LibRISCV
- LibRISCV.CmdLine
- Effects
- Decoding
- Expressions
- Logging
- Operations
- LibRISCV.Loader
- LibRISCV.Semantics
Downloads
- libriscv-0.1.0.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees