Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Debug-localize-repair: a symbiotic construction for heap manipulations

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We present Wolverine2, an integrated Debug-Localize-Repair environment for heap manipulating programs. Wolverine2 provides an interactive debugging environment: while concretely executing a program via on an interactive shell supporting common debugging facilities, Wolverine2 displays the abstract program states (as box-and-arrow diagrams) as a visual aid to the programmer, packages a novel, proof-directed repair algorithm to quickly synthesize the repair patches and a new bug localization algorithm to reduce the search space of repairs. Wolverine2 supports “hot-patching” of the generated patches to provide a seamless debugging environment, and also facilitates new debug-localize-repair possibilities: specification refinement and checkpoint-based hopping. We evaluate Wolverine2 on 6400 buggy programs (generated using automated fault injection) on a variety of data-structures like singly, doubly, and circular linked lists, AVL trees, Red-Black trees, Splay Trees and Binary Search Trees; Wolverine2 could repair all the buggy instances within realistic programmer wait-time (less than 5 s in most cases). Wolverine2 could also repair more than 80% of the 247 (buggy) student submissions where a reasonable attempt was made.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18

Similar content being viewed by others

Availability of data and material

To be made available post-publication.

Notes

  1. We thank the anonymous reviewers of the preliminary conference version of this paper for suggesting this feature.

