pietrobraione / jbse

A symbolic Java virtual machine for program analysis, verification and test generation
http://pietrobraione.github.io/jbse/
GNU General Public License v3.0
103 stars 29 forks source link

JBSE issue with JDBC #63

Closed cniddodi closed 2 years ago

cniddodi commented 2 years ago

JBSE throws the following error while running code using java.sql.DriverManager despite providing the required jar files:

[java/sql/DriverManager].java/sql/DriverManager:logWriter.java/io/PrintWriter:out not expanded, because no concrete, compatible, pre-initialized class was found.

Here is the code:

public void findUser(String login) {

        String url = "jdbc:mysql://localhost:3306/dvja?useSSL=false";
        String username = "java";
        String password = "password";

        try (Connection conn = DriverManager.getConnection(url, username, password)) {

            String query = "SELECT * FROM users WHERE login = '" + login + "'";
            Statement st = conn.createStatement();

            ResultSet rs = st.executeQuery(query);

            st.close();
            conn.close();

        } catch (Exception e) {
             ;
        }
    }
pietrobraione commented 2 years ago

This issue happens whenever there is a field in an object (in this case, the static field DriverManager.logWriter.out) that is declared with an abstract type (in this case, java.io.PrintWriter) and that the Java code execution does not initialize, so JBSE fills it with a symbolic (unknown) reference. JBSE cannot make hypotheses on the class of the concrete object the reference points to: The possible subclasses of java.io.PrintWriter are too many, and JBSE cannot say which is the right one, nor it can try each of them. You have two alternatives: Either you can configure JBSE by specifying a class substitution rule of the kind "whenever you meet a symbolic reference with class java.io.PrintWriter, assume that it points to an object with class ...", or you can ask JBSE to run the static initializer of DriverManager class, so its static fields are initialized with the right objects. I usually prefer the second alternative, that is ok inasmuch the static fields of the class are final and point to immutable objects, or to object whose state is not really relevant.