Apply CC fixes to existing code #700

schuessf · 2024-12-06T16:52:22Z

During the update to Java 21 (see #672), we also slightly changed our coding conventions.
This can lead to unnecessary diffs, when editing existing files (many existing file did not even follow our old coding conventions...).
In this PR I applied the new coding conventions automatically (starting with CACSL2BoogieTranslator) and we can discuss possible changes to the coding conventions here.

Eclipse does not actually allow to apply the save actions automatically to multiple files. But I found a way 😉

There is a similar command Clean Up that can be applied on a whole project under the Source menu (Note: There is also a command Format there, but it only applies the formatter).
The Clean Up actions can be set up under Preferences -> Java -> Code Style -> Cleanup and they are almost the same as the save actions, but their is no common way to set them.
We could also add these cleanup settings to our settings that the users should import, but we don't want to keep them in sync manually and also the import of the cleanup actions did not work.
Therefore I wrote a small python script (see below) that creates an .xml file that can be imported under the cleanup-settings from our .epf file.
After this file is imported, you can simply select some files / plugins / the whole workspace to run Source -> Clean up, which should apply our save actions on multiple files automatically.

def create_cleanup_settings(in_file, out_file):
    lines = ['<?xml version="1.0" encoding="UTF-8" standalone="no"?>',
             '<profiles version="2">',
             '\t<profile kind="CleanUpProfile" name="Ultimate" version="2">']
    with open(in_file) as f:
        settings = re.findall(r'/instance/org.eclipse.jdt.ui/sp_cleanup.(.*?)=(.*?)\s', f.read())
    for n, s in settings:
        lines.append(f'\t\t<setting id="cleanup.{n}" value="{s}"/>')
    lines.append('\t</profile>')
    lines.append('</profiles>')
    with open(out_file, "w") as f:
        print("\n".join(lines), file=f)

schuessf · 2024-12-06T16:53:25Z

...slator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/CLocation.java

@@ -188,19 +188,17 @@ private IASTNode getMergedNode(final CLocation otherCloc) {
 			return otherNode;
 		} else if (otherNode == null) {
 			return myNode;
+		} else // we have two nodes and want to merge them; if one of both is a translation unit, we take the other


Merging else and if is a good idea in general, but it looks somehow weird, if there is a comment in between, but I don't know how to handle this.

schuessf · 2024-12-06T16:56:16Z

...freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/PostProcessor.java

-						"You selected the library mode (i.e., each procedure can be starting procedure and global "
-								+ "variables are not initialized). This program contains a \"main\" procedure. Maybe you "
-								+ "wanted to select the \"main\" procedure as starting procedure.";
+				final String msg = """


That's really a nice usage of multiline string, we were able to get rid of the quotes \".

schuessf · 2024-12-06T16:58:59Z

...rc/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/container/c/CType.java

-		result = prime * result + (mIsRestrict ? 1231 : 1237);
-		result = prime * result + (mIsVolatile ? 1231 : 1237);
-		return result;
+		return Objects.hash(mIsConst, mIsExtern, mIsInline, mIsRestrict, mIsVolatile);


That's so much nicer, Boolean::hashCode returns exactly 1231 or 1237 and Objects::hash computes exactly this combination.

schuessf · 2024-12-06T17:00:23Z

...ltimate/plugins/generator/cacsl2boogietranslator/preferences/CACSLPreferenceInitializer.java

-			+ "if the program lost track of allocated memory. If this is set to false we are unsound (at SV-COMP) in "
-			+ "cases where not all memory is freed but pointers to that memory are live at the end of the "
-			+ "main procedure.";
+	public static final String DESC_SVCOMP_MEMTRACK_COMPATIBILITY_MODE = """


While I think these multiline Strings are generally nicer, I don't think we should change existing code, as also the line breaks are somehow strange now.

schuessf · 2024-12-06T17:02:42Z

...informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java

@@ -747,7 +748,7 @@ public IBacktranslatedCFG<String, CACSLLocation> translateCFG(final IBacktransla
 		// printCFG(cfg, mLogger::info);
 		final boolean oldValue = mGenerateBacktranslationWarnings;
 		mGenerateBacktranslationWarnings = false;
-		IBacktranslatedCFG<String, CACSLLocation> translated = translateCFG(cfg, (a, b, c) -> translateCFGEdge(a, b, c),
+		IBacktranslatedCFG<String, CACSLLocation> translated = translateCFG(cfg, (IFunction<Map<IExplicitEdgesMultigraph<?, ?, String, ? extends BoogieASTNode, ?>, Multigraph<String, CACSLLocation>>, IMultigraphEdge<?, ?, String, BoogieASTNode, ?>, Multigraph<String, CACSLLocation>, Multigraph<String, CACSLLocation>>) this::translateCFGEdge,


This change is really bad! In general, this::translateCFGEdge is a bit nicer than (a, b, c) -> translateCFGEdge(a, b, c), but the save actions introduced an unncessary cast here and for long class names C, I actually prefer c -> f(c) over C::f.

schuessf · 2024-12-06T17:13:48Z

...i_freiburg/informatik/ultimate/cdt/translation/implementation/base/FunctionTableBuilder.java

+				// we only update the table with a declaration, if there is no entry for that name yet.
+				// otherwise we might only keep the declaration and omit the implementation from
+				// reachableDeclarations.
+				if ((d instanceof IASTFunctionDeclarator) && !mFunctionTable.containsKey(rslvKey)) {


Oddly enough, Eclipse inserts unnecessary parentheses here that would be removed again, if we run the save actions afterwards again 😆

schuessf · 2024-12-06T17:17:01Z

...e/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java

@@ -134,7 +134,7 @@ public BacktranslatedExpression translateEnsuresExpression(

 	private Optional<Expression> computeOldVarEqualities(final String proc,
 			final Set<de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression> modifiableGlobals) {
-		final var modifiableNames = modifiableGlobals.stream().map(e -> e.getIdentifier()).collect(Collectors.toSet());
+		final var modifiableNames = modifiableGlobals.stream().map(de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression::getIdentifier).collect(Collectors.toSet());


e -> e.getIdentifier()) is definitely nicer than de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression::getIdentifier...
Also, Eclipse does not respect the maximum line length here.

Maybe even without this change, we should run Clean up twice.

Up to the fixpoint :)

Apply CC fixes to CACSL2BoogieTranslator automatically

628260f

schuessf requested review from maul-esel, Heizmann, bahnwaerter and danieldietsch December 6, 2024 17:00

schuessf commented Dec 6, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Apply CC fixes to existing code #700

Apply CC fixes to existing code #700

schuessf commented Dec 6, 2024 •

edited

Loading

schuessf Dec 6, 2024

schuessf Dec 6, 2024

schuessf Dec 6, 2024

schuessf Dec 6, 2024

schuessf Dec 6, 2024

schuessf Dec 6, 2024

schuessf Dec 6, 2024

schuessf Dec 6, 2024

danieldietsch Dec 6, 2024

Apply CC fixes to existing code #700

Are you sure you want to change the base?

Apply CC fixes to existing code #700

Conversation

schuessf commented Dec 6, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

schuessf commented Dec 6, 2024 •

edited

Loading