Disable MC stateful API when not running in MC

This is a better fix for the null-dereference found by the sanitizers
since 2 nights. Instead of hiding the problem on these builds (as done
in previous commit), fix it for every builds.

MC stateful API is only needed when stateful MC is compiled in

Don't use CLOEXEC

In one case (Checker->App), we were removing it after setup so we
don't need it.

In the other case (App->App), it was just to be tiddy but it's not
really useful: Forking applications are barely supported anyway.

Ensure that the clang optimizer does not swallow the segfault I'm expecting

Instead of actually dereferencing the null pointer (which drives the
static analyzers nuts), simply send myself a SIGSEGV.

Ignore empty replay path + hide a global (to avoid init fiasco)

I was observing that the model_checking_mode global did not had the
same value when compiling with or without optimizations.

Maybe I had a sort of race condition on model_checking_mode during
initialization, or maybe the config element of the replay path was
either called before or after the initialization of the library, thus
replacing the model_checking_mode to REPLAY even if it was supposed to
be APP_SIDE in my case.

It's fixed now, but I'm not completely sure of which of these change
was the right one (probably the replay path). Both seem legit, so commit both.

More logs around the configuration of the MC variants

Really diplay cmake parameters in the jenkins logs

Jenkins: display cmake parameters in the logs

Option model-checking OFF by default

Don't qwack when the default empty string is passed as a replay path

Revert "Also valgrind childs in CI, to valgrind MC apps"

This is already done in Tests.cmake (note so in my_valgrind.pl)

This reverts commit ee681140d428f4adb2cbfde207a04a4fc5a84b95.

Fix an initialization race around the AppSide

Fix make distcheck

Also valgrind childs in CI, to valgrind MC apps

Only compile stateless MC when libevent is found

Rename SIMGRID_HAVE_MC into SIMGRID_HAVE_STATEFUL_MC (so that MC can be optional again)

Fix non-MC builds when MC-only dependencies are missing

Compile the safe part of MC in default mode too

Safety properties (with no checkpointing) are not requiring anything
weird nowadays. Liveness properties, communication determinism and
state-equality reductions are not considered safe as they still need
some memory introspection black magic.

Try to please the ultramodern clang running on FreeBSD by properly giving a copy operator to the abstract class too

We should stop using the copy operator, and use a nice and clean
clone() call instead. Mathieu's on it.

Fix doc on how to select the compiler before compiling

Merge branch 'master' into 'master'

Guiding Backtrack in DFSExplorer

See merge request simgrid/simgrid!143

[gitlab-ci] Run "make distcheck-configure" for merge requests.

Allow to skip some stages of "make distcheck".

Now:
* "make distcheck-archive" only checks the archive
* "make distcheck-configure" also runs cmake et checks the file MANIFEST.in
* "make distcheck" depends on the previous stages, and runs the full build+install+tests

Correctly select the clang compiler on gitlab CI

Gitlab CI: Use clang on modelchecker builds, for MRs

Fix clang builds

Add a small implementation note in MC

Merge branch 'master' into 'master'

Add battery plugin and fix DAG doc

See merge request simgrid/simgrid!142

Add battery plugin and fix DAG doc

Merge branch 'master' of https://framagit.org/simgrid/simgrid

Rename guide as strategy and fix counter-example display with recipe

Replace state copy with recipe: list of transition to replay a state

Cosmetics (help project_description.sh) [ci-skip].

[jenkins] Remove stale sockets from simgrid-mc.

Add missing file

Change opened states for a priority queue

Abide by both compiler warnings

Now handle random transition and multiple times transitions

Merge branch 'master' of https://framagit.org/simgrid/simgrid

Activate the stdobject test now that it works

Don't set a really short timeout on sendsend now that this test works

Revert "Revalidate tesh files now that safety checking is based on reforks"

We can revert this, as we don't re-initialize again and again the
application in refork mode. Instead, we fork a pre-initialized app.

This reverts commit b2a9ee8e090af818cca9e72cd0e44fa1b91586b0.

Implement reforks by forking the application, to save the app exec time

Instead of forking from the checker and exec()ing the application, we
now fork+exec an application that we use as a proxy to the real
application process.

When we need a new application process, we fork it from the proxy,
which is much faster as it's already initialized.

The extra complexity is when the socket closes abruptly on the Checker
side, which means that the application died. We cannot waitpid() on
the app directly, as it's our grandchild. So, we have to ask the proxy
to do the waitpid for us and return the status.

Allow up to 30 elements in ENUM_CLASS

memset 0 the memory that is sent over the network

MC protocol: rename INITIAL_ADDRESSES msg to NEED_MEMINFO

Actually, now that the appside is not ptraced, there is no point killing it

Closing the socket is enough; it will exit on its self.

Also, there is no point waitpid()ing it, as the libevent loop is
already doing so.

Invert another logic error: we need ptrace when we need mem_info, not the opposite

This test is always false, as we asserted so just above

Do not ask for memory info when restarting in refork mode

Use a portable name for SIGABRT

That test seems to pass nowadays

Try to use the same test file for non-linux now that we don't use ptrace

MC: disable personality() as it fails on CI and is not mandatory

