A versatile, flexible and executable formal model for the RISC-V architecture.
A formal model for the RISC-VInstruction 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.