Linting Framework

pom.xml

@@ -72,6 +72,24 @@
         </pluginManagement>
 
         <plugins>
+            <plugin>
+                <groupId>org.codehaus.mojo</groupId>
+                <artifactId>jaxb2-maven-plugin</artifactId>
+                <version>2.3</version>
+                <executions>
+                    <execution>
+                        <id>xjc</id>
+                        <goals>
+                            <goal>xjc</goal>
+                        </goals>
+                    </execution>
+                </executions>
+                <configuration>
+                    <!-- The package of your generated sources -->
+                    <packageName>edu.kit.formal.proofscriptparser.lint</packageName>
+                </configuration>
+            </plugin>
+
             <plugin>
                 <groupId>org.codehaus.mojo</groupId>
                 <artifactId>license-maven-plugin</artifactId>

src/main/java/edu/kit/formal/interpreter/GoalNode.java

 package edu.kit.formal.interpreter;
 
+import de.uka.ilkd.key.api.ProjectedNode;
 import edu.kit.formal.proofscriptparser.ast.Type;
 import lombok.Getter;
 

src/main/java/edu/kit/formal/interpreter/Interpreter.java

@@ -108,28 +108,11 @@ public class Interpreter extends DefaultASTVisitor<Void>
     }
 
 
-    public VariableAssignment evaluateWithAssignments(GoalNode g, Expression expr) {
-        enterScope(expr);
-        Evaluator evaluator = new Evaluator(g.getAssignments(), g);
-        evaluator.setMatcher(matcherApi);
-        evaluator.getEntryListeners().addAll(entryListeners);
-        evaluator.getExitListeners().addAll(exitListeners);
-        exitScope(expr);
-        Value value = evaluator.eval(expr);
-        if (value.equals(Value.TRUE)) {
-            if (evaluator.getMatchedVariables().size() == 0)
-                return new VariableAssignment();
-            else
-                return evaluator.getMatchedVariables().get(0);
-        }
-        return null;
-    }
-
-    public Value evaluate(Expression expr) {
+    private Value evaluate(Expression expr) {
         return evaluate(getSelectedNode(), expr);
     }
 
-    public Value evaluate(GoalNode g, Expression expr) {
+    private Value evaluate(GoalNode g, Expression expr) {
         enterScope(expr);
         Evaluator evaluator = new Evaluator(g.getAssignments(), g);
         evaluator.setMatcher(matcherApi);
@@ -157,6 +140,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
     }
 
     /**
+     *
      * @param casesStatement
      * @return
      */
@@ -237,6 +221,78 @@ public class Interpreter extends DefaultASTVisitor<Void>
         return null;
     }
 
+    /**
+     * Match a set of goal nodes against a matchpattern of a case and return the metched goals together with instantiated variables
+     *
+     * @param allGoalsBeforeCases
+     * @param aCase
+     * @return
+     */
+    private Map<GoalNode, VariableAssignment> matchGoal(Set<GoalNode> allGoalsBeforeCases, CaseStatement aCase) {
+
+        HashMap<GoalNode, VariableAssignment> matchedGoals = new HashMap<>();
+        Expression matchExpression = aCase.getGuard();
+
+        for (GoalNode goal : allGoalsBeforeCases) {
+            VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
+            if (va != null) {
+                matchedGoals.put(goal, va);
+            }
+
+        }
+        return matchedGoals;
+    }
+
+    /**
+     * Evaluate a match in a specific goal
+     *
+     * @param matchExpression
+     * @param goal
+     * @return
+     */
+    private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode goal) {
+        enterScope(matchExpression);
+        Evaluator eval = new Evaluator(goal.getAssignments(), goal);
+        eval.setMatcher(matcherApi);
+        eval.getEntryListeners().addAll(entryListeners);
+        eval.getExitListeners().addAll(exitListeners);
+        exitScope(matchExpression);
+        Value v = eval.eval(matchExpression);
+        if (v.getData().equals(Value.TRUE)) {
+            if (eval.getMatchedVariables().size() == 0) {
+                return new VariableAssignment();
+            } else {
+                return eval.getMatchedVariables().get(0);
+            }
+        }
+        return null;
+    }
+
+    /**
+     * For each selected goal put a state onto the stack and visit the body of the case
+     *
+     * @param
+     * @param caseStmts
+     * @param goalsToApply @return
+     */
+    private List<GoalNode> executeCase(Statements caseStmts, Set<GoalNode> goalsToApply) {
+        enterScope(caseStmts);
+        List<GoalNode> goalsAfterCases = new ArrayList<>();
+
+        for (GoalNode next : goalsToApply) {
+            List<GoalNode> goalList = new ArrayList<>();
+            goalList.add(next);
+            State s = new State(goalList, next);
+            stateStack.push(s);
+            caseStmts.accept(this);
+            State aftercase = (State) stateStack.pop();
+            goalsAfterCases.addAll(aftercase.getGoals());
+        }
+        exitScope(caseStmts);
+        return goalsAfterCases;
+
+
+    }
 
     /**
      * @param caseStatement

src/main/java/edu/kit/formal/interpreter/VariableAssignment.java

@@ -185,4 +185,11 @@ public class VariableAssignment {
 
         return this.joinWithoutCheck(assignment);
     }
+
+    public VariableAssignment push(VariableAssignment va) {
+        VariableAssignment nva = push();
+        nva.types.putAll(va.types);
+        nva.values.putAll(va.values);
+        return nva;
+    }
 }

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

@@ -62,7 +62,6 @@ public interface ASTTraversal<T> extends Visitor<T> {
 
     @Override
     default T visit(TermLiteral term) {
-        term.accept(this);
         return null;
     }
 

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

@@ -23,7 +23,6 @@ package edu.kit.formal.proofscriptparser.ast;
  */
 
 
