Description
There are a handful of places in the verifier where we produce line number information:
copilot-verifier/copilot-verifier/src/Copilot/Verifier.hs
Lines 574 to 577 in d8dc402
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):
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.