Revalidate tesh files now that safety checking is based on reforks

Fix the refork feature by not ptracing App so that it dies properly

More explicit error message

Fix another sonar warning

Delete redundant blank lines at the start of a code blocks (CodeFactor).

Add copy constructor to state, so we can backtrack different ways

Strengthen debug messages on channel send/recv.

Simplify member initialization.

Fix test: program needs exactly 2 processes.

Reduce scope for variable.

Simplify loop.

Determine n_transitions on receiving side (and remove it from the message).

There's no need to compute the total transition count anymore.

Remove superfluous test, and reduce depth of nested statements.

Merge loops and get rid of the "probes" temporary vector.

Merge branch 'master' of https://framagit.org/simgrid/simgrid

Dont use handle_waitpid after we killed the App, as this function may report this as an error

Actually, read()=0 is not an issue in the AppSide

it simply means that the checker closed the socket on its side, so we
should quit ASAP without complaining.

Merge branch 'master' of https://framagit.org/simgrid/simgrid

try to fix stack handling

Fix some easy sonar smells

const-ness, try_emplace, attribute noreturn, ...

The most important one is the TransitionObjectAccess one, where a
field in the subclass was hiding a field of the same name in the
superclass. Maybe the bug I was experiencing in that area was related.

Fix two sonar bugs

- don't throw from the destructor
- don't slice objects (downcast objects instead of downcasting
  references). I suspect that this one is a false positive but the
  tests still pass this way so let's go.

Change an example to take its platform file from the command line if provided

Merge branch 'udpor-phase6' into 'master'

Phase 6 of UDPOR Integration: Add `K`-partial alternatives computation + clean up phase

See merge request simgrid/simgrid!139

jenkins::Flags if you run the tests, be verbose on errors [no-ci]

Make sure that the dtor of CheckerSide actually kills the application and waits for it

Fix the liveness tests when the reforks are compiled in but not activated

fix order of execute_next calls

Manually handle the memory associated to the libevent events

The previous version with std::unique_ptr resulted in segfaults errors
reported by valgrind, and I fail to get it right.

Do not initialize the App's memory introspection if it's not needed

Reforks are still not activated in this code, as the DFS constructor
pretends that it needs memory introspection when it does not. The
version activating reforks is currently commented here, if you want to
play with it.

Things seem more or less working with this change. Known issues:
 - liveness checking is killed by a out-of-bounds access to a vector
   while handling the property automaton. This is the case even when
   reforks are not activated, making this change improper for the
   master branch.
 - The checker is not very good at killing the application in refork
   mode, and many processes remain around until after they are
   abandoned by their checker.
   I'm not sure of whether they only consume memory or whether they
   also burn the CPU in an active loop. In both cases, this is ...
   suboptimal.
   This point is OK when not activating reforks.
 - valgrind reports some sort of double free on the libevent's events.
   I fail to get the std::unique_ptr thing right. See next commit.

Put everything in position to re-fork the verified App

If you pass "need_memory_introspection = false" to the Exploration
constructor, then the application is re-forked systematically instead
of taking snapshot that are then restored.

But it's still in progress, in the sense that the memory is still
introspected even if we don't need it. The network protocol still
needs to be changed so that the memory info are asked only if
"need_memory_introspection = true" and not otherwise.

For the time being, using reforks is very memory intensive for some
reason, and my computers gets to its knees when running the tests.
Until after the OOM killer saves me by cleaning stuff.

Merge branch 'master' of https://framagit.org/simgrid/simgrid

add wait guide and mofidication for the heuristic computation

Address minor comments in MR review

Remove empty Comb.cpp

Add documentation for Comb data structure

The Comb data structure lacked documentation
prior to this commit. Since it plays a pretty
important role in the computation of `K`-partial
alternatives, it was given a more extensive
explanation to ensure that it was used properly.

cosmetics

Move more of the CheckerSide creation logic to the object constructor

MC: disable Address Space Layout Randomization in the application

This will allow to re-fork the application on restore without
invalidating all the metadata we accumulated in the previous
exploration traces.

Differ the creation of the RemoteProcessMemory to when we have enough information

Better responsabilities splitup between CheckerSide and RemoteProcessMemory

Move methods not related to Memory out of RemoteProcessMemory

Now that ModelChecker is gone, it's time to move to the next step of cleanup.

The goal is that CheckerSide is in charge of the interaction with the
application process and RemoteProcessMemory is in charge of its memory.

Right now, RemoteProcessMemory does a bit more, as it stores the pid
and whether or not the application process is running.

This is bad because we want to make RemoteProcessMemory optional, only
used when we need to introspect the application memory (liveness
checking, non-progression checking, etc), so that we can run the app
in valgrind when we don't need to introspect its memory (safety
checking without non-progression checking).

I know I just moved this chunks of code from ModelChecker to
RemoteProcessMemory to now move it further, and I'm sorry for the
noise, but this code drives me nuts and I need to clean it step by step.

Finally kill the now empty ModelChecker class

Move the memory handling of RemoteProcessMemory singleton from ModelChecker to CheckerSide

Move handle_message from ModelChecker to RemoteProcessMemory

Move handle_waitpid from ModelChecker to RemoteProcessMemory