Skip to content

Commit 1e74f09

Browse files
committed
added listener for top and bottom #334
1 parent aa4a18a commit 1e74f09

23 files changed

+449
-311
lines changed

lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/Analysis.java

Lines changed: 24 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ public AnalysisState<A> assign(
142142
state.getExecutionInformation()));
143143

144144
if (events != null)
145-
events.post(new AnalysisAssignEnd<>(state, res, id, value));
145+
events.post(new AnalysisAssignEnd<>(pp, state, res, id, value));
146146

147147
return res;
148148
}
@@ -191,7 +191,7 @@ public AnalysisState<A> assign(
191191
state.getExecutionInformation()));
192192

193193
if (events != null)
194-
events.post(new AnalysisAssignEnd<>(state, res, id, expression));
194+
events.post(new AnalysisAssignEnd<>(pp, state, res, id, expression));
195195

196196
return res;
197197
}
@@ -212,7 +212,7 @@ public AnalysisState<A> smallStepSemantics(
212212
state.getExecutionInformation()));
213213

214214
if (events != null)
215-
events.post(new AnalysisSmallStepEnd<>(state, res, expression));
215+
events.post(new AnalysisSmallStepEnd<>(pp, state, res, expression));
216216

217217
return res;
218218
}
@@ -238,7 +238,7 @@ public AnalysisState<A> assume(
238238
state.getExecutionInformation()));
239239

240240
if (events != null)
241-
events.post(new AnalysisAssumeEnd<>(state, res, expression));
241+
events.post(new AnalysisAssumeEnd<>(src, state, res, expression));
242242

243243
return res;
244244
}
@@ -255,7 +255,7 @@ public Satisfiability satisfies(
255255
Satisfiability sat = domain.satisfies(state.getExecutionState(), expression, pp);
256256

257257
if (events != null)
258-
events.post(new AnalysisSatisfiesEnd<>(state, sat, expression));
258+
events.post(new AnalysisSatisfiesEnd<>(pp, state, sat, expression));
259259

260260
return sat;
261261
}
@@ -476,14 +476,16 @@ public AnalysisState<A> makeLattice() {
476476
*
477477
* @param state the current analysis state
478478
* @param exception the exception to move the execution state to
479+
* @param pp the program point where the move happens
479480
*
480481
* @return the updated analysis state
481482
*
482483
* @throws SemanticException if something goes wrong during the computation
483484
*/
484485
public AnalysisState<A> moveExecutionToError(
485486
AnalysisState<A> state,
486-
Error exception)
487+
Error exception,
488+
ProgramPoint pp)
487489
throws SemanticException {
488490
if (state.isBottom() || state.getExecution().isBottom() || state.getExecutionState().isBottom())
489491
return state;
@@ -499,7 +501,7 @@ public AnalysisState<A> moveExecutionToError(
499501
result = result.addSmashedError(exception, state.getExecution());
500502

501503
if (events != null)
502-
events.post(new AnalysisExecToErrorEnd<>(state, result, exception));
504+
events.post(new AnalysisExecToErrorEnd<>(pp, state, result, exception));
503505

504506
return result;
505507
}
@@ -517,6 +519,7 @@ public AnalysisState<A> moveExecutionToError(
517519
* are removed from the resulting state.
518520
*
519521
* @param state the current analysis state
522+
* @param pp the program point where the move happens
520523
* @param protectedBlock the block that is being protected from the errors
521524
* to move
522525
* @param targets the types to move
@@ -530,6 +533,7 @@ public AnalysisState<A> moveExecutionToError(
530533
*/
531534
public AnalysisState<A> moveErrorsToExecution(
532535
AnalysisState<A> state,
536+
ProgramPoint pp,
533537
ProtectedBlock protectedBlock,
534538
Collection<Type> targets,
535539
Collection<Type> excluded,
@@ -589,7 +593,14 @@ public AnalysisState<A> moveErrorsToExecution(
589593
AnalysisState<A> bottom = state.bottom();
590594

591595
if (events != null)
592-
events.post(new AnalysisErrorsToExecEnd<>(state, bottom, protectedBlock, targets, excluded, variable));
596+
events.post(new AnalysisErrorsToExecEnd<>(
597+
pp,
598+
state,
599+
bottom,
600+
protectedBlock,
601+
targets,
602+
excluded,
603+
variable));
593604

594605
return bottom;
595606
}
@@ -623,7 +634,7 @@ public AnalysisState<A> moveErrorsToExecution(
623634
AnalysisState<A> res = state.removeAllErrors(false).withExecution(result);
624635

625636
if (events != null)
626-
events.post(new AnalysisErrorsToExecEnd<>(state, res, protectedBlock, targets, excluded, variable));
637+
events.post(new AnalysisErrorsToExecEnd<>(pp, state, res, protectedBlock, targets, excluded, variable));
627638

628639
return res;
629640
}
@@ -769,13 +780,15 @@ public AnalysisState<A> removeCaughtErrors(
769780
* exists for halting, it is merged with the current state.
770781
*
771782
* @param state the current analysis state
783+
* @param pp the program point where the move happens
772784
*
773785
* @return the updated analysis state
774786
*
775787
* @throws SemanticException if something goes wrong during the computation
776788
*/
777789
public AnalysisState<A> moveExecutionToHalting(
778-
AnalysisState<A> state)
790+
AnalysisState<A> state,
791+
ProgramPoint pp)
779792
throws SemanticException {
780793
if (state.isBottom() || state.getExecution().isBottom() || state.getExecutionState().isBottom())
781794
return state;
@@ -787,7 +800,7 @@ public AnalysisState<A> moveExecutionToHalting(
787800
AnalysisState<A> res = state.bottomExecution().withHalt(halt);
788801

789802
if (events != null)
790-
events.post(new AnalysisExecToHaltEnd<>(state, res));
803+
events.post(new AnalysisExecToHaltEnd<>(pp, state, res));
791804

792805
return res;
793806
}

0 commit comments

Comments
 (0)