SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
130 stars 91 forks source link

Adding Gradle Support for SPF #70

Closed gaurangkudale closed 2 years ago

gaurangkudale commented 2 years ago

Hi there Can someone please review this pull request?

gaurangkudale commented 2 years ago

` BUILD SUCCESSFUL in 1s 1 actionable task: 1 executed PS C:\Users\gaura\jpf\jpf-symbc> gradle compileAnnotationsJava

Deprecated Gradle features were used in this build, making it incompatible with Gradle 8.0.

You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins.`

Here I'm able to execute the gradle compileAnnotationsJava but that's not the same case for other tasks

Here I've attached the logs file where I executed gradlew compileClassesJava Logs.txt

gaurangkudale commented 2 years ago

Here basically the task compileJava is failing because of errors in jpf-symbc\src\classes Can anyone please price the detailed review for this PR ASAP?

gaurangkudale commented 2 years ago

Is anyone interested in reviewing the changes?

yannicnoller commented 2 years ago

@gaurangkudale I will have a look by the end of this week

gaurangkudale commented 2 years ago

@gaurangkudale I will have a look by the end of this week

Sure but do you have any idea why I'm getting the above error because I'm did every possible thing to solve that error If you help me to solve this problem so that I can continue contacting

gaurangkudale commented 2 years ago

@yannicnoller Any Updates?

glockyco commented 2 years ago

Hi @gaurangkudale,

the errors that you're currently seeing (short snippet shown below) occur because the JPF JARs are missing from the classpath. Beyond the JPF JARs, the JARs in the lib/ directory also have to be added to the classpath.

Task :compileJava C:\Users\gaura\jpf\jpf-symbc\src\main\gov\nasa\jpf\symbc\concolic\FunctionExpression.java:46: error: package gov.nasa.jpf.util does not exist import gov.nasa.jpf.util.FileUtils; ^ C:\Users\gaura\jpf\jpf-symbc\src\main\gov\nasa\jpf\symbc\concolic\FunctionExpression.java:47: error: package gov.nasa.jpf.vm does not exist import gov.nasa.jpf.vm.ClassLoaderInfo; ^ [...]

In the build.xml file used by Ant, the corresponding parts of the file are the following:

[...]

<!-- generic classpath settings -->
<path id="lib.path">
    <!-- our own classes and libs come first -->
    <pathelement location="build/main"/>
     <!-- we don't have these
    <pathelement location="build/peers"/>
    -->
    <fileset dir=".">
        <include name="lib/*.jar"/>
    </fileset>
    <!-- add in what we need from the core -->
    <pathelement path="${jpf-core.native_classpath}"/>
</path>

[...]

<target name="-compile-main" if="have_main">
    <mkdir dir="build/main"/>
    <javac srcdir="src/main" destdir="build/main"
        debug="${debug}" source="${src_level}" deprecation="${deprecation}"
        classpathref="lib.path"
        includeantruntime="false"/>
</target>

[...]

Note how lib.path defines the locations of the dependencies, which are then added to the classpath via classpathref="lib.path". Similar target definitions also exist for -compile-peers, -compile-classes, etc.

The tricky bit here is that ${jpf-core.native_classpath} is defined in the jpf.properties file of jpf-core, and the location of jpf-core is defined in the site.properties file, which is usually located at ~/.jpf/site.properties. Furthermore, the jpf-core path commonly contains ${user.home} or similar variables, which also have to be resolved correctly.

To see how jpf-nhandler handles this, you can look at their build.xml file and the corresponding code in the buildSrc directory of the project. Further information about Gradle build sources can be found in the Gradle documentation.


In my own jpf-symbc fork (see: glockyco/jpf-symbc/java-8-gradle), I've taken a different approach: I've kept the needed Ant property definitions in a build-properties.xml file and am reading them with ant.importBuild in the build.gradle file. That way, all the resolving of ${...} is still done automatically for us. Probably not an idiomatic way to do things, but much easier to implement than the jpf-nhandler solution, in case you need something to use as a starting point.

yannicnoller commented 2 years ago

Thanks, @glockyco, for your suggestion! @gaurangkudale, please have a look when you find the time. Thanks!

gaurangkudale commented 2 years ago

@glockyco Thank you for your suggestion I will look into your personal reposetory and work on this PR

gaurangkudale commented 2 years ago

Hi @gaurangkudale,

the errors that you're currently seeing (short snippet shown below) occur because the JPF JARs are missing from the classpath. Beyond the JPF JARs, the JARs in the lib/ directory also have to be added to the classpath.

Task :compileJava C:\Users\gaura\jpf\jpf-symbc\src\main\gov\nasa\jpf\symbc\concolic\FunctionExpression.java:46: error: package gov.nasa.jpf.util does not exist import gov.nasa.jpf.util.FileUtils; ^ C:\Users\gaura\jpf\jpf-symbc\src\main\gov\nasa\jpf\symbc\concolic\FunctionExpression.java:47: error: package gov.nasa.jpf.vm does not exist import gov.nasa.jpf.vm.ClassLoaderInfo; ^ [...]

