Hi everyone,
I had some time to look deeper at the two points I mentioned above.
- 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.
I did some check, and there really is an issue with the way verify_ssa.cc implements this “weak SSA” verification.
In this “weak-SSA” form, variables are allowed to be redefined (only with let-in expressions) if their definitions are the same (in order to allow things like (Let x = 1 in x) + (Let x = 1 in x+1)).
But I would expect this notion of being “the same” to mean “will lead to the same result after computing”, not “being syntactically equal”, as this the spirit of the SSA form (and other passes could use this information to avoid some re-computations for instance).
But currently, verify_ssa implements the SSA verification by using the ExprDeepEqual check, which looks for a syntactical equality. So a function call (like f()) will of course be found deeply equal to itself.
But that leads the verify SSA pass to think that
(Let x = f() in x) + (Let x = f() in x) is in weak SSA-form, when to me it is not ! (unless we know or can prove that the function ‘f’ has no side effects).
You can try this code to easily verify what I’m saying:
RelayExpr fun = GlobalVar("fun");
Array<PrimExpr> emptyArray;
// Function call : f()
Call call = Call(DataType::Int(32), fun, emptyArray);
// 1 - What does ExprDeepEqual tells?
ExprDeepEqual deep_equal_;
if (deep_equal_(call, call))
{
std::cout << "Yes, f() is deeply equal to f()" << std::endl;
}
else
{
std::cout << "No, f() is NOT deeply equal to f()" << std::endl;
}
// 2 - What does VerifySSA tells?
Var x("x");
// Let x = f() in x
Let let1 = Let(x, call, x);
// Let x = f() in x
Let let2 = Let(x, call, x);
// (Let x = f() in x) + (Let x = f() in x)
PrimExpr sum = Add(let1, let2);
Var buffer("Mem");
Var i1("i1");
// Mem[i1] = (Let x = f() in x) + (Let x = f() in x);
Stmt progStmt = Store(buffer, sum, i1, IntImm(DataType::Int(32), 1));
// Just a main function calling progStmt
Array<tir::Var> emptyVars;
PrimFunc prog = PrimFunc(emptyVars, progStmt);
if(VerifySSA(prog))
{
std::cout << "Handwritten prog Is SSA!" << std::endl;
}
else
{
std::cout << "Handwritten prog is NOT SSA" << std::endl;
}
Which will tell that f() and f() are deeply equal (which is fine), and that the program is in quasi SSA form (which is wrong).
If you tell me that I am correct thinking that VerifySSA() should not return true here, then I will create a proper issue for that and will then try to fix it myself to help.
And just to be clear, the problem does not come from ExprDeepEqual, as it is right to tell that f() is deeply equal to f(). It is just that VerifySSA() should be stricter than that.
- 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?
After looking again at this second point, I was wrong on this one and everything is good regarding this.
It’s just that this “weak-SSA form” allows variables redefinition for Let-In expression (but not for Let-in statements!) as long as the definitions are the same. But for a Let-in statement, it is forbidden to have any kind of redefinition, and this is checked carefully by MarkDef(), which is called systematically. So there is no problem here.
Thanks!