-
 import edu.kit.formal.proofscriptparser.Visitable;
 import edu.kit.formal.proofscriptparser.Visitor;
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -46,7 +45,13 @@ public abstract class ASTNode<T extends ParserRuleContext>
         ruleContext = c;
     }
 
+    public T getRuleCtx() {
+        return ruleContext;
+    }
+
     public Optional<T> getRuleContext() {
+        if (ruleContext == null)
+            return Optional.empty();
         return Optional.of(ruleContext);
     }
 

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

+package edu.kit.formal.proofscriptparser.lint;
+
+import edu.kit.formal.proofscriptparser.lint.checkers.IssuesId;
+
+import javax.xml.bind.JAXBContext;
+import javax.xml.bind.JAXBElement;
+import javax.xml.bind.JAXBException;
+import javax.xml.bind.Unmarshaller;
+import java.io.InputStream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (23.05.17)
+ */
+public class IssuesRepository {
+    private static Issues ISSUES;
+
+    public static Issues get() {
+        if (ISSUES == null) {
+            load();
+        }
+        return ISSUES;
+    }
+
+
+    public static Issue getIssue(IssuesId id) {
+        return get().getIssue()
+                .stream()
+                .filter(i -> id.toString().equalsIgnoreCase(i.getRulename()))
+                .findFirst().orElse(new Issue());
+
+    }
+
+    private static void load() {
+        try {
+            Unmarshaller unmarshaller =
+                    JAXBContext.newInstance(ObjectFactory.class).createUnmarshaller();
+            //unmarshaller.setSchema(schema);
+            InputStream issuesFile = LinterStrategy.class
+                    .getResourceAsStream("lint-issues-en.xml");
+            if (issuesFile != null) {
+                JAXBElement<Issues> e = (JAXBElement<Issues>) unmarshaller.unmarshal(issuesFile);
+                ISSUES = e.getValue();
+            } else
+                ISSUES = new Issues();
+        } catch (JAXBException e) {
+            e.printStackTrace();
+        }
+    }
+}

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

 package edu.kit.formal.proofscriptparser.lint;
 
 import edu.kit.formal.proofscriptparser.ast.ASTNode;
-import edu.kit.formal.proofscriptparser.ast.GoalSelector;
-import edu.kit.formal.proofscriptparser.ast.Statement;
-import lombok.*;
+import lombok.Data;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+import org.antlr.v4.runtime.ParserRuleContext;
+import org.antlr.v4.runtime.Token;
 
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -14,46 +16,47 @@ import java.util.List;
  * @version 1 (23.05.17)
  */
 @Data
