projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
3e0a2fe
)
Fixing more bugs with the reachability analysis.
author
rtrimana
<rtrimana@uci.edu>
Wed, 15 Apr 2020 23:34:11 +0000
(16:34 -0700)
committer
rtrimana
<rtrimana@uci.edu>
Wed, 15 Apr 2020 23:34:11 +0000
(16:34 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
patch
|
blob
|
history
diff --git
a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 104af2bd9993dd0cabb776e3e793e1a2060ba2fa..26dd6bd0b274f2b4fc6e6b963f0176fc224ca545 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@
-404,10
+404,6
@@
public class DPORStateReducer extends ListenerAdapter {
// Store restorable state object for this state (always store the latest)
RestorableVMState restorableState = vm.getRestorableState();
restorableStateMap.put(stateId, restorableState);
// Store restorable state object for this state (always store the latest)
RestorableVMState restorableState = vm.getRestorableState();
restorableStateMap.put(stateId, restorableState);
- // Map multiple state IDs to a choice counter
- for (Integer stId : justVisitedStates) {
- stateToChoiceCounterMap.put(stId, choiceCounter);
- }
}
private Integer[] copyChoices(Integer[] choicesToCopy) {
}
private Integer[] copyChoices(Integer[] choicesToCopy) {
@@
-495,6
+491,7
@@
public class DPORStateReducer extends ListenerAdapter {
HashSet<Integer> eventSet = new HashSet<>();
stateToEventMap.put(stateId, eventSet);
}
HashSet<Integer> eventSet = new HashSet<>();
stateToEventMap.put(stateId, eventSet);
}
+ stateToChoiceCounterMap.put(stateId, choiceCounter);
analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
justVisitedStates.add(stateId);
currVisitedStates.add(stateId);
analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
justVisitedStates.add(stateId);
currVisitedStates.add(stateId);
@@
-588,6
+585,10
@@
public class DPORStateReducer extends ListenerAdapter {
if (currentCG instanceof IntIntervalGenerator) {
// This is the interval CG used in device handlers
ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
if (currentCG instanceof IntIntervalGenerator) {
// This is the interval CG used in device handlers
ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
+ // Iterate until we find the IntChoiceFromSet CG
+ while (!(parentCG instanceof IntChoiceFromSet)) {
+ parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
+ }
int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
// Find the index of the event/choice in refChoices
for (int i = 0; i<refChoices.length; i++) {
int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
// Find the index of the event/choice in refChoices
for (int i = 0; i<refChoices.length; i++) {
@@
-844,6
+845,9
@@
public class DPORStateReducer extends ListenerAdapter {
if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
currVisitedStates.contains(stateId) && (stateId > 0)) {
// Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
currVisitedStates.contains(stateId) && (stateId > 0)) {
// Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
+ if (stateToChoiceCounterMap.get(stateId) == null) {
+ System.out.println();
+ }
int conflictChoice = stateToChoiceCounterMap.get(stateId);
int currentChoice = choiceCounter - 1;
// Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
int conflictChoice = stateToChoiceCounterMap.get(stateId);
int currentChoice = choiceCounter - 1;
// Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)