nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible

verfasst von : Marius Kamp, Michael Philippsen

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Bit-vector-based program synthesis is an important building block of state-of-the-art techniques in computer programming. Some of these techniques do not only rely on a synthesizer’s ability to return an appropriate program if it exists but also require a synthesizer to detect if there is no such program at all in the entire search space (i.e., the problem is infeasible), which is a computationally demanding task.

In this paper, we propose an approach to quickly identify some synthesis problems as infeasible. We observe that a specification function encodes dependencies between input and output bits that a correct program must satisfy. To exploit this fact, we present approximate analyses of essential bits and use them in two novel algorithms to check if a synthesis problem is infeasible. Our experiments show that adding our technique to applications of bit vector synthesis can save up to 33% of their time.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking

Nächstes Kapitel Automated Repair of Heap-Manipulating Programs Using Deductive Synthesis

The benchmark sources provide a means to obtain the correct program. For example, some sources specify rewrite rules. Here, the left hand side corresponds to the specification function and the right hand side is an implementing program.

We observed that synthesizers for the class of Syntax Guided Synthesis problems perform poorly due to the necessary restrictions, as others noted before us [4].

Alur, R., et al.: Syntax-guided synthesis. In: FMCAD 2013: Formal Methods in Computer-Aided Design, Portland, OR, pp. 1–8 (2013). https://sygus.org

Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metasketches. In: POPL 2016: Principles of Programming Languages, St. Petersburg, FL, pp. 775–788 (2016). https://doi.org/10.1145/2837614.2837666

Buchwald, S.: Optgen: a generator for local optimizations. In: Franke, B. (ed.) CC 2015. LNCS, vol. 9031, pp. 171–189. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46663-6_9CrossRef

Buchwald, S., Fried, A., Hack, S.: Synthesizing an instruction selection rule library from semantic specifications. In: CGO 2018: Code Generation and Optimization, Vienna, Austria, pp. 300–313 (2018). https://doi.org/10.1145/3168821

Cowan, M., Moreau, T., Chen, T., Bornholt, J., Ceze, L.: Automatic generation of high-performance quantized machine learning kernels. In: CGO 2020: Code Generation and Optimization, San Diego, CA, pp. 305–316 (2020). https://doi.org/10.1145/3368826.3377912

Crama, Y., Hammer, P.L.: Fundamental concepts and applications. In: Boolean Functions: Theory, Algorithms, and Applications, pp. 3–66. Cambridge University Press, Cambridge (2011). ISBN: 978-0-521-84751-3. https://doi.org/10.1017/CBO9780511852008.002

Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)CrossRef

Diestel, R.: Graph Theory. Springer, Berlin (2017). https://doi.org/10.1007/978-3-662-53622-3CrossRefMATH

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49CrossRef

10.

Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI 2011: Programming Language Design and Implementation, San Jose, CA, pp. 62–73 (2011). https://doi.org/10.1145/1993498.1993506

11.

Hu, Q., Breck, J., Cyphert, J., D’Antoni, L., Reps, T.: Proving unrealizability for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 335–352. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_18CrossRef

12.

Hu, Q., Cyphert, J., D’Antoni, L., Reps, T.W.: Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In: PLDI 2020: Programming Language Design and Implementation, London, UK, pp. 1128–1142 (2020). https://doi.org/10.1145/3385412.3385979

13.

Kamp, M., Philippsen, M.: Artifact for “approximate bit dependency analysis to identify program synthesis problems as infeasible”, October 2020. https://doi.org/10.5281/zenodo.4275482

14.

Mechtaev, S., Griggio, A., Cimatti, A., Roychoudhury, A.: Symbolic execution with existential second-order constraints. In: ESEC/FSE 2018: European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Lake Buena Vista, FL, pp. 389–399 (2018). https://doi.org/10.1145/3236024.3236049

15.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

16.

Nötzli, A., et al.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 279–297. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-24258-9_20CrossRef

17.

Phothilimthana, P.M., Jelvis, T., Shah, R., Totla, N., Chasins, S., Bodik, R.: Chlorophyll: synthesis-aided compiler for low-power spatial architectures. ACM SIGPLAN Not. 49(6), 396–407 (2014). https://doi.org/10.1145/2666356.2594339CrossRef

18.

Sasnauskas, R., et al.: Souper: a synthesizing superoptimizer (2018). arXiv:1711.04422, April 2018. https://github.com/google/souper

19.

Van Geffen, J., Nelson, L., Dillig, I., Wang, X., Torlak, E.: Synthesizing JIT compilers for in-kernel DSLs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 564–586. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_29CrossRef

20.

Warren Jr., H.S.: Functions realizable with word-parallel logical and two’s-complement addition instructions. Commun. ACM 20(6), 439–441 (1977). https://doi.org/10.1145/359605.359632MathSciNetCrossRefMATH

21.

Warren Jr., H.S.: Hacker’s Delight. Addison-Wesley, Upper Saddle River (2012)

22.

Wegener, I.: The Complexity of Boolean Functions. B. G. Teubner, Stuttgart (1987)MATH

Titel: Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
verfasst von: Marius Kamp
Michael Philippsen
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-67066-5

Electronic ISBN: 978-3-030-67067-2

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-67067-2_16

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"