Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
7e1fbb84
Commit
7e1fbb84
authored
Jun 23, 2017
by
Sarah Grebing
Browse files
Merge changes and commit enahcnements for controlflowgraph
parent
8f5c005d
Pipeline
#11464
failed with stage
in 2 minutes and 23 seconds
Changes
10
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java
0 → 100644
View file @
7e1fbb84
package
edu.kit.formal.interpreter
;
import
edu.kit.formal.proofscriptparser.ast.ASTNode
;
/**
* ControlFlowNode for ControlFlowGraph to look up step-edges for teh debugger.
*/
public
class
ControlFlowNode
{
ASTNode
scriptstmt
;
public
ControlFlowNode
(
ASTNode
node
)
{
this
.
setScriptstmt
(
node
);
}
public
ASTNode
getScriptstmt
()
{
return
scriptstmt
;
}
public
void
setScriptstmt
(
ASTNode
scriptstmt
)
{
this
.
scriptstmt
=
scriptstmt
;
}
public
String
toString
()
{
StringBuilder
sb
=
new
StringBuilder
();
sb
.
append
(
"Node {"
);
if
(
scriptstmt
!=
null
)
{
sb
.
append
(
scriptstmt
.
toString
());
}
else
{
sb
.
append
(
"No Stmt"
);
}
sb
.
append
(
"}"
);
return
sb
.
toString
();
}
}
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
View file @
7e1fbb84
...
...
@@ -2,7 +2,9 @@ package edu.kit.formal.interpreter;
import
com.google.common.graph.MutableValueGraph
;
import
com.google.common.graph.ValueGraphBuilder
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.interpreter.funchdl.CommandLookup
;
import
edu.kit.formal.interpreter.funchdl.ProofScriptHandler
;
import
edu.kit.formal.proofscriptparser.DefaultASTVisitor
;
import
edu.kit.formal.proofscriptparser.ast.*
;
...
...
@@ -10,29 +12,32 @@ import edu.kit.formal.proofscriptparser.ast.*;
* Visitor to create ProgramFlowGraph
*/
public
class
ProgramFlowVisitor
extends
DefaultASTVisitor
<
Void
>
{
private
final
CommandLookup
functionLookup
;
private
PTreeNode
lastNode
;
private
ControlFlowNode
lastNode
;
private
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
graph
=
ValueGraphBuilder
.
directed
().
allowsSelfLoops
(
true
).
build
();
private
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
graph
=
ValueGraphBuilder
.
directed
().
allowsSelfLoops
(
true
).
build
()
;
private
Interpreter
<
KeyData
>
inter
;
public
ProgramFlowVisitor
(
CommandLookup
functionLookup
)
{
this
.
functionLookup
=
functionLookup
;
}
public
MutableValueGraph
<
PTree
Node
,
EdgeTypes
>
getGraph
()
{
public
MutableValueGraph
<
ControlFlow
Node
,
EdgeTypes
>
getGraph
()
{
return
graph
;
}
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
PTree
Node
scriptNode
=
new
PTree
Node
(
proofScript
);
ControlFlow
Node
scriptNode
=
new
ControlFlow
Node
(
proofScript
);
lastNode
=
scriptNode
;
return
this
.
visit
(
proofScript
.
getBody
());
}
@Override
public
Void
visit
(
AssignmentStatement
assignment
)
{
PTree
Node
node
=
new
PTree
Node
(
assignment
);
ControlFlow
Node
node
=
new
ControlFlow
Node
(
assignment
);
graph
.
addNode
(
node
);
lastNode
=
node
;
return
null
;
...
...
@@ -40,7 +45,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
Statements
statements
)
{
PTree
Node
curLastNode
=
lastNode
;
ControlFlow
Node
curLastNode
=
lastNode
;
for
(
Statement
stmnt
:
statements
)
{
stmnt
.
accept
(
this
);
graph
.
putEdgeValue
(
curLastNode
,
lastNode
,
EdgeTypes
.
STEP_OVER
);
...
...
@@ -53,19 +58,47 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
CallStatement
call
)
{
PTreeNode
currentNode
=
new
PTreeNode
(
call
);
//fixme handle stepinto
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
call
);
graph
.
addNode
(
currentNode
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
currentNode
;
CommandLookup
lookup
=
inter
.
getFunctionLookup
();
boolean
atomic
=
lookup
.
isAtomic
(
call
);
//Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist
if
(
atomic
)
{
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_INTO
);
// graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
ProofScriptHandler
psh
=
(
ProofScriptHandler
)
lookup
.
getBuilder
(
call
);
psh
.
getScript
(
call
.
getCommand
()).
getBody
().
accept
(
this
);
//verbinde letzten knoten aus auruf mi step return zu aktuellem knoten
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_RETURN
);
}
lastNode
=
currentNode
;
return
null
;
}
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
return
super
.
visit
(
foreach
);
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
foreach
);
graph
.
addNode
(
currentNode
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
currentNode
;
foreach
.
getBody
().
accept
(
this
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_RETURN
);
lastNode
=
currentNode
;
return
null
;
}
@Override
...
...
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
View file @
7e1fbb84
...
...
@@ -5,31 +5,50 @@ import edu.kit.formal.interpreter.data.KeyData;
import
edu.kit.formal.proofscriptparser.ast.ProofScript
;
/**
* Class controlling proof tree structure for debugger
* Class controlling
and maintaining
proof tree structure for debugger
and handling step functions for the debugger
*
* @author S. Grebing
*/
public
class
ProofTreeController
{
private
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
graph
;
/**
* ControlFlowGraph to lookup edges
*/
private
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
controlFlowGraph
;
private
Interpreter
<
KeyData
>
currentInterpreter
;
/**
* Graph that is computed on the fly in order to allow stepping
*/
private
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
stateGraph
;
/**
* Current interpreter
*/
private
Interpreter
<
KeyData
>
currentInterpreter
;
/**
* Current State in graph
*/
private
PTreeNode
statePointer
;
public
ProofTreeController
(
Interpreter
<
KeyData
>
inter
,
ProofScript
mainScript
)
{
this
.
currentInterpreter
=
inter
;
build
Empty
Graph
(
mainScript
);
build
ControlFlow
Graph
(
mainScript
);
}
private
void
buildEmptyGraph
(
ProofScript
mainScript
)
{
/**
* Build the control flow graph for looking up step-edges for the given script inligning called script commands
*
* @param mainScript
*/
private
void
buildControlFlowGraph
(
ProofScript
mainScript
)
{
ProgramFlowVisitor
visitor
=
new
ProgramFlowVisitor
(
currentInterpreter
.
getFunctionLookup
());
mainScript
.
accept
(
visitor
);
System
.
out
.
println
(
visitor
.
getGraph
());
this
.
controlFlowGraph
=
visitor
.
getGraph
();
System
.
out
.
println
(
controlFlowGraph
);
}
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/CommandHandler.java
View file @
7e1fbb84
...
...
@@ -26,4 +26,8 @@ public interface CommandHandler<T> {
void
evaluate
(
Interpreter
<
T
>
interpreter
,
CallStatement
call
,
VariableAssignment
params
);
default
boolean
isAtomic
()
{
return
false
;
}
}
src/main/java/edu/kit/formal/interpreter/funchdl/CommandLookup.java
View file @
7e1fbb84
...
...
@@ -10,4 +10,8 @@ import edu.kit.formal.proofscriptparser.ast.CallStatement;
*/
public
interface
CommandLookup
<
T
>
{
void
callCommand
(
Interpreter
<
T
>
i
,
CallStatement
c
,
VariableAssignment
p
);
boolean
isAtomic
(
CallStatement
call
);
public
CommandHandler
getBuilder
(
CallStatement
callStatement
);
}
src/main/java/edu/kit/formal/interpreter/funchdl/DefaultLookup.java
View file @
7e1fbb84
...
...
@@ -32,7 +32,15 @@ public class DefaultLookup implements CommandLookup {
b
.
evaluate
(
interpreter
,
call
,
params
);
}
private
CommandHandler
getBuilder
(
CallStatement
callStatement
)
{
@Override
public
boolean
isAtomic
(
CallStatement
call
)
{
CommandHandler
cmdh
=
getBuilder
(
call
);
if
(
cmdh
!=
null
)
return
cmdh
.
isAtomic
();
return
true
;
}
public
CommandHandler
getBuilder
(
CallStatement
callStatement
)
{
CommandHandler
found
=
null
;
for
(
CommandHandler
b
:
builders
)
{
if
(
b
.
handles
(
callStatement
))
{
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @
7e1fbb84
...
...
@@ -19,6 +19,7 @@ import java.util.HashMap;
import
java.util.Map
;
/**
* This class handle the call of key's proof script commands, e.g. select or auto;
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptHandler.java
View file @
7e1fbb84
...
...
@@ -37,6 +37,9 @@ public class ProofScriptHandler implements CommandHandler {
proofScripts
.
forEach
(
s
->
scripts
.
put
(
s
.
getName
(),
s
));
}
public
ProofScript
getScript
(
String
name
)
{
return
scripts
.
get
(
name
);
}
/**
* lib/test.test
*
...
...
@@ -93,6 +96,11 @@ public class ProofScriptHandler implements CommandHandler {
ps
.
accept
(
interpreter
);
}
@Override
public
boolean
isAtomic
()
{
return
true
;
}
public
void
addScripts
(
List
<
ProofScript
>
ast
)
{
ast
.
forEach
(
script
->
scripts
.
put
(
script
.
getName
(),
script
));
}
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/RuleCommandHandler.java
View file @
7e1fbb84
...
...
@@ -70,4 +70,5 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
throw
new
RuntimeException
(
e
);
}
}
}
src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps
View file @
7e1fbb84
script t(i:int, j:int){
i:= 0;
j:= 0;
f;
g;
}
script f(){
impRight;
}
script g(){
impLeft;
}
\ No newline at end of file
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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