Improve C litmus grammar

[hernanponcedeleon]

I encounter a few litmus tests causing problems to our grammar. This PR fixes those problems.

• missing support for MUL and DIV in expressions

C oota-causality-9
(*
* Result: Sometimes (but requires modeling the compiler)
*
* http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/testcases.html
*
* Decision: Allowed. Similar to test case 8, except that the x is not
*	always 0 or 1. However, a compiler might determine that the
*	read of x by thread 2 will never see the write by thread 3
*	(perhaps because thread 3 will be scheduled after thread 1).
*	Thus, the compiler can determine that r1 will always be 0 or 1.
*
* Note: I used a different deterministic computation, but r2==1.
*	I also modified their condition, but it should be equivalent.
*)
{
   [x] = 0;
   [y] = 0;
}

P0(atomic_int *x, atomic_int *y) {
   int r1 = atomic_load_explicit(x, memory_order_relaxed);
   int r2 = 1 + r1 * r1 - r1;
   atomic_store_explicit(y, r2, memory_order_relaxed);
}

P1(atomic_int *x, atomic_int *y) {
   int r3 = atomic_load_explicit(y, memory_order_relaxed);
   atomic_store_explicit(x, r3, memory_order_relaxed);
}

P2(atomic_int *x, atomic_int *y) {
   atomic_store_explicit(x, 2, memory_order_relaxed);
}

locations [1:r3]
exists(0:r1=1 /\ 0:r2=1)

C oota-non-lb
{
	[x] = 2;
	[y] = 1;
	[z] = 1;
}

P0(atomic_int *x, atomic_int *y, atomic_int *z) {
	int r0 = atomic_load_explicit(y, memory_order_relaxed);
	int r1 = atomic_load_explicit(z, memory_order_relaxed);
	int r2 = r0 + r1;
	atomic_store_explicit(x, r2, memory_order_relaxed);
}

P1(atomic_int *x, atomic_int *y, atomic_int *z) {
	int r3 = atomic_load_explicit(x, memory_order_relaxed);
	atomic_store_explicit(y, r3 / 2, memory_order_relaxed);
}

P2(atomic_int *x, atomic_int *y, atomic_int *z) {
	int r4 = atomic_load_explicit(x, memory_order_relaxed);
	atomic_store_explicit(z, r4 / 2, memory_order_relaxed);
}

locations [0:r0;0:r1;0:r2;1:r3;2:r4]
exists(x=42 /\ y=21 /\ z=21)
(*
 * Above "exists" clause gives OOTA cycle, plus:
 * exists(x=2*S1 /\ y=S1 /\ z=S1)
 *)

• it is possible to discard the value from a value retuning instructions, i.e. there is no need to enforce int r0 = atomic_fetch_add_explicit(...)

C mp-rs-add-st-cpp11
{ [x] = 0; [y] = 0;  }

P0 (atomic_int* x, int* y) {
  *y = 1;
  atomic_store_explicit(x, 1, memory_order_release);
  atomic_fetch_add_explicit(x, 1, memory_order_relaxed);
  atomic_store_explicit(x, 3, memory_order_relaxed);
}

P1 (atomic_int* x, int* y) {
  int a = atomic_load_explicit(x, memory_order_acquire);
  if (a > 1) {
    int b = *y;
  }
}

~exists(1:a=3 /\ 1:b=0)

• In variable declarations, it is possible to skip the last ;

C linearisation2
{ [x] = 0; [y] = 0; [w] = 0; [z] = 0 }

P0 (atomic_int* w, atomic_int* x, volatile int* y) {
  int t = atomic_load_explicit(x, memory_order_acquire);
  t = t + *y;
  if (t == 2) {
    atomic_store_explicit(w, 1, memory_order_release);
  }
}

P1 (atomic_int* w, atomic_int* z) {
  int r0 = atomic_load_explicit(w, memory_order_relaxed);
  if (r0) {
    atomic_store_explicit(z, 1, memory_order_relaxed);
  }
}

P2 (atomic_int* x, volatile int* y, atomic_int* z) {
  int r1 = atomic_load_explicit(z, memory_order_relaxed);
  if (r1) {
    *y = 1;
    atomic_store_explicit(x, 1, memory_order_release);
  }
}

exists (0:t=2 /\ w=1 /\ x=1 /\ y=1 /\ z=1)

• I noticed herd7 supports SCAS and WCAS as synonyms of atomic_compare_exchange_strong and atomic_compare_exchange_weak, however all tests I found using this use it wrong by actually adding a memory order (i.e. even with these fixes we will still throw and exception on the test below)

C a2_reorder+rel+Racq
{ [x] = 0; [y] = 0; [zero] = 0; }

P0 (volatile int* x, volatile int* y) {
  SCAS(x, zero, 1, memory_order_release, memory_order_relaxed);
  int t2 = atomic_load_explicit(y, memory_order_acquire);
}

P1 (volatile int* x, volatile int* y) {
  int r1 = atomic_load_explicit(x, memory_order_acquire);
  if (r1) {
    *y = 1;
  }
}

[ThomasHaas]

LGTM