Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix SyntacticContextAnalysis #653

Merged
merged 1 commit into from
Apr 18, 2024
Merged

Fix SyntacticContextAnalysis #653

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 20 additions & 25 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@
import com.google.common.collect.Iterables;

import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Stack;
import java.util.function.Predicate;
Expand Down Expand Up @@ -100,9 +99,6 @@ public String toString() {
}
}

// We use this enum to track loop nesting
private enum LoopMarkerTypes {START, INC, END}

// ============================================================================

private final Map<Event, Info> infoMap = new HashMap<>();
Expand Down Expand Up @@ -138,7 +134,7 @@ private void run(Program program) {
}

private void run(Thread thread, LoopAnalysis loops) {
final Map<Event, LoopMarkerTypes> loopMarkerTypesMap = getLoopMarkerTypesMap(thread, loops);
final Map<Event, LoopAnalysis.LoopIterationInfo> loopMarkerTypesMap = getLoopMarkerTypesMap(thread, loops);

Stack<Context> curContextStack = new Stack<>();
curContextStack.push(new ThreadContext(thread));
Expand All @@ -161,32 +157,31 @@ private void run(Thread thread, LoopAnalysis loops) {
} while (!topCallCtx.funCallMarker.getFunctionName().equals(retMarker.getFunctionName()));
}

if (loopMarkerTypesMap.containsKey(ev)) {
switch (loopMarkerTypesMap.get(ev)) {
case START -> curContextStack.push(new LoopContext(ev, 1));
case INC -> {
assert curContextStack.peek() instanceof LoopContext;
int iterNum = ((LoopContext) curContextStack.pop()).iterationNumber;
curContextStack.push(new LoopContext(ev, iterNum + 1));
}
case END -> {
assert curContextStack.peek() instanceof LoopContext;
curContextStack.pop();
}
final LoopAnalysis.LoopIterationInfo iteration = loopMarkerTypesMap.get(ev);
if (iteration != null) {
final boolean start = ev == iteration.getIterationStart();
final boolean end = ev == iteration.getIterationEnd();
assert start || end;
if (start) {
curContextStack.push(new LoopContext(ev, iteration.getIterationNumber()));
}
if (end) {
assert curContextStack.peek() instanceof LoopContext c &&
c.loopMarker == iteration.getIterationStart() &&
c.iterationNumber == iteration.getIterationNumber();
curContextStack.pop();
}
}
}
}

private Map<Event, LoopMarkerTypes> getLoopMarkerTypesMap(Thread thread, LoopAnalysis loopAnalysis) {
final Map<Event, LoopMarkerTypes> loopMarkerTypesMap = new HashMap<>();
private Map<Event, LoopAnalysis.LoopIterationInfo> getLoopMarkerTypesMap(Thread thread, LoopAnalysis loopAnalysis) {
final Map<Event, LoopAnalysis.LoopIterationInfo> loopMarkerTypesMap = new HashMap<>();
for (LoopAnalysis.LoopInfo loop : loopAnalysis.getLoopsOfFunction(thread)) {
final List<LoopAnalysis.LoopIterationInfo> iterations = loop.iterations();

loopMarkerTypesMap.put(iterations.get(0).getIterationStart(), LoopMarkerTypes.START);
iterations.subList(1, iterations.size())
.forEach(iter -> loopMarkerTypesMap.put(iter.getIterationStart(), LoopMarkerTypes.INC));
loopMarkerTypesMap.put(iterations.get(iterations.size() - 1).getIterationEnd(), LoopMarkerTypes.END);
for (LoopAnalysis.LoopIterationInfo iteration : loop.iterations()) {
loopMarkerTypesMap.put(iteration.getIterationStart(), iteration);
loopMarkerTypesMap.put(iteration.getIterationEnd(), iteration);
}
}
return loopMarkerTypesMap;
}
Expand Down
Loading