Great. Thanks a lot for your time, I really appreciate it.
I had a quick look at the analysis pass which does this verification. I think I
found it in src/tir/analysis/verify_ssa.cc, and there a a couple of things I
don't fully understand about it and would love to have some input if someone
knows.
Of course, this visitor explores the AST of the input (both expressions and
statements), trying to find variables that are defined multiple times. Actually
I realized that variables that are mapped to the same value are allowed. Let's
call this quasi-SSA form.
So in this recursive exploration, we have the important case of a LetNode (the
Let-In construction as an expression), and it does what I would have expected :
if it finds the current variable being defined by this Let-In in the hash-table
of previously defined variables, it will return false if the value associated
to the value found in the table (it->second) is not "deeply-equal" to the value
to which we are trying to bind this variable now (op->value). Great.
1) There is just one thing here that annoys me here:
I had a look at this deep_equal() function, which is in fact an operator () on
the class ExprDeepEqual (in include/tvm/tir/analysis.h), which is being
implemented in deep_equal.cc.
And I would have expected it to be wary of function calls, that could -despite
being deeply_equal on the surface- lead to different value.
I'm thinking of something like :
Let x = funcWithSideEffect 42 in
Let x = funcWithSideEffect 42 in
x+x
x can seem to be associated to the same value in both cases (funcWithSideEffect
42) and deep_equal_() will answer yes, but if as its name suggests
funcWithSideEffect() does some side effects which makes it such that it does
not always return the same value when called with the same argument, then it
won't be in quasi-SSA form.
If later someone uses this quasi-SSA property that for removing redundant
computation, the semantics of the program would not be preserved.
But perhaps I missed it and this kind of situation is prevented somewhere.
2) Another thing that I don't understand is why the same verification is not
performed for a LetStmtNode (i.e. the Let-In construction as a statement).
Instead, it only marks the variable that it seens in the hash-table. But what
if it was already in the hash-table? Shouldn't we check that and if we find it,
and if not associated to the same value, then returning false?
Currently, I have the impression that if the second/third/etc redefinitions are
being done in a Let-In Statement, that will pass the bar when it should not be
considered in quasi-SSA form.
But I'm sure I've missed something, as if many passes rely in this, we would
probably have seen many problems if this verification was too weak.
I'll try to define some toy TIR programs to check that in practice, but
meanwhile if someone has any explanation would be very happy to learn more
about this.
Kind regards,
Franck
---
[Visit
Topic](https://discuss.tvm.apache.org/t/tir-are-multiple-let-in-with-the-same-var-allowed-ssa/10881/5)
to respond.
You are receiving this because you enabled mailing list mode.
To unsubscribe from these emails, [click
here](https://discuss.tvm.apache.org/email/unsubscribe/b7b1052031437bbd88fa09420c2a3cd09eb265ac6df301bb623ab0a86f88c73f).
