Abstract / Description of output

Programming or scripting languages used in real-world systems are seldom designed with a formal semantics in mind from the outset. Therefore, developing well-founded analysis tools for these systems requires reverse-engineering a formal semantics as a first step. This can take months or years of effort. Can we (at least partially) automate this process? Though desirable, automatically reverse-engineering semantics rules from an implementation is very challenging, as found by Krishnamurthi et al. [2019]. In this paper, we highlight that scaling methods with the size of the language is very difficult due to state space explosion, so we propose to learn semantics incrementally. We give a formalisation of Krishnamurthi et al.'s desugaring learning framework in order to clarify the assumptions necessary for an incremental learning algorithm to be feasible. We show that this reformulation allows us to extend the search space and express rules that Krishnamurthi et al. described as challenging, while still retaining feasibility. We evaluate enumerative synthesis as a baseline algorithm, and demonstrate that, with our reformulation of the problem, it is possible to learn correct desugaring rules for the example source and core languages proposed by Krishnamurthi et al., in most cases identical to the intended rules. In addition, with user guidance, our system was able to synthesize rules for desugaring list comprehensions and try/catch/finally constructs.
Original languageEnglish
Article number122
Number of pages29
JournalProceedings of the ACM on Programming Languages
Volume5
Issue numberOOPSLA
DOIs
Publication statusPublished - 15 Oct 2021
EventACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity - Chicago, United States
Duration: 17 Oct 202122 Oct 2021
https://2021.splashcon.org/

Keywords / Materials (for Non-textual outputs)

  • programming language semantics
  • testing
  • enumerative synthesis

Fingerprint

Dive into the research topics of 'One Down, 699 to Go: or, synthesising compositional desugarings'. Together they form a unique fingerprint.

Cite this