Parser combinators are a well-known mechanism used for the compositional construction of parsers, and have shown to be particularly useful in writing parsers for rich grammars with data-dependencies and global state. Verifying applications written using them, however, has proven to be challenging in large part because of the inherently effectful nature of the parsers being composed and the difficulty in reasoning about the arbitrarily rich data-dependent semantic actions that can be associated with parsing actions. In this paper, we address these challenges by defining a parser combinator framework called Morpheus equipped with abstractions for defining composable effects tailored for parsing and semantic actions and a rich specification language used to define safety properties over the constituent parsers comprising a program. Even though its abstractions yield many of the same expressivity benefits as other parser combinator systems, Morpheus is carefully engineered to yield a substantially more tractable automated verification pathway. We demonstrate its utility in verifying a number of realistic, challenging parsing applications, including several cases that involve non-trivial data-dependent relations.

翻译：解析器组合子是一种用于组合式构建解析器的著名机制，在处理具有数据依赖性和全局状态的丰富文法时尤为有效。然而，验证使用这些组合子编写的应用程序一直是一项极具挑战性的任务，这主要源于所组合的解析器本身具有副作用本质，以及难以对与解析操作相关联的任意丰富数据依赖语义动作进行推理。本文通过定义一个名为Morpheus的解析器组合子框架来应对这些挑战，该框架配备了专门用于定义解析和语义动作的可组合效应的抽象机制，以及用于对程序所包含的各个解析器定义安全性属性的丰富规约语言。尽管其抽象机制提供了与其他解析器组合子系统相同的表达能力优势，但Morpheus经过精心设计，能够实现显著更易处理的自动化验证路径。我们通过验证多个现实且具有挑战性的解析应用（包括若干涉及非平凡数据依赖关系的案例）展示了其实用性。