Constraints solving takes a large proportion of time in symbolic execution. Z3 Solver [5], the state-of-the-art tool, specializes in constraint solving and can solve constraints with customized strategies. The performance of Z3 Solver varies for different groups of constraints, and a well-performed strategy for a specific group does not convey the consistent performance for other groups. Numerous approaches address the acceleration issue (Proteus [13], ISAC [17], SUNNY [3], StartEvo [24]) by inventing algorithms or learning to choose a well-performed strategy. We rephrase the acceleration problem into a search space coverage problem. Besides, we extend the coverage of the search space by embedding reinforcement learning with a natural language processing model. We evaluate our framework...[ Read more ]

Constraints solving takes a large proportion of time in symbolic execution. Z3 Solver [5], the state-of-the-art tool, specializes in constraint solving and can solve constraints with customized strategies. The performance of Z3 Solver varies for different groups of constraints, and a well-performed strategy for a specific group does not convey the consistent performance for other groups. Numerous approaches address the acceleration issue (Proteus [13], ISAC [17], SUNNY [3], StartEvo [24]) by inventing algorithms or learning to choose a well-performed strategy. We rephrase the acceleration problem into a search space coverage problem. Besides, we extend the coverage of the search space by embedding reinforcement learning with a natural language processing model. We evaluate our framework on ten open source projects from Github. We have obtained a positive result: our framework has improved the search space coverage and accelerated Z3 Solver with a lower bound of six times.