Make symbolic memory parametric and concretise every symbolic address

[filipeom]

Since this depends on #367, the relevant changes are in 6c8a21e.

Summary

1. Parameterizes symbolic memory on an abstract backend which allows handling addresses in an isolated way (symbolic_memory_make.ml).

2. Implements a concrete backend that always concretizes symbolic expressions to concrete addresses (symbolic_memory_conrcetizing.ml).

Last remark: I left the original symbolic_memory.ml in order to not break concolic execution. It's unclear to me that we will be able to perform concolic execution with the same symbolic execution memory backend that we use for owi sym.

Benchmarking

• TestComp with 5 second timeout:

# results-testcomp-owi_w8_O3_sZ3-2024-07-29_14h49m24s
Run 1216/1216: testcomp/sv-benchmarks/c/xcsp/aim-200-6-0-sat-4.c
  Timeout in 5.01258 12.243 0.433289
  Nothing:      0    Reached:    591    Timeout:    624    Other:      1    Killed:      0

[filipeom]

With the branching changes, now in test-comp we get the following results (on my pc, -w8 and 5s timeout):

Run 1216/1216: testcomp/sv-benchmarks/c/xcsp/aim-200-6-0-sat-4.c
  Timeout in 5.01408 11.8628 0.385292
  Nothing:      0    Reached:    593    Timeout:    622    Other:      1    Killed:      0

No more nothings. I'll leave it running with 30s while I make this ready for review

EDIT: Results for 30s on my local machine

Run 1216/1216: testcomp/sv-benchmarks/c/xcsp/aim-200-6-0-sat-4.c
  Timeout in 30.0183 207.06 3.34624
  Nothing:      0    Reached:    663    Timeout:    552    Other:      1    Killed:      0

[zapashcanon]

These are very good results for 5 seconds and 8 workers! :D

[zapashcanon]

@zshipko, FYI, with this PR we observed that most of the tasks where we were not able to handle symbolic memory on the Test-Comp benchmarks are now solved by Owi. It might help a lot when running Owi on Rust code ; and if it's not enough, #338 is going to make the situation much better but we have not benchmarked it yet.

[zapashcanon]

I'm going to benchmark this before merging.

The current results on main are:
Nothing: 75 Reached: 608 Timeout: 532 Other: 1 Killed: 0
(from results-testcomp-owi_w24_O3_sZ3-2024-07-30_16h02m38s/results)

[zapashcanon]

Results:

Nothing: 0 Reached: 689 Timeout: 526 Other: 1 Killed: 0

The output of diff compared to main:

tool1 had 608 reached and tool2 had 689 reached
tool1 had 532 timeout and tool2 had 526 timeout
tool1 had 075 nothing and tool2 had 000 nothing
tool1 had 001 other   and tool2 had 001 other
tool1 had 000 killed  and tool2 had 000 killed

tools have 608 reached tasks in common

tool1 had 000 tasks tool2 did not found
tool2 had 081 tasks tool1 did not found

on      commonly  reached tasks, tool 1 took 1432.690579 sec. (mean 2.356399) and tool 2 took 1400.800041 sec. (mean 2.303947)
on *not commonly* reached tasks, tool 1 took 0.000000 sec. (mean -nan) and tool 2 took 169.033071 sec. (mean 2.086828)

among tasks reached only by tool 1, tool 2 replied 000 nothing, 000 timeout, 00 other and 00 killed
among tasks reached only by tool 2, tool 1 replied 074 nothing, 007 timeout, 00 other and 00 killed

So almost all the nothing became reached and a few of them became timeout. For some reason, some timeout also became reached, I would say they are only noise or cases where we were failing again and again on limited memory model.

But actually, this is not as good as we thought, because we have 78 Trap: out of bounds memory access or Trap: memory heap buffer overflow. Which mean, we are finding the Test-Comp bug in 611 cases only (which is better than before! :D).

So in short, this is a clear improvement, I'm curious to see if and how #273 is going to make the improvement even better.