Artifact ICST 2026 submission 157

Abstract. TODO. Note: The datasets and code are anonymised and will be made publicly available and de-anonymised upon acceptance, including a mapping to the corresponding GitHub repositories and the full commit histories of the SUTs, along with the original pull requests (PRs) and reported issues content and links. Public Bug Reports, Pull Requests, and References Anon. for Review. We will de-anonymise the records upon acceptance. Finding Pipeline Component Report venue Status Evidence #1 A Poly/ML lexer X86 Anon4Review Confirmed Confirmed bug with a proposed fix; no fix approved. #2 A Poly/ML lexer X86 Anon4Review Fixed Commit Anon4Review #3 A Poly/ML lexer X86 Anon4Review Fixed Commit Anon4Review #4 A Poly/ML lexer X86 N/A WON’T FIX Anon4Review #5 A Poly/ML lexer X86 N/A Not reported Informational observation; likely intentional parser deviation #6 B Poly/ML ARM64 Anon4Review Reported A fix was suggested as Anon4Review #7 B Poly/ML ARM64 Anon4Review WON’T FIX #8 B Poly/ML ARM64 Anon4Review Fixed Commit Anon4Review #9 D Isabelle/jEdit Anon4Review Fixed Maintainers committed a different patch (Anon4Review) in response to our report that prevents the observed behaviour from happening. #10 D Isabelle/jEdit NA Fixed Old bug. Fixed (before we reported it) on the trunk (Anon4Review). #11 D Isabelle/jEdit Anon4Review Fixed Maintainers committed a different patch (Anon4Review) in response to our report that prevents the observed behaviour from happening. #12 C Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive #13 C Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive #14 C Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive #15 C Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive #16 C Isabelle/jEdit Anon4Review” False Positive Email evidence: differences in output confirmed, not significant. False Positive #17 C Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive #18 C Isabelle/jEdit Mailing list False Positive Email evidence: differences in output confirmed, not significant. False Positive #19 F Zipperposition GitHub Issue Anon4Review Fixed Anon4Review #20 F Zipperposition GitHub Issue Anon4Review Fixed Anon4Review #21 G E prover Direct email on Thursday, 2 April 2026 Fixed Commit Anon4Review: “Fixed parser source bug … Thanks to Anon4Review”. #22 G Zipperposition GitHub Issue Anon4Review Fixed Anon4Review #23 J Z3 NA Fixed Old bug in Isabelle-bundled Z3 4.4.0 #24 J Z3 NA Fixed Old bug in Isabelle-bundled Z3 4.4.0 #25 K Kernel NA Reported Known bug, PR XXXX #26 K Kernel NA Reported Known bug, PR XXXX Statistics on Report, Fix, and Close time of Reported Findings: Finding Pipeline Open Fixed Closed/Merged #1 A 19/03/2026 TODAY() TODAY() #2 A 10/03/2026 31/03/2026 06/05/2026 #3 A 10/03/2026 31/03/2026 06/05/2026 #4 A NA NA NA #5 A NA NA NA #6 B 16/04/2026 17/07/2026 TODAY() #7 B NA NA NA #8 B 16/04/2026 19/04/2026 30/04/2026 #9 D 02/04/2026 18/05/2026 18/05/2026 #10 D NA NA 22/12/2025 #11 D 14/04/2026 19/04/2026 19/04/2026 #12 C NA NA NA #13 C NA NA NA #14 C NA NA NA #15 C NA NA NA #16 C NA NA NA #17 C NA NA NA #18 C NA NA NA #19 F 23/03/2026 02/04/2026 03/04/2026 #20 F 04/04/2026 07/04/2026 07/04/2026 #21 G 02/04/2026 02/04/2026 02/04/2026 #22 G 16/04/2026 16/04/2026 28/05/2026 #23 J NA NA NA #24 J NA NA NA #25 K 26/10/2026 TODAY() TODAY() #26 K 26/10/2026 TODAY() TODAY() We added further details explaining how we identified fixes corresponding to bug reports when developers did not explicitly link a fix to a single reported finding. Finding #9 The fix was done just after the report. We used an LLM (OpenAI, 15/07/2026, GPT 5.5 High configuration) to map each fix to the reported issue: This changeset is **most closely related to Finding #9**, because it modifies `src/Pure/Concurrent/delay.scala` and the way delayed events are scheduled throughout Isabelle. However, **it does not appear to be the direct fix for Finding #9**. Finding #9 concerns an exception escaping from `Delay.run()`, killing the shared event-timer thread. Its proposed fix was to log the exception **without rethrowing it**. In this changeset, the relevant modification is instead: ```scala -if (do_run) event +if (do_run) app(event) ``` It also replaces the global `Delay` factory with `Delay_Ops`, introduces separate `GUI.Delay` and `Resources.Delay` objects, and supplies context-specific loggers and execution mechanisms. The GUI version, for example, sends the event through `GUI_Thread.later`. There is no shown removal of the problematic exception rethrow, and the changeset contains no new `catch` or exception-handling logic. Therefore: > **Classification: related follow-up/refactoring for Finding #9, but not sufficient evidence of the direct Finding #9 fix.** **Best label:** **Finding #9-related architectural change**, with medium confidence that it was motivated by or followed the Finding #9 discussion, but low confidence that this changeset itself fixes the reported exception-rethrow defect. Finding #11 The fix was done just after the report. We used an LLM (OpenAI, 15/07/2026, GPT 5.5 High configuration) to map each fix to the reported issue: This changeset is fixing **Finding #11 — XML serialisation null-handling corruption**. Finding #12 identifies this exact code in `XML.Output.string`: ```scala if (str == null) { builder ++= str } ``` Because Scala/Java’s `StringBuilder.append(null)` writes the four characters `"null"`, a null value could silently corrupt the serialised XML rather than causing an explicit failure. The changeset removes that special null branch: ```scala str foreach { ... } ``` Consequently, a null string is no longer silently converted into the text `"null"`. Instead, it fails, which reflects the maintainer’s stated position that valid XML trees must never contain null. The additional `Tree.toString` protection returns `"<malformed>"` for applicable XML errors, making top-level diagnostic output more robust. ### Classification > **Changeset `Anon4Review` → Finding #11** **Confidence:** Very high — it changes the exact `XML.Output.string` code described in Finding #11. There is a minor difference between the student’s proposed solution and the accepted implementation: * **Author patch:** make the null branch a no-op. * **Accepted approach:** remove permissive null handling and let malformed XML fail, while making `toString` output more defensive. Findings #13 to #18: The maintainer acknowledged that the reported differences are real, but argued that differences between batch build and PIDE should not automatically be treated as software bugs. We therefore classify such reports as false positives only when the observed divergence does not identify a concrete defect or actionable improvement. See msg00019 for further details. Finding #23 was a crash: Based on the trace, these are all test inputs that lead to an EXC_BAD_ACCESS at location 181: ================ mut_02539_230fd4c313 ================ (lldb) target create "/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3" Current executable set to '/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64). (lldb) settings set -- target.run-args "-smt2" "/Users/anon4review/smt_fuzz_v2/mutants/mut_02539_230fd4c313.smt2" (lldb) run warning: libobjc.A.dylib is being read from process memory. This indicates that LLDB could not read from the host's in-memory shared cache. This will likely reduce debugging performance. Process 8749 launched: '/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64) Process 8749 stopped * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010108954f) frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 z3`___lldb_unnamed_symbol_100348702: -> 0x1003487b7 <+181>: movsbl (%rax,%r14), %eax 0x1003487bc <+186>: cmpl $-0x1, %eax 0x1003487bf <+189>: je 0x1003487d4 ; <+210> 0x1003487c1 <+191>: testl %eax, %eax Target 0: (z3) stopped. (lldb) bt * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010108954f) * frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 frame #1: 0x0000000100349064 z3`___lldb_unnamed_symbol_100348fec + 120 frame #2: 0x0000000100349a63 z3`___lldb_unnamed_symbol_100349974 + 239 frame #3: 0x000000010034dfd0 z3`___lldb_unnamed_symbol_10034da76 + 1370 frame #4: 0x0000000100332867 z3`___lldb_unnamed_symbol_1003327b6 + 177 frame #5: 0x0000000100339b95 z3`___lldb_unnamed_symbol_100339b08 + 141 frame #6: 0x00000001002de2a2 z3`___lldb_unnamed_symbol_1002dd64e + 3156 frame #7: 0x00000001006ba18d z3`___lldb_unnamed_symbol_1006b9f90 + 509 frame #8: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #9: 0x00000001006bfca1 z3`___lldb_unnamed_symbol_1006bfae4 + 445 frame #10: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #11: 0x00000001006b68a6 z3`___lldb_unnamed_symbol_1006b6860 + 70 frame #12: 0x00000001006b6af1 z3`___lldb_unnamed_symbol_1006b69d0 + 289 frame #13: 0x00000001005d3bb9 z3`___lldb_unnamed_symbol_1005d39ee + 459 frame #14: 0x00000001005d3035 z3`___lldb_unnamed_symbol_1005d2fa4 + 145 frame #15: 0x00000001005d2af1 z3`___lldb_unnamed_symbol_1005d2806 + 747 frame #16: 0x000000010053477b z3`___lldb_unnamed_symbol_100534638 + 323 frame #17: 0x000000010051d453 z3`___lldb_unnamed_symbol_10051cd84 + 1743 frame #18: 0x00000001005234ec z3`___lldb_unnamed_symbol_1005233d0 + 284 frame #19: 0x0000000100510968 z3`___lldb_unnamed_symbol_100510940 + 40 frame #20: 0x000000010000b241 z3`___lldb_unnamed_symbol_10000b110 + 305 frame #21: 0x000000010000ac4e z3`___lldb_unnamed_symbol_10000aa10 + 574 frame #22: 0x0000000100000f74 z3`___lldb_unnamed_symbol_100000f40 + 52 (lldb) quit ================ mut_02606_702c48cda4 ================ (lldb) target create "/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3" Current executable set to '/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64). (lldb) settings set -- target.run-args "-smt2" "/Users/anon4review/smt_fuzz_v2/mutants/mut_02606_702c48cda4.smt2" (lldb) run warning: libobjc.A.dylib is being read from process memory. This indicates that LLDB could not read from the host's in-memory shared cache. This will likely reduce debugging performance. WARNING: unknown logic, ignoring set-logic command Process 8821 launched: '/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64) Process 8821 stopped * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010347c7cf) frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 z3`___lldb_unnamed_symbol_100348702: -> 0x1003487b7 <+181>: movsbl (%rax,%r14), %eax 0x1003487bc <+186>: cmpl $-0x1, %eax 0x1003487bf <+189>: je 0x1003487d4 ; <+210> 0x1003487c1 <+191>: testl %eax, %eax Target 0: (z3) stopped. (lldb) bt * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x60010347c7cf) * frame #0: 0x00000001003487b7 z3`___lldb_unnamed_symbol_100348702 + 181 frame #1: 0x0000000100349064 z3`___lldb_unnamed_symbol_100348fec + 120 frame #2: 0x0000000100349a63 z3`___lldb_unnamed_symbol_100349974 + 239 frame #3: 0x000000010034dfd0 z3`___lldb_unnamed_symbol_10034da76 + 1370 frame #4: 0x0000000100332867 z3`___lldb_unnamed_symbol_1003327b6 + 177 frame #5: 0x0000000100339b95 z3`___lldb_unnamed_symbol_100339b08 + 141 frame #6: 0x00000001002de2a2 z3`___lldb_unnamed_symbol_1002dd64e + 3156 frame #7: 0x00000001006bfcf5 z3`___lldb_unnamed_symbol_1006bfae4 + 529 frame #8: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #9: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #10: 0x00000001006b68a6 z3`___lldb_unnamed_symbol_1006b6860 + 70 frame #11: 0x00000001006b6af1 z3`___lldb_unnamed_symbol_1006b69d0 + 289 frame #12: 0x00000001005d3bb9 z3`___lldb_unnamed_symbol_1005d39ee + 459 frame #13: 0x00000001005d3035 z3`___lldb_unnamed_symbol_1005d2fa4 + 145 frame #14: 0x00000001005d2af1 z3`___lldb_unnamed_symbol_1005d2806 + 747 frame #15: 0x000000010053477b z3`___lldb_unnamed_symbol_100534638 + 323 frame #16: 0x000000010051d453 z3`___lldb_unnamed_symbol_10051cd84 + 1743 frame #17: 0x00000001005234ec z3`___lldb_unnamed_symbol_1005233d0 + 284 frame #18: 0x0000000100510968 z3`___lldb_unnamed_symbol_100510940 + 40 frame #19: 0x000000010000b241 z3`___lldb_unnamed_symbol_10000b110 + 305 frame #20: 0x000000010000ac4e z3`___lldb_unnamed_symbol_10000aa10 + 574 frame #21: 0x0000000100000f74 z3`___lldb_unnamed_symbol_100000f40 + 52 (lldb) quit Finding #24 was a crash: Based on the trace, these are all test inputs that lead to an EXC_BAD_ACCESS at location 343: ================ mut_04980_25978f85bf ================ (lldb) target create "/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3" Current executable set to '/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64). (lldb) settings set -- target.run-args "-smt2" "/Users/anon4review/smt_fuzz_v2/mutants/mut_04980_25978f85bf.smt2" (lldb) run warning: libobjc.A.dylib is being read from process memory. This indicates that LLDB could not read from the host's in-memory shared cache. This will likely reduce debugging performance. Process 8839 launched: '/Users/anon4review/Isabelle2025/Isabelle2025.app/contrib/z3-4.4.0pre-4/x86_64-darwin/z3' (x86_64) Process 8839 stopped * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x6001021b559f) frame #0: 0x000000010034cc2d z3`___lldb_unnamed_symbol_10034cad6 + 343 z3`___lldb_unnamed_symbol_10034cad6: -> 0x10034cc2d <+343>: movsbl (%rcx,%rdx), %ecx 0x10034cc31 <+347>: testl %ecx, %ecx 0x10034cc33 <+349>: je 0x10034cc52 ; <+380> 0x10034cc35 <+351>: cmpl $-0x1, %ecx Target 0: (z3) stopped. (lldb) bt * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x6001021b559f) * frame #0: 0x000000010034cc2d z3`___lldb_unnamed_symbol_10034cad6 + 343 frame #1: 0x000000010034e345 z3`___lldb_unnamed_symbol_10034da76 + 2255 frame #2: 0x0000000100332867 z3`___lldb_unnamed_symbol_1003327b6 + 177 frame #3: 0x0000000100339b95 z3`___lldb_unnamed_symbol_100339b08 + 141 frame #4: 0x00000001002de2a2 z3`___lldb_unnamed_symbol_1002dd64e + 3156 frame #5: 0x00000001006bd840 z3`___lldb_unnamed_symbol_1006bd7de + 98 frame #6: 0x00000001006bfca1 z3`___lldb_unnamed_symbol_1006bfae4 + 445 frame #7: 0x00000001006ba18d z3`___lldb_unnamed_symbol_1006b9f90 + 509 frame #8: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #9: 0x00000001006bfca1 z3`___lldb_unnamed_symbol_1006bfae4 + 445 frame #10: 0x00000001006ba2f8 z3`___lldb_unnamed_symbol_1006b9f90 + 872 frame #11: 0x00000001006b68a6 z3`___lldb_unnamed_symbol_1006b6860 + 70 frame #12: 0x00000001006b6af1 z3`___lldb_unnamed_symbol_1006b69d0 + 289 frame #13: 0x00000001005d3bb9 z3`___lldb_unnamed_symbol_1005d39ee + 459 frame #14: 0x00000001005d3035 z3`___lldb_unnamed_symbol_1005d2fa4 + 145 frame #15: 0x00000001005d2af1 z3`___lldb_unnamed_symbol_1005d2806 + 747 frame #16: 0x000000010053477b z3`___lldb_unnamed_symbol_100534638 + 323 frame #17: 0x000000010051d453 z3`___lldb_unnamed_symbol_10051cd84 + 1743 frame #18: 0x00000001005234ec z3`___lldb_unnamed_symbol_1005233d0 + 284 frame #19: 0x0000000100510968 z3`___lldb_unnamed_symbol_100510940 + 40 frame #20: 0x000000010000b241 z3`___lldb_unnamed_symbol_10000b110 + 305 frame #21: 0x000000010000ac4e z3`___lldb_unnamed_symbol_10000aa10 + 574 frame #22: 0x0000000100000f74 z3`___lldb_unnamed_symbol_100000f40 + 52 (lldb) quit =====