一句话：将程序外延等价推广到抽象解释诱导的抽象等价，证明任何非平凡抽象解释都会揭示程序的内涵差异。
本文把程序的外延（函数）等价推广为由抽象解释诱导的抽象等价，具体解释下的标准外延等价成为其特例。作者研究 Rice 定理等外延等价性质在抽象框架中的推广，并构造基于控制流与数据流变换的不完全性团：对任意非平凡抽象，都能生成一对在具体语义下外延等价、但在抽象语义下可区分的程序。由此得出，非平凡抽象解释必然揭示程序的内涵方面；此类不完全程序类还是图灵完备的。结果还联系了代码混淆与程序分析精度，说明抽象解释虽可靠，却可被代码变换变为不完全并产生误报。
In this paper we generalise the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations . The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.
@article{paperbot564,
title = {Abstract extensionality: on the properties of incomplete abstract interpretations},
author = {Roberto Bruni and Roberto Giacobazzi and Roberta Gori and Isabel Garcia-Contreras and Dusko Pavlovic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371096}
}