References

  1. Abreu R, Zoeteweij P, Golsteijn R, Van Gemund AJ (2009) A practical evaluation of spectrum-based fault localization. J Syst Softw 82(11):1780–1792

    Article  Google Scholar 

  2. Ball T, Naik M, Rajamani SK (2003) From symptom to cause: localizing errors in counterexample traces. In: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’03, New York, NY, USA. ACM

  3. Bavishi R, Pandey A, Roy S (2016) Regression aware debugging for mobile applications. In: Mobile! 2016: proceedings of the 1st international workshop on mobile development (invited paper), Mobile! 2016, New York, NY, USA., pp 21–22 Association for Computing Machinery

  4. Bavishi R, Pandey A, Roy S (2016) To be precise: regression aware debugging. In: Proceedings of the 2016 ACM SIGPLAN international conference on object-oriented programming, systems, languages, and applications, OOPSLA 2016, New York, NY, USA. ACM

  5. Bendersky E. Pycparser: C parser in Python. https://pypi.python.org/pypi/pycparser. Accessed 24 Jan 2017

  6. Bhatia S, Kohli P, Singh R (2018) Neuro-symbolic program corrector for introductory programming assignments. In: Proceedings of the 40th international conference on software engineering, ICSE ’18, New York, NY, USA. Association for Computing Machinery

  7. Chandra S, Torlak E, Barman S, Bodik R (2011) Angelic debugging. In: Proceedings of the 33rd international conference on software engineering, ICSE ’11, New York, NY, USA. ACM

  8. Chatterjee P, Chatterjee A, Campos J, Abreu R, Roy S (2020) Diagnosing software faults using multiverse analysis. In: Bessiere C (ed) Proceedings of the twenty-ninth international joint conference on artificial intelligence, IJCAI-20, vol 7. International Joint Conferences on Artificial Intelligence Organization, pp 1629–1635. Main track

  9. Chatterjee P, Roy S, Diep BP, Lal A (2020) Distributed bounded model checking. In: FMCAD, July 2020

  10. Das R, Ahmed UZ, Karkare A, Gulwani S (2016) Prutor: a system for tutoring CS1 and collecting student programs for analysis. CoRR, arXiv:1608.03828

  11. De Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the theory and practice of software, 14th international conference on tools and algorithms for the construction and analysis of systems, Berlin, Heidelberg. Springer-Verlag, pp 337–340

  12. Demsky B, Rinard M (2003) Automatic detection and repair of errors in data structures. In: Proceedings of the 18th annual ACM SIGPLAN conference on object-oriented programing, systems, languages, and applications, OOPSLA ’03, New York, NY, USA. ACM

  13. Elkarablieh B, Khurshid S (2008) Juzi: a tool for repairing complex data structures. In: Proceedings of the 30th international conference on software engineering, ICSE ’08, New York, NY, USA. ACM

  14. Feser JK, Chaudhuri S, Dillig I (2015) Synthesizing data structure transformations from input–output examples. In: Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, PLDI ’15, New York, NY, USA. ACM

  15. Geeks for Geeks. Data structures. http://www.geeksforgeeks.org/data-structures/. Accessed 24 Jan 2017

  16. Free Software Foundation. GDB Python API. https://sourceware.org/gdb/onlinedocs/gdb/Python-API.html. Accessed 25 Jan 2017

  17. Free Software Foundation. GDB: the GNU project debugger. https://sourceware.org/gdb/. Accessed 24 Jan 2017

  18. Garg A, Roy S (2015) Synthesizing heap manipulations via integer linear programming. In: Blazy S, Jensen T (eds) Static analysis, SAS 2015. Proceedings. Springer, Berlin

    Google Scholar 

  19. Godefroid P, Klarlund N, Sen K (2005) DART: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation, PLDI ’05, New York, NY, USA. ACM

  20. Golia P, Roy S, Meel KS (2020) Manthan: a data-driven approach for Boolean function synthesis. In: Lahiri SK, Wang C (eds) Computer aided verification (CAV). Springer, Cham, pp 611–633

    Chapter  Google Scholar 

  21. Golia P, Roy S, Slivovsky F, Meel KS (2021) Engineering an efficient Boolean functional synthesis engine. In: ICCAD

  22. Groce A, Chaki S, Kroening D, Strichman O (2006) Error explanation with distance metrics. Int J Softw Tools Technol Transf 8(3):229–247

    Article  Google Scholar 

  23. Grumberg O, Lerda F, Strichman O, Theobald M (2005) Proof-guided underapproximation-widening for multi-process systems. In: Proceedings of the 32Nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’05, New York, NY, USA. ACM

  24. Gulwani S, Radiček I, Zuleger F (2018) Automated clustering and program repair for introductory programming assignments. In: Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, New York, NY, USA. Association for Computing Machinery, pp 465–480

  25. Guo PJ (2013) Online python tutor: embeddable web-based program visualization for CS education. In: Proceeding of the 44th ACM technical symposium on computer science education, SIGCSE ’13, New York, NY, USA. ACM

  26. Gupta R, Pal S, Kanade A, Shevade S (2017) Deepfix: fixing common C language errors by deep learning. In: Proceedings of the Thirty-First AAAI conference on artificial intelligence, AAAI’17. AAAI Press, pp 1345–1351

  27. Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580

    Article  MATH  Google Scholar 

  28. Hu Q, Samanta R, Singh R, D’Antoni L (2019) Direct manipulation for imperative programs. In: Chang BY (ed) Static analysis. Springer, Cham, pp 347–367

    Chapter  Google Scholar 

  29. Hu Y, Ahmed UZ, Mechtaev S, Leong B, Roychoudhury A (2019) Re-factoring based program repair applied to programming assignments. In: ASE ’19. IEEE Press, pp 388–398

  30. igraph—the network analysis package. http://igraph.org/python/. Accessed 24 Jan 2017

  31. Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32Nd ACM/IEEE international conference on software engineering, ICSE ’10, New York, NY, USA, vol 1. ACM

  32. Jones JA, Harrold MJ (2005) Empirical evaluation of the tarantula automatic fault-localization technique. In: Proceedings of the 20th IEEE/ACM international conference on automated software engineering, ASE ’05, New York, NY, USA. ACM

  33. Jose M, Majumdar R (2011) Bug-assist: assisting fault localization in ANSI-C programs. In: Proceedings of the 23rd international conference on computer aided verification, CAV’11, Berlin, Heidelberg. Springer-Verlag

  34. Jose M, Majumdar R (2011) Cause clue clauses: error localization using maximum satisfiability. In: Proceedings of the 32nd ACM SIGPLAN conference on programming language design and implementation, PLDI ’11, New York, NY, USA. ACM

  35. Kneuss E, Koukoutos M, Kuncak V (2015) Deductive program repair. In: CAV

  36. Le Goues C, Nguyen T, Forrest S, Weimer W (2012) GenProg: a generic method for automatic software repair. IEEE Trans Softw Eng 38:54–72

    Article  Google Scholar 

  37. Leung A, Sarracino J, Lerner S (2015) Interactive parser synthesis by example. SIGPLAN Not 50(6):565–574

    Article  Google Scholar 

  38. Liblit B, Naik M, Zheng AX, Aiken A, Jordan MI (2005) Scalable statistical bug isolation. In: Proceedings of the 2005 ACM SIGPLAN conference on programming language design and implementation, PLDI ’05, New York, NY, USA. ACM

  39. Liu C, Yan X, Fei L, Han J, Midkiff SP (2005) SOBER: statistical model-based bug localization. In: ESEC/FSE-13, New York, NY, USA. ACM

  40. Liu Y, Li B (2010) Automated program debugging via multiple predicate switching. In: Proceedings of the twenty-fourth AAAI conference on artificial intelligence, AAAI’10. AAAI Press

  41. Loncaric C, Ernst MD, Torlak E (2018) Generalized data structure synthesis. In: Proceedings of the 40th international conference on software engineering, ICSE ’18, New York, NY, USA. Association for Computing Machinery, pp 958–968

  42. Long F, Rinard M (2016) Automatic patch generation by learning correct code. In: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’16, New York, NY, USA. ACM

  43. Malik MZ, Siddiqui JH, Khurshid S (2011) Constraint-based program debugging using data structure repair. In: 2011 fourth IEEE international conference on software testing, verification and validation, March 2011

  44. Malik MZ, Ghori K, Elkarablieh B, Khurshid S (2009) A case for automated debugging using data structure repair. In: Proceedings of the 2009 IEEE/ACM international conference on automated software engineering, ASE ’09, USA. IEEE Computer Society

  45. Mechtaev S, Yi J, Roychoudhury A (2015) DirectFix: looking for simple program repairs. In: Proceedings of the 37th international conference on software engineering, ICSE ’15, Piscataway, NJ, USA, vol 1, pp 448–458

  46. Mechtaev S, Yi J, Roychoudhury A (2016) Angelix: scalable multiline program patch synthesis via symbolic analysis. In: Proceedings of the 38th international conference on software engineering, ICSE ’16, New York, NY, USA. ACM

  47. Modi V, Roy S, Aggarwal SK (2013) Exploring program phases for statistical bug localization. In: Proceedings of the 11th ACM SIGPLAN-SIGSOFT workshop on program analysis for software tools and engineering, PASTE ’13, New York, NY, USA. ACM

  48. Nguyen HD, Qi D, Roychoudhury A, Chandra S (2013) SemFix: program repair via semantic analysis. In: Proceedings of the 2013 international conference on software engineering, ICSE ’13, Piscataway, NJ, USA. IEEE Press

  49. Nguyen T-T, Ta Q-T, Chin W-N (2019) Automatic program repair using formal verification and expression templates. In: VMCAI

  50. Nguyen T, Weimer W, Le Goues C, Forrest S (2009) Using execution paths to evolve software patches. In: International conference on software testing, verification and validation workshops, 2009. ICSTW’09. IEEE, pp 152–153

  51. Pandey A, Kotcharlakota PR, Roy S (2019) Deferred concretization in symbolic execution via fuzzing. In: Proceedings of the 28th ACM SIGSOFT international symposium on software testing and analysis, ISSTA 2019, New York, NY, USA. Association for Computing Machinery, pp 228–238

  52. Pham V-T, Khurana S, Roy S, Roychoudhury A (2017) Bucketing failing tests via symbolic analysis. In: Huisman M, Rubin J (eds) Fundamental approaches to software engineering. Springer, Berlin, pp 43–59

    Chapter  Google Scholar 

  53. Polikarpova N, Sergey I (2019) Structuring the synthesis of heap-manipulating programs. Proc ACM Program Lang 3:1–30

    Article  Google Scholar 

  54. Pu Y, Narasimhan K, Solar-Lezama A, Barzilay R (2016) Sk_p: a neural program corrector for moocs. In: Companion proceedings of the 2016 ACM SIGPLAN international conference on systems, programming, languages and applications: software for humanity, SPLASH Companion 2016, page 39-40, New York, NY, USA. Association for Computing Machinery

  55. Rolim R, Soares G, D’Antoni L, Polozov O, Gulwani S, Gheyi R, Suzuki R, Hartmann B (2017) Learning syntactic program transformations from examples. In: Proceedings of the 39th international conference on software engineering, ICSE ’17. IEEE Press

  56. Roy S, Hsu J, Albarghouthi A (2021) Learning differentially private mechanisms. In: 2021 IEEE symposium on security and privacy (SP), Los Alamitos, CA, USA, May 2021. IEEE Computer Society, pp 852–865

  57. Roy S (2013) From concrete examples to heap manipulating programs. In: Logozzo F, Fähndrich M (eds) Static analysis: 20th international symposium, SAS 2013, Seattle, WA, USA, 20–22 June 2013. Proceedings. Springer, Berlin

  58. Roy S, Pandey A, Dolan-Gavitt B, Hu Y (2018) Bug synthesis: challenging bug-finding tools with deep faults. In: Proceedings of the 2018 26th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering, ESEC/FSE 2018, New York, NY, USA. Association for Computing Machinery, pp 224–234

  59. Sen K, Marinov D, Agha G (2005) CUTE: a concolic unit testing engine for C. In: ESEC/FSE-13, New York, NY, USA. ACM

  60. Singal D, Agarwal P, Jhunjhunwala S, Roy S (2018) Parse condition: symbolic encoding of ll(1) parsing. In: Barthe G, Sutcliffe G, Veanes M (eds) LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning. EPiC series in computing, vol 57. EasyChair, pp 637–655

  61. Singh R, Gulwani S, Solar-Lezama A (2013) Automated feedback generation for introductory programming assignments. In: Proceedings of the 34th ACM SIGPLAN conference on programming language design and implementation, PLDI ’13, New York, NY, USA. Association for Computing Machinery

  62. Singh R, Solar-Lezama A (2011) Synthesizing data structure manipulations from storyboards. In: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on foundations of software engineering, ESEC/FSE ’11, New York, NY, USA. ACM

  63. Tan SH, Yoshida H, Prasad MR, Roychoudhury A (2016) Anti-patterns in search-based program repair. In: Proceedings of the 2016 24th ACM SIGSOFT international symposium on foundations of software engineering, FSE 2016, New York, NY, USA. Association for Computing Machinery, pp 727–738

  64. Verma A, Kalita PK, Pandey A, Roy S (2020) Interactive debugging of concurrent programs under relaxed memory models. In: Proceedings of the 18th ACM/IEEE international symposium on code generation and optimization, CGO 2020, New York, NY, USA. Association for Computing Machinery, pp 68–80

  65. Verma S, Roy S (2017) Synergistic debug-repair of heap manipulations. In: Proceedings of the 2017 11th joint meeting on foundations of software engineering, ESEC/FSE 2017, New York, NY, USA. ACM

  66. Wang K, Singh R, Su Z (2017) Dynamic neural program embedding for program repair. arXiv,  arXiv:1711.07163

  67. Wang K, Singh R, Su Z (2018) Search, align, and repair: data-driven feedback generation for introductory programming exercises. In: Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018,, New York, NY, USA. Association for Computing Machinery pp 481–495

  68. Weimer W (2006) Patches as better bug reports. In: Proceedings of the 5th international conference on generative programming and component engineering, GPCE ’06, New York, NY, USA. ACM

  69. Weimer W, Nguyen T, Le Goues C, Forrest S (2009) Automatically finding patches using genetic programming. In: Proceedings of the 31st international conference on software engineering, ICSE ’09, Washington, DC, USA. IEEE Computer Society

  70. Zeller A (2002) Isolating cause-effect chains from computer programs. In: Proceedings of the 10th ACM SIGSOFT symposium on foundations of software engineering, SIGSOFT ’02/FSE-10, New York, NY, USA. ACM

  71. Zeller A, Hildebrandt R (2002) Simplifying and isolating failure-inducing input. IEEE Trans Softw Eng 28(2):183–200

    Article  Google Scholar 

  72. Zimmermann T, Zeller A (2002) Visualizing memory graphs. In: Diehl S (ed) Revised lectures on software visualization, international seminar. Springer-Verlag, London

    Google Scholar 

