From 2674fc0c5c9e2bd9127eec6077c92a3a6a53a920 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sun, 20 Oct 2024 04:09:09 +0800 Subject: [PATCH 01/14] Initial support for bounds dumping Signed-off-by: Hernan Ponce de Leon --- dartagnan/pom.xml | 7 ++- .../java/com/dat3m/dartagnan/Dartagnan.java | 16 +++++++ .../com/dat3m/dartagnan/GlobalSettings.java | 4 ++ .../event/metadata/UnrollingBound.java | 3 ++ .../program/processing/LoopUnrolling.java | 46 +++++++++++++++++-- pom.xml | 2 + 6 files changed, 74 insertions(+), 4 deletions(-) create mode 100644 dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/UnrollingBound.java diff --git a/dartagnan/pom.xml b/dartagnan/pom.xml index 50aa8ad175..63b113485b 100644 --- a/dartagnan/pom.xml +++ b/dartagnan/pom.xml @@ -45,7 +45,12 @@ org.apache.maven maven-model - 3.3.9 + ${maven-model.version} + + + org.apache.commons + commons-csv + ${commons-csv.version} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 780e2cfe73..4e8b153a73 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -16,6 +16,8 @@ import com.dat3m.dartagnan.program.event.core.Assert; import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.metadata.UnrollingBound; +import com.dat3m.dartagnan.program.event.metadata.UnrollingId; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.utils.options.BaseOptions; @@ -34,6 +36,9 @@ import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableSet; import com.google.common.io.CharSource; + +import scala.collection.mutable.UnrolledBuffer.Unrolled; + import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.apache.maven.model.io.xpp3.MavenXpp3Reader; @@ -51,6 +56,7 @@ import java.io.File; import java.io.FileReader; +import java.io.FileWriter; import java.io.IOException; import java.math.BigInteger; import java.nio.file.Path; @@ -341,6 +347,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm .append("\t") .append(synContext.getSourceLocationWithContext(ev, true)) .append("\n"); + increaseBoundAndDumpToFile(ev); } } summary.append("=================================================\n"); @@ -398,6 +405,15 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm return summary.toString(); } + private static void increaseBoundAndDumpToFile(Event ev) { + try (FileWriter writer = new FileWriter(GlobalSettings.getBoundsFile(), true)) { + writer.append(String.valueOf(ev.getMetadata(UnrollingId.class).value())).append(',') + .append(String.valueOf(ev.getMetadata(UnrollingBound.class).value() + 1)).append('\n'); + } catch (IOException e) { + e.printStackTrace(); + } + } + private static void printWarningIfThreadStartFailed(Program p, EncodingContext encoder, ProverEnvironment prover) throws SolverException { for (Event e : p.getThreadEvents()) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java index 80c3d43a9b..36e4cc160a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java @@ -38,6 +38,10 @@ public static String getCatDirectory() { return env + "/cat"; } + public static String getBoundsFile() { + return getOutputDirectory() + "/bounds.csv"; + } + public static String getOrCreateOutputDirectory() throws IOException { String path = getOutputDirectory(); Files.createDirectories(Paths.get(path)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/UnrollingBound.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/UnrollingBound.java new file mode 100644 index 0000000000..8c0ba81e82 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/UnrollingBound.java @@ -0,0 +1,3 @@ +package com.dat3m.dartagnan.program.event.metadata; + +public record UnrollingBound(int value) implements Metadata { } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 293f15f489..d55aa8dec7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.program.processing; +import com.dat3m.dartagnan.GlobalSettings; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; @@ -11,14 +12,20 @@ import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.lang.svcomp.LoopBound; +import com.dat3m.dartagnan.program.event.metadata.UnrollingBound; import com.dat3m.dartagnan.program.event.metadata.UnrollingId; import com.google.common.base.Preconditions; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.*; +import org.apache.commons.csv.CSVFormat; +import org.apache.commons.csv.CSVRecord; +import java.io.FileReader; +import java.io.FileWriter; +import java.io.IOException; +import java.io.Reader; import java.util.*; - import static com.dat3m.dartagnan.configuration.OptionNames.BOUND; @Options @@ -89,9 +96,31 @@ private void unrollLoopsInFunction(Function func, int defaultBound) { return; } final Map loopBoundsMap = computeLoopBoundsMap(func, defaultBound); + final Map loopBoundsMapFromFile = loadLoopBoundsMapFromFile(func); + Map mergedBounds = new HashMap<>(loopBoundsMap); + loopBoundsMapFromFile.forEach((key, value) -> mergedBounds.merge(key, value, Math::max)); func.getEvents(CondJump.class).stream() - .filter(loopBoundsMap::containsKey) - .forEach(j -> unrollLoop(j, loopBoundsMap.get(j))); + .filter(mergedBounds::containsKey) + .forEach(j -> unrollLoop(j, mergedBounds.get(j))); + } + + private Map loadLoopBoundsMapFromFile(Function func) { + + Map loopBoundsMapFromFile = new HashMap<>(); + try (Reader reader = new FileReader(GlobalSettings.getBoundsFile())) { + Iterable 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); + } + } + } catch (IOException e) { + e.printStackTrace(); + } + return loopBoundsMapFromFile; } private Map computeLoopBoundsMap(Function func, int defaultBound) { @@ -128,6 +157,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); int iterCounter = 0; while (++iterCounter <= bound) { if (iterCounter == bound) { @@ -146,6 +176,7 @@ private void unrollLoop(CondJump loopBackJump, int bound) { boundEvent.getPredecessor().insertAfter(endOfLoopMarker); boundEvent.copyAllMetadataFrom(loopBackJump); + boundEvent.setMetadata(new UnrollingBound(bound)); endOfLoopMarker.copyAllMetadataFrom(loopBackJump); } else { @@ -195,4 +226,13 @@ private Event newBoundEvent(Function func) { return boundEvent; } + private void dumpBoundToFile(Event jump, int bound) { + System.out.println("Dumping " + jump.getGlobalId() + " with value " + bound); + try (FileWriter writer = new FileWriter(GlobalSettings.getBoundsFile(), true)) { + writer.append(String.valueOf(jump.getGlobalId())).append(',').append(String.valueOf(bound)).append('\n'); + } catch (IOException e) { + e.printStackTrace(); + } + } + } \ No newline at end of file diff --git a/pom.xml b/pom.xml index 4776af4439..4b6665d857 100644 --- a/pom.xml +++ b/pom.xml @@ -47,6 +47,8 @@ 32.1.2-jre 4.13.2 2.23.0 + 3.3.9 + 1.12.0 5.11.0 3.3.4 From e17b9366f4685a5587230bea7a970c07deca99a1 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 21 Oct 2024 01:42:48 +0800 Subject: [PATCH 02/14] Dump source code location with context to bounds file Signed-off-by: Hernan Ponce de Leon --- .../src/main/java/com/dat3m/dartagnan/Dartagnan.java | 4 +++- .../dartagnan/program/processing/LoopUnrolling.java | 9 +++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 4e8b153a73..d2cdacd90e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -407,8 +407,10 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm 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('\n'); + .append(String.valueOf(ev.getMetadata(UnrollingBound.class).value() + 1)).append(',') + .append(synContext.getSourceLocationWithContext(ev, false)).append('\n'); } catch (IOException e) { e.printStackTrace(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index d55aa8dec7..f24a2f6e8b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -5,6 +5,7 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.EventUser; @@ -227,9 +228,13 @@ private Event newBoundEvent(Function func) { } private void dumpBoundToFile(Event jump, int bound) { - System.out.println("Dumping " + jump.getGlobalId() + " with value " + bound); try (FileWriter writer = new FileWriter(GlobalSettings.getBoundsFile(), true)) { - writer.append(String.valueOf(jump.getGlobalId())).append(',').append(String.valueOf(bound)).append('\n'); + 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'); } catch (IOException e) { e.printStackTrace(); } From a9c8286838094c41845d1ef3b4d67e6dc0991c1e Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 21 Oct 2024 04:44:28 +0800 Subject: [PATCH 03/14] Cleanup Signed-off-by: Hernan Ponce de Leon --- .../java/com/dat3m/dartagnan/Dartagnan.java | 43 ++++++++++++++---- .../program/processing/LoopUnrolling.java | 45 ++++++++++++------- 2 files changed, 63 insertions(+), 25 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index d2cdacd90e..39789164c6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -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; @@ -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.*; @@ -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"); @@ -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 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(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index f24a2f6e8b..83c57494cf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -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 @@ -106,16 +110,16 @@ private void unrollLoopsInFunction(Function func, int defaultBound) { } private Map loadLoopBoundsMapFromFile(Function func) { - Map loopBoundsMapFromFile = new HashMap<>(); try (Reader reader = new FileReader(GlobalSettings.getBoundsFile())) { Iterable 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 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) { @@ -125,7 +129,6 @@ private Map loadLoopBoundsMapFromFile(Function func) { } private Map computeLoopBoundsMap(Function func, int defaultBound) { - LoopBound curBoundAnnotation = null; final Map loopBoundsMap = new HashMap<>(); for (Event event : func.getEvents()) { @@ -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) { @@ -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(); } From 7d3e1337bbf42d20102862a8bfdf096ca2c95b4b Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 21 Oct 2024 04:50:01 +0800 Subject: [PATCH 04/14] Use option to set bounds path Signed-off-by: Hernan Ponce de Leon --- .../dartagnan/configuration/OptionNames.java | 1 + .../program/processing/LoopUnrolling.java | 15 +++++++++++---- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index db9a0a0a52..c1c451da26 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -5,6 +5,7 @@ public class OptionNames { // Base Options public static final String PROPERTY = "property"; public static final String BOUND = "bound"; + public static final String BOUNDS_LOAD_PATH = "bound.load"; public static final String TARGET = "target"; public static final String METHOD = "method"; public static final String SOLVER = "solver"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 83c57494cf..07aef7f9c7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -31,7 +31,7 @@ import java.util.*; import java.util.function.Predicate; -import static com.dat3m.dartagnan.configuration.OptionNames.BOUND; +import static com.dat3m.dartagnan.configuration.OptionNames.*; @Options public class LoopUnrolling implements ProgramProcessor { @@ -57,6 +57,11 @@ public void setUnrollingBound(int bound) { this.bound = bound; } + @Option(name = BOUNDS_LOAD_PATH, + description = "Path to the CSV file containing loop bounds.", + secure = true) + private String bounds_load_path = ""; + // ===================================================================== private LoopUnrolling() { } @@ -101,9 +106,11 @@ private void unrollLoopsInFunction(Function func, int defaultBound) { return; } final Map loopBoundsMap = computeLoopBoundsMap(func, defaultBound); - final Map loopBoundsMapFromFile = loadLoopBoundsMapFromFile(func); Map mergedBounds = new HashMap<>(loopBoundsMap); - loopBoundsMapFromFile.forEach((key, value) -> mergedBounds.merge(key, value, Math::max)); + if(!bounds_load_path.isEmpty()) { + final Map loopBoundsMapFromFile = loadLoopBoundsMapFromFile(func); + loopBoundsMapFromFile.forEach((key, value) -> mergedBounds.merge(key, value, Math::max)); + } func.getEvents(CondJump.class).stream() .filter(mergedBounds::containsKey) .forEach(j -> unrollLoop(j, mergedBounds.get(j))); @@ -111,7 +118,7 @@ private void unrollLoopsInFunction(Function func, int defaultBound) { private Map loadLoopBoundsMapFromFile(Function func) { Map loopBoundsMapFromFile = new HashMap<>(); - try (Reader reader = new FileReader(GlobalSettings.getBoundsFile())) { + try (Reader reader = new FileReader(bounds_load_path)) { Iterable records = CSVFormat.DEFAULT.parse(reader); for (CSVRecord record : records) { int nexId = Integer.parseInt(record.get(0)); From 5831551cd58e21186a7b18c38ba412ddd63b8490 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 21 Oct 2024 16:29:23 +0800 Subject: [PATCH 05/14] Create bounds file if missing Signed-off-by: Hernan Ponce de Leon --- .../program/processing/LoopUnrolling.java | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 07aef7f9c7..3b55aa4768 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -23,6 +23,7 @@ import org.apache.commons.csv.CSVPrinter; import org.apache.commons.csv.CSVRecord; +import java.io.File; import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; @@ -86,6 +87,7 @@ public void run(Program program) { logger.warn("Skipped unrolling: Program is already unrolled."); return; } + createBoundsFileIfMissing(); final int defaultBound = this.bound; program.getFunctions().forEach(this::run); program.getThreads().forEach(this::run); @@ -95,7 +97,6 @@ public void run(Program program) { logger.info("Program unrolled {} times", defaultBound); } - private void run(Function function) { function.getEvents().forEach(e -> e.setMetadata(new UnrollingId(e.getGlobalId()))); // Track ids before unrolling unrollLoopsInFunction(function, bound); @@ -237,6 +238,17 @@ private Event newBoundEvent(Function func) { return boundEvent; } + private void createBoundsFileIfMissing() { + File file = new File(GlobalSettings.getBoundsFile()); + if (!file.exists()) { + try { + file.createNewFile(); + } catch (IOException e) { + e.printStackTrace(); + } + } + } + private void dumpBoundIfMissing(Event jump, Integer bound) { String evId = String.valueOf(jump.getMetadata(UnrollingId.class).value()); final SyntacticContextAnalysis synContext = SyntacticContextAnalysis.newInstance(jump.getFunction().getProgram()); From 2dbe50ba08ca23a60c6ee2ad0fe7199fb5e9f01f Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 22 Oct 2024 03:12:50 +0800 Subject: [PATCH 06/14] Add bound.save option Signed-off-by: Hernan Ponce de Leon --- .../src/main/java/com/dat3m/dartagnan/Dartagnan.java | 11 +++++++---- .../dat3m/dartagnan/configuration/OptionNames.java | 1 + .../dartagnan/program/processing/LoopUnrolling.java | 11 ++++++++--- 3 files changed, 16 insertions(+), 7 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 39789164c6..350d6defe6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -67,6 +67,7 @@ import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory; import static com.dat3m.dartagnan.configuration.OptionInfo.collectOptions; +import static com.dat3m.dartagnan.configuration.OptionNames.BOUNDS_SAVE_PATH; import static com.dat3m.dartagnan.configuration.OptionNames.PHANTOM_REFERENCES; import static com.dat3m.dartagnan.configuration.OptionNames.TARGET; import static com.dat3m.dartagnan.configuration.Property.*; @@ -350,7 +351,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm .append("\t") .append(synContext.getSourceLocationWithContext(ev, true)) .append("\n"); - increaseBoundAndDump(ev); + increaseBoundAndDump(ev, task.getConfig()); } } summary.append("=================================================\n"); @@ -408,7 +409,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm return summary.toString(); } - private static void increaseBoundAndDump(Event ev) { + private static void increaseBoundAndDump(Event ev, Configuration config) { String evId = String.valueOf(ev.getMetadata(UnrollingId.class).value()); String incBound = String.valueOf(ev.getMetadata(UnrollingBound.class).value() + 1); @@ -416,7 +417,9 @@ private static void increaseBoundAndDump(Event ev) { // We read from and write to the same CSV file, // thus we need to split this in two loops List modifiedRecords = new ArrayList<>(); - try (Reader reader = new FileReader(GlobalSettings.getBoundsFile())) { + // We read the file written by the LoopUnrolling pass, + // thus we use BOUNDS_SAVE_PATH also for the reader + try (Reader reader = new FileReader(config.getProperty(BOUNDS_SAVE_PATH))) { for (CSVRecord record : CSVFormat.DEFAULT.parse(reader)) { String nextId = record.get(0); String nextBound = record.get(1); @@ -430,7 +433,7 @@ private static void increaseBoundAndDump(Event ev) { e.printStackTrace(); } - try (Writer writer = new FileWriter(GlobalSettings.getBoundsFile(), false); + try (Writer writer = new FileWriter(config.getProperty(BOUNDS_SAVE_PATH), false); CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) { for (String[] record : modifiedRecords) { csvPrinter.printRecord(record[0], record[1], record[2]); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index c1c451da26..20e39a44a5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -6,6 +6,7 @@ public class OptionNames { public static final String PROPERTY = "property"; public static final String BOUND = "bound"; public static final String BOUNDS_LOAD_PATH = "bound.load"; + public static final String BOUNDS_SAVE_PATH = "bound.save"; public static final String TARGET = "target"; public static final String METHOD = "method"; public static final String SOLVER = "solver"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 3b55aa4768..ae200e5475 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -63,6 +63,11 @@ public void setUnrollingBound(int bound) { secure = true) private String bounds_load_path = ""; + @Option(name = BOUNDS_SAVE_PATH, + description = "Path to the CSV file to save loop bounds.", + secure = true) + private String bounds_save_path = GlobalSettings.getBoundsFile(); + // ===================================================================== private LoopUnrolling() { } @@ -239,7 +244,7 @@ private Event newBoundEvent(Function func) { } private void createBoundsFileIfMissing() { - File file = new File(GlobalSettings.getBoundsFile()); + File file = new File(bounds_save_path); if (!file.exists()) { try { file.createNewFile(); @@ -253,8 +258,8 @@ 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); + try (Reader reader = new FileReader(bounds_load_path); + Writer writer = new FileWriter(bounds_save_path, true); CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) { boolean found = false; for (CSVRecord record : CSVFormat.DEFAULT.parse(reader)) { From 546d5581535606599e022a08f9e47140aba6ad20 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 22 Oct 2024 16:14:05 +0800 Subject: [PATCH 07/14] Fix null pointer exception Signed-off-by: Hernan Ponce de Leon --- .../src/main/java/com/dat3m/dartagnan/Dartagnan.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 350d6defe6..ed9edb159a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -419,7 +419,9 @@ private static void increaseBoundAndDump(Event ev, Configuration config) { List modifiedRecords = new ArrayList<>(); // We read the file written by the LoopUnrolling pass, // thus we use BOUNDS_SAVE_PATH also for the reader - try (Reader reader = new FileReader(config.getProperty(BOUNDS_SAVE_PATH))) { + try (Reader reader = new FileReader(config.hasProperty(BOUNDS_SAVE_PATH) ? + config.getProperty(BOUNDS_SAVE_PATH) : + GlobalSettings.getBoundsFile())) { for (CSVRecord record : CSVFormat.DEFAULT.parse(reader)) { String nextId = record.get(0); String nextBound = record.get(1); @@ -433,7 +435,9 @@ private static void increaseBoundAndDump(Event ev, Configuration config) { e.printStackTrace(); } - try (Writer writer = new FileWriter(config.getProperty(BOUNDS_SAVE_PATH), false); + try (Writer writer = new FileWriter(config.hasProperty(BOUNDS_SAVE_PATH) ? + config.getProperty(BOUNDS_SAVE_PATH) : + GlobalSettings.getBoundsFile(), false); CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) { for (String[] record : modifiedRecords) { csvPrinter.printRecord(record[0], record[1], record[2]); From 536873b9978a9ed8002c818077386cc4ae876c71 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 25 Oct 2024 10:37:41 +0200 Subject: [PATCH 08/14] Cleaned up code and simplified it. --- .../java/com/dat3m/dartagnan/Dartagnan.java | 97 +++++------ .../program/processing/LoopUnrolling.java | 152 ++++++++++-------- 2 files changed, 137 insertions(+), 112 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index ed9edb159a..5864ccc77a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -16,8 +16,7 @@ import com.dat3m.dartagnan.program.event.core.Assert; import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Load; -import com.dat3m.dartagnan.program.event.metadata.UnrollingBound; -import com.dat3m.dartagnan.program.event.metadata.UnrollingId; +import com.dat3m.dartagnan.program.processing.LoopUnrolling; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.Utils; import com.dat3m.dartagnan.utils.options.BaseOptions; @@ -36,8 +35,8 @@ import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableSet; import com.google.common.io.CharSource; - import org.apache.commons.csv.CSVFormat; +import org.apache.commons.csv.CSVParser; import org.apache.commons.csv.CSVPrinter; import org.apache.commons.csv.CSVRecord; import org.apache.logging.log4j.LogManager; @@ -59,17 +58,13 @@ 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.*; import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory; import static com.dat3m.dartagnan.configuration.OptionInfo.collectOptions; -import static com.dat3m.dartagnan.configuration.OptionNames.BOUNDS_SAVE_PATH; -import static com.dat3m.dartagnan.configuration.OptionNames.PHANTOM_REFERENCES; -import static com.dat3m.dartagnan.configuration.OptionNames.TARGET; +import static com.dat3m.dartagnan.configuration.OptionNames.*; import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis.*; import static com.dat3m.dartagnan.utils.GitInfo.*; @@ -343,18 +338,26 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm } } else if (result == UNKNOWN && modelChecker.hasModel()) { // We reached unrolling bounds. - summary.append("=========== Not fully unrolled loops ============\n"); + final List reachedBounds = new ArrayList<>(); for (Event ev : p.getThreadEventsWithAllTags(Tag.BOUND)) { - final boolean isReached = TRUE.equals(model.evaluate(encCtx.execution(ev))); - if (isReached) { - summary - .append("\t") - .append(synContext.getSourceLocationWithContext(ev, true)) - .append("\n"); - increaseBoundAndDump(ev, task.getConfig()); + if (TRUE.equals(model.evaluate(encCtx.execution(ev)))) { + reachedBounds.add(ev); } } + summary.append("=========== Not fully unrolled loops ============\n"); + for (Event bound : reachedBounds) { + summary + .append("\t") + .append(synContext.getSourceLocationWithContext(bound, true)) + .append("\n"); + } summary.append("=================================================\n"); + + try { + increaseBoundAndDump(reachedBounds, task.getConfig()); + } catch (IOException e) { + e.printStackTrace(); + } } summary.append(result).append("\n"); } else { @@ -409,42 +412,40 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm return summary.toString(); } - private static void increaseBoundAndDump(Event ev, Configuration config) { - - 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 modifiedRecords = new ArrayList<>(); - // We read the file written by the LoopUnrolling pass, - // thus we use BOUNDS_SAVE_PATH also for the reader - try (Reader reader = new FileReader(config.hasProperty(BOUNDS_SAVE_PATH) ? - config.getProperty(BOUNDS_SAVE_PATH) : - 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(); + private static void increaseBoundAndDump(List boundEvents, Configuration config) throws IOException { + final File boundsFile = new File(config.hasProperty(BOUNDS_SAVE_PATH) ? + config.getProperty(BOUNDS_SAVE_PATH) : + GlobalSettings.getBoundsFile()); + + // Parse old entries + final List entries; + try (CSVParser parser = CSVParser.parse(new FileReader(boundsFile), CSVFormat.DEFAULT)) { + entries = parser.getRecords(); } - try (Writer writer = new FileWriter(config.hasProperty(BOUNDS_SAVE_PATH) ? - config.getProperty(BOUNDS_SAVE_PATH) : - GlobalSettings.getBoundsFile(), false); - CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) { - for (String[] record : modifiedRecords) { - csvPrinter.printRecord(record[0], record[1], record[2]); + // Compute update for entries + final Map loopId2UpdatedBound = new HashMap<>(); + for (Event e : boundEvents) { + assert e instanceof CondJump; + final CondJump loopJump = (CondJump) e; + final int loopId = LoopUnrolling.getPersistentLoopId(loopJump); + final int bound = LoopUnrolling.getUnrollingBoundAnnotation(loopJump); + loopId2UpdatedBound.put(loopId, bound + 1); + } + + // Write new entries + try (CSVPrinter csvPrinter = new CSVPrinter(new FileWriter(boundsFile, false), CSVFormat.DEFAULT)) { + for (CSVRecord entry : entries) { + final int entryId = Integer.parseInt(entry.get(0)); + if (!loopId2UpdatedBound.containsKey(entryId)) { + csvPrinter.printRecord(entry); + } else { + final String[] content = entry.values(); + content[0] = String.valueOf(loopId2UpdatedBound.get(entryId)); + csvPrinter.printRecord(Arrays.asList(content)); + } } csvPrinter.flush(); - } catch (IOException e) { - e.printStackTrace(); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index ae200e5475..84222a6c66 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -16,21 +16,17 @@ import com.dat3m.dartagnan.program.event.metadata.UnrollingBound; import com.dat3m.dartagnan.program.event.metadata.UnrollingId; import com.google.common.base.Preconditions; -import org.apache.logging.log4j.LogManager; -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 org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.sosy_lab.common.configuration.*; -import java.io.File; -import java.io.FileReader; -import java.io.FileWriter; -import java.io.IOException; -import java.io.Reader; -import java.io.Writer; +import java.io.*; +import java.nio.file.Files; +import java.nio.file.Path; import java.util.*; -import java.util.function.Predicate; import static com.dat3m.dartagnan.configuration.OptionNames.*; @@ -52,7 +48,10 @@ public class LoopUnrolling implements ProgramProcessor { @IntegerOption(min = 1) private int bound = 1; - public int getUnrollingBound() { return bound; } + public int getUnrollingBound() { + return bound; + } + public void setUnrollingBound(int bound) { Preconditions.checkArgument(bound >= 1, "The unrolling bound must be positive."); this.bound = bound; @@ -61,16 +60,17 @@ public void setUnrollingBound(int bound) { @Option(name = BOUNDS_LOAD_PATH, description = "Path to the CSV file containing loop bounds.", secure = true) - private String bounds_load_path = ""; + private String boundsLoadPath = ""; @Option(name = BOUNDS_SAVE_PATH, description = "Path to the CSV file to save loop bounds.", secure = true) - private String bounds_save_path = GlobalSettings.getBoundsFile(); + private String boundsSavePath = GlobalSettings.getBoundsFile(); // ===================================================================== - private LoopUnrolling() { } + private LoopUnrolling() { + } private LoopUnrolling(Configuration config) throws InvalidConfigurationException { this(); @@ -92,7 +92,9 @@ public void run(Program program) { logger.warn("Skipped unrolling: Program is already unrolled."); return; } - createBoundsFileIfMissing(); + if (pathIsSpecified(boundsSavePath)) { + ensureFileExistsAndIsEmpty(boundsSavePath); + } final int defaultBound = this.bound; program.getFunctions().forEach(this::run); program.getThreads().forEach(this::run); @@ -112,33 +114,9 @@ private void unrollLoopsInFunction(Function func, int defaultBound) { return; } final Map loopBoundsMap = computeLoopBoundsMap(func, defaultBound); - Map mergedBounds = new HashMap<>(loopBoundsMap); - if(!bounds_load_path.isEmpty()) { - final Map loopBoundsMapFromFile = loadLoopBoundsMapFromFile(func); - loopBoundsMapFromFile.forEach((key, value) -> mergedBounds.merge(key, value, Math::max)); - } func.getEvents(CondJump.class).stream() - .filter(mergedBounds::containsKey) - .forEach(j -> unrollLoop(j, mergedBounds.get(j))); - } - - private Map loadLoopBoundsMapFromFile(Function func) { - Map loopBoundsMapFromFile = new HashMap<>(); - try (Reader reader = new FileReader(bounds_load_path)) { - Iterable records = CSVFormat.DEFAULT.parse(reader); - for (CSVRecord record : records) { - int nexId = Integer.parseInt(record.get(0)); - int nextBound = Integer.parseInt(record.get(1)); - Predicate 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) { - e.printStackTrace(); - } - return loopBoundsMapFromFile; + .filter(loopBoundsMap::containsKey) + .forEach(j -> unrollLoop(j, loopBoundsMap.get(j))); } private Map computeLoopBoundsMap(Function func, int defaultBound) { @@ -165,6 +143,17 @@ private Map computeLoopBoundsMap(Function func, int defaultBo } } } + + // Merge with loaded bounds if those exist. + if(pathIsSpecified(boundsLoadPath)) { + final Map loopBoundsMapFromFile = loadLoopBoundsMapFromFile(func, boundsLoadPath); + loopBoundsMapFromFile.forEach((key, value) -> loopBoundsMap.merge(key, value, Math::max)); + } + // Store bounds we computed + if (pathIsSpecified(boundsSavePath)) { + dumpLoopBoundsMapToFile(func, loopBoundsMap, boundsSavePath); + } + return loopBoundsMap; } @@ -174,7 +163,6 @@ private void unrollLoop(CondJump loopBackJump, int bound) { Preconditions.checkArgument(loopBegin.getLocalId() < loopBackJump.getLocalId(), "The jump does not belong to a loop."); - dumpBoundIfMissing(loopBackJump, bound); int iterCounter = 0; while (++iterCounter <= bound) { if (iterCounter == bound) { @@ -243,34 +231,70 @@ private Event newBoundEvent(Function func) { return boundEvent; } - private void createBoundsFileIfMissing() { - File file = new File(bounds_save_path); - if (!file.exists()) { - try { - file.createNewFile(); - } catch (IOException e) { - e.printStackTrace(); + // ------------------------------------------------------------------------ + // Functions related to loading and storing bound maps + + private boolean pathIsSpecified(String path) { + return !path.isEmpty(); + } + + private void ensureFileExistsAndIsEmpty(String filePath) { + try { + final File file = new File(filePath); + if (!file.createNewFile()) { + // Clear file content + new FileWriter(file).close(); } + } catch (IOException e) { + e.printStackTrace(); } } - 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(bounds_load_path); - Writer writer = new FileWriter(bounds_save_path, 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; - } + public static int getPersistentLoopId(CondJump loopBackjump) { + return loopBackjump.getMetadata(UnrollingId.class).value(); + } + + public static int getUnrollingBoundAnnotation(CondJump boundEvent) { + Preconditions.checkArgument(boundEvent.hasTag(Tag.BOUND)); + return boundEvent.getMetadata(UnrollingBound.class).value(); + } + + private Map loadLoopBoundsMapFromFile(Function func, String filePath) { + Preconditions.checkArgument(pathIsSpecified(filePath)); + Preconditions.checkArgument(Files.exists(Path.of(filePath))); + + final List jumps = func.getEvents(CondJump.class); + final Map loopBoundsMapFromFile = new HashMap<>(); + try (Reader reader = new FileReader(filePath)) { + Iterable records = CSVFormat.DEFAULT.parse(reader); + for (CSVRecord record : records) { + final int loopId = Integer.parseInt(record.get(0)); + final int bound = Integer.parseInt(record.get(1)); + jumps.stream() + .filter(e -> getPersistentLoopId(e) == loopId) + .findFirst().ifPresent(loop -> loopBoundsMapFromFile.put(loop, bound)); } - if (!found) { - csvPrinter.printRecord(evId, bound.toString(), sourceLoc); + } catch (IOException e) { + e.printStackTrace(); + } + return loopBoundsMapFromFile; + } + + private void dumpLoopBoundsMapToFile(Function func, Map boundsMap, String filePath) { + Preconditions.checkArgument(pathIsSpecified(filePath)); + Preconditions.checkArgument(Files.exists(Path.of(filePath))); + + final SyntacticContextAnalysis synContext = SyntacticContextAnalysis.newInstance(func.getProgram()); + try (Writer writer = new FileWriter(filePath, true); + CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) { + for (Map.Entry entry : boundsMap.entrySet()) { + final CondJump loopJump = entry.getKey(); + final int loopId = getPersistentLoopId(loopJump); + final int loopBound = entry.getValue(); + final String sourceLoc = synContext.getSourceLocationWithContext(loopJump, false); + csvPrinter.printRecord(loopId, loopBound, sourceLoc); } + writer.flush(); csvPrinter.flush(); } catch (IOException e) { e.printStackTrace(); From c875e5c67778d095e0ad1dddf4c40d6f660f9dcf Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 25 Oct 2024 10:42:16 +0200 Subject: [PATCH 09/14] Fixed wrong update to bounds file --- dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 5864ccc77a..2b42aa89fd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -441,7 +441,7 @@ private static void increaseBoundAndDump(List boundEvents, Configuration csvPrinter.printRecord(entry); } else { final String[] content = entry.values(); - content[0] = String.valueOf(loopId2UpdatedBound.get(entryId)); + content[1] = String.valueOf(loopId2UpdatedBound.get(entryId)); csvPrinter.printRecord(Arrays.asList(content)); } } From 78969e5a79f39d320637c14f1c80fef7c0ff5049 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 25 Oct 2024 12:00:00 +0200 Subject: [PATCH 10/14] Fixed issue when specifying same file for loading and storing bounds. --- .../program/processing/LoopUnrolling.java | 108 ++++++++++-------- 1 file changed, 62 insertions(+), 46 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 84222a6c66..d90c4fd0d3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -23,7 +23,10 @@ import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.*; -import java.io.*; +import java.io.FileReader; +import java.io.FileWriter; +import java.io.IOException; +import java.io.Reader; import java.nio.file.Files; import java.nio.file.Path; import java.util.*; @@ -69,6 +72,10 @@ public void setUnrollingBound(int bound) { // ===================================================================== + // We use this once for loading bounds from files (if any), and then to track + // all computed loop bounds for later storing them into a file (if desired). + private Map> globalLoopBoundsMap = new HashMap<>(); + private LoopUnrolling() { } @@ -92,15 +99,18 @@ public void run(Program program) { logger.warn("Skipped unrolling: Program is already unrolled."); return; } - if (pathIsSpecified(boundsSavePath)) { - ensureFileExistsAndIsEmpty(boundsSavePath); - } + + globalLoopBoundsMap = loadLoopBoundsMapFromFile(program, boundsLoadPath); + final int defaultBound = this.bound; program.getFunctions().forEach(this::run); program.getThreads().forEach(this::run); program.markAsUnrolled(defaultBound); IdReassignment.newInstance().run(program); // Reassign ids because of newly created events + dumpLoopBoundsMapToFile(program, globalLoopBoundsMap, boundsSavePath); + globalLoopBoundsMap = null; // Save up some memory + logger.info("Program unrolled {} times", defaultBound); } @@ -145,14 +155,12 @@ private Map computeLoopBoundsMap(Function func, int defaultBo } // Merge with loaded bounds if those exist. - if(pathIsSpecified(boundsLoadPath)) { - final Map loopBoundsMapFromFile = loadLoopBoundsMapFromFile(func, boundsLoadPath); + if(globalLoopBoundsMap.containsKey(func)) { + final Map loopBoundsMapFromFile = globalLoopBoundsMap.get(func); loopBoundsMapFromFile.forEach((key, value) -> loopBoundsMap.merge(key, value, Math::max)); } - // Store bounds we computed - if (pathIsSpecified(boundsSavePath)) { - dumpLoopBoundsMapToFile(func, loopBoundsMap, boundsSavePath); - } + // Remember bounds for function for dumping. + globalLoopBoundsMap.put(func, loopBoundsMap); return loopBoundsMap; } @@ -238,20 +246,9 @@ private boolean pathIsSpecified(String path) { return !path.isEmpty(); } - private void ensureFileExistsAndIsEmpty(String filePath) { - try { - final File file = new File(filePath); - if (!file.createNewFile()) { - // Clear file content - new FileWriter(file).close(); - } - } catch (IOException e) { - e.printStackTrace(); - } - } - public static int getPersistentLoopId(CondJump loopBackjump) { - return loopBackjump.getMetadata(UnrollingId.class).value(); + final UnrollingId id = loopBackjump.getMetadata(UnrollingId.class); + return id != null ? id.value() : loopBackjump.getGlobalId(); } public static int getUnrollingBoundAnnotation(CondJump boundEvent) { @@ -259,42 +256,61 @@ public static int getUnrollingBoundAnnotation(CondJump boundEvent) { return boundEvent.getMetadata(UnrollingBound.class).value(); } - private Map loadLoopBoundsMapFromFile(Function func, String filePath) { - Preconditions.checkArgument(pathIsSpecified(filePath)); - Preconditions.checkArgument(Files.exists(Path.of(filePath))); + private Map> loadLoopBoundsMapFromFile(Program program, String filePath) { + if (!pathIsSpecified(filePath)) { + return new HashMap<>(); + } + if (!Files.exists(Path.of(filePath))) { + logger.warn("There is no bounds file at path {} . Using default bounds.", filePath); + return new HashMap<>(); + } - final List jumps = func.getEvents(CondJump.class); - final Map loopBoundsMapFromFile = new HashMap<>(); + // Compute mapping from ids to loop events + final Map idToJump = new HashMap<>(); + program.getFunctions().forEach(f -> f.getEvents(CondJump.class).forEach( + jump -> idToJump.put(getPersistentLoopId(jump), jump)) + ); + + // Read CSV file to find bounds for loop events + final Map> loopBoundsMapPerFunction = new HashMap<>(); try (Reader reader = new FileReader(filePath)) { Iterable records = CSVFormat.DEFAULT.parse(reader); for (CSVRecord record : records) { final int loopId = Integer.parseInt(record.get(0)); final int bound = Integer.parseInt(record.get(1)); - jumps.stream() - .filter(e -> getPersistentLoopId(e) == loopId) - .findFirst().ifPresent(loop -> loopBoundsMapFromFile.put(loop, bound)); + final CondJump loopJump = idToJump.get(loopId); + if (loopJump == null) { + logger.warn("Loaded bounds file does not match with the program. Ignoring file."); + loopBoundsMapPerFunction.clear(); + break; + } + loopBoundsMapPerFunction + .computeIfAbsent(loopJump.getFunction(), key -> new HashMap<>()) + .put(loopJump, bound); } } catch (IOException e) { e.printStackTrace(); } - return loopBoundsMapFromFile; + + return loopBoundsMapPerFunction; } - private void dumpLoopBoundsMapToFile(Function func, Map boundsMap, String filePath) { - Preconditions.checkArgument(pathIsSpecified(filePath)); - Preconditions.checkArgument(Files.exists(Path.of(filePath))); - - final SyntacticContextAnalysis synContext = SyntacticContextAnalysis.newInstance(func.getProgram()); - try (Writer writer = new FileWriter(filePath, true); - CSVPrinter csvPrinter = new CSVPrinter(writer, CSVFormat.DEFAULT)) { - for (Map.Entry entry : boundsMap.entrySet()) { - final CondJump loopJump = entry.getKey(); - final int loopId = getPersistentLoopId(loopJump); - final int loopBound = entry.getValue(); - final String sourceLoc = synContext.getSourceLocationWithContext(loopJump, false); - csvPrinter.printRecord(loopId, loopBound, sourceLoc); + private void dumpLoopBoundsMapToFile(Program program, Map> loopBounds, String filePath) { + if (!pathIsSpecified(filePath)) { + return; + } + + final SyntacticContextAnalysis synContext = SyntacticContextAnalysis.newInstance(program); + try (CSVPrinter csvPrinter = new CSVPrinter( new FileWriter(filePath, true), CSVFormat.DEFAULT)) { + for (Map loopBoundsMap : loopBounds.values()) { + for (Map.Entry entry : loopBoundsMap.entrySet()) { + final CondJump loopJump = entry.getKey(); + final int loopId = getPersistentLoopId(loopJump); + final int loopBound = entry.getValue(); + final String sourceLoc = synContext.getSourceLocationWithContext(loopJump, false); + csvPrinter.printRecord(loopId, loopBound, sourceLoc); + } } - writer.flush(); csvPrinter.flush(); } catch (IOException e) { e.printStackTrace(); From b88bd72ca8c76c96e483316e92431e2d7ff8c241 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Fri, 25 Oct 2024 20:55:06 +0200 Subject: [PATCH 11/14] Fix appending rather than clearing the bounds file. --- .../com/dat3m/dartagnan/program/processing/LoopUnrolling.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index d90c4fd0d3..e83fad564a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -301,7 +301,7 @@ private void dumpLoopBoundsMapToFile(Program program, Map loopBoundsMap : loopBounds.values()) { for (Map.Entry entry : loopBoundsMap.entrySet()) { final CondJump loopJump = entry.getKey(); From bf1d312c2c7eb4070ed172e953d78d0a288b1aad Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sat, 26 Oct 2024 17:34:57 +0800 Subject: [PATCH 12/14] Log warning when there are problems with bounds file Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java | 2 +- .../com/dat3m/dartagnan/program/processing/LoopUnrolling.java | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 2b42aa89fd..4d9fd5cac9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -356,7 +356,7 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm try { increaseBoundAndDump(reachedBounds, task.getConfig()); } catch (IOException e) { - e.printStackTrace(); + logger.warn("Failed to save bounds file: {}", e.getLocalizedMessage()); } } summary.append(result).append("\n"); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index e83fad564a..b0b81a6291 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -289,7 +289,7 @@ private Map> loadLoopBoundsMapFromFile(Program .put(loopJump, bound); } } catch (IOException e) { - e.printStackTrace(); + // Nothing to be done, filePath is guaranteed to exists when the FileReader is called. } return loopBoundsMapPerFunction; @@ -313,7 +313,7 @@ private void dumpLoopBoundsMapToFile(Program program, Map Date: Sat, 26 Oct 2024 17:44:48 +0800 Subject: [PATCH 13/14] Log warning when there are problems to read bounds file Signed-off-by: Hernan Ponce de Leon --- .../com/dat3m/dartagnan/program/processing/LoopUnrolling.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index b0b81a6291..2d58ab94b3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -289,7 +289,7 @@ private Map> loadLoopBoundsMapFromFile(Program .put(loopJump, bound); } } catch (IOException e) { - // Nothing to be done, filePath is guaranteed to exists when the FileReader is called. + logger.warn("Failed to read bounds file: {}", e.getLocalizedMessage()); } return loopBoundsMapPerFunction; From dbdc0652d4ca0a271fc28ddc8d685e91a2a8dd0a Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Sun, 27 Oct 2024 18:11:15 +0800 Subject: [PATCH 14/14] Remove getBoundsFile() Signed-off-by: Hernan Ponce de Leon --- dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java | 7 ++++--- .../src/main/java/com/dat3m/dartagnan/GlobalSettings.java | 4 ---- .../dat3m/dartagnan/program/processing/LoopUnrolling.java | 2 +- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 4d9fd5cac9..2bbb4721ef 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -413,9 +413,10 @@ public static String generateResultSummary(VerificationTask task, ProverEnvironm } private static void increaseBoundAndDump(List boundEvents, Configuration config) throws IOException { - final File boundsFile = new File(config.hasProperty(BOUNDS_SAVE_PATH) ? - config.getProperty(BOUNDS_SAVE_PATH) : - GlobalSettings.getBoundsFile()); + if(!config.hasProperty(BOUNDS_SAVE_PATH)) { + return; + } + final File boundsFile = new File(config.getProperty(BOUNDS_SAVE_PATH)); // Parse old entries final List entries; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java index 36e4cc160a..80c3d43a9b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java @@ -38,10 +38,6 @@ public static String getCatDirectory() { return env + "/cat"; } - public static String getBoundsFile() { - return getOutputDirectory() + "/bounds.csv"; - } - public static String getOrCreateOutputDirectory() throws IOException { String path = getOutputDirectory(); Files.createDirectories(Paths.get(path)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 2d58ab94b3..5ba72b9c4f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -68,7 +68,7 @@ public void setUnrollingBound(int bound) { @Option(name = BOUNDS_SAVE_PATH, description = "Path to the CSV file to save loop bounds.", secure = true) - private String boundsSavePath = GlobalSettings.getBoundsFile(); + private String boundsSavePath = ""; // =====================================================================