Soundness
保守近似:<br> 分析会捕获所有程序行为,<br>或,分析结果为程序的所有可能执行建模。
我们可以对实际程序进行完全合理的分析吗?
学术界
几乎所有已发布的全程序分析都不适用于实际的编程语言。
工业界
几乎所有现实的全程序静态分析工具(例如,错误检测,安全分析等)都必须做出unsound choices。
Hard Language Features for Static Analysis<br>//静态分析难以分析的语言特征
Java
Reflection(反射), native code(本机代码), dynamic class loading(动态类加载), etc.
JavaScript
eval, document object model (DOM)(文档对象模型), etc.
C/C++
Pointer arithmetic(指针算术), function pointers(函数指针), etc.
Hard-to-analyze features
难以分析的特征:对这些特征采取激进的保守处理可能会使分析过于不精确而无法扩展,从而使分析无用。
对这些特征采取激进的保守处理造成的结果
一般来说,<br>声称的sound的静态分析,<br>在实施过程中拥有完善的核心。<br>也就是说,大多数语言功能都过于近似,<br>而一些特定的 and/or 困难的被低估了。
难以分析的语言特征的处理,<br>通常被省略,<br>或仅在论文的某些实施/评估部分中以随意的态度被提及。
无法正确处理某些难以分析的语言特征(例如Java反射)可能会对分析结果产生深远影响。
然后声称论文的合理性可能会误导读者
对于非专家,他们可能会错误地得出结论,认为分析是正确的并且自信地依赖于分析结果。
对于专家来说,他们仍然很难解释分析结果(分析的sound,速度,精确度如何),而又没有明确说明他们如何对待那些重要且难懂的语言特征。
Soundiness
真相(Truthiness):某人的“真相(truth)” 在没有任何事实或证据的情况下,凭直觉相信自己是真实的.
良好的(soundy)分析通常意味着该分析大部分是正确的(sound),<br>并且针对困难的/特定的(hard/specific)语言特征具有公认的(well-identified)不正确(unsound)处理。
Soundness, Soundiness and Unsoundness
sound
正确的(sound)分析需要捕获所有动态行为。
soundy
合理的(soundy)分析旨在捕获具有某些分析困难的语言特征的所有动态行为,这些特征在合理的范围内被不合理地(unsoundly)处理。
unsound
不合理的(unsound)分析故意忽略其设计中的某些行为,以提高效率,精度或可访问性。