Download references

Funding

Not applicable.

Author information

Authors and Affiliations

  1. Paul G. Allen School of Computer Science and Engineering, University of Washington, Seattle, USA

    Sahil Verma

  2. Department of Computer Science and Engineering, Indian Institute of Technology Kanpur, Kanpur, India

    Subhajit Roy

Authors
  1. Sahil Verma
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Subhajit Roy
    View author publications

    You can also search for this author in PubMed Google Scholar

Contributions

Not applicable.

Corresponding author

Correspondence to Sahil Verma.

Ethics declarations

Conflicts of interest

The second author has visits and collaborations with NUS Singapore, UW-Madison, Microsoft, University of Lisbon and NYU.

Code availability

To be made available post-publication.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

A Theoretical analysis of the bug localization algorithm

A Theoretical analysis of the bug localization algorithm

Let \(\mathcal {I}\) be the identity function that copies the \(\omega _{pre} \text { or } \omega _{post}\). Then,

  • \([\omega ^f_0, \omega ^f_1, \omega ^f_2, \dots , \omega ^f_n] \leftarrow [\mathcal {I}, \Delta _{1, 1}, \Delta _{1, 2}, \dots \Delta _{1, n}] (\omega _{pre}\), P)

  • \([\Omega ^b_0, \Omega ^b_1, \Omega ^b_2, \dots , \Omega ^b_n] \leftarrow [\nabla _{n, 1}, \nabla _{n, 2}, \dots \nabla _{n, n}, \mathcal {I}] (\omega _{post}\), P)

  • \([\Gamma _0, \Gamma _1, \Gamma _2, \dots , \Gamma _n] \leftarrow [\omega ^f_0, \omega ^f_1, \omega ^f_2, \dots , \omega ^f_n] \otimes [\Omega ^b_0, \Omega ^b_1, \Omega ^b_2, \dots , \Omega ^b_n]\); \(\Omega \) is a set of states while \(\omega \) is a single state.

