Apply CC fixes to existing code

[schuessf]

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]

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]

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

[schuessf]

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

[schuessf]

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]

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]

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

[schuessf]

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.

[schuessf]

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

[danieldietsch]

Up to the fixpoint :)

[Heizmann]

The current rules remove variables that are seemingly unnecessary as for example in the following example.

Term fewerQuantifiers = myComplexMethod(arg0, arg1);
return fewerQuantifiers;

However these variables are not unnecessary they

• serve as documentation and
• they ease debugging. When I step through the code, I can immediately see the value of this variable.

[bahnwaerter]

However these variables are not unnecessary they

• serve as documentation and
• they ease debugging. When I step through the code, I can immediately see the value of this variable.

Such measures tend to indicate an unfavorable naming of a function or its excessive complexity. In this case, one should rather give the function a meaningful name or reduce its complexity. To debug the return value of a function, you can use watch expressions in the Eclipse debugger. Watch expressions are also useful for expressions like foo.getBar().equals("xyz"); where you only want to inspect foo.getBar() without rewriting the code for debugging.

[Heizmann]

Such measures tend to indicate an unfavorable naming of a function or its excessive complexity. In this case, one should rather give the function a meaningful name or reduce its complexity. To debug the return value of a function, you can use watch expressions in the Eclipse debugger. Watch expressions are also useful for expressions like foo.getBar().equals("xyz"); where you only want to inspect foo.getBar() without rewriting the code for debugging.

Sounds plausible but

• You may not be able to modify the methods that you call.
• The method name refers to its capabilities in general, but your return value may have additional properties that the method does not ensure.
• In practice, watching expressions is (for a human) more difficult and time-consuming than inspecting values.
• You cannot watch an expression that has side effects without changing the system's state.

[danieldietsch]

... watch expressions ...

Newer Eclipse versions also display the return value of a called function without a watch expression. The only downside is that you see it only when returning from the function, i.e., not anymore in the next step (as far as I know).
As the next step is another function (after all, its a return), this again should never be a problem: either the other function also returns this value immediately, or it does something with it (and can then save the value in a local variable if this is appropriate for debugging/readability or necessary for other reasons.

You may not be able to modify the methods that you call.

In Ultimate, you are probably always able to rename the methods you are calling.

I think in many circumstances it is helpful and increases readability if you use appropriately named local variables instead of inlining expressions. If the return of your method is itself a method call, however, then the description of that value should already be clear from the method you are in (not the one you are calling), because this is now the value you are returning. If it is not clear from the caller name, the callers docs, the callees name or the callees docs, it is probably more appropriate to add a line comment there, as this value is not some intermediate result but the result of the function.

[Heizmann]

Newer Eclipse versions also display the return value of a called function without a watch expression. The only downside is that you see it only when returning from the function, i.e., not anymore in the next step (as far as I know). As the next step is another function (after all, its a return), this again should never be a problem: either the other function also returns this value immediately, or it does something with it (and can then save the value in a local variable if this is appropriate for debugging/readability or necessary for other reasons.

The question is not only what is doable, but what is efficiently doable. Debugging is time-consuming, we have to make sure that developers can debug efficiently. (E.g., maybe you want to set a conditional breakpoint that puts the return value of the method in relation to other values)

[danieldietsch]

Yes, it seems that Eclipse does not support referencing return values in breakpoint conditions.