-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
bde4891
commit f2abf97
Showing
13 changed files
with
378 additions
and
59 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
|
||
To run HIPPODROME on each benchmark individually: | ||
1. cd examples/<name-of-project> | ||
2. hippodrome --config_file="CONFIG.json" | ||
|
||
Notes. | ||
a. HIPPODROME makes a copy of the original (unfixed) file. To revert a fixed file to its original state simply run | ||
"mv <filename>.orig <filename>" | ||
b. The config file is already set for you. You can change it knowing that if follows this format: | ||
|
||
```json | ||
{"infer":"<path-to-infer>", | ||
"options":["--racerdfix-only", "--starvation", <list-of-strings-representing-additional-infer-options>], | ||
"json_path": "./infer-out/", | ||
"target_options": ["--", "javac", "<java-files-to-be-analysed>"], | ||
"prio_file": [], | ||
"iterations": 10 | ||
} | ||
``` | ||
where | ||
* ``infer`` sets the path to the running infer | ||
* ``options`` are the options passed to the infer process | ||
* ``json_path`` is the path to the directory where infer writes its reports | ||
* ``targer_options`` tells how to compile the target files and which files to compile | ||
* ``prio_files`` selects only these files to be fixed. If left empty, RacerDFix will attempt to fix all the files | ||
* ``iterations`` the number of iterations allowed to re-analyse and re-patch the target files before stopping the patching process. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
package account; | ||
|
||
//import java.lang.*; | ||
|
||
import com.facebook.infer.annotation.*; | ||
|
||
@ThreadSafe | ||
public class Account { | ||
double amount; | ||
String name; | ||
|
||
//constructor | ||
public Account(String nm,double amnt ) { | ||
amount=amnt; | ||
name=nm; | ||
} | ||
//functions | ||
synchronized void depsite(double money){ | ||
amount+=money; | ||
} | ||
|
||
synchronized void withdraw(double money){ | ||
amount-=money; | ||
} | ||
|
||
synchronized void transfer(Account ac,double mn){ | ||
amount-=mn; | ||
//System.out.println("ac.amount is $"+ac.amount); | ||
if (name.equals("D")) { | ||
System.out.println("unprotected"); | ||
ac.amount += mn;//no aquire for the other lock!! | ||
//+= might cause problem --it is not atomic. | ||
} else { | ||
//System.out.println("protected"); | ||
synchronized (ac) { ac.amount+=mn; } | ||
} | ||
} | ||
|
||
synchronized void print(){ | ||
} | ||
|
||
}//end of class Acount |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,62 @@ | ||
package account; | ||
|
||
import java.io.*; | ||
|
||
/** | ||
* Title: Software Testing course | ||
* Description: The goal of the exercise is implementing a program which demonstrate a parallel bug. | ||
* In the exercise we have two accounts.The program enable tranfering money from one account to the other.Although the functions were defended by locks (synchronize) there exists an interleaving which we'll experience a bug. | ||
* Copyright: Copyright (c) 2003 | ||
* Company: Haifa U. | ||
* @author Zoya Shaham and Maya Maimon | ||
* @version 1.0 | ||
*/ | ||
|
||
public class Main { | ||
|
||
|
||
public static void main(String[] args) { | ||
|
||
try{ | ||
ManageAccount.num = 10; | ||
ManageAccount[] bank=new ManageAccount[ManageAccount.num]; | ||
String[] accountName={new String("A"),new String("B"),new String("C"),new String("D"),new String("E"), | ||
new String("F"),new String("G"),new String("H"),new String("I"),new String("J"),}; | ||
for (int j=0;j<ManageAccount.num;j++){ | ||
bank[j]=new ManageAccount(accountName[j],100); | ||
ManageAccount.accounts[j].print();;//print it | ||
} | ||
|
||
|
||
//start the threads | ||
for (int k=0;k<ManageAccount.num;k++){ | ||
bank[k].start(); | ||
} | ||
|
||
// wait until all are finished | ||
for (int k=0;k<ManageAccount.num;k++){ | ||
bank[k].join(); | ||
} | ||
ManageAccount.printAllAccounts(); | ||
|
||
//updating the output file | ||
boolean bug = false; | ||
//flags which will indicate the kind of the bug | ||
for (int k=0;k<ManageAccount.num;k++){ | ||
//System.out.println("account "+k+" has $"+ManageAccount.accounts[k].amount); | ||
if(ManageAccount.accounts[k].amount<300){ | ||
bug=true; | ||
} | ||
else if(ManageAccount.accounts[k].amount>300){ | ||
bug=true; | ||
} | ||
} | ||
|
||
if(bug) | ||
throw new RuntimeException("bug found"); | ||
|
||
} catch(InterruptedException e){ | ||
} | ||
|
||
}//end of function main | ||
}//end of class Main |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
package account; | ||
|
||
/** | ||
* Title: Software Testing course | ||
* Description: The goal of the exercise is implementing a program which demonstrate a parallel bug. | ||
* In the exercise we have two accounts.The program enable tranfering money from one account to the other.Although the functions were defended by locks (synchronize) there exists an interleaving which we'll experience a bug. | ||
* Copyright: Copyright (c) 2003 | ||
* Company: Haifa U. | ||
* @author Maya Maimon | ||
* @version 1.0 | ||
*/ | ||
|
||
public class ManageAccount extends Thread { | ||
Account account; | ||
static Account[] accounts=new Account[10] ;//we may add more later to increase the parallelism level | ||
static int num=2;//the number of the accounts | ||
static int accNum=0;//index to insert the next account | ||
int i;//the index | ||
|
||
public ManageAccount(String name,double amount) { | ||
account=new Account(name,amount); | ||
i=accNum; | ||
accounts[i]=account; | ||
accNum=(accNum+1)%num;//the next index in a cyclic order | ||
} | ||
|
||
public void run(){ | ||
account.depsite(300); | ||
account.transfer(accounts[(i+1)%num],10); | ||
account.depsite(10); | ||
account.transfer(accounts[(i+2)%num],10); | ||
account.withdraw(20); | ||
account.depsite(10); | ||
account.transfer(accounts[(i+1)%num],10); | ||
account.withdraw(100); | ||
} | ||
|
||
static public void printAllAccounts(){ | ||
for (int j=0;j<num;j++){ | ||
if( ManageAccount.accounts[j]!=null){ | ||
ManageAccount.accounts[j].print();;//print it | ||
} | ||
} | ||
} | ||
|
||
}//end of class ManageAccount |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
package com.test; | ||
|
||
import java.io.BufferedInputStream; | ||
import java.io.DataInputStream; | ||
import java.io.DataOutputStream; | ||
import java.io.IOException; | ||
import java.net.ServerSocket; | ||
import java.net.Socket; | ||
import com.facebook.infer.annotation.ThreadSafe; | ||
|
||
@ThreadSafe | ||
public class ThreadA { | ||
|
||
byte[] messageByte = new byte[100]; | ||
|
||
public void foo(boolean read) { | ||
ServerSocket server; | ||
Socket clientSocket = null; | ||
int currentBytesRead; | ||
|
||
try { | ||
server = new ServerSocket(8080); | ||
Socket socket = server.accept(); | ||
|
||
DataInputStream in = new DataInputStream(new BufferedInputStream(socket.getInputStream())); | ||
DataOutputStream out = new DataOutputStream(clientSocket.getOutputStream()); | ||
|
||
if(read) | ||
currentBytesRead = in.read(messageByte); | ||
else | ||
out.write(messageByte); | ||
} catch (IOException e) { | ||
e.printStackTrace(); } | ||
} | ||
} |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
package wrongLock; | ||
|
||
import com.facebook.infer.annotation.*; | ||
/** | ||
* @author Xuan | ||
* Created on 2005-1-18 | ||
* <p> | ||
* This class simulates the wrong lock bug | ||
* Method A requests a lock on data while method B request a lock | ||
* on the class. | ||
*/ | ||
@ThreadSafe | ||
public class WrongLock { | ||
Data data; | ||
|
||
public WrongLock(Data data) { | ||
this.data = data; | ||
} | ||
|
||
public void A() { | ||
synchronized (data) { | ||
int x = data.value; | ||
data.value++; | ||
//assert (data.value==x+1); | ||
if (data.value != (x + 1)) | ||
throw new RuntimeException("bug found"); | ||
} | ||
} | ||
|
||
public void B() { | ||
synchronized (this) { | ||
data.value++; | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
{"infer":"/Users/andrea/git/infer-clean/infer/infer/bin/infer", | ||
"options":["--racerdfix-only", "--starvation"], | ||
"json_path": "./infer-out/", | ||
"target_options": ["--", "javac", "src/test/resources/java-benchmark/deadlock-paper/Hello.java"], | ||
"prio_files": [], | ||
"iterations": 10, | ||
"hippodrome_options": ["--atomicity=true"] | ||
} |
Oops, something went wrong.