Track register in Litmus CAS

[MattWindsor91]

In at least some cases (eg in C11 partialSC), R+W events have a register associated with them, and that register feeds into the forbidden execution. For instance, one such event structure is (mind my ASCII):

[RMW x=0 -> x=1] --co-> [RMW x=0 -> x=2]

In this case, both RMWs store the read value to r0, because the witnessing C execution is (0:r0 = 0 /\ 1:r0 = 0 /\ x=2).
However, at the moment, this register is thrown away at the Litmus level and replaced with a temporary expected value, with the postcondition just pointing to a dangling r0 (or, on master, not mentioning those registers at all).

This is an attempt to push those registers through the Litmus IR and into the pretty-printer for C. I've assumed that there still exist possibilities where the RMW does not spill to a register, so I've extended the Cas(...) variant with
an optional register, and kept the old logic around for when this is None.

I'm not sure if this change adversely affects other CAS instances eg. on other models, so there might need to be some further work needed; for this reason and because there are issues with master not propagating the registers through (not sure why not), this is targeting dev.

Example output for above event structure before changes:

C test_2
// Hint: try simulating with herd7 <test_2.litmus>
// WARNING: C litmus output is experimental!

// Declaring global variables.
{
  x = 0;
}

// Thread 0
void P0(atomic_int *x) {
  int expected;
  expected = 0; /* returns bool */ atomic_compare_exchange_strong_explicit(x, &expected, 1, memory_order_relaxed, memory_order_relaxed);
}

// Thread 1
void P1(atomic_int *x) {
  int expected;
  expected = 0; /* returns bool */ atomic_compare_exchange_strong_explicit(x, &expected, 2, memory_order_relaxed, memory_order_relaxed);
}

exists (0:r0 == 0 /\ 1:r0 == 0 /\ x == 2)

The postcondition here is right, but it refers to r0 instead of expected (the default variable introduced when there is no register for a CAS). (The current master version of Memalloy gives us exists (x == 2), which is clearly too general; as mentioned before, when I've tried to apply this change there, the event registers haven't been available and there's no change)

And after:

C test_2
// Hint: try simulating with herd7 <test_2.litmus>
// WARNING: C litmus output is experimental!

// Declaring global variables.
{
  x = 0;
}

// Thread 0
void P0(atomic_int *x) {
  int r0 = 0;

  r0 = 0; /* returns bool */ atomic_compare_exchange_strong_explicit(x, &r0, 1, memory_order_relaxed, memory_order_relaxed);
}

// Thread 1
void P1(atomic_int *x) {
  int r0 = 0;

  r0 = 0; /* returns bool */ atomic_compare_exchange_strong_explicit(x, &r0, 2, memory_order_relaxed, memory_order_relaxed);
}

exists (0:r0 == 0 /\ 1:r0 == 0 /\ x == 2)