article

From Datalog to flix: a declarative language for fixed points on lattices

Authors:

Ondřej LhotákAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 6

Pages 194 - 208

https://doi.org/10.1145/2980983.2908096

Published: 02 June 2016 Publication History

Abstract

We present Flix, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. Flix is inspired by Datalog and extends it with lattices and monotone functions. Using Flix, implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax. We define a model-theoretic semantics of Flix as a natural extension of the Datalog semantics. This semantics captures the declarative meaning of Flix programs without imposing any specific evaluation strategy. An efficient strategy is semi-naive evaluation which we adapt for Flix. We have implemented a compiler and runtime for Flix, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. The declarative nature of Flix clearly exposes the similarity between these two algorithms.

References

[1]

L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, University of Copenhagen, 1994.

[2]

K. R. Apt, H. A. Blair, and A. Walker. Towards a Theory of Declarative Knowledge. In Foundations of Deductive Databases and Logic Programming. 1988. B978-0-934613-40-8.50006-3.

Digital Library

[3]

F. Bancilhon, D. Maier, Y. Sagiv, and J. D. Ullman. Magic Sets and Other Strange Ways to Implement Logic Programs. In Proc. Principles of Database Systems (PODS), 1985. 1145/6012.15399.

Digital Library

[4]

W. C. Benton and C. N. Fischer. Interactive, Scalable, Declarative Program Analysis: From Prototype to Implementation. In Proc. Principles and Practice of Declarative Programming (PPDP), 2007.

Digital Library

[5]

N. Bjørner, K. McMillan, and A. Rybalchenko. On Solving Universally Quantified Horn Clauses. In Proc. Symposium on Static Analysis (SAS), 2013.

[6]

978-3-642-38856-9_8.

[7]

S. M. Blackburn, R. Garner, C. Hoffman, A. M. Khan, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, J. E. B. Moss, A. Phansalkar, D. Stefanovi´c, T. VanDrunen, D. von Dincklage, and B. Wiedermann. The DaCapo benchmarks: Java Benchmarking Development and Analysis. In Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2006.

Digital Library

[8]

1167488.

[9]

M. Bravenboer and Y. Smaragdakis. Strictly Declarative Specification of Sophisticated Points-To Analyses. In Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2009.

Digital Library

[10]

G. Brewka, T. Eiter, and M. Truszczy´nski. Answer Set Programming at a Glance. Communications of the ACM, 2011.

Digital Library

[11]

[12]

S. Ceri, G. Gottlob, and L. Tanca. What You Always Wanted to Know About Datalog (and Never Dared to Ask). IEEE Transactions on Knowledge and Data Engineering (TKDE), 1989.

Digital Library

[13]

W. Clocksin and C. S. Mellish. Programming in Prolog. Springer Berlin Heidelberg, 2003.

[14]

978-3-642-55481-0.

[15]

M. Codish, A. Mulkers, M. Bruynooghe, M. G. De La Banda, and M. Hermenegildo. Improving Abstract Interpretations by Combining Domains. ACM Transactions on Programming Languages and Systems (TOPLAS), 1995. 200994.200998.

Digital Library

[16]

J. Cohen. Constraint Logic Programming Languages. Communications of the ACM, 1990.

Digital Library

[17]

N. Conway, W. R. Marczak, P. Alvaro, J. M. Hellerstein, and D. Maier. Logic and Lattices for Distributed Programming. In Proc. Symposium on Cloud Computing (SoCC), 2012. 1145/2391229.2391230.

Digital Library

[18]

A. Cortesi, G. Costantini, and P. Ferrara. A Survey on Product Operators in Abstract Interpretation. In Proc. Festschrift for David Schmidt, 2013.

[19]

P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Principles of Programming Languages (POPL), 1977.

Digital Library

[20]

512973.

[21]

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C – A Software Analysis Perspective. In Software Engineering and Formal Methods (SEFM), 2012.

Digital Library

[22]

[23]

E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov. Complexity and Expressive Power of Logic Programming. ACM Computing Surveys (CSUR), 2001.

Digital Library

[24]

S. Dawson, C. Ramakrishnan, and D. Warren. Practical Program Analysis Using General Purpose Logic Programming Systems – A Case Study. In Proc. Programming Language Design and Implementation (PLDI), 1996. 231379.231399.

