Origins

The origin is a mandatory field in every node, and is the facility by which we store any and all metadata about the node. It arranges the preferred naming scheme of nodes that should have a name, it describes the context in which the node was created, and can remember what text range(s) in the input participated in making the node.

As it is metadata that is nominally not semantically relevant, it does not participate in the structural equality of nodes.

Naming

The name of a node is not relevant to rewriting logic, so it is included in the metadata. For simple source input, the preferred name is just the same as it is in the source. For generated nodes we can use PreferredName and NamePrefix to indicate the preferred name, or its shorthand Origin.where(name = ..., prefix = ...). We emphasize once more that the name has no semantic relevance: VerCors would be equally sound if all preferred names are x.

The preferred name is currently used in two places:

• vct.col.print.Namer for debug output and some source transformation outputs (e.g. VeyMont);
• viper.api.transform.ColToSilver for serialization into the Viper language.

Context

For debugging purposes we can add context to an origin. This is typically not necessary for reporting verification failures, as they are reported very close to the input origin. Nevertheless it is useful to know why a node exists, so we mostly add ad-hoc instances of LabelContext, or its shorthand Origin.where(context = ...).

Source Context

Most origins contain at least one pair of ReadableOrigin and PositionRange. Often it is tempting to "just ask" what file position a node comes from, but it is not very often so straightforward to explain away the reason a node exists as such. Nevertheless it is useful to know what source code primarily contributed to the node.

Origin extends HasContext, which defines messageInContext to render a message in the context it describes. This will usually contain the file name, as well as the fragment in the file that the origin refers to. There is also Origin.shortPosition, which will attempt to locate an arbitrary file position in the Origin - this is generally not advisable to use outside debugging.