Skip to content

If e1 Then s1 'Else skip' adaptation #21

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Pichers merged 7 commits into from
Jun 16, 2025
Merged

If e1 Then s1 'Else skip' adaptation #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
5352ab6
If e1 Then s1 'Else skip' adaptation
Pichers May 13, 2025
7ac32ca
Added if related tests
Pichers May 20, 2025
ef6521f
Added the use of edited variables after ifs
Pichers Jun 11, 2025
9526f6e
Added new if then skip permission check test
Pichers Jun 15, 2025
826e637
Added an incorrect test for if without else permissions
Pichers Jun 15, 2025
99e3963
Merge branch 'main' into IfNoElseSupport
Pichers Jun 16, 2025
ee05e25
missing comma
Pichers Jun 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 15 additions & 5 deletions latte/src/main/java/typechecking/LatteTypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -534,11 +534,21 @@ public void visitCtIf(CtIf ifElement) {
PermissionEnvironment thenPermEnv = permEnv.cloneLast();
exitScopes();

enterScopes();
super.visitCtBlock(ifElement.getElseStatement());
SymbolicEnvironment elseSymbEnv = symbEnv.cloneLast();
PermissionEnvironment elsePermEnv = permEnv.cloneLast();
exitScopes();
SymbolicEnvironment elseSymbEnv;
PermissionEnvironment elsePermEnv;

if (ifElement.getElseStatement() != null) {
//Else statement
enterScopes();
super.visitCtBlock(ifElement.getElseStatement());
elseSymbEnv = symbEnv.cloneLast();
elsePermEnv = permEnv.cloneLast();
exitScopes();
} else {
//No Else statement
elseSymbEnv = symbEnv.cloneLast();
elsePermEnv = permEnv.cloneLast();
}

joining(thenSymbEnv, thenPermEnv, elseSymbEnv, elsePermEnv);
}
Expand Down
43 changes: 43 additions & 0 deletions latte/src/test/examples/MyNodeAllKindsIfs.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
package latte;

import specification.Free;
import specification.Unique;

/*
* This file is part of the Latte test suite.
*/
class MyNode {

@Unique Object value;
@Unique Node next;

/**
* Constructor for the Node class using @Free value and next nodes
* @param value
* @param next
*/
public MyNode (@Free Object value, @Free Node next) {
this.value = value;
this.next = next;
}

public Object test(@Free Object v1, @Free Object v2, boolean c1, boolean c2){
if (c1) {
this.value = v1;
} else if (c2) {
this.value = v2;
} else {
this.value = v1;
}

if (c2 || this.value == null) {
this.value = v1;
} else {
this.value = v2;
}
if (c1 && this.value == v1) {
this.value = v2;
}
return this.value;
}
}
30 changes: 30 additions & 0 deletions latte/src/test/examples/MyNodeIfNoElse.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
package latte;

import specification.Free;
import specification.Unique;

/*
* This file is part of the Latte test suite.
*/
class MyNode {

@Unique Object value;
@Unique Node next;

/**
* Constructor for the Node class using @Free value and next nodes
* @param value
* @param next
*/
public MyNode (@Free Object value, @Free Node next) {
this.value = value;
this.next = next;
}

public Object test(@Free Object v1, boolean c1){
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Jun 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Create at least one more separate test where we check if the return type has the permission required after the if conditions.
For the previous example check if the return is still @Unique for example (might need changes):

public @Unique Object test(@Free Object v1, boolean c1){
  Object n;
   n = new Object(); // n is free
  this.value = n; // should be fine
  if (c1){
      this.value = v1; // should be fine
  }
  return this.value; // is this.value still Unique?
}

This way we can check if the information in the context is the expected one.

if (c1) {
this.value = v1;
}
return this.value;
}
}
20 changes: 20 additions & 0 deletions latte/src/test/examples/MyNodeIfPermissionCheck.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
package latte;

import specification.Free;
import specification.Unique;

class MyNodeIfNoElse {

@Unique Object value;

public @Unique Object test(@Free Object v1, boolean cond) {
Object n;
n = new Object();

this.value = n;
if (cond) {
this.value = v1;
}
return this.value; // should still be @Unique
}
}
23 changes: 23 additions & 0 deletions latte/src/test/examples/MyNodeIncorrectIfPermission.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
package latte;

import specification.Free;
import specification.Unique;
import specification.Shared;
import specification.Borrowed;

class MyNodeIfNoElse {

@Unique Object value;

public @Unique Object test(@Shared Object v1, boolean cond) {
Object n;
n = new Object();

this.value = n;
if (cond) {
this.value = v1;
}

return this.value;
}
}
6 changes: 5 additions & 1 deletion latte/src/test/java/AppTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ private static Stream<Arguments> provideCorrectTestCases() {
Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java"),
Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java"),
Arguments.of("src/test/examples/stack_overflow/MediaRecord.java"),
Arguments.of("src/test/examples/MyNodeAllKindsIfs.java"),
Arguments.of("src/test/examples/MyNodeIfNoElse.java"),
Arguments.of("src/test/examples/MyNodeIfPermissionCheck.java"),
Arguments.of("src/test/examples/MyNodeInvocationIf.java"),
Arguments.of("src/test/examples/MyNodeIfInvocationPermission.java")
);
Expand All @@ -62,7 +65,8 @@ private static Stream<Arguments> provideIncorrectTestCases() {
Arguments.of("src/test/examples/SmallestIncorrectExample.java", "UNIQUE but got BORROWED"),
Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", "UNIQUE but got SHARED"),
Arguments.of("src/test/examples/FieldAccessNoThis.java", "UNIQUE but got SHARED"),
Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE")
Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE"),
Arguments.of("src/test/examples/MyNodeIncorrectIfPermission.java", "Expected UNIQUE but got SHARED")
);
}

Expand Down
Loading