All Projects → SpoonLabs → Nopol

SpoonLabs / Nopol

Licence: gpl-2.0
Automatic program repair and patch generation system for Java based on dynamic analysis and code synthesis with SMT, developed at University of Lille and Inria, France.

Programming Languages

java
68154 projects - #9 most used programming language

Labels

Projects that are alternatives of or similar to Nopol

TargomanSMT
Targoman SMT framework source code
Stars: ✭ 29 (-60.27%)
Mutual labels:  smt
archsat
A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
Stars: ✭ 20 (-72.6%)
Mutual labels:  smt
Pysmt
pySMT: A library for SMT formulae manipulation and solving
Stars: ✭ 352 (+382.19%)
Mutual labels:  smt
py2many
Transpiler of Python to many other languages
Stars: ✭ 420 (+475.34%)
Mutual labels:  smt
vim-smt2
A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)
Stars: ✭ 35 (-52.05%)
Mutual labels:  smt
smt
A Go library that implements a Sparse Merkle tree for a key-value map.
Stars: ✭ 83 (+13.7%)
Mutual labels:  smt
stevia
A simple (unfinished) SMT solver for QF_ABV.
Stars: ✭ 30 (-58.9%)
Mutual labels:  smt
Liquidhaskell
Liquid Types For Haskell
Stars: ✭ 863 (+1082.19%)
Mutual labels:  smt
z3 tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
Stars: ✭ 117 (+60.27%)
Mutual labels:  smt
Stp
Simple Theorem Prover, an efficient SMT solver for bitvectors
Stars: ✭ 341 (+367.12%)
Mutual labels:  smt
clpsmt-miniKanren
CLP(SMT) on top of miniKanren
Stars: ✭ 31 (-57.53%)
Mutual labels:  smt
suslik
Synthesis of Heap-Manipulating Programs from Separation Logic
Stars: ✭ 107 (+46.58%)
Mutual labels:  smt
Smack
SMACK Software Verifier and Verification Toolchain
Stars: ✭ 305 (+317.81%)
Mutual labels:  smt
mailer-plugin
This plugin allows you to configure email notifications for build results
Stars: ✭ 35 (-52.05%)
Mutual labels:  smt
Adafruit cad parts
CAD files for various boards, components and parts
Stars: ✭ 386 (+428.77%)
Mutual labels:  smt
the-thoralf-plugin
This a type-checker plugin to rule all type checker plugins involving type-equality reasoning using smt solvers.
Stars: ✭ 22 (-69.86%)
Mutual labels:  smt
kafka-connect-transform-kryptonite
Kryptonite for Kafka is a client-side 🔒 field level 🔓 crypto library for Apache Kafka® currently focused on Kafka Connect scenarios. It's an ! UNOFFICIAL ! community project
Stars: ✭ 30 (-58.9%)
Mutual labels:  smt
Dreal4
SMT Solver for Nonlinear Theories of Reals
Stars: ✭ 72 (-1.37%)
Mutual labels:  smt
Cvc4
CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
Stars: ✭ 476 (+552.05%)
Mutual labels:  smt
Sat smt by example
"SAT/SMT by example" free ebook
Stars: ✭ 339 (+364.38%)
Mutual labels:  smt

Nopol Build Status Coverage Status

Nopol is an automatic software repair tool for Java. This code is research code, released under the GPL licence.

If you use this code for academic research, please cite: Nopol: Automatic Repair of Conditional Statement Bugs in Java Programs (Jifeng Xuan, Matias Martinez, Favio Demarco, Maxime Clément, Sebastian Lamelas, Thomas Durieux, Daniel Le Berre, Daniel Le Berre, Martin Monperrus). IEEE Transactions on Software Engineering, 2016.

@article{xuan:hal-01285008,
 title = {Nopol: Automatic Repair of Conditional Statement Bugs in Java Programs},
 author = {Xuan, Jifeng and Martinez, Matias and Demarco, Favio and Clément, Maxime and Lamelas, Sebastian and Durieux, Thomas and Le Berre, Daniel and Monperrus, Martin},
 journal = {IEEE Transactions on Software Engineering},
 doi = {10.1109/TSE.2016.2560811},
 year = {2016},
}

Others papers about Nopol:

Getting started

Nopol requires Java and an SMT solver installed on the machine (e.g. Z3)

  1. Compile NoPol:
git clone https://github.com/SpoonLabs/nopol.git
cd nopol/nopol
export JAVA_HOME=/usr/lib/jvm/java-8-openjdk-amd64

# -DskipTests is required, to run the tests one needs to compile ../test-projects/ (see below)
mvn package -DskipTests
  1. Locate the Nopol jar file produced at step 1)
