research-article

G2Q: Haskell constraint solving

Authors:

William T. Hallahan,

Ruzica PiskacAuthors Info & Claims

Haskell 2019: Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell

Pages 44 - 57

https://doi.org/10.1145/3331545.3342590

Published: 08 August 2019 Publication History

Abstract

Constraint solvers give programmers a useful interface to solve challenging constraints at runtime. In particular, SMT solvers have been used for a vast variety of different, useful applications, ranging from strengthening Haskell's type system to verifying network protocols.

Unfortunately, interacting with constraint solvers directly from Haskell requires a great deal of manual effort. Data must be represented in and translated between two forms: that understood by Haskell, and that understood by the SMT solver. Such a translation is often done via printing and parsing text, meaning that any notion of type safety is lost. Furthermore, direct translations are rarely sufficient, as it typically takes many iterations on a design in order to get optimal -- or even acceptable -- performance from a SMT solver on large scale problems. This need for iteration complicates the translation issue: it is easy to introduce a runtime bug and frustrating to fix said bug.

To address these problems, we introduce a new constraint solving library, G2Q. G2Q includes a quasiquoter that allows solving constraints written in Haskell itself, thus unifying data representation, ensuring correct typing, and simplifying development iteration. We describe the API to our library and its backend. Rather than a direct translation to SMT formulas, G2Q makes use of the G2 symbolic execution engine. This allows G2Q to solve problems that are out of scope when directly encoded as SMT formulas. Finally, we demonstrate the usability of G2Q via four example programs.

References

[1]

Siddharth Agarwal. 2012. Functional SMT solving: A new interface for programmers. Master’s thesis, Indian Institute of Technology Kanpur (2012).

[2]

Markus Aronsson and Mary Sheeran. 2017. Hardware Software Codesign in Haskell. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell (Haskell 2017). ACM, New York, NY, USA, 162–173.

Digital Library

[3]

Henk P Barendregt. 1992. Lambda calculi with types. (1992).

[4]

Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi’c, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11) (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 171–177. http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf Snowbird, Utah.

Digital Library

[5]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard 2.6. 103. http://smtlib.cs.uiowa.edu/papers/smt-libreference-v2.6-r2017-07-18.pdf

[6]

Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI, Vol. 8. 209–224.

Digital Library

[7]

Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later. Commun. ACM 56, 2 (2013), 82–90.

Digital Library

[8]

Nicolaas Govert De Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes Mathematicae (Proceedings), Vol. 75. Elsevier, 381–392.

[9]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340. http://dl.acm.org/citation.cfm?id=1792734.1792766

Digital Library

[10]

Iavor S. Diatchki. 2015. Improving Haskell Types with SMT. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ’15). ACM, New York, NY, USA, 1–10.

Digital Library

[11]

Isil Dillig, Thomas Dillig, and Alex Aiken. 2012. Automated error diagnosis using abductive inference. In ACM SIGPLAN Notices, Vol. 47. ACM, 181–192.

Digital Library

[12]

Bruno Dutertre and Leonardo De Moura. 2006. The yices smt solver. Tool paper at http://yices. csl. sri. com/tool-paper. pdf 2, 2 (2006), 1–2.

[13]

Anton Ekblad. 2017. A meta-EDSL for Distributed Web Applications. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell (Haskell 2017). ACM, New York, NY, USA, 75–85.

Digital Library

[14]

Trevor Elliott, Lee Pike, Simon Winwood, Pat Hickey, James Bielman, Jamey Sharp, Eric Seidel, and John Launchbury. 2015. Guilt Free Ivory. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell (Haskell ’15). ACM, New York, NY, USA, 189–200.

Digital Library

[15]

Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. 1996. Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18, 2 (March 1996), 109–138.

Digital Library

[16]

William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac. 2019. Lazy Counterfactual Symbolic Execution. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). ACM, New York, NY, USA, 411–424.

Digital Library

[17]

Michael Hanus, Herbert Kuchen, and Juan Jose Moreno-Navarro. 1995. Curry: A truly functional logic language. In Proc. ILPS, Vol. 95. 95–107.

[18]

Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving Practical Distributed Systems Correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP ’15). ACM, New York, NY, USA, 1–17.

Digital Library

[19]

Isaac Jones. 2005. The Haskell Cabal, a common architecture for building applications and libraries. (2005).

[20]

Simon L Peyton Jones. 1992. Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine. Journal of functional programming 2, 2 (1992), 127–202.

[21]

Simon Peyton Jones and Mark Shields. 2004. Lexically-scoped type variables. (2004).

[22]

Susumu Katayama. 2013. MagicHaskeller on the Web: Automated programming as a service. In Haskell Symposium.

[23]

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. 2011. Scala to the Power of Z3: Integrating SMT and Programming. In International Conference on Automated Deduction. Springer, 400–406.

Digital Library

[24]

Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. 2012. Constraints As Control. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12). ACM, New York, NY, USA, 151–164.

Digital Library

[25]

Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. 2010. Complete Functional Synthesis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’10). ACM, New York, NY, USA, 316–329.

Digital Library

[26]

Henry Lieberman. 2001. Your wish is my command: Programming by example. Morgan Kaufmann.

[27]

