Add support for Parametric

[tonghaining]

No description provided.

[hernanponcedeleon]

@tonghaining as a test case for the PR, you can remove the hack we have for linux-kernel.cat and original code from here.

EDIT: you can also slightly improve spirv.cat by defining imm(r) as here.

[ThomasHaas]

I'm wondering if we even need semantic representations of these parametric calls in the Wmm class.
I feel like this feature can be implemented purely in the parser by inlining at parsing time.
I might try this later.

[ThomasHaas]

I think there is a question about semantics of parametric definitions: do they act like macros or like proper functions?
Consider this case:

let a = ...
let f(r) = r | a
let a = ...
let b = f(c) // Does f(c) use the new or the old definition of "a"?

If it acts like macros, then the parametric relation is evaluated in the current namespace (it sees updated definitions), if it acts like a function then the evaluation is wrt. the namespace at definition time of the function (it sees only the definitions that existed when the function was defined).

[hernanponcedeleon]

The correct answer is "what would herd7 do?"

For this memory model

let a = po
let f(r) = r | a
let a = 0
let b = f(0)

flag ~empty (b) as b-is-non-empty

It flags the execution

herd7 -model ~/git/Dat3M/cat/func.cat ~/git/Dat3M/litmus/C11/manual/example1.litmus
Test example1 Allowed
States 54
Ok
Witnesses
Positive: 1 Negative: 53
Flag b-is-non-empty
Condition exists (1:r1=1 /\ 1:r2=2 /\ 2:r3=0 /\ 3:r4=1)
Observation example1 Sometimes 1 53
Time example1 0.01
Hash=c66dd6b1853dd1bfb042d6c4c75f37c9

Moving let a = 0 before the function definition makes the flag msg disappear

[ThomasHaas]

This PR should be subsumed by #736

[hernanponcedeleon]

The implementation in #736 is working properly, thus I am closing this PR.