Hackage :: [Package]

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.

[maintain] [Publish]

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]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees