Program analysis too loopy? Set the loops aside

Program analysis too loopy? Set the loops aside

For access to this article, please select a purchase option:

Buy article PDF
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
IET Software — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

Among the many obstacles to efficient and sound program analysis, loops may be the most prevalent. In program analyses that traverse paths, loops introduce a variable, possibly infinite and number of paths. This study assesses the potential of a program analysis technique that analyses loops separately and replaces the loop with a summary, similar to how many analyses use summaries for interprocedural analysis. This study is conducted by comparing the path counts when loops are analysed separately to a baseline path count where loops are traversed at most once. Although the number of paths is decreased in many cases, the magnitude of the decrease is typically not sufficient for long, complex functions. In addition, loops are classified by the task they perform, analysed using the number of paths as an estimate of their complexity and further inspected for programming elements that may make loop analysis more difficult. Of the 2869 loops used in this study, 84% of the loops have fewer than ten paths and only 1.3% have more than 10 000 paths. Nearly 60% of the loops traverse arrays or strings and roughly half of the loops contain a function call.


    1. 1)
      • 1. King, J.: ‘Symbolic execution and program testing’, Commun. ACM, 1976, 19, (7), pp. 385394 (doi: 10.1145/360248.360252).
    2. 2)
      • 2. Bush, W., Pincus, J., Sielaff, D.: ‘A static analyzer for finding dynamic programming errors’, Softw., Pract. Exp., 2000, 30, (7), pp. 775802 (doi: 10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H).
    3. 3)
      • 3. Pǎsǎreanu, C., Mehlitz, P., Bushnell, D., et al: ‘Combining unit-level symbolic execution and system-level concrete execution for testing NASA software’. Proc. Int. Symp. Software Testing and Analysis, Seattle, Washington, 2008, pp. 1526.
    4. 4)
      • 4. Godefroid, P., Luchaup, D.: ‘Automatic partial loop summarization in dynamic test generation’. Proc. 2011 Int. Symp. Software Testing and Analysis, Toronto, Canada, 2011, pp. 2333.
    5. 5)
      • 5. Abd-El-Hafiz, S., Basili, V.: ‘A knowledge-based approach to the analysis of loops’, IEEE Trans. Softw. Eng., 1996, 22, (5), pp. 339360 (doi: 10.1109/32.502226).
    6. 6)
      • 6. Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.: ‘Loop summarization using abstract transformers’. Proc. Sixth Int. Symp. Automated Technology for Verification and Analysis, Seoul, Korea, 2008, pp. 111125.
    7. 7)
      • 7. GrammaTech, Inc.: ‘CodeSurfer’, accessed March 2012.
    8. 8)
      • 8. Halstead, M.: ‘Elements of software science’ (Elsevier Science Inc., 1977).
    9. 9)
      • 9. Kovács, L., Voronkov, A.: ‘Finding loop invariants for programs over arrays using a theorem prover’. Proc. 12th Int. Conf. Fundamental Approaches to Software Engineering, York, UK, 2009, pp. 470485.
    10. 10)
      • 10. Martel, M.: ‘Improving the static analysis of loops by dynamic partitioning techniques’. Proc. Third Int. Workshop on Source Code Analysis and Manipulation, Amsterdam, The Netherlands, 2003, pp. 1321.
    11. 11)
      • 11. Flanagan, C., Qadeer, S.: ‘Predicate abstraction for software verification’. Proc. Symp. Principles of Programming Languages, Portland, Oregon, 2002, pp. 191202.
    12. 12)
      • 12. Lokuciejewski, P., Cordes, D., Falk, H., Marwedel, P.: ‘A fast and precise static loop analysis based on abstract interpretation, program slicing and polytope models’. Proc. Int. Symp. Code Generation and Optimization, Seattle, Washington, 2009, pp. 136146.
    13. 13)
      • 13. Kirner, M.: ‘Automatic loop bound analysis of programs written in C’. Master's thesis, Technischen Universitat at Wien, 2006.
    14. 14)
      • 14. Burnim, J., Jalbert, N., Stergiou, C., Sen, K.: ‘Looper: lightweight detection of infinite loops at runtime’. Proc. IEEE/ACM Int. Conf. Automated Software Engineering, Auckland, New Zealand, 2009, pp. 161169.
    15. 15)
      • 15. White, L., Wiszniewski, B.: ‘Path testing of computer programs with loops using a tool for simple loop patterns’, Softw., Pract. Exp., 1991, 21, (10), pp. 10751102 (doi: 10.1002/spe.4380211007).
    16. 16)
      • 16. Xie, Y., Chou, A., Engler, D.: ‘ARCHER: using symbolic, path-sensitive analysis to detect memory access errors’. Proc. Ninth European Software Engineering Conf. held jointly with 11th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, Helsinki, Finland, 2003, pp. 327336.
    17. 17)
      • 17. Hu, L., Harman, M., Hierons, R., Binkley, D.: ‘Loop squashing transformations for amorphous slicing’. Proc. 11th Working Conf. Reverse Engineering, Delft, The Netherlands, 2004, pp. 152160.
    18. 18)
      • 18. Ngo, M., Tan, H.: ‘Detecting large number of infeasible paths through recognizing their patterns’. Proc. Sixth Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. Foundations of Software Engineering, Dubrovnik, Croatia, 2007, pp. 215224.
    19. 19)
      • 19. Binkley, D., Harman, M., Lakhotia, K.: ‘FlagRemover: a testability transformation for transforming loop-assigned flags’, ACM Trans. Softw. Eng. Methodol., 2011, 20, (3), pp. 133 (doi: 10.1145/2000791.2000796).
    20. 20)
      • 20. Zhao, Y., Gong, Y., Liu, L., Xiao, Q., Yang, Z.: ‘Context-sensitive interprocedural defect detection based on a unified symbolic procedure summary model’. Proc. 11th Int. Conf. Quality Software, Madrid, Spain, 2011, pp. 5160.
    21. 21)
      • 21. Yorsh, G., Yahav, E., Chandra, S.: ‘Generating precise and concise procedure summaries’. Proc. 35th Annual Symp. Principles of Programming Languages, San Francisco, California, 2008, pp. 221234.
    22. 22)
      • 22. Ancourt, C., Coelho, F., Irigoin, F.: ‘A modular static analysis approach to affine loop invariants detection’, Electron. Notes Theor. Comput. Sci., 2010, 267, (1), pp. 316 (doi: 10.1016/j.entcs.2010.09.002).
    23. 23)
      • 23. Saxena, P., Poosankam, P., McCamant, S., Song, D.: ‘Loop-extended symbolic execution on binary programs’. Proc. Int. Symp. Software Testing and Analysis, Chicago, Illinois, 2009, pp. 225236.
    24. 24)
      • 24. Sen, K., Marinov, D., Agha, G.: ‘CUTE: a concolic unit testing engine for C’. Proc. 10th European Software Engineering Conf. held jointly with 13th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, Lisbon, Portugal, 2005, pp. 263272.
    25. 25)
      • 25. Tillmann, N., de Halleux, J.: ‘Pex–white box test generation for .NET’, Tests Proofs, Lecture Notes Comput. Sci., 2008, 4966, pp. 134153 (doi: 10.1007/978-3-540-79124-9_10).
    26. 26)
      • 26. Larson, E.: ‘A plethora of paths’. Proc. IEEE 17th Int. Conf. Program Comprehension, Vancouver, Canada, 2009, pp. 4049.
    27. 27)
      • 27. Gabel, M., Su, Z.: ‘A study of the uniqueness of source code’. Proc. 18th ACM SIGSOFT Int. Symp. Foundations of Software Engineering, Santa Fe, New Mexico, 2010, pp. 147156.
    28. 28)
      • 28. Harman, M., Hierons, R., Danicic, S., Howroyd, J., Laurence, M., Fox, C.: ‘Node coarsening calculi for program slicing’. Proc. Eighth Working Conf. Reverse Engineering, Stuttgart, Germany, 2001, pp. 2534.
    29. 29)
      • 29. Das, M., Lerner, S., Seigle, M.: ‘ESP: path-sensitive program verification in polynomial time’. Proc. Conf. Programming Language Design and Implementation, Berlin, Germany, 2002, pp. 5768.
    30. 30)
      • 30. Dillig, I., Dillig, T., Aiken, A.: ‘Sound, complete and scalable path-sensitive analysis’. Proc. Conf. Programming Language Design and Implementation, Tucson, Arizona, 2008, pp. 270280.
    31. 31)
      • 31. Ball, T., Larus, J.: ‘Efficient path profiling’. Proc. 29th Annual ACM/IEEE Int. Symp. Microarchitecture, Paris, France, 1996, pp. 4657.
    32. 32)
      • 32. McCabe, T.: ‘A complexity measure’, IEEE Trans. Softw. Eng., 1976, SE-2, (4), pp. 308320 (doi: 10.1109/TSE.1976.233837).
    33. 33)
      • 33. Henry, S., Kafura, D., Harris, K.: ‘On the relationships among three software metrics’, ACM SIGMETRICS Perform. Eval. Rev., 1981, 10, (1), pp. 8188 (doi: 10.1145/1010627.807911).
    34. 34)
      • 34. Scientific Toolworks, Inc: ‘Understand source code analysis & metrics’., accessed March 2012.
    35. 35)
      • 35. Gulwani, S., Tiwari, A.: ‘Computing procedure summaries for interprocedural analysis’. Proc. European Symp. Programming, Braga, Portugal, 2007, pp. 253267.

Related content

This is a required field
Please enter a valid email address