Digital Library

[25]

O. de Moor, G. Gottlob, T. Furche, and A. Sellers, editors. Datalog Reloaded – First International Workshop, Datalog 2010, 2011.

Digital Library

[26]

T. Eiter, G. Gottlob, and H. Mannila. Adding Disjunction to Datalog. In Proc. Principles of Database Systems (PODS), 1994.

Digital Library

[27]

T. Eiter, G. Gottlob, and H. Mannila. Disjunctive Datalog. ACM Transactions on Database Systems (TODS), 1997. 1145/261124.261126.

Digital Library

[28]

S. Fink and J. Dolby. WALA – The TJ Watson Libraries for Analysis, 2012.

[29]

M. Fitting. Fixpoint Semantics for Logic Programming a Survey. Theoretical Computer Science (TCS), 2002. 1016/S0304-3975(00)00330-3.

Digital Library

[30]

C. Flanagan. Automatic Software Model Checking Using CLP. In Proc. European Symposium on Programming (ESOP), 2003.

Digital Library

[31]

[32]

M. Gelfond and V. Lifschitz. The Stable Model Semantics for Logic Programming. In Proc. International Conference on Logic Programming (ICLP/SLP), 1988.

[33]

M. Gelfond and V. Lifschitz. Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing, 1991.

[34]

G. Graefe. Query Evaluation Techniques for Large Databases. ACM Computing Surveys (CSUR), 1993.

Digital Library

[35]

152610.152611.

[36]

S. Gregory. Parallel Logic Programming in PARLOG: The Language and its Implementation. Addison-Wesley, 1987.

Digital Library

[37]

S. Gulwani and A. Tiwari. Combining Abstract Interpreters. In Proc. Programming Language Design and Implementation (PLDI), 2006.

Digital Library

[38]

E. Hajiyev, M. Verbaere, and O. D. Moor. codeQuest: Scalable Source Code Queries with Datalog. In Proc. European Conference on Object-Oriented Programming (ECOOP), 2006.

Digital Library

[39]

[40]

M. Hind. Pointer Analysis: Haven’t We Solved This Problem Yet? In Proc. Program Analysis for Software Tools and Engineering (PASTE), 2001.

Digital Library

[41]

S. S. Huang, T. J. Green, and B. T. Loo. Datalog and Emerging Applications: An Interactive Tutorial. In Proc. Management of Data (SIGMOD), 2011.

Digital Library

[42]

J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Principles of Programming Languages (POPL), 1987.

Digital Library

[43]

[44]

J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 1994. 0743-1066(94)90033-7.

[45]

J. B. Kam and J. D. Ullman. Monotone Data Flow Analysis Frameworks. Acta Informatica, 1977. BF00290339.

Digital Library

[46]

K. Kunen. Negation in Logic Programming. Journal of Logic Programming, 1987. 90007-0.

Digital Library

[47]

M. S. Lam, J. Whaley, V. B. Livshits, M. C. Martin, D. Avots, M. Carbin, and C. Unkel. Context-sensitive Program Analysis as Database Queries. In Proc. Principles of Database Systems (PODS), 2005.

Digital Library

[48]

N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri, and F. Scarcello. The DLV System for Knowledge Representation and Reasoning. ACM Transactions on Computational Logic (TOCL), 2006.

Digital Library

[49]

O. Lhoták and K.-C. A. Chung. Points-To Analysis with Efficient Strong Updates. In Proc. Principles of Programming Languages (POPL), 2011.

[50]

O. Lhoták and L. Hendren. Scaling Java Points-To Analysis using Spark. In Proc. Compiler Construction (CC), 2003.

Digital Library

[51]

[52]

N. Li and J. C. Mitchell. Datalog with Constraints: A Foundation for Trust Management Languages. In Proc. Practical Aspects of Declarative Languages (PADL), 2003. 1007/3-540-36388-2_6.

Digital Library

[53]

V. Lifschitz. Answer Set Planning. In Proc. Logic Programming and Nonmonotonic Reasoning (LPNMR), 1999.

Digital Library

[54]

[55]

V. Lifschitz. What Is Answer Set Programming? In Proc. Artificial Intelligence (AAAI), 2008.

Digital Library

[56]

F. Martin. PAG – An Efficient Program Analyzer Generator. Journal on Software Tools for Technology Transfer (STTT), 1998.

