Integration with other concolic executors

[domenukk]

Hello there.

We have developed a new Rust-native concolic executor that we would like to integrate with libAFL for hybrid fuzzing. Before proceeding, I would like to discuss some considerations regarding the integration of a new concolic executor.

I reviewed the existing implementation for SymCC and noted the following:

• DSE (concolic execution) is expected to report a trace (set of constraints) from an execution.
• The stage negates these constraints and solves them to generate diverging inputs.

Thus, the integration will involve generating constraints in libAFL's format, with the rest of the process being handled by the framework.

I have a couple of questions:

1. Are there plans for other use cases of constraints within the fuzzer? If the primary goal is to find diverging inputs, should the fuzzer manage the solver and constraints, or could it simply receive new diverging inputs from the concolic executor? Additionally, what other valuable constraints, beyond assembly-like boolean expressions, could DSE generate for the fuzzer?

I noticed that the expression definitions are closely tied to Z3/SymCC, and there are some inconsistencies in the design (e.g., calls and returns are not treated as symbolic expressions). Do you see any pending improvements in these areas?

Thanks

Originally posted by @momvart in https://github.com/AFLplusplus/LibAFL/discussions/2666