Remove option program.processing.loopBounds.useDefAnalysis

Remove NaiveLoopBoundAnnotation.newInstance()
Add NaiveLoopBoundAnnotation.fromConfig(Configuration)
Add ReachingDefinitionsAnalysis.configure(Configuration)
Set BackwardsReachingDefinitionsAnalysis package-private

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";

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<RegReader, ReaderInfo> readerMap = new HashMap<>();
     private final Map<RegWriter, Readers> 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<Register> finalRegisters = finalRegisters(program);

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);
+            };
+        }
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveLoopBoundAnnotation.java

@@ -6,26 +6,22 @@
 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;
 import com.dat3m.dartagnan.program.event.core.CondJump;
 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<Event> preDominatorTree = DominatorAnalysis.computePreDominatorTree(function.getEntry(), function.getExit());
         final List<LoopAnalysis.LoopInfo> loops = LoopAnalysis.onFunction(function).getLoopsOfFunction(function);
 

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(

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());