[57]

M. Méndez-Lojo, J. Navas, and M. Hermenegildo. A Flexible, (C)LP-Based Approach to the Analysis of Object-Oriented Programs. In Proc. Logic-Based Program Synthesis and Transformation (LOPSTR), 2007.

[58]

978-3-540-78769-3_11.

[59]

K. Muthukumar and M. Hermenegildo. Compile-time Derivation of Variable Dependency Using Abstract Interpretation. Journal of Logic Programming, 1992.

Digital Library

[60]

0743-1066(92)90035-2.

[61]

N. A. Naeem and O. Lhoták. Typestate-like Analysis of Multiple Interacting Objects. In Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2008.

Digital Library

[62]

[63]

N. A. Naeem, O. Lhoták, and J. Rodriguez. Practical Extensions to the IFDS Algorithm. In Proc. Compiler Construction (CC), 2010.

Digital Library

[64]

F. Nielson, H. R. Nielson, and H. Seidl. A Succinct Solver for ALFP. Nordic Journal of Computing (NJC), 2002.

Digital Library

[65]

F. Nielson, H. R. Nielson, H. Sun, M. Buchholtz, R. R. Hansen, H. Pilegaard, and H. Seidl. The Succinct Solver Suite. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2004. 21.

[66]

N. Ramsey, J. Dias, and S. P. Jones. Hoopl: A Modular, Reusable Library for Dataflow Analysis and Transformation. In Proc. Haskell Symposium, 2010.

Digital Library

[67]

1863539.

[68]

T. Reps, S. Horwitz, and M. Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. In Proc. Principles of Programming Languages (POPL), 1995. 199448.199462.

Digital Library

[69]

M. Sagiv, T. Reps, and S. Horwitz. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theoretical Computer Science (TCS), 1996. 0304-3975(96)00072-2.

Digital Library

[70]

Y. Smaragdakis and M. Bravenboer. Using Datalog for Fast and Easy Program Analysis. In Datalog Reloaded, 2011.

Digital Library

[71]

[72]

Y. Smaragdakis, M. Bravenboer, and O. Lhoták. Pick Your Contexts Well: Understanding Object-Sensitivity. In Proc. Principles of Programming Languages (POPL), 2011. 1145/1925844.1926390.

Digital Library

[73]

L. Sterling and E. Y. Shapiro. The Art of Prolog: Advanced Programming Techniques. MIT Press, 1994.

Digital Library

[74]

T. Swift and D. S. Warren. XSB: Extending Prolog with Tabled Logic Programming. Theory and Practice of Logic Programming (TPLP), 2012.

Digital Library

[75]

J. D. Ullman. Principles of Database Systems. Galgotia publications, 1984.

Digital Library

[76]

J. D. Ullman. Principles of Database and Knowledge-Base Systems, Volume I. Computer Science Press, 1988.

Digital Library

[77]

R. Vallée-Rai, P. Co, E. Gagnon, L. Hendren, P. Lam, and V. Sundaresan. Soot – A Java Bytecode Optimization Framework. In Proc. Centre for Advanced Studies on Collaborative Research (CASCON), 1999.

Digital Library

[78]

A. Van Gelder, K. A. Ross, and J. S. Schlipf. The Well-Founded Semantics for General Logic Programs. Journal of the ACM (JACM), 1991.

Digital Library

[79]

P. Wadler and S. Blott. How to Make Ad-hoc Polymorphism Less Ad Hoc. In Proc. Principles of Programming Languages (POPL), 1989.

Digital Library

[80]

J. Whaley and M. S. Lam. Cloning-based Context-sensitive Pointer Alias Analysis using Binary Decision Diagrams. In Proc. Programming Language Design and Implementation (PLDI), 2004.

Digital Library

Cited By

Yan ZZhang XDi P(2024)Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural NetworksProceedings of the ACM on Programming Languages10.1145/36897658:OOPSLA2(1532-1560)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689765
Dura AReichenbach CRodríguez GSadayappan PSukumaran-Rajam A(2024)Clog: A Declarative Language for C Static Code CheckersProceedings of the 33rd ACM SIGPLAN International Conference on Compiler Construction10.1145/3640537.3641579(186-197)Online publication date: 17-Feb-2024
https://dl.acm.org/doi/10.1145/3640537.3641579
Abeysinghe SXhebraj ARompf T(2024)Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisProceedings of the ACM on Programming Languages10.1145/36329288:POPL(2577-2609)Online publication date: 5-Jan-2024
https://doi.org/10.1145/3632928
Show More Cited By

