Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Updated the readme to be more friendly towards new devs and Windows users. #71

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

Updated the readme to be more friendly towards new devs and Windows users. #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
53be5a1
Updated readme to be more friendly to new devs and Windows users.
phunky-tech Jun 22, 2022
a69355c
Merge pull request #2 from phillipbruce1/readme-update
phunky-tech Jun 22, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 40 additions & 18 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@ Symbolic (Java) PathFinder:
This JPF extension provides symbolic execution for Java bytecode.
It performs a non-standard interpretation of byte-codes.
It allows symbolic execution on methods with arguments of basic types
(int, long, double, boolean, etc.). It also supports symbolic strings, arrays,
(int, long, double, boolean, etc.). It also supports symbolic strings, arrays,
and user-defined data structures.

SPF now has a "symcrete" mode that executes paths
SPF now has a "symcrete" mode that executes paths
triggered by concrete inputs and collects constraints along the paths

A paper describing Symbolic PathFinder appeared at ISSTA'08:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we change the format of this reference?

Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software
Corina S. Pǎsǎreanu, Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person, and Mark Pape. In Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA '08). https://doi.org/10.1145/1390630.1390635

@inproceedings{spf,
   author = {P{\u{a}}s{\u{a}}reanu, Corina S. and Mehlitz, Peter C. and Bushnell, David H. and Gundy-Burlet, Karen and Lowry, Michael and Person, Suzette and Pape, Mark},
   title = {Combining Unit-Level Symbolic Execution and System-Level Concrete Execution for Testing Nasa Software},
   year = {2008},
   isbn = {9781605580500},
   publisher = {Association for Computing Machinery},
   address = {New York, NY, USA},
   url = {https://doi.org/10.1145/1390630.1390635},
   doi = {10.1145/1390630.1390635},
   booktitle = {Proceedings of the 2008 International Symposium on Software Testing and Analysis},
   pages = {15–26},
   numpages = {12},
   keywords = {software model checking, symbolic execution, unit testing, system testing},
   location = {Seattle, WA, USA},
   series = {ISSTA '08}
}

Expand All @@ -22,28 +22,50 @@ M. Lowry, S. Person, M. Pape.
Getting Started
----------------

First of all please use Java 8 (I am afraid our tools do not work with newer versions of Java).
Also please use eclipse (highly recommended).
> NOTE: It is strongly recommended to use Eclipse.

Then please download jpf-core from here:
https://github.com/yannicnoller/jpf-core/tree/0f2f2901cd0ae9833145c38fee57be03da90a64f
or here
https://github.com/corinus/jpf-core
### Configuring Files

And jpf-symbc from here:
https://github.com/SymbolicPathFinder/jpf-symbc
You can download jpf-core from one of the links below:
- https://github.com/corinus/jpf-core
- https://github.com/yannicnoller/jpf-core/tree/0f2f2901cd0ae9833145c38fee57be03da90a64f

Import them in Eclipse as 2 Java projects.
Also create a .jpf dir in your home directory and create in it a file called "site.properties" with the following content:
And download jpf-symbc from here:
- https://github.com/SymbolicPathFinder/jpf-symbc

jpf-core = ${user.home}/.../path-to-jpf-core-folder/jpf-core
> Note: You can use `git clone <url>` to download the projects as git repositories

jpf-symbc = ${user.home}/.../path-to-jpf-core-folder/jpf-symbc
Put them in the same directory. In this example, we'll call the parent directory `spf-files`. It should look like this:

extensions=${jpf-core},${jpf-symbc}
```
spf-files/
| jpf-core/
| jpf-symbc/
```

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it would be worthwhile to mention that the user should first attempt to build the jpf-core and jpf-symbc locally before moving on to Eclipse. This way they can already detect errors that are not due to any Eclipse configuration, e.g., the java8 setup etc. In general, it would also be good to add the expected output so that users can check and see which warnings might be expected.

Create a new Eclipse workspace in the `spf-files` directory, then import `jpf-core` and `jpf-symbc` into the workspace as Java projects. To do this in Eclipse, go to `File > Import > General > Existing Projects into Workspace` and hit next. Select `spf-files` as the root directory, then select both projects to import and hit finish.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is not necessary. One also can use an existing workspace afak, so maybe we can just remove that part of the sentence? Or say create new one or use an existing one...

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this comment is meant to address the first part of the line

Create a new Eclipse workspace ...


You can then try to run some examples by selecting a .jpf file from the "examples" directory and then selecting a run configuration from the "Run" menu in Eclipse.
In particular you should select: "run-JPF-symbc" to run Symbolic PathFinder on your example; configuration "run-JPF-symbc-mac" is tailored for Mac; for Windows please change the environment variable in the run configuration to PATH; it should point to the lib directory in your jpf-symbc project.
On Mac or Linux, create a `.jpf` directory in your home directory. On Windows, create it in your User folder (i.e. `C:\Users\<your username>\.jpf`). In `.jpf`, create a file called `site.properties` and add the following:

Good luck!
```
jpf-core = /path/to/.../jpf-core/
jpf-symbc = /path/to/.../jpf-symbc/

extensions = ${jpf-core}, ${jpf-symbc}
```

> **NOTE FOR WINDOWS USERS:** Instead of using `/` for the file path like above, or `\` like in Windows Explorer, you need to use `\\` (i.e. `C:\\Users\\<username>\\spf-files\\jpf-symbc`)

### Configuring Eclipse

We need to force Eclipse to use Java 8, as newer versions of Java are not yet supported. In Elcipse, go to `Window > Preferences > Java > Compiler` and set the "Compiler compliance level" to 1.8.

Next we need to tell Eclipse where to find the Java 8 JDK. Go to `Window > Preferences > Java > Installed JREs`. If you do not already have a Java 8 compliant JDK, then you will need to download one. Once you do, go to "Add...", select "Standard VM", then select "Directory..." next to "JRE home" and browse to find the `jre` directory for the desired JDK (i.e. `/path/to/jdk/.../jre`). Once selected, hit "Finish" and "Apply and Close".

Lastly, we need to point Eclipse to the necessary dependencies. Go to `Run > Run Configurations...`. Under the "Java Application" dropdown, there should be several run configurations. Select `run-JPF-symbc` and go to the Environment tab along the top. There should be two variables: `LD_LIBRARY_PATH` for Mac and Linux, and `PATH` for Windows. Change each to point to `jpf-symbc/lib` (i.e. `/path/to/.../jpf-symbc/lib`). Windows users should use `\\` as described above.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for macOS it is "DYLD_LIBRARY_PATH"


### Building and Running

Now you should be able to build the project successfully. In `Project > Clean`, check "Clean all projects" and hit "Clean". If that works, find an example `.jpf` file in `jpf-symbc/src/examples`. Right click on it and go to `Run As > Run Configurations...` in the popup menu, or click the file and go to `Run > Run Configurations...` in the Eclipse toolbar. Click `run-JPF-symbc`, hit "Run" in the bottom right, and you should see the example run without errors!

Have fun!
68 changes: 47 additions & 21 deletions Readme
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,17 +1,16 @@
Symbolic (Java) PathFinder:
---------------------------

Created new branch that contains many updates to SPF;
in particular, interfacing with Z3 is robust;
also SPF now has a "symcrete" mode that executes paths
triggered by concrete inputs and collects constraints along the paths


This JPF extension provides symbolic execution for Java bytecode.
It performs a non-standard interpretation of byte-codes.
Currently, it allows symbolic execution on methods with arguments of basic types
(int, long, double, boolean, etc.). Symbolic input globals and method
pre-conditions are specified via user annotations (see symbc/examples and
symbc/test).
It allows symbolic execution on methods with arguments of basic types
(int, long, double, boolean, etc.). It also supports symbolic strings, arrays,
and user-defined data structures.

SPF now has a "symcrete" mode that executes paths
triggered by concrete inputs and collects constraints along the paths

A paper describing Symbolic PathFinder appeared at ISSTA'08:

Expand All @@ -23,23 +22,50 @@ M. Lowry, S. Person, M. Pape.
Getting Started
----------------

First of all please use Java 8 (I am afraid our tools do not work with newer versions of Java).
> NOTE: It is strongly recommended to use Eclipse.

### Configuring Files

You can download jpf-core from one of the links below:
- https://github.com/corinus/jpf-core
- https://github.com/yannicnoller/jpf-core/tree/0f2f2901cd0ae9833145c38fee57be03da90a64f

And download jpf-symbc from here:
- https://github.com/SymbolicPathFinder/jpf-symbc

> Note: You can use `git clone <url>` to download the projects as git repositories

Put them in the same directory. In this example, we'll call the parent directory `spf-files`. It should look like this:

```
spf-files/
| jpf-core/
| jpf-symbc/
```

Create a new Eclipse workspace in the `spf-files` directory, then import `jpf-core` and `jpf-symbc` into the workspace as Java projects. To do this in Eclipse, go to `File > Import > General > Existing Projects into Workspace` and hit next. Select `spf-files` as the root directory, then select both projects to import and hit finish.

On Mac or Linux, create a `.jpf` directory in your home directory. On Windows, create it in your User folder (i.e. `C:\Users\<your username>\.jpf`). In `.jpf`, create a file called `site.properties` and add the following:

```
jpf-core = /path/to/.../jpf-core/
jpf-symbc = /path/to/.../jpf-symbc/

extensions = ${jpf-core}, ${jpf-symbc}
```

> **NOTE FOR WINDOWS USERS:** Instead of using `/` for the file path like above, or `\` like in Windows Explorer, you need to use `\\` (i.e. `C:\\Users\\<username>\\spf-files\\jpf-symbc`)

Then please download jpf-core from here:
https://github.com/yannicnoller/jpf-core/tree/0f2f2901cd0ae9833145c38fee57be03da90a64f
### Configuring Eclipse
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be helpful to also have some screenshots.


And jpf-symbc from here:
https://github.com/SymbolicPathFinder/jpf-symbc/tree/b64ab6a0c8dde218b34969b46ee526ece7ddee44
We need to force Eclipse to use Java 8, as newer versions of Java are not yet supported. In Elcipse, go to `Window > Preferences > Java > Compiler` and set the "Compiler compliance level" to 1.8.

Import them in Eclipse as 2 Java projects.
Also create a .jpf dir in your home directory and create in it a file called "site.properties" with the following content:
Next we need to tell Eclipse where to find the Java 8 JDK. Go to `Window > Preferences > Java > Installed JREs`. If you do not already have a Java 8 compliant JDK, then you will need to download one. Once you do, go to "Add...", select "Standard VM", then select "Directory..." next to "JRE home" and browse to find the `jre` directory for the desired JDK (i.e. `/path/to/jdk/.../jre`). Once selected, hit "Finish" and "Apply and Close".

jpf-core = ${user.home}/.../path-to-jpf-core-folder/jpf-core
jpf-symbc = ${user.home}/.../path-to-jpf-core-folder/pf-symbc
extensions=${jpf-core},${jpf-symbc}
Lastly, we need to point Eclipse to the necessary dependencies. Go to `Run > Run Configurations...`. Under the "Java Application" dropdown, there should be several run configurations. Select `run-JPF-symbc` and go to the Environment tab along the top. There should be two variables: `LD_LIBRARY_PATH` for Mac and Linux, and `PATH` for Windows. Change each to point to `jpf-symbc/lib` (i.e. `/path/to/.../jpf-symbc/lib`). Windows users should use `\\` as described above.

### Building and Running
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be helpful to also show an example, and the expected output.


You can then try to run some examples by selecting a .jpf file from the "examples" directory and then selecting a run configuration from the "Run" menu in Eclipse.
In particular you should select: "run-JPF-symbc" to run Symbolic PathFinder on your example (configuration "run-JPF-symbc-mac" is tailored for Mac).
Now you should be able to build the project successfully. In `Project > Clean`, check "Clean all projects" and hit "Clean". If that works, find an example `.jpf` file in `jpf-symbc/src/examples`. Right click on it and go to `Run As > Run Configurations...` in the popup menu, or click the file and go to `Run > Run Configurations...` in the Eclipse toolbar. Click `run-JPF-symbc`, hit "Run" in the bottom right, and you should see the example run without errors!

Good luck!
Have fun!