Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
a8e7207d
Commit
a8e7207d
authored
Jun 27, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Interim (incomplete commit)
parent
d7e2b00f
Changes
6
Show whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
154 additions
and
60 deletions
+154
-60
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
...t/formal/gui/controller/DebuggerMainWindowController.java
+11
-10
src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java
...main/java/edu/kit/formal/interpreter/ControlFlowNode.java
+13
-4
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
...n/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
+52
-8
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
.../java/edu/kit/formal/interpreter/ProofTreeController.java
+25
-31
src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java
...in/java/edu/kit/formal/interpreter/StateGraphVisitor.java
+41
-7
src/test/resources/edu/kit/formal/interpreter/contraposition/recursion.kps
...s/edu/kit/formal/interpreter/contraposition/recursion.kps
+12
-0
No files found.
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
a8e7207d
...
...
@@ -52,7 +52,7 @@ public class DebuggerMainWindowController implements Initializable {
private
final
PuppetMaster
blocker
=
new
PuppetMaster
();
private
SimpleBooleanProperty
debugMode
=
new
SimpleBooleanProperty
(
false
);
// private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
@FXML
private
Pane
rootPane
;
...
...
@@ -62,12 +62,9 @@ public class DebuggerMainWindowController implements Initializable {
* Code Area
* **********************************************************************************************************/
//@FXML
//private ScriptArea scriptArea;
@FXML
private
ScriptTabPane
tabPane
;
//@FXML
//private Tab startTab;
/***********************************************************************************************************
* MenuBar
* **********************************************************************************************************/
...
...
@@ -113,7 +110,11 @@ public class DebuggerMainWindowController implements Initializable {
private
ObservableBooleanValue
executeNotPossible
=
interpreterService
.
runningProperty
().
or
(
facade
.
readyToExecuteProperty
().
not
());
/**
* Controller for debugging functions
*/
private
ProofTreeController
pc
;
public
static
void
showExceptionDialog
(
String
title
,
String
headerText
,
String
contentText
,
Throwable
ex
)
{
Alert
alert
=
new
Alert
(
Alert
.
AlertType
.
ERROR
);
alert
.
setTitle
(
title
);
...
...
@@ -226,14 +227,14 @@ public class DebuggerMainWindowController implements Initializable {
Interpreter
<
KeyData
>
currentInterpreter
=
ib
.
build
();
if
(
debugMode
)
{
blocker
.
getStepUntilBlock
().
set
(
1
);
//
blocker.getStepUntilBlock().set(1);
//for stepping functionality
pc
=
new
ProofTreeController
(
currentInterpreter
,
scripts
.
get
(
0
));
currentInterpreter
.
getEntryListeners
().
add
(
pc
.
getStateVisitor
());
}
blocker
.
install
(
currentInterpreter
);
//
blocker.install(currentInterpreter);
//highlight signature of main script
tabPane
.
getSelectedScriptArea
().
setDebugMark
(
scripts
.
get
(
0
).
getStartPosition
().
getLineNumber
());
...
...
@@ -388,8 +389,8 @@ public class DebuggerMainWindowController implements Initializable {
}
public
void
stepOver
(
ActionEvent
actionEvent
)
{
blocker
.
getStepUntilBlock
().
addAndGet
(
1
);
blocker
.
unlock
();
//
blocker.getStepUntilBlock().addAndGet(1);
//
blocker.unlock();
pc
.
stepOver
();
}
...
...
@@ -487,7 +488,7 @@ public class DebuggerMainWindowController implements Initializable {
private
void
updateView
()
{
//check proof
//
check state for empty/error goal nodes
leer
//check state for empty/error goal nodes
//currentGoals.set(state.getGoals());
//currentSelectedGoal.set(state.getSelectedGoalNode());
blocker
.
publishState
();
...
...
src/main/java/edu/kit/formal/interpreter/ControlFlowNode.java
View file @
a8e7207d
...
...
@@ -2,7 +2,7 @@ package edu.kit.formal.interpreter;
import
edu.kit.formal.proofscriptparser.ast.ASTNode
;
import
java.util.
Array
List
;
import
java.util.
Linked
List
;
import
java.util.List
;
/**
...
...
@@ -11,18 +11,27 @@ import java.util.List;
public
class
ControlFlowNode
{
/**
* Statement node
*/
private
ASTNode
scriptstmt
;
private
List
<
ASTNode
>
callCtx
=
new
ArrayList
<>();
/**
* Call context
*/
private
LinkedList
<
ASTNode
>
callCtx
=
new
LinkedList
<>();
public
ControlFlowNode
(
ASTNode
node
)
{
this
.
setScriptstmt
(
node
);
}
public
List
<
ASTNode
>
getCallCtx
()
{
return
callCtx
;
}
public
void
setCallCtx
(
List
<
ASTNode
>
callCtx
)
{
public
void
setCallCtx
(
Linked
List
<
ASTNode
>
callCtx
)
{
this
.
callCtx
=
callCtx
;
}
...
...
@@ -38,7 +47,7 @@ public class ControlFlowNode {
StringBuilder
sb
=
new
StringBuilder
();
sb
.
append
(
"Node {"
);
if
(
scriptstmt
!=
null
)
{
sb
.
append
(
scriptstmt
.
getNodeName
().
toString
());
sb
.
append
(
scriptstmt
.
getNodeName
().
toString
()
+
"@"
+
scriptstmt
.
getStartPosition
()
);
}
else
{
sb
.
append
(
"No Stmt"
);
}
...
...
src/main/java/edu/kit/formal/interpreter/ProgramFlowVisitor.java
View file @
a8e7207d
package
edu.kit.formal.interpreter
;
import
com.google.common.graph.EndpointPair
;
import
com.google.common.graph.MutableValueGraph
;
import
com.google.common.graph.ValueGraphBuilder
;
import
edu.kit.formal.interpreter.funchdl.CommandLookup
;
...
...
@@ -7,8 +8,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
;
import
java.util.*
;
/**
* Visitor to create ProgramFlowGraph
...
...
@@ -19,7 +19,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
* Lookup for names of scripts
*/
private
final
CommandLookup
functionLookup
;
private
Map
<
ASTNode
,
ControlFlowNode
>
mappingOfNodes
;
/**
* Last visited Node
*/
...
...
@@ -30,20 +30,45 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
*/
private
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
graph
=
ValueGraphBuilder
.
directed
().
allowsSelfLoops
(
true
).
build
();
private
List
<
ASTNode
>
context
=
new
Array
List
<>();
private
Linked
List
<
ASTNode
>
context
=
new
Linked
List
<>();
public
ProgramFlowVisitor
(
CommandLookup
functionLookup
)
{
this
.
functionLookup
=
functionLookup
;
mappingOfNodes
=
new
HashMap
<>();
}
public
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
getGraph
()
{
return
graph
;
}
public
Set
<
EndpointPair
<
ControlFlowNode
>>
getAllEdgesForNodeAsTarget
(
ASTNode
node
)
{
ControlFlowNode
assocNode
=
mappingOfNodes
.
get
(
node
);
if
(
assocNode
!=
null
)
{
Set
<
EndpointPair
<
ControlFlowNode
>>
edges
=
new
HashSet
<>();
graph
.
edges
().
forEach
(
e
->
{
if
(
e
.
target
().
equals
(
assocNode
))
{
edges
.
add
(
e
);
System
.
out
.
println
(
e
.
target
());
System
.
out
.
println
(
e
.
source
());
System
.
out
.
println
(
graph
.
edgeValue
(
e
.
target
(),
e
.
source
()));
}
});
return
edges
;
}
else
{
return
Collections
.
EMPTY_SET
;
}
}
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
ControlFlowNode
scriptNode
=
new
ControlFlowNode
(
proofScript
);
mappingOfNodes
.
put
(
proofScript
,
scriptNode
);
graph
.
addNode
(
scriptNode
);
System
.
out
.
println
(
"\n"
+
scriptNode
+
"\n"
);
lastNode
=
scriptNode
;
...
...
@@ -55,6 +80,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
public
Void
visit
(
AssignmentStatement
assignment
)
{
ControlFlowNode
assignmentNode
=
new
ControlFlowNode
(
assignment
);
mappingOfNodes
.
put
(
assignment
,
assignmentNode
);
graph
.
addNode
(
assignmentNode
);
System
.
out
.
println
(
"\n"
+
assignmentNode
+
"\n"
);
lastNode
=
assignmentNode
;
...
...
@@ -74,32 +100,45 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
return
null
;
}
//stack wenn atomic false
@Override
public
Void
visit
(
CallStatement
call
)
{
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
call
);
if
(!
context
.
isEmpty
())
{
currentNode
.
setCallCtx
(
context
);
}
mappingOfNodes
.
put
(
call
,
currentNode
);
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
)
{
LinkedList
<
ASTNode
>
copiedContext
=
new
LinkedList
<>();
//to check whether context is restored properly, copy context before call
context
.
stream
().
forEach
(
e
->
{
copiedContext
.
add
(
e
);
});
context
.
add
(
call
);
// graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
ProofScriptHandler
psh
=
(
ProofScriptHandler
)
functionLookup
.
getBuilder
(
call
);
psh
.
getScript
(
call
.
getCommand
()).
getBody
().
accept
(
this
);
//verbinde letzten knoten aus auruf mit step return zu aktuellem knoten
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_RETURN
);
graph
.
putEdgeValue
(
currentNode
,
lastNode
,
EdgeTypes
.
STEP_INTO
);
context
.
removeLast
();
//check if context is restored properly
//copiedcontext == context
}
context
.
remove
(
call
);
lastNode
=
currentNode
;
return
null
;
...
...
@@ -108,6 +147,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
foreach
);
mappingOfNodes
.
put
(
foreach
,
currentNode
);
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
...
...
@@ -122,6 +162,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
TheOnlyStatement
theOnly
)
{
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
theOnly
);
mappingOfNodes
.
put
(
theOnly
,
currentNode
);
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
...
...
@@ -137,6 +178,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
RepeatStatement
repeatStatement
)
{
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
repeatStatement
);
mappingOfNodes
.
put
(
repeatStatement
,
currentNode
);
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
...
...
@@ -151,6 +193,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
ControlFlowNode
currentNode
=
new
ControlFlowNode
(
casesStatement
);
mappingOfNodes
.
put
(
casesStatement
,
currentNode
);
graph
.
addNode
(
currentNode
);
System
.
out
.
println
(
"\n"
+
currentNode
+
"\n"
);
graph
.
putEdgeValue
(
lastNode
,
currentNode
,
EdgeTypes
.
STEP_OVER
);
...
...
@@ -158,6 +201,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
List
<
CaseStatement
>
cases
=
casesStatement
.
getCases
();
for
(
CaseStatement
aCase
:
cases
)
{
ControlFlowNode
caseNode
=
new
ControlFlowNode
(
aCase
);
mappingOfNodes
.
put
(
aCase
,
caseNode
);
graph
.
addNode
(
caseNode
);
System
.
out
.
println
(
"\n"
+
caseNode
+
"\n"
);
graph
.
putEdgeValue
(
currentNode
,
caseNode
,
EdgeTypes
.
STEP_OVER
);
//??is this right?
...
...
src/main/java/edu/kit/formal/interpreter/ProofTreeController.java
View file @
a8e7207d
package
edu.kit.formal.interpreter
;
import
com.google.common.graph.MutableValueGraph
;
import
edu.kit.formal.gui.controller.PuppetMaster
;
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
;
/**
...
...
@@ -14,17 +13,18 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
public
class
ProofTreeController
{
/**
*
Visitor to retrieve state graph
*
To control stepping
*/
private
StateGraphVisitor
stateGraphVisitor
;
private
final
PuppetMaster
blocker
=
new
PuppetMaster
()
;
/**
*
ControlFlowGraph to lookup edges
*
Visitor to retrieve state graph
*/
private
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
controlFlowGraph
;
private
StateGraphVisitor
stateGraphVisitor
;
/**
* Graph that is computed on the fly in order to allow stepping
*/
private
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
stateGraph
;
private
ProgramFlowVisitor
controlFlowGraphVisitor
;
/**
* Current interpreter
*/
...
...
@@ -35,17 +35,15 @@ public class ProofTreeController {
private
PTreeNode
statePointer
;
public
ProofTreeController
(
Interpreter
<
KeyData
>
inter
,
ProofScript
mainScript
)
{
this
.
currentInterpreter
=
inter
;
blocker
.
deinstall
()
;
this
.
currentInterpreter
=
inter
;
buildControlFlowGraph
(
mainScript
);
this
.
stateGraphVisitor
=
new
StateGraphVisitor
(
inter
,
mainScript
,
this
.
controlFlowGraph
);
stateGraph
=
stateGraphVisitor
.
getStateGraph
();
this
.
stateGraphVisitor
=
new
StateGraphVisitor
(
inter
,
mainScript
,
controlFlowGraphVisitor
);
statePointer
=
stateGraphVisitor
.
getRootNode
();
// System.out.println(stateGraph.nodes());
//initializeStateGraph(mainScript);
blocker
.
getStepUntilBlock
().
set
(
1
);
blocker
.
install
(
currentInterpreter
);
}
/**
...
...
@@ -54,30 +52,26 @@ public class ProofTreeController {
* @param mainScript
*/
private
void
buildControlFlowGraph
(
ProofScript
mainScript
)
{
ProgramFlowVisitor
v
isitor
=
new
ProgramFlowVisitor
(
currentInterpreter
.
getFunctionLookup
());
mainScript
.
accept
(
v
isitor
);
this
.
controlFlowGraph
=
visitor
.
getGraph
();
System
.
out
.
println
(
v
isitor
.
asdot
());
this
.
controlFlowGraphV
isitor
=
new
ProgramFlowVisitor
(
currentInterpreter
.
getFunctionLookup
());
mainScript
.
accept
(
controlFlowGraphV
isitor
);
System
.
out
.
println
(
"CFG\n"
+
controlFlowGraphV
isitor
.
asdot
());
}
public
PTreeNode
stepOver
()
{
blocker
.
getStepUntilBlock
().
addAndGet
(
1
);
blocker
.
unlock
();
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
))
{
// 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());
//PTreeNode current = statePointer;
//ASTNode stmt = current.getScriptstmt();
//System.out.println("CurrentPointer: " + stmt.getNodeName() + "@" + stmt.getStartPosition());
return
null
;
}
...
...
src/main/java/edu/kit/formal/interpreter/StateGraphVisitor.java
View file @
a8e7207d
package
edu.kit.formal.interpreter
;
import
com.google.common.graph.EndpointPair
;
import
com.google.common.graph.MutableValueGraph
;
import
com.google.common.graph.ValueGraphBuilder
;
import
edu.kit.formal.proofscriptparser.DefaultASTVisitor
;
import
edu.kit.formal.proofscriptparser.ast.*
;
import
java.util.Set
;
/**
* Created by sarah on 6/26/17.
*/
public
class
StateGraphVisitor
extends
DefaultASTVisitor
<
Void
>
{
Interpreter
currentInterpreter
;
/**
* Interpreter
*/
private
Interpreter
currentInterpreter
;
/**
* Graph that is computed on the fly in order to allow stepping
*/
private
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
stateGraph
;
/**
* Root of state graph
*/
private
PTreeNode
root
;
/**
* last added node
*/
private
PTreeNode
lastNode
;
/**
*
C
ontrol
F
low
G
raph
*
Visitor for c
ontrol
f
low
g
raph
*/
private
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
graph
;
private
ProgramFlowVisitor
cfgVisitor
;
public
StateGraphVisitor
(
Interpreter
inter
,
ProofScript
mainScript
,
MutableValueGraph
<
ControlFlowNode
,
EdgeTypes
>
cfg
)
{
public
StateGraphVisitor
(
Interpreter
inter
,
ProofScript
mainScript
,
ProgramFlowVisitor
cfgVisitor
)
{
stateGraph
=
ValueGraphBuilder
.
directed
().
build
();
this
.
currentInterpreter
=
inter
;
graph
=
cfg
;
System
.
out
.
println
(
cfg
.
nodes
().
stream
().
toString
());
this
.
cfgVisitor
=
cfgVisitor
;
}
public
MutableValueGraph
<
PTreeNode
,
EdgeTypes
>
getStateGraph
()
{
return
stateGraph
;
}
...
...
@@ -47,16 +60,35 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
return
lastNode
;
}
//public (ControlFlowNode, ControlflowNode, Edge) getReturnEdge(ASTNode node)
//public Node findNode(ASTNode, state){}
/**
* Creat a new node for the state graph and add edges to already existing nodes
*
* @param node
* @return
*/
public
Void
createNewNode
(
ASTNode
node
)
{
PTreeNode
newStateNode
=
new
PTreeNode
(
node
);
newStateNode
.
setState
(
currentInterpreter
.
getCurrentState
());
stateGraph
.
addNode
(
newStateNode
);
Set
<
EndpointPair
<
ControlFlowNode
>>
targetEdges
=
cfgVisitor
.
getAllEdgesForNodeAsTarget
(
node
);
for
(
EndpointPair
<
ControlFlowNode
>
targetEdge
:
targetEdges
)
{
ControlFlowNode
cfn
=
targetEdge
.
source
();
ASTNode
assocNode
=
cfn
.
getScriptstmt
();
//mapping
}
if
(
lastNode
==
null
)
{
root
=
newStateNode
;
}
else
{
stateGraph
.
putEdgeValue
(
lastNode
,
newStateNode
,
EdgeTypes
.
STATE_FLOW
);
}
lastNode
=
newStateNode
;
return
null
;
...
...
@@ -134,4 +166,6 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
sb
.
append
(
"}"
);
return
sb
.
toString
();
}
}
src/test/resources/edu/kit/formal/interpreter/contraposition/recursion.kps
0 → 100644
View file @
a8e7207d
script t(){
f;
impRight;
}
script f(){
g;
}
script g(){
f;
}
\ No newline at end of file
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