Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
24
Issues
24
List
Boards
Labels
Service Desk
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
e4dcaaf4
Commit
e4dcaaf4
authored
May 24, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Plain Diff
Merge remote-tracking branch 'origin/master'
parents
6a5eb734
4395a508
Changes
9
Hide whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
182 additions
and
17 deletions
+182
-17
src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java
...n/java/edu/kit/formal/proofscriptparser/ASTTraversal.java
+1
-0
src/main/java/edu/kit/formal/proofscriptparser/ast/Literal.java
...in/java/edu/kit/formal/proofscriptparser/ast/Literal.java
+4
-9
src/main/java/edu/kit/formal/proofscriptparser/lint/LintProblem.java
...va/edu/kit/formal/proofscriptparser/lint/LintProblem.java
+6
-2
src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/IssuesId.java
.../kit/formal/proofscriptparser/lint/checkers/IssuesId.java
+4
-1
src/main/java/edu/kit/formal/proofscriptparser/lint/checkers/VariableDeclarationCheck.java
...fscriptparser/lint/checkers/VariableDeclarationCheck.java
+119
-0
src/main/resources/META-INF/services/edu.kit.formal.proofscriptparser.lint.LintRule
...F/services/edu.kit.formal.proofscriptparser.lint.LintRule
+2
-1
src/main/resources/edu/kit/formal/proofscriptparser/lint/lint-issues-en.xml
.../edu/kit/formal/proofscriptparser/lint/lint-issues-en.xml
+9
-1
src/test/java/edu/kit/formal/proofscriptparser/lint/LinterTest.java
...ava/edu/kit/formal/proofscriptparser/lint/LinterTest.java
+13
-3
src/test/resources/edu/kit/formal/proofscriptparser/lint/lint2.kps
...resources/edu/kit/formal/proofscriptparser/lint/lint2.kps
+24
-0
No files found.
src/main/java/edu/kit/formal/proofscriptparser/ASTTraversal.java
View file @
e4dcaaf4
...
...
@@ -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
View file @
e4dcaaf4
...
...
@@ -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
View file @
e4dcaaf4
...
...
@@ -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
View file @
e4dcaaf4
...
...
@@ -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
0 → 100644
View file @
e4dcaaf4
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
View file @
e4dcaaf4
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
View file @
e4dcaaf4
<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
View file @
e4dcaaf4
...
...
@@ -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
0 → 100644
View file @
e4dcaaf4
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;
}
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment