zbMATH — the first resource for mathematics

Parse condition: symbolic encoding of LL(1) parsing. (English) Zbl 1415.68120
Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 637-655 (2018).
Summary: In this work, we propose the notion of a parse condition – a logical condition that is satisfiable if and only if a given string \(w\) can be successfully parsed using a grammar \(\mathcal{G}\). Further, we propose an algorithm for building an SMT encoding of such parse conditions for LL(1) grammars and demonstrate its utility by building two applications over it: automated repair of syntax errors in tiger programs and automated parser synthesis to automatically synthesize LL(1) parsers from examples. We implement our ideas into a tool, Cyclops, that is able to successfully repair 80% of our benchmarks (675 buggy tiger programs), clocking an average of 30 seconds per repair and synthesize parsers for interesting languages from examples. Like verification conditions (encoding a program in logic) have found widespread applications in program analysis, we believe that parse conditions can serve as a foundation for interesting applications in syntax analysis.
For the entire collection see [Zbl 1407.68021].
68Q42 Grammars and rewriting systems
Full Text: DOI