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
d7e2b00f
Commit
d7e2b00f
authored
Jun 26, 2017
by
Sarah Grebing
Browse files
Interim (incomplete commit)
parent
f15159ee
Pipeline
#11593
passed with stage
in 2 minutes and 15 seconds
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
d7e2b00f
...
...
@@ -4,7 +4,10 @@ import de.uka.ilkd.key.proof.init.ProofInputException;
import
de.uka.ilkd.key.speclang.Contract
;
import
edu.kit.formal.gui.controls.*
;
import
edu.kit.formal.gui.model.RootModel
;
import
edu.kit.formal.interpreter.*
;
import
edu.kit.formal.interpreter.Interpreter
;
import
edu.kit.formal.interpreter.InterpreterBuilder
;
import
edu.kit.formal.interpreter.KeYProofFacade
;
import
edu.kit.formal.interpreter.ProofTreeController
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.interpreter.data.State
;
import
edu.kit.formal.proofscriptparser.Facade
;
...
...
@@ -159,7 +162,7 @@ public class DebuggerMainWindowController implements Initializable {
});
/**
* create a new ins
e
pctionviewtab that is the main tab and not closable
* create a new insp
e
ctionviewtab that is the main tab and not closable
*/
inspectionViewTabPane
.
createNewInspectionViewTab
(
model
,
true
);
...
...
@@ -224,10 +227,10 @@ public class DebuggerMainWindowController implements Initializable {
if
(
debugMode
)
{
blocker
.
getStepUntilBlock
().
set
(
1
);
//for stepping functionality
StateGraphVisitor
visitor
=
new
StateGraphVisitor
(
currentInterpreter
,
scripts
.
get
(
0
));
pc
=
new
ProofTreeController
(
currentInterpreter
,
scripts
.
get
(
0
),
visitor
);
currentInterpreter
.
getEntryListeners
().
add
(
visitor
);
pc
=
new
ProofTreeController
(
currentInterpreter
,
scripts
.
get
(
0
));
currentInterpreter
.
getEntryListeners
().
add
(
pc
.
getStateVisitor
());
}
blocker
.
install
(
currentInterpreter
);
...
...
@@ -391,8 +394,7 @@ public class DebuggerMainWindowController implements Initializable {
}
public
void
stepBack
(
ActionEvent
actionEvent
)
{
System
.
out
.
println
(
blocker
.
getHistoryLogger
());
blocker
.
unlock
();
pc
.
stepBack
();
}
...
...
src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java
View file @
d7e2b00f
...
...
@@ -2,24 +2,35 @@ package edu.kit.formal.interpreter;
import
edu.kit.formal.proofscriptparser.ast.ASTNode
;
import
java.util.ArrayList
;
import
java.util.List
;
/**
* ControlFlowNode for ControlFlowGraph to look up step-edges for teh debugger.
*/
@Deprecated
public
class
ControlFlowNode
{
edu
.
kit
.
formal
.
proofscriptparser
.
ast
.
ASTNode
scriptstmt
;
private
ASTNode
scriptstmt
;
private
List
<
ASTNode
>
callCtx
=
new
ArrayList
<>();
public
ControlFlowNode
(
ASTNode
node
)
{
this
.
setScriptstmt
(
node
);
}
public
List
<
ASTNode
>
getCallCtx
()
{
return
callCtx
;
}
public
edu
.
kit
.
formal
.
proofscriptparser
.
ast
.
ASTNode
getScriptstmt
()
{
public
void
setCallCtx
(
List
<
ASTNode
>
callCtx
)
{
this
.
callCtx
=
callCtx
;
}
public
ASTNode
getScriptstmt
()
{
return
scriptstmt
;
}
public
void
setScriptstmt
(
edu
.
kit
.
formal
.
proofscriptparser
.
ast
.
ASTNode
scriptstmt
)
{
public
void
setScriptstmt
(
ASTNode
scriptstmt
)
{
this
.
scriptstmt
=
scriptstmt
;
}
...
...
@@ -27,10 +38,15 @@ public class ControlFlowNode {
StringBuilder
sb
=
new
StringBuilder
();
sb
.
append
(
"Node {"
);
if
(
scriptstmt
!=
null
)
{
sb
.
append
(
scriptstmt
.
toString
());
sb
.
append
(
scriptstmt
.
getNodeName
().
toString
());
}
else
{
sb
.
append
(
"No Stmt"
);
}
if
(
callCtx
.
isEmpty
())
{
sb
.
append
(
"Empty Context"
);
}
else
{
sb
.
append
(
callCtx
.
toString
());
}
sb
.
append
(
"}"
);
return
sb
.
toString
();
}
...
...
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
View file @
d7e2b00f
...
...
@@ -7,6 +7,7 @@ import edu.kit.formal.interpreter.funchdl.ProofScriptHandler;
import
edu.kit.formal.proofscriptparser.DefaultASTVisitor
;
import
edu.kit.formal.proofscriptparser.ast.*
;
import
java.util.ArrayList
;
import
java.util.List
;
/**
...
...
@@ -22,40 +23,47 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
/**
* Last visited Node
*/
private
AST
Node
lastNode
;
private
ControlFlow
Node
lastNode
;
/**
* Control Flow Graph
*/
private
MutableValueGraph
<
AST
Node
,
EdgeTypes
>
graph
=
ValueGraphBuilder
.
directed
().
allowsSelfLoops
(
true
).
build
();
private
MutableValueGraph
<
ControlFlow
Node
,
EdgeTypes
>
graph
=
ValueGraphBuilder
.
directed
().
allowsSelfLoops
(
true
).
build
();
private
List
<
ASTNode
>
context
=
new
ArrayList
<>();
public
ProgramFlowVisitor
(
CommandLookup
functionLookup
)
{
this
.
functionLookup
=
functionLookup
;
}
public
MutableValueGraph
<
AST
Node
,
EdgeTypes
>
getGraph
()
{
public
MutableValueGraph
<
ControlFlow
Node
,
EdgeTypes
>
getGraph
()
{
return
graph
;
}
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
lastNode
=
proofScript
;
ControlFlowNode
scriptNode
=
new
ControlFlowNode
(
proofScript
);
graph
.
addNode
(
scriptNode
);
System
.
out
.
println
(
"\n"
+
scriptNode
+
"\n"
);
lastNode
=
scriptNode
;
return
this
.
visit
(
proofScript
.
getBody
());
}
@Override
public
Void
visit
(
AssignmentStatement
assignment
)
{
graph
.
addNode
(
assignment
);
lastNode
=
assignment
;
ControlFlowNode
assignmentNode
=
new
ControlFlowNode
(
assignment
);
graph
.
addNode
(
assignmentNode
);
System
.
out
.
println
(
"\n"
+
assignmentNode
+
"\n"
);
lastNode
=
assignmentNode
;
return
null
;
}
@Override
public
Void
visit
(
Statements
statements
)
{
AST
Node
curLastNode
=
lastNode
;
ControlFlow
Node
curLastNode
=
lastNode
;
for
(
Statement
stmnt
:
statements
)
{
stmnt
.
accept
(
this
);
graph
.
putEdgeValue
(
curLastNode
,
lastNode
,
EdgeTypes
.
STEP_OVER
);
...
...
@@ -66,26 +74,24 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
return
null
;
}
//stack wenn atomic false
@Override
public
Void
visit
(
CallStatement
call
)
{
ASTNode
currentNode
=
call
;
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
call
);
if
(!
context
.
isEmpty
())
{
currentNode
.
setCallCtx
(
context
);
}
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
currentNode
;
boolean
atomic
=
functionLookup
.
isAtomic
(
call
);
//Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist
if
(
atomic
)
{
context
.
add
(
call
);
// graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
ProofScriptHandler
psh
=
(
ProofScriptHandler
)
functionLookup
.
getBuilder
(
call
);
psh
.
getScript
(
call
.
getCommand
()).
getBody
().
accept
(
this
);
...
...
@@ -93,7 +99,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_RETURN
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_INTO
);
}
context
.
remove
(
call
);
lastNode
=
currentNode
;
return
null
;
...
...
@@ -101,8 +107,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
AST
Node
currentNode
=
foreach
;
ControlFlow
Node
currentNode
=
new
ControlFlowNode
(
foreach
)
;
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
currentNode
;
...
...
@@ -114,8 +121,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
TheOnlyStatement
theOnly
)
{
AST
Node
currentNode
=
theOnly
;
ControlFlow
Node
currentNode
=
new
ControlFlowNode
(
theOnly
)
;
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
currentNode
;
...
...
@@ -128,8 +136,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
RepeatStatement
repeatStatement
)
{
AST
Node
currentNode
=
repeatStatement
;
ControlFlow
Node
currentNode
=
new
ControlFlowNode
(
repeatStatement
)
;
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
currentNode
;
...
...
@@ -141,14 +150,16 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
AST
Node
currentNode
=
casesStatement
;
ControlFlow
Node
currentNode
=
new
ControlFlowNode
(
casesStatement
)
;
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_BACK
);
List
<
CaseStatement
>
cases
=
casesStatement
.
getCases
();
for
(
CaseStatement
aCase
:
cases
)
{
AST
Node
caseNode
=
aCase
;
ControlFlow
Node
caseNode
=
new
ControlFlowNode
(
aCase
)
;
graph
.
addNode
(
caseNode
);
System
.
out
.
println
(
"\n"
+
caseNode
+
"\n"
);
graph
.
putEdgeValue
(
currentNode
,
caseNode
,
EdgeTypes
.
STEP_OVER
);
//??is this right?
graph
.
putEdgeValue
(
caseNode
,
currentNode
,
EdgeTypes
.
STEP_BACK
);
lastNode
=
caseNode
;
...
...
@@ -167,9 +178,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
graph
.
nodes
().
forEach
(
n
->
{
sb
.
append
(
n
.
hashCode
())
.
append
(
" [label=\""
)
.
append
(
n
.
getNodeName
())
.
append
(
n
.
getScriptstmt
().
getNodeName
())
.
append
(
"@"
)
.
append
(
n
.
getStartPosition
().
getLineNumber
())
.
append
(
n
.
getScriptstmt
().
getStartPosition
().
getLineNumber
())
.
append
(
"\"]\n"
);
});
...
...
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
View file @
d7e2b00f
...
...
@@ -2,6 +2,7 @@ package edu.kit.formal.interpreter;
import
com.google.common.graph.MutableValueGraph
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.proofscriptparser.Visitor
;
import
edu.kit.formal.proofscriptparser.ast.ASTNode
;
import
edu.kit.formal.proofscriptparser.ast.ProofScript
;
...
...
@@ -11,12 +12,15 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
* @author S. Grebing
*/
public
class
ProofTreeController
{
//TODO Listener auf den Interperter
StateGraphVisitor
stateGraphVisitor
;
/**
* Visitor to retrieve state graph
*/
private
StateGraphVisitor
stateGraphVisitor
;
/**
* ControlFlowGraph to lookup edges
*/
private
MutableValueGraph
<
AST
Node
,
EdgeTypes
>
controlFlowGraph
;
private
MutableValueGraph
<
ControlFlow
Node
,
EdgeTypes
>
controlFlowGraph
;
/**
* Graph that is computed on the fly in order to allow stepping
*/
...
...
@@ -30,13 +34,14 @@ public class ProofTreeController {
*/
private
PTreeNode
statePointer
;
public
ProofTreeController
(
Interpreter
<
KeyData
>
inter
,
ProofScript
mainScript
,
StateGraphVisitor
stateGraphVisitor
)
{
public
ProofTreeController
(
Interpreter
<
KeyData
>
inter
,
ProofScript
mainScript
)
{
this
.
currentInterpreter
=
inter
;
buildControlFlowGraph
(
mainScript
);
this
.
stateGraphVisitor
=
new
StateGraphVisitor
(
inter
,
mainScript
,
this
.
controlFlowGraph
);
stateGraph
=
stateGraphVisitor
.
getStateGraph
();
statePointer
=
stateGraphVisitor
.
getRootNode
();
this
.
stateGraphVisitor
=
stateGraphVisitor
;
// System.out.println(stateGraph.nodes());
//initializeStateGraph(mainScript);
...
...
@@ -50,44 +55,29 @@ public class ProofTreeController {
*/
private
void
buildControlFlowGraph
(
ProofScript
mainScript
)
{
ProgramFlowVisitor
visitor
=
new
ProgramFlowVisitor
(
currentInterpreter
.
getFunctionLookup
());
mainScript
.
accept
(
visitor
);
this
.
controlFlowGraph
=
visitor
.
getGraph
();
//
System.out.println(visitor.asdot());
System
.
out
.
println
(
visitor
.
asdot
());
}
/* private void initializeStateGraph(ProofScript mainScript){
stateGraph = ValueGraphBuilder.directed().build();
State<KeyData> initState = currentInterpreter.getCurrentState();
System.out.println(initState);
PTreeNode initNode = new PTreeNode(mainScript);
initNode.setState(initState);
stateGraph.addNode(initNode);
// statePointer = initNode;
}*/
public
PTreeNode
stepOver
()
{
if
(
statePointer
==
null
)
{
this
.
statePointer
=
stateGraphVisitor
.
getLastNode
();
}
PTreeNode
current
=
statePointer
;
ASTNode
stmt
=
current
.
getScriptstmt
();
System
.
out
.
println
(
"CurrentPointer: "
+
stmt
.
getNodeName
()
+
"@"
+
stmt
.
getStartPosition
());
if
(
controlFlowGraph
.
asGraph
().
nodes
().
contains
(
stmt
))
{
// System.out.println("\n\nAdjacent:{\n"+controlFlowGraph.asGraph().adjacentNodes(stmt)+"}\n\n\n");
Object
[]
nodeArray
=
controlFlowGraph
.
asGraph
().
adjacentNodes
(
stmt
).
toArray
();
ASTNode
firtSucc
=
(
ASTNode
)
nodeArray
[
0
];
for
(
PTreeNode
succ
:
stateGraph
.
successors
(
current
))
{
if
(
succ
.
getScriptstmt
().
equals
(
firtSucc
))
{
statePointer
=
succ
;
}
}
// Object[] nodeArray = controlFlowGraph.asGraph().adjacentNodes(stmt).toArray();
// ControlFlowNode firtSucc = (ControlFlowNode) nodeArray[0];
// for (PTreeNode succ : stateGraph.successors(current)) {
// if (succ.getScriptstmt().equals(firtSucc)) {
// statePointer = succ;
// }
// }
}
//System.out.println(stateGraphVisitor.asdot());
return
null
;
}
...
...
@@ -104,4 +94,7 @@ public class ProofTreeController {
}
public
Visitor
getStateVisitor
()
{
return
this
.
stateGraphVisitor
;
}
}
src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java
View file @
d7e2b00f
...
...
@@ -3,11 +3,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.data.State
;
import
edu.kit.formal.proofscriptparser.DefaultASTVisitor
;
import
edu.kit.formal.proofscriptparser.ast.
ASTNode
;
import
edu.kit.formal.proofscriptparser.ast.ProofScript
;
import
edu.kit.formal.proofscriptparser.ast.
*
;
/**
* Created by sarah on 6/26/17.
...
...
@@ -18,21 +16,22 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
* Graph that is computed on the fly in order to allow stepping
*/
private
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
stateGraph
;
private
PTreeNode
root
;
private
PTreeNode
lastNode
;
public
StateGraphVisitor
(
Interpreter
inter
,
ProofScript
mainScript
)
{
/**
* Control Flow Graph
*/
private
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
graph
;
public
StateGraphVisitor
(
Interpreter
inter
,
ProofScript
mainScript
,
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
cfg
)
{
stateGraph
=
ValueGraphBuilder
.
directed
().
build
();
this
.
currentInterpreter
=
inter
;
State
<
KeyData
>
initState
=
currentInterpreter
.
getCurrentState
();
System
.
out
.
println
(
initState
);
PTreeNode
initNode
=
new
PTreeNode
(
mainScript
);
initNode
.
setState
(
initState
);
stateGraph
.
addNode
(
initNode
);
root
=
initNode
;
lastNode
=
initNode
;
graph
=
cfg
;
System
.
out
.
println
(
cfg
.
nodes
().
stream
().
toString
());
}
...
...
@@ -48,17 +47,68 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
return
lastNode
;
}
@Override
public
Void
defaultVisit
(
ASTNode
node
)
{
public
Void
createNewNode
(
ASTNode
node
)
{
PTreeNode
newStateNode
=
new
PTreeNode
(
node
);
newStateNode
.
setState
(
currentInterpreter
.
getCurrentState
());
stateGraph
.
addNode
(
newStateNode
);
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
EdgeTypes
.
STATE_FLOW
);
if
(
lastNode
==
null
)
{
root
=
newStateNode
;
}
else
{
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
EdgeTypes
.
STATE_FLOW
);
}
lastNode
=
newStateNode
;
System
.
out
.
println
(
asdot
());
return
null
;
}
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
createNewNode
(
proofScript
);
return
null
;
}
@Override
public
Void
visit
(
AssignmentStatement
assignment
)
{
return
createNewNode
(
assignment
);
}
@Override
public
Void
visit
(
Statements
statements
)
{
return
createNewNode
(
statements
);
}
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
return
createNewNode
(
casesStatement
);
}
@Override
public
Void
visit
(
CaseStatement
caseStatement
)
{
return
createNewNode
(
caseStatement
);
}
@Override
public
Void
visit
(
CallStatement
call
)
{
return
createNewNode
(
call
);
}
@Override
public
Void
visit
(
TheOnlyStatement
theOnly
)
{
return
createNewNode
(
theOnly
);
}
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
return
createNewNode
(
foreach
);
}
@Override
public
Void
visit
(
RepeatStatement
repeatStatement
)
{
return
createNewNode
(
repeatStatement
);
}
public
String
asdot
()
{
StringBuilder
sb
=
new
StringBuilder
();
sb
.
append
(
"digraph G {\nnode [shape=rect]\n "
);
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/DefaultLookup.java
View file @
d7e2b00f
...
...
@@ -32,12 +32,17 @@ public class DefaultLookup implements CommandLookup {
b
.
evaluate
(
interpreter
,
call
,
params
);
}
@Override
public
boolean
isAtomic
(
CallStatement
call
)
{
CommandHandler
cmdh
=
getBuilder
(
call
);
if
(
cmdh
!=
null
)
return
cmdh
.
isAtomic
();
return
true
;
try
{
CommandHandler
cmdh
=
getBuilder
(
call
);
if
(
cmdh
!=
null
)
return
cmdh
.
isAtomic
();
return
true
;
}
catch
(
NoCallHandlerException
nche
)
{
return
false
;
}
}
public
CommandHandler
getBuilder
(
CallStatement
callStatement
)
{
...
...
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