So You Want To Analyze Scheme Programs With Datalog?
summary
Implements a modified CESK/AAM with mCFA that uses flat closures and a push-down-for-free allocator, compiles a substantial Scheme subset into CSV EDB facts and encodes the transition rules in Soufflé Datalog. Evaluates on Van Horn’s worst-case “padding” term (32 let clauses, exponential results for insufficient k), shows >1-context analyses finish quickly while 1-CFA explodes, and finds Soufflé’s OpenMP parallelism degrades performance so single-threaded runs are best; globalized store differs from the formal semantics.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:15Outline
- 1:24Control Flow
- 2:01Abstract Interpretation
- 2:50Abstract Interpreter
- 3:47Abstract Machines
- 5:11Precision
- 6:36Contexts
- 8:27Datalog
- 9:31Implementation
- 11:17Context Creation
- 12:40Datalog Implementation
- 14:10Operational Semantics
- 15:20Reconstruct a worst case
- 16:50The worst case
- 17:35Souffle
- 18:41Future Plans
related talks
21mFlow-Analysis-Based Closure Optimization
34mChecking a Denotational Semantics of Scheme in Agda
22mSatisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
46mMechanizing Abstract Interpretation
15mTool Talk: Soufflé
30mAnalyzing Programs with SMT Solvers
15mFormulog: Datalog for SMT-Based Static Analysis
01h 38mGHC Core Optimisations