A Query-Based Constraint Acquisition Approach for Enhanced Precision in Program Precondition Inference

Program annotations in the form of function pre/postconditions play a crucial role in various software engineering and program verification tasks. However, the frequent unavailability of these annotations necessitates manual retrofitting. This paper shows how constraint acquisition, a learning framework derived from constraint programming and version space learning, can be extended for automatically inferring program preconditions. Our approach performs this inference in a black-box manner through automatic query generation and input-output observations of program executions. We introduce PreCA, the first-ever precondition inference framework leveraging query-based constraint acquisition. Notably, we specialize PreCA to handle memory-related preconditions on binary code, which pose significant challenges in data and information management systems. In contrast to prior black-box techniques, PreCA provides well-defined guarantees. Specifically, it employs a sound and complete method to generate preconditions consistent with all the observed input-output relationships of the program. Furthermore, empirical evaluations on our benchmark demonstrate that PreCA outperforms the results of state-of-the-art approaches, delivering comparable or superior results in 5s, as opposed to the 1-hour runtime of existing approaches on identical machines. We also present two successful use cases from the standard libc and the mbedtls cryptographic library. PreCA notably infers for the former one a more precise precondition than specified in the documentation.