Track source locations of preconditions

[langston-barrett]

While implementing #414, I noticed that matchArg can only report source locations on the level of overrides. It would be nice if we could provide the user with line numbers for each precondition.

This would probably involve changing

  , _csArgBindings     :: Map Integer (t, SetupValue) -- ^ function arguments

to something like

  , _csArgBindings     :: Map Integer (ArgSpec t)

where

data ArgSpec t = ArgSpec { _val :: SetupValue, _loc :: What4.ProgramLoc, _type :: t }

[langston-barrett]

This is especially important for points-to assertions. I might have tens of these in my preconditions, many with the same types involved. It's quite difficult to tell which one should be fixed when something goes wrong, especially if they're all symbolic.

[langston-barrett]

It looks like the problem is that crucible_precond, crucible_points_to, etc. use getPosition from the TopLevel monad, which ignores their position inside the CrucibleSetup block.

[langston-barrett]

The case of crucible_precond, crucible_points_to, etc. was fixed in #477. matchArg could still use the solution outlined above.

[robdockins]

PR #1679 implements most of this, to the point I think it's time to close this ticket.