Remove unmaintained features

[sim642]

After Goblint 1.1.0 aka "fat" the plan is to release Goblint 2.0.0 aka "lean", where we have the opportunity to remove numerous unmaintained and deprecated features which might hinder refactoring and development. This issue is to collect ideas for such removals and discuss them.

Ideas

• Containment analysis. Requires LLVM C++ → C conversion, which has been removed upstream. Goblintutil has a bunch of name demangling logic specific to that conversion.
• Deadlocks by races analysis. Seems suspiciously incomplete: uses must and may locks, but in the predicates completely ignores both. Probably an attempt to implement this paper: https://www.sciencedirect.com/science/article/pii/S2352220814000492.
• Shapes analysis. Highly specific to cyclic doubly-linked lists. Builds on region analysis, making the latter more difficult to fix (Cleaning up and documenting region analysis #107).
• Non-Apron octagon analysis.
• nestra tests. Currently unused. Should be converted into regression tests (with desired checks added) or just removed.
• osek, osektransactionality, flag, flagmodes?
• presub and postsub. They are part of every analysis spec ctx, but only used by some old analyses and mostly replaced with queries. During profiling I have noticed that filter_presubs can take 10% of runtime manipulating the assoc lists used for MCP2. (Might also be a good idea to rewrite that using Map?)
  • postsub removal is part of Run dead code analysis with reanalyze #737
  • presub is part of Remove ARINC analyses #812
• ListDomain in base analysis. Very unused, untested and broken. Run dead code analysis with reanalyze #737 (comment)
• condvars analysis. Unused, not subsumed by var_eq? Now part of Clean up existing must-equality analyses #743.
• Phases. Currently all phases must be manually specified ahead of time and there's no pure communication between the phases. We probably want something more dynamic a la refinement anyway. The phases field in the JSON configuration complicates things due to its recursive schema (Replace JSON schema validation and add full options schema #476). Remove phases #820
• arinc? @vogler (Remove ARINC analyses #812)
• extraction (arinc , osek)? Remove ARINC analyses #812

[vesalvojdani]

So there are some stuff that are more-or-less hopeless, and people will probably not be able to run them in the fat release either... But the OSEK stuff still probably works, but we do not have anyone at the moment to maintain it, so probably we can do this in two steps. We go for a 1.2.0 "semi-fat" release with all the previous stuff that still runs, i.e., we have enabled regressions tests for. Then, for the 1.2 line, we might want have a monthly action that checks whether it still builds, and we could occasionally back-port stuff to.

[michael-schwarz]

I would also like to clean up things such as these strange obfuscated function names:

    | `Unknown "F59" (* strcpy *)
    | `Unknown "F60" (* strncpy *)
    | `Unknown "F63" (* memcpy *)

If we don't want to remove them altogether, they should at least be in some module where one is able to turn them off.

[sim642]

Yeah, those appear to be some ARINC obfuscation things that would indeed be nice to get rid of.
The funny thing is, we have a special implementation for those, but not even memcpy itself.

[vogler]

There's some more ARINC deobfuscation here:

analyzer/src/util/goblintutil.ml

Lines 371 to 385 in 87f42a1

	let scrambled = try Sys.getenv "scrambled" = "true" with Not_found -> false
	(* typedef struct {
	PROCESS_NAME_TYPE NAME;
	SYSTEM_ADDRESS_TYPE ENTRY_POINT;
	STACK_SIZE_TYPE STACK_SIZE;
	PRIORITY_TYPE BASE_PRIORITY;
	SYSTEM_TIME_TYPE PERIOD;
	SYSTEM_TIME_TYPE TIME_CAPACITY;
	DEADLINE_TYPE DEADLINE;
	} PROCESS_ATTRIBUTE_TYPE; *)
	let arinc_name = if scrambled then "M161" else "NAME"
	let arinc_entry_point = if scrambled then "M162" else "ENTRY_POINT"
	let arinc_base_priority = if scrambled then "M164" else "BASE_PRIORITY"
	let arinc_period = if scrambled then "M165" else "PERIOD"
	let arinc_time_capacity = if scrambled then "M166" else "TIME_CAPACITY"

Idk why I didn't use it in special. It'd be better to deobfuscate somewhere before such that not every analysis has to take care to do it. Then we could just match memcpy etc. there.

[michael-schwarz]

I think we should also either remove the tests in the folder nestra, or add assertions to them and add them to the regression tests.

[jerhard]

@vogler We were discussing whether we can remove the Arinc-related analyses and domains, or whether we should keep them for now, in case you need them for some benchmarking or for some other reason.

[vogler]

Keep them for now. I'll have a look at them.

[michael-schwarz]

Do we want to keep SolverInteractiveWGlob? It is some sort of interactive solver that can be started and suspended during solving. Currently, the module is not used anywhere and the solver can thus not be used.

If we want to keep it, we should make it usable and otherwise remove it.