Skip to content

Commit 2d3aa3e

Browse files
CatarinaGamboaCatarinaGamboa
authored
Update readme and add examples (#1)
* only check distinct for borrowed or higher permissions in invocation * add example for urlconnection reuse * url connection set property example * add examples urlconnection property with several methods * add example for timertask * add example result set without calling next * add example for resultsetforwardonly * updated
1 parent 3290646 commit 2d3aa3e

10 files changed

Lines changed: 840 additions & 9 deletions

‎README.md‎

Lines changed: 202 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,203 @@
1-
# latte: Lightweight Aliasing Tracking for Java
1+
# Latte: Lightweight Aliasing Tracking for Java
22

3-
Small project following the paper https://arxiv.org/pdf/2309.05637.pdf
3+
Latte is a lightweight static analysis tool for tracking aliasing in Java programs. This tool allows you to annotate your programs with permissions where aliases are tracked to prevent bugs related to unexpected object references and side effects.
4+
5+
For more details, check our [research paper](https://arxiv.org/pdf/2309.05637).
6+
7+
## Overview
8+
9+
Latte enables developers to identify and track aliasing relationships in their Java code using a permission-based type system. The tool statically verifies aliasing properties to help prevent common concurrency and memory management bugs.
10+
11+
## Latte Annotations System
12+
13+
Latte uses annotations to specify the permissions of fields and parameters to track their uniqueness properties and the aliases that are created throughout the program:
14+
15+
- For parameters:
16+
- `@Free` - For parameters that are globally unique. When a caller passes an argument to a `@Free` parameter, they cannot observe that value again.
17+
- `@Borrowed` - For parameters that are unique in the callee's scope but may be stored elsewhere on the heap or stack.
18+
- For fields:
19+
- `@Unique` - For fields that cannot be aliased with other fields.
20+
- For both:
21+
- `@Shared` - For parameters or fields that can be shared, so they have no uniqueness guarantees.
22+
23+
Local variables are not annotated and start with a default annotation that allows them to take the assignment's permissions.
24+
25+
## Project Structure
26+
27+
```
28+
latte-umbrella/
29+
├── src/
30+
│ └── main/
31+
│ └── java/
32+
│ ├── latte/
33+
│ │ └── latte_umbrella/
34+
│ │ └── App.java # Main application entry point
35+
│ └── examples/ # Test examples for the analysis
36+
│ └── test/
37+
│ └── java/
38+
│ ├── AppTest.java # Creating JUnit tests
39+
│ └── examples/ # Java classes to be used in the JUnit tests
40+
41+
```
42+
43+
## Getting Started
44+
45+
### Prerequisites
46+
47+
- Java 11 or higher
48+
- Maven
49+
50+
### Prerequisites
51+
52+
- Java 11 or higher
53+
- Maven
54+
55+
### Installation
56+
57+
Clone the repository and build with Maven:
58+
59+
```bash
60+
git clone https://github.com/your-username/latte.git
61+
cd latte
62+
mvn clean install
63+
```
64+
65+
To use Latte in your Java projects, you need to:
66+
1. Add the latte.jar to your project dependencies
67+
2. Import the specifications in your files (e.g., `import specification.Free`)
68+
69+
70+
### Usage
71+
72+
Run the tool against your Java code by executing the main application:
73+
74+
```bash
75+
java -cp target/latte-umbrella-1.0.0.jar latte.latte_umbrella.App [options] <file-to-analyze>
76+
```
77+
78+
## Running Examples
79+
80+
The project includes example files to test the analysis capabilities:
81+
82+
```bash
83+
# Run the analysis on a specific example
84+
java -cp target/latte-umbrella-1.0.0.jar latte.latte_umbrella.App src/main/java/examples/Example1.java
85+
```
86+
87+
## Example
88+
89+
Here is an example of Java classes using the Latte annotations:
90+
91+
```java
92+
class Node {
93+
@Unique Object value; // Field value is Unique
94+
@Unique Node next; // Field next is Unique
95+
96+
97+
public Node (@Free Object value, @Free Node next) {
98+
// We can assign @Free objects to Unique fields given that they have no aliases
99+
this.value = value;
100+
this.next = next;
101+
}
102+
}
103+
104+
public class MyStack {
105+
106+
@Unique Node root; // Field root is Unique
107+
108+
public MyStack(@Free Node root) {
109+
this.root = root; // Since root is @Free we can assign it to root:@Unique
110+
}
111+
112+
void push(@Free Object value) {
113+
Node r; // Local variables start with a default annotation that allows
114+
Node n; // them to take the assignment's permissions
115+
116+
r = this.root; // r is an alias to this.root with permission @Unique
117+
this.root = null; // Nullify this.root so there is only one pointer to the
118+
// value of the root, no other aliases
119+
n = new Node(value, r); // Create new root with values that have no aliases. The constructors
120+
// always return an new object that is @Free
121+
this.root = n; // Replace root with a new value that is @Free and so can be assigned
122+
// to an @Unique field
123+
}
124+
}
125+
```
126+
127+
## Testing
128+
129+
Tests can be run using Maven:
130+
131+
```bash
132+
mvn test
133+
```
134+
135+
You can also test the tool directly on the example files:
136+
137+
```bash
138+
java -cp target/latte-umbrella-1.0.0.jar latte.latte_umbrella.App src/main/java/examples/MyStack.java
139+
```
140+
141+
## Contributing
142+
143+
We welcome contributions to Latte! Here's how to get started:
144+
145+
### Development Workflow
146+
147+
1. **Create a new branch for your feature:**
148+
```bash
149+
git checkout -b feature/your-feature-name
150+
```
151+
152+
2. **Make your changes and commit them:**
153+
```bash
154+
git add .
155+
git commit -m "Description of your changes"
156+
```
157+
158+
3. **Set the upstream branch and push your changes:**
159+
```bash
160+
git push --set-upstream origin feature/your-feature-name
161+
```
162+
163+
4. **Create a Pull Request:**
164+
- Go to the repository on GitHub
165+
- Click on "Pull Requests" > "New Pull Request"
166+
- Select your branch
167+
- Fill in the PR template with details about your changes
168+
- Request a review from a team member
169+
170+
5. **Address review feedback** and update your PR as needed
171+
172+
### Code Standards
173+
174+
- Follow Java code conventions
175+
- Write unit tests for new functionality
176+
- Update documentation for any changes
177+
178+
## Known Limitations
179+
180+
The tool is still under active development, and some features are limited:
181+
182+
- Does not support if statements without else branches
183+
- Limited verification of aliases related to while loops
184+
- Limited support for complex collections and generics
185+
186+
## Future Work
187+
188+
We are continuously improving Latte to support more complex Java patterns and enhance the aliasing tracking capabilities.
189+
190+
## Contributing Issues
191+
192+
If you encounter any problems while using Latte, please add an Issue to the repository with:
193+
- A description of the problem
194+
- Code sample that demonstrates the issue
195+
- Expected vs. actual behavior
196+
197+
## License
198+
199+
[Your license here]
200+
201+
## Contact
202+
203+
[Your contact information here]

‎latte-umbrella/src/main/java/typechecking/LatteTypeChecker.java‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -213,10 +213,7 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
213213
CtParameter<?> p = m.getParameters().get(i);
214214
UniquenessAnnotation expectedUA = new UniquenessAnnotation(p);
215215
UniquenessAnnotation vvPerm = permEnv.get(vv);
216-
// {𝜈𝑖 : borrowed ≤ 𝛼𝑖 }
217-
if (!vvPerm.isGreaterEqualThan(Uniqueness.BORROWED)){
218-
logError(String.format("Symbolic value %s:%s is not greater than BORROWED", vv, vvPerm), arg);
219-
}
216+
220217
logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA));
221218
// Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′
222219
if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA))
@@ -227,7 +224,12 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
227224

