Programmers care about the amount of time, memory, and energy their program require to run. This is not only a matter of ecological ethic, but also of safety: software can fail or degrade in quality when not enough resources are available.
This work aims to improve static resource analyzers by proposing a neutral formalism capable of combining several analysis techniques and of reusing them of different languages. It is based on an abstract machine and corresponding type system through the Curry-Howard correspondence. At type-level, it embeds the intuitionistic linear sequent calculus together with "parameters" at the second order. Those parameters are manipulated with the conjunctive-implicative fragment of classical first-order logic, with a user-provided signature. At term level, this corresponds to a call-by-push-value virtual machine, with explicit resource manipulation. Parameters represent characteristic quantities of data structures and computations (sizes, iteration counts, etc.)
Our type system generates, together with a typed program, a first-order constraint over the parameters used in it. Those include both the free parameter variables, but also those bounds by quantifiers. This constraint being first-order, it is amendable to SMT solving. Furthermore, in the important case of integers with signature ($mathbb{N}$, 0, 1, +, -, *), those quantifiers can be eliminated without significant loss of predictive power in cases found in the wild. This quantifier-free constraint can then be turned into an integer optimisation program, giving closed-form bounds on the values of those parameters. This provides resource bounds to programs written in the machine language. Our abstract machine admits a effect system capable of soundly encoding resource-passing without adding new primitives. This facilitates resource analysis for other languages: any compilation scheme to the machine automatically extends to a resource-aware one, which is sound regarding the original semantics.
We show the feasibility of our method through its implementation, "AutoBill". It takes as input either a ML-style call-by-value language, a Call-by-Push-Value lambda-calculus, or in machine languages. Parameters with arbitrary user-defined sorts are supported. AutoBill then generates the corresponding constraint in a standard format. The Z3 solver can then provide closed-form bounds on those parameters. The extensibility of our method is demonstrated through the addition of a monadic effect system in the ML-language, and through the encoding of AARA analyses. AutoBill supports parameters annotations for user-described size and complexity, which previous AARA implementations didn't support.