Port entire build process from configure/make to dune

[sim642]

The build process is a real pile of hacks, particularly because:

1. Machdep is generated at compile time of CIL, which is morally wrong.

   It's build process is also extremely convoluted:

   1. Build an OCaml program (machdepConfigure.exe).
   2. Run that OCaml program to generate a C header (machdep-config.h).
   3. Build a C program (machdep-ml.exe) which includes that header.
   4. Run that C program to generate a part of an OCaml record definition.
   5. Construct the OCaml Machdep module using cppo to include part of that record definition.
   6. Build the Machdep module for CIL library.

2. Apple's stupid gcc symlink to their Clang, which makes every gcc call a multi-step process. Moreover, homebrew's gcc doesn't support -m32, so additional conditional compilation is needed (whereas the old configure/make rather silently ignored those assembler errors).

   Even though we removed MSVC support, maybe we should add Clang support. That would solve all these obscure GCC problems and Clang should be much more similar to GCC than MSVC.

[michael-schwarz]

For me locally, all tests fail when I run dune runtest or dune test.

     testcil alias test/runtest (exit 2)
(cd _build/default/test && ./testcil -r --regrtest)
Test infrastructure for CIL on linux
There are 430 tests enabled
------------ [0] CC="gcc" make arcombine ------------

[0] A regression test command failed:
  CC="gcc" make arcombine
------------ [1] CC="gcc" make baddef ------------
------------ [2] CC="gcc" make comb ------------
------------ [3] CC="gcc" make combine1 ------------

[3] A regression test command failed:
  CC="gcc" make combine1
------------ [4] CC="gcc" make combine10 ------------
[....]

[424] A regression test command failed:
  CC=gcc make testrungcc/enum3g
[425] A regression test command failed:
  CC=gcc make testrungcc/enum3h
[426] A regression test command failed:
  CC=gcc make testrungcc/enum3i
[427] A regression test command failed:
  CC=gcc make testrungcc/enum3j
[428] A regression test command failed:
  CC=gcc make testrungcc/enum3k
[429] A regression test command failed:
  CC=gcc make testrungcc/enum3l

[michael-schwarz]

But once we get that to work stabley, I think it is a good idea to ditch all of this autoconf based madness.

[sim642]

I think _build/default/test/cil.log should contain more detailed information about what's going wrong.
But if I were to guess, it might be due to a dirty build, which dune clean or make clean (before switching to this branch) might fix. If you've used make in the past, you'll have some of the make-generated files directly in the source tree, which dune might be just copying into _build instead of generating them using the newly defined rules.

[michael-schwarz]

Looks good! I updates the readme slightly and added a comment on how to run an individual test from the suite.

[michael-schwarz]

But if I were to guess, it might be due to a dirty build, which dune clean or make clean (before switching to this branch) might fix.

It was indeed a dirty build, but none of those helped. The issue was gone after a fresh checkout hough 🎉

[michael-schwarz]

@sim642: It looks like the new build process for the documentation is broken: https://github.com/goblint/cil/runs/7405853088?check_suite_focus=true

[sim642]

Should be fixed on master now.