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 f0d77eb788..61831093e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -46,7 +46,6 @@ public class OptionNames { public static final String DYNAMIC_SPINLOOP_DETECTION = "program.processing.spinloops"; public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments"; public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType"; - public static final String LOOP_BOUNDS_USE_DEF_METHOD = "program.processing.loopBounds.useDefAnalysis"; // Program Property Options public static final String REACHING_DEFINITIONS_METHOD = "program.analysis.reachingDefinitions"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java index c0eef846b7..255cccd3f2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BackwardsReachingDefinitionsAnalysis.java @@ -10,8 +10,8 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.verification.Context; import com.google.common.base.Preconditions; +import com.google.common.base.Verify; import com.google.common.collect.Iterables; -import org.sosy_lab.common.configuration.Configuration; import java.util.ArrayList; import java.util.Collection; @@ -39,7 +39,7 @@ * that is, backward jumps cause re-evaluation of the loop body until convergence. * This results in a squared worst-case time complexity in terms of events being processed. */ -public class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { +class BackwardsReachingDefinitionsAnalysis implements ReachingDefinitionsAnalysis { private final Map readerMap = new HashMap<>(); private final Map writerMap = new HashMap<>(); @@ -57,7 +57,7 @@ public Writers getWriters(RegReader reader) { @Override public Writers getFinalWriters() { final ReaderInfo result = readerMap.get(FINAL_READER); - Preconditions.checkState(result != null, "final state has not been analyzed."); + Verify.verify(result != null, "final state has not been analyzed."); return result; } @@ -78,7 +78,7 @@ public Readers getReaders(RegWriter writer) { */ public Readers getInitialReaders() { final Readers result = writerMap.get(INITIAL_WRITER); - Preconditions.checkState(result != null, "initial state has not been analyzed."); + Verify.verify(result != null, "initial state has not been analyzed."); return result; } @@ -101,9 +101,8 @@ public static BackwardsReachingDefinitionsAnalysis forFunction(Function function * Optionally queries {@link ExecutionAnalysis} for pairs of writers appearing together in an execution. * @param program Contains a set of threads to be analyzed. Additionally-defined functions are ignored. * @param analysisContext Collection of previous analyses to be used as dependencies. - * @param config User-defined settings for this analysis. */ - public static BackwardsReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) { + public static BackwardsReachingDefinitionsAnalysis forProgram(Program program, Context analysisContext) { final ExecutionAnalysis exec = analysisContext.get(ExecutionAnalysis.class); final var analysis = new BackwardsReachingDefinitionsAnalysis(); final Set finalRegisters = finalRegisters(program); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java index 41caac9a2f..d2997516ab 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ReachingDefinitionsAnalysis.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.program.analysis; +import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.RegReader; @@ -80,22 +81,38 @@ interface RegisterWriters { static ReachingDefinitionsAnalysis fromConfig(Program program, Context analysisContext, Configuration config) throws InvalidConfigurationException { - var c = new Config(); - config.inject(c); - ReachingDefinitionsAnalysis analysis = switch (c.method) { - case BACKWARD -> BackwardsReachingDefinitionsAnalysis.fromConfig(program, analysisContext, config); + ReachingDefinitionsAnalysis analysis = switch (configure(config).method) { + case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forProgram(program, analysisContext); case FORWARD -> Dependency.fromConfig(program, analysisContext, config); }; analysisContext.register(ReachingDefinitionsAnalysis.class, analysis); return analysis; } + static Config configure(Configuration config) throws InvalidConfigurationException { + var c = new Config(); + config.inject(c); + return c; + } + + enum Method { BACKWARD, FORWARD } + @Options final class Config { - @Option(name = REACHING_DEFINITIONS_METHOD, description = "", secure = true) + @Option(name = REACHING_DEFINITIONS_METHOD, + description = "Specifies the static analysis algorithm, that collects the relationship between" + + " register writers and their direct readers.", + secure = true) private Method method = Method.BACKWARD; - } - enum Method { BACKWARD, FORWARD} + private Config() {} + + public ReachingDefinitionsAnalysis forFunction(Function function) { + return switch (method) { + case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forFunction(function); + case FORWARD -> UseDefAnalysis.forFunction(function); + }; + } + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java index 55c3083c87..4ecfc1498e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java @@ -6,12 +6,10 @@ import com.dat3m.dartagnan.expression.misc.ITEExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.DominatorAnalysis; import com.dat3m.dartagnan.program.analysis.LiveRegistersAnalysis; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; -import com.dat3m.dartagnan.program.analysis.UseDefAnalysis; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.RegWriter; @@ -19,13 +17,11 @@ import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Local; import com.dat3m.dartagnan.utils.DominatorTree; -import org.sosy_lab.common.configuration.Option; -import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import java.util.List; -import static com.dat3m.dartagnan.configuration.OptionNames.LOOP_BOUNDS_USE_DEF_METHOD; - /* This pass adds a loop bound annotation to static loops of the form @@ -48,19 +44,17 @@ TODO: support general step increments */ -@Options public class NaiveLoopBoundAnnotation implements FunctionProcessor { - @Option(name = LOOP_BOUNDS_USE_DEF_METHOD, - description = "", - secure = true) - private Method method = Method.BACKWARD; + private final ReachingDefinitionsAnalysis.Config reachingDefinitionsAnalysis; - public static NaiveLoopBoundAnnotation newInstance() { - return new NaiveLoopBoundAnnotation(); + private NaiveLoopBoundAnnotation(ReachingDefinitionsAnalysis.Config c) { + reachingDefinitionsAnalysis = c; } - public enum Method { BACKWARD, FORWARD } + public static NaiveLoopBoundAnnotation fromConfig(Configuration config) throws InvalidConfigurationException { + return new NaiveLoopBoundAnnotation(ReachingDefinitionsAnalysis.configure(config)); + } @Override public void run(Function function) { @@ -69,10 +63,7 @@ public void run(Function function) { } final LiveRegistersAnalysis liveAnalysis = LiveRegistersAnalysis.forFunction(function); - final ReachingDefinitionsAnalysis useDefAnalysis = switch(method) { - case BACKWARD -> BackwardsReachingDefinitionsAnalysis.forFunction(function); - case FORWARD -> UseDefAnalysis.forFunction(function); - }; + final ReachingDefinitionsAnalysis useDefAnalysis = reachingDefinitionsAnalysis.forFunction(function); final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(function.getEntry(), function.getExit()); final List loops = LoopAnalysis.onFunction(function).getLoopsOfFunction(function); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java index 19c24b528e..60b209d087 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java @@ -108,7 +108,7 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep ProgramProcessor.fromFunctionProcessor(MemToReg.fromConfig(config), Target.FUNCTIONS, true), ProgramProcessor.fromFunctionProcessor(sccp, Target.FUNCTIONS, false), dynamicSpinLoopDetection ? DynamicSpinLoopDetection.fromConfig(config) : null, - ProgramProcessor.fromFunctionProcessor(NaiveLoopBoundAnnotation.newInstance(), Target.FUNCTIONS, true), + ProgramProcessor.fromFunctionProcessor(NaiveLoopBoundAnnotation.fromConfig(config), Target.FUNCTIONS, true), LoopUnrolling.fromConfig(config), // We keep unrolling global for now printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling", Printer.Mode.ALL) : null, ProgramProcessor.fromFunctionProcessor( diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 62f05b006a..fea312ebc5 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -10,7 +10,6 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.analysis.BackwardsReachingDefinitionsAnalysis; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.ReachingDefinitionsAnalysis; @@ -113,7 +112,7 @@ private void reachingDefinitionMustOverride(ReachingDefinitionsAnalysis.Method m @Test - public void reachingDefinitionSupportsLoops() { + public void reachingDefinitionSupportsLoops() throws InvalidConfigurationException { ProgramBuilder b = ProgramBuilder.forLanguage(SourceLanguage.LITMUS); b.newFunction("test", 0, types.getFunctionType(types.getArchType(), List.of()), List.of()); Register r0 = b.getOrNewRegister(0, "r0"); @@ -187,7 +186,11 @@ public void reachingDefinitionSupportsLoops() { b.addChild(0, ret); Program program = b.build(); - final var dep = BackwardsReachingDefinitionsAnalysis.forFunction(program.getFunctions().get(0)); + Configuration config = Configuration.builder() + .setOption(REACHING_DEFINITIONS_METHOD, ReachingDefinitionsAnalysis.Method.BACKWARD.name()) + .build(); + final ReachingDefinitionsAnalysis dep = ReachingDefinitionsAnalysis.configure(config) + .forFunction(program.getFunctions().get(0)); assertFalse(dep.getWriters(r00).ofRegister(r0).mustBeInitialized()); assertList(dep.getWriters(r00).ofRegister(r0).getMayWriters()); assertFalse(dep.getWriters(r10).ofRegister(r0).mustBeInitialized());