Theorem 1

If a real bug is at location i, it implies that i is in the suspicious set

Proof

Let \(\hat{P}\) and P denote the correct and buggy programs, respectively.

Assumption: Assume that in the trace \(P_n\) (sequence of statements of length n), the ith statement has a real bug and \(LHS(s_i)\) be x. Let us define the correct execution as the forward execution states of \(\hat{P}\) at each program point. Let \(\Delta _{0, i}(\omega _{pre}, \hat{P})[x] = \texttt {n1}\), \(\Delta _{0, i}(\omega _{pre}, P)[x] = \texttt {n2}\), \(\omega _{post}[x] = \texttt {n3}\) and \(\omega _{pre}[x] = \texttt {n0}\). Therefore, the number of nodes and points-to pairs in the datastructure, \(\texttt {n} \ge 2 \). [Assump1]

Fig. 19
figure 19

Illustrations for the proof of theorem 1

Full size image

Case 1

The ith statement is upward exposed: this is illustrated in Fig. 19a.

  1. 1.

    \(\Delta _{0, i-1}(\omega _{pre}, P)\) = \(\Delta _{0, i-1}(\omega _{pre}, \hat{P})\) [Since the bug is in ith stmt]

  2. 2.

    \(\nabla _{n, i}(\omega _{post}, P)[x] = \omega _{pre}[x]\) [\(asgn_{1}\) rule in Fig. 12]

  3. 3.

    \(\Delta _{0, i-1}(\omega _{pre}, P)[x] = \omega _{pre}[x]\) [Lemma  1]

  4. 4.

    \(\nabla _{n, i}(\omega _{post}, P)[x] = \Delta _{0, i-1}(\omega _{pre}, P)[x]\) [From 2 and 3]

  5. 5.

    \(\Gamma _{i-1}[x] = 0\) [Since \(\Gamma _{i-1} = (\nabla _{n, i} - \Delta _{0, i-1}) * (multiplying factor)\) and \(\nabla _{n, i} - \Delta _{0, i-1} = 0\)]

  6. 6.

    Also since ith statement is upward exposed there is no previous splitting of states when this statement is backtracked. [Backward Semantics in Fig. 12]

  7. 7.

    Without loss of generality, lets say there are already p backtracked states before ith statement is backtracked.

  8. 8.

    Subcase 1: There has not been any splitting for x in the backward execution. Therefore for all the p states (in \(\nabla _{n, i+1}\)), x points-to \(\texttt {n3}\) [Stmt is both upward and downward exposed]

  9. 9.

    \(\Gamma _{i}[x] = p * multiplying factor > 0\) [From 8 and since \(\Gamma _{i} = (\nabla _{n, i+1} - \Delta _{0, i}) * (multiplying factor)\)]

  10. 10.

    Subcase 2: There has been a previous splitting for x in the backward execution. Therefore in atleast one of the p states, the value of \(x \ne \texttt {n1}\). This is because splitting happens uniformly across all nodes and there are atleast 2 nodes in the data-structure. [Rules in Fig. 12]

  11. 11.

    \(\Gamma _{i}[x] > 0\) [From 10]

  12. 12.

    Hence for loop at step 5 in Algorithm 4, since \(\Gamma _{i-1} \ne \Gamma _{i}, i^{th}\) statement will be added to suspicious set.

