Re: Gradual 'tree' typing and C++

--=-=-=
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable

Martin Uecker <[email protected]> writes:

>> > Usually something inside of fold_build2_loc actually accesses some
>> > properties of the type and type checking triggers there.  So, by moving
>> > that check earlier, all we'd achieve is to assert one or two frames up
>> > in the callstack.
>
> I agree that run-time checking the dynamic downcast is only marginally
> useful.  What would be more useful would be the static check that ensures
> that a tree_expr cannot be passed to a function expecting a tree_type.=20

This is indeed what I'd like to end up being able to provide.

By adding a type system here, the check isn't merely moving up.

For sake of discussion, lets presume that there is a precondition on
some function B, i.e. something like (still using the template syntax;
though it could be a language extension of some sort as I said before, I
just haven't thought sufficiently in that direction yet):

   R func_b (ttree<T_C> t);

(i.e. that B receives a tree of T_C)

... and that 'B' is called from 'A'.

There are two cases (with some subcases):

1. 'A' somehow guarantees that only a tree passing such a check reaches
   B.  In this case, such a guarantee can come either from A itself, or
   from some caller of A, or from an invariant of some callee (or
   component ref, or so on; those can also be understood as functions)
   of A other than B.

   This invariant is propagated through type annotations:

     i. If that check is in A, then the type of the tree being passed to
        B was already encoded in the variable (call it 't_a') holding it
        in A.
    ii. Else, if that check in in some caller, then A also declares that
        precondition by having a function signature that encodes it.
   iii. Else, some unrelated callee encodes the guarantee it provides in
        its return type/out parameter.

   Now, the "graduality" of such a type system would imply that we're
   permitting the insertion of implicit casts from plain, unmarked
   'tree's to typed trees that encode these qualities and back (at least
   for now).

   This means that, initially, it may be the case that none of these
   three subcases apply (for instance, maybe the check mentioned in (i)
   is actually an assert on 't_a', where 't_a' lacks a type annotation,
   like it would be today).

   If so, the check is moved into the frame of A rather than B, yes, but
   this is done implicitly, by the conversion rule from 'tree' ->
   'ttree<T_C>', until the lack of type annotation is corrected (for
   instance, by turning the check on 't_a' into a fallible downcast, and
   thus turning 't_a' into a 'ttree' compatible with the one B desires).

   The real effect on the code is that an assert on the first line of
   B is lost, and what it used to check is encoded in the type signature
   of B, making it also more useful.

   The "lost" assertion is only lost in appearance, in actuality it
   moves to the exact point(s) where the type system is not sure the
   precondition is met.  It is only lost if truly superfluous.

   One may, rightfully, be wary of such implicit behavior, but I think
   it is justifiable in this case as it mirrors precisely what a
   developer would need to write and ensure anyway (lest they create a
   bug), if accompanied with a method by which we can ensure we don't
   introduce new cases where it manifests (i.e., a way to prevent
   unwanted regressions in the real strictness of the types in the
   codebase, so that it can be ratcheted down until it ceases to exist).

2. Otherwise, there was no such guarantee anywhere in A or its callers.
   In this case, a (possibly latent) bug is discovered.

I appreciate that this is still quite vague and abstract, but I hope
this clarifies what I actually have in mind.

I think that the most important benefit here is in refactoring.  If we
change something, the compiler is able to verify that we aren't
violating invariants or expectations by checking whether all the tree
type annotations are compatible.

Merely running the testsuite does not suffice.

The C++ Named Address Space support provides an example (indeed, the one
that motivated the typed qualifiers refactor): the C++ FE treated
qualifier sets (loosely typed as ints) as something that can be simply
bit-OR'd together, in /many/ places.

This changed when address space qualification was added, and there was
no way of detecting where this changed.

The testsuite passed cleanly, of course, because the testsuite cannot
cover every combination of otherwise orthogonal features present in C++
(and to a much lesser extent, C, too; this isn't uniquely a C++ problem,
but it is exacerbated there by the rate of growth.. and the already
present size).  The number of tests required follows a factorial.

A similar thing goes for cases where, say, a new tree is introduced.  It
is difficult to know all the sites where the new tree needs to be
handled.  (-Wswitch doesn't help; you'd either need to list all trees,
some of which are FE specific and you may not be in an FE, or add a
default case.  To be clear, a type system like this would not help
either if there isn't a corresponding 'match' statement or expresson of
some sort, that permits the type system to verify that all the possible
cases of a 'ttree' were covered, or something like Pythons
'typing.assert_never'; I am not sure yet to what extent either can be
implemented in C++14 yet).

I reckon we'd have been discovering subtle address space related bugs in
the C++ FE a long way down the line if I'd opted not to implement more
strictly typed qualifier sets.

(that is not to say that many tests shouldn't be written, just that
 they, IMO and IME, do not suffice alone)

> Still, the main benefit for me would not be static / run-time checking
> but the self-documenting nature of the types in the source code.

That's also something that was on my mind when thinking about this.

When I just started hacking GCC, I recall distinctly that it was hard to
understand what goes for what tree.

There's a logic to it, of course, and at this point I think I understand
that logic well enough for it not to be a frequent trip-up, but that's
after some years of (relatively light, all things considered) work.  It
is daunting for a new hacker.

Even today, sometimes, the best I can do is I dig up testcases and add
'debug_tree (...)'.

Working backwards from TREE_CHECKs is not great.  It is less bad to work
back from asserts, but still not great.  Plus, anything hand-verified is
simply something that will be made accidentally incorrect in the future.

> I would also see a real benefit also if tree types were to properly
> maintain=C2=A0 their invariants.  Currently, there are a lot of implicit
> assumptions mixed with some incomplete explicit testing done in
> verify_type etc.,=C2=A0 but doing this more systematically by properly
> encapsulating the trees in subtypes with an API that ensures that the
> invariants are maintained (instead of checking them occasionally)
> would be helpful.
>
> Because now, if I add something to c_verify_type because I notice
> that some part of the C FE implicit assumes this property, I always
> encounter some new corner cases where this assumption is actually
> violated.=20

Adding a type system would also help with this.  If accessors are typed,
one knows what accessor is semantically correct for what tree code, and
what can be stored in or read out of that accessor.

It's not a silver bullet, but it can help.

>> > With types vs. non-types, there is also the complication what is
>> > error_mark_node, currently we treat it as both expression and type, but
>> > with limited usability, TREE_TYPE (error_mark_node) is error_mark_node.
>>=20
>> I think I was suggesting to have ERROR_TYPE/error_type_node at some
>> point.  That would
>> be a requirement for any of this.  It would also avoid some ice-on-inval=
id
>> where type accessors are used on error_mark_node without a prior
>> check for this case (but possibly only delay those).
>
> The issue with errors is also that it not really clear in what context an
> error_mark_node is allowed and where not.  This is also something
> where static type checking could help.

Indeed, the validity of error and even null trees in a given location
should be encoded and checked by such a type system.

Some languages (cough, Java, cough) neglect to do this and it is its own
source of bugs.  Mypy and TypeScript do not (and, even on the JVM,
Kotlin does not, and I presume Scala does not either but I haven't had
much experience with it), and the benefit is clear to anyone who has
dealt with both.
=2D-=20
Arsen Arsenovi=C4=87

--=-=-=
Content-Type: application/pgp-signature; name="signature.asc"

-----BEGIN PGP SIGNATURE-----

iKoEARYKAFIWIQT+4rPRE/wAoxYtYGFSwpQwHqLEkwUCamFI+hsUgAAAAAAEAA5t
YW51MiwyLjUrMS4xMiwyLDIYHGFhcnNlbm92aWNAYmF5bGlicmUuY29tAAoJEFLC
lDAeosSTyZgA/1Gv4rX9w/z8LFDNoJ57Brb+foHTUnvJcb5xjJuqX9fZAP9cJXhm
BlvA5D8BYOukNAKT3sAUHJ0QyxSxbifJM0MBDg==
=sODv
-----END PGP SIGNATURE-----
--=-=-=--