Automating Grammar Comparison: Insights and Findings

Slide Note
Embed
Share

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.


Uploaded on Oct 08, 2024 | 0 Views


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


  1. Automating Grammar Comparison by Ravichandhran Madhavan, EPFL Mikael May r, EPFL Sumit Gulwani, MSR Viktor Kuncak, EPFL

  2. Overview of the Talk Proving equivalence of two CFGs Generation of words belonging to a CFG Finding counter-examples for equivalence

  3. Applications Online grammar tutoring system : grammar.epfl.ch Compatibility of programming language grammars

  4. Motivation & Contributions

  5. Example Well formed function types over Int Int Int => Int Int , Int => Int => Int ... type args => type | Int args Int , args | Int

  6. 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

  7. 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

  8. Comparing PL Grammars Grammars are often rewritten for efficient parsing Need to catch errors introduced during rewriting Identify sources of imprecision

  9. 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

  10. Summary of Results

  11. 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

  12. 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

  13. 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%)

  14. Proving Equivalence

  15. 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]

  16. 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

  17. 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

  18. 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

  19. 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

  20. 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

  21. Discovering Counter- Examples

  22. 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|)

  23. 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

  24. Results

  25. 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

  26. 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

  27. 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

  28. 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%)

  29. 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

  30. Summary of Evaluation Queries Refuted Proved Unknown Avg. Time / query 1395 1042 (74.6%) 289 64 107ms (20.7%) (4.6%)

  31. 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%)

  32. 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

Related


More Related Content