Generate XCFA

[radl97]

Add XCFA generation capability to Gazer.

Basic usage: tools/gazer-theta/gazer-theta --xcfa --memory=simple --theta-path=$THETA_DIR/theta/subprojects/xcfa-cli/build/libs/theta-xcfa-cli-*.jar --lib-path=$THETA_DIR/theta/lib <files...>.

• Additions to CLI options: -xcfa, --memory=simple flags.
  • Simple memory model only interfaces well with xcfa (Gazer needs an SSA-like CFA, which contradicts with how globals work.)
• Supports global variables
• Supports multiple functions, inputs and outputs
• Contains no threads
• No tests so far (tested only manually)
• Works only if the CLI is permissive (JCommander.newBuilder().acceptUnknownOptions(true)) as it still passes CEGAR-related options
• (No stable XCFA CLI from Theta)

Issues: Passing by reference does not throw error as it should (as it is not supported). Tracing not supported at all. We would need a model too for this, after all

[sallaigy]

I took a look at the PR and I would like to raise a few major concerns before moving on further. FIrst of all, the PR is huge and I believe it would make sense to split it up into smaller ones:

1. The reogranization of the code regarding Theta CFA generation, just to lay some groundwork.
2. As a first iteration, I think it would make sense to implement the simple memory model without XCFA considerations. This has two benefits: 1) limits the scope and 2) it could be used by the BMC and current Theta CFA backend. Also, can't we implement it using MemorySSA?
3. The actual implementation of the XCFA transformation with the necessary stuff to support threaded programs in Gazer.

Also there are some major remarks:

• I am not a big fan of introducing ordering and load/store information in the current variable assignment class, this information should stay outside. We could introduce another kind of variable assignment (and thus a new kind of assignment edge) that stores this information.
• Also I don't think we should add specific exceptions to the CFA formalism to support global variables. Even though the current stateless formalism makes it difficult to deal with globals for Theta, we should not add exceptions to this rule. Either we should 1) introduce the concept of true recursive and cyclic CFAs for the different backends and not mix the two or 2) not generate recursive CFAs by default and translate CFAs into recursive ones only for BMC or 3) do something else :). But this is a larger topic, I would be happy to discuss it further.

[radl97]

I will give a detailed answer tomorrow. However, as your review points out a lot of design-related issues, I will also add that the Theta CEGAR-related options should not be passed to Theta-XCFA right now (and it is not trivial where exactly that configuration should reside).

[radl97]

I will open new, smaller PRs instead, cherry-picking these commits. There are some changes needed before getting into the core XCFA generation.