From f1d7edec81b87000ce6425e385e6464b9abfa9f5 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 11:14:50 +0000 Subject: [PATCH 1/8] only check distinct for borrowed or higher permissions in invocation --- .../main/java/typechecking/LatteTypeChecker.java | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/latte-umbrella/src/main/java/typechecking/LatteTypeChecker.java b/latte-umbrella/src/main/java/typechecking/LatteTypeChecker.java index be62cf7..3bc1005 100644 --- a/latte-umbrella/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte-umbrella/src/main/java/typechecking/LatteTypeChecker.java @@ -213,10 +213,7 @@ public void visitCtInvocation(CtInvocation 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 void visitCtInvocation(CtInvocation invocation) { // distinct(Ξ”β€², {πœˆπ‘– : borrowed ≀ 𝛼𝑖 }) // distinct(Ξ”, 𝑆) ⇐⇒ βˆ€πœˆ, πœˆβ€² ∈ 𝑆 : Ξ” ⊒ 𝜈 ⇝ πœˆβ€² =β‡’ 𝜈 = πœˆβ€² - if (!symbEnv.distinct(paramSymbValues)){ + List 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 void visitCtLiteral(CtLiteral 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 From bb6d6b4fe9956ba952850974691f5afd2d7dd9cf Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 11:32:02 +0000 Subject: [PATCH 2/8] add example for urlconnection reuse --- .../URLConnectionReuseConnection.java | 57 +++++++++++++++++++ .../java/latte/latte_umbrella/AppTest.java | 11 +++- 2 files changed, 67 insertions(+), 1 deletion(-) create mode 100644 latte-umbrella/src/test/examples/URLConnectionReuseConnection.java diff --git a/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java b/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java new file mode 100644 index 0000000..32b3e87 --- /dev/null +++ b/latte-umbrella/src/test/examples/URLConnectionReuseConnection.java @@ -0,0 +1,57 @@ +import specification.Borrowed; +import specification.Unique; + +public class URLConnectionReuseConnection { + + public static void example4278917(@Borrowed URL address) { + + try { + // Step 1) Open the connection + URLConnection connection = address.openConnection(); // returns a unique object + + // Step 2) Connect + connection.connect(); + + /* Other code in original question */ + + // Step 3) Setup parameters and connection properties after connection == ERROR + connection.setAllowUserInteraction(true); + connection.addRequestProperty("AUTHENTICATION_REQUEST_PROPERTY", "authorizationRequest"); + connection.getHeaderFields(); + + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } +} + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="interact") + void getHeaderFields(){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} +} + diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 32e0fd0..3f668a8 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -76,7 +76,6 @@ public void testBox1(){ e.printStackTrace(); assert(false); } - } @@ -90,6 +89,16 @@ public void testHttpEntityNoAnnotations(){ } } + @Test + public void testURLConnectionReuseConnection(){ + try { + App.launcher("src/test/examples/URLConnectionReuseConnection.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } + /* * Incorrect Examples */ From e1352e3e5b07528f090e4d944ce334d69f090cc2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 12:07:35 +0000 Subject: [PATCH 3/8] url connection set property example --- .../examples/URLConnectionSetProperty1.java | 79 +++++++++++++++++++ .../java/latte/latte_umbrella/AppTest.java | 10 +++ 2 files changed, 89 insertions(+) create mode 100644 latte-umbrella/src/test/examples/URLConnectionSetProperty1.java diff --git a/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java b/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java new file mode 100644 index 0000000..e3467d6 --- /dev/null +++ b/latte-umbrella/src/test/examples/URLConnectionSetProperty1.java @@ -0,0 +1,79 @@ +import specification.Borrowed; +import specification.Unique; +import java.io.IOException; +import java.io.InputStream; + +public class URLConnectionSetProperty1 { + + public static void example331538(@Borrowed URL address) { + try { + + // Step 1) Open the connection + URLConnection cnx = address.openConnection(); + + // Step 2) Setup parameters and connection properties + cnx.setAllowUserInteraction(false); // Step 2) + cnx.setDoOutput(true); + cnx.addRequestProperty("User-Agent", + "Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.0)"); + + + // Step 3) + cnx.connect(); + + // Step 4) + cnx.getContent(); + + // Get the input stream and process it + InputStream is = cnx.getInputStream(); + System.out.println("Successfully opened input stream."); + + // Ensure to close the InputStream after use + is.close(); + + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } +} + + + + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setDoOutput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} + + //@StateRefinement(this, from="interact") + void getContent(){} + + + //@StateRefinement(this, from="interact") + @Unique //????? Not sure: Returns an input stream that reads from this open connection. + InputStream getInputStream(){ return null;} + +} \ No newline at end of file diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 3f668a8..6e7b147 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -98,6 +98,16 @@ public void testURLConnectionReuseConnection(){ assert(false); } } + + @Test + public void testURLConnectionSetProperty1(){ + try { + App.launcher("src/test/examples/URLConnectionSetProperty1.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } /* * Incorrect Examples From 4ba1475a3fa49680cdd905c4c98f3bbf383c0664 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 13:49:49 +0000 Subject: [PATCH 4/8] add examples urlconnection property with several methods --- ...ConnectionSetPropertyMultipleComplete.java | 114 ++++++++++++++++++ ...URLConnectionSetPropertyMultipleShort.java | 103 ++++++++++++++++ .../java/latte/latte_umbrella/AppTest.java | 10 ++ 3 files changed, 227 insertions(+) create mode 100644 latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java create mode 100644 latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java diff --git a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java b/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java new file mode 100644 index 0000000..a50dd0a --- /dev/null +++ b/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleComplete.java @@ -0,0 +1,114 @@ +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; + +import specification.Borrowed; +import specification.Shared; +import specification.Unique; + +public class URLConnectionSetPropertyMultipleComplete { + + String sessionId = "1234"; + public void example5368535(@Borrowed URL address, String content) { + try { + URLConnection con = openConnection(address, true, true, "POST"); + + //ERROR write before set + writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() + setCookies(con); // writeOutput calls cnx.setRequestProperty + + con.connect(); + + System.out.println("Request completed successfully."); + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } + + // Exactly from the original code + @Unique + public URLConnection openConnection(@Borrowed URL url, boolean in, boolean out, String requestMethode) throws IOException{ + URLConnection con = url.openConnection(); + con.setDoInput(in); + con.setDoOutput (out); + con.setRequestMethod(requestMethode); + con.setRequestProperty ("Content-Type", "application/x-www-form-urlencoded"); + return con; + } + + // Set cookies + private void setCookies(@Borrowed URLConnection cnx) { + if (sessionId != null) { + cnx.setRequestProperty("Cookie", sessionId); + System.out.println("Cookie set: " + sessionId); + } + } + + // Write content + private void writeToOutput(@Borrowed URLConnection cnx, String content) throws IOException { + try { + OutputStream os = cnx.getOutputStream() ; + os.write(content.getBytes()); + os.flush(); + os.close(); + } catch (IOException e) { + System.err.println("Error writing content: " + e.getMessage()); + throw e; + } + } + +} + + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setDoOutput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setRequestProperty(String a, String b){} + + //@StateRefinement(this, from="manipulate") + void setRequestMethod(String a){} + + //@StateRefinement(this, from="manipulate") + void setDoInput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} + + //@StateRefinement(this, from="interact") + void getContent(){} + + + //@StateRefinement(this, from="interact") + @Unique //????? Not sure: Returns an input stream that reads from this open connection. + InputStream getInputStream(){ return null;} + + + //@StateRefinement(this, from="interact") + @Shared //????? Not sure: Returns an output stream that writes to this connection. + OutputStream getOutputStream(){ return null;} + +} \ No newline at end of file diff --git a/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java b/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java new file mode 100644 index 0000000..3a2792d --- /dev/null +++ b/latte-umbrella/src/test/examples/URLConnectionSetPropertyMultipleShort.java @@ -0,0 +1,103 @@ +import java.io.IOException; +import java.io.InputStream; +import java.io.OutputStream; + +import specification.Borrowed; +import specification.Shared; +import specification.Unique; + +public class URLConnectionSetPropertyMultipleShort { + + String sessionId = "1234"; + public void example5368535(@Borrowed URL address, String content) { + try { + URLConnection con = openConnection(address, true, true, "POST"); + + //ERROR write before set + writeToOutput(con, content); // writeOutput calls cnx.getOutputStream() + setCookies(con); // writeOutput calls cnx.setRequestProperty + + con.connect(); + + System.out.println("Request completed successfully."); + } catch (IOException e) { + // Handle exceptions related to network or stream issues + System.err.println("Error: " + e.getMessage()); + } + } + + // Setters + @Unique // @StateRefinement(return, to="manipulate") + public URLConnection openConnection(@Borrowed URL url, boolean in, boolean out, + String requestMethode) throws IOException { + URLConnection con = url.openConnection(); + con.setDoInput(in); + con.setDoOutput (out); + return con; + } + + // Set cookies + // @StateRefinement(cnx, from="manipulate") + private void setCookies(@Borrowed URLConnection cnx) { + cnx.setRequestProperty("Cookie", sessionId); + } + + // Write content + // @StateRefinement(cnx, from="interact") + private void writeToOutput(@Borrowed URLConnection cnx, String content) throws IOException { + cnx.getOutputStream(); + } +} + + +class URL{ + @Unique // @StateRefinement (return, to="manipulate") + public URLConnection openConnection() { + return new URLConnection(); + } +} + + +/** + * --- openConnection() ----> [MANIPULATE PARAMS] ------> connect() -----> [INTERACT] + * setAllowUserInteraction() getContent() + * addRequestProperty()... getHeaderFields()... + */ +// @StateSet({"manipulate", "interact"}) +class URLConnection{ + + //@StateRefinement(this, from="manipulate") + void setAllowUserInteraction(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setDoOutput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void setRequestProperty(String a, String b){} + + //@StateRefinement(this, from="manipulate") + void setRequestMethod(String a){} + + //@StateRefinement(this, from="manipulate") + void setDoInput(boolean b){} + + //@StateRefinement(this, from="manipulate") + void addRequestProperty(String s1, String s2){} + + //@StateRefinement(this, from="manipulate", to="interact") + void connect() throws IOException {} + + //@StateRefinement(this, from="interact") + void getContent(){} + + + //@StateRefinement(this, from="interact") + @Unique //????? Not sure: Returns an input stream that reads from this open connection. + InputStream getInputStream(){ return null;} + + + //@StateRefinement(this, from="interact") + @Shared //????? Not sure: Returns an output stream that writes to this connection. + OutputStream getOutputStream(){ return null;} + +} diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 6e7b147..9e9ca96 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -108,6 +108,16 @@ public void testURLConnectionSetProperty1(){ assert(false); } } + + @Test + public void testURLConnectionSetPropertyMultipleShort(){ + try { + App.launcher("src/test/examples/URLConnectionSetPropertyMultipleShort.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } /* * Incorrect Examples From 57df128336299ce0e1efbe4fe5d2415ff3809a1a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 14:19:20 +0000 Subject: [PATCH 5/8] add example for timertask --- .../examples/TimerTaskCannotReschedule.java | 59 +++++++++++++++++++ .../java/latte/latte_umbrella/AppTest.java | 10 ++++ 2 files changed, 69 insertions(+) create mode 100644 latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java diff --git a/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java b/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java new file mode 100644 index 0000000..cdb64d8 --- /dev/null +++ b/latte-umbrella/src/test/examples/TimerTaskCannotReschedule.java @@ -0,0 +1,59 @@ +import java.util.TimerTask; + +import specification.Borrowed; +import specification.Free; + +public class TimerTaskCannotReschedule { + + /* + * Error cannot reschedule a timer + */ + public static void example1801324_simplified( @Borrowed Timer timer, String sessionKey, @Free TimerTask tt) { + + // Step 2) Cancel the timer + timer.cancel(); + + // Step 3 Schedule a new task for this timer -> ERROR Cannot reschedule a Timer + timer.schedule(tt , 1000); + } + +} + +/* + * [If the timer is cancelled] any further attempt to schedule a task on the timer will result in an IllegalStateException + * + * START --- schedule() ----> [SCHEDULED]--------> + * ----------------------------------------> cancel() -----> [CANCELLED] (no further scheduling allowed) + */ +class Timer{ + //@StateRefinement(this, to="cancelled") + public void cancel() { } + + // @StateRefinement(this, from="start", to="scheduled") + public void schedule(TimerTask task, /* delay > 0 */int delay) {} + +} + + +// /* +// * Error cannot reschedule a timer +// */ +// public static void example1801324( Map timers, String sessionKey) { + +// // Step 1) Get the timer +// Timer timer = timers.get(sessionKey); + +// // Step 2) Cancel the timer +// timer.cancel(); + +// // Step 3) Schedule a new task for this timer -> ERROR Cannot reschedule a Timer +// timer.schedule(new TimerTask() { +// @Override +// public void run() { +// System.out.println("Timer task completed."); +// } +// }, 1000); +// } + + + diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 9e9ca96..67f3978 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -118,6 +118,16 @@ public void testURLConnectionSetPropertyMultipleShort(){ assert(false); } } + + @Test + public void testTimerTaskCannotReschedule(){ + try { + App.launcher("src/test/examples/TimerTaskCannotReschedule.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } /* * Incorrect Examples From a7035ecf9d70fbed0c7d209fb98d0b877e718a60 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 14:51:10 +0000 Subject: [PATCH 6/8] add example result set without calling next --- .../src/test/examples/ResultSetNoNext.java | 64 +++++++++++++++++++ .../java/latte/latte_umbrella/AppTest.java | 10 +++ 2 files changed, 74 insertions(+) create mode 100644 latte-umbrella/src/test/examples/ResultSetNoNext.java diff --git a/latte-umbrella/src/test/examples/ResultSetNoNext.java b/latte-umbrella/src/test/examples/ResultSetNoNext.java new file mode 100644 index 0000000..daf205b --- /dev/null +++ b/latte-umbrella/src/test/examples/ResultSetNoNext.java @@ -0,0 +1,64 @@ + +import java.util.TimerTask; + +import specification.Borrowed; +import specification.Free; +import specification.Unique; + +public class ResultSetNoNext { + + + /* + * Error - in ResultSet, after executing the query we need to call next() before getting a value + */ + public static void example6367737(@Borrowed 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 parentMessage = pstat.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + + float avgsum = parentMessage.getFloat("IMPAVG"); // Error because we are trying to get a value before next + // To be correct we need to call next() before the getter + } + + + 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(); + } + + // To change resultSetType + // prepareStatement​(String sql, int resultSetType, int resultSetConcurrency){} + } + + + class PreparedStatement{ + void setString(int index, String s){} + + // @StateRefinement(return, to="TYPE_FORWARD_ONLY, col == -1") + ResultSet executeQuery(String s){return null;} + } + + class ResultSet{ + // @StateRefinement(this, col > 0) + float getFloat(String s){return 0;} + + // @StateRefinement(this, col == old(col) + 1) + void next(){} + } + + +} + + diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 67f3978..8883cde 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -128,6 +128,16 @@ public void testTimerTaskCannotReschedule(){ assert(false); } } + + @Test + public void testResultSetNoNext(){ + try { + App.launcher("src/test/examples/ResultSetNoNext.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } /* * Incorrect Examples From ea84ba655c415a1e4e87ab5a34c0def89001d96e Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 12 Feb 2025 15:05:41 +0000 Subject: [PATCH 7/8] add example for resultsetforwardonly --- .../test/examples/ResultSetForwardOnly.java | 94 +++++++++++++++++++ .../java/latte/latte_umbrella/AppTest.java | 10 ++ 2 files changed, 104 insertions(+) create mode 100644 latte-umbrella/src/test/examples/ResultSetForwardOnly.java diff --git a/latte-umbrella/src/test/examples/ResultSetForwardOnly.java b/latte-umbrella/src/test/examples/ResultSetForwardOnly.java new file mode 100644 index 0000000..5a9c115 --- /dev/null +++ b/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;} + } + + +} + + diff --git a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java index 8883cde..23a861a 100644 --- a/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java +++ b/latte-umbrella/src/test/java/latte/latte_umbrella/AppTest.java @@ -138,6 +138,16 @@ public void testResultSetNoNext(){ assert(false); } } + + @Test + public void testResultSetForwardOnly(){ + try { + App.launcher("src/test/examples/ResultSetForwardOnly.java"); + } catch (Exception e) { + e.printStackTrace(); + assert(false); + } + } /* * Incorrect Examples From c051a616b376d2360fa8eae8779dc38dd23bb535 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 11 Apr 2025 11:52:50 +0100 Subject: [PATCH 8/8] updated --- README.md | 204 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 202 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 5a9a354..65213f5 100644 --- a/README.md +++ b/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] +``` + +## 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] \ No newline at end of file