Generation And Application Of Functional Constraint Based On API Documentation

Specifications play an important role in software engineering,which can be easily processed by analysis tools to understand the semantics of complex programs.With the widespread use of software libraries,generating specifications for library APIs has become an emerging need.We have studied a kind of software engineering approaches,which use SMT formulas as program specifications.However,such specifications are absent currently: manual writing can be costly and error-prone,while symbolic execution is more practical and reliable,but insufficient in handling API invocations.To facilitate symbolic execution engines to process API invocations,we aim to generate functional constraints in SMT for library APIs,which reflect the program state transformation caused by the APIs.There are two kinds of related work about specification generation,the first is based on program analysis and the second is based on documentation analysis.Both of them are not applicable to generate functional constraints because,they only focus on parts of the program semantics instead of the input-output behavior,and many of them rely on heuristic rules,which limits the generalizability and scalability.Based on the related work,we studied some typical libraries' API documentations and found these documents are highly abstract and has clear hierarchy,complete functional descriptions,and standardized writing format.Generating functional constraints from API documentations has the advantages of masking code implementation complexity and facilitating integration with domain knowledge.In this paper,we systematically study the generation of functional constraints based on API documentation and their application in symbolic execution:We propose the Doc2 SMT approach to generate strong functional constraints for library APIs based on their documentations.First,Doc2 SMT uses the general translation rules to translate the API descriptions into candidate OCL expressions.Second,Doc2 SMT guides users to construct a domain model,and finds out the well-formed expressions based on the domain model.Third,Doc2 SMT translates the OCL expressions into SMT formulas and checks the functional consistency between the SMT constraints and the API code.Based on the proposed approach,we conduct application research on improving the symbolic execution of API invocations and propose the Ex SPF approach to inject API functional constraints into the SPF symbolic execution engine.Ex SPF adapts the interpretation of invoke instructions and extends the path condition parser to insert the API constraint into current path constraint,instead of analyzing the API code.Ex SPF listens the execution of return instructions to collect path constraints.We implemented these approaches and conducted experiments for evaluation.For the 259 methods of 10 container classes collected from the JDK collections framework,Doc2 SMT managed to generate valid SMT constraints,which passed the dynamic validation,for 182 methods,180 of them are consistent with the methods' behavior,and the average generation time is about 2 minutes per method.Ex SPF generated 699 tests for the 16 static utility methods from the JDK and Apache collections libraries,which is 17.5 times the number of tests generated by SPF,the average generation time is about 0.55 seconds per test.