Detection And Repair Of Integer Defects In C Programs

Integer defects are bound to finite machine representation of integers,and possibly lead to serious software failures and vulnerabilities.Manual code review usually fails for integer defects which reside deeply in the program and manifests only for corner inputs.Furthermore,due to the complicated semantics of C integers,repairing integer defects is error-prone even for experts.To achieve precise and efficient integer defect detection and repair,our research is conducted in 3 bottom-up levels: computational logic,static analysis and program repair.Our main contributions are summarized as follows.1.A sound and complete framework for parallelizing SMT solving for multi-core systems,namely LDC,is proposed.LDC is instantiated in the quantifier-free theory of equality,and the decision procedure terminates.Our approach is implemented as a parallelized SMT solver PZ3.The experimental results have shown its superior performance on SMT-LIB benchmarks and random problems.Furthermore PZ3 has competitive performance over the state-of-the-art portfolio-based SMT solver.2.In order to precisely reason on program semantics locally with high efficiency,a compositional static analysis framework,namely C2 PA,is proposed.This dissertation proves the soundness of C2 PA and proposes a new analysis under C2 PA for reasoning on integer semantics of C programs.Our approach is implemented as a static analyzer Tsmart-BD.The experimental results show that Tsmart-BD outperforms the state-of-the-art tools on standard benchmarks as its false-negative rate and false-positive rate are 0.0% and 12.7%,respectively.Moreover,Tsmart-BD finishes a complete analysis on Vim(which has over 320 k LOC)within 7.5min.3.Two approaches for automating C integer defect repair are proposed:(1)elevating precision of integer arithmetic in C programs to make the compiled executables have integer errors eliminated,(2)generating fixes for detected integer defects based on typical fixing patterns.Two approaches are implemented as the tools CInt Fix and Int PTI,respectively.All the target defects in the standard benchmarks are correctly repaired by both tools.On open-source code,CInt Fix transforms 556.416 k LOC at the rate of 1.18 k LOC/s;Int PTI is capable to prevent unnecessary fixes on 96.3%critical program sites and the runtime overhead introduced by fixes is about 0.5%.Our approaches are integrated to the software analysis toolkit Tsmart which is applied to the development of the embedded software in a realistic train control system.67 new integer defects in total are detected and correctly repaired.