Soufflé (programming language)
From HandWiki
Short description: Parallel logic programming language
| Paradigms | Declarative, Logic programming |
|---|---|
| Family | Datalog |
| Stable release | 2.3[1]
|
| Typing discipline | Static |
| License | UPL |
| Filename extensions | .dl |
| Website | souffle-lang |
| Influenced by | |
| Datalog | |
Soufflé is an open source parallel logic programming language, influenced by Datalog. Soufflé includes both an interpreter and a compiler that targets parallel C++. Soufflé has been used to build static analyzers, disassemblers, and tools for binary reverse engineering. Soufflé is considered by academic researchers to be high-performance and "state of the art," and is often used in benchmarks in academic papers.[2][3][4]
Programming examples
Given a set of edges in a graph, the following program computes the set of (directed) paths between any two nodes. This is also known as the transitive closure of the edge relation.
.decl edge(x:number, y:number) .input edge .decl path(x:number, y:number) .output path path(x, y) :- edge(x, y). path(x, y) :- path(x, z), edge(z, y).
Features
- An interpreter[5] and a compiler[6] that targets parallel C++ (C++ that uses OpenMP). Both the interpreter and compiler use semi-naïve evaluation.[7]
- Stratified negation[8]
- Aggregation[9]
- Automatic index selection[10]
- Specialized parallel data structures,[11] including disjoint-sets,[12] B-trees,[13] and tries.[14]
- Static typing[15]
- Records and algebraic data types[16]
- A foreign function interface[17]
Related tools
In addition to a compiler and an interpreter, the Soufflé project also publishes:
- a profiler,
- a "provenance"-based debugger,[18]
- an "auto-scheduler" (also called a "join optimizer") that chooses efficient query plans based on a profile, as in profile-guided optimization.[19]
Applications
Soufflé has been used to build static analyzers, including:
- A pointer analysis for Java[20]
- A control-flow analysis for Scheme[21]
- Various analyses for smart contract languages[22]
It has also been used to build tools for binary analysis, including reverse engineering,[23] and disassemblers.[24]
References
- ↑ "Release Release 2.3 · souffle-lang/souffle" (in en). https://github.com/souffle-lang/souffle/releases/tag/2.3.
- ↑ Ketsman, Bas; Koutris, Paraschos (2022-06-28). "Modern Datalog Engines" (in English). Foundations and Trends in Databases 12 (1): 1–68. doi:10.1561/1900000073. ISSN 1931-7883. https://www.nowpublishers.com/article/Details/DBS-073.
- ↑ Gilray, Thomas; Sahebolamri, Arash; Kumar, Sidharth; Micinski, Kristopher (2022-11-21). "Higher-Order, Data-Parallel Structured Deduction". arXiv:2211.11573 [cs.PL].
- ↑ Sahebolamri, Arash; Gilray, Thomas; Micinski, Kristopher (2022-03-18). "Seamless deductive inference via macros". Proceedings of the 31st ACM SIGPLAN International Conference on Compiler Construction. CC 2022. New York, NY, USA: Association for Computing Machinery. pp. 77–88. doi:10.1145/3497776.3517779. ISBN 978-1-4503-9183-2. https://doi.org/10.1145/3497776.3517779.
- ↑ Hu, Xiaowen; Zhao, David; Jordan, Herbert; Scholz, Bernhard (2021-06-15). Artifact for Paper: An Efficient Interpreter for Datalog by De-specializing Relations. doi:10.1145/3410297. http://dx.doi.org/10.1145/3410297. Retrieved 2023-02-26.
- ↑ Scholz, Bernhard; Jordan, Herbert; Subotić, Pavle; Westmann, Till (2016-03-17). "On fast large-scale program analysis in Datalog". Proceedings of the 25th International Conference on Compiler Construction. CC 2016. New York, NY, USA: Association for Computing Machinery. pp. 196–206. doi:10.1145/2892208.2892226. ISBN 978-1-4503-4241-4. https://doi.org/10.1145/2892208.2892226.
- ↑ Jordan, Scholz & Subotić 2016.
- ↑ "Rules | Soufflé • A Datalog Synthesis Tool for Static Analysis". https://souffle-lang.github.io/rules.
- ↑ "Aggregates and Generative Functors | Soufflé • A Datalog Synthesis Tool for Static Analysis". https://souffle-lang.github.io/aggregates.
- ↑ Subotić, Pavle; Jordan, Herbert; Chang, Lijun; Fekete, Alan; Scholz, Bernhard (October 2018). "Automatic index selection for large-scale datalog computation" (in EN). Proceedings of the VLDB Endowment 12 (2): 141–153. doi:10.14778/3282495.3282500. ISSN 2150-8097. https://dl.acm.org/doi/abs/10.14778/3282495.3282500.
- ↑ Jordan, Herbert; Subotić, Pavle; Zhao, David; Scholz, Bernhard (2022-01-25). "Specializing parallel data structures for Datalog" (in en). Concurrency and Computation: Practice and Experience 34 (2). doi:10.1002/cpe.5643. ISSN 1532-0626. https://onlinelibrary.wiley.com/doi/10.1002/cpe.5643.
- ↑ Nappa, Patrick; Zhao, David; Subotić, Pavle; Scholz, Bernhard (September 2019). "Fast Parallel Equivalence Relations in a Datalog Compiler". 2019 28th International Conference on Parallel Architectures and Compilation Techniques (PACT). pp. 82–96. doi:10.1109/PACT.2019.00015. ISBN 978-1-7281-3613-4. https://ieeexplore.ieee.org/document/8891656.
- ↑ Jordan, Herbert; Subotić, Pavle; Zhao, David; Scholz, Bernhard (2019-02-16). "A specialized B-tree for concurrent datalog evaluation". Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming. PPoPP '19. New York, NY, USA: Association for Computing Machinery. pp. 327–339. doi:10.1145/3293883.3295719. ISBN 978-1-4503-6225-2. https://doi.org/10.1145/3293883.3295719.
- ↑ Jordan, Herbert; Subotić, Pavle; Zhao, David; Scholz, Bernhard (2019-02-17). "Brie". Proceedings of the 10th International Workshop on Programming Models and Applications for Multicores and Manycores. PMAM'19. New York, NY, USA: Association for Computing Machinery. pp. 31–40. doi:10.1145/3303084.3309490. ISBN 978-1-4503-6290-0. https://doi.org/10.1145/3303084.3309490.
- ↑ "Types | Soufflé • A Datalog Synthesis Tool for Static Analysis". https://souffle-lang.github.io/types. "Soufflé is a statically typed language."
- ↑ "Types | Soufflé • A Datalog Synthesis Tool for Static Analysis". https://souffle-lang.github.io/types.
- ↑ "User-Defined Functors | Soufflé • A Datalog Synthesis Tool for Static Analysis". https://souffle-lang.github.io/functors.
- ↑ Zhao, David; Subotić, Pavle; Scholz, Bernhard (2020-04-17). "Debugging Large-scale Datalog: A Scalable Provenance Evaluation Strategy". ACM Transactions on Programming Languages and Systems 42 (2): 7:1–7:35. doi:10.1145/3379446. ISSN 0164-0925. https://doi.org/10.1145/3379446.
- ↑ Arch, Samuel; Hu, Xiaowen; Zhao, David; Subotić, Pavle; Scholz, Bernhard (2022). Villanueva, Alicia. ed. "Building a Join Optimizer for Soufflé" (in en). Logic-Based Program Synthesis and Transformation. Lecture Notes in Computer Science (Cham: Springer International Publishing) 13474: 83–102. doi:10.1007/978-3-031-16767-6_5. ISBN 978-3-031-16767-6. https://link.springer.com/chapter/10.1007/978-3-031-16767-6_5.
- ↑ Antoniadis, Triantafyllou & Smaragdakis 2017.
- ↑ Silverman, Davis Ross; Sun, Yihao; Micinski, Kristopher; Gilray, Thomas (2021-07-27). "So You Want to Analyze Scheme Programs With Datalog?". arXiv:2107.12909 [cs.PL].
- ↑ Tsankov, Petar; Dan, Andrei; Drachsler-Cohen, Dana; Gervais, Arthur; Bünzli, Florian; Vechev, Martin (2018-10-15). "Securify". Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. CCS '18. New York, NY, USA: Association for Computing Machinery. pp. 67–82. doi:10.1145/3243734.3243780. ISBN 978-1-4503-5693-0. https://doi.org/10.1145/3243734.3243780.
- Brent, Lexi; Jurisevic, Anton; Kong, Michael; Liu, Eric; Gauthier, Francois; Gramoli, Vincent; Holz, Ralph; Scholz, Bernhard (2018-09-11). "Vandal: A Scalable Security Analysis Framework for Smart Contracts". arXiv:1809.03981 [cs.PL].
- Grech, Neville; Kong, Michael; Jurisevic, Anton; Brent, Lexi; Scholz, Bernhard; Smaragdakis, Yannis (2018-10-24). "MadMax: surviving out-of-gas conditions in Ethereum smart contracts". Proceedings of the ACM on Programming Languages 2 (OOPSLA): 116:1–116:27. doi:10.1145/3276486. https://doi.org/10.1145/3276486.
- Praitheeshan, Purathani; Pan, Lei; Yu, Jiangshan; Liu, Joseph; Doss, Robin (2020-09-16). "Security Analysis Methods on Ethereum Smart Contract Vulnerabilities: A Survey". arXiv:1908.08605 [cs.CR].
- ↑ Sun, Yihao; Ching, Jeffrey; Micinski, Kristopher (2021-01-12). "Declarative Demand-Driven Reverse Engineering". arXiv:2101.04718 [cs.PL].
- ↑ Flores-Montoya, Antonio; Schulte, Eric (2020-08-12). "Datalog disassembly". Proceedings of the 29th USENIX Conference on Security Symposium. SEC'20 (USA: USENIX Association): 1075–1092. ISBN 978-1-939133-17-5. https://dl.acm.org/doi/10.5555/3489212.3489273.
Sources
- Jordan, Herbert; Scholz, Bernhard; Subotić, Pavle (2016). Chaudhuri, Swarat; Farzan, Azadeh. eds. "Soufflé: On Synthesis of Program Analyzers" (in en). Computer Aided Verification. Lecture Notes in Computer Science (Cham: Springer International Publishing) 9780: 422–430. doi:10.1007/978-3-319-41540-6_23. ISBN 978-3-319-41540-6. https://link.springer.com/chapter/10.1007/978-3-319-41540-6_23.
- Antoniadis, Tony; Triantafyllou, Konstantinos; Smaragdakis, Yannis (2017-06-18). "Porting doop to Soufflé". Proceedings of the 6th ACM SIGPLAN International Workshop on State of the Art in Program Analysis. SOAP 2017. New York, NY, USA: Association for Computing Machinery. pp. 25–30. doi:10.1145/3088515.3088522. ISBN 978-1-4503-5072-3. https://doi.org/10.1145/3088515.3088522.
External links
 |  |
