Organize some general modules into dune libraries

[sim642]

This is a first step towards reducing the spaghetti module dependencies that we have inside the mostly monolithic goblint_lib dune library. From the bottom of the module dependency graph, I took leaf modules (without dependencies) and some of their parents and organized them into three new dune libraries.
The only way towards such better organization is to do it bottom-up because there's no other way without cyclic dependencies: can't extract witnesses into a dune library because goblint_lib needs witnesses and witnesses need some general modules from goblint_lib (like Printable).

Coding-wise, this doesn't really change anything right now because the libraries are either still unwrapped or always opened, so the modules from those libraries are accessible in goblint_lib just like before.
The exact modules in goblint_std and goblint_common aren't yet ideal, but further splitting requires splitting of some module files and rethinking their internal dependencies.

TODO

• Fix Gobview (Add goblint.common dependency gobview#32).

[michael-schwarz]

I have to say I'm not a huge fan. While this indeed cleans up the module structure, the thing which we should arguably care about more, namely a meaningful organization of the source code overall, is worse after this PR.

This will make it impossible for students or new people to contribute without going for a fishing expedition in a huge mess of modules all living in some common folder.

Consider, e.g.,

• src/cdomains/basetype.ml → src/common/basetype.ml
• src/framework/controlSpecC.ml → src/common/controlSpecC.ml
• src/domains/myCheck.ml → src/common/myCheck.ml

There is a reason those were in three separate folders. By creating a big ball of mud, we're not doing ourselves any favors.

Can this somehow be fixed while still keeping the modularization?

CC @jerhard @stilscher for opinions.

[sim642]

This will make it impossible for students or new people to contribute without going for a fishing expedition in a huge mess of modules all living in some common folder.

Consider, e.g.,

• src/cdomains/basetype.ml → src/common/basetype.ml
• src/framework/controlSpecC.ml → src/common/controlSpecC.ml
• src/domains/myCheck.ml → src/common/myCheck.ml

There is a reason those were in three separate folders. By creating a big ball of mud, we're not doing ourselves any favors.

Can this somehow be fixed while still keeping the modularization?

It's not any bigger of a mess than we already have with everything together in one namespace that ignores all directory structure, so there's even no way to properly organize modules.

All three modules you mention are actually something I'm hoping to eventually get rid of altogether:

1. Basetype used to be a huge dump of everything (base type lacks any real meaning). Most of it's now gone and CilType took the majority.
2. ControlSpecC exists only to work around a module dependency cycle. AFAIK that's because Analyses currently is a mix of things that should be separate (ctx vs Spec vs constraint systems vs Result output vs whatnot).
3. MyCheck is a relic from my BSc thesis. It would ideally be in goblint.std as GobQCheck but it contains a dummy varinfo Arbitrary.t definition that shouldn't be there.

I could do all that and a lot more in this PR but that makes it a monster which will be very difficult to keep up to date and let alone merge. Not to speak of all other branches (including from students) that would go into huge conflicts. Currently this PR is mostly just file moves, which git can easily follow.

As is, goblint.common isn't a very coherent selection and I'm hoping to split it further (e.g. goblint.config, goblint.output, etc). Currently that's simply not possible because the module dependencies between those modules are not well-suited for splitting. Some modules would needed to be split themselves or some functions moved between modules to make a clean organization possible. This PR is just the first step to isolate some groups to make it possible to incrementally (ship of Theseus style) improve without having to do one big "reorganize goblint.lib entirely".

The current directories aren't useful for students anyway because all the modules live together in one dune library. Unless you know by heart, which subdirectory something is in, you have to jump to files by name/jump to definition anyway. For example:

• MyCheck is in domains/ although util/ would make more sense.
• ValueDomainQueries is in domains/ although cdomains/ is where ValueDomain itself lives.
• AutoTune is straight in /.
• CilMaps is in util/ although it's more related to incremental/.

Because it's one big namespace, everything has been just placed with little care because it makes no difference.

A particularly fun gem is Spec. All analyses implement the Spec interface, but there's also spec.ml which is Ralf's old thing. By overapproximation of ocamldep, this means that all other analyses spuriously depend on that. This PR doesn't fix that but this just shows how important good modularization is to avoid spurious dependencies and spurious dependency cycles arising from them. I suspect a number of 0-suffixed modules could be avoided just by breaking these spurious module dependencies.

[sim642]

Another motivation for ever achieving modularization is to get rid of this mess:

analyzer/src/dune

Lines 14 to 53 in d9afd55

	(select apronDomain.ml from
	(apron apron.octD apron.boxD apron.polkaMPQ zarith_mlgmpidl -> apronDomain.apron.ml)
	(-> apronDomain.no-apron.ml)
	)
	(select apronPrecCompareUtil.ml from
	(apron -> apronPrecCompareUtil.apron.ml)
	(-> apronPrecCompareUtil.no-apron.ml)
	)
	(select apronAnalysis.ml from
	(apron -> apronAnalysis.apron.ml)
	(-> apronAnalysis.no-apron.ml)
	)
	(select affineEqualityAnalysis.ml from
	(apron -> affineEqualityAnalysis.apron.ml)
	(-> affineEqualityAnalysis.no-apron.ml)
	)
	(select affineEqualityDomain.ml from
	(apron -> affineEqualityDomain.apron.ml)
	(-> affineEqualityDomain.no-apron.ml)
	)
	(select relationAnalysis.ml from
	(apron -> relationAnalysis.apron.ml)
	(-> relationAnalysis.no-apron.ml)
	)
	(select relationPriv.ml from
	(apron -> relationPriv.apron.ml)
	(-> relationPriv.no-apron.ml)
	)
	(select relationDomain.ml from
	(apron -> relationDomain.apron.ml)
	(-> relationDomain.no-apron.ml)
	)
	(select relationPrecCompareUtil.ml from
	(apron -> relationPrecCompareUtil.apron.ml)
	(-> relationPrecCompareUtil.no-apron.ml)
	)
	(select sharedFunctions.ml from
	(apron -> sharedFunctions.apron.ml)
	(-> sharedFunctions.no-apron.ml)
	)

In a perfect world, all the apron analyses would be in a separate optional dune library and that's it!

Without taking the first step with this PR, that will never be possible otherwise because domains and analyses cannot be separated into dune libraries without extracting a common base. That is because Goblint itself (goblint.lib) depends on the analysis and the analysis depends on Lattice.S (which is in goblint.lib).

Moreover, the unqualified subdirs mode that we use to put all the modules from all subdirectories together into one dune library is little used by others and thus comes with dune bugs that require workarounds on top of workarounds:

analyzer/src/dune

Lines 67 to 72 in d9afd55

	; Workaround for alternative dependencies with unqualified subdirs.
	; See: https://github.com/ocaml/dune/issues/4383#issuecomment-805107435.
	; TODO: Remove workaround with dune 3.0, where this should get fixed.
	(copy_files# cdomains/apron/*.ml)
	(copy_files# analyses/apron/*.ml)
	(copy_files# util/apron/*.ml)

analyzer/src/analyses/apron/dune

Lines 1 to 3 in d9afd55

	; Workaround for workaround for alternative dependencies with unqualified subdirs.
	; copy_files causes "dependency cycle that does not involve any files" otherwise
	(include_subdirs no)

There's little interest from dune developers to maintain this largely unused mode: ocaml/dune#4383, ocaml/dune#4381, etc.

[sim642]

I tried and it turns out it's possible to have the old directory structure also in common with (include_subdirs unqualified), so I did that for now. Apparently that dune stanza does two things: it acts as no for the library in parent directory and introduces the current directory as a new unqualified library root.

I also added odoc pages to give a better overview of our dune libraries.

I locally confirmed that merges cleanly with #1093 and #1201. After merge they compile without changes and pass all tests.