Hi, I'm currently working on a pass for symbolic loop analysis and like to start a small discussion. The goal is to get an expression for the loop enabling calculation of e.g. the trip count. Furthermore, inter-loop-dependencies should be regarded. I'm currently testing with Livermore loops. For instance, the following code (Livermore kernel 2) for (l = 1; l <= loop; l++) { ii = n; ipntp = 0; do { ipnt = ipntp; ipntp += ii; ii /= 2; i = ipntp - 1; for (k = ipnt + 1; k < ipnpt; k = k + 2) { [...] } } while (ii > 0); } currently leads to this analysis result: L0: l[Init: 1] <= ConstExpr by l += 1 L1: ii[Init: ConstExpr] > 0 by ii /= 2 L2: k[Init: ipnt + 1] < ipntp[Init: 0, Inc: ipntp + ii] by k += 2 plus the info, that L2 is contained in L1 is contained in L0: L0 -> L1 -> L2 SCEV for such a case results in "unpredictable backedge-taken count". The "init" and "inc" at "ipntp" for L2 also contain the information, that "init" occurs on every L0 and "inc" occurs on every L1. Based on the evaluation of the loop properties and the generated formulas, one could for instance pre-calculate the values for l, ii and k, of course only if the needed parameters are known. What do you think? Would this pass be useful for others except for me? Is there any related work? I've found [1], but they do not use LLVM and it seems to specialized to me. Cheers, Sebastian [1]: Knoop, J., Kovács, L., & Zwirchmayr, J. (2012). Symbolic loop bound computation for wcet analysis. In Perspectives of Systems Informatics (pp. 227-242). Springer Berlin, Heidelberg. http://www.complang.tuwien.ac.at/lkovacs/pub/PSI11_Kovacs.pdf -- Mit freundlichen Grüßen / Kind regards Sebastian Dreßler Zuse Institute Berlin (ZIB) Takustraße 7 D-14195 Berlin-Dahlem Germany dressler at zib.de Phone: +49 30 84185-261 http://www.zib.de/