diff --git a/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/ast/SqlComparisonOperator.java b/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/ast/SqlComparisonOperator.java index 473989d0ed..7718edb773 100644 --- a/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/ast/SqlComparisonOperator.java +++ b/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/ast/SqlComparisonOperator.java @@ -2,6 +2,7 @@ public enum SqlComparisonOperator { EQUALS_TO("="), + NOT_EQUALS_TO("<>"), GREATER_THAN(">"), GREATER_THAN_OR_EQUAL(">="), LESS_THAN("<"), diff --git a/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java b/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java index d03ce20462..cebf38b411 100644 --- a/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java +++ b/core-extra/dbconstraint/src/main/java/org/evomaster/dbconstraint/parser/jsql/JSqlVisitor.java @@ -310,8 +310,11 @@ public void visit(MinorThanEquals minorThanEquals) { @Override public void visit(NotEqualsTo notEqualsTo) { - // TODO This translation should be implemented - throw new RuntimeException("Extraction of condition not yet implemented"); + notEqualsTo.getLeftExpression().accept(this); + SqlCondition left = stack.pop(); + notEqualsTo.getRightExpression().accept(this); + SqlCondition right = stack.pop(); + stack.push(new SqlComparisonCondition(left, SqlComparisonOperator.NOT_EQUALS_TO, right)); } @Override diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt index 23d16281e1..eb12789a79 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SMTConditionVisitor.kt @@ -42,9 +42,12 @@ class SMTConditionVisitor( * @return The corresponding SMT node. */ override fun visit(condition: SqlAndCondition, parameter: Void?): SMTNode { - val left = condition.leftExpr.accept(this, parameter) as AssertSMTNode - val right = condition.rightExpr.accept(this, parameter) as AssertSMTNode - return AssertSMTNode(AndAssertion(listOf(left.assertion, right.assertion))) + val left = condition.leftExpr.accept(this, parameter) + val right = condition.rightExpr.accept(this, parameter) + if (left is EmptySMTNode && right is EmptySMTNode) return EmptySMTNode() + if (left is EmptySMTNode) return right + if (right is EmptySMTNode) return left + return AssertSMTNode(AndAssertion(listOf((left as AssertSMTNode).assertion, (right as AssertSMTNode).assertion))) } /** @@ -55,8 +58,11 @@ class SMTConditionVisitor( * @return The corresponding SMT node. */ override fun visit(condition: SqlOrCondition, parameter: Void?): SMTNode { - val conditions = condition.orConditions.map { it.accept(this, parameter) as AssertSMTNode } - return AssertSMTNode(OrAssertion(conditions.map { it.assertion })) + val conditions = condition.orConditions.map { it.accept(this, parameter) } + val nonEmpty = conditions.filterIsInstance() + if (nonEmpty.isEmpty()) return EmptySMTNode() + if (nonEmpty.size == 1) return nonEmpty[0] + return AssertSMTNode(OrAssertion(nonEmpty.map { it.assertion })) } /** @@ -67,6 +73,9 @@ class SMTConditionVisitor( * @return The corresponding SMT node. */ override fun visit(condition: SqlComparisonCondition, parameter: Void?): SMTNode { + if (condition.leftOperand is SqlNullLiteralValue || condition.rightOperand is SqlNullLiteralValue) { + return EmptySMTNode() // TODO: Change this when we add support for nullable columns in the db schema + } val left = getVariableAndLiteral(condition.leftOperand) val right = getVariableAndLiteral(condition.rightOperand) diff --git a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt index 8e183f7902..a963e53dec 100644 --- a/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt +++ b/core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt @@ -14,6 +14,7 @@ import org.evomaster.core.logging.LoggingUtil import org.evomaster.core.utils.StringUtils import org.evomaster.dbconstraint.ConstraintDatabaseType import org.evomaster.dbconstraint.ast.SqlCondition +import net.sf.jsqlparser.JSQLParserException import org.evomaster.dbconstraint.parser.SqlConditionParserException import org.evomaster.dbconstraint.parser.jsql.JSqlConditionParser import org.evomaster.solver.smtlib.* @@ -114,7 +115,9 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I smt.addNode(constraint) } } catch (e: SqlConditionParserException) { - throw RuntimeException("Error parsing check expression: " + check.sqlCheckExpression, e) + LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: ${check.sqlCheckExpression}. Reason: ${e.message}") + } catch (e: JSQLParserException) { + LoggingUtil.getInfoLogger().warn("Could not translate CHECK constraint to SMT-LIB, skipping: ${check.sqlCheckExpression}. Reason: ${e.message}") } } } @@ -276,7 +279,7 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I for (foreignKey in table.foreignKeys) { val referencedTable = findReferencedTable(foreignKey) val referencedTableName = referencedTable.id.name.lowercase() - val referencedColumnSelector = findReferencedPKSelector(referencedTable, foreignKey) + val referencedColumnSelector = findReferencedPKSelector(table, referencedTable, foreignKey) for (sourceColumn in foreignKey.sourceColumns) { val nodes = assertForEqualsAny( @@ -328,13 +331,24 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I * @param foreignKey The foreign key constraint. * @return The primary key column name in the referenced table. */ - private fun findReferencedPKSelector(referencedTable: TableDto, foreignKey: ForeignKeyDto): String { + private fun findReferencedPKSelector(sourceTable: TableDto, referencedTable: TableDto, foreignKey: ForeignKeyDto): String { val referencedPrimaryKeys = referencedTable.columns.filter { it.primaryKey } - if (referencedPrimaryKeys.isEmpty()) { - throw RuntimeException("Referenced table has no primary key: ${foreignKey.targetTable}") + val sourceColumnName = foreignKey.sourceColumns.firstOrNull() + val sourceSmtType = sourceColumnName?.let { scn -> + sourceTable.columns.firstOrNull { it.name.equals(scn, ignoreCase = true) } + ?.let { TYPE_MAP[it.type.uppercase()] } } - // Assuming single-column primary keys - return referencedPrimaryKeys[0].name + if (referencedPrimaryKeys.isNotEmpty() && + (sourceSmtType == null || TYPE_MAP[referencedPrimaryKeys[0].type.uppercase()] == sourceSmtType)) { + return referencedPrimaryKeys[0].name + } + // No PK or type mismatch: find a type-compatible column + if (sourceSmtType != null) { + referencedTable.columns.firstOrNull { TYPE_MAP[it.type.uppercase()] == sourceSmtType } + ?.let { return it.name } + } + return referencedTable.columns.firstOrNull()?.name + ?: throw RuntimeException("Referenced table has no columns: ${foreignKey.targetTable}") } /** @@ -364,11 +378,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I val where = plainSelect.where if (where != null) { - val condition = parser.parse(where.toString(), toDBType(schema.databaseType)) - val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() - for (i in 1..numberOfRows) { - val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) - smt.addNode(constraint) + try { + val condition = parser.parse(where.toString(), toDBType(schema.databaseType)) + val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() + for (i in 1..numberOfRows) { + val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) + smt.addNode(constraint) + } + } catch (e: RuntimeException) { + LoggingUtil.getInfoLogger().warn("Could not translate WHERE clause to SMT-LIB, skipping: ${where}. Reason: ${e.message}") } } } @@ -390,11 +408,15 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I val onExpressions = join.onExpressions if (onExpressions.isNotEmpty()) { val onExpression = onExpressions.elementAt(0) - val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType)) - val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() - for (i in 1..numberOfRows) { - val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) - smt.addNode(constraint) + try { + val condition = parser.parse(onExpression.toString(), toDBType(schema.databaseType)) + val tableFromQuery = TablesNamesFinder().getTables(sqlQuery as Statement).first() + for (i in 1..numberOfRows) { + val constraint = parseQueryCondition(tableAliases, tableFromQuery, condition, i) + smt.addNode(constraint) + } + } catch (e: RuntimeException) { + LoggingUtil.getInfoLogger().warn("Could not translate JOIN ON clause to SMT-LIB, skipping: ${onExpression}. Reason: ${e.message}") } } } @@ -525,8 +547,12 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I "BIGINT" to "Int", "BIT" to "Int", "INTEGER" to "Int", + "INT2" to "Int", + "INT4" to "Int", + "INT8" to "Int", "TINYINT" to "Int", "SMALLINT" to "Int", + "NUMERIC" to "Int", "TIMESTAMP" to "Int", "DATE" to "Int", "FLOAT" to "Real", @@ -539,6 +565,10 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I "TEXT" to "String", "CHARACTER LARGE OBJECT" to "String", "BOOLEAN" to "String", + "BOOL" to "String", + "UUID" to "String", + "JSONB" to "String", + "BYTEA" to "String", ) } } diff --git a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt index 3f677ab29d..742d4dd012 100644 --- a/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt +++ b/core/src/test/kotlin/org/evomaster/core/solver/SmtLibGeneratorTest.kt @@ -209,6 +209,27 @@ class SmtLibGeneratorTest { } } + /** + * Test that a <> (not-equals) condition in the WHERE clause is correctly translated + * to a distinct SMT-LIB assertion. + */ + @Test + @Throws(JSQLParserException::class) + fun selectFromUsersWithNotEquals() { + val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM Users WHERE age <> 30;") + + val response: SMTLib = generator.generateSMT(selectStatement) + + val expected = tableConstraints + expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users1)", "30")))) + expected.addNode(AssertSMTNode(DistinctAssertion(listOf("(AGE users2)", "30")))) + expected.addNode(CheckSatSMTNode()) + expected.addNode(GetValueSMTNode("users1")) + expected.addNode(GetValueSMTNode("users2")) + + assertEquals(expected, response) + } + /** * Test the generation of SMT from a simple select statement and a database schema * @throws JSQLParserException if the statement is not valid @@ -383,6 +404,34 @@ class SmtLibGeneratorTest { assertEquals(expected, response) } + /** + * Test that NULL comparisons in the WHERE clause are skipped (not emitted as invalid SMT-LIB), + * and the remaining non-null constraints are still applied. + */ + @Test + @Throws(JSQLParserException::class) + fun selectFromUsersWithNullComparison() { + val selectStatement: Statement = CCJSqlParserUtil.parse("SELECT * FROM Users WHERE name = NULL AND age > 30;") + + val response: SMTLib = generator.generateSMT(selectStatement) + + val expected = tableConstraints + // The NULL comparison is skipped; only the non-null constraint is emitted + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users1)", "30"))) + expected.addNode(AssertSMTNode(GreaterThanAssertion("(AGE users2)", "30"))) + + val satConstraints = arrayOf( + CheckSatSMTNode(), + GetValueSMTNode("users1"), + GetValueSMTNode("users2") + ) + for (constraint in satConstraints) { + expected.addNode(constraint) + } + + assertEquals(expected, response) + } + /** * Test that a BIT column type is translated to Int in the SMT-LIB representation. */