SHF: Small: New Frontiers in Constraint-Based Program Analysis

点击翻译按钮获取中文摘要

Title: SHF:Small:New Frontiers in Constraint-Based Program AnalysisConstraint-based analysis is a popular approach to program analysis: it allows to separate analysis specification from analysis implementation, it enables sophisticated implementations by leveraging advances in off-the-shelf solvers, and it provides natural program specifications as constraints. This project proposes Dominoes, a framework that extends the benefits of constraint-based analysis by enabling automatic synthesis of common and emerging use-cases of program analyses, such as finding good abstractions, analyzing incomplete programs, and incorporating user feedback. The intellectual merit of this project is to fundamentally advance demand-driven, compositional, and learning-based analysis techniques. By automatically synthesizing use-cases once and for all, Dominoes amplifies the traditional benefits of constraint-based analysis, liberating analysis designers from having to re-implement those use-cases for their analyses. The project's broader significance and importance lies in enhancing the applicability and usefulness of program analyses by making them more automated, scalable, and flexible. Artifacts embodying these analyses will improve software quality in aspects of reliability, security, performance, and energy efficiency. Dominoes will also improve the productivity of analysis users by allowing them to adapt analyses to their feedback.Dominoes automatically synthesizes implementations of use-cases for any program analysis expressed in Datalog, a popular declarative logic programming language. Existing constraint-based analysis frameworks predominantly focus on solving hard constraints, whereas Dominoes also accommodates soft constraints that arise naturally in diverse use-cases of program analysis, e.g., to model various tradeoffs, intuitions of analysis users, and missing program specifications. The versatility of Dominoes is demonstrated by applying it to three important use-cases: client-driven analysis, summary-based analysis, and user-guided analysis. Despite their diversity, all three use-cases entail solving instances of the maximum satisfiability (MaxSAT) problem, which consists of a combination of hard (inviolable) constraints and soft (violable) constraints. Solving such mixed constraints is not only computationally hard but also poses the problem of specifying weights or confidences of soft constraints. Dominoes develops MaxSAT optimizations comprising demand-driven, compositional, and learning-based methods that are general and independent of any analysis, use-case, or solver, and aim to scale to instances well beyond the reach of existing MaxSAT solvers.