no description available

Fuqi Jia

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Rui Han

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Xutong Ma

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Baoquan Cui

Institute of Software at Chinese Academy of Sciences, China

Minghao Liu

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Pei Huang

Stanford University

United States

Feifei Ma

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Jian Zhang

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Third-party Python modules are usually implemented as binary extensions by using native code (C/C++) to provide additional features and runtime acceleration. In native code, the heap-allocated PyObjects are managed by the reference counting mechanism provided in Python/C APIs for automatic reclaiming. Hence, improper refcount manipulations can lead to memory leaks and use-after-free problems, and cannot be detected by simply pairing the occurrence of source and sink points. To detect such problems, state-of-the-art approaches have made groundbreaking contributions to identifying inappropriate final refcount values before returning from native code to Python. However, not all problems can be exposed at the end of a path. To detect those hidden in the middle of a path in native code, it is also crucial to track the lifecycle state of PyObjects through the refcount and lifecycle operations in API calls.

To achieve this goal, we propose the PyObject State Transition Model (PSTM) recording the lifecycle states and refcount values of PyObjects to describe the effects of Python/C API calls and pointer operations. We track state transitions of PyObjects with symbolic execution based on the model, and report problems when a statement triggers a transition to buggy states. The program state is also expanded to handle pointer nullity checks and smart pointers of PyObjects. We conduct experiments on 12 open-source projects and detect 259 real problems out of 280 reports, which is twice as many bugs as state-of-the-art approaches. We submit 168 real bugs to those active projects, and 106 issues are either confirmed or resolved.

Xutong Ma

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Jiwei Yan

Institute of Software at Chinese Academy of Sciences, China

China

Hao Zhang

Institute of Software, Chinese Academy of Sciences

Jun Yan

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Jian Zhang

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

The satisfiability problem modulo the nonlinear real arithmetic (NRA) theory serves as the foundation for a wide range of important applications, such as model checking, program analysis, and software testing. However, due to the high computational complexity, developing efficient solving algorithms for this problem has consistently presented a substantial challenge. We present a hybrid SMT(NRA) solver, called NRAgo, which combines the efficiency of gradient-based optimization method with the completeness of algebraic solving algorithm. With our approach, the practical performance on many satisfiable instances is substantially improved. The experimental evaluation shows that NRAgo achieves remarkable acceleration effects on a set of challenging SMT(NRA) benchmarks that are hard to solve for state-of-the-art SMT solvers.

Minghao Liu

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Kunhang Lv

Institute of Software, Chinese Academy of Sciences

China

Pei Huang

Stanford University

United States

Rui Han

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Fuqi Jia

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Yu Zhang

Institute of Software, Chinese Academy of Sciences

Feifei Ma

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Jian Zhang

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

The fundamental asynchronous thread (java.lang.Thread) in Java can be easily misused, due to the lack of deep understanding for garbage collection and thread interruption mechanism. For example, a careless implementation of asynchronous thread may cause no response to the interrupt mechanism in time, resulting in unexpected thread-related behaviors, especially resource leak/waste. Currently, few works aim at these misuses and related works adopt either the dynamic approach which lacks effective inputs or the static path-sensitive approach with high time consumption due to the path explosion, causing false negatives. We have found that the behavior of threads and the interaction between threads and its referencing objects can be abstracted. In this paper, we propose an event analysis approach to detect the defects in Java programs and Android apps, which focuses on the existence or the order of the events to reduce the false negatives. We extract the misuse-related events, containing the thread events and the destroy events of the object referenced by the thread. Then we analyze the events with loop identification, happens-before relationship construction and alias determination. Finally, we implement an automatic tool named Leopard and evaluate it on real world Java programs and Android apps. Experiments show that it is efficient when comparing with the existing approach (misuse: 723 vs 47, time: 60s vs 30min), which also outperforms the existing work in precision. The manual check indicates that Leopard is more efficient and effective than existing work. Besides, 66 issues reported by us have been confirmed and 21 of them have been fixed by developers.

Baoquan Cui

Institute of Software at Chinese Academy of Sciences, China

MiaoMiao Wang

Technology Center of Software Engineering, ISCAS, China. University of Chinese Academy of Sciences, China.

Chi Zhang

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Jiwei Yan

Institute of Software at Chinese Academy of Sciences, China

China

Jun Yan

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Jian Zhang

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China