Summary-Based Compositional Analysis for Soft Contract Verification

Design-by-contract is a development best practice
that requires the interactions between software components to
be governed by precise specifications, called contracts. Contracts
often take the form of pre- and post-conditions on function
definitions, and are usually translated to (frequently redundant)
run-time checks. So-called soft contract verifiers have been
proposed to reduce the run-time overhead introduced by such
contract checks by verifying parts of the contracts ahead of
time, while leaving those that cannot be verified as residual runtime checks. In the state of the art, static analyses based on
the Abstracting Abstract Machines (AAM) approach to abstract
interpretation have been proposed for implementing such soft
verifiers. However, these approaches result in whole-program
analyses which are difficult to scale.
In this paper, we propose a scalable summary-based compositional analysis for soft contract verification, which summarises
both the correct behaviour and erroneous behaviour of all
functions in the program using symbolic path conditions. Information from these summaries propagates backwards through
the call graph, reducing the amount of redundant analysis
states and improving the overall performance of the analysis.
This backwards flow enables path constraints associated with
erroneous program states to flow to call sites where they can be
refuted, whereas in the state of the art they can only be refuted
using the information available at the original location of the
error.
To demonstrate our improvements in both precision and performance compared to the state-of-the-art, we implemented our
analysis in a framework called MAF (short for Modular Analysis
Framework) — a framework for the analysis of higher-order
dynamic programming languages. We conducted an empirical
study and found an average performance improvement of 21%,
and an average precision improvement of 38.15%.