动态代价上的增量定量分析

在定量程序分析中，执行迹被赋予值以表示一种质量度量。此类分析涵盖重要应用，例如资源使用。众所周知，检查所有迹是不可行的，因此传统算法在一个过近似集合上进行推理。通常，由于该集合中包含了不可行路径，会导致不准确性。因此，路径敏感性是一种解决方案。然而，还有另一个导致不准确性的原因：代价模型，即每条迹分析的量化方式，是动态的。也就是说，迹的代价取决于执行该迹的上下文。因此，本已受到路径敏感性挑战的准确分析目标，现在又受到上下文敏感性的进一步挑战。在本文中，我们解决了在动态代价模型上定义的定量分析问题。我们的算法是一个“anytime”算法：它能快速生成一个答案，但如果分析资源预算允许，它会通过细化迭代逐步产生更好的解。每次迭代的结果保持可靠，但重要的是，在给定无限资源预算时必须收敛到精确分析。为了具备可扩展性，我们的算法被设计为增量的。最后，我们通过对一组实际的基准测试进行评估，证明了该方法达到了新的实用水平。