The problem of finding a constant bound on a term given a set of assumptions has wide applications in optimization as well as program analysis. However, in many contexts the objective term may be unbounded. Still, some sort of symbolic bound may be useful. In this paper we introduce the optimal symbolic-bound synthesis problem, and a technique that tackles this problem for non-linear arithmetic with function symbols. This allows us to automatically produce symbolic bounds on complex arithmetic expressions from a set of both equality and inequality assumptions. Our solution employs a novel combination of powerful mathematical objects -- Gr\"obner bases together with polyhedral cones -- to represent an infinite set of implied inequalities. We obtain a sound symbolic bound by reducing the objective term by this infinite set. We implemented our method in a tool, AutoBound, which we tested on problems originating from real Solidity programs. We find that AutoBound yields relevant bounds in each case, matching or nearly-matching upper bounds produced by a human analyst on the same set of programs.

翻译：在给定一组假设条件下寻找项上的常数界问题，在优化和程序分析中具有广泛应用。然而在许多实际场景中，目标项可能是无界的，此时符号界仍具有实用价值。本文提出了最优符号界合成问题，并发展了一种针对带函数符号的非线性算术的求解技术。该技术能够从等式和不等式假设集合中自动生成复杂算术表达式的符号界。我们的解决方案创新性地结合了两种强大的数学工具——Gröbner基与多面体锥——来表示无限个隐含不等式集合，并通过该无限集合约简目标项以获得可靠的符号界。我们将该方法实现为工具AutoBound，并在来自真实Solidity程序的问题集上进行了测试。实验表明，AutoBound在每个案例中都能生成相关界，其性能与人类分析师对同一程序集生成的上界相当或接近吻合。