Almost-correct specifications: a modular semantic framework for assigning confidence to warnings
Almost-correct specifications: a modular semantic framework for assigning confidence to warnings
复制标题
几乎正确的规范：用于为警告分配置信度的模块化语义框架
DOI：
10.1145/2491956.2462188
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Shuvendu K. Lahiri
中科院分区：
文献类型：
--
作者：
Sam Blackshear;Shuvendu K. Lahiri
由于需要精确的环境规范（前置条件和被调用方后置条件），模块化断言检查器受到错误警报的困扰。即使是完全精确的检查器也会在不受约束或部分规范所允许的最糟糕的环境下报告断言失败。无法排除过度对抗的环境使得此类检查器对开发人员的吸引力降低，并严重限制了此类工具在开发周期中的采用。在这项工作中，我们提出了一个参数化的框架，优先级的断言失败报告的模块化验证，抑制警告过于恶魔的环境的目标。我们将其形式化为几乎正确的规范，作为天使规范（在一组谓词上）的最小削弱，以排除任何过程内的死代码。我们的工作的灵感和概括的语义不一致检测的一些方面。我们的表述使我们能够将这一想法提升到一般的警告类别。我们已经开发了一个原型acspec，我们用它来探索框架的一些实例，并报告了一组不同的C基准测试的初步结果。
Modular assertion checkers are plagued with false alarms due to the need for precise environment specifications (preconditions and callee postconditions). Even the fully precise checkers report assertion failures under the most demonic environments allowed by unconstrained or partial specifications. The inability to preclude overly adversarial environments makes such checkers less attractive to developers and severely limits the adoption of such tools in the development cycle. In this work, we propose a parameterized framework for prioritizing the assertion failures reported by a modular verifier, with the goal of suppressing warnings from overly demonic environments. We formalize it almost-correct specifications as the minimal weakening of an angelic specification (over a set of predicates) that precludes any dead code intraprocedurally. Our work is inspired by and generalizes some aspects of semantic inconsistency detection. Our formulation allows us to lift this idea to a general class of warnings. We have developed a prototype acspec, which we use to explore a few instantiations of the framework and report preliminary findings on a diverse set of C benchmarks.