From 0cafd4225689f2a67c3ab4996af9c26f5e336e8b Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Wed, 12 Mar 2025 18:22:30 +0100
Subject: [PATCH] Remove strict scope check vor assign substitutions: it broke
double function assignments
see test
---
.../de/tlc4b/analysis/MachineContext.java | 40 ++++---------------
.../java/de/tlc4b/analysis/ScopeTest.java | 14 ++++++-
2 files changed, 20 insertions(+), 34 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index ae6f85e..da4e0eb 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -48,7 +48,7 @@ public class MachineContext extends DepthFirstAdapter {
private AOperationsMachineClause operationMachineClause;
private AAssertionsMachineClause assertionsMachineClause;
- private ArrayList<LinkedHashMap<String, Node>> contextTable;
+ private List<Map<String, Node>> contextTable;
protected final Hashtable<Node, Node> referencesTable;
@@ -311,7 +311,7 @@ public class MachineContext extends DepthFirstAdapter {
pExpression.apply(this);
}
for (int i = contextTable.size() - 1; i >= 0; i--) {
- LinkedHashMap<String, Node> currentScope = contextTable.get(i);
+ Map<String, Node> currentScope = contextTable.get(i);
if (currentScope.containsKey(name)) {
this.referencesTable.put(node, currentScope.get(name));
return;
@@ -397,7 +397,7 @@ public class MachineContext extends DepthFirstAdapter {
private void putLocalVariableIntoCurrentScope(AIdentifierExpression node) throws ScopeException {
String name = Utils.getTIdentifierListAsString(node.getIdentifier());
- LinkedHashMap<String, Node> currentScope = contextTable.get(contextTable.size() - 1);
+ Map<String, Node> currentScope = contextTable.get(contextTable.size() - 1);
if (currentScope.containsKey(name)) {
throw new ScopeException("Duplicate Identifier: " + name);
} else {
@@ -409,7 +409,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAIdentifierExpression(AIdentifierExpression node) {
String name = Utils.getTIdentifierListAsString(node.getIdentifier());
for (int i = contextTable.size() - 1; i >= 0; i--) {
- LinkedHashMap<String, Node> currentScope = contextTable.get(i);
+ Map<String, Node> currentScope = contextTable.get(i);
if (currentScope.containsKey(name)) {
this.referencesTable.put(node, currentScope.get(name));
return;
@@ -422,7 +422,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAPrimedIdentifierExpression(APrimedIdentifierExpression node) {
String name = Utils.getTIdentifierListAsString(node.getIdentifier());
for (int i = contextTable.size() - 1; i >= 0; i--) {
- LinkedHashMap<String, Node> currentScope = contextTable.get(i);
+ Map<String, Node> currentScope = contextTable.get(i);
if (currentScope.containsKey(name)) {
this.referencesTable.put(node, currentScope.get(name));
return;
@@ -596,34 +596,8 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAAssignSubstitution(AAssignSubstitution node) {
- ArrayList<LinkedHashMap<String, Node>> temp = contextTable;
- {
- List<PExpression> copy = new ArrayList<>(node.getLhsExpression());
- ArrayList<LinkedHashMap<String, Node>> varTable = new ArrayList<>();
- varTable.add(variables);
- for (PExpression e : copy) {
- if (e instanceof AFunctionExpression) {
- contextTable = varTable;
- ((AFunctionExpression) e).getIdentifier().apply(this);
-
- // full context table
- contextTable = temp;
- for (Node n : ((AFunctionExpression) e).getParameters()) {
- n.apply(this);
- }
- } else {
- contextTable = temp; // TODO outputparameter + variables
- e.apply(this);
- }
- }
- }
- {
- contextTable = temp;
- List<PExpression> copy = new ArrayList<>(node.getRhsExpressions());
- for (PExpression e : copy) {
- e.apply(this);
- }
- }
+ super.caseAAssignSubstitution(node);
+ // TODO: check if only writable variables are written to?
}
@Override
diff --git a/src/test/java/de/tlc4b/analysis/ScopeTest.java b/src/test/java/de/tlc4b/analysis/ScopeTest.java
index 96b5355..ae1900c 100644
--- a/src/test/java/de/tlc4b/analysis/ScopeTest.java
+++ b/src/test/java/de/tlc4b/analysis/ScopeTest.java
@@ -4,6 +4,8 @@ import org.junit.Ignore;
import org.junit.Test;
import static de.tlc4b.util.TestUtil.checkMachine;
+import static de.tlc4b.util.TestUtil.translate;
+
import de.tlc4b.exceptions.ScopeException;
public class ScopeTest {
@@ -151,5 +153,15 @@ public class ScopeTest {
+ "PROPERTIES #(x,x).(1 = 1 & x = x)\n" + "END";
checkMachine(machine);
}
-
+
+ @Test
+ public void testDoubleFunctionAssign() throws Exception {
+ String machine = "MACHINE test\n"
+ + "VARIABLES f\n"
+ + "INVARIANT f : 1..3 +-> (1..3 +-> BOOL)\n"
+ + "INITIALISATION f := {}\n"
+ + "OPERATIONS put(x, y, value) = SELECT x : 1..3 & y : 1..3 & value : BOOL THEN f(x)(y) := value END\n"
+ + "END";
+ translate(machine);
+ }
}
--
GitLab