Automating Grammar Comparison: Insights and Findings
This presentation delves into automating grammar comparison, showcasing the equivalence of CFGs, generating words in CFGs, and uncovering counter-examples. It explores applications such as online grammar tutoring systems and compatibility of programming language grammars. Motivation, contributions, examples, and comparisons of PL grammars are discussed with a focus on identifying imprecisions and summarizing results from evaluating the tool on various CFG pairs. Notable findings include discrepancies in CFGs and the prevalence of counter-examples in random word sampling.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Automating Grammar Comparison by Ravichandhran Madhavan, EPFL Mikael May r, EPFL Sumit Gulwani, MSR Viktor Kuncak, EPFL
Overview of the Talk Proving equivalence of two CFGs Generation of words belonging to a CFG Finding counter-examples for equivalence
Applications Online grammar tutoring system : grammar.epfl.ch Compatibility of programming language grammars
Motivation & Contributions
Example Well formed function types over Int Int Int => Int Int , Int => Int => Int ... type args => type | Int args Int , args | Int
LL(1) Grammar for Function Types type Int rest rest => type | , Int args | args , Int args | => type Equivalence is not obvious Hard to verify manually But, this is exactly what we do while grading
An Incorrect Solution T A => T | Int A Int , T | Int type args => type | Int args Int , args | Int Buggy Smallest counter-example ? Int , Int , Int => Int
Comparing PL Grammars Grammars are often rewritten for efficient parsing Need to catch errors introduced during rewriting Identify sources of imprecision
Imprecisions Example enum ID implements Char { ... } accepted by ANTLR v4 Java 7 Grammar private private public public class ID { ... } accepted by ANTLR v4 and Oracle JLS 7 Grammars
Comparing PL Grammars Evaluated the tool on 5 pairs of CFGs of 5 languages Our tool found hundreds of discrepancies in < 1 min More than 40% of words sampled uniformly at random are counter-examples
Finding Regression Errors Automatically injected 3 kinds of errors into each grammar Generated a total of 300 benchmarks Our tool detected 87.3% of the errors 3 times more errors than available state of the art and 10 times faster
Grammar Tutoring System Analyzed a total of 1395 unique equivalence queries Provided a verdict on 95% of queries Disproved 1042 (74.6%) by finding counter-examples Proved 289 (20.7%)
Background Undecidable for CFGs but decidable for proper subclasses Deterministic CFGs [G. Snizergues, 01] LL grammars [Korenjak & Hopcroft, 66], [Olshansky & Pnueli, 77], [Rosenkrantz & Stearns, 69] Sub-deterministic CFGs [Valiant, 1970s] [Harrison, Havel & Yehudai, 79]
Generating Subgoals Ambiguous S a T T a T b | b P a R R a b b | a R b | b Hypothesize this holds for all strings with length < k S P S => a T and P => a R T R Branch Rule suffices to hold for strings of length < k
Equivalence To Inclusion S a T T a T b | b P a R R a b b | a R b | b S P S => a T and P => a R T R T b (bb U Rb) ? ? T b (bb U Rb)(bb U Rb) T b
Exploiting Test cases S a T T a T b | b P a R R a b b | a R b | b S P T R Use examples to simplify ? ? (bb U Rb) T b T b R b
Preventing Divergence S a T T a T b | b P a R R a b b | a R b | b Derive shortest word of T from R b T b R b R b =>* b b R is used in the derivation T R b b Compare the parts that were used by the derivation and those that weren t Split Rule
Using Inductive Hypotheses P a R R a b b | a R b | b S P S a T T a T b | b T R ? ? (bb U Rb) T b T b Rb b b T R Holds by hypothesis
Discovering Counter- Examples
Enumerating Words / Parse Trees Enumerators are bijective functions from natural numbers to parse trees 1 2 3 4 .. . We define the function explicitly Allows random access Sequential enumeration Randomly sampling Incremental O(|i|2|w||maxRHS|)
Discovering Counter-examples for Equivalence Sample words from one grammar and check if they can be parsed by the other We use two parsers: CYK with optimizations for batch parsing Antlr v4 Parser
Benchmark PL Grammars ANSI C 2011 grammars Javascript (Mozilla Spec Vs Antlr) Pascal Java 7 (Oracle Spec Vs Antlr) VHDL Avg. size: 212.6 nonterminals & 420.2 productions
Comparing Grammars for the Same Language More than 40% of words sampled uniformly at random are counter-examples ~ 1ms to sample u.a.r one word of length between 1 and 50
Detecting Fine grained Errors We injected 3 types of Error in each benchmark Removing a production Removing a nonterminal of a production Making a production infeasible in a specific context A -> a B B -> a c | d A -> a B B -> a c B -> a c | d
Detecting Fine grained Errors [Cont.] # Errors Found (T1 , T2, T3) Avg. time taken / error found Avg. counter example size Our tool 262 / 300 (97% , 92%, 73%) 28.1s 35 cfga 81 / 300 342.6s 12.2 (33%, 29%, 19%)
Grammar Tutoring System Offers exercises on Constructing grammars from english descriptions Conversions to normal forms CNF, GNF Leftmost derivation of a string from a grammar Has 60 problems with different difficulty level Used it in a 3rd year undergraduate course on computer language processing
Summary of Evaluation Queries Refuted Proved Unknown Avg. Time / query 1395 1042 (74.6%) 289 64 107ms (20.7%) (4.6%)
Results on Proving Equivalence Queries (fed to the proof engine) Proved Time LL(2) Ambiguous 353 289 410ms 63 18% 101 28.6% (81.9%)
Conclusion We propose, implement, and evaluate approaches for Enumerating and sampling words in polynomial time Discovering counter-examples for equivalence Proving equivalence that is complete for LL grammars applicable to arbitrary (ambiguous) grammars http://grammar.epfl.ch
