The first open-source AI-driven tool for automatically generating system-level test cases (also known as fuzzing) for web/enterprise applications. Currently targeting whitebox and blackbox testing of Web APIs, like REST, GraphQL and RPC (e.g., gRPC and Thrift).
This pull request introduces significant refactoring to improve the design and interfaces of the EvoMaster codebase related to SMT (Satisfiability Modulo Theories) constraint solving. The main changes are summarized below:
In Java:
Solver Package Refinement: The solver package now exclusively contains the solver for Z3 and the SMTLib interface, which is utilized to avoid handling strings directly.
The solver no longer needs to understand schema, columns, or tables. It focuses solely on SMTLib constraint solving.
SMTResultParser: A new class created to transform a string response from Z3 into an SMTLibValue object. This streamlines the process of interpreting solver results.
SMTLib Class: This class defines an SMTLib constraint. It includes a toString method that generates the string representation necessary for storing in a file for Z3 to execute.
In Kotlin:
New Package: A new package org.evomaster.core.solver has been created.
Circular Dependencies Resolved: Circular dependencies were addressed. The Kotlin package now handles TableDto, SchemaDto, and related classes.
DbConstraintSolver Interface: A contract for implementing database constraint solvers.
SMTLibZ3DbConstraintSolver: This class implements the DbConstraintSolver interface and utilizes the SMTLibGenerator to convert schemas and queries into valid SMT constraints for Z3.
Summary
This PR does not introduce new functionality. Instead, it refactors the existing codebase to enhance the design and interfaces, making the solution more modular and maintainable.
Pending Work
Implement table constraints as SMT constraints.
Implement the transformation of SQL query WHERE clauses into SMT constraints.
These improvements aim to create a more robust and scalable system for handling SMT constraints and solving database-related problems within EvoMaster.
Refactor of Solver Package
This pull request introduces significant refactoring to improve the design and interfaces of the EvoMaster codebase related to SMT (Satisfiability Modulo Theories) constraint solving. The main changes are summarized below:
In Java:
SMTLibValueobject. This streamlines the process of interpreting solver results.toStringmethod that generates the string representation necessary for storing in a file for Z3 to execute.In Kotlin:
org.evomaster.core.solverhas been created.TableDto,SchemaDto, and related classes.DbConstraintSolverinterface and utilizes theSMTLibGeneratorto convert schemas and queries into valid SMT constraints for Z3.Summary
This PR does not introduce new functionality. Instead, it refactors the existing codebase to enhance the design and interfaces, making the solution more modular and maintainable.
Pending Work
WHEREclauses into SMT constraints.These improvements aim to create a more robust and scalable system for handling SMT constraints and solving database-related problems within EvoMaster.