How is a variable in an assertion mapped into IR?

[Baltoli]

If we have an assertion such as:

eventually(
  acq_rel(lock)
)

How is lock translated into something the IR can use? I think this logic lives inside the argument parser, so it would be good to go digging there to make sure we can work out how to do this for static analysis.

[Baltoli]

This is actually done by the instrumenter, which has a method for collecting arguments at an assertion site (CollectArgs). This builds up a table mapping names to Values from the following sources:

• All the global variables
• Arguments to the function enclosing the assertion site
• Local variables (i.e. those allocated on the stack at the beginning of the function)

It is possible to get the variable name back from each of these sources.

The assertion itself has a set of arguments with an index attached to them. Its argument vector is then populated by mapping the names in the manifest to the value found in scope.