Merge pull request #1434 from WebFuzzing/fix/exec-solver

Fix found errors when debugging Z3 Solver

Author: arcuri82

core/src/main/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolver.kt

@@ -10,6 +10,7 @@ import org.evomaster.client.java.controller.api.dto.database.schema.DatabaseType
 import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto
 import org.evomaster.client.java.controller.api.dto.database.schema.TableDto
 import org.evomaster.core.EMConfig
+import org.evomaster.core.logging.LoggingUtil
 import org.evomaster.core.search.gene.BooleanGene
 import org.evomaster.core.search.gene.Gene
 import org.evomaster.core.search.gene.numeric.DoubleGene
@@ -102,11 +103,21 @@ class SMTLibZ3DbConstraintSolver() : DbConstraintSolver {
     private fun parseStatement(sqlQuery: String): Statement {
         return try {
             CCJSqlParserUtil.parse(sqlQuery)
-        } catch (e: JSQLParserException) {
-            throw RuntimeException(e)
+        } catch (_: JSQLParserException) {
+            val sanitizedQuery = removeNotSupportedKeywords(sqlQuery)
+            return try {
+                CCJSqlParserUtil.parse(sanitizedQuery)
+            } catch (e: JSQLParserException) {
+                LoggingUtil.getInfoLogger().error("Failed to parse SQL query '$sqlQuery' as SQL Statement")
+                throw RuntimeException(e)
+            }
         }
     }
 
+    private fun removeNotSupportedKeywords(sqlQuery: String): String {
+        return sqlQuery.replace("local temporary", "")
+    }
+
     /**
      * Converts Z3's response to a list of SqlActions.
      *

core/src/main/kotlin/org/evomaster/core/solver/SmtLibGenerator.kt

@@ -10,6 +10,7 @@ import org.evomaster.client.java.controller.api.dto.database.schema.DatabaseType
 import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto
 import org.evomaster.client.java.controller.api.dto.database.schema.ForeignKeyDto
 import org.evomaster.client.java.controller.api.dto.database.schema.TableDto
+import org.evomaster.core.logging.LoggingUtil
 import org.evomaster.core.utils.StringUtils
 import org.evomaster.dbconstraint.ConstraintDatabaseType
 import org.evomaster.dbconstraint.ast.SqlCondition
@@ -459,7 +460,17 @@ class SmtLibGenerator(private val schema: DbInfoDto, private val numberOfRows: I
         val tablesFinder = TablesNamesFinder()
 
         // Add tables from the FROM clause
-        for (tableName in tablesFinder.getTables(sqlQuery)){
+        val tables = try {
+            tablesFinder.getTables(sqlQuery)
+        } catch (e: Exception) {
+            // This is because the jsqlParser does not support visit(Execute execute) {
+            //        throw new UnsupportedOperationException(NOT_SUPPORTED_YET); }
+            // https://github.com/JSQLParser/JSqlParser/blob/484eaa1c0f623cc67f8bf324e4367f8474eb77f1/src/main/java/net/sf/jsqlparser/util/TablesNamesFinder.java#L1180
+            LoggingUtil.getInfoLogger().error("Failed to find tables: ${e.message}")
+            emptySet<String>()
+        }
+
+        for (tableName in tables){
             tablesMentioned.add(tableName.lowercase())
         }
 

core/src/test/kotlin/org/evomaster/core/solver/SMTLibZ3DbConstraintSolverTest.kt

@@ -1,14 +1,12 @@
 package org.evomaster.core.solver
 
-import net.sf.jsqlparser.JSQLParserException
 import org.evomaster.client.java.controller.api.dto.database.schema.DbInfoDto
 import org.evomaster.client.java.sql.DbInfoExtractor
 import org.evomaster.client.java.sql.SqlScriptRunner
 import org.evomaster.core.search.gene.Gene
 import org.evomaster.core.search.gene.numeric.IntegerGene
 import org.evomaster.core.search.gene.sql.SqlPrimaryKeyGene
 import org.evomaster.core.search.gene.string.StringGene
-import org.evomaster.solver.smtlib.*
 import org.junit.jupiter.api.AfterAll
 import org.junit.jupiter.api.Assertions.*
 import org.junit.jupiter.api.BeforeAll
@@ -48,17 +46,15 @@ class SMTLibZ3DbConstraintSolverTest {
 
     /**
      * Test the generation of SMT from a simple select statement and a database schema
-     * @throws JSQLParserException if the statement is not valid
      */
     @Test
-    @Throws(JSQLParserException::class)
     fun selectFromUsers() {
 
         val newActions = solver.solve(schemaDto, "SELECT * FROM Users;", 2)
 
         assertEquals(2, newActions.size)
 
-        val genesInsert1: List<Gene> = newActions.get(0).seeTopGenes()
+        val genesInsert1: List<Gene> = newActions[0].seeTopGenes()
 
         assertEquals(4, genesInsert1.size)
 
@@ -87,7 +83,7 @@ class SMTLibZ3DbConstraintSolverTest {
             }
         }
 
-        val genesInsert2: List<Gene> = newActions.get(1).seeTopGenes()
+        val genesInsert2: List<Gene> = newActions[1].seeTopGenes()
 
         assertEquals(4, genesInsert2.size)
 
@@ -116,4 +112,16 @@ class SMTLibZ3DbConstraintSolverTest {
             }
         }
     }
+
+    /**
+     * Test the generation of SMT from a complicated cache local temporary table does not throw exception
+     */
+    @Test
+    fun selectLocal() {
+
+        val newActions = solver.solve(schemaDto, "create cached local temporary table if not exists HT_feature_constraint (id bigint not null) on commit drop transactional", 2)
+
+        // This will be empty as the query does not correspond to the created database, just checking that it doesn't throw an exception
+        assertEquals(0, newActions.size)
+    }
 }