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

标题：SHF：Small：基于约束的程序分析的新前沿基于约束的分析是一种流行的程序分析方法：它允许将分析规范与分析实现分开，它通过利用现成求解器中的先进技术来实现复杂的实现，并提供自然的程序规范作为约束。这个项目提出了Dominos，一个框架，通过支持程序分析的常见和新兴用例的自动合成，扩展了基于约束的分析的好处，例如找到好的抽象，分析不完整的程序，以及合并用户反馈。该项目的智力价值在于从根本上推进了需求驱动、组合和基于学习的分析技术。通过一劳永逸地自动合成用例，Dominos放大了基于约束的分析的传统好处，使分析设计人员不必为分析重新实现那些用例。该项目的更广泛的意义和重要性在于通过使程序分析更加自动化、可伸缩和灵活来增强程序分析的适用性和有用性。包含这些分析的构件将在可靠性、安全性、性能和能源效率方面提高软件质量。Domos还将通过允许分析用户根据他们的反馈调整分析来提高他们的生产力。Dominos自动合成以Datalog(一种流行的声明性逻辑编程语言)表示的任何程序分析的用例实现。现有的基于约束的分析框架主要集中于解决硬约束，而Dominos也适应在程序分析的不同用例中自然产生的软约束，例如，对各种权衡、分析用户的直觉和缺失的程序规范进行建模。通过将Dominos应用于三个重要的用例：客户驱动的分析、基于摘要的分析和用户引导的分析，演示了Dominos的多功能性。尽管它们各有不同，但所有三个用例都需要解决最大可满足性(MaxSAT)问题的实例，该问题由硬(不可侵犯)约束和软(可违反)约束的组合组成。求解这种混合约束不仅在计算上很困难，而且还带来了指定软约束的权重或置信度的问题。Domos开发MaxSAT优化，包括需求驱动、组合和基于学习的方法，这些方法是通用的，独立于任何分析、用例或解算器，旨在扩展到远远超出现有MaxSAT解算器能力范围的实例。

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.