Symbolic encoding of LL(1) parsing and its applications

Parsers are omnipresent in almost all software systems. However, an operational implementation of parsers cannot answer many “how”, “why” and “what if” questions, why does this parser not accept this string, or, can we have to parser for it to accept a set of strings? To lift the parsing theory to answer such questions, we build a symbolic encoding of parsing. Our symbolic encoding, that we referred to as a parse condition , is a logical condition that is satisfiable if and only if a given string w can be successfully parsed using a grammar 𝒢 . We build an SMT encoding of such parse conditions for LL(1) grammars and demonstrate its utility by building three applications over it: automated repair of syntax errors in Tiger programs, automated parser synthesis to automatically synthesize LL(1) parsers from examples, and automatic root cause analysis of parser construction to debug errors in parse tables. We implement our ideas into a tool, Cyclops , that successfully repairs 80