Variable Linting

src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java

@@ -36,6 +36,7 @@ import java.util.Map;
 public interface ASTTraversal<T> extends Visitor<T> {
     @Override
     default T visit(ProofScript proofScript) {
+        proofScript.getSignature().accept(this);
         proofScript.getBody().accept(this);
         return null;
     }

src/main/java/edu/kit/formal/proofscriptparser/ast/Literal.java

@@ -24,6 +24,8 @@ package edu.kit.formal.proofscriptparser.ast;
 
 
 
+import lombok.Getter;
+import lombok.Setter;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.Token;
 
@@ -34,17 +36,10 @@ import java.util.Optional;
  * @version 1 (28.04.17)
  */
 public abstract class Literal extends Expression<ParserRuleContext> {
+    @Getter
+    @Setter
     protected Token token;
 
-    public Optional<Token> getToken() {
-        return Optional.of(token);
-    }
-
-    public Literal setToken(Token token) {
-        this.token = token;
-        return this;
-    }
-
     /**
      * {@inheritDoc}
      */

src/main/java/edu/kit/formal/proofscriptparser/lint/LintProblem.java

@@ -38,8 +38,7 @@ public class LintProblem {
 
     public static LintProblem create(Issue issue, Token... markTokens) {
         LintProblem lp = new LintProblem(issue);
-        lp.getMarkTokens().addAll(Arrays.asList(markTokens));
-        return lp;
+        return lp.tokens(markTokens);
     }
 
     public String getMessage() {
@@ -59,4 +58,9 @@ public class LintProblem {
         }
         return this;
     }
+
+    public LintProblem tokens(Token... toks) {
+        getMarkTokens().addAll(Arrays.asList(toks));
+        return this;
+    }
 }

src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/IssuesId.java

@@ -8,5 +8,8 @@ package edu.kit.formal.proofscriptparser.lint.checkers;
  */
 public enum IssuesId {
     EMPTY_BLOCKS, EQUAL_SCRIPT_NAMES, NEGATED_MATCH_WITH_USING, SUCC_SAME_BLOCK,
-    FOREACH_AFTER_THEONLY, THEONLY_AFTER_FOREACH
+    FOREACH_AFTER_THEONLY,
+    REDECLARE_VARIABLE, REDECLARE_VARIABLE_TYPE_MISMATCH,
+    VARIABLE_NOT_DECLARED,
+    VARIABLE_NOT_USED, THEONLY_AFTER_FOREACH
 }

src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/VariableDeclarationCheck.java

+package edu.kit.formal.proofscriptparser.lint.checkers;
+
+import edu.kit.formal.interpreter.VariableAssignment;
+import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.lint.Issue;
+import edu.kit.formal.proofscriptparser.lint.IssuesRepository;
+import org.antlr.v4.runtime.Token;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (23.05.17)
+ */
+public class VariableDeclarationCheck extends AbstractLintRule {
+    private static final Issue REDECLARE_VARIABLE = IssuesRepository.getIssue(IssuesId.REDECLARE_VARIABLE);
+    private static final Issue REDECLARE_VARIABLE_TYPE_MISMATCH = IssuesRepository.getIssue(IssuesId.REDECLARE_VARIABLE_TYPE_MISMATCH);
+    private static final Issue VARIABLE_NOT_DECLARED = IssuesRepository.getIssue(IssuesId.VARIABLE_NOT_DECLARED);
+    private static final Issue VARIABLE_NOT_USED = IssuesRepository.getIssue(IssuesId.VARIABLE_NOT_USED);
+
+
+    public VariableDeclarationCheck() {
+        super(UVSearcher::new);
+    }
+
+    static class UVSearcher extends Searcher {
+        private VariableAssignment current = new VariableAssignment(null);
+        private Map<String, Token> hits = new HashMap<>();
+
+
+        @Override
+        public Void visit(ProofScript proofScript) {
+            current = current.push();
+            super.visit(proofScript);
+            current = current.pop();
+            current.asMap().forEach((s, t) -> {
+                if (hits.get(s) != null) {
+                    problem(VARIABLE_NOT_USED);
+                }
+            });
+
+            return null;
+        }
+
+        @Override
+        public Void visit(TheOnlyStatement foreach) {
+            current = current.push();
+            super.visit(foreach);
+            current = current.pop();
+            return null;
+        }
+
+        @Override
+        public Void visit(CaseStatement caseStatement) {
+            current = current.push();
+            super.visit(caseStatement);
+            current = current.pop();
+            return null;
+        }
+
+        private void declare(Variable var, Type type) {
+            if (current.lookupType(var.getIdentifier()) != null) {
+                problem(REDECLARE_VARIABLE).tokens(var.getToken());
+
+                if (!current.lookupType(var.getIdentifier()).equals(type)) {
+                    problem(REDECLARE_VARIABLE_TYPE_MISMATCH).tokens(var.getToken());
+                }
+            } else {
+                current.addVarDecl(var.getIdentifier(), type);
+            }
+        }
+
+        private void check(Variable var) {
+            if (!current.getTypes().containsKey(var.getIdentifier())) {
+                problem(VARIABLE_NOT_DECLARED).tokens(var.getToken());
+            }
+            hits.put(var.getIdentifier(), var.getToken());
+        }
+
+        @Override
+        public Void visit(Signature signature) {
+            for (Map.Entry<Variable, Type> v : signature.entrySet()) {
+                declare(v.getKey(), v.getValue());
+            }
+            return null;
+        }
+
+        @Override
+        public Void visit(AssignmentStatement assign) {
+            if (assign.getRhs() != null)
+                assign.getRhs().accept(this);
+
+            if (assign.getType() != null) {
+                declare(assign.getLhs(), assign.getType());
+            } else {
+                check(assign.getLhs());
+            }
+
+            return null;
+        }
+
+
+        @Override
+        public Void visit(Variable v) {
+            check(v);
+            return null;
+        }
+
+        @Override
+        public Void visit(Parameters parameters) {
+            for (Expression e : parameters.values()) {
+                e.accept(this);
+            }
+            return null;
+        }
+
+    }
+}

src/main/resources/META-INF/services/edu.kit.formal.proofscriptparser.lint.LintRule

 edu.kit.formal.proofscriptparser.lint.checkers.EmptyBlocks
 edu.kit.formal.proofscriptparser.lint.checkers.SuccessiveGoalSelector
 edu.kit.formal.proofscriptparser.lint.checkers.NegatedMatchWithUsing
-edu.kit.formal.proofscriptparser.lint.checkers.EqualScriptNames
\ No newline at end of file
+edu.kit.formal.proofscriptparser.lint.checkers.EqualScriptNames
+edu.kit.formal.proofscriptparser.lint.checkers.VariableDeclarationCheck
\ No newline at end of file

src/main/resources/edu/kit/formal/proofscriptparser/lint/lint-issues-en.xml

 <issues version="1.0" xmlns="http://formal.iti.kit.edu/lint-issues-1.0">
     <issue id="0" severity="info" rulename="empty_blocks">
-      Empty blocks are useless!
+        Empty blocks are useless!
     </issue>
     <issue id="1" severity="error" rulename="equal_script_names">
         The identifier of scripts need to be unique.
@@ -15,4 +15,12 @@
     </issue>
     <issue id="4" severity="warn" rulename="FOREACH_AFTER_THEONLY"/>
     <issue id="5" severity="warn" rulename="THEONLY_AFTER_FOREACH"/>
+
+    <issue id="7" severity="warn" rulename="REDECLARE_VARIABLE">
+
+    </issue>
+    <issue id="8" severity="warn" rulename="REDECLARE_VARIABLE_TYPE_MISMATCH"/>
+    <issue id="9" severity="warn" rulename="VARIABLE_NOT_DECLARED"/>
+    <issue id="10" severity="warn" rulename="VARIABLE_NOT_USED"/>
+
 </issues>
\ No newline at end of file

src/test/java/edu/kit/formal/proofscriptparser/lint/LinterTest.java

@@ -17,17 +17,27 @@ import static org.junit.Assert.assertEquals;
 public class LinterTest {
     @Test
     public void testRegisteredLinter() {
-        assertEquals(4, LinterStrategy.getDefaultLinter().getCheckers().size());
+        assertEquals(5, LinterStrategy.getDefaultLinter().getCheckers().size());
     }
 
     @Test
     public void testLint1() throws IOException {
+        runLint("lint1.kps");
+    }
+
+
+    @Test
+    public void testLint2() throws IOException {
+        runLint("lint2.kps");
+    }
+
+    public void runLint(String filename) throws IOException {
         LinterStrategy ls = LinterStrategy.getDefaultLinter();
-        List<ProofScript> nodes = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream("lint1.kps")));
+        List<ProofScript> nodes = Facade.getAST(CharStreams.fromStream(getClass().getResourceAsStream(filename)));
         List<LintProblem> problems = ls.check(nodes);
 
         for (LintProblem lp : problems) {
-            System.out.printf("@%s > (%s-%04d|%s) : %s%n",
+            System.out.printf("@%03d > (%s-%04d|%s) : %s%n",
                     lp.getLineNumber(),
                     lp.getIssue().getSeverity(),
                     lp.getIssue().getId(),

src/test/resources/edu/kit/formal/proofscriptparser/lint/lint2.kps

+script A (i:int, j:int, a:bool) {
+   k: int := i + j;
+   foreach {
+        j : int := 5*k+i;
+        j : int := j;
+   }
+
+    cases  {
+        case true {
+            c : bool;
+        }
+
+        case false  {
+            d : bool;
+        }
+
+        case match `f(x)` using [d:int, a:bool, Y:bool] {
+
+        }
+    }
+
+    a := a & d;
+
+}