-@NoArgsConstructor
-@AllArgsConstructor
+@RequiredArgsConstructor
 public class LintProblem {
     @Getter
-    @Setter(AccessLevel.MODULE)
-    private String message;
+    private final Issue issue;
 
     @Getter
-    @Setter(AccessLevel.MODULE)
-    private char level;
+    private List<Token> markTokens = new ArrayList<>();
 
-    @Getter
-    @Setter(AccessLevel.MODULE)
-    private int number;
-
-    @Getter
-    @Setter(AccessLevel.MODULE)
-    private String lintRule;
+    public Token getFirstToken() {
+        if (markTokens.size() == 0)
+            return null;
+        return markTokens.get(0);
+    }
 
-    @Getter
-    private List<ASTNode> affectedNodes = new ArrayList<>();
+    public int getLineNumber() {
+        if (getFirstToken() == null)
+            return -1;
+        return getFirstToken().getLine();
+    }
 
-    public static LintProblem create(String ruleName) {
-        LintProblem lp = new LintProblem();
-        lp.setLintRule(ruleName);
+    public static LintProblem create(Issue issue, Token... markTokens) {
+        LintProblem lp = new LintProblem(issue);
+        lp.getMarkTokens().addAll(Arrays.asList(markTokens));
         return lp;
     }
 
-    public LintProblem level(char w) {
-        setLevel(w);
-        return this;
+    public String getMessage() {
+        return String.format(getIssue().getValue(), markTokens.toArray());
     }
 
-    public LintProblem message(String s) {
-        setMessage(s);
-        return this;
+    public static <T extends ParserRuleContext>
+    LintProblem create(Issue issue, ASTNode<T>... nodes) {
+        return new LintProblem(issue).nodes(nodes);
     }
 
-    public LintProblem nodes(ASTNode... nodes) {
-        getAffectedNodes().addAll(Arrays.asList(nodes));
+    public <T extends ParserRuleContext> LintProblem nodes(ASTNode<T>... nodes) {
+        for (ASTNode n : nodes) {
+            ParserRuleContext ctx = n.getRuleCtx();
+            if (ctx != null)
+                markTokens.add(ctx.getStart());
+        }
         return this;
     }
 }

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

@@ -18,7 +18,11 @@ public class Linter {
         LinterStrategy ls = LinterStrategy.getDefaultLinter();
         List<LintProblem> problems = ls.check(scripts);
         for (LintProblem lp : problems) {
-            System.out.printf("%s-%04d: %s", lp.getLevel(), lp.getNumber(), lp.getMessage());
+            System.out.printf("@%s > (%s-%04d) : %s",
+                    lp.getLineNumber(),
+                    lp.getIssue().getSeverity(),
+                    lp.getIssue().getId(),
+                    lp.getMessage());
         }
     }
 

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

@@ -3,6 +3,11 @@ package edu.kit.formal.proofscriptparser.lint;
 import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import lombok.Getter;
 
+import javax.xml.bind.JAXBContext;
+import javax.xml.bind.JAXBElement;
+import javax.xml.bind.JAXBException;
+import javax.xml.bind.Unmarshaller;
+import java.io.InputStream;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.ServiceLoader;

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

 package edu.kit.formal.proofscriptparser.lint.checkers;
 
 import edu.kit.formal.proofscriptparser.ast.ASTNode;
-import edu.kit.formal.proofscriptparser.ast.ProofScript;
-import edu.kit.formal.proofscriptparser.lint.LintProblem;
-import edu.kit.formal.proofscriptparser.lint.LintRule;
+import edu.kit.formal.proofscriptparser.lint.*;
 
 import java.util.List;
 
@@ -31,4 +29,5 @@ public abstract class AbstractLintRule implements LintRule {
     public String getName() {
         return getClass().getSimpleName();
     }
+
 }

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

 package edu.kit.formal.proofscriptparser.lint.checkers;
 
-import edu.kit.formal.proofscriptparser.ast.Statements;
-import edu.kit.formal.proofscriptparser.lint.LintProblem;
+import edu.kit.formal.proofscriptparser.ast.*;
+import edu.kit.formal.proofscriptparser.lint.Issue;
+import edu.kit.formal.proofscriptparser.lint.IssuesRepository;
 
 /**
  * @author Alexander Weigl
  * @version 1 (23.05.17)
  */
 public class EmptyBlocks extends AbstractLintRule {
+    private static Issue EMPTY_BLOCK = IssuesRepository.getIssue(IssuesId.EMPTY_BLOCKS);
+
     public EmptyBlocks() {
         super(EmptyBlockSearcher::new);
     }
 
     private static class EmptyBlockSearcher extends Searcher {
-        @Override
-        public Void visit(Statements statements) {
+
+        public void check(ASTNode node, Statements statements) {
             if (statements.size() == 0) {
-                problems.add(LintProblem.create("")
-                        .level('I')
-                        .message("Empty Block ")
-                        .nodes(statements)
-                );
+                problem(EMPTY_BLOCK, node);
             }
-            return super.visit(statements);
+        }
+
+        @Override
+        public Void visit(ProofScript proofScript) {
+            check(proofScript, proofScript.getBody());
+            return super.visit(proofScript);
+        }
+
+        @Override
+        public Void visit(CaseStatement caseStatement) {
+            check(caseStatement, caseStatement.getBody());
+            return super.visit(caseStatement);
+        }
+
+        @Override
+        public Void visit(TheOnlyStatement theOnly) {
+            check(theOnly, theOnly.getBody());
+            return super.visit(theOnly);
+        }
+
+        @Override
+        public Void visit(ForeachStatement foreach) {
+            check(foreach, foreach.getBody());
+            return super.visit(foreach);
+        }
+
+        @Override
+        public Void visit(RepeatStatement repeatStatement) {
+            check(repeatStatement, repeatStatement.getBody());
+            return super.visit(repeatStatement);
         }
     }
 }

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

+package edu.kit.formal.proofscriptparser.lint.checkers;
+
+import edu.kit.formal.proofscriptparser.ast.ASTNode;
+import edu.kit.formal.proofscriptparser.ast.ProofScript;
+import edu.kit.formal.proofscriptparser.lint.Issue;
+import edu.kit.formal.proofscriptparser.lint.IssuesRepository;
+import edu.kit.formal.proofscriptparser.lint.LintProblem;
+import edu.kit.formal.proofscriptparser.lint.LintRule;
+import org.antlr.v4.runtime.Token;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (23.05.17)
+ */
+public class EqualScriptNames implements LintRule {
+    private Issue ISSUE = IssuesRepository.getIssue(IssuesId.EQUAL_SCRIPT_NAMES);
+
+    @Override
+    public void check(List<? extends ASTNode> node, List<LintProblem> problems) {
+        Map<String, Token> scripts = new HashMap<>();
+        for (ASTNode s : node) {
+            if (s instanceof ProofScript) {
+                ProofScript proofScript = (ProofScript) s;
+                if (scripts.containsKey(proofScript.getName())) {
+                    problems.add(LintProblem.create(ISSUE,
+                            scripts.get(proofScript.getName()),
+                            proofScript.getRuleContext().get().name));
+                }
+                scripts.put(proofScript.getName(),
+                        proofScript.getRuleContext().get().name);
+            }
+        }
+    }
+
+    @Override
+    public String getName() {
+        return ISSUE.getRulename();
+    }
+}

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

+package edu.kit.formal.proofscriptparser.lint.checkers;
+
+/**
+ * Should correspond to <code>issues-list-en.xml</code>
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.05.17)
+ */
+public enum IssuesId {
+    EMPTY_BLOCKS, EQUAL_SCRIPT_NAMES, NEGATED_MATCH_WITH_USING, SUCC_SAME_BLOCK,
+    FOREACH_AFTER_THEONLY, THEONLY_AFTER_FOREACH
+}

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

@@ -2,13 +2,17 @@ package edu.kit.formal.proofscriptparser.lint.checkers;
 
 import edu.kit.formal.proofscriptparser.ast.MatchExpression;
 import edu.kit.formal.proofscriptparser.ast.UnaryExpression;
+import edu.kit.formal.proofscriptparser.lint.Issue;
+import edu.kit.formal.proofscriptparser.lint.IssuesRepository;
 
 /**
  * @author Alexander Weigl
  * @version 1 (23.05.17)
  */
 public class NegatedMatchWithUsing extends AbstractLintRule {
-    protected NegatedMatchWithUsing(SearcherFactory factory) {
+    private static Issue ISSUE = IssuesRepository.getIssue(IssuesId.NEGATED_MATCH_WITH_USING);
+
+    public NegatedMatchWithUsing() {
         super(NMWUSearcher::new);
     }
 
@@ -18,7 +22,7 @@ public class NegatedMatchWithUsing extends AbstractLintRule {
             if (ue.getExpression() instanceof MatchExpression) {
                 MatchExpression me = (MatchExpression) ue.getExpression();
                 if (me.getSignature() != null && me.getSignature().size() > 0) {
-                    problem("NMWU").message("negated match with using ").nodes(ue, me);
+                    problem(ISSUE, ue, me);
                 }
             }
             return super.visit(ue);

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

@@ -2,6 +2,10 @@ package edu.kit.formal.proofscriptparser.lint.checkers;
 
 import edu.kit.formal.proofscriptparser.ASTTraversal;
 import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
+import edu.kit.formal.proofscriptparser.ast.ASTNode;
+import edu.kit.formal.proofscriptparser.ast.MatchExpression;
+import edu.kit.formal.proofscriptparser.ast.UnaryExpression;
+import edu.kit.formal.proofscriptparser.lint.Issue;
 import edu.kit.formal.proofscriptparser.lint.LintProblem;
 import lombok.Getter;
 
@@ -16,9 +20,13 @@ public abstract class Searcher implements ASTTraversal<Void> {
     @Getter
     protected final List<LintProblem> problems = new ArrayList<>(10);
 
-    LintProblem problem(String rulename) {
-        LintProblem lp = LintProblem.create(rulename);
+    LintProblem problem(Issue issue) {
+        LintProblem lp = new LintProblem(issue);
         problems.add(lp);
         return lp;
     }
+
+    LintProblem problem(Issue issue, ASTNode... nodes) {
+        return problem(issue).nodes(nodes);
+    }
 }

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

@@ -4,7 +4,8 @@ import edu.kit.formal.proofscriptparser.ast.ForeachStatement;
 import edu.kit.formal.proofscriptparser.ast.GoalSelector;
 import edu.kit.formal.proofscriptparser.ast.RepeatStatement;
 import edu.kit.formal.proofscriptparser.ast.TheOnlyStatement;
-import edu.kit.formal.proofscriptparser.lint.LintProblem;
+import edu.kit.formal.proofscriptparser.lint.Issue;
+import edu.kit.formal.proofscriptparser.lint.IssuesRepository;
 
 import java.util.Objects;
 
@@ -13,26 +14,28 @@ import java.util.Objects;
  * @version 1 (23.05.17)
  */
 public class SuccessiveGoalSelector extends AbstractLintRule {
+    private static Issue SUCC_SAME_BLOCK =
+            IssuesRepository.getIssue(IssuesId.SUCC_SAME_BLOCK);
+    private static final Issue FOREACH_AFTER_THEONLY =
+            IssuesRepository.getIssue(IssuesId.FOREACH_AFTER_THEONLY);
+    private static final Issue THEONLY_AFTER_FOREACH =
+            IssuesRepository.getIssue(IssuesId.THEONLY_AFTER_FOREACH);
 
     public SuccessiveGoalSelector() {
         super(SGSearcher::new);
     }
 
     static class SGSearcher extends Searcher {
+
         @Override
         public Void visit(TheOnlyStatement theOnly) {
             if (check(theOnly, theOnly.getNodeName())) {
-                problems.add(LintProblem.create("")
-                        .level('W')
-                        .message("succ. same goal selector")
-                        .nodes(theOnly, theOnly.getBody().get(0)));
+                problem(SUCC_SAME_BLOCK,
+                        theOnly, theOnly.getBody().get(0));
             }
 
             if (check(theOnly, "ForeachStatement")) {
-                problems.add(LintProblem.create("")
-                        .level('W')
-                        .message("foreach following theonly has no effect")
-                        .nodes(theOnly, theOnly.getBody().get(0)));
+                problem(FOREACH_AFTER_THEONLY, theOnly, theOnly.getBody().get(0));
             }
 
             return super.visit(theOnly);
@@ -45,30 +48,24 @@ public class SuccessiveGoalSelector extends AbstractLintRule {
         @Override
         public Void visit(ForeachStatement foreach) {
             if (check(foreach, foreach.getNodeName())) {
-                problems.add(LintProblem.create("")
-                        .level('W')
-                        .message("succ. same goal selector")
-                        .nodes(foreach, foreach.getBody().get(0)));
+                problem(SUCC_SAME_BLOCK,
+                        foreach, foreach.getBody().get(0));
             }
 
             if (check(foreach, "TheOnlyStatement")) {
-                problems.add(LintProblem.create("")
-                        .level('W')
-                        .message("theonly following foreach has no effect")
-                        .nodes(foreach, foreach.getBody().get(0)));
+                problem(THEONLY_AFTER_FOREACH,
+                        foreach, foreach.getBody().get(0));
             }
             return super.visit(foreach);
         }
 
         @Override
-        public Void visit(RepeatStatement repeatStatement) {
-            if (check(repeatStatement, repeatStatement.getNodeName())) {
-                problems.add(LintProblem.create("")
-                        .level('W')
-                        .message("succ. same goal selector")
-                        .nodes(repeatStatement, repeatStatement.getBody().get(0)));
+        public Void visit(RepeatStatement repeat) {
+            if (check(repeat, repeat.getNodeName())) {
+                problem(SUCC_SAME_BLOCK,
+                        repeat, repeat.getBody().get(0));
             }
-            return super.visit(repeatStatement);