Index Terms

From Datalog to flix: a declarative language for fixed points on lattices
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

From Datalog to flix: a declarative language for fixed points on lattices
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

We present Flix, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. Flix is inspired by Datalog and extends it with lattices and monotone functions. Using Flix, implementors ...
Semi-Inflationary DATALOG: A declarative database language with procedural features

This paper presents a rule-based database language which extends stratified DATALOG by adding a controlled form of inflationary fixpoint, immersed in a context of classical stratified negation with least fixpoint. The proposed language, called Semi-...
Datafun: a functional Datalog
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Datalog may be considered either an unusually powerful query language or a carefully limited logic programming language. Datalog is declarative, expressive, and optimizable, and has been applied successfully in a wide variety of problem domains. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 6

PLDI '16

June 2016

726 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2980983

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2016
726 pages
ISBN:9781450342612
DOI:10.1145/2908080
General Chair:
Chandra Krintz
University of California at Santa Barbara, USA
,
Program Chair:
Emery Berger
University of Massachusetts at Amherst, USA

Copyright © 2016 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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 June 2016

Published in SIGPLAN Volume 51, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

73
Total Citations
View Citations
1,075
Total Downloads

Downloads (Last 12 months)97
Downloads (Last 6 weeks)9

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yan ZZhang XDi P(2024)Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural NetworksProceedings of the ACM on Programming Languages10.1145/36897658:OOPSLA2(1532-1560)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689765
Dura AReichenbach CRodríguez GSadayappan PSukumaran-Rajam A(2024)Clog: A Declarative Language for C Static Code CheckersProceedings of the 33rd ACM SIGPLAN International Conference on Compiler Construction10.1145/3640537.3641579(186-197)Online publication date: 17-Feb-2024
https://dl.acm.org/doi/10.1145/3640537.3641579
Abeysinghe SXhebraj ARompf T(2024)Flan: An Expressive and Efficient Datalog Compiler for Program AnalysisProceedings of the ACM on Programming Languages10.1145/36329288:POPL(2577-2609)Online publication date: 5-Jan-2024
https://doi.org/10.1145/3632928
Herlihy AMartres GAilamaki AOdersky M(2024)Adaptive Recursive Query Optimization2024 IEEE 40th International Conference on Data Engineering (ICDE)10.1109/ICDE60146.2024.00035(368-381)Online publication date: 13-May-2024
https://doi.org/10.1109/ICDE60146.2024.00035
Zhang YWang YFlatt OCao DZucker PRosenthal ETatlock ZWillsey M(2023)Better Together: Unifying Datalog and Equality SaturationProceedings of the ACM on Programming Languages10.1145/35912397:PLDI(468-492)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591239
Sun YKumar SGilray TMicinski K(2023)Communication-Avoiding Recursive Aggregation2023 IEEE International Conference on Cluster Computing (CLUSTER)10.1109/CLUSTER52292.2023.00024(197-208)Online publication date: 31-Oct-2023
https://doi.org/10.1109/CLUSTER52292.2023.00024
Jurjo DMorales JLopez-Garcia PHermenegildo M(2023)A Rule-Based Approach for Designing and Composing Abstract DomainsLogic-Based Program Synthesis and Transformation10.1007/978-3-031-45784-5_6(80-98)Online publication date: 16-Oct-2023
https://doi.org/10.1007/978-3-031-45784-5_6
Madsen MScholliers CSinger J(2022)The Principles of the Flix Programming LanguageProceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3563835.3567661(112-127)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563835.3567661
Cheng XDevecsery DFalsafi BFerdman MLu SWenisch T(2022)Creating concise and efficient dynamic analyses with ALDAProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507760(740-752)Online publication date: 28-Feb-2022
https://dl.acm.org/doi/10.1145/3503222.3507760
Kouhounestani MLee W(2022)Datalog Static Analysis in SecrecyIEEE Access10.1109/ACCESS.2022.317784110(56179-56192)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3177841
Show More Cited By

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 Issue’s Table of Contents