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

Allow bounds to be saved to and loaded from files #759

Merged
merged 14 commits into from
Oct 27, 2024
Merged

Allow bounds to be saved to and loaded from files #759

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
2674fc0
Initial support for bounds dumping
hernanponcedeleon Oct 19, 2024
e17b936
Dump source code location with context to bounds file
hernanponcedeleon Oct 20, 2024
a9c8286
Cleanup
hernanponcedeleon Oct 20, 2024
7d3e133
Use option to set bounds path
hernanponcedeleon Oct 20, 2024
5831551
Create bounds file if missing
hernanponcedeleon Oct 21, 2024
2dbe50b
Add bound.save option
hernanponcedeleon Oct 21, 2024
546d558
Fix null pointer exception
hernanponcedeleon Oct 22, 2024
536873b
Cleaned up code and simplified it.
ThomasHaas Oct 25, 2024
c875e5c
Fixed wrong update to bounds file
ThomasHaas Oct 25, 2024
78969e5
Fixed issue when specifying same file for loading and storing bounds.
ThomasHaas Oct 25, 2024
b88bd72
Fix appending rather than clearing the bounds file.
ThomasHaas Oct 25, 2024
bf1d312
Log warning when there are problems with bounds file
hernanponcedeleon Oct 26, 2024
cc4c408
Log warning when there are problems to read bounds file
hernanponcedeleon Oct 26, 2024
dbdc065
Remove getBoundsFile()
hernanponcedeleon Oct 27, 2024
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
Prev Previous commit
Next Next commit
Cleanup 
Signed-off-by: Hernan Ponce de Leon <zeta96@gmail.com>
  • Loading branch information
@hernanponcedeleon
hernanponcedeleon committed Oct 20, 2024
commit a9c8286838094c41845d1ef3b4d67e6dc0991c1e
43 changes: 34 additions & 9 deletions dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,9 @@
import com.google.common.collect.ImmutableSet;
import com.google.common.io.CharSource;

import scala.collection.mutable.UnrolledBuffer.Unrolled;

import org.apache.commons.csv.CSVFormat;
import org.apache.commons.csv.CSVPrinter;
import org.apache.commons.csv.CSVRecord;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.apache.maven.model.io.xpp3.MavenXpp3Reader;
Expand All @@ -58,6 +59,8 @@
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.Reader;
import java.io.Writer;
import java.math.BigInteger;
import java.nio.file.Path;
import java.util.*;
Expand Down Expand Up @@ -347,7 +350,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
.append("\t")
.append(synContext.getSourceLocationWithContext(ev, true))
.append("\n");
increaseBoundAndDumpToFile(ev);
increaseBoundAndDump(ev);
}
}
summary.append("=================================================\n");
Expand Down Expand Up @@ -405,12 +408,34 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm
return summary.toString();
}