Geoffrey Mainland. 2007. Why It’s Nice to Be Quoted: Quasiquoting for Haskell. In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop (Haskell ’07). ACM, New York, NY, USA, 73–82.

Digital Library

[28]

Mladen Nikoli\’c. 2012. Statistical Methodology for Comparison of SAT Solvers. In EMSQMS 2010. Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions (EPiC Series in Computing), Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli (Eds.), Vol. 6. EasyChair, 33–38.

[29]

Divesh Otwani and Richard A. Eisenberg. 2018. The Thoralf Plugin: For Your Fancy Type Needs. In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (Haskell 2018). ACM, New York, NY, USA, 106–118.

Digital Library

[30]

Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press.

[31]

Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). ACM, New York, NY, USA, 522–538.

Digital Library

[32]

Igor Rivin, Ilan Vardi, and Paul Zimmermann. 1994. The n-queens problem. The American Mathematical Monthly 101, 7 (1994), 629–639.

[33]

Eric L Seidel, Niki Vazou, and Ranjit Jhala. 2015. Type targeted testing. In European Symposium on Programming Languages and Systems. Springer, 812–836.

Digital Library

[34]

Tim Sheard and Simon Peyton Jones. 2002. Template Metaprogramming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell (Haskell ’02). ACM, New York, NY, USA, 1–16.

Digital Library

[35]

Emina Torlak and Rastislav Bodik. 2013. Growing Solver-aided Languages with Rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward! 2013). ACM, New York, NY, USA, 135–152.

Digital Library

[36]

Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14). ACM, New York, NY, USA, 530–541.

Digital Library

[37]

Richard Uhler and Nirav Dave. 2014. Smten with satisfiability-based search. In ACM SIGPLAN Notices, Vol. 49. ACM, 157–176.

Digital Library

[38]

Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, and Graham Hutton. 2018. Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl). In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (Haskell 2018). ACM, New York, NY, USA, 132–144.

Digital Library

[39]

Niki Vazou, Eric L. Seidel, and Ranjit Jhala. 2014. LiquidHaskell: Experience with Refinement Types in the Real World. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). ACM, New York, NY, USA, 39–51.

Digital Library

[40]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). ACM, New York, NY, USA, 269–282.

Digital Library

[41]

Dimitrios Vytiniotis, Simon Peyton Jones, Koen Claessen, and Dan Rosén. 2013. HALO: Haskell to logic through denotational semantics. In ACM Sigplan Notices, Vol. 48. ACM, 431–442.

Digital Library

[42]

Dana N Xu, Simon Peyton Jones, and Koen Claessen. 2009. Static contract checking for Haskell. Vol. 44. ACM.

Digital Library

Cited By

Lu SBodík R(2023)Grisette: Symbolic Compilation as a Functional Programming LibraryProceedings of the ACM on Programming Languages10.1145/35712097:POPL(455-487)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571209
Santolucito MPiskac RZhang JSherriff MHeckman SCutter PMonge A(2020)Formal Methods and Computing Identity-based Mentorship for Early Stage ResearchersProceedings of the 51st ACM Technical Symposium on Computer Science Education10.1145/3328778.3366957(135-141)Online publication date: 26-Feb-2020
https://dl.acm.org/doi/10.1145/3328778.3366957

Index Terms

G2Q: Haskell constraint solving
1. Computing methodologies
  1. Symbolic and algebraic manipulation
2. Software and its engineering
  1. Software notations and tools
    1. Software libraries and repositories

Recommendations

Type and interval aware array constraint solving for symbolic execution
ISSTA 2021: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis

Array constraints are prevalent in analyzing a program with symbolic execution. Solving array constraints is challenging due to the complexity of the precise encoding for arrays. In this work, we propose to synergize symbolic execution and array ...
Optimizing Constraint Solving to Better Support Symbolic Execution
ICSTW '11: Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops

Constraint solving is an integral part of symbolic execution, as most symbolic execution techniques rely heavily on an underlying constraint solver. In fact, the performance of the constraint solver used by a symbolic execution technique can ...
Constraint handling rules: the story so far
PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programming

Rule-based programming experiences renaissance due to its applications in areas such as Business Rules, Semantic Web, Computational Biology, Verification and Security. Executable rules are used in declarative programming languages, in program ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

Haskell 2019: Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell

August 2019

175 pages

ISBN:9781450368131

DOI:10.1145/3331545

Program Chair:
Richard A. Eisenberg

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 August 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICFP '19

Sponsor:

SIGPLAN

ICFP '19: ACM SIGPLAN International Conference on Functional Programming

August 22 - 23, 2019

Berlin, Germany

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
182
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)2

Reflects downloads up to 02 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lu SBodík R(2023)Grisette: Symbolic Compilation as a Functional Programming LibraryProceedings of the ACM on Programming Languages10.1145/35712097:POPL(455-487)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571209
Santolucito MPiskac RZhang JSherriff MHeckman SCutter PMonge A(2020)Formal Methods and Computing Identity-based Mentorship for Early Stage ResearchersProceedings of the 51st ACM Technical Symposium on Computer Science Education10.1145/3328778.3366957(135-141)Online publication date: 26-Feb-2020
https://dl.acm.org/doi/10.1145/3328778.3366957

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten