Update readme and add examples

README.md

@@ -1,3 +1,203 @@
-# latte: Lightweight Aliasing Tracking for Java
+# Latte: Lightweight Aliasing Tracking for Java
 
-Small project following the paper https://arxiv.org/pdf/2309.05637.pdf
+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.
+
+For more details, check our [research paper](https://arxiv.org/pdf/2309.05637).
+
+## Overview
+
+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.
+
+## Latte Annotations System
+
+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:
+
+- For parameters:
+  - `@Free` - For parameters that are globally unique. When a caller passes an argument to a `@Free` parameter, they cannot observe that value again.
+  - `@Borrowed` - For parameters that are unique in the callee's scope but may be stored elsewhere on the heap or stack.
+- For fields:
+  - `@Unique` - For fields that cannot be aliased with other fields.
+- For both:
+  - `@Shared` - For parameters or fields that can be shared, so they have no uniqueness guarantees.
+
+Local variables are not annotated and start with a default annotation that allows them to take the assignment's permissions.
+
+## Project Structure
+
+```
+latte-umbrella/
+├── src/
+│   └── main/
+│       └── java/
+│           ├── latte/
+│           │   └── latte_umbrella/
+│           │       └── App.java  # Main application entry point
+│           └── examples/         # Test examples for the analysis
+│   └── test/
+│       └── java/
+│           ├── AppTest.java # Creating JUnit tests
+│       └── examples/ # Java classes to be used in the JUnit tests
+
+```
+
+## Getting Started
+
+### Prerequisites
+
+- Java 11 or higher
+- Maven
+
+### Prerequisites
+
+- Java 11 or higher
+- Maven
+
+### Installation
+
+Clone the repository and build with Maven:
+
+```bash
+git clone https://github.com/your-username/latte.git
+cd latte
+mvn clean install
+```
+
+To use Latte in your Java projects, you need to:
+1. Add the latte.jar to your project dependencies
+2. Import the specifications in your files (e.g., `import specification.Free`)
+
+
+### Usage
+
+Run the tool against your Java code by executing the main application:
+
+```bash
+java -cp target/latte-umbrella-1.0.0.jar latte.latte_umbrella.App [options] <file-to-analyze>
+```
+
+## Running Examples
+
+The project includes example files to test the analysis capabilities:
+
+```bash
+# Run the analysis on a specific example
+java -cp target/latte-umbrella-1.0.0.jar latte.latte_umbrella.App src/main/java/examples/Example1.java
+```
+
+## Example
+
+Here is an example of Java classes using the Latte annotations:
+
+```java
+class Node {
+    @Unique Object value;   // Field value is Unique
+    @Unique Node next;      // Field next is Unique
+
+
+    public Node (@Free Object value, @Free Node next) {
+        // We can assign @Free objects to Unique fields given that they have no aliases
+        this.value = value; 
+        this.next = next;
+    }
+}
+
+public class MyStack {
+
+    @Unique Node root;          // Field root is Unique		
+
+    public MyStack(@Free Node root) {
+        this.root = root;       // Since root is @Free we can assign it to root:@Unique		
+    }
+
+    void push(@Free Object value) {	
+        Node r;                 // Local variables start with a default annotation that allows
+        Node n;                 // them to take the assignment's permissions
+
+        r = this.root; 			// r is an alias to this.root with permission @Unique
+        this.root = null; 		// Nullify this.root so there is only one pointer to the 
+                                // value of the root, no other aliases
+        n = new Node(value, r); // Create new root with values that have no aliases. The constructors  
+                                // always return an new object that is @Free 
+        this.root = n; 			// Replace root with a new value that is @Free and so can be assigned 
+                                // to an @Unique field
+    }
+}
+```
+
+## Testing
+
+Tests can be run using Maven:
+
+```bash
+mvn test
+```
+
+You can also test the tool directly on the example files:
+
+```bash
+java -cp target/latte-umbrella-1.0.0.jar latte.latte_umbrella.App src/main/java/examples/MyStack.java
+```
+
+## Contributing
+
+We welcome contributions to Latte! Here's how to get started:
+
+### Development Workflow
+
+1. **Create a new branch for your feature:**
+   ```bash
+   git checkout -b feature/your-feature-name
+   ```
+
+2. **Make your changes and commit them:**
+   ```bash
+   git add .
+   git commit -m "Description of your changes"
+   ```
+
+3. **Set the upstream branch and push your changes:**
+   ```bash
+   git push --set-upstream origin feature/your-feature-name
+   ```
+
+4. **Create a Pull Request:**
+   - Go to the repository on GitHub
+   - Click on "Pull Requests" > "New Pull Request"
+   - Select your branch
+   - Fill in the PR template with details about your changes
+   - Request a review from a team member
+
+5. **Address review feedback** and update your PR as needed
+
+### Code Standards
+
+- Follow Java code conventions
+- Write unit tests for new functionality
+- Update documentation for any changes
+
+## Known Limitations
+
+The tool is still under active development, and some features are limited:
+
+- Does not support if statements without else branches
+- Limited verification of aliases related to while loops
+- Limited support for complex collections and generics
+
+## Future Work
+
+We are continuously improving Latte to support more complex Java patterns and enhance the aliasing tracking capabilities.
+
+## Contributing Issues
+
+If you encounter any problems while using Latte, please add an Issue to the repository with:
+- A description of the problem
+- Code sample that demonstrates the issue
+- Expected vs. actual behavior
+
+## License
+
+[Your license here]
+
+## Contact
+
+[Your contact information here]

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

@@ -213,10 +213,7 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
 			CtParameter<?> p = m.getParameters().get(i);
 			UniquenessAnnotation expectedUA = new UniquenessAnnotation(p);
 			UniquenessAnnotation vvPerm = permEnv.get(vv);
-			// {𝜈𝑖 : borrowed ≤ 𝛼𝑖 }
-			if (!vvPerm.isGreaterEqualThan(Uniqueness.BORROWED)){
-				logError(String.format("Symbolic value %s:%s is not greater than BORROWED", vv, vvPerm), arg);
-			}
+
 			logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA));
 			// Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′
 			if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA))
@@ -227,7 +224,12 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
 
 		// distinct(Δ′, {𝜈𝑖 : borrowed ≤ 𝛼𝑖 })
 		// distinct(Δ, 𝑆) ⇐⇒ ∀𝜈, 𝜈′ ∈ 𝑆 : Δ ⊢ 𝜈 ⇝ 𝜈′ =⇒ 𝜈 = 𝜈′
-		if (!symbEnv.distinct(paramSymbValues)){
+		List<SymbolicValue> check_distinct = new ArrayList<>();
+		for(SymbolicValue sv: paramSymbValues)
+			if (permEnv.get(sv).isGreaterEqualThan(Uniqueness.BORROWED))
+				check_distinct.add(sv);
+
+		if (!symbEnv.distinct(check_distinct)){
 			logError(String.format("Non-distinct parameters in constructor call of %s", klass.getSimpleName()), invocation);
 		}
 
@@ -653,7 +655,7 @@ public <T> void visitCtLiteral(CtLiteral<T> literal) {
 
 		// Get a fresh symbolic value and add it to the environment with a shared default value
 		SymbolicValue sv = symbEnv.getFresh();
-		UniquenessAnnotation ua = new UniquenessAnnotation(Uniqueness.FREE);
+		UniquenessAnnotation ua = new UniquenessAnnotation(Uniqueness.SHARED);
 
 		if (literal.getValue() == null)
 			ua = new UniquenessAnnotation(Uniqueness.FREE);  // its a null literal

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

@@ -0,0 +1,94 @@
+package examples;
+
+
+import java.util.TimerTask;
+
+import specification.Borrowed;
+import specification.Free;
+import specification.Unique;
+
+public class ResultSetForwardOnly {
+    /*
+     * Error ResultSet is FORWARD_ONLY and we try to get a value before
+     */
+    public static void example6367737(Connection con, String username, String password ) throws Exception {
+
+        // Step 1) Prepare the statement
+        PreparedStatement pstat =
+          con.prepareStatement("select typeid from users where username=? and password=?");  
+
+        // Step 2) Set parameters for the statement
+        pstat.setString(1, username);
+        pstat.setString(2, password);
+
+        // Step 3) Execute the query
+        ResultSet rs = pstat.executeQuery();
+
+        // Step 4) Process the result
+        int rowCount=0;
+        while(rs.next()){       
+            rowCount++;         
+        }
+
+        // ERROR! because it is FORWARD_ONLY, we cannot go back and check beforeFirst
+        rs.beforeFirst(); 
+
+        int typeID = 0; // ...
+
+        // To be correct we need to change the resultset to be scrollable
+        /*PreparedStatement pstat =      
+          con.prepareStatement("select typeid from users where username=? and password=?",
+          ResultSet.TYPE_SCROLL_SENSITIVE, 
+          ResultSet.CONCUR_UPDATABLE);
+        */
+      }
+
+
+    class Connection{
+
+        // Result sets created using the returned PreparedStatement object will by default be type TYPE_FORWARD_ONLY 
+        // and have a concurrency level of CONCUR_READ_ONLY.
+        @Unique // @StateRefinement (return, to="TYPE_FORWARD_ONLY, CONCUR_READ_ONLY")
+        public PreparedStatement prepareStatement(String s) {
+            return new PreparedStatement();
+        }
+
+        @Unique // @StateRefinement (return, to="type == resultSetType")
+        public PreparedStatement prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){
+            return new PreparedStatement();
+
+        }
+    }
+
+    //  @Ghost("type")
+    class PreparedStatement{
+
+        void setString(int index, String s){}
+
+        // @StateRefinement(return, to="type != TYPE_FORWARD_ONLY, col == -1")
+        ResultSet executeQuery(String s){return null;}
+
+        // @StateRefinement(return, to="type, col == -1")
+        ResultSet executeQuery(){return null;}
+    }
+
+    // @Ghost("type")
+    class ResultSet{
+
+        // @StateRefinement(this, type == )
+        void beforeFirst(){}
+
+        // @StateRefinement(this, col > 0)
+        float getFloat(String s){return 0;}
+
+        // @StateRefinement(this, col > 0)
+        int getInt(int s){return 0;}
+
+        // @StateRefinement(this, col == old(col) + 1)
+        boolean next(){return true;}
+    }
+
+
+}
+
+