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
affd4938
Commit
affd4938
authored
May 22, 2018
by
Lulu Luong
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Gutter + Underline SP
parent
f5cfd41e
Pipeline
#21922
failed with stages
in 2 minutes and 39 seconds
Changes
8
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
128 additions
and
28 deletions
+128
-28
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
...ava/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
+3
-1
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java
.../edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java
+2
-3
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
...edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+23
-8
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
...ormal/psdbg/gui/controller/InteractiveModeController.java
+15
-6
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
...ava/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
+50
-0
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
...u/kit/iti/formal/psdbg/gui/controls/ScriptController.java
+31
-3
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
...kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
+1
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java
...ain/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java
+3
-6
No files found.
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
View file @
affd4938
...
...
@@ -607,9 +607,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
va
.
declare
(
entry
.
getKey
(),
val
.
getType
());
va
.
assign
(
entry
.
getKey
(),
val
);
}
catch
(
NullPointerException
npe
)
{
System
.
out
.
println
(
"Caught Nullpointer in evaluation of Stateless parameters: "
+
entry
.
toString
()
);
Value
val
=
evaluator
.
eval
(
entry
.
getValue
());
va
.
declare
(
entry
.
getKey
(),
val
.
getType
());
va
.
assign
(
entry
.
getKey
(),
val
);
}
});
return
va
;
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java
View file @
affd4938
package
edu.kit.iti.formal.psdbg.interpreter.data
;
import
com.google.errorprone.annotations.Var
;
import
edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor
;
import
edu.kit.iti.formal.psdbg.parser.ast.*
;
import
lombok.AllArgsConstructor
;
...
...
@@ -16,7 +15,7 @@ public class SavePoint {
private
final
String
name
;
private
int
startOffset
=
-
1
;
private
int
endOffset
=
-
1
;
private
int
lineNumer
=
-
1
;
private
int
lineNum
b
er
=
-
1
;
private
ForceOption
force
=
ForceOption
.
YES
;
public
SavePoint
(
CallStatement
call
)
{
...
...
@@ -28,7 +27,7 @@ public class SavePoint {
try
{
startOffset
=
call
.
getRuleContext
().
getStart
().
getStartIndex
();
endOffset
=
call
.
getRuleContext
().
getStart
().
getStopIndex
();
lineNumer
=
call
.
getRuleContext
().
getStart
().
getLine
();
lineNum
b
er
=
call
.
getRuleContext
().
getStart
().
getLine
();
}
catch
(
NullPointerException
npe
)
{
}
}
else
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
affd4938
...
...
@@ -63,15 +63,13 @@ import org.dockfx.DockNode;
import
org.dockfx.DockPane
;
import
org.dockfx.DockPos
;
import
org.key_project.util.collection.ImmutableList
;
import
org.omg.CORBA.Environment
;
import
org.reactfx.util.FxTimer
;
import
org.reactfx.util.Timer
;
import
javax.annotation.Nullable
;
import
javax.swing.*
;
import
java.io.File
;
import
java.io.FileWriter
;
import
java.io.IOException
;
import
java.io.PrintWriter
;
import
java.io.*
;
import
java.net.URL
;
import
java.nio.charset.Charset
;
import
java.time.Duration
;
...
...
@@ -149,8 +147,6 @@ public class DebuggerMain implements Initializable {
private
ToggleButton
btnInteractiveMode
;
@FXML
private
Button
interactive_undo
;
//TODO: dir
private
File
dir
;
private
JavaArea
javaArea
=
new
JavaArea
();
private
DockNode
javaAreaDock
=
new
DockNode
(
javaArea
,
"Java Source"
,
...
...
@@ -262,7 +258,6 @@ public class DebuggerMain implements Initializable {
Events
.
register
(
this
);
// model.setDebugMode(false);
scriptController
=
new
ScriptController
(
dockStation
);
//TODO:
interactiveModeController
=
new
InteractiveModeController
(
scriptController
);
btnInteractiveMode
.
setSelected
(
false
);
inspectionViewsController
=
new
InspectionViewsController
(
dockStation
);
...
...
@@ -648,7 +643,9 @@ public class DebuggerMain implements Initializable {
LOGGER
.
debug
(
"MainScript: {}"
,
ms
.
getName
());
ib
.
setScripts
(
scripts
);
System
.
out
.
println
(
"ms = "
+
FACADE
.
getProof
().
getProofFile
());
interactiveModeController
.
setSavepoint
(
null
);
executeScript0
(
ib
,
breakpoints
,
ms
,
addInitBreakpoint
);
...
...
@@ -688,6 +685,7 @@ public class DebuggerMain implements Initializable {
ms
.
setBody
(
body
);
LOGGER
.
debug
(
"Parsed Scripts, found {}"
,
scripts
.
size
());
LOGGER
.
debug
(
"MainScript: {}"
,
ms
.
getName
());
//ib.setDirectory(model.getKeyFile() != null ? model.getKeyFile() : model.getJavaFile());
...
...
@@ -1237,6 +1235,7 @@ public class DebuggerMain implements Initializable {
@FXML
public
void
interactiveMode
(
ActionEvent
actionEvent
)
{
if
(
btnInteractiveMode
.
isSelected
())
{
assert
model
.
getDebuggerFramework
()
!=
null
;
interactiveModeController
.
setDebuggerFramework
(
model
.
getDebuggerFramework
());
...
...
@@ -1256,9 +1255,11 @@ public class DebuggerMain implements Initializable {
@FXML
public
void
selectSavepoint
(
ActionEvent
actionEvent
)
{
if
(
cboSavePoints
.
getValue
()
!=
null
)
{
stopDebugMode
(
actionEvent
);
SavePoint
selected
=
cboSavePoints
.
getValue
();
try
{
abortExecution
();
}
catch
(
Exception
e
)
{
...
...
@@ -1279,6 +1280,10 @@ public class DebuggerMain implements Initializable {
try
{
File
dir
=
FACADE
.
getFilepath
().
getAbsoluteFile
().
getParentFile
();
File
proofFile
=
selected
.
getProofFile
(
dir
);
if
(!
proofFile
.
isFile
())
{
throw
new
FileNotFoundException
();
}
FACADE
.
reload
(
proofFile
);
if
(
iModel
.
getGoals
().
size
()
>
0
)
{
iModel
.
setSelectedGoalNodeToShow
(
iModel
.
getGoals
().
get
(
0
));
...
...
@@ -1287,6 +1292,16 @@ public class DebuggerMain implements Initializable {
LOGGER
.
info
(
"Reloaded Successfully"
);
statusBar
.
publishMessage
(
"Reloaded Sucessfully"
);
}
interactiveModeController
.
setSavepoint
(
selected
);
scriptController
.
getMainScript
().
getScriptArea
().
setSavepointMarker
(
selected
.
getLineNumber
());
scriptController
.
getMainScript
().
getScriptArea
().
setStyleClass
(
selected
.
getStartOffset
(),
selected
.
getEndOffset
()
+
1
,
"problem"
);
//TODO: styleClass:underlinesave
}
catch
(
FileNotFoundException
e
){
Utils
.
showWarningDialog
(
"File doesn't exist"
,
"File does not exist"
,
"Proof file does not exist. Please execute the script first."
,
e
);
}
catch
(
ProofInputException
|
ProblemLoaderException
e
)
{
LOGGER
.
error
(
e
);
Utils
.
showExceptionDialog
(
"Loading Error"
,
"Could not clear Environment"
,
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
View file @
affd4938
...
...
@@ -9,7 +9,6 @@ import de.uka.ilkd.key.logic.SequentFormula;
import
de.uka.ilkd.key.macros.scripts.EngineState
;
import
de.uka.ilkd.key.macros.scripts.RuleCommand
;
import
de.uka.ilkd.key.macros.scripts.ScriptException
;
import
de.uka.ilkd.key.pp.LogicPrinter
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.proof.Proof
;
...
...
@@ -23,6 +22,7 @@ import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import
edu.kit.iti.formal.psdbg.interpreter.Evaluator
;
import
edu.kit.iti.formal.psdbg.interpreter.data.GoalNode
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
edu.kit.iti.formal.psdbg.interpreter.data.SavePoint
;
import
edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode
;
...
...
@@ -42,11 +42,9 @@ import org.apache.logging.log4j.Logger;
import
org.key_project.util.collection.ImmutableList
;
import
recoder.util.Debug
;
import
javax.annotation.Nullable
;
import
java.math.BigInteger
;
import
java.util.ArrayList
;
import
java.util.HashMap
;
import
java.util.List
;
import
java.util.Map
;
import
java.util.*
;
import
java.util.stream.Collectors
;
@Getter
...
...
@@ -77,6 +75,9 @@ public class InteractiveModeController {
private
CasesStatement
casesStatement
;
@Setter
@Nullable
private
SavePoint
savepoint
;
//not null if interactive mode started from savepoint
public
void
start
(
Proof
currentProof
,
InspectionModel
model
)
{
Events
.
register
(
this
);
cases
.
clear
();
...
...
@@ -148,7 +149,15 @@ public class InteractiveModeController {
Events
.
unregister
(
this
);
String
c
=
getCasesAsString
();
scriptController
.
getDockNode
(
scriptArea
).
undock
();
Events
.
fire
(
new
Events
.
InsertAtTheEndOfMainScript
(
c
));
if
(
savepoint
==
null
)
{
Events
.
fire
(
new
Events
.
InsertAtTheEndOfMainScript
(
c
));
}
else
{
//TODO: insert Script after Savepoint
System
.
out
.
println
(
"Interactive Script should be inserted in line "
+
savepoint
.
getLineNumber
());
Events
.
fire
(
new
Events
.
InsertAtTheEndOfMainScript
(
c
));
}
}
@Subscribe
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
View file @
affd4938
...
...
@@ -70,6 +70,8 @@ import org.reactfx.value.Val;
import
org.reactfx.value.Var
;
import
java.io.File
;
import
java.nio.file.Files
;
import
java.nio.file.LinkOption
;
import
java.time.Duration
;
import
java.util.*
;
import
java.util.function.BiConsumer
;
...
...
@@ -421,8 +423,25 @@ public class ScriptArea extends BorderPane {
gutter
.
lineAnnotations
.
forEach
(
a
->
a
.
setMainScript
(
false
));
if
(
lineNumber
>
0
)
gutter
.
getLineAnnotation
(
lineNumber
-
1
).
setMainScript
(
true
);
}
/**
* Set marker in gutter at the line of the Savepoint, which is loaded
* @param lineNumber line in where the marker is to be set
*/
public
void
setSavepointMarker
(
int
lineNumber
)
{
gutter
.
lineAnnotations
.
forEach
(
a
->
a
.
setSavepoint
(
false
));
gutter
.
getLineAnnotation
(
lineNumber
-
1
).
setSavepoint
(
true
);
}
private
void
underline
(
int
linenumber
)
{
}
private
boolean
hasExecutionMarker
()
{
return
getText
().
contains
(
EXECUTION_MARKER
);
}
...
...
@@ -1468,6 +1487,10 @@ public class ScriptArea extends BorderPane {
MaterialDesignIcon
.
CHECK
,
"12"
);
private
MaterialDesignIconView
iconSavepoint
=
new
MaterialDesignIconView
(
MaterialDesignIcon
.
CONTENT_SAVE
,
"12"
);
private
Label
lineNumber
=
new
Label
(
"not set"
);
public
GutterView
(
GutterAnnotation
ga
)
{
...
...
@@ -1476,6 +1499,7 @@ public class ScriptArea extends BorderPane {
old
.
breakpoint
.
removeListener
(
this
::
update
);
old
.
breakpoint
.
removeListener
(
this
::
update
);
old
.
mainScript
.
removeListener
(
this
::
update
);
old
.
savepoint
.
removeListener
(
this
::
update
);
lineNumber
.
textProperty
().
unbind
();
}
...
...
@@ -1483,6 +1507,7 @@ public class ScriptArea extends BorderPane {
nv
.
mainScript
.
addListener
(
this
::
update
);
nv
.
breakpoint
.
addListener
(
this
::
update
);
nv
.
conditional
.
addListener
(
this
::
update
);
nv
.
savepoint
.
addListener
(
this
::
update
);
lineNumber
.
textProperty
().
bind
(
nv
.
textProperty
());
...
...
@@ -1494,6 +1519,7 @@ public class ScriptArea extends BorderPane {
public
void
update
(
Observable
o
)
{
getChildren
().
setAll
(
lineNumber
);
if
(
getAnnotation
().
isMainScript
())
getChildren
().
add
(
iconMainScript
);
else
if
(
getAnnotation
().
isSavepoint
())
getChildren
().
add
(
iconSavepoint
);
else
addPlaceholder
();
if
(
getAnnotation
().
isBreakpoint
())
getChildren
().
add
(
getAnnotation
().
getConditional
()
...
...
@@ -1534,6 +1560,8 @@ public class ScriptArea extends BorderPane {
private
BooleanProperty
mainScript
=
new
SimpleBooleanProperty
();
private
SimpleBooleanProperty
savepoint
=
new
SimpleBooleanProperty
();
public
String
getText
()
{
return
text
.
get
();
}
...
...
@@ -1589,6 +1617,19 @@ public class ScriptArea extends BorderPane {
public
BooleanProperty
mainScriptProperty
()
{
return
mainScript
;
}
public
boolean
isSavepoint
()
{
return
savepoint
.
get
();
}
public
SimpleBooleanProperty
savepointProperty
()
{
return
savepoint
;
}
public
void
setSavepoint
(
boolean
savepoint
)
{
this
.
savepoint
.
set
(
savepoint
);
}
}
public
static
class
BreakpointDialog
extends
BorderPane
{
...
...
@@ -1707,6 +1748,13 @@ public class ScriptArea extends BorderPane {
@FXML
public
void
setMainScript
(
ActionEvent
event
)
{
LOGGER
.
debug
(
"ScriptAreaContextMenu.setMainScript"
);
// Check if script is saved
if
(!
filePath
.
getValue
().
isFile
())
{
Utils
.
showInfoDialog
(
"Saving Script"
,
"Save Script"
,
"Script has to be saved first before it can be executed."
);
return
;
}
List
<
ProofScript
>
ast
=
Facade
.
getAST
(
getText
());
int
pos
=
currentMouseOver
.
get
().
getInsertionIndex
();
ast
.
stream
().
filter
(
ps
->
...
...
@@ -1717,6 +1765,8 @@ public class ScriptArea extends BorderPane {
new
MainScriptIdentifier
(
filePath
.
get
().
getAbsolutePath
(),
proofScript
.
getStartPosition
().
getLineNumber
(),
proofScript
.
getName
(),
ScriptArea
.
this
)));
}
@FXML
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
View file @
affd4938
...
...
@@ -10,11 +10,10 @@ import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier;
import
edu.kit.iti.formal.psdbg.gui.controller.Events
;
import
edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier
;
import
edu.kit.iti.formal.psdbg.interpreter.data.SavePoint
;
import
edu.kit.iti.formal.psdbg.interpreter.data.State
;
import
edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint
;
import
edu.kit.iti.formal.psdbg.parser.Facade
;
import
edu.kit.iti.formal.psdbg.parser.ast.ASTNode
;
import
edu.kit.iti.formal.psdbg.parser.ast.CallStatement
;
import
edu.kit.iti.formal.psdbg.parser.ast.ProofScript
;
import
edu.kit.iti.formal.psdbg.parser.ast.*
;
import
javafx.beans.property.ListProperty
;
import
javafx.beans.property.ObjectProperty
;
import
javafx.beans.property.SimpleListProperty
;
...
...
@@ -93,6 +92,35 @@ public class ScriptController {
}
}
/*
public int getLineOfSavepoint(SavePoint sp) {
Optional<ProofScript> ms = getMainScript(). find(getCombinedAST());
if(ms.isPresent()) {
List<CallStatement> list = ms.get().getBody().stream()
.filter(SavePoint::isSaveCommand)
.map(a -> (CallStatement) a).
collect(Collectors.toList());
if(!list.isEmpty()) {
for(int i = 0; i < list.size(); i++) {
if(true) {
Parameters param = list.get(i).getParameters();
String splistname = ((StringLiteral) param.get(new Variable("#2"))).getText();
if(splistname.equals(sp.getName())) {
int index = ms.get().getBody().indexOf(list.get(i));
return ms.get().getBody().get(index).getStartPosition().getLineNumber();
}
}
}
}
}
return -1;
}
*/
private
void
addDefaultInlineActions
()
{
actionSuppliers
.
add
(
new
FindLabelInGoalList
());
actionSuppliers
.
add
(
new
FindTermLiteralInSequence
());
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
View file @
affd4938
...
...
@@ -51,7 +51,7 @@ public class SequentOptionsMenu extends ContextMenu {
}
catch
(
Exception
e
)
{
Utils
.
showInfoDialog
(
"Please Select a Goal first."
,
"Please Select a Goal node from the list first to open the SequentMatcher Window."
,
"Please Select a Goal node from the list first to open the SequentMatcher Window."
,
e
);
"Please Select a Goal node from the list first to open the SequentMatcher Window."
);
// e.printStackTrace();
// System.out.println(e);
}
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java
View file @
affd4938
...
...
@@ -211,7 +211,7 @@ public class Utils {
StringWriter
sw
=
new
StringWriter
();
PrintWriter
pw
=
new
PrintWriter
(
sw
);
ex
.
printStackTrace
(
pw
);
String
exceptionText
=
sw
.
toString
();
alert
.
setWidth
(
400
);
...
...
@@ -224,15 +224,12 @@ public class Utils {
alert
.
showAndWait
();
}
public
static
void
showInfoDialog
(
String
title
,
String
headerText
,
String
contentText
,
Throwable
ex
)
{
public
static
void
showInfoDialog
(
String
title
,
String
headerText
,
String
contentText
)
{
Alert
alert
=
new
Alert
(
Alert
.
AlertType
.
INFORMATION
);
alert
.
setTitle
(
title
);
alert
.
setHeaderText
(
headerText
);
alert
.
setContentText
(
contentText
);
StringWriter
sw
=
new
StringWriter
();
PrintWriter
pw
=
new
PrintWriter
(
sw
);
ex
.
printStackTrace
(
pw
);
String
exceptionText
=
sw
.
toString
();
alert
.
setWidth
(
400
);
...
...
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