libriscv: A versatile, flexible and executable formal model for the RISC-V architecture.
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.
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
For package maintainers and hackage trustees
Candidates
Versions [RSS] | 0.1.0.0 |
---|---|
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-10T09:39:58Z |
Distributions | |
Executables | riscv-tiny |
Downloads | 18 total (5 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs uploaded by user Build status unknown [no reports yet] |