Versatile and Flexible Modelling of the RISC-V Instruction Set Architecture

Abstract. Formal languages are commonly used to model the seman- tics of instruction set architectures (e.g. ARM). The majority of prior work on these formal languages focuses on concrete instruction execu- tion 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. Con- trary 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. sym- bolic 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 in- terpreters. 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.