[HN Gopher] Souffle: A Datalog Synthesis Tool for Static Analysis
___________________________________________________________________
Souffle: A Datalog Synthesis Tool for Static Analysis
Author : nickmain
Score : 19 points
Date : 2022-11-30 19:39 UTC (3 hours ago)
(HTM) web link (souffle-lang.github.io)
(TXT) w3m dump (souffle-lang.github.io)
| NeutralForest wrote:
| I sometimes see posts about Datalog & Co being posted here. I
| must say I don't understand where and when this is used. Like, I
| see the home page, I see the example page and I still don't
| understand. Is there any actual application using this? What for?
| burakemir wrote:
| (Mangle was posted recently which I like so I am a bit biased)
|
| Datalog is a formalism like relational algebra but additionally
| supports recursion.
|
| So it can roughly play the role of SQL. Compiler writers have
| used it to query their symbol tables and identify patterns for
| example (seems to be the origin of Souffle, "static analysis").
|
| I believe the reemergence of datalog is at least in part due to
| compute and memory being more plentiful so it is more
| affordable and practical to use a declarative query language. A
| lot of databases (or the part that is relevant for answering a
| particular query) comfortably fits in a single machine's memory
| and an expressive query language is fun to use. There is also
| an incremental evaluation story.
|
| Another potential reason is that the logical data model makes
| it easy to represent any kind of data without schema changes
| and such.
|
| A lot of programs end up either doing SQL or something SQL-
| like. There are therefore many applications of such datalog
| like languages.
|
| In many places where people use custom "rule languages" they
| could use datalog instead. (edited: typo & rule languages)
| lukashrb wrote:
| As I understand, implicit joins are another selling point
| mechtaev wrote:
| Souffle Datalog is used for defining program analyses in such
| projects like Doop [1] for Java and cclyzer++ [2] for LLVM.
|
| GitHub's CodeQL [3] is another Datalog dialect used for
| detecting bugs and vulnerabilities.
|
| Datomic [4] is a database that uses Datalog as the query
| language.
|
| [1] https://bitbucket.org/yanniss/doop/src/master/
|
| [2] https://github.com/GaloisInc/cclyzerpp
|
| [3] https://codeql.github.com/
|
| [4] https://www.datomic.com/
| jitl wrote:
| You could theoretically use Datalog anywhere you're currently
| using a SELECT SQL statement - it's a declarative way to
| produce a set of tuples given some existing sets of tuples.
|
| But, Datalog is much better at _deductive_ reasoning compared
| to SQL. There 's a great interactive tutorial here:
| https://percival.ink/
|
| You can also see how Souffle itself can be useful in this blog
| post: https://ianthehenry.com/posts/drinking-with-datalog/
|
| That post describes building a recipe engine that can tell you,
| given a bunch of recipes + the current contents of your bar
| cart, what drinks you can make, as well as giving you top
| ingredients you could buy that would allow you to make new
| drinks. It's quite a readable walkthrough of a very practical
| application of Datalog/Souffle in a place where SQL would
| certainly struggle.
| rad_gruchalski wrote:
| Not Datalog but inspired by Datalog:
| https://www.openpolicyagent.org/docs/latest/policy-language/.
___________________________________________________________________
(page generated 2022-11-30 23:00 UTC)