$ ls target/*jar
target/nopol-0.2-SNAPSHOT.jar
target/nopol-0.2-SNAPSHOT-jar-with-dependencies.jar # we use this one

In the following, nopol.jar refers to the jar file with dependencies (target/nopol-<VERSION>-SNAPSHOT-jar-with-dependencies.jar)

  1. Compile the test-projects
$ cd ../test-projects/
# compiling app (in target/classes) and tests (in target/test-classes), but don't run the tests (they obviously fail, because the goal is to repair them)
$ mvn test -DskipTests 

3b) Optional: run the tests of Nopol to check your installation

$ cd ../nopol/
$ mvn test
  1. Execute Nopol (parameters explained below)

(Long commands are broken in several lines, separated by a backslash, which means an escaped linebreak in Unix shells.)

cd ../test-projects/
java -jar nopol.jar \
-s src/main/java/ \
-c target/classes:target/test-classes:/home/<user>/.m2/repository/junit/junit/4.11/junit-4.11.jar:/home/<user>/.m2/repository/org/hamcrest/hamcrest-core/1.3/hamcrest-core-1.3.jar \
-t symbolic_examples.symbolic_example_1.NopolExampleTest \
-p ../nopol/lib/z3/z3_for_linux

If you keep nopol.jar instead of the actual jar located at the previous step, you'll get Error: unable to access jarfile nopol.jar (see above). You should replace also <user> by your own username.

It should output something like:

----INFORMATION----
Nb classes : 34
Nb methods : 53
Nb statements: 5
Nb statement executed by the passing tests of the patched line: 0
Nb statement executed by the failing tests of the patched line: 0
Nb unit tests : 9
Nb Statements Analyzed : 3
Nb Statements with Angelic Value Found : 1
Nb inputs in SMT : 8
Nb SMT level: 2
Nb SMT components: [4] [== of arity: 2, != of arity: 2, < of arity: 2, <= of arity: 2]
                  class java.lang.Boolean: 4
Nb variables in SMT : 13
Nb run failing test  : [2, 1]
Nb run passing test : [4, 18]
NoPol Execution time : 3262ms
----PATCH FOUND----
symbolic_examples.symbolic_example_1.NopolExample:12: CONDITIONAL index < 1

NoPol (SMT and Dynamoth) returns also a unix code (integer):

  • 0 if a patch has been found
  • -1 otherwise

Parameter -c can be found with mvn dependency:build-classpath.

Minimal Usage

4 parameters are required

Usage: java -jar nopol.jar

  (-s|--source) source1:source2:...:sourceN 
        Define the path to the source code of the project. For instance `src/main/java`

  (-c|--classpath) <classpath>
        Define the classpath of the project separated by a path separator (`:` on Linux). 
        Must contain the application binary classes (`target/classes`)
        Must contain the application test classes (`target/test-classes`)
        Must contain the library classes (`lib/junit.jar` for instance)
        
  [(-t|--test) test1:test2:...:testN ]
        Define the tests of the project. For instance `symbolic_examples.symbolic_example_1.NopolExampleTest`

  [(-p|--solver-path) <solverPath>]
        Define the solver binary path (only used with smt synthesis). For instance `../nopol/lib/z3/z3_for_linux`

Advanced Usage

See also notes below.

Usage: java -jar nopol.jar

  [(-m|--mode) <repair|ranking>]
        Define the mode of execution. (default: repair)

  [(-e|--type) <pre_then_cond|condition|precondition>]
        The type of statement to analyze (only used with repair mode). (default: pre_then_cond)

  [(-o|--oracle) <angelic|symbolic>]
        Define the oracle (only used with repair mode). (default: angelic)

  [(-y|--synthesis) <smt|dynamoth>]
        Define the patch synthesis. (default: smt)

  [(-l|--solver) <z3|cvc4>]
        Define the solver (only used with smt synthesis). (default: z3)

  [--complianceLevel <complianceLevel>]
        The Java version of the project. (default: 7)

  [--maxTime <maxTime>]
        The maximum time execution in minute for the whole execution of Nopol.(default: 10)

  [--maxTimeType <maxTimeType>]
        The maximum time execution in minute for one type of patch per per suspicious statement (eg. 5 minutes max to find a precondition at line x). (default: 5)

  [(-z|--flocal) < cocospoon|dumb|gzoltar>]
        Define the fault localizer to be used. (default: cocospoon). 
          "cocospoon" means source code instrumentation plus ochiai metric.
          "dumb" means random fault localization. 
          "gzoltar" means binary code instrumentation with external library plus ochiai metric.

Notes: For using Dynamoth (-y dynamoth), you must add tools.jar in the classpath of Nopol, and use java with -cp (and not -jar):

java -cp $JAVA_HOME/lib/tools.jar:../nopol/target/nopol-SNAPSHOT-jar-with-dependencies.jar fr.inria.lille.repair.Main <nopol arguments>

Examples of Real Bugs Targeted by Nopol:

Apache Commons Math:

Apache Commons Lang:

Google GSON:

Contact

For questions and feedback , please contact @monperrus

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].