Publication
Versatile and Flexible Modelling of the RISC-V Instruction Set Architecture
Sören Tempel; Tobias Brandt; Christoph Lüth
In: 24th International Symposium on Trends in Functional Programming (TFP). International Symposium on Trends in Functional Programming (TFP-2023), January 12-15, Boston, MA, USA, 2023.
Abstract
Formal languages are commonly used to model the semantics of instruction set architectures (e.g. ARM). The majority of prior work on these formal languages focuses on concrete instruction execution and validation tasks. We present a novel Haskell-based modelling approach which allows the creation of flexible and versatile architecture models based on free monads and a custom expression language. Contrary to existing work, our approach does not make any assumptions regarding the representation of memory and register values. This way, we can implement non-concrete software analysis techniques (e.g. symbolic execution where values are SMT expressions) on top of our model as interpreters for this model. In contrast to prior work, our modelling approach is therefore explicitly focused on the creation of custom ISA interpreters. We employ our outlined approach to create an abstract model and a concrete interpreter for the RISC-V base instruction set. Based on this model, we demonstrate that custom interpreters can be implemented with minimal effort using dynamic information flow tracking as a case study.