228225
// distinct(Δ′, {𝜈𝑖 : borrowed ≤ 𝛼𝑖 })
229226
// distinct(Δ, 𝑆) ⇐⇒ ∀𝜈, 𝜈′ ∈ 𝑆 : Δ ⊢ 𝜈 ⇝ 𝜈′ =⇒ 𝜈 = 𝜈′
230-
if (!symbEnv.distinct(paramSymbValues)){
227+
List<SymbolicValue> check_distinct = new ArrayList<>();
228+
for(SymbolicValue sv: paramSymbValues)
229+
if (permEnv.get(sv).isGreaterEqualThan(Uniqueness.BORROWED))
230+
check_distinct.add(sv);
231+
232+
if (!symbEnv.distinct(check_distinct)){
231233
logError(String.format("Non-distinct parameters in constructor call of %s", klass.getSimpleName()), invocation);
232234
}
233235

@@ -653,7 +655,7 @@ public <T> void visitCtLiteral(CtLiteral<T> literal) {
653655

654656
// Get a fresh symbolic value and add it to the environment with a shared default value
655657
SymbolicValue sv = symbEnv.getFresh();
656-
UniquenessAnnotation ua = new UniquenessAnnotation(Uniqueness.FREE);
658+
UniquenessAnnotation ua = new UniquenessAnnotation(Uniqueness.SHARED);
657659

658660
if (literal.getValue() == null)
659661
ua = new UniquenessAnnotation(Uniqueness.FREE); // its a null literal

‎latte-umbrella/src/test/examples/ResultSetForwardOnly.java‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
package examples;
2+
3+
4+
import java.util.TimerTask;
5+
6+
import specification.Borrowed;
7+
import specification.Free;
8+
import specification.Unique;
9+
10+
public class ResultSetForwardOnly {
11+
/*
12+
* Error ResultSet is FORWARD_ONLY and we try to get a value before
13+
*/
14+
public static void example6367737(Connection con, String username, String password ) throws Exception {
15+
16+
// Step 1) Prepare the statement
17+
PreparedStatement pstat =
18+
con.prepareStatement("select typeid from users where username=? and password=?");
19+
20+
// Step 2) Set parameters for the statement
21+
pstat.setString(1, username);
22+
pstat.setString(2, password);
23+
24+
// Step 3) Execute the query
25+
ResultSet rs = pstat.executeQuery();
26+
27+
// Step 4) Process the result
28+
int rowCount=0;
29+
while(rs.next()){
30+
rowCount++;
31+
}
32+
33+
// ERROR! because it is FORWARD_ONLY, we cannot go back and check beforeFirst
34+
rs.beforeFirst();
35+
36+
int typeID = 0; // ...
37+
38+
// To be correct we need to change the resultset to be scrollable
39+
/*PreparedStatement pstat =
40+
con.prepareStatement("select typeid from users where username=? and password=?",
41+
ResultSet.TYPE_SCROLL_SENSITIVE,
42+
ResultSet.CONCUR_UPDATABLE);
43+
*/
44+
}
45+
46+
47+
class Connection{
48+
49+
// Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY
50+
// and have a concurrency level of CONCUR_READ_ONLY.
51+
@Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY")
52+
public PreparedStatement prepareStatement(String s) {
53+
return new PreparedStatement();
54+
}
55+
56+
@Unique // @StateRefinement (return, to="type == resultSetType")
57+
public PreparedStatement prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){
58+
return new PreparedStatement();
59+
60+
}
61+
}
62+
63+
// @Ghost("type")
64+
class PreparedStatement{
65+
66+
void setString(int index, String s){}
67+
68+
// @StateRefinement(return, to="type != TYPE_FORWARD_ONLY, col == -1")
69+
ResultSet executeQuery(String s){return null;}
70+
71+
// @StateRefinement(return, to="type, col == -1")
72+
ResultSet executeQuery(){return null;}
73+
}
74+
75+
// @Ghost("type")
76+
class ResultSet{
77+
78+
// @StateRefinement(this, type == )
79+
void beforeFirst(){}
80+
81+
// @StateRefinement(this, col > 0)
82+
float getFloat(String s){return 0;}
83+
84+
// @StateRefinement(this, col > 0)
85+
int getInt(int s){return 0;}
86+
87+
// @StateRefinement(this, col == old(col) + 1)
88+
boolean next(){return true;}
89+
}
90+
91+
92+
}
93+
94+

0 commit comments

Comments
 (0)