Display Copilot-related line number information

[RyanGlScott]

There are a handful of places in the verifier where we produce line number information:

• copilot-verifier/copilot-verifier/src/Copilot/Verifier.hs

  Line 521 in d8dc402

  loc <- getCurrentProgramLoc sym

• copilot-verifier/copilot-verifier/src/Copilot/Verifier.hs

  Lines 574 to 577 in d8dc402

  	-- TODO, would be lovely to be able to do better than dummy positions for all these things
  	-- so we can correspond assumptions and asserts back to the parts of the original spec that
  	-- gave rise to them.
  	dummyLoc = mkProgramLoc "<>" InternalPos

• copilot-verifier/copilot-verifier/src/Copilot/Verifier.hs

  Line 794 in d8dc402

  let loc = mkProgramLoc "<>" InternalPos

None of these currently display any information about the Copilot program being verified. In the best case, we simply print out line information about the C program (obtained from crucible-llvm's getCurrentProgramLoc function, but in the worst case, we print out nothing at all (which is what the silly "<>" strings accomplish).

We should modify Copilot to make it possible to use line number information about the Copilot program within the verifier. Specifically, I'm thinking that we will add CallStack information to some parts of a Copilot Spec:

-- | A Copilot specification is a list of streams, together with monitors on
-- these streams implemented as observers, triggers or properties.
data Spec = Spec
  { specStreams    :: [Stream]
  , specObservers  :: [Observer]
  , specTriggers   :: [Trigger]
  , specProperties :: [Property]
  }

We aren't making use of Observers in our work, so we can ignore those. We are making use of Triggers, Propertys, and Streams however.

Let's start with Triggers, as they are a bit simpler. We should add something like a triggerCallStack :: CallStack field here. The trigger function is the primary means by which Triggers are produced, and In order to produce precise CallStack information for Triggers, we should add a HasCallStack constraint to trigger (and any other functions that produce Triggers).

We can handle Propertys in a similar way. The primary means by which Propety values are produced is the prop function, and we could add a propertyCallStack :: CallStack field to Property here.

Streams are a more interesting example because there are many different ways to construct them. The Copilot.Language.Operators directory in copilot-language contains various Stream-producing functions, including (but not limited to):

• extern
• (++) and drop
• Bitwise operations

All of these will need HasCallStack constraints. But where should we store these? Most likely, we will want to change copilot-language's Stream data type. Stream has data constructors corresponding to all of the possible ways to construct stream expressions, and I suspect that we will need to give each data constructor a CallStack field. Once that is done, we can plumb this information up into the verifier. (I haven't fully thought through the details of how that will work yet, but one step at a time.)

We should do this work in a branch of our fork of copilot for now.

[AlexMahrer]

The initial call sites for Triggers are now captured from the copilot spec and passed through to the verifier. I added these changes to a new copilot-verifier branch, develop-callstack-support. I've also created a develop-callstack-support branch on our Copilot fork, which contains the necessary Copilot changes.

Here is some output from Demo1 demonstrating the changes - the call site of the trigger is now being output:

...
[copilot-verifier] Emitted a proof goal (asserting triggers fired in corresponding ways)
[copilot-verifier]   During the transition step of bisimulation
[copilot-verifier]   Proof goal 13 (18 total)
[copilot-verifier] 
[copilot-verifier] * Function: trigger
[copilot-verifier]   Position: src/Demo1.hs:24:3
[copilot-verifier] * Trigger name: odd
...

A few notes for future work on this:

• Streams and Properties still need to be supported.
• The call sites internal to copilot spec processing are not needed. Those call sites can be ignored using freezeCallStack.
• Passing the call stacks explicitly in the copilot code will allow us to take advantage of compiler checks that are not enforced on implicit params.
• Some refactoring can be done in the verifier to remove redundant information from the global trigger variables.