Skip to content

Commit ad4f316

Browse files
S3vroS3vro
authored
Feat/semantics java vars (#172)
* feat: added semantic checking for JavaVariables * fix: checkstyle
1 parent 405cf42 commit ad4f316

4 files changed

Lines changed: 241 additions & 2 deletions

File tree

‎backend/src/main/java/edu/kit/cbc/common/corc/parsing/SemanticChecker.java‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
package edu.kit.cbc.common.corc.parsing;
2+
3+
4+
import edu.kit.cbc.common.corc.cbcmodel.CbCFormula;
5+
import edu.kit.cbc.common.corc.cbcmodel.Condition;
6+
import edu.kit.cbc.common.corc.cbcmodel.statements.AbstractStatement;
7+
import edu.kit.cbc.common.corc.cbcmodel.statements.CompositionStatement;
8+
import edu.kit.cbc.common.corc.cbcmodel.statements.SelectionStatement;
9+
import edu.kit.cbc.common.corc.cbcmodel.statements.SmallRepetitionStatement;
10+
import edu.kit.cbc.common.corc.cbcmodel.statements.Statement;
11+
import edu.kit.cbc.common.corc.parsing.condition.ast.ExistsTree;
12+
import edu.kit.cbc.common.corc.parsing.condition.ast.ForAllTree;
13+
import edu.kit.cbc.common.corc.parsing.condition.ast.OldTree;
14+
import edu.kit.cbc.common.corc.parsing.parser.ast.ArrayAcessTree;
15+
import edu.kit.cbc.common.corc.parsing.parser.ast.BinaryOperationTree;
16+
import edu.kit.cbc.common.corc.parsing.parser.ast.CallTree;
17+
import edu.kit.cbc.common.corc.parsing.parser.ast.IdentTree;
18+
import edu.kit.cbc.common.corc.parsing.parser.ast.LengthTree;
19+
import edu.kit.cbc.common.corc.parsing.parser.ast.Tree;
20+
import edu.kit.cbc.common.corc.parsing.parser.ast.UnaryOperationTree;
21+
import edu.kit.cbc.common.corc.parsing.program.ast.AssignTree;
22+
import edu.kit.cbc.common.corc.parsing.program.ast.BlockTree;
23+
import edu.kit.cbc.common.corc.parsing.program.ast.StatementTree;
24+
import java.util.HashSet;
25+
import java.util.Set;
26+
import java.util.stream.Collectors;
27+
28+
public class SemanticChecker {
29+
30+
private static final java.util.List<String> IGNORED_VARIABLES = java.util.List.of("true", "false");
31+
32+
public static void checkVariables(CbCFormula formula) throws SemanticException {
33+
if (formula == null) {
34+
return;
35+
}
36+
37+
Set<String> declaredVariables = new HashSet<>();
38+
if (formula.getJavaVariables() != null) {
39+
declaredVariables = formula.getJavaVariables().stream()
40+
.map(v -> {
41+
String name = v.getName().trim();
42+
String[] parts = name.split("\\s+");
43+
String last = parts[parts.length - 1];
44+
return last.replace("[]", "");
45+
})
46+
.collect(Collectors.toSet());
47+
}
48+
49+
if (formula.getGlobalConditions() != null) {
50+
for (Condition condition : formula.getGlobalConditions()) {
51+
checkCondition(condition, declaredVariables);
52+
}
53+
}
54+
55+
checkStatement(formula.getStatement(), declaredVariables);
56+
}
57+
58+
private static void checkStatement(AbstractStatement statement, Set<String> declaredVariables)
59+
throws SemanticException {
60+
if (statement == null) {
61+
return;
62+
}
63+
64+
checkCondition(statement.getPreCondition(), declaredVariables);
65+
checkCondition(statement.getPostCondition(), declaredVariables);
66+
67+
if (statement instanceof CompositionStatement comp) {
68+
checkCondition(comp.getIntermediateCondition(), declaredVariables);
69+
checkStatement(comp.getFirstStatement(), declaredVariables);
70+
checkStatement(comp.getSecondStatement(), declaredVariables);
71+
} else if (statement instanceof SelectionStatement sel) {
72+
if (sel.getGuards() != null) {
73+
for (Condition guard : sel.getGuards()) {
74+
checkCondition(guard, declaredVariables);
75+
}
76+
}
77+
if (sel.getCommands() != null) {
78+
for (AbstractStatement cmd : sel.getCommands()) {
79+
checkStatement(cmd, declaredVariables);
80+
}
81+
}
82+
} else if (statement instanceof SmallRepetitionStatement rep) {
83+
checkCondition(rep.getInvariant(), declaredVariables);
84+
checkCondition(rep.getVariant(), declaredVariables);
85+
checkCondition(rep.getGuard(), declaredVariables);
86+
checkStatement(rep.getLoopStatement(), declaredVariables);
87+
} else if (statement instanceof Statement stmt) {
88+
checkTree(stmt.getProgramTree(), declaredVariables);
89+
}
90+
}
91+
92+
private static void checkCondition(Condition condition, Set<String> declaredVariables) throws SemanticException {
93+
if (condition == null) {
94+
return;
95+
}
96+
checkTree(condition.getParsedCondition(), declaredVariables);
97+
}
98+
99+
private static void checkTree(Tree node, Set<String> scope) throws SemanticException {
100+
if (node == null) {
101+
return;
102+
}
103+
104+
if (node instanceof ForAllTree forAll) {
105+
Set<String> newScope = new HashSet<>(scope);
106+
if (forAll.variable() != null) {
107+
newScope.add(forAll.variable().name());
108+
}
109+
checkTree(forAll.condition(), newScope);
110+
} else if (node instanceof ExistsTree exists) {
111+
Set<String> newScope = new HashSet<>(scope);
112+
if (exists.variable() != null) {
113+
newScope.add(exists.variable().name());
114+
}
115+
checkTree(exists.condition(), newScope);
116+
} else if (node instanceof IdentTree id) {
117+
String name = id.name();
118+
if (!scope.contains(name) && IGNORED_VARIABLES.stream().noneMatch(name::equalsIgnoreCase)) {
119+
throw new SemanticException("Variable '" + name + "' is used but not defined.");
120+
}
121+
} else if (node instanceof LengthTree len) {
122+
if (!scope.contains(len.variable())) {
123+
throw new SemanticException("Variable '" + len.variable() + "' is used but not defined.");
124+
}
125+
} else if (node instanceof ArrayAcessTree arr) {
126+
checkTree(arr.name(), scope);
127+
checkTree(arr.expr(), scope);
128+
} else if (node instanceof BinaryOperationTree bin) {
129+
checkTree(bin.lhs(), scope);
130+
checkTree(bin.rhs(), scope);
131+
} else if (node instanceof CallTree call) {
132+
checkTree(call.name(), scope);
133+
if (call.params() != null) {
134+
for (Tree param : call.params()) {
135+
checkTree(param, scope);
136+
}
137+
}
138+
} else if (node instanceof UnaryOperationTree un) {
139+
checkTree(un.expr(), scope);
140+
} else if (node instanceof AssignTree assign) {
141+
checkTree(assign.name(), scope);
142+
checkTree(assign.expr(), scope);
143+
} else if (node instanceof BlockTree block) {
144+
if (block.statements() != null) {
145+
for (StatementTree stmt : block.statements()) {
146+
checkTree(stmt, scope);
147+
}
148+
}
149+
} else if (node instanceof OldTree old) {
150+
checkTree(old.variable(), scope);
151+
}
152+
}
153+
}

‎backend/src/main/java/edu/kit/cbc/common/corc/parsing/SemanticException.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package edu.kit.cbc.common.corc.parsing;
2+
3+
public class SemanticException extends Exception {
4+
5+
public SemanticException(String message) {
6+
super(message);
7+
}
8+
}

‎backend/src/main/java/edu/kit/cbc/common/corc/parsing/parser/ast/AstWalker.java‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
package edu.kit.cbc.common.corc.parsing.parser.ast;
2+
3+
import edu.kit.cbc.common.corc.parsing.condition.ast.ExistsTree;
4+
import edu.kit.cbc.common.corc.parsing.condition.ast.ForAllTree;
5+
import edu.kit.cbc.common.corc.parsing.condition.ast.OldTree;
6+
import edu.kit.cbc.common.corc.parsing.program.ast.AssignTree;
7+
import edu.kit.cbc.common.corc.parsing.program.ast.BlockTree;
8+
import edu.kit.cbc.common.corc.parsing.program.ast.StatementTree;
9+
import java.util.function.Consumer;
10+
11+
/**
12+
* A utility class to walk the entire Abstract Syntax Tree (AST).
13+
* It visits a node and then recursively visits its children, applying the
14+
* specified action.
15+
*/
16+
public class AstWalker {
17+
18+
/**
19+
* Walks the given AST node and all its children recursively,
20+
* applying the provided action to each node.
21+
* The traversal is done pre-order (parent is processed before its children).
22+
*
23+
* @param node the root node to start walking from (can be null)
24+
* @param action the arbitrary function to apply to each node
25+
*/
26+
public static void walk(Tree node, Consumer<Tree> action) {
27+
if (node == null) {
28+
return;
29+
}
30+
31+
action.accept(node);
32+
33+
if (node instanceof ArrayAcessTree arr) {
34+
walk(arr.name(), action);
35+
walk(arr.expr(), action);
36+
} else if (node instanceof BinaryOperationTree bin) {
37+
walk(bin.lhs(), action);
38+
walk(bin.rhs(), action);
39+
} else if (node instanceof CallTree call) {
40+
walk(call.name(), action);
41+
if (call.params() != null) {
42+
for (Tree param : call.params()) {
43+
walk(param, action);
44+
}
45+
}
46+
} else if (node instanceof UnaryOperationTree un) {
47+
walk(un.expr(), action);
48+
} else if (node instanceof AssignTree assign) {
49+
walk(assign.name(), action);
50+
walk(assign.expr(), action);
51+
} else if (node instanceof BlockTree block) {
52+
if (block.statements() != null) {
53+
for (StatementTree stmt : block.statements()) {
54+
walk(stmt, action);
55+
}
56+
}
57+
} else if (node instanceof ExistsTree exists) {
58+
walk(exists.variable(), action);
59+
walk(exists.condition(), action);
60+
} else if (node instanceof ForAllTree forAll) {
61+
walk(forAll.variable(), action);
62+
walk(forAll.condition(), action);
63+
} else if (node instanceof OldTree old) {
64+
walk(old.variable(), action);
65+
}
66+
}
67+
}

‎backend/src/main/java/edu/kit/cbc/editor/EditorController.java‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package edu.kit.cbc.editor;
22

3+
34
import edu.kit.cbc.common.Problem;
45
import edu.kit.cbc.common.corc.cbcmodel.CbCFormula;
56
import edu.kit.cbc.common.corc.codegeneration.CodeGenerator;
@@ -20,6 +21,8 @@
2021
import io.micronaut.scheduling.annotation.ExecuteOn;
2122
import jakarta.validation.Valid;
2223
import java.io.IOException;
24+
import java.util.List;
25+
import java.util.Map;
2326
import java.util.Optional;
2427
import java.util.UUID;
2528

@@ -54,12 +57,20 @@ public HttpResponse<String> generate(@Body @Valid CbCFormula formula) {
5457
@Post(uri = "/verify")
5558
@Produces(MediaType.APPLICATION_JSON)
5659
@Consumes(MediaType.APPLICATION_JSON)
57-
public HttpResponse<?> verify(@QueryValue Optional<String> projectId, @Body @Valid CbCFormula formula) throws IOException {
60+
public HttpResponse<?> verify(@QueryValue Optional<String> projectId, @Body @Valid CbCFormula formula)
61+
throws IOException {
62+
try {
63+
edu.kit.cbc.common.corc.parsing.SemanticChecker.checkVariables(formula);
64+
} catch (edu.kit.cbc.common.corc.parsing.SemanticException e) {
65+
66+
return HttpResponse
67+
.badRequest(Map.of("_embedded", Map.of("errors", List.of(Map.of("message", e.getMessage())))));
68+
}
69+
5870
UUID jobId = orchestrator.addJob(projectId, formula, filesController);
5971
return HttpResponse.ok(jobId);
6072
}
6173

62-
6374
@Post(uri = "/javaGen")
6475
@Produces(MediaType.TEXT_PLAIN)
6576
@Consumes(MediaType.APPLICATION_JSON)

0 commit comments

Comments
 (0)