Synthesis of loop-free programs

By Sumit Gulwani, Susmit Jha, Ashish Tiwari, Ramarathnam Venkatesan. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2011

367 citations recorded by the source corpus.

We consider the problem of synthesizing loop-free programs that implement a desired functionality using components from a given library. Specifications of the desired functionality and the library components are provided as logical relations between their respective input and output variables. The library components can be used at most once, and hence the library is required to contain a reasonable overapproximation of the multiset of the components required. We solve the above component-based synthesis problem using a constraint-based approach that involves first generating a synthesis constraint, and then solving the constraint. The synthesis constraint is a first-order ∃∀ logic formula whose size is quadratic in the number of components. We present a novel algorithm for solving such constraints. Our algorithm is based on counterexample guided iterative synthesis paradigm and uses off-the-shelf SMT solvers. We present experimental results that show that our tool Brahma can efficiently synthesize highly nontrivial 10-20 line loop-free bitvector programs. These programs represent a state space of approximately 2010 programs, and are beyond the reach of the other tools based on sketching and superoptimization.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/ea93cf600859aa09b0b7b727c12f36543608e1cd

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Component-based synthesis for complex APIs (2017, methodology): “…that S Y P ET combines the practicality of API completion tools with the power of synthesis tools: While programs synthesized by S Y P ET are moderately sized, straight-line code fragments, S Y P ET can handle two orders of magnitude more components than previous synthesis tools [15, 16, 26, 38].”
Unsupervised Learning by Program Synthesis (2015, methodology): “The program synthesis community introduced solver-based methods for learning programs [7, 23, 9], and our work builds upon their techniques.”
Nopol: Automatic Repair of Conditional Statement Bugs in Java Programs (2018, methodology): “Before applying N OPOL to the buggy program, the user does not need to know whether”
Learning programs from noisy data (2016, background): “While not obvious, we will see that the problem of synthesizing a program from noisy data appears in this setting as well, and thus the general framework of synthesis with noise discussed so far also applies here.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “…engines for a variety of applications, including software and hardware veriﬁcation [19, 52, 60, 68, 82, 86], model checking [41, 42, 98], type checking, static analysis, security [10,62], automated test-case generation [40,135], synthesis [2,65], planning, scheduling, and optimization [127].”
Spreadsheet table transformations from examples (2011, methodology): “Program synthesis has traditionally been motivated by the need to synthesize non-trivial algorithms [11, 21, 22] or to discover tricky code-snippets [10, 23].”
DeepCoder: Learning to Write Programs (2016, neutral): “, Sketch (Solar-Lezama, 2008) and Brahma (Gulwani et al., 2011).”
Program Synthesis (2017, background): “The control structure of the program may be restricted to a user-provided looping template [135], a partial program with holes [132], straight-line programs [8, 47, 63, 87, 109], or a guarded statement set with control flow at the very top [43].”
Growing solver-aided languages with rosette (2013, methodology): “Performance of ROSETTE’s superoptimizer on 25 bitvector benchmarks from [17]”
Accelerating search-based program synthesis using learned probabilistic models (2018, background): “Various strategies have been proposed to address this challenge [3, 4, 13, 17, 32].”
Syntax-guided synthesis (2013, methodology): “We also tried a modification to the original algorithm [8], in which, instead of searching for a loop-free program that utilizes all components from the given library at once, we search for programs of increasing length such that every line can still select any component from the library.”
Synthesizing coupling proofs of differential privacy (2017, background): “The synthesis statistics show the size (in terms of ast nodes) of the largest formula passed to synth and number of variables appearing in it; the number of cegis iterations of the synthesis algorithm [28]; and the time spent in synth.”
Spreadsheet data manipulation using examples (2012, background): “, bit-vector tricks [7], switching logic in hybrid systems [21]).”
Program Synthesis Using Natural Language (2015, background): “Traditional program synthesis, synthesizing programs from complete specifications [18, 35, 51, 52], has not yet seen wide adoption due to the difficultly of writing such specifications and verifying the synthesized program satisfies this specification.”
Foofah: Transforming Data By Example (2017, methodology): “proposed a constraint-based program synthesis technique to synthesize loop-free bit-manipulation programs [15, 21] using logic solvers, like the SMT solver.”
Stochastic superoptimization (2012, methodology): “Gulwani [9] notes this as a source of benchmarks for program synthesis and superoptimization, and identifies a 25 program benchmark which ranges in complexity from turning off the right-most bit in a word, to rounding up to the next highest power of 2, or selecting the upper 32 bits from a 64-bit mu”
FrAngel: component-based synthesis with control structures (2018, methodology): “Loops in particular have been a common source of difficulty in component-based synthesis [Feng et al. 2017b; Gulwani et al. 2011a; Jha et al. 2010; Menon et al. 2013].”
Neuro-Symbolic Program Synthesis (2016, background): “…et al., 2012), superoptimization by ﬁnding smaller equivalent loop bodies (Schkufza et al., 2013), protocol synthesis from scenarios (Udupa et al., 2013), synthesis of loop-free programs (Gulwani et al., 2011), and automated feedback generation for programming assignments (Singh et al., 2013).”