libriscv: A versatile, flexible and executable formal model for the RISC-V architecture.

[ formal-languages, library, mit, program ] [ Propose Tags ] [ Report a vulnerability ]

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.

Downloads

Maintainer's Corner

Package maintainers

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 31 total (1 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]