From 5352ab6c6ce55c4914a0cd24e02a34b9ca2fb0b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Tue, 13 May 2025 23:51:52 +0100 Subject: [PATCH 1/5] If e1 Then s1 'Else skip' adaptation --- .../java/typechecking/LatteTypeChecker.java | 20 ++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 63d07c6..4d6f702 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -532,11 +532,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); } From 7ac32ca1422c28d311dad046bd5feffa19919fc3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Tue, 20 May 2025 18:20:22 +0100 Subject: [PATCH 2/5] Added if related tests --- .../src/test/examples/MyNodeAllKindsIfs.java | 42 +++++++++++++++++++ latte/src/test/examples/MyNodeIfNoElse.java | 29 +++++++++++++ latte/src/test/java/AppTest.java | 4 +- 3 files changed, 74 insertions(+), 1 deletion(-) create mode 100644 latte/src/test/examples/MyNodeAllKindsIfs.java create mode 100644 latte/src/test/examples/MyNodeIfNoElse.java diff --git a/latte/src/test/examples/MyNodeAllKindsIfs.java b/latte/src/test/examples/MyNodeAllKindsIfs.java new file mode 100644 index 0000000..15ffb0a --- /dev/null +++ b/latte/src/test/examples/MyNodeAllKindsIfs.java @@ -0,0 +1,42 @@ +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 void 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 = v1; + } else { + this.value = v2; + } + if (c1 && c2) { + this.value = v2; + } + } +} diff --git a/latte/src/test/examples/MyNodeIfNoElse.java b/latte/src/test/examples/MyNodeIfNoElse.java new file mode 100644 index 0000000..9aa847c --- /dev/null +++ b/latte/src/test/examples/MyNodeIfNoElse.java @@ -0,0 +1,29 @@ +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 void test(@Free Object v1, boolean c1){ + if (c1) { + this.value = v1; + } + } +} diff --git a/latte/src/test/java/AppTest.java b/latte/src/test/java/AppTest.java index 8bd0f59..a9629b3 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -40,7 +40,9 @@ private static Stream provideCorrectTestCases() { Arguments.of("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java"), 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/stack_overflow/MediaRecord.java"), + Arguments.of("src/test/examples/MyNodeAllKindsIfs.java"), + Arguments.of("src/test/examples/MyNodeIfNoElse.java") ); } From ce646de4fcfad21c91fef50acc7a45f8edae259d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Wed, 11 Jun 2025 17:10:00 +0100 Subject: [PATCH 3/5] Added support for function invocation in If condition --- latte/src/main/java/typechecking/LatteTypeChecker.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 4d6f702..586667c 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -522,6 +522,8 @@ public void visitCtIf(CtIf ifElement) { visitCtVariableRead((CtVariableRead)condition); } else if (condition instanceof CtFieldRead){ visitCtFieldRead((CtFieldRead)condition); + } else if (condition instanceof CtInvocation) { + visitCtInvocation((CtInvocation) condition); } else { logError("Cannot evaluate the condition of the if statement: " + condition.toString(), condition); } From caf3f26ac3966f61b710b6e22f1ad249dbe78291 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Wed, 11 Jun 2025 17:54:16 +0100 Subject: [PATCH 4/5] Added a check for invication return type (must be boolean) --- latte/src/main/java/typechecking/LatteTypeChecker.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 586667c..d7497d8 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -523,7 +523,11 @@ public void visitCtIf(CtIf ifElement) { } else if (condition instanceof CtFieldRead){ visitCtFieldRead((CtFieldRead)condition); } else if (condition instanceof CtInvocation) { - visitCtInvocation((CtInvocation) condition); + CtInvocation invocation = (CtInvocation) condition; + if (!invocation.getType().getQualifiedName().equals("boolean")) { + logError("Method invoked in if condition must return boolean", condition); + } + visitCtInvocation(invocation); } else { logError("Cannot evaluate the condition of the if statement: " + condition.toString(), condition); } From 1b5a118ab726ae437d1318683c9f9b1eab24828d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ant=C3=B3nio=20Almeida?= Date: Wed, 11 Jun 2025 18:05:40 +0100 Subject: [PATCH 5/5] Added related test --- .../src/test/examples/MyNodeInvocationIf.java | 35 +++++++++++++++++++ latte/src/test/java/AppTest.java | 3 +- 2 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 latte/src/test/examples/MyNodeInvocationIf.java diff --git a/latte/src/test/examples/MyNodeInvocationIf.java b/latte/src/test/examples/MyNodeInvocationIf.java new file mode 100644 index 0000000..5f44a1e --- /dev/null +++ b/latte/src/test/examples/MyNodeInvocationIf.java @@ -0,0 +1,35 @@ +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 void test(@Free Object v1, boolean c1){ + if (boolRead(c1)) { + this.value = v1; + } else { + this.value = null; + } + } + + private boolean boolRead(boolean b){ + return b; + } +} diff --git a/latte/src/test/java/AppTest.java b/latte/src/test/java/AppTest.java index a9629b3..6b67cd4 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -42,7 +42,8 @@ private static Stream provideCorrectTestCases() { 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/MyNodeIfNoElse.java"), + Arguments.of("src/test/examples/MyNodeInvocationIf.java") ); }