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
0abbf1e7
Commit
0abbf1e7
authored
Jun 04, 2017
by
Alexander Weigl
Browse files
first running debugger
parent
5e6b1ed9
Pipeline
#10941
passed with stage
in 2 minutes and 21 seconds
Changes
10
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
0abbf1e7
...
...
@@ -5,12 +5,14 @@ import de.uka.ilkd.key.pp.ProgramPrinter;
import
de.uka.ilkd.key.speclang.Contract
;
import
edu.kit.formal.gui.controls.JavaArea
;
import
edu.kit.formal.gui.controls.ScriptArea
;
import
edu.kit.formal.gui.controls.SequentView
;
import
edu.kit.formal.gui.model.RootModel
;
import
edu.kit.formal.interpreter.KeYProofFacade
;
import
edu.kit.formal.interpreter.data.GoalNode
;
import
edu.kit.formal.interpreter.data.KeyData
;
import
edu.kit.formal.interpreter.dbg.Debugger
;
import
javafx.beans.Observable
;
import
javafx.beans.property.SimpleBooleanProperty
;
import
javafx.collections.SetChangeListener
;
import
javafx.concurrent.Service
;
import
javafx.concurrent.Task
;
import
javafx.event.ActionEvent
;
...
...
@@ -21,7 +23,6 @@ import javafx.scene.layout.GridPane;
import
javafx.scene.layout.Pane
;
import
javafx.scene.layout.Priority
;
import
javafx.stage.FileChooser
;
import
lombok.Setter
;
import
org.apache.commons.io.FileUtils
;
import
org.controlsfx.dialog.Wizard
;
...
...
@@ -79,7 +80,7 @@ public class DebuggerMainWindowController implements Initializable {
* GoalView
* **********************************************************************************************************/
@FXML
private
ListView
goalView
;
private
ListView
<
GoalNode
<
KeyData
>>
goalView
;
private
ExecutorService
executorService
=
null
;
private
KeYProofFacade
facade
;
private
Wizard
contractChooserDialog
=
new
Wizard
();
...
...
@@ -98,14 +99,16 @@ public class DebuggerMainWindowController implements Initializable {
@FXML
private
Label
lblFilename
;
@Setter
private
Debugger
debugger
;
private
final
PuppetMaster
blocker
=
new
PuppetMaster
();
private
File
initialDirectory
;
@FXML
private
JavaArea
javaSourceCode
;
@FXML
private
SequentView
sequentView
;
/**
* @param location
...
...
@@ -136,30 +139,64 @@ public class DebuggerMainWindowController implements Initializable {
e
.
printStackTrace
();
}
javaSourceCode
.
insertText
(
0
,
writer
.
toString
());
});
//debug
javaSourceCode
.
getMarkedLines
().
add
(
2
);
javaSourceCode
.
getMarkedLines
().
add
(
3
);
scriptArea
.
getMarkedLines
().
addListener
(
new
SetChangeListener
<
Integer
>()
{
@Override
public
void
onChanged
(
Change
<?
extends
Integer
>
change
)
{
blocker
.
getBreakpoints
().
clear
();
blocker
.
getBreakpoints
().
addAll
(
change
.
getSet
());
}
});
blocker
.
currentGoalsProperty
().
addListener
((
o
,
old
,
fresh
)
->
{
model
.
currentGoalNodesProperty
().
setAll
(
fresh
);
});
model
.
currentSelectedGoalNodeProperty
().
bind
(
blocker
.
currentSelectedGoalProperty
());
goalView
.
itemsProperty
().
bind
(
model
.
currentGoalNodesProperty
());
model
.
currentSelectedGoalNodeProperty
().
addListener
((
p
,
old
,
fresh
)
->
{
goalView
.
getSelectionModel
().
select
(
fresh
);
/* TODO get lines of active statements marked lines
javaSourceCode.getMarkedLines().clear();
javaSourceCode.getMarkedLines().addAll(
);*/
});
goalView
.
getSelectionModel
().
selectedItemProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
{
sequentView
.
setNode
(
newValue
.
getData
().
getNode
());
});
goalView
.
setCellFactory
(
GoalNodeListCell:
:
new
);
}
//region Actions: Execution
@FXML
public
void
executeScript
()
{
buttonStartInterpreter
.
setText
(
"Interpreting..."
);
startDebugMode
.
setDisable
(
true
);
facade
.
executeScript
(
scriptArea
.
getText
());
List
<
GoalNode
<
KeyData
>>
g
=
model
.
getCurrentState
().
getGoals
();
this
.
model
.
getCurrentGoalNodes
().
addAll
(
g
);
buttonStartInterpreter
.
setText
(
"execute Script"
);
executeScript
(
false
);
}
@FXML
public
void
executeInDebugMode
()
{
setDebugMode
(
true
);
executeScript
();
executeScript
(
true
);
}
private
void
executeScript
(
boolean
debugMode
)
{
this
.
debugMode
.
set
(
debugMode
);
lblStatusMessage
.
setText
(
"Interpreting..."
);
blocker
.
deinstall
(
facade
.
getInterpreter
());
if
(
debugMode
)
{
blocker
.
getStepUntilBlock
().
set
(
1
);
blocker
.
install
(
facade
.
getInterpreter
());
}
facade
.
executeScript
(
scriptArea
.
getText
());
List
<
GoalNode
<
KeyData
>>
g
=
model
.
getCurrentState
().
getGoals
();
this
.
model
.
getCurrentGoalNodes
().
addAll
(
g
);
lblStatusMessage
.
setText
(
"Script executed"
);
}
//endregion
...
...
@@ -317,7 +354,7 @@ public class DebuggerMainWindowController implements Initializable {
fileChooser
.
setTitle
(
title
);
fileChooser
.
setSelectedExtensionFilter
(
new
FileChooser
.
ExtensionFilter
(
description
,
fileEndings
));
if
(
initialDirectory
==
null
)
initialDirectory
=
new
File
(
"src/test/resources/edu/kit/formal/"
);
initialDirectory
=
new
File
(
"src/test/resources/edu/kit/formal/
interpreter/contraposition/
"
);
if
(!
initialDirectory
.
exists
())
initialDirectory
=
new
File
(
"."
);
...
...
@@ -326,6 +363,11 @@ public class DebuggerMainWindowController implements Initializable {
return
fileChooser
;
}
public
void
stepOver
(
ActionEvent
actionEvent
)
{
blocker
.
getStepUntilBlock
().
addAndGet
(
1
);
blocker
.
unlock
();
}
public
class
ContractLoaderService
extends
Service
<
List
<
Contract
>>
{
@Override
protected
Task
<
List
<
Contract
>>
createTask
()
{
...
...
@@ -386,5 +428,21 @@ public class DebuggerMainWindowController implements Initializable {
public
void
setDebugMode
(
boolean
debugMode
)
{
this
.
debugMode
.
set
(
debugMode
);
}
private
class
GoalNodeListCell
extends
ListCell
<
GoalNode
<
KeyData
>>
{
public
GoalNodeListCell
(
ListView
<
GoalNode
<
KeyData
>>
goalNodeListView
)
{
itemProperty
().
addListener
(
this
::
update
);
}
private
void
update
(
Observable
observable
)
{
if
(
getItem
()
==
null
)
{
setText
(
""
);
return
;
}
KeyData
item
=
getItem
().
getData
();
setText
(
item
.
getNode
().
name
());
}
}
//endregion
}
src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java
0 → 100644
View file @
0abbf1e7
package
edu.kit.formal.gui.controller
;
import
edu.kit.formal.interpreter.Interpreter
;
import
edu.kit.formal.interpreter.data.GoalNode
;
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.Visitor
;
import
edu.kit.formal.proofscriptparser.ast.*
;
import
javafx.application.Platform
;
import
javafx.beans.property.SimpleObjectProperty
;
import
java.util.List
;
import
java.util.Set
;
import
java.util.concurrent.ConcurrentSkipListSet
;
import
java.util.concurrent.atomic.AtomicInteger
;
import
java.util.concurrent.locks.Condition
;
import
java.util.concurrent.locks.Lock
;
import
java.util.concurrent.locks.ReentrantLock
;
/**
* Created by weigl on 21.05.2017.
*/
public
class
PuppetMaster
{
private
Interpreter
<
KeyData
>
puppet
;
private
AtomicInteger
stepUntilBlock
=
new
AtomicInteger
(-
1
);
private
Set
<
Integer
>
brkpnts
=
new
ConcurrentSkipListSet
<>();
private
final
Lock
lock
=
new
ReentrantLock
();
private
final
Condition
block
=
lock
.
newCondition
();
private
final
SimpleObjectProperty
<
List
<
GoalNode
<
KeyData
>>>
currentGoals
=
new
SimpleObjectProperty
<>();
private
final
SimpleObjectProperty
<
GoalNode
<
KeyData
>>
currentSelectedGoal
=
new
SimpleObjectProperty
<>();
private
Visitor
<
Void
>
entryListener
=
new
EntryListener
();
private
Visitor
<
Void
>
exitListener
=
new
ExitListener
();
public
PuppetMaster
()
{
}
public
PuppetMaster
(
Interpreter
<
KeyData
>
inter
)
{
install
(
puppet
);
}
public
void
install
(
Interpreter
<
KeyData
>
interpreter
)
{
if
(
puppet
!=
null
)
deinstall
(
puppet
);
interpreter
.
getEntryListeners
().
add
(
entryListener
);
interpreter
.
getEntryListeners
().
add
(
exitListener
);
puppet
=
interpreter
;
}
public
void
deinstall
(
Interpreter
<
KeyData
>
interpreter
)
{
interpreter
.
getEntryListeners
().
remove
(
entryListener
);
interpreter
.
getEntryListeners
().
remove
(
exitListener
);
}
public
Void
checkForHalt
(
ASTNode
node
)
{
if
(
stepUntilBlock
.
get
()
>
0
)
stepUntilBlock
.
decrementAndGet
();
if
(
stepUntilBlock
.
get
()
==
0
)
{
publishState
();
block
();
}
int
lineNumber
=
node
.
getStartPosition
().
getLineNumber
();
if
(
brkpnts
.
contains
(
lineNumber
))
{
publishState
();
block
();
}
return
null
;
}
private
void
publishState
()
{
System
.
out
.
println
(
"PuppetMaster.publishState"
);
final
State
<
KeyData
>
state
=
puppet
.
getCurrentState
().
copy
();
Platform
.
runLater
(()
->
{
currentGoals
.
set
(
state
.
getGoals
());
currentSelectedGoal
.
set
(
state
.
getSelectedGoalNode
());
});
}
/**
* Blocks the current thread. Makes him awakable on {@code block}.
*/
private
void
block
()
{
try
{
lock
.
lock
();
block
.
await
();
}
catch
(
InterruptedException
e
)
{
e
.
printStackTrace
();
}
finally
{
lock
.
unlock
();
}
}
public
void
addBreakpoint
(
int
i
)
{
brkpnts
.
add
(
i
);
}
public
void
unlock
()
{
try
{
lock
.
lock
();
block
.
signal
();
}
finally
{
lock
.
unlock
();
}
}
public
GoalNode
<
KeyData
>
getCurrentSelectedGoal
()
{
return
currentSelectedGoal
.
get
();
}
public
SimpleObjectProperty
<
GoalNode
<
KeyData
>>
currentSelectedGoalProperty
()
{
return
currentSelectedGoal
;
}
public
void
setCurrentSelectedGoal
(
GoalNode
<
KeyData
>
currentSelectedGoal
)
{
this
.
currentSelectedGoal
.
set
(
currentSelectedGoal
);
}
public
List
<
GoalNode
<
KeyData
>>
getCurrentGoals
()
{
return
currentGoals
.
get
();
}
public
SimpleObjectProperty
<
List
<
GoalNode
<
KeyData
>>>
currentGoalsProperty
()
{
return
currentGoals
;
}
public
void
setCurrentGoals
(
List
<
GoalNode
<
KeyData
>>
currentGoals
)
{
this
.
currentGoals
.
set
(
currentGoals
);
}
public
Set
<
Integer
>
getBreakpoints
()
{
return
brkpnts
;
}
public
AtomicInteger
getStepUntilBlock
()
{
return
stepUntilBlock
;
}
private
class
EntryListener
extends
DefaultASTVisitor
<
Void
>
{
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
return
checkForHalt
(
proofScript
);
}
@Override
public
Void
visit
(
AssignmentStatement
assignment
)
{
return
checkForHalt
(
assignment
);
}
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
return
checkForHalt
(
casesStatement
);
}
@Override
public
Void
visit
(
CaseStatement
caseStatement
)
{
return
checkForHalt
(
caseStatement
);
}
@Override
public
Void
visit
(
CallStatement
call
)
{
return
checkForHalt
(
call
);
}
@Override
public
Void
visit
(
TheOnlyStatement
theOnly
)
{
return
checkForHalt
(
theOnly
);
}
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
return
checkForHalt
(
foreach
);
}
@Override
public
Void
visit
(
RepeatStatement
repeatStatement
)
{
return
checkForHalt
(
repeatStatement
);
}
}
private
class
ExitListener
extends
DefaultASTVisitor
<
Void
>
{
}
}
src/main/java/edu/kit/formal/gui/controls/ScriptArea.java
View file @
0abbf1e7
...
...
@@ -70,6 +70,14 @@ public class ScriptArea extends CodeArea {
}).subscribe(s -> setStyleSpans(0, s));*/
}
public
ObservableSet
<
Integer
>
getMarkedLines
()
{
return
markedLines
;
}
public
void
setMarkedLines
(
ObservableSet
<
Integer
>
markedLines
)
{
this
.
markedLines
=
markedLines
;
}
private
void
highlightProblems
()
{
LinterStrategy
ls
=
LinterStrategy
.
getDefaultLinter
();
List
<
LintProblem
>
pl
=
ls
.
check
(
Facade
.
getAST
(
CharStreams
.
fromString
(
getText
())));
...
...
src/main/java/edu/kit/formal/gui/controls/SequentView.java
View file @
0abbf1e7
package
edu.kit.formal.gui.controls
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.NamespaceSet
;
import
de.uka.ilkd.key.logic.Sequent
;
import
de.uka.ilkd.key.pp.IdentitySequentPrintFilter
;
import
de.uka.ilkd.key.pp.LogicPrinter
;
import
de.uka.ilkd.key.pp.NotationInfo
;
import
de.uka.ilkd.key.pp.ProgramPrinter
;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.settings.ProofIndependentSettings
;
import
javafx.beans.Observable
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.scene.input.MouseEvent
;
import
org.fxmisc.richtext.CodeArea
;
import
java.io.StringWriter
;
/**
* @author Alexander Weigl
* @version 1 (03.06.17)
*/
public
class
SequentView
extends
CodeArea
{
private
LogicPrinter
lp
;
private
IdentitySequentPrintFilter
filter
;
private
LogicPrinter
.
PosTableStringBackend
backend
;
private
SimpleObjectProperty
<
de
.
uka
.
ilkd
.
key
.
proof
.
Node
>
node
=
new
SimpleObjectProperty
<>();
public
SequentView
()
{
setEditable
(
false
);
node
.
addListener
(
this
::
update
);
setOnMouseMoved
(
this
::
hightlight
);
}
private
void
hightlight
(
MouseEvent
mouseEvent
)
{
double
x
=
mouseEvent
.
getX
();
double
y
=
mouseEvent
.
getY
();
/*
TextAreaSkin skin = (TextAreaSkin) getSkin();
int insertionPoint = skin.getInsertionPoint(x, y);
PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
if (pis != null) {
System.out.println(pis);
Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength());
selectRange(r.start(), r.end());
} else {
selectRange(0, 0);
}
mouseEvent.consume();
*/
}
public
void
update
(
Observable
o
)
{
Services
services
=
node
.
get
().
proof
().
getEnv
().
getServicesForEnvironment
();
NamespaceSet
nss
=
services
.
getNamespaces
();
Sequent
sequent
=
node
.
get
().
sequent
();
filter
=
new
IdentitySequentPrintFilter
(
sequent
);
ProgramPrinter
prgPrinter
=
new
ProgramPrinter
(
new
StringWriter
());
this
.
backend
=
new
LogicPrinter
.
PosTableStringBackend
(
80
);
ProofIndependentSettings
.
DEFAULT_INSTANCE
.
getViewSettings
().
setUseUnicode
(
true
);
ProofIndependentSettings
.
DEFAULT_INSTANCE
.
getViewSettings
().
setUsePretty
(
true
);
NotationInfo
.
DEFAULT_UNICODE_ENABLED
=
true
;
NotationInfo
.
DEFAULT_PRETTY_SYNTAX
=
true
;
NotationInfo
notation
=
new
NotationInfo
();
notation
.
refresh
(
services
,
true
,
true
);
lp
=
new
LogicPrinter
(
prgPrinter
,
notation
,
backend
,
services
,
false
);
lp
.
printSequent
(
sequent
);
clear
();
insertText
(
0
,
backend
.
getString
());
}
public
Node
getNode
()
{
return
node
.
get
();
}
public
SimpleObjectProperty
<
Node
>
nodeProperty
()
{
return
node
;
}
public
void
setNode
(
Node
node
)
{
this
.
node
.
set
(
node
);
}
}
src/main/java/edu/kit/formal/interpreter/Interpreter.java
View file @
0abbf1e7
...
...
@@ -437,7 +437,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
public
State
<
T
>
getCurrentState
()
{
return
stateStack
.
peek
();
try
{
return
stateStack
.
peek
();
}
catch
(
EmptyStackException
e
)
{
return
new
State
<
T
>(
null
);
//FIXME
}
}
public
State
<
T
>
newState
(
List
<
GoalNode
<
T
>>
goals
,
GoalNode
<
T
>
selected
)
{
...
...
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
View file @
0abbf1e7
...
...
@@ -14,6 +14,7 @@ import edu.kit.formal.interpreter.data.KeyData;
import
edu.kit.formal.interpreter.data.State
;
import
edu.kit.formal.interpreter.exceptions.InterpreterRuntimeException
;
import
edu.kit.formal.proofscriptparser.Facade
;
import
edu.kit.formal.proofscriptparser.ast.ProofScript
;
import
lombok.Getter
;
import
java.io.File
;
...
...
@@ -47,14 +48,8 @@ public class KeYProofFacade {
currentRoot
=
pa
.
getFirstOpenGoal
();
KeyData
keyData
=
new
KeyData
(
currentRoot
.
getProofNode
(),
pa
.
getEnv
(),
pa
.
getProof
());
try
{
interpreter
.
interpret
(
Facade
.
getAST
(
currentScriptText
),
new
GoalNode
<>(
null
,
keyData
));
return
interpreter
.
getCurrentState
();
}
catch
(
IOException
e
)
{
e
.
printStackTrace
();
}
return
null
;
interpreter
.
interpret
(
Facade
.
getAST
(
currentScriptText
),
new
GoalNode
<>(
null
,
keyData
));
return
interpreter
.
getCurrentState
();
}
public
void
prepareEnvWithKeYFile
(
File
keYFile
)
{
...
...
@@ -110,22 +105,20 @@ public class KeYProofFacade {
*
* @param
*/
public
voi
d
executeScript
(
String
scriptText
)
throws
InterpreterRuntimeException
{
public
Threa
d
executeScript
(
String
scriptText
)
throws
InterpreterRuntimeException
{
if
(
interpreter
==
null
)
{
throw
new
InterpreterRuntimeException
(
"No interpreter created"
);
}
ProjectedNode
root
=
pa
.
getFirstOpenGoal
();
KeyData
keyData
=
new
KeyData
(
root
.
getProofNode
(),
pa
.
getEnv
(),
pa
.
getProof
());
try
{
interpreter
.
interpret
(
Facade
.
getAST
(
scriptText
),
new
GoalNode
<>(
null
,
keyData
));
this
.
model
.
setCurrentState
(
interpreter
.
getCurrentState
());
}
catch
(
IOException
e
)
{
e
.
printStackTrace
();
}
List
<
ProofScript
>
ast
=
Facade
.
getAST
(
scriptText
);
Thread
t
=
new
Thread
(()
->
{
interpreter
.
interpret
(
ast
,
new
GoalNode
<>(
null
,
keyData
));
});
this
.
model
.
setCurrentState
(
interpreter
.
getCurrentState
());
t
.
start
();
return
t
;
}
public
Services
getService
()
{
...
...
src/main/java/edu/kit/formal/interpreter/data/State.java
View file @
0abbf1e7
...
...
@@ -74,7 +74,7 @@ public class State<T> {
* @return
*/
public
State
<
T
>
copy
()
{
List
<
GoalNode
<
T
>>
copiedGoals
=
new
ArrayList
<>();
List
<
GoalNode
<
T
>>
copiedGoals
=
new
ArrayList
<>(
goals
);
GoalNode
<
T
>
refToSelGoal
=
selectedGoalNode
;
return
new
State
<
T
>(
copiedGoals
,
refToSelGoal
);
}
...
...
src/main/java/edu/kit/formal/proofscriptparser/Facade.java
View file @
0abbf1e7
...
...
@@ -86,7 +86,7 @@ public abstract class Facade {
return
getAST
(
CharStreams
.
fromPath
(
inputfile
.
toPath
()));
}
public
static
List
<
ProofScript
>
getAST
(
String
input
)
throws
IOException
{
public
static
List
<
ProofScript
>
getAST
(
String
input
)
{
return
getAST
(
CharStreams
.
fromString
(
input
));
}
...
...
src/main/resources/DebuggerMain.fxml
View file @
0abbf1e7
...
...
@@ -43,7 +43,8 @@
</graphic>
</Button>
<Button
disable=
"${! controller.debugMode}"
>
<Button
onAction=
"#stepOver"
disable=
"${! controller.debugMode}"
>
<graphic>
<MaterialDesignIconView
glyphName=
"DEBUG_STEP_OVER"
size=
"24.0"
/>
</graphic>
...
...
src/test/java/edu/kit/formal/interpreter/InterpreterTest.java
View file @
0abbf1e7
...
...
@@ -59,7 +59,7 @@ public class InterpreterTest {
@Test
public
void
testSimple2
()
throws
IOException
{
// Interpreter inter = execute(getClass().getResourceAsStream("testSimple2.txt"));
// Assert.assertSame(0, ((BigInteger) inter.getCurrent
State
().getGoals().get(0).getAssignments().lookupVarValue("j").getData()).intValue());
// Assert.assertSame(0, ((BigInteger) inter.getCurrent
Goals
().getGoals().get(0).getAssignments().lookupVarValue("j").getData()).intValue());
}
@Test
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel