Abstract definitional interpreters are an approach to developing abstract interpretation-based static analyses in which language semantics are expressed through monadic recursive interpreters. These interpreters are then instantiated with an abstract value domain and executed in a suitable monadic context that carries abstract program state. Unfortunately, correctly implementing these definitional interpreters remains a difficult task. Moreover, instantiating analyses requires configuring many components. In this tool paper, we present the design of a framework called Monarch that provides reusable components to programmers for implementing abstract definitional interpreters. Our design consists of the following components: abstract domains, a framework for expressing program semantics, and analysis instantiation techniques. Finally, we present an implementation in Haskell and give example instantiations in Scheme and Python to show how these components are used.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Monarch: A Modular Framework for Abstract Definitional Interpreters in Haskell

  • Bram Vandenbogaerde,
  • Sarah Verbelen,
  • Noah Van Es,
  • Coen De Roover

摘要

Abstract definitional interpreters are an approach to developing abstract interpretation-based static analyses in which language semantics are expressed through monadic recursive interpreters. These interpreters are then instantiated with an abstract value domain and executed in a suitable monadic context that carries abstract program state. Unfortunately, correctly implementing these definitional interpreters remains a difficult task. Moreover, instantiating analyses requires configuring many components. In this tool paper, we present the design of a framework called Monarch that provides reusable components to programmers for implementing abstract definitional interpreters. Our design consists of the following components: abstract domains, a framework for expressing program semantics, and analysis instantiation techniques. Finally, we present an implementation in Haskell and give example instantiations in Scheme and Python to show how these components are used.