Invalid sequence index, more debug info

[weaversa]

Do you think it would be possible to output a line number or something when running a function gives an invalid sequence error? Right now, if something is going to index out of bounds, it just says Invalid sequence index: 640 but doesn't give any more information.

[weaversa]

:safe also doesn’t give any indication about where the error occurs.

[brianhuffman]

There are a couple of things we could do here: First, in order to be able to attach source location information onto exceptions, we would need to extend the Eval monad with some extra state (probably using ReaderT), which might include a Range value to indicate source location, or maybe something like a call stack. Using the location info that we currently have in the type-checked AST, this would at least let you know the name and location of the function (or functions) that you were evaluating when the error occurred.

The second thing we might want to do is to preserve more location information in the type-checked AST. Right now, the Name values are annotated with the source location where they are bound, but that's it. The parser AST has source range annotations all over the place, and we could preserve a lot more of these. Then you could have more precise source ranges on errors, identifying the exact sub-expression where the error occurred instead of just which declaration.

[yav]

I've done some things like that on other projects and one thing to watch out for is how names are handled: we may want to distinguish between the definition site of a name and use sites of a name, otherwise you end up with rather confusing locations. Some potential options are:

1. Use different types for these names
2. Use the same type for all names (like now) but the occurrences of the same name may have different locations
3. Names always contain their definitions sites, but the variable expression containing the name is annotated with the use site

To me (3) feels like the best option.

Another tricky bit is that transformations on the annotated AST would have to be careful about having sensible locations, and we should not assume that nesting in the AST implies containment of the locations (e.g., if you inline something). The biggest transformation we do at the moment is probably specialization so we'd have to be a bit careful there.

[robdockins]

Coincidentally, I've been working on this exact issue. I have a branch that prints source locations for runtime errors. I'll have to see what we can do for :safe.

[robdockins]

With the merge of #995, we now get results like the following.

Cryptol> :safe (\x y -> x / y : Integer)
Counterexample
(\x y -> (x / y) : Integer) 0 0 ~> ERROR
division by 0
-- Backtrace --
(Cryptol::/) called at <interactive>:1:16--1:21
<interactive>::it called at <interactive>:1:7--1:32
(Total Elapsed Time: 0.018s, using "Z3")

Cryptol> :safe (\i -> [1,2,3:Integer]@(i:[8]))
Counterexample
(\i -> [1, 2, 3 : Integer] @ (i : [8])) 0x03 ~> ERROR
invalid sequence index: 3
-- Backtrace --
(Cryptol::@) called at <interactive>:2:14--2:37
<interactive>::it called at <interactive>:2:7--2:38
(Total Elapsed Time: 0.008s, using "Z3")