An automated resource analysis technique is introduced, targeting a Call-By-Push-Value abstract machine, with memory prediction as a practical goal. The machine has a polymorphic and linear type system enhanced with a first-order logical fragment, which encodes both low-level operational semantics of resource manipulations and high-level synthesis of algorithmic complexity. Resource analysis must involve a diversity of static analysis, for escape, aliasing, algorithmic invariants, and more. Knowing this, we implement the Automated Amortized Resource Analysis framework (AARA) from scratch in our generic system. In this setting, access to resources is a state-passing effect which produces a compile-time approximation of runtime resource usage. We implemented type inference constraint generation for our calculus, accompanied with an elaboration of bounds for iterators on algebraic datatypes, for minimal ML-style programming languages with Call-by-Value and Call-By-Push-Value semantics. The closed-formed bounds are derived as multivariate polynomials over the integers. This now serves as a base for the development of an experimental toolkit for automated memory analysis of functional languages.

翻译：本文介绍了一种面向调用-压值抽象机的自动资源分析技术，以内存预测为实际目标。该机器采用增强了一阶逻辑片段的多态线性类型系统，该系统既能编码资源操作的低层操作语义，又能编码算法复杂性的高层综合。资源分析必须涉及多种静态分析，包括逃逸分析、别名分析、算法不变式分析等。基于此，我们在通用系统中从零实现了自动摊销资源分析框架。在该框架中，资源访问被建模为状态传递效应，可生成运行时资源使用量的编译时近似值。我们实现了该演算的类型推断约束生成，并针对代数数据类型上的迭代器进行了界限推导，适用于具有传值和调用-压值语义的最小化ML风格编程语言。闭式界限被推导为整数上的多元多项式。这为开发函数式语言自动内存分析的实验工具包奠定了基础。