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.

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

Extend loop normalization #705

Merged
merged 14 commits into from
Aug 3, 2024
Prev Previous commit
Next Next commit
Feedback implemented
hernanponcedeleon committed Aug 3, 2024
commit 81dbe60f0bfc0273f46351a5b337e857770c5623
Original file line number Diff line number Diff line change
@@ -2,6 +2,7 @@

import com.dat3m.dartagnan.expression.Expression;
import com.dat3m.dartagnan.expression.ExpressionFactory;
import com.dat3m.dartagnan.expression.type.IntegerType;
import com.dat3m.dartagnan.expression.type.TypeFactory;
import com.dat3m.dartagnan.program.Function;
import com.dat3m.dartagnan.program.Register;
@@ -118,55 +119,63 @@ private void guaranteeSingleUnconditionalBackjump(Function function) {
}

private void guaranteeSingleEntry(Function function) {
final IntegerType sourceRegType = types.getArchType();
int labelCounter = 0;
for (Label label : function.getEvents(Label.class)) {

final List<CondJump> backJumps = label.getJumpSet().stream()
.filter(j -> j.getLocalId() > label.getLocalId())
for (Label loopBegin : function.getEvents(Label.class)) {
final List<CondJump> backJumps = loopBegin.getJumpSet().stream()
.filter(j -> j.getLocalId() > loopBegin.getLocalId())
.sorted()
.toList();
if (backJumps.isEmpty()) {
continue;
}

int counter = 0;

final Label loopBegin = label;
final CondJump last = backJumps.get(backJumps.size() - 1);

final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", label, labelCounter), types.getArchType());
final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));
function.getEntry().insertAfter(initJumpedFromOutside);

final CondJump loopEnd = backJumps.get(backJumps.size() - 1);
final List<Label> loopBodyLabels = loopBegin.getSuccessor().getSuccessors().stream()
.takeWhile(ev -> ev != last)
.takeWhile(ev -> ev != loopEnd)
.filter(Label.class::isInstance).map(Label.class::cast)
.toList();

if(loopBodyLabels.stream().noneMatch(l -> hasExternalEntries(loopBegin, l))) {
continue;
}

for (Label l : loopBodyLabels) {
final List<CondJump> externalEntries = l.getJumpSet().stream()
.filter(j -> j.getLocalId() < loopBegin.getLocalId())
.toList();
final Register sourceReg = function.newRegister(String.format("__jumpedTo_%s#%s_From", loopBegin, labelCounter), sourceRegType);
final Local initJumpedFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(sourceRegType));
function.getEntry().insertAfter(initJumpedFromOutside);

for (CondJump fromOutside : externalEntries) {
counter++;
for (Label target : loopBodyLabels) {
final List<CondJump> externalEntries = getExternalEntries(loopBegin, target);
if(externalEntries.isEmpty()) {
continue;
}
counter++;

final Expression source = expressions.makeValue(BigInteger.valueOf(counter), types.getArchType());
final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
final Expression source = expressions.makeValue(BigInteger.valueOf(counter), sourceRegType);
final Local jumpingFrom = EventFactory.newLocal(sourceReg, source);
final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), target);
loopBegin.insertAfter(jumpToInternal);

for (CondJump fromOutside : externalEntries) {
fromOutside.updateReferences(Map.of(fromOutside.getLabel(), loopBegin));
fromOutside.getPredecessor().insertAfter(jumpingFrom);

final Label internalLabel = fromOutside.getLabel();
final CondJump jumpToInternal = EventFactory.newJump(expressions.makeEQ(sourceReg, source), internalLabel);
final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(types.getArchType()));

loopBegin.insertAfter(jumpToInternal);
last.getPredecessor().insertAfter(resetJumpFromOutside);
}

final Local resetJumpFromOutside = EventFactory.newLocal(sourceReg, expressions.makeZero(sourceRegType));
loopEnd.getPredecessor().insertAfter(resetJumpFromOutside);
}

labelCounter++;
}
}

private boolean hasExternalEntries(Label loopBegin, Label internal) {
return internal.getJumpSet().stream().anyMatch(j -> j.getLocalId() < loopBegin.getLocalId());
}

private List<CondJump> getExternalEntries(Label loopBegin, Label internal) {
return internal.getJumpSet().stream().filter(j -> j.getLocalId() < loopBegin.getLocalId()).toList();
}
}