Case 2

The ith statement is sandwiched. We add all sandwiched statements to the suspicious set since the program loses all information regarding the correctness of such a statement.

Case 3

The ith statement is downward exposed and not upward exposed: this is illustrated in Fig. 19b.

  1. 1.

    There will be splitting of states when ith statement is backtracked. [\(asgn_{2}\) rule in Fig. 12]

  2. 2.

    Without loss of generality, lets say there are p backtracked states before ith statement is backward executed.

  3. 3.

    In all these p states, the value of variable \(x = \texttt {n3}\). [Lemma  2]

  4. 4.

    Let there be \(\texttt {s}\) splits for x until the full backtrack of the program.

  5. 5.

    The final number of states after backtracking is \(n^{s} = M\), where n is the number of nodes and points-to pairs [Rules in Fig. 12]

  6. 6.

    Each of the p states contribute a difference of 1 in \(\Gamma _{i} = p * \frac{n^s}{p} = n^s\) [\(\Gamma _{i} = (\nabla _{n, i+1} - \Delta _{0, i}) * (multiplying factor)\)]

  7. 7.

    \(\Gamma _{i-1} = \frac{n^s}{p*n} * (n-1)*p = n^s - n^{s-1}\) [Out of n nodes, 1 will match with a node in \(\Delta _{0, i}(\omega _{pre}, {P})\); uniform splitting]

  8. 8.

    \(\Gamma _{i-1} - \Gamma _{i} = n^s - n^{s-1} - n^s \ne 0\), for \(n > 1\) [Since number of nodes and points-to pairs> 1]

  9. 9.

    Hence, for the loop at step 5 in Algorithm 4, since \(\Gamma _{i-1} \ne \Gamma _{i}, i^{th}\) statement will be added to suspicious set.

In all cases, Algorithm 4 successfully catches the buggy statement.

Theorem 2

If C is the set of suspicious locations captured by Algorithm 4, then replacing all statements \(s \notin C\) by \(lhs = *\) maintains the ground truth repair in the proof-guided repair algorithm.

Proof

Any statement which depends on a buggy statement is also put in the suspicious set by our algorithm. This is natural because upon execution of the buggy statement, an incorrect state is achieved, and any statements which further depend on this state would be buggy with respect to the ground truth state. Hence, we can slice away the statement from repair by making them non-deterministic. \(\square \)

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Verma, S., Roy, S. Debug-localize-repair: a symbiotic construction for heap manipulations. Form Methods Syst Des 58, 399–439 (2021). https://doi.org/10.1007/s10703-021-00387-z

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-021-00387-z

Keywords

Search

Navigation