In the build.xml file used by Ant, the corresponding parts of the file are the following:

[...]

<!-- generic classpath settings -->
<path id="lib.path">
    <!-- our own classes and libs come first -->
    <pathelement location="build/main"/>
     <!-- we don't have these
    <pathelement location="build/peers"/>
    -->
    <fileset dir=".">
        <include name="lib/*.jar"/>
    </fileset>
    <!-- add in what we need from the core -->
    <pathelement path="${jpf-core.native_classpath}"/>
</path>

[...]

<target name="-compile-main" if="have_main">
    <mkdir dir="build/main"/>
    <javac srcdir="src/main" destdir="build/main"
        debug="${debug}" source="${src_level}" deprecation="${deprecation}"
        classpathref="lib.path"
        includeantruntime="false"/>
</target>

[...]

Note how lib.path defines the locations of the dependencies, which are then added to the classpath via classpathref="lib.path". Similar target definitions also exist for -compile-peers, -compile-classes, etc.

The tricky bit here is that ${jpf-core.native_classpath} is defined in the jpf.properties file of jpf-core, and the location of jpf-core is defined in the site.properties file, which is usually located at ~/.jpf/site.properties. Furthermore, the jpf-core path commonly contains ${user.home} or similar variables, which also have to be resolved correctly.

To see how jpf-nhandler handles this, you can look at their build.xml file and the corresponding code in the buildSrc directory of the project. Further information about Gradle build sources can be found in the Gradle documentation.

In my own jpf-symbc fork (see: glockyco/jpf-symbc/java-8-gradle), I've taken a different approach: I've kept the needed Ant property definitions in a build-properties.xml file and am reading them with ant.importBuild in the build.gradle file. That way, all the resolving of ${...} is still done automatically for us. Probably not an idiomatic way to do things, but much easier to implement than the jpf-nhandler solution, in case you need something to use as a starting point.

Hi @glockyco I was going through your personal fork [glockyco/jpf-symbc/java-8-gradle](https://github.com/glockyco/jpf-symbc/tree/java-8-gradle) but I am getting this following error while trying to build the project do you have any thoughts on this?

`C:\Users\gaura\spf-gradle\jpf-symbc-java-8-gradle>gradlew

FAILURE: Build failed with an exception.

BUILD FAILED in 2s`

glockyco commented 2 years ago

Build file 'C:\Users\gaura\spf-gradle\jpf-symbc-java-8-gradle\build.gradle' line: 40

A problem occurred evaluating root project 'jpf-symbc'. Cannot invoke method split() on null object

This would happen if the jpf.properties file of jpf-core cannot be found. By default, we're looking for this file in the jpf-core directory configured in ${user.home}/.jpf/site.properties (see: "Creating a site properties file" in the JPF wiki).

If things still don't work for you after you've created a valid site.properties file, you might want to try changing the fallback location of jpf-core (<property name="jpf-core" value = "../jpf-core"/>) configured in the build-properties.xml file of the jpf-symbc root directory.

gaurangkudale commented 2 years ago

Build file 'C:\Users\gaura\spf-gradle\jpf-symbc-java-8-gradle\build.gradle' line: 40 A problem occurred evaluating root project 'jpf-symbc'. Cannot invoke method split() on null object

This would happen if the jpf.properties file of jpf-core cannot be found. By default, we're looking for this file in the jpf-core directory configured in ${user.home}/.jpf/site.properties (see: "Creating a site properties file" in the JPF wiki).

If things still don't work for you after you've created a valid site.properties file, you might want to try changing the fallback location of jpf-core (<property name="jpf-core" value = "../jpf-core"/>) configured in the build-properties.xml file of the jpf-symbc root directory.

Thanks I'll try this!

gaurangkudale commented 2 years ago

Build file 'C:\Users\gaura\spf-gradle\jpf-symbc-java-8-gradle\build.gradle' line: 40 A problem occurred evaluating root project 'jpf-symbc'. Cannot invoke method split() on null object

This would happen if the jpf.properties file of jpf-core cannot be found. By default, we're looking for this file in the jpf-core directory configured in ${user.home}/.jpf/site.properties (see: "Creating a site properties file" in the JPF wiki).

If things still don't work for you after you've created a valid site.properties file, you might want to try changing the fallback location of jpf-core (<property name="jpf-core" value = "../jpf-core"/>) configured in the build-properties.xml file of the jpf-symbc root directory.

Hey @glockyco Can you please tell me which jpf-core version have you used? or can you link that here

glockyco commented 2 years ago

Can you please tell me which jpf-core version have you used?

I'm currently using the master branch of jpf-core (commit 2f8f3c4 as of right now) but any jpf-core version that supports Java 8 should be fine.