diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 3647d7067e..9e228b93f3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -9,10 +9,10 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Program.SourceLanguage; import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Assert; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.utils.Result; import com.dat3m.dartagnan.utils.options.BaseOptions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java index 66e8556be1..d684352e91 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodeSets.java @@ -1,13 +1,16 @@ package com.dat3m.dartagnan.encoding; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Definition.Visitor; import com.dat3m.dartagnan.wmm.Relation; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.utils.EventGraph; -import java.util.*; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; // Propagates relationships in a verification task that need to be constrained in an SMT-based verification. final class EncodeSets implements Visitor> { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java index 5a37e8481f..b76feda76c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -9,8 +9,13 @@ import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; -import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.event.core.CondJump; +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; +import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.verification.VerificationTask; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index 07d53ef0fe..a817612802 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -5,7 +5,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.memory.Location; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.sosy_lab.java_smt.api.*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 5817c9c763..5fe707af7c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -7,11 +7,11 @@ import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.base.Preconditions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index 953b4d2151..bf5dd071f7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -7,15 +7,17 @@ import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; import com.dat3m.dartagnan.program.specification.AbstractAssert; import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.RelationNameRepository; import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.relation.RelationNameRepository; import com.dat3m.dartagnan.wmm.utils.EventGraph; import com.google.common.base.Preconditions; import com.google.common.collect.Lists; @@ -23,7 +25,10 @@ import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.java_smt.api.*; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; import java.util.*; import java.util.function.BiFunction; @@ -32,7 +37,7 @@ import static com.dat3m.dartagnan.configuration.Property.*; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LITMUS; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.CO; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java index df6b2afc6e..8e0bda0348 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/SymmetryEncoder.java @@ -3,14 +3,14 @@ import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.utils.Tuple; import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.Tuple; import com.google.common.base.Preconditions; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index 6f79724beb..202d5b07e7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -5,13 +5,13 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.analysis.Dependency; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.FenceWithId; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; -import com.dat3m.dartagnan.program.event.core.MemoryEvent; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.core.RMWStoreExclusive; import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; import com.dat3m.dartagnan.wmm.Definition; @@ -19,8 +19,8 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.utils.Flag; import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.Flag; import com.google.common.collect.Iterables; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -34,7 +34,7 @@ import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS; import static com.dat3m.dartagnan.program.event.Tag.*; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.RF; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; import static com.google.common.base.Verify.verify; import static java.lang.Boolean.TRUE; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java index 1ad556acfb..c975bf76c4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java @@ -19,7 +19,7 @@ import java.util.Optional; import static com.dat3m.dartagnan.program.event.Tag.VISIBLE; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.ID; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.ID; class VisitorBase extends CatBaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java index ac47a5f0ae..a6d27bc139 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java @@ -10,14 +10,11 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.expression.type.TypeFactory; -import com.dat3m.dartagnan.program.Function; -import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.Program.SourceLanguage; -import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.ScopeHierarchy; +import com.dat3m.dartagnan.program.*; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.Program.SourceLanguage; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; import com.dat3m.dartagnan.program.event.metadata.OriginalId; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java index de5efef88f..a126788b8a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java @@ -13,10 +13,10 @@ import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.IfAsJump; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.memory.MemoryObject; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java index 2898291ff7..8babca5754 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java @@ -21,7 +21,7 @@ import java.util.HashMap; import java.util.Map; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; public class VisitorLitmusPPC extends LitmusPPCBaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java index 5239f03569..0a60d40f88 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java @@ -5,7 +5,6 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.IConst; -import com.dat3m.dartagnan.expression.IExpr; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; @@ -15,13 +14,16 @@ import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp; import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp; -import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.event.core.Label; +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.antlr.v4.runtime.misc.Interval; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java index 3b8018cb30..4ff717b582 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java @@ -15,11 +15,11 @@ import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; import org.antlr.v4.runtime.misc.Interval; public class VisitorLitmusRISCV extends LitmusRISCVBaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java index 2c3593780f..134e2d4f79 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java @@ -14,15 +14,15 @@ import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMW; -import com.dat3m.dartagnan.program.event.core.MemoryEvent; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp; +import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.program.event.core.Store; -import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.antlr.v4.runtime.misc.Interval; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java index 731fc64a80..f51aa513dd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java @@ -17,7 +17,7 @@ import com.google.common.collect.ImmutableSet; import org.antlr.v4.runtime.misc.Interval; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.MFENCE; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.MFENCE; public class VisitorLitmusX86 extends LitmusX86BaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index 8b2a6da822..1d2bc7db9c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -11,9 +11,9 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.metadata.Metadata; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java index 0b9c74f468..82ada61e1e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java @@ -8,8 +8,8 @@ import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.expression.type.VoidType; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.processing.Intrinsics; import com.google.common.base.Preconditions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java index 1ee1ea8a28..55dcb5cc8e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program; import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.functions.AbortIf; import com.dat3m.dartagnan.program.event.functions.Return; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java index bfd9528c9d..c0ce860333 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.expression.INonDet; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.specification.AbstractAssert; import com.google.common.base.Preconditions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java index b9c3c370c3..620debc3cb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Thread.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program; import com.dat3m.dartagnan.expression.type.FunctionType; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.Store; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BranchEquivalence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BranchEquivalence.java index f18d72d57d..8573199219 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BranchEquivalence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/BranchEquivalence.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java index 5154661383..99e9eeed9b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/Dependency.java @@ -3,10 +3,10 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.verification.Context; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java index 4a822c9d0f..db0147f496 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ExecutionAnalysis.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.analysis; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.verification.Context; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LoopAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LoopAnalysis.java index 6363df3f40..0bce78260e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LoopAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/LoopAnalysis.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.google.common.base.Verify; import com.google.common.collect.ImmutableList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java index 845e3b197d..4e5393c52f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/SyntacticContextAnalysis.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; @@ -32,7 +32,8 @@ public class SyntacticContextAnalysis { Contexts represent information surrounding an event like the executing thread, the call stack and the iteration numbers of loops. */ - public interface Context { } + public interface Context { + } public record ThreadContext(Thread thread) implements Context { @Override @@ -69,9 +70,17 @@ private Info(Event event, ImmutableList contextStack) { this.contextStack = contextStack; } - public Event getEvent() { return this.event; } - public ImmutableList getContextStack() { return this.contextStack; } - public boolean hasContext() { return !contextStack.isEmpty(); } + public Event getEvent() { + return this.event; + } + + public ImmutableList getContextStack() { + return this.contextStack; + } + + public boolean hasContext() { + return !contextStack.isEmpty(); + } public ImmutableList getContextOfType(Class contextClass) { final Stream filteredContext = contextStack.stream() @@ -92,7 +101,7 @@ public String toString() { } // We use this enum to track loop nesting - private enum LoopMarkerTypes { START, INC, END } + private enum LoopMarkerTypes {START, INC, END} // ============================================================================ @@ -106,7 +115,8 @@ public Info getContextInfo(Event ev) { return retVal; } - private SyntacticContextAnalysis() {} + private SyntacticContextAnalysis() { + } public static SyntacticContextAnalysis newInstance(Program program) { final SyntacticContextAnalysis analysis = new SyntacticContextAnalysis(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ThreadSymmetry.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ThreadSymmetry.java index fecbe11dbc..0332e6e8d6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ThreadSymmetry.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/ThreadSymmetry.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.utils.equivalence.AbstractEquivalence; import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import com.google.common.base.Preconditions; @@ -73,13 +73,13 @@ private void createSymmetryMappings() { // ================= Public methods =================== public Event map(Event source, Thread targetThread) { - Preconditions.checkArgument(areEquivalent(source.getThread(), targetThread), - "Target thread is not symmetric with source thread."); + Preconditions.checkArgument(areEquivalent(source.getThread(), targetThread), + "Target thread is not symmetric with source thread."); return thread2id2EventMap.get(targetThread).get(event2IdMap.get(source)); } public Function createEventPermutation(List origPerm, List targetPerm) { - Preconditions.checkArgument(origPerm.size() == targetPerm.size(), + Preconditions.checkArgument(origPerm.size() == targetPerm.size(), "Target permutation has different size to original permutation."); if (origPerm.equals(targetPerm)) { return Function.identity(); @@ -104,8 +104,8 @@ public Function createEventTransposition(Thread t1, Thread t2) { } public List> createAllEventPermutations(EquivalenceClass eqClass) { - Preconditions.checkArgument(eqClass.getEquivalence() == this, - " is not a symmetry class of this symmetry equivalence."); + Preconditions.checkArgument(eqClass.getEquivalence() == this, + " is not a symmetry class of this symmetry equivalence."); final List symmThreads = new ArrayList<>(eqClass); symmThreads.sort(Comparator.comparingInt(Thread::getId)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java index e92b147186..a40f248724 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AliasAnalysis.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.configuration.Alias; import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.core.Init; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; -import com.dat3m.dartagnan.program.event.core.MemoryEvent; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; import com.dat3m.dartagnan.utils.visualization.Graphviz; import org.apache.logging.log4j.LogManager; @@ -18,11 +18,7 @@ import java.io.File; import java.io.FileWriter; import java.io.IOException; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; +import java.util.*; import static com.dat3m.dartagnan.GlobalSettings.getOutputDirectory; import static com.dat3m.dartagnan.configuration.OptionNames.*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java index 3f81b70650..e3d6d1e187 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java @@ -5,11 +5,11 @@ import com.dat3m.dartagnan.expression.IExprBin; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.Local; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; -import com.dat3m.dartagnan.program.event.core.MemoryEvent; import com.dat3m.dartagnan.program.event.core.Store; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.base.Preconditions; import com.google.common.base.Verify; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java index 8eeb33c039..98a4611144 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/EqualityAliasAnalysis.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.wmm.utils.EventGraph; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java index a8d3e6177d..50c2d4c8f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java @@ -4,9 +4,14 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegWriter; +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.Local; +import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; +import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Sets; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/AbstractEvent.java similarity index 98% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/AbstractEvent.java index f2270890b0..6a7f0cd59d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/AbstractEvent.java @@ -1,14 +1,12 @@ -package com.dat3m.dartagnan.program.event.core; +package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.EventUser; import com.dat3m.dartagnan.program.event.metadata.CustomPrinting; import com.dat3m.dartagnan.program.event.metadata.Metadata; import com.dat3m.dartagnan.program.event.metadata.MetadataMap; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.dat3m.dartagnan.verification.Context; import com.google.common.base.Preconditions; import org.sosy_lab.java_smt.api.BooleanFormula; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Event.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Event.java similarity index 95% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Event.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Event.java index 6026ee55ff..ee302a3149 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Event.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Event.java @@ -1,13 +1,11 @@ -package com.dat3m.dartagnan.program.event.core; +package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.encoding.Encoder; import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.EventUser; import com.dat3m.dartagnan.program.event.metadata.Metadata; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.dat3m.dartagnan.verification.Context; import org.sosy_lab.java_smt.api.BooleanFormula; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index 5d5095305f..30fcfeb28a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -15,17 +15,14 @@ import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp; -import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp; -import com.dat3m.dartagnan.program.event.core.FenceWithId; import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp; import com.dat3m.dartagnan.program.event.arch.tso.TSOXchg; import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMW; +import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; import com.dat3m.dartagnan.program.event.core.annotations.StringAnnotation; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument; import com.dat3m.dartagnan.program.event.core.threading.ThreadCreate; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; @@ -46,7 +43,7 @@ import java.util.*; import java.util.stream.Collectors; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; public class EventFactory { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventUser.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventUser.java index 14f7af9070..0da983cb3f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventUser.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventUser.java @@ -1,8 +1,6 @@ package com.dat3m.dartagnan.program.event; -import com.dat3m.dartagnan.program.event.core.Event; - import java.util.Map; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java similarity index 88% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java index 92db61bfd2..9893a6d0a3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/visitors/EventVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventVisitor.java @@ -1,19 +1,25 @@ -package com.dat3m.dartagnan.program.event.visitors; +package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.program.event.arch.StoreExclusive; import com.dat3m.dartagnan.program.event.arch.lisa.LISARMW; -import com.dat3m.dartagnan.program.event.arch.ptx.*; -import com.dat3m.dartagnan.program.event.arch.vulkan.*; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp; import com.dat3m.dartagnan.program.event.arch.tso.TSOXchg; +import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMW; +import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation; -import com.dat3m.dartagnan.program.event.core.rmw.*; import com.dat3m.dartagnan.program.event.lang.Alloc; import com.dat3m.dartagnan.program.event.lang.catomic.*; import com.dat3m.dartagnan.program.event.lang.linux.*; import com.dat3m.dartagnan.program.event.lang.llvm.*; -import com.dat3m.dartagnan.program.event.lang.pthread.*; -import com.dat3m.dartagnan.program.event.lang.svcomp.*; +import com.dat3m.dartagnan.program.event.lang.pthread.InitLock; +import com.dat3m.dartagnan.program.event.lang.pthread.Lock; +import com.dat3m.dartagnan.program.event.lang.pthread.Unlock; +import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic; +import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic; public interface EventVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/MemoryEvent.java similarity index 72% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryEvent.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/MemoryEvent.java index 827bece8b9..f4a676cd06 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/MemoryEvent.java @@ -1,8 +1,4 @@ -package com.dat3m.dartagnan.program.event.core; - -import com.dat3m.dartagnan.program.event.MemoryAccess; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +package com.dat3m.dartagnan.program.event; import java.util.HashSet; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/utils/RegReader.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/RegReader.java similarity index 77% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/utils/RegReader.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/RegReader.java index bdc6b77039..eaae1d4115 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/utils/RegReader.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/RegReader.java @@ -1,9 +1,8 @@ -package com.dat3m.dartagnan.program.event.core.utils; +package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.Event; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/utils/RegWriter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/RegWriter.java similarity index 61% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/utils/RegWriter.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/RegWriter.java index 9cb73045ff..c19b8b2465 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/utils/RegWriter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/RegWriter.java @@ -1,7 +1,6 @@ -package com.dat3m.dartagnan.program.event.core.utils; +package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.Event; public interface RegWriter extends Event { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index cc39f27971..eda7730609 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -1,7 +1,6 @@ package com.dat3m.dartagnan.program.event; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.program.event.core.Event; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/StoreExclusive.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/StoreExclusive.java index 7b092c8280..4c2f3e553c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/StoreExclusive.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/StoreExclusive.java @@ -2,10 +2,10 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.StoreBase; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; /* This event is common among ARMv8, RISCV, and PPC. diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/LISARMW.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/LISARMW.java index d6fac2bead..ae4cde6852 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/LISARMW.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/lisa/LISARMW.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LISARMW extends RMWXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomCAS.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomCAS.java index dd44bc2ad6..5eaf555088 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomCAS.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomCAS.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWCmpXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class PTXAtomCAS extends RMWCmpXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomExch.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomExch.java index 25eaa60877..64dffdf00d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomExch.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomExch.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class PTXAtomExch extends RMWXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java index 0cc1f2ab8f..9d4a4b9b6f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class PTXAtomOp extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java index 652ec1079c..4663f6d676 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class PTXRedOp extends RMWOpBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/TSOXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/TSOXchg.java index 47210d8912..3a586f776c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/TSOXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/tso/TSOXchg.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import static com.dat3m.dartagnan.program.event.Tag.TSO; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMW.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMW.java index 3af641dbf3..40f8ab5677 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMW.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMW.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class VulkanRMW extends RMWXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java index 8cc976ad79..74ed76f7c5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class VulkanRMWOp extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java index 7c8b89d0b9..bd6c3bf3f1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/FenceBase.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.common; +import com.dat3m.dartagnan.program.event.AbstractEvent; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; @NoInterface public abstract class FenceBase extends AbstractEvent { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/LoadBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/LoadBase.java index d774f08dcd..3a89309506 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/LoadBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/LoadBase.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.MemoryAccess; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; @NoInterface diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWCmpXchgBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWCmpXchgBase.java index fa27447d52..25d428dfaa 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWCmpXchgBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWCmpXchgBase.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.MemoryAccess; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.RegWriter; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java index 33362d141c..2bf35642b5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.RegWriter; /* This class can be used as base for many value-returning operator-based RMWs, such as diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWXchgBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWXchgBase.java index 5122460172..2bc9d54268 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWXchgBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWXchgBase.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.MemoryAccess; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.RegWriter; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/SingleAccessMemoryEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/SingleAccessMemoryEvent.java index c49e15222c..a16bb7b617 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/SingleAccessMemoryEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/SingleAccessMemoryEvent.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.Type; +import com.dat3m.dartagnan.program.event.AbstractEvent; import com.dat3m.dartagnan.program.event.MemoryAccess; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.MemoryEvent; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.google.common.base.Preconditions; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryCoreEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryCoreEvent.java index beb875477f..1502f9d93a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryCoreEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/AbstractMemoryCoreEvent.java @@ -3,6 +3,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.Type; +import com.dat3m.dartagnan.program.event.AbstractEvent; import com.dat3m.dartagnan.program.event.common.NoInterface; import com.google.common.base.Preconditions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assert.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assert.java index dfd2dea8ef..16002bbd8d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assert.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assert.java @@ -3,8 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.RegReader; import com.google.common.base.Preconditions; import java.util.HashSet; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assume.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assume.java index 1031ab0fe0..48331baa33 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assume.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Assume.java @@ -4,8 +4,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.RegReader; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java index 8a8bcbc412..557c928266 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java @@ -5,10 +5,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.*; import com.google.common.base.Preconditions; import java.util.HashSet; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java index 34e8456960..e2c76bbdc8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/ExecutionStatus.java @@ -5,10 +5,10 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; -import org.sosy_lab.java_smt.api.*; +import com.dat3m.dartagnan.program.event.*; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; import java.math.BigInteger; import java.util.Map; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/FenceWithId.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/FenceWithId.java index 52d2d7a317..5a48228c7e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/FenceWithId.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/FenceWithId.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.HashSet; import java.util.Set; @@ -20,6 +20,7 @@ public FenceWithId(String name, Expression fenceID) { private FenceWithId(FenceWithId other) { super(other); + this.fenceID = other.fenceID; } public Expression getFenceID() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericVisibleEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericVisibleEvent.java index e4dba20ff4..db36451cc4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericVisibleEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/GenericVisibleEvent.java @@ -1,7 +1,8 @@ package com.dat3m.dartagnan.program.event.core; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class GenericVisibleEvent extends AbstractEvent { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/IfAsJump.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/IfAsJump.java index 17143815d1..b8aec499b5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/IfAsJump.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/IfAsJump.java @@ -1,7 +1,8 @@ package com.dat3m.dartagnan.program.event.core; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.google.common.base.Preconditions; import java.util.ArrayList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Init.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Init.java index d8885c5a84..4e4830253f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Init.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Init.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program.event.core; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.dat3m.dartagnan.program.memory.MemoryObject; /** diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Label.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Label.java index cb215b364a..22cbda4de6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Label.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Label.java @@ -1,7 +1,8 @@ package com.dat3m.dartagnan.program.event.core; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.Set; import java.util.stream.Collectors; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java index ea4ab939fa..9a3d7a1a0f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Load.java @@ -2,11 +2,11 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.MemoryAccess; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java index e9c256a44b..9384e991e6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Local.java @@ -4,10 +4,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.*; import com.google.common.base.Preconditions; import org.sosy_lab.java_smt.api.BooleanFormula; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryCoreEvent.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryCoreEvent.java index 770f8a326d..bf282e0bf4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryCoreEvent.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/MemoryCoreEvent.java @@ -3,9 +3,10 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.HashSet; import java.util.Objects; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStore.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStore.java similarity index 84% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStore.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStore.java index 02dbe65a77..e7f77ab6bc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStore.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStore.java @@ -1,12 +1,10 @@ -package com.dat3m.dartagnan.program.event.core.rmw; +package com.dat3m.dartagnan.program.event.core; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventUser; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.Load; -import com.dat3m.dartagnan.program.event.core.Store; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; import java.util.Map; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStoreExclusive.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStoreExclusive.java similarity index 89% rename from dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStoreExclusive.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStoreExclusive.java index f3fb47582a..75f80a4cea 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/rmw/RMWStoreExclusive.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/RMWStoreExclusive.java @@ -1,11 +1,10 @@ -package com.dat3m.dartagnan.program.event.core.rmw; +package com.dat3m.dartagnan.program.event.core; import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.Store; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import org.sosy_lab.java_smt.api.BooleanFormula; public class RMWStoreExclusive extends Store { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Skip.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Skip.java index 29345fa713..59860c8edd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Skip.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Skip.java @@ -1,6 +1,7 @@ package com.dat3m.dartagnan.program.event.core; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; public class Skip extends AbstractEvent { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java index da9c8618e9..4f7749cddc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Store.java @@ -3,10 +3,10 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.MemoryAccess; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.List; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/CodeAnnotation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/CodeAnnotation.java index 1f59ed632e..88147b1403 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/CodeAnnotation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/annotations/CodeAnnotation.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.core.annotations; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; /* Annotation events have no semantics (like skip). diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadArgument.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadArgument.java index f0dbfc49d0..0fbf80e526 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadArgument.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadArgument.java @@ -2,11 +2,7 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.*; import com.google.common.base.Preconditions; import org.sosy_lab.java_smt.api.BooleanFormula; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadCreate.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadCreate.java index 53b806c911..d91472fb34 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadCreate.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadCreate.java @@ -4,9 +4,9 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; +import com.dat3m.dartagnan.program.event.RegReader; import java.util.ArrayList; import java.util.HashSet; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadStart.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadStart.java index 8d2048d477..18d867e738 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadStart.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/threading/ThreadStart.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.program.event.core.threading; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.EventVisitor; import java.util.Map; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/AbortIf.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/AbortIf.java index 7c20769882..ec144dca91 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/AbortIf.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/AbortIf.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.RegReader; import com.google.common.base.Preconditions; import java.util.HashSet; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/FunctionCall.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/FunctionCall.java index d84d37d783..b09c07429f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/FunctionCall.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/FunctionCall.java @@ -7,8 +7,8 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Register.UsageType; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.RegReader; import com.google.common.base.Preconditions; import java.util.ArrayList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/Return.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/Return.java index 485928e5a2..ee12f25ac5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/Return.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/Return.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.RegReader; import java.util.HashSet; import java.util.Optional; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/ValueFunctionCall.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/ValueFunctionCall.java index 8c68a7d5da..864041c616 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/ValueFunctionCall.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/functions/ValueFunctionCall.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.type.FunctionType; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.RegWriter; import com.google.common.base.Preconditions; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java index a13f6f580a..228ceba3f7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java @@ -9,9 +9,9 @@ import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; import com.google.common.base.Preconditions; import org.sosy_lab.java_smt.api.BooleanFormula; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java index 085ca4b5de..e74113bc5a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicCmpXchg.java @@ -3,11 +3,11 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.MemoryAccess; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.SingleAccessMemoryEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java index f48c2ce519..f1b6df6ac9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class AtomicFetchOp extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java index 40a6a03ff8..da62486f14 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicLoad.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.LoadBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_ACQUIRE_RELEASE; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java index a3829c0f54..3830771397 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicStore.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program.event.lang.catomic; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.StoreBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_ACQUIRE; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicThreadFence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicThreadFence.java index b516b99290..ff96ccbd57 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicThreadFence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicThreadFence.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.catomic; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.FenceBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class AtomicThreadFence extends FenceBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java index 95229ca062..f9fba82771 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicXchg.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class AtomicXchg extends RMWXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMAddUnless.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMAddUnless.java index 6cdac006c0..c213c35a5a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMAddUnless.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMAddUnless.java @@ -3,11 +3,11 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.MemoryAccess; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.SingleAccessMemoryEvent; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMCmpXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMCmpXchg.java index 073d461ad5..c87f328889 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMCmpXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMCmpXchg.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWCmpXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMCmpXchg extends RMWCmpXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFence.java index 25173e59ae..8b21b8304e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFence.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.linux; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.FenceBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMFence extends FenceBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java index 35854f6acd..276e4bfd2a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMFetchOp extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java index 606e0fbfa8..10fa490e87 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLoad.java @@ -2,12 +2,12 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.LoadBase; import com.dat3m.dartagnan.program.event.core.Load; import com.dat3m.dartagnan.program.event.metadata.CustomPrinting; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.Optional; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java index 4c114beee1..a4826c8aca 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMLock.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.MemoryAccess; import com.dat3m.dartagnan.program.event.common.SingleAccessMemoryEvent; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMLock extends SingleAccessMemoryEvent { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java index 15f5d076a4..3e5b1c4319 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMOpAndTest extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java index 326a165d42..3b71319977 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWOpBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMOpNoReturn extends RMWOpBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java index c51002ff6f..604ada0356 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMOpReturn extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java index 94e0d45387..f60dcb802f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMStore.java @@ -1,12 +1,12 @@ package com.dat3m.dartagnan.program.event.lang.linux; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.StoreBase; import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.metadata.CustomPrinting; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.Optional; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java index 4ff829a35c..1c89e6a33b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMUnlock.java @@ -3,11 +3,11 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.StoreBase; import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.metadata.CustomPrinting; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.Optional; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMXchg.java index 54e6d4e7ee..8f651fa2cd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMXchg.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class LKMMXchg extends RMWXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java index ea4701ee55..fb43f87905 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmCmpXchg.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWCmpXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; // FIXME: This instruction writes to two registers, which we cannot express right now. diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmFence.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmFence.java index 753b07884d..6fae4afb38 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmFence.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmFence.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.llvm; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.FenceBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class LlvmFence extends FenceBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmLoad.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmLoad.java index b375fe33ad..3aeb71af69 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmLoad.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmLoad.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.LoadBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_ACQUIRE_RELEASE; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java index dd72af1ebe..3577ed3269 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.op.IOpBin; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class LlvmRMW extends RMWOpResultBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmStore.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmStore.java index 5ef9fffb66..5e2f3ba1d2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmStore.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmStore.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program.event.lang.llvm; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.StoreBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_ACQUIRE; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java index 4eff3ccd81..e5b897340d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmXchg.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWXchgBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import com.google.common.base.Preconditions; public class LlvmXchg extends RMWXchgBase { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java index b37ff88061..b377db8142 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/InitLock.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program.event.lang.pthread; import com.dat3m.dartagnan.expression.Expression; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.StoreBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_SC; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.java index 0a1fc2fdc1..f536121a5a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Lock.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.StoreBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_SC; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Unlock.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Unlock.java index c29e9c1ddf..b54e466bb7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Unlock.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/pthread/Unlock.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.type.TypeFactory; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.StoreBase; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import static com.dat3m.dartagnan.program.event.Tag.C11.MO_SC; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/BeginAtomic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/BeginAtomic.java index 143626a23a..37e286ff59 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/BeginAtomic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/BeginAtomic.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program.event.lang.svcomp; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; public class BeginAtomic extends AbstractEvent { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java index e02d44f99b..1abfa121fc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/EndAtomic.java @@ -2,10 +2,10 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.analysis.BranchEquivalence; +import com.dat3m.dartagnan.program.event.AbstractEvent; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.core.AbstractEvent; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.verification.Context; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/LoopBound.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/LoopBound.java index 758ed93c95..974d21c174 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/LoopBound.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/svcomp/LoopBound.java @@ -5,8 +5,8 @@ import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; import com.google.common.base.Preconditions; import java.util.HashSet; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/CustomPrinting.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/CustomPrinting.java index 4b0d3b3c8a..578db9f38f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/CustomPrinting.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/metadata/CustomPrinting.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.metadata; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import java.util.Optional; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/DifferenceFilter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/DifferenceFilter.java index fdd46a308b..b10947fe38 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/DifferenceFilter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/DifferenceFilter.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.filter; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; public class DifferenceFilter extends Filter { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java index 02a9bab13e..8c91a0514e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/Filter.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.filter; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import java.util.HashMap; import java.util.Map; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/IntersectionFilter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/IntersectionFilter.java index 04279cc00b..1c5aeb2897 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/IntersectionFilter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/IntersectionFilter.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.filter; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; public class IntersectionFilter extends Filter { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/TagFilter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/TagFilter.java index 4a5a2054b9..6d13d8bdc8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/TagFilter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/TagFilter.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.filter; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; public class TagFilter extends Filter { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/UnionFilter.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/UnionFilter.java index 76a817de2e..cc6d6ef7aa 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/UnionFilter.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/filter/UnionFilter.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.filter; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; public class UnionFilter extends Filter { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java index 5eea6736b7..9827f94f7e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java @@ -6,52 +6,52 @@ public class Location extends IExpr { - private final String name; - private final MemoryObject base; - private final int offset; - - public Location(String name, MemoryObject b, int o) { - super(TypeFactory.getInstance().getArchType()); - this.name = name; - base = b; - offset = o; - } - - public String getName() { - return name; - } - - public MemoryObject getMemoryObject() { - return base; - } - - public int getOffset() { - return offset; - } - - @Override - public T accept(ExpressionVisitor visitor) { - return visitor.visit(this); - } - - @Override - public String toString() { - return name; - } - - @Override - public int hashCode(){ - return base.hashCode() + offset; - } - - @Override - public boolean equals(Object obj) { - if (this == obj) { - return true; - } else if (obj == null || getClass() != obj.getClass()) { - return false; - } - Location o = (Location)obj; - return base.equals(o.base) && offset == o.offset; - } + private final String name; + private final MemoryObject base; + private final int offset; + + public Location(String name, MemoryObject b, int o) { + super(TypeFactory.getInstance().getArchType()); + this.name = name; + base = b; + offset = o; + } + + public String getName() { + return name; + } + + public MemoryObject getMemoryObject() { + return base; + } + + public int getOffset() { + return offset; + } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visit(this); + } + + @Override + public String toString() { + return name; + } + + @Override + public int hashCode() { + return base.hashCode() + offset; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) { + return true; + } else if (obj == null || getClass() != obj.getClass()) { + return false; + } + Location o = (Location) obj; + return base.equals(o.base) && offset == o.offset; + } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/BranchReordering.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/BranchReordering.java index f202211109..904d490b8c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/BranchReordering.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/BranchReordering.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.IRHelper; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; import com.google.common.collect.Lists; import org.sosy_lab.common.configuration.Configuration; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java index 0592584981..54fb3c59ec 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/CoreCodeVerification.java @@ -2,11 +2,9 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.program.Function; -import com.dat3m.dartagnan.program.event.core.FenceWithId; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument; import com.dat3m.dartagnan.program.event.core.threading.ThreadCreate; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java index 7dd4b0f74e..aaace28beb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DeadAssignmentElimination.java @@ -3,10 +3,10 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.Local; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.lang.Alloc; import com.google.common.collect.Lists; import org.sosy_lab.common.configuration.Configuration; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java index 29e546b4e6..88376e8531 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java @@ -9,13 +9,9 @@ import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; -import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.functions.FunctionCall; import com.dat3m.dartagnan.program.event.metadata.UnrollingId; import com.google.common.base.Preconditions; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java index 5fdbd161f5..227eff4fee 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java @@ -9,7 +9,7 @@ import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.memory.MemoryObject; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IdReassignment.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IdReassignment.java index d0b51d658d..4387cabb34 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IdReassignment.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/IdReassignment.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.google.common.collect.Iterables; public class IdReassignment implements ProgramProcessor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java index de3b28baa6..2d788e5333 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java @@ -8,13 +8,8 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.functions.AbortIf; import com.dat3m.dartagnan.program.event.functions.FunctionCall; import com.dat3m.dartagnan.program.event.functions.Return; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index cf7b8ade0d..8a4aea81a6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -7,9 +7,9 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.ExecutionStatus; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.functions.FunctionCall; @@ -20,25 +20,19 @@ import com.google.common.primitives.UnsignedLong; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; - -import java.math.BigInteger; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.EnumSet; -import java.util.List; -import java.util.Map; -import java.util.TreeSet; -import java.util.function.BiPredicate; -import java.util.stream.Collectors; - import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; +import java.math.BigInteger; +import java.util.*; +import java.util.function.BiPredicate; +import java.util.stream.Collectors; + +import static com.dat3m.dartagnan.configuration.OptionNames.REMOVE_ASSERTION_OF_TYPE; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; -import static com.dat3m.dartagnan.configuration.OptionNames.REMOVE_ASSERTION_OF_TYPE; /** * Manages a collection of all functions that the verifier can define itself, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java index 125bc3c500..90d7fb1b95 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LogThreadStatistics.java @@ -2,7 +2,11 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.core.*; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.core.GenericVisibleEvent; +import com.dat3m.dartagnan.program.event.core.Init; +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.core.annotations.CodeAnnotation; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.apache.logging.log4j.LogManager; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopFormVerification.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopFormVerification.java index d3384cc934..b841932d08 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopFormVerification.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopFormVerification.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; 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 d8f98735e5..ddd01311f6 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 @@ -4,11 +4,11 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.EventUser; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.lang.svcomp.LoopBound; import com.dat3m.dartagnan.program.event.metadata.UnrollingId; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java index 98bfe9198d..0b3b4cc350 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java @@ -10,24 +10,15 @@ import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.lang.Alloc; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; +import java.util.*; /* * Replaces memory accesses that involve addresses that are only used by one thread. diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java index 3265ef71a5..ef3c486cbe 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemoryAllocation.java @@ -6,9 +6,9 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Local; import com.dat3m.dartagnan.program.event.lang.Alloc; import com.dat3m.dartagnan.program.memory.Memory; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java index 4f2f8b99d2..f1e3b57b38 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java @@ -11,11 +11,11 @@ import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; import com.dat3m.dartagnan.program.event.functions.FunctionCall; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java index 8ff6289c43..1a55cf44db 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RegisterDecomposition.java @@ -8,10 +8,10 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.core.Local; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.lang.llvm.LlvmCmpXchg; import java.util.ArrayList; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java index 43250b4b0d..ff6c98bcb0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.Atom; import com.dat3m.dartagnan.expression.BExprUn; import com.dat3m.dartagnan.program.Function; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java index fc05a6d4c6..6a5dcb3fad 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadFunctions.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.memory.MemoryObject; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java index b29bae2cf7..b848361e4c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveUnusedMemory.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.Sets; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java index 9ef026c000..39d813ff80 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.expression.IValue; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Function; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.functions.ValueFunctionCall; import org.sosy_lab.common.configuration.Configuration; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java index d85da76e52..c0ed74d766 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java @@ -2,12 +2,12 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.functions.FunctionCall; import com.dat3m.dartagnan.program.event.lang.svcomp.SpinStart; import com.google.common.collect.Sets; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java index 4fdd8ef796..c48e06011c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.BConst; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Function; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.annotations.FunCallMarker; import com.dat3m.dartagnan.program.event.core.annotations.FunReturnMarker; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java index f7a8792bb1..17dc3f6e30 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java @@ -7,13 +7,13 @@ import com.dat3m.dartagnan.program.IRHelper; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.analysis.LoopAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.RegReader; +import com.dat3m.dartagnan.program.event.RegWriter; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Local; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.google.common.base.Preconditions; import com.google.common.base.Verify; import org.apache.logging.log4j.LogManager; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SymmetryReduction.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SymmetryReduction.java index 9f282d8929..a31921f743 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SymmetryReduction.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SymmetryReduction.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Assert; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java index 578b6cc051..273f89c795 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java @@ -14,16 +14,11 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.EventFactory; -import com.dat3m.dartagnan.program.event.EventUser; -import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Local; import com.dat3m.dartagnan.program.event.core.threading.ThreadCreate; import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.functions.AbortIf; import com.dat3m.dartagnan.program.event.functions.FunctionCall; import com.dat3m.dartagnan.program.event.functions.Return; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java index a19f0b0e02..1986100df4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java @@ -3,9 +3,9 @@ import com.dat3m.dartagnan.expression.BConst; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.functions.AbortIf; import com.dat3m.dartagnan.program.event.functions.Return; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java index 05df0d2e0b..81b44fb31e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/Compilation.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.metadata.CompilationId; import com.dat3m.dartagnan.program.processing.IdReassignment; import com.dat3m.dartagnan.program.processing.ProgramProcessor; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java index 94efc23c61..83d2f89931 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorArm8.java @@ -5,12 +5,12 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.Tag.ARMv8; import com.dat3m.dartagnan.program.event.Tag.C11; import com.dat3m.dartagnan.program.event.arch.StoreExclusive; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; import com.dat3m.dartagnan.program.event.lang.catomic.*; import com.dat3m.dartagnan.program.event.lang.linux.*; import com.dat3m.dartagnan.program.event.lang.llvm.*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java index f1ae66467e..cbad490516 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorBase.java @@ -7,20 +7,20 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.arch.StoreExclusive; import com.dat3m.dartagnan.program.event.arch.lisa.LISARMW; import com.dat3m.dartagnan.program.event.arch.tso.TSOXchg; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Load; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; +import com.dat3m.dartagnan.program.event.core.RMWStore; import com.dat3m.dartagnan.program.event.lang.linux.*; import com.dat3m.dartagnan.program.event.lang.llvm.LlvmLoad; import com.dat3m.dartagnan.program.event.lang.llvm.LlvmStore; import com.dat3m.dartagnan.program.event.lang.pthread.InitLock; import com.dat3m.dartagnan.program.event.lang.pthread.Lock; import com.dat3m.dartagnan.program.event.lang.pthread.Unlock; -import com.dat3m.dartagnan.program.event.visitors.EventVisitor; import java.util.Collections; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java index a7d1cca697..a74c66eee1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorC11.java @@ -4,9 +4,10 @@ import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.Tag.C11; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; import com.dat3m.dartagnan.program.event.lang.catomic.*; import com.dat3m.dartagnan.program.event.lang.llvm.*; import com.dat3m.dartagnan.program.event.metadata.MemoryOrder; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java index aa8fee3b7b..f6d6166bff 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorIMM.java @@ -4,6 +4,7 @@ import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.Tag.C11; import com.dat3m.dartagnan.program.event.Tag.IMM; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java index 90f329fbac..5b6dd0d288 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorLKMM.java @@ -6,10 +6,13 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; +import com.dat3m.dartagnan.program.event.core.Label; +import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.RMWStore; +import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.lang.linux.*; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java index 244cf5c18c..a4b90d00cc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java @@ -2,11 +2,14 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.arch.ptx.*; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomCAS; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomExch; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXAtomOp; +import com.dat3m.dartagnan.program.event.arch.ptx.PTXRedOp; import com.dat3m.dartagnan.program.event.core.Load; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; +import com.dat3m.dartagnan.program.event.core.RMWStore; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java index 5cc3fc9d7b..f3d909c5fb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPower.java @@ -5,6 +5,7 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.Tag.C11; import com.dat3m.dartagnan.program.event.core.*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java index a188c24052..2ad05fc87d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorRISCV.java @@ -5,10 +5,10 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.arch.StoreExclusive; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; import com.dat3m.dartagnan.program.event.lang.catomic.*; import com.dat3m.dartagnan.program.event.lang.linux.*; import com.dat3m.dartagnan.program.event.lang.llvm.*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java index 6c6b12b3ed..206c05442f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorTso.java @@ -5,6 +5,8 @@ import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.arch.tso.TSOXchg; import com.dat3m.dartagnan.program.event.core.*; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java index a8842938c1..fdff445e2c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java @@ -2,13 +2,13 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Register; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMW; import com.dat3m.dartagnan.program.event.arch.vulkan.VulkanRMWOp; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.Load; +import com.dat3m.dartagnan.program.event.core.RMWStore; import com.dat3m.dartagnan.program.event.core.Store; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; import java.util.List; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AbstractAssert.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AbstractAssert.java index 4b3d6c8aed..3cbbab5458 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AbstractAssert.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AbstractAssert.java @@ -1,11 +1,10 @@ package com.dat3m.dartagnan.program.specification; -import java.util.List; - import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.Register; import org.sosy_lab.java_smt.api.BooleanFormula; -import com.dat3m.dartagnan.program.Register; +import java.util.List; public abstract class AbstractAssert { @@ -15,23 +14,24 @@ public abstract class AbstractAssert { private String type; - public void setType(String type){ + public void setType(String type) { this.type = type; } - public String getType(){ + + public String getType() { return type; } - public boolean isSafetySpec(){ + public boolean isSafetySpec() { // "Forall" queries are safety specs, while existential ones are not. return ASSERT_TYPE_FORALL.equals(type) || ASSERT_TYPE_NOT_EXISTS.equals(type); } - public String toStringWithType(){ + public String toStringWithType() { return type != null ? (type + " (" + this + ")") : toString(); } public abstract BooleanFormula encode(EncodingContext context); - + public abstract List getRegs(); } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java index 2e29f9a17b..f4f6771a8b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java @@ -15,7 +15,7 @@ public class AssertBasic extends AbstractAssert { private final Expression e2; private final COpBin op; - public AssertBasic(Expression e1, COpBin op, Expression e2){ + public AssertBasic(Expression e1, COpBin op, Expression e2) { this.e1 = e1; this.e2 = e2; this.op = op; @@ -29,26 +29,26 @@ public BooleanFormula encode(EncodingContext context) { } @Override - public String toString(){ + public String toString() { return valueToString(e1) + op + valueToString(e2); } - private String valueToString(Expression value){ - if(value instanceof Register register){ + private String valueToString(Expression value) { + if (value instanceof Register register) { return register.getFunction().getId() + ":" + value; } return value.toString(); } - @Override - public List getRegs() { - List regs = new ArrayList<>(); - if(e1 instanceof Register r1) { - regs.add(r1); - } - if(e2 instanceof Register r2) { - regs.add(r2); - } - return regs; - } + @Override + public List getRegs() { + List regs = new ArrayList<>(); + if (e1 instanceof Register r1) { + regs.add(r1); + } + if (e2 instanceof Register r2) { + regs.add(r2); + } + return regs; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeAnd.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeAnd.java index 8138c2610e..7c323ba3e6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeAnd.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeAnd.java @@ -1,19 +1,18 @@ package com.dat3m.dartagnan.program.specification; -import java.util.ArrayList; -import java.util.List; - import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.Register; import org.sosy_lab.java_smt.api.BooleanFormula; -import com.dat3m.dartagnan.program.Register; +import java.util.ArrayList; +import java.util.List; public class AssertCompositeAnd extends AbstractAssert { private final AbstractAssert a1; private final AbstractAssert a2; - public AssertCompositeAnd(AbstractAssert a1, AbstractAssert a2){ + public AssertCompositeAnd(AbstractAssert a1, AbstractAssert a2) { this.a1 = a1; this.a2 = a2; } @@ -27,12 +26,12 @@ public BooleanFormula encode(EncodingContext ctx) { public String toString() { return a1 + " && " + a2; } - - @Override - public List getRegs() { - List regs = new ArrayList<>(); - regs.addAll(a1.getRegs()); - regs.addAll(a2.getRegs()); - return regs; - } + + @Override + public List getRegs() { + List regs = new ArrayList<>(); + regs.addAll(a1.getRegs()); + regs.addAll(a2.getRegs()); + return regs; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeOr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeOr.java index bb0c6229b0..991cd0f71e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeOr.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertCompositeOr.java @@ -1,19 +1,18 @@ package com.dat3m.dartagnan.program.specification; -import java.util.ArrayList; -import java.util.List; - import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.Register; import org.sosy_lab.java_smt.api.BooleanFormula; -import com.dat3m.dartagnan.program.Register; +import java.util.ArrayList; +import java.util.List; public class AssertCompositeOr extends AbstractAssert { private final AbstractAssert a1; private final AbstractAssert a2; - public AssertCompositeOr(AbstractAssert a1, AbstractAssert a2){ + public AssertCompositeOr(AbstractAssert a1, AbstractAssert a2) { this.a1 = a1; this.a2 = a2; } @@ -29,10 +28,10 @@ public String toString() { } @Override - public List getRegs() { - List regs = new ArrayList<>(); - regs.addAll(a1.getRegs()); - regs.addAll(a2.getRegs()); - return regs; - } + public List getRegs() { + List regs = new ArrayList<>(); + regs.addAll(a1.getRegs()); + regs.addAll(a2.getRegs()); + return regs; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java index 426498302f..0fcaeba3ea 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertInline.java @@ -2,7 +2,6 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.program.Register; -import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Assert; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; @@ -14,7 +13,7 @@ public class AssertInline extends AbstractAssert { private final Assert assertion; - public AssertInline(Assert assertion){ + public AssertInline(Assert assertion) { this.assertion = assertion; } @@ -26,7 +25,7 @@ public BooleanFormula encode(EncodingContext ctx) { } @Override - public String toString(){ + public String toString() { return String.format("%s@%d", assertion.getExpression(), assertion.getGlobalId()); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertNot.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertNot.java index 3171c9b74a..db89e1930b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertNot.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertNot.java @@ -1,29 +1,28 @@ package com.dat3m.dartagnan.program.specification; -import java.util.List; - import com.dat3m.dartagnan.encoding.EncodingContext; -import org.sosy_lab.java_smt.api.BooleanFormula; - import com.dat3m.dartagnan.program.Register; import com.google.common.base.Preconditions; +import org.sosy_lab.java_smt.api.BooleanFormula; + +import java.util.List; public class AssertNot extends AbstractAssert { private final AbstractAssert child; - public AssertNot(AbstractAssert child){ - Preconditions.checkNotNull(child, "Empty assertion clause in " + this.getClass().getName()); + public AssertNot(AbstractAssert child) { + Preconditions.checkNotNull(child, "Empty assertion clause in " + this.getClass().getName()); this.child = child; } - AbstractAssert getChild(){ + AbstractAssert getChild() { return child; } @Override public BooleanFormula encode(EncodingContext ctx) { - return ctx.getBooleanFormulaManager().not(child.encode(ctx)); + return ctx.getBooleanFormulaManager().not(child.encode(ctx)); } @Override @@ -32,7 +31,7 @@ public String toString() { } @Override - public List getRegs() { - return child.getRegs(); - } + public List getRegs() { + return child.getRegs(); + } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertTrue.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertTrue.java index 1e82b8ac51..0fc5bbc12d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertTrue.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertTrue.java @@ -1,12 +1,11 @@ package com.dat3m.dartagnan.program.specification; -import java.util.Collections; -import java.util.List; - import com.dat3m.dartagnan.encoding.EncodingContext; +import com.dat3m.dartagnan.program.Register; import org.sosy_lab.java_smt.api.BooleanFormula; -import com.dat3m.dartagnan.program.Register; +import java.util.Collections; +import java.util.List; public class AssertTrue extends AbstractAssert { @@ -16,12 +15,12 @@ public BooleanFormula encode(EncodingContext ctx) { } @Override - public String toString(){ + public String toString() { return "true"; } @Override - public List getRegs() { - return Collections.emptyList(); - } + public List getRegs() { + return Collections.emptyList(); + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index cf2ca89980..6bb1837da0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -31,7 +31,7 @@ import java.util.List; import java.util.Set; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; public class ExecutionGraph { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/RMWGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/RMWGraph.java index 8fb1ed23b2..ba40524879 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/RMWGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/basePredicates/RMWGraph.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.solver.caat4wmm.basePredicates; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; +import com.dat3m.dartagnan.program.event.core.RMWStore; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge; import com.dat3m.dartagnan.verification.model.EventData; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/AddressLiteral.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/AddressLiteral.java index 8a04dcd678..5d55b3f51c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/AddressLiteral.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/AddressLiteral.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.solver.caat4wmm.coreReasoning; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.utils.logic.AbstractLiteral; import com.dat3m.dartagnan.wmm.utils.Tuple; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java index 73574f7e82..03c53ced97 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge; import com.dat3m.dartagnan.solver.caat.reasoning.CAATLiteral; import com.dat3m.dartagnan.solver.caat.reasoning.EdgeLiteral; @@ -24,7 +24,7 @@ import java.util.function.Function; import static com.dat3m.dartagnan.GlobalSettings.REFINEMENT_SYMMETRIC_LEARNING; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; // The CoreReasoner transforms base reasons of the CAATSolver to core reason of the WMMSolver. public class CoreReasoner { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/ExecLiteral.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/ExecLiteral.java index fdea3a8915..398e469754 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/ExecLiteral.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/ExecLiteral.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.solver.caat4wmm.coreReasoning; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.utils.logic.AbstractDataLiteral; /* diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/RelLiteral.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/RelLiteral.java index 6b0b4b9568..57c81c8c7a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/RelLiteral.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/RelLiteral.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.solver.caat4wmm.coreReasoning; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.utils.logic.AbstractDataLiteral; import com.dat3m.dartagnan.wmm.utils.Tuple; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java index ef60326ca8..8ff3aa4361 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/printer/Printer.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Init; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Skip; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/symmetry/CoSymmetryBreaking.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/symmetry/CoSymmetryBreaking.java index db423bc47c..2a2bdb0be8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/symmetry/CoSymmetryBreaking.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/symmetry/CoSymmetryBreaking.java @@ -5,14 +5,14 @@ import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import com.dat3m.dartagnan.verification.VerificationTask; import com.dat3m.dartagnan.wmm.Relation; +import com.dat3m.dartagnan.wmm.RelationNameRepository; import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.axiom.Axiom; -import com.dat3m.dartagnan.wmm.relation.RelationNameRepository; import com.dat3m.dartagnan.wmm.utils.Tuple; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java index 2664865830..368900784f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventData.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.verification.model; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; -import com.dat3m.dartagnan.program.event.core.Event; import java.math.BigInteger; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventMap.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventMap.java index 3d8e7a50e8..cc2695aa0e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventMap.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/EventMap.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.verification.model; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import java.util.Collection; import java.util.HashMap; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java index bf4174ff2e..fcc2635b8a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModel.java @@ -4,11 +4,9 @@ import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.event.Tag; +import com.dat3m.dartagnan.program.event.*; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.core.threading.ThreadArgument; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; -import com.dat3m.dartagnan.program.event.core.utils.RegWriter; import com.dat3m.dartagnan.program.event.lang.svcomp.BeginAtomic; import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic; import com.dat3m.dartagnan.program.filter.Filter; @@ -31,8 +29,8 @@ import java.util.*; import java.util.stream.Collectors; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.CO; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.RF; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; import static com.google.common.base.Preconditions.checkNotNull; /* diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java index b981af6e03..c68e5e09bb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java @@ -8,8 +8,8 @@ import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.*; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Assert; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.processing.ProcessingManager; import com.dat3m.dartagnan.program.specification.AbstractAssert; import com.dat3m.dartagnan.program.specification.AssertCompositeAnd; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 9c737406de..447be2bff1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -8,8 +8,8 @@ import com.dat3m.dartagnan.program.analysis.BranchEquivalence; import com.dat3m.dartagnan.program.analysis.SyntacticContextAnalysis; import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; -import com.dat3m.dartagnan.program.event.core.Event; -import com.dat3m.dartagnan.program.event.core.MemoryEvent; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; import com.dat3m.dartagnan.program.filter.Filter; @@ -57,7 +57,7 @@ import static com.dat3m.dartagnan.solver.caat.CAATSolver.Status.*; import static com.dat3m.dartagnan.utils.Result.*; import static com.dat3m.dartagnan.utils.visualization.ExecutionGraphVisualizer.generateGraphvizFile; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; ; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java index c11f364e3d..3802beeacd 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java @@ -4,9 +4,9 @@ import com.dat3m.dartagnan.expression.BConst; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.core.Assert; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.core.Store; import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java index 9b1d2d2485..3ed0724187 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Relation.java @@ -10,7 +10,7 @@ import java.util.List; import java.util.Optional; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; import static com.google.common.base.Preconditions.checkState; public final class Relation implements Dependent { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java new file mode 100644 index 0000000000..bbda22bf9c --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java @@ -0,0 +1,77 @@ +package com.dat3m.dartagnan.wmm; + +import com.google.common.collect.ImmutableSet; + +import java.util.Arrays; + +public class RelationNameRepository { + + public static final String PO = "po"; + public static final String LOC = "loc"; + public static final String ID = "id"; + public static final String INT = "int"; + public static final String EXT = "ext"; + public static final String CO = "co"; + public static final String RF = "rf"; + public static final String RMW = "rmw"; + public static final String CRIT = "rcu-rscs"; + public static final String IDD = "idd"; + public static final String ADDRDIRECT = "addrDirect"; + public static final String CTRLDIRECT = "ctrlDirect"; + public static final String EMPTY = "0"; + public static final String RFINV = "rf^-1"; + public static final String FR = "fr"; + public static final String MM = "(M*M)"; + public static final String MV = "(M*V)"; + public static final String IDDTRANS = "idd^+"; + public static final String DATA = "data"; + public static final String ADDR = "addr"; + public static final String CTRL = "ctrl"; + public static final String POLOC = "po-loc"; + public static final String RFE = "rfe"; + public static final String RFI = "rfi"; + public static final String COE = "coe"; + public static final String COI = "coi"; + public static final String FRE = "fre"; + public static final String FRI = "fri"; + public static final String MFENCE = "mfence"; + public static final String ISH = "ish"; + public static final String ISB = "isb"; + public static final String SYNC = "sync"; + public static final String ISYNC = "isync"; + public static final String LWSYNC = "lwsync"; + public static final String CTRLISYNC = "ctrlisync"; + public static final String CTRLISB = "ctrlisb"; + public static final String CASDEP = "casdep"; + public static final String SR = "sr"; + public static final String SCTA = "scta"; // same-cta, the same as same_block_r in alloy + public static final String SSG = "ssg"; + public static final String SWG = "swg"; + public static final String SQF = "sqf"; + public static final String SSW = "ssw"; + public static final String SYNC_BARRIER = "sync_barrier"; + public static final String SYNC_FENCE = "sync_fence"; + public static final String SYNCBAR = "syncbar"; + public static final String VLOC = "vloc"; + + public static final ImmutableSet RELATION_NAMES; + + static { + // CARE: Using reflection inside the class initializer is dangerous, + // but it works here because all constants get initialized before the initializer runs. + RELATION_NAMES = Arrays.stream(RelationNameRepository.class.getDeclaredFields()) + .filter(f -> f.getType().equals(String.class)) + .map(f -> { + try { + return (String) f.get(null); + } catch (IllegalAccessException e) { + throw new RuntimeException(e); + } + }).collect(ImmutableSet.toImmutableSet()); + } + + public static boolean contains(String name) { + return RELATION_NAMES.contains(name); + } + +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java index 94945d1b94..59bf6b544d 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java @@ -4,7 +4,6 @@ import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.wmm.axiom.Axiom; import com.dat3m.dartagnan.wmm.definition.*; -import com.dat3m.dartagnan.wmm.relation.RelationNameRepository; import com.google.common.collect.ImmutableSet; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -20,7 +19,7 @@ import static com.dat3m.dartagnan.configuration.OptionNames.ENABLE_ACTIVE_SETS; import static com.dat3m.dartagnan.configuration.OptionNames.REDUCE_ACYCLICITY_ENCODE_SETS; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Verify.verify; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java index 6df95832b0..125927f23f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/RelationAnalysis.java @@ -8,13 +8,11 @@ import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; +import com.dat3m.dartagnan.program.event.Event; +import com.dat3m.dartagnan.program.event.MemoryEvent; +import com.dat3m.dartagnan.program.event.RegReader; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.FenceWithId; import com.dat3m.dartagnan.program.event.core.*; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStore; -import com.dat3m.dartagnan.program.event.core.rmw.RMWStoreExclusive; -import com.dat3m.dartagnan.program.event.core.threading.ThreadStart; -import com.dat3m.dartagnan.program.event.core.utils.RegReader; import com.dat3m.dartagnan.program.event.lang.svcomp.EndAtomic; import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.program.memory.VirtualMemoryObject; @@ -28,8 +26,8 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.axiom.Axiom; import com.dat3m.dartagnan.wmm.definition.Difference; -import com.dat3m.dartagnan.wmm.utils.Tuple; import com.dat3m.dartagnan.wmm.utils.EventGraph; +import com.dat3m.dartagnan.wmm.utils.Tuple; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; @@ -44,8 +42,8 @@ import static com.dat3m.dartagnan.configuration.OptionNames.*; import static com.dat3m.dartagnan.program.Register.UsageType.*; import static com.dat3m.dartagnan.program.event.Tag.*; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.CO; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.RF; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.RF; import static com.dat3m.dartagnan.wmm.utils.EventGraph.difference; import static com.dat3m.dartagnan.wmm.utils.EventGraph.intersection; import static com.google.common.base.Preconditions.checkNotNull; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java index 3e168c0f11..e45027fe30 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/axiom/Acyclic.java @@ -2,8 +2,8 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.utils.dependable.DependencyGraph; import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Relation; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DifferentThreads.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DifferentThreads.java index f493dd8065..2e8886c3c4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DifferentThreads.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DifferentThreads.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.EXT; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.EXT; public class DifferentThreads extends Definition { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java index c020cecf1e..c6e38f2800 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/DirectControlDependency.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.CTRLDIRECT; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CTRLDIRECT; //TODO: We can restrict the codomain to visible events as the only usage of this Relation is in // ctrl := idd^+;ctrlDirect & (R*V) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Empty.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Empty.java index 85a848a0a1..281292276c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Empty.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Empty.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; -import com.dat3m.dartagnan.wmm.relation.RelationNameRepository; +import com.dat3m.dartagnan.wmm.RelationNameRepository; public class Empty extends Definition { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameThread.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameThread.java index dc06d28448..7b38b1e8e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameThread.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SameThread.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.wmm.Definition; import com.dat3m.dartagnan.wmm.Relation; -import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.INT; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.INT; public class SameThread extends Definition { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java deleted file mode 100644 index dca41d18ca..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/relation/RelationNameRepository.java +++ /dev/null @@ -1,77 +0,0 @@ -package com.dat3m.dartagnan.wmm.relation; - -import com.google.common.collect.ImmutableSet; - -import java.util.Arrays; - -public class RelationNameRepository { - - public static final String PO = "po"; - public static final String LOC = "loc"; - public static final String ID = "id"; - public static final String INT = "int"; - public static final String EXT = "ext"; - public static final String CO = "co"; - public static final String RF = "rf"; - public static final String RMW = "rmw"; - public static final String CRIT = "rcu-rscs"; - public static final String IDD = "idd"; - public static final String ADDRDIRECT = "addrDirect"; - public static final String CTRLDIRECT = "ctrlDirect"; - public static final String EMPTY = "0"; - public static final String RFINV = "rf^-1"; - public static final String FR = "fr"; - public static final String MM = "(M*M)"; - public static final String MV = "(M*V)"; - public static final String IDDTRANS = "idd^+"; - public static final String DATA = "data"; - public static final String ADDR = "addr"; - public static final String CTRL = "ctrl"; - public static final String POLOC = "po-loc"; - public static final String RFE = "rfe"; - public static final String RFI = "rfi"; - public static final String COE = "coe"; - public static final String COI = "coi"; - public static final String FRE = "fre"; - public static final String FRI = "fri"; - public static final String MFENCE = "mfence"; - public static final String ISH = "ish"; - public static final String ISB = "isb"; - public static final String SYNC = "sync"; - public static final String ISYNC = "isync"; - public static final String LWSYNC = "lwsync"; - public static final String CTRLISYNC = "ctrlisync"; - public static final String CTRLISB = "ctrlisb"; - public static final String CASDEP = "casdep"; - public static final String SR = "sr"; - public static final String SCTA = "scta"; // same-cta, the same as same_block_r in alloy - public static final String SSG = "ssg"; - public static final String SWG = "swg"; - public static final String SQF = "sqf"; - public static final String SSW = "ssw"; - public static final String SYNC_BARRIER = "sync_barrier"; - public static final String SYNC_FENCE = "sync_fence"; - public static final String SYNCBAR = "syncbar"; - public static final String VLOC = "vloc"; - - public static final ImmutableSet RELATION_NAMES; - - static { - // CARE: Using reflection inside the class initializer is dangerous, - // but it works here because all constants get initialized before the initializer runs. - RELATION_NAMES = Arrays.stream(RelationNameRepository.class.getDeclaredFields()) - .filter(f -> f.getType().equals(String.class)) - .map(f -> { - try { - return (String)f.get(null); - } catch (IllegalAccessException e) { - throw new RuntimeException(e); - } - }).collect(ImmutableSet.toImmutableSet()); - } - - public static boolean contains(String name) { - return RELATION_NAMES.contains(name); - } - -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java index 8fdc8ddb08..174947e4d4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraph.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.wmm.utils; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import java.util.Collections; import java.util.Set; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java index 01d18fcfe1..461e692dce 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/EventGraph.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.wmm.utils; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import java.util.*; import java.util.function.BiConsumer; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Tuple.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Tuple.java index f40fcb1121..035c4c910c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Tuple.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/Tuple.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.wmm.utils; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; public record Tuple(Event first, Event second) implements Comparable { diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java index 1ad7fd2eb2..4319f86b5f 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/compilation/AbstractCompilationTest.java @@ -3,8 +3,8 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.configuration.Property; import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.utils.ResourceHelper; import com.dat3m.dartagnan.utils.rules.Provider; import com.dat3m.dartagnan.utils.rules.Providers; 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 1f990d710a..2c90f0d275 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -14,6 +14,7 @@ import com.dat3m.dartagnan.program.analysis.Dependency; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; import com.dat3m.dartagnan.program.analysis.alias.AliasAnalysis; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.EventFactory; import com.dat3m.dartagnan.program.event.core.*; import com.dat3m.dartagnan.program.event.metadata.OriginalId; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java index 779d285f76..867fd920f7 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EmptyEventGraphTest.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.wmm.utils; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Skip; import org.junit.Test; diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java index cf9d90a91e..54945cd4c3 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/wmm/utils/EventGraphTest.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.wmm.utils; -import com.dat3m.dartagnan.program.event.core.Event; +import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.Skip; import org.junit.Test;