Continuously Reasoning about Programs using Differential Bayesian Inference

被引:14
作者
Heo, Kihong [1 ]
Raghothaman, Mukund [1 ]
Si, Xujie [1 ]
Naik, Mayur [1 ]
机构
[1] Univ Penn, Philadelphia, PA 19104 USA
来源
PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19) | 2019年
基金
美国国家科学基金会;
关键词
Static analysis; software evolution; continuous integration; alarm relevance; alarm prioritization; STATIC ANALYSIS; LINES; BUGS;
D O I
10.1145/3314221.3314616
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Programs often evolve by continuously integrating changes from multiple programmers. The effective adoption of program analysis tools in this continuous integration setting is hindered by the need to only report alarms relevant to a particular program change. We present a probabilistic framework, Drake, to apply program analyses to continuously evolving programs. Drake is applicable to a broad range of analyses that are based on deductive reasoning. The key insight underlying Drake is to compute a graph that concisely and precisely captures differences between the derivations of alarms produced by the given analysis on the program before and after the change. Performing Bayesian inference on the graph thereby enables to rank alarms by likelihood of relevance to the change. We evaluate Drake using SparrowDa static analyzer that targets buffer-overrun, format-string, and integer-overflow errorsDon a suite of ten widely-used C programs each comprising 13k-112k lines of code. Drake enables to discover all true bugs by inspecting only 30 alarms per benchmark on average, compared to 85 (3x more) alarms by the same ranking approach in batch mode, and 118 (4x more) alarms by a differential approach based on syntactic masking of alarms which also misses 4 of the 26 bugs overall.
引用
收藏
页码:561 / 575
页数:15
相关论文
共 57 条
  • [1] Abiteboul S., 1994, FDN DATABASES LOGICA, V1st
  • [2] [Anonymous], TECHNICAL REPORT
  • [3] Ball Thomas, 2002, P 29 ACM SIGPLAN S P, P1
  • [4] Barthe Gilles, 2011, FORMAL METHODS FM 20, P200
  • [5] A Few Billion Lines of Code Later Using Static Analysis to Find Bugs in the Real World
    Bessey, Al
    Block, Ken
    Chelf, Ben
    Chou, Andy
    Fulton, Bryan
    Hallem, Seth
    Henri-Gros, Charles
    Kamsky, Asya
    McPeak, Scott
    Engler, Dawson
    [J]. COMMUNICATIONS OF THE ACM, 2010, 53 (02) : 66 - 75
  • [6] A static analyzer for large safety-critical software
    Blanchet, B
    Cousot, P
    Cousot, R
    Feret, J
    Mauborgne, L
    Miné, A
    Monniaux, D
    Rival, X
    [J]. ACM SIGPLAN NOTICES, 2003, 38 (05) : 196 - 207
  • [7] Bravenboer M, 2009, OOPSLA 2009, CONFERENCE PROCEEDINGS, P243
  • [8] Moving Fast with Software Verification
    Calcagno, Cristiano
    Distefano, Dino
    Dubreil, Jeremy
    Gabi, Dominik
    Hooimeijer, Pieter
    Luca, Martino
    O'Hearn, Peter
    Papakonstantinou, Irene
    Purbrick, Jim
    Rodriguez, Dulma
    [J]. NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 3 - 11
  • [9] Campbell Ann, 2013, SONARQUBE IN ACTION
  • [10] Hyperproperties
    Clarkson, Michael
    Schneider, Fred
    [J]. JOURNAL OF COMPUTER SECURITY, 2010, 18 (06) : 1157 - 1210