Add support to CAAT for SyncBar and SyncFence relations

[ThomasHaas]

CAAT still does not work with virtual memory objects, so it will produce wrong results on the PTX7.5 litmus tests.

[hernanponcedeleon]

You should at least enable caat in the spirv tests, e.g.

Dat3M/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/benchmarks/SpirvRacesTest.java

Line 123 in 9a23ab0

assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult());

[ThomasHaas]

Some of those tests also use virtual memory objects, so I cannot enable all of them.

EDIT: Ok, I'm not sure if the tests actually contain virtual memory. I just saw errors related to vloc but vloc also relates accesses to physical memory.

[hernanponcedeleon]

Is the comment "refinement still fails to understand virtual memory" outdated? If not, in which benchmarks is this causing problems?

[ThomasHaas]

The comment is still valid and it will produce wrong results on PTX7.5 litmus tests. I haven't checked the details, but I believe the ExecutionModel just does not capture virtual accesses correctly and this causes Refinement to produce wrong results.

[ThomasHaas]

I should add: I think virtual addressing was added in a very ad hoc manner and has many flaws. If we really want to support it in the long run, we should properly think it through before trying to fit in the ad hoc solution into all the solver backends.