private static void increaseBoundAndDumpToFile(Event ev) {
try (FileWriter writer = new FileWriter(GlobalSettings.getBoundsFile(), true)) {
final SyntacticContextAnalysis synContext = newInstance(ev.getThread().getProgram());
writer.append(String.valueOf(ev.getMetadata(UnrollingId.class).value())).append(',')
.append(String.valueOf(ev.getMetadata(UnrollingBound.class).value() + 1)).append(',')
.append(synContext.getSourceLocationWithContext(ev, false)).append('\n');
private static void increaseBoundAndDump(Event ev) {

String evId = String.valueOf(ev.getMetadata(UnrollingId.class).value());
String incBound = String.valueOf(ev.getMetadata(UnrollingBound.class).value() + 1);

// We read from and write to the same CSV file,
// thus we need to split this in two loops
List<String[]> modifiedRecords = new ArrayList<>();
try (Reader reader = new FileReader(GlobalSettings.getBoundsFile())) {
for (CSVRecord record : CSVFormat.DEFAULT.parse(reader)) {
String nextId = record.get(0);
String nextBound = record.get(1);
String sourceLoc = record.get(2);
if (nextId.equals(evId)) {
nextBound = incBound;
}
modifiedRecords.add(new String[] { nextId, nextBound, sourceLoc });
}
} catch (IOException e) {
e.printStackTrace();
}

try (Writer writer = new FileWriter(GlobalSettings.getBoundsFile(), false);
CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) {
for (String[] record : modifiedRecords) {
csvPrinter.printRecord(record[0], record[1], record[2]);
}
csvPrinter.flush();
} catch (IOException e) {
e.printStackTrace();
}
Expand Down
45 changes: 29 additions & 16 deletions dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,17 @@
import org.apache.logging.log4j.Logger;
import org.sosy_lab.common.configuration.*;
import org.apache.commons.csv.CSVFormat;
import org.apache.commons.csv.CSVPrinter;
import org.apache.commons.csv.CSVRecord;

import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.Reader;
import java.io.Writer;
import java.util.*;
import java.util.function.Predicate;

import static com.dat3m.dartagnan.configuration.OptionNames.BOUND;

@Options
Expand Down Expand Up @@ -106,16 +110,16 @@ private void unrollLoopsInFunction(Function func, int defaultBound) {
}

private Map<CondJump, Integer> loadLoopBoundsMapFromFile(Function func) {

Map<CondJump, Integer> loopBoundsMapFromFile = new HashMap<>();
try (Reader reader = new FileReader(GlobalSettings.getBoundsFile())) {
Iterable<CSVRecord> records = CSVFormat.DEFAULT.parse(reader);
for (CSVRecord record : records) {
int evId = Integer.parseInt(record.get(0));
int bound = Integer.parseInt(record.get(1));
if(func.getEvents(CondJump.class).stream().anyMatch(e -> e.getGlobalId() == evId)) {
CondJump loop = func.getEvents(CondJump.class).stream().filter(e -> e.getGlobalId() == evId).findAny().get();
loopBoundsMapFromFile.put(loop, bound);
int nexId = Integer.parseInt(record.get(0));
int nextBound = Integer.parseInt(record.get(1));
Predicate<Event> predicate = e -> e.getGlobalId() == nexId;
if(func.getEvents(CondJump.class).stream().anyMatch(predicate)) {
CondJump loop = func.getEvents(CondJump.class).stream().filter(predicate).findAny().get();
loopBoundsMapFromFile.put(loop, nextBound);
}
}
} catch (IOException e) {
Expand All @@ -125,7 +129,6 @@ private Map<CondJump, Integer> loadLoopBoundsMapFromFile(Function func) {
}

private Map<CondJump, Integer> computeLoopBoundsMap(Function func, int defaultBound) {

LoopBound curBoundAnnotation = null;
final Map<CondJump, Integer> loopBoundsMap = new HashMap<>();
for (Event event : func.getEvents()) {
Expand Down Expand Up @@ -158,7 +161,7 @@ private void unrollLoop(CondJump loopBackJump, int bound) {
Preconditions.checkArgument(loopBegin.getLocalId() < loopBackJump.getLocalId(),
"The jump does not belong to a loop.");

dumpBoundToFile(loopBackJump, bound);
dumpBoundIfMissing(loopBackJump, bound);
int iterCounter = 0;
while (++iterCounter <= bound) {
if (iterCounter == bound) {
Expand Down Expand Up @@ -227,14 +230,24 @@ private Event newBoundEvent(Function func) {
return boundEvent;
}

private void dumpBoundToFile(Event jump, int bound) {
try (FileWriter writer = new FileWriter(GlobalSettings.getBoundsFile(), true)) {
final SyntacticContextAnalysis synContext = SyntacticContextAnalysis
.newInstance(jump.getFunction().getProgram());
writer.append(String.valueOf(jump.getGlobalId())).append(',')
.append(String.valueOf(bound)).append(',')
.append(synContext.getSourceLocationWithContext(jump, false))
.append('\n');
private void dumpBoundIfMissing(Event jump, Integer bound) {
String evId = String.valueOf(jump.getMetadata(UnrollingId.class).value());
final SyntacticContextAnalysis synContext = SyntacticContextAnalysis.newInstance(jump.getFunction().getProgram());
String sourceLoc = synContext.getSourceLocationWithContext(jump, false);
try (Reader reader = new FileReader(GlobalSettings.getBoundsFile());
Writer writer = new FileWriter(GlobalSettings.getBoundsFile(), true);
CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) {
boolean found = false;
for (CSVRecord record : CSVFormat.DEFAULT.parse(reader)) {
String nextId = record.get(0);
if (found = nextId.equals(evId)) {
break;
}
}
if (!found) {
csvPrinter.printRecord(evId, bound.toString(), sourceLoc);
}
csvPrinter.flush();
} catch (IOException e) {
e.printStackTrace();
}
Expand Down