From b2bee3df6639892d532b73709ffdd69b85c32aa9 Mon Sep 17 00:00:00 2001 From: Matthias Heizmann Date: Fri, 30 Aug 2024 06:41:50 +0200 Subject: [PATCH 1/4] Let AtomicBlockInfo use more precise types Use IIcfgTransition instead of IElement because this annotation is always written to edges. --- .../rcfgbuilder/cfg/AtomicBlockInfo.java | 54 ++++++++----------- .../generator/rcfgbuilder/cfg/CfgBuilder.java | 10 ++-- 2 files changed, 27 insertions(+), 37 deletions(-) diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java index 0b6331194d1..977f67c1119 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java @@ -31,9 +31,10 @@ import java.util.function.IntPredicate; import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.ModernAnnotations; -import de.uni_freiburg.informatik.ultimate.core.model.models.IElement; import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils; import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition; +import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IcfgLocation; /** * An annotation used to mark CFG edges that are the beginning or end of an atomic block, in the sense of SV-COMP's @@ -86,8 +87,8 @@ public String toString() { * The element whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks the beginning of an atomic block. */ - public static boolean isStartOfAtomicBlock(final IElement element) { - return hasAnnotatedDelta(element, d -> d > 0); + public static boolean isStartOfAtomicBlock(final IIcfgTransition edge) { + return hasAnnotatedDelta(edge, d -> d > 0); } /** @@ -99,75 +100,64 @@ public static boolean isStartOfAtomicBlock(final IElement element) { * The element whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks the end of an atomic block. */ - public static boolean isEndOfAtomicBlock(final IElement element) { - return hasAnnotatedDelta(element, d -> d < 0); + public static boolean isEndOfAtomicBlock(final IIcfgTransition edge) { + return hasAnnotatedDelta(edge, d -> d < 0); } /** * Determines if the given element (an edge) is annotated as the result of a complete atomic block composition. - * - * @param element - * The element whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks a complete atomic block. */ - public static boolean isCompleteAtomicBlock(final IElement element) { - return hasAnnotatedDelta(element, d -> d == 0); + public static boolean isCompleteAtomicBlock(final IIcfgTransition edge) { + return hasAnnotatedDelta(edge, d -> d == 0); } /** * Marks the given element (an edge) as the beginning of an atomic block. - * - * @param element - * The edge to be marked. */ - public static void addBeginAnnotation(final IElement element) { - addAnnotation(element, START_DELTA); + public static void addBeginAnnotation(final IIcfgTransition edge) { + addAnnotation(edge, START_DELTA); } /** * Marks the given element (an edge) as the end of an atomic block. * - * @param element - * The edge to be marked. */ - public static void addEndAnnotation(final IElement element) { - addAnnotation(element, END_DELTA); + public static void addEndAnnotation(final IIcfgTransition edge) { + addAnnotation(edge, END_DELTA); } /** * Marks the given element (an edge) as the result of a complete atomic block composition. * - * @param element - * The edge to be marked. */ - public static void addCompleteAnnotation(final IElement element) { - addAnnotation(element, 0); + public static void addCompleteAnnotation(final IIcfgTransition edge) { + addAnnotation(edge, 0); } /** * Removes any {@link AtomicBlockInfo} annotation, if present. * - * @param element - * The edge from which annotations shall be removed */ - public static void removeAnnotation(final IElement element) { - element.getPayload().getAnnotations().remove(AtomicBlockInfo.class.getName()); + public static void removeAnnotation(final IIcfgTransition edge) { + edge.getPayload().getAnnotations().remove(AtomicBlockInfo.class.getName()); } - private static boolean hasAnnotatedDelta(final IElement element, final IntPredicate condition) { - final AtomicBlockInfo annotation = ModelUtils.getAnnotation(element, AtomicBlockInfo.class); + private static boolean hasAnnotatedDelta(final IIcfgTransition edge, + final IntPredicate condition) { + final AtomicBlockInfo annotation = ModelUtils.getAnnotation(edge, AtomicBlockInfo.class); if (annotation != null) { return condition.test(annotation.mDelta); } return false; } - private static void addAnnotation(final IElement element, final int delta) { - final var previous = ModelUtils.getAnnotation(element, AtomicBlockInfo.class); + private static void addAnnotation(final IIcfgTransition edge, final int delta) { + final var previous = ModelUtils.getAnnotation(edge, AtomicBlockInfo.class); if (previous != null) { throw new UnsupportedOperationException( "Incompatible atomic block annotation: " + previous.mDelta + " and " + delta); } - element.getPayload().getAnnotations().put(AtomicBlockInfo.class.getName(), new AtomicBlockInfo(delta)); + edge.getPayload().getAnnotations().put(AtomicBlockInfo.class.getName(), new AtomicBlockInfo(delta)); } } diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 1df360a93cb..0fb484a9496 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -1527,7 +1527,7 @@ private void beginAtomicBlock(final Statement st) { assert mCurrent instanceof CodeBlock : "Start marker for atomic section must be an edge"; // mark current edge as start of atomic block - AtomicBlockInfo.addBeginAnnotation(mCurrent); + AtomicBlockInfo.addBeginAnnotation((IIcfgTransition) mCurrent); } private void endAtomicBlock(final Statement st) { @@ -1537,13 +1537,13 @@ private void endAtomicBlock(final Statement st) { } assert mCurrent instanceof CodeBlock : "End marker for atomic section must be an edge"; - if (AtomicBlockInfo.isStartOfAtomicBlock(mCurrent)) { + if (AtomicBlockInfo.isEndOfAtomicBlock((IIcfgTransition) mCurrent)) { // if current edge is both start and end of an atomic block, it is already atomic -- nothing else to do - AtomicBlockInfo.removeAnnotation(mCurrent); - AtomicBlockInfo.addCompleteAnnotation(mCurrent); + AtomicBlockInfo.removeAnnotation((IIcfgTransition) mCurrent); + AtomicBlockInfo.addCompleteAnnotation((IIcfgTransition) mCurrent); } else { // mark current edge as end of atomic block - AtomicBlockInfo.addEndAnnotation(mCurrent); + AtomicBlockInfo.addEndAnnotation((IIcfgTransition) mCurrent); } // ensure nothing is appended to current edge From 050258ae3d632aa996a5f081f549bbadb125b0bb Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Fri, 30 Aug 2024 17:58:18 +0200 Subject: [PATCH 2/4] simplify: omit unnecessary type parameter --- .../rcfgbuilder/cfg/AtomicBlockInfo.java | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java index 977f67c1119..d614df24528 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java @@ -34,7 +34,6 @@ import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils; import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations; import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IIcfgTransition; -import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.structure.IcfgLocation; /** * An annotation used to mark CFG edges that are the beginning or end of an atomic block, in the sense of SV-COMP's @@ -87,7 +86,7 @@ public String toString() { * The element whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks the beginning of an atomic block. */ - public static boolean isStartOfAtomicBlock(final IIcfgTransition edge) { + public static boolean isStartOfAtomicBlock(final IIcfgTransition edge) { return hasAnnotatedDelta(edge, d -> d > 0); } @@ -100,22 +99,23 @@ public static boolean isStartOfAtomicBlock(final IIcf * The element whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks the end of an atomic block. */ - public static boolean isEndOfAtomicBlock(final IIcfgTransition edge) { + public static boolean isEndOfAtomicBlock(final IIcfgTransition edge) { return hasAnnotatedDelta(edge, d -> d < 0); } /** * Determines if the given element (an edge) is annotated as the result of a complete atomic block composition. + * * @return true if there is an {@link AtomicBlockInfo} annotation that marks a complete atomic block. */ - public static boolean isCompleteAtomicBlock(final IIcfgTransition edge) { + public static boolean isCompleteAtomicBlock(final IIcfgTransition edge) { return hasAnnotatedDelta(edge, d -> d == 0); } /** * Marks the given element (an edge) as the beginning of an atomic block. */ - public static void addBeginAnnotation(final IIcfgTransition edge) { + public static void addBeginAnnotation(final IIcfgTransition edge) { addAnnotation(edge, START_DELTA); } @@ -123,7 +123,7 @@ public static void addBeginAnnotation(final IIcfgTra * Marks the given element (an edge) as the end of an atomic block. * */ - public static void addEndAnnotation(final IIcfgTransition edge) { + public static void addEndAnnotation(final IIcfgTransition edge) { addAnnotation(edge, END_DELTA); } @@ -131,7 +131,7 @@ public static void addEndAnnotation(final IIcfgTrans * Marks the given element (an edge) as the result of a complete atomic block composition. * */ - public static void addCompleteAnnotation(final IIcfgTransition edge) { + public static void addCompleteAnnotation(final IIcfgTransition edge) { addAnnotation(edge, 0); } @@ -139,12 +139,11 @@ public static void addCompleteAnnotation(final IIcfg * Removes any {@link AtomicBlockInfo} annotation, if present. * */ - public static void removeAnnotation(final IIcfgTransition edge) { + public static void removeAnnotation(final IIcfgTransition edge) { edge.getPayload().getAnnotations().remove(AtomicBlockInfo.class.getName()); } - private static boolean hasAnnotatedDelta(final IIcfgTransition edge, - final IntPredicate condition) { + private static boolean hasAnnotatedDelta(final IIcfgTransition edge, final IntPredicate condition) { final AtomicBlockInfo annotation = ModelUtils.getAnnotation(edge, AtomicBlockInfo.class); if (annotation != null) { return condition.test(annotation.mDelta); @@ -152,7 +151,7 @@ private static boolean hasAnnotatedDelta(final IIcfgT return false; } - private static void addAnnotation(final IIcfgTransition edge, final int delta) { + private static void addAnnotation(final IIcfgTransition edge, final int delta) { final var previous = ModelUtils.getAnnotation(edge, AtomicBlockInfo.class); if (previous != null) { throw new UnsupportedOperationException( From c68dfa26998ad12fc910b6a23d697cb6700d1245 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Fri, 30 Aug 2024 17:59:24 +0200 Subject: [PATCH 3/4] undo accidental change of method --- .../ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java index 0fb484a9496..910a380194f 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/CfgBuilder.java @@ -1537,7 +1537,7 @@ private void endAtomicBlock(final Statement st) { } assert mCurrent instanceof CodeBlock : "End marker for atomic section must be an edge"; - if (AtomicBlockInfo.isEndOfAtomicBlock((IIcfgTransition) mCurrent)) { + if (AtomicBlockInfo.isStartOfAtomicBlock((IIcfgTransition) mCurrent)) { // if current edge is both start and end of an atomic block, it is already atomic -- nothing else to do AtomicBlockInfo.removeAnnotation((IIcfgTransition) mCurrent); AtomicBlockInfo.addCompleteAnnotation((IIcfgTransition) mCurrent); From a9f6b247150e9a06c37dd61626dd4416e569b151 Mon Sep 17 00:00:00 2001 From: "maul.esel" Date: Fri, 30 Aug 2024 18:01:51 +0200 Subject: [PATCH 4/4] doc fixes --- .../rcfgbuilder/cfg/AtomicBlockInfo.java | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java index d614df24528..b208d0dcb4b 100644 --- a/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java +++ b/trunk/source/RCFGBuilder/src/de/uni_freiburg/informatik/ultimate/plugins/generator/rcfgbuilder/cfg/AtomicBlockInfo.java @@ -82,8 +82,8 @@ public String toString() { * * Note that an edge can be the start of an atomic block or the end, but not both. * - * @param element - * The element whose annotation is examined. + * @param edge + * The edge whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks the beginning of an atomic block. */ public static boolean isStartOfAtomicBlock(final IIcfgTransition edge) { @@ -95,8 +95,8 @@ public static boolean isStartOfAtomicBlock(final IIcfgTransition edge) { * * Note that an edge can be the start of an atomic block or the end, but not both. * - * @param element - * The element whose annotation is examined. + * @param edge + * The edge whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks the end of an atomic block. */ public static boolean isEndOfAtomicBlock(final IIcfgTransition edge) { @@ -106,6 +106,8 @@ public static boolean isEndOfAtomicBlock(final IIcfgTransition edge) { /** * Determines if the given element (an edge) is annotated as the result of a complete atomic block composition. * + * @param edge + * The edge whose annotation is examined. * @return true if there is an {@link AtomicBlockInfo} annotation that marks a complete atomic block. */ public static boolean isCompleteAtomicBlock(final IIcfgTransition edge) { @@ -114,6 +116,9 @@ public static boolean isCompleteAtomicBlock(final IIcfgTransition edge) { /** * Marks the given element (an edge) as the beginning of an atomic block. + * + * @param element + * The edge to be marked. */ public static void addBeginAnnotation(final IIcfgTransition edge) { addAnnotation(edge, START_DELTA); @@ -122,6 +127,8 @@ public static void addBeginAnnotation(final IIcfgTransition edge) { /** * Marks the given element (an edge) as the end of an atomic block. * + * @param element + * The edge to be marked. */ public static void addEndAnnotation(final IIcfgTransition edge) { addAnnotation(edge, END_DELTA); @@ -130,6 +137,8 @@ public static void addEndAnnotation(final IIcfgTransition edge) { /** * Marks the given element (an edge) as the result of a complete atomic block composition. * + * @param element + * The edge to be marked. */ public static void addCompleteAnnotation(final IIcfgTransition edge) { addAnnotation(edge, 0); @@ -138,6 +147,8 @@ public static void addCompleteAnnotation(final IIcfgTransition edge) { /** * Removes any {@link AtomicBlockInfo} annotation, if present. * + * @param element + * The edge from which annotations shall be removed. */ public static void removeAnnotation(final IIcfgTransition edge) { edge.getPayload().getAnnotations().remove(AtomicBlockInfo.class.getName());