Patch correctness assessment represents a crucial step in the patch validation process, with the potential to enhance the practical adoption of automated program repair (APR) techniques and substantially reduce validation costs. While some automated techniques have been proposed for assessing patch correctness, they primarily focus on either ranking patches based on their likelihood of being correct or classifying them as correct or incorrect without offering any further explanatory information. In this paper, we introduce FIXCHECK, a novel approach that combines random testing and large language models to automatically generate fault-revealing tests for potentially incorrect patches. To achieve this, FIXCHECK employs a two-fold process: Firstly, a random testing procedure generates a comprehensive set of test cases. Secondly, a large language model is utilized to derive meaningful assertions for each test case. Additionally, FIXCHECK incorporates a selection and prioritization mechanism, which evaluates the generated tests executed on the patched program and discards or ranks them based on their likelihood of revealing faults in the patch. To assess the effectiveness of our approach, we conducted evaluations on a benchmark comprising 160 patches, encompassing both patches created by developers and patches generated by APR tools. The results demonstrate that FIXCHECK effectively generates fault-revealing tests for 62 % of incorrect patches written by developers, with a high level of confidence. Furthermore, it complements existing patch correctness assessment techniques by providing fault-revealing tests for up to 50% of the incorrect patches identified by state-of-the-art techniques.

Patch correctness assessment aims at effectively detecting overfitted patches, i.e., patches that causes all tests to pass but do not actually fix the bug. Although several automated techniques for assessing patch correctness have been proposed, these techniques typically yield a binary result (correct/incorrect) without providing any additional information explaining the rationale behind the decision of classifying a patch as correct or incorrect. This tool demo paper presents FixCheck, a tool based on static analysis, random testing and Large Language Models (LLMs), that seeks to improve the patch correctness analysis process by providing fault-revealing tests for potentially incorrect patches. To this end, FixCheck first employs static analysis and random testing to generate a comprehensive set of test cases that are similar to the original failing test case. Then, FixCheck relies on LLMs to derive meaningful assertions for each new test case. Finally, FixCheck executes the generated tests, and those that fail are selected and prioritized based on their likelihood of revealing a defect in the patch.

Lazy initialization enables symbolic execution for programs with heap-allocated inputs. It starts the program execution with a symbolic heap and concretizes it on demand as the program accesses it. However, the main challenge of lazy initialization is efficiently determining whether the current symbolic heap becomes infeasible with respect to the program’s precondition. Pruning infeasible heaps is crucial to avoid significant runtime overhead and false alarms.In this paper, we propose PLI (Precise Lazy Initialization), an approach that precisely decides whether there exists a concretization of the current symbolic heap that satisfies the program’s precondition. Unlike previous approaches, PLI also takes into account the constraints in the path condition to determine the feasibility of the current symbolic heap. Furthermore, PLI allows preconditions to be specified as standard operational predicates for concrete structures, eliminating the need for additional specifications tailored to symbolic heaps.In our empirical evaluation, PLI demonstrated comparable performance to existing lazy approaches while reducing the number of explored paths by 43% (all infeasible) and eliminating all false alarms in the analysis. Moreover, PLI exhibited faster execution and better scalability compared to "eager" (enumeration-based) approaches, achieving a 67% reduction in explored paths.

Android apps interact with their environment extensively, which can result in flaky, slow, or hard-to-debug tests. Developers often address these problems using test doubles---developer-defined objects that replace app or library classes during test execution. Although test doubles are widely used, there is limited understanding of how they are used in practice. To bridge this gap, we present an in-depth empirical study that aims to shed light on how developers create and use test doubles in Android apps. In our study, we first analyze a dataset of 1,006 apps with publicly available test suites to identify which frameworks and approaches developers most commonly use to create test doubles. We then investigate several research questions by studying how test doubles defined using these popular frameworks are created and used in the ten apps in the dataset that define the highest number of test doubles using these frameworks. Our results, based on the analysis of 2,365 test doubles that replace a total of 784 classes, provide insight into the types of test doubles used within Android apps and how they are utilized. Our results also show that test doubles used in Android apps and traditional Java test doubles differ in at least some respect. Finally, our results show that test doubles can introduce test smells and even mistakes in the test code. In the paper, we also discuss some implications of our findings that can help researchers and practitioners working in this area and guide future research.

Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs’ fields on demand, as the program under analysis accesses them. However, when the program’s assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE’s performance. repOK can only decide the feasibility of fully concrete structures, and thus previous work relied on manually crafted specifications designed to decide the (in)validity of partially symbolic inputs, to avoid producing spurious symbolic structures. However, these additional specifications require significant further effort from the developers.