a3 reports 24 potential bugs in Python infrastructure

[lemmy]

https://pypi.org/project/a3-python/

(a3env) mkuppe@mkuppe-mlt a3 % a3 scan ValidationTestSuite --output-sarif a3-results.sarif

======================================================================
  A³ — Full Project Analysis
  Target: /Users/mkuppe/src/a3/ValidationTestSuite
======================================================================

======================================================================
STEP 1: BUILDING CALL GRAPH
======================================================================
  Functions: 1174  (0.4s)

======================================================================
STEP 2: COMPUTING CRASH SUMMARIES
======================================================================
  [1174/1174] 100%
  Summaries: 1174  (11.7s)

======================================================================
STEP 3: BUILDING CODE OBJECTS FOR DSE
======================================================================
  Code objects: 1174  (0.0s)

======================================================================
STEP 4: BUG TYPE COVERAGE
======================================================================
     411  NULL_PTR
      24  BOUNDS

======================================================================
STEP 5: BARRIER CERTIFICATE + DSE ANALYSIS
======================================================================
  Total bug instances:     804
  Fully guarded (guards):  714
  Unguarded:               90
  [90/90] done.

  Barrier results (0.2s):
    Proven FP:   66/90
    Remaining:   24

  Barrier contributions:
       50  post_condition
       12  refinement_type
        4  inductive_invariant

======================================================================
STEP 6: DSE RESULTS
======================================================================
  DSE analysed:        24
  DSE confirmed FP:    0
  DSE confirmed TP:    24

======================================================================
STEP 7: TRUE POSITIVE CANDIDATES
======================================================================
     15  BOUNDS
      9  NULL_PTR

  Production code bugs:  24
  Test-only code bugs:   0

  PRODUCTION BUGS TO INVESTIGATE:
    NULL_PTR        (1 unguarded) testgen.testcase.TlcModel.render
    BOUNDS          (3 unguarded) testgen.html_report.generate_index_workers_html
    BOUNDS          (1 unguarded) testgen.html_report.generate_failed_html
    BOUNDS          (1 unguarded) testgen.html_report.generate_feature_toc
    BOUNDS          (2 unguarded) testgen.html_report.generate_html_report
    NULL_PTR        (9 unguarded) testgen.feature.combine_tlc
    NULL_PTR        (9 unguarded) testgen.feature.combine_tlc_reduced
    NULL_PTR        (9 unguarded) testgen.feature.combine_apalache
    BOUNDS          (1 unguarded) testgen.type.UnionT.refine
    BOUNDS          (1 unguarded) testgen.type.UnionT.sample
    BOUNDS          (2 unguarded) testgen.type.RecordT.sample
    BOUNDS          (1 unguarded) testgen.feature.Except0F.case_rec
    BOUNDS          (1 unguarded) testgen.feature.Except2FunTupleF.arg_n
    NULL_PTR        (2 unguarded) testgen.feature.TupleF.case_expr
    NULL_PTR        (2 unguarded) testgen.feature.LambdaF.lam
    BOUNDS          (2 unguarded) testgen.feature.Cross2F.plug
    BOUNDS          (2 unguarded) testgen.feature.Cross3F.plug
    NULL_PTR        (7 unguarded) testgen.feature.TlcSingletonFunF.fun_replace
    BOUNDS          (1 unguarded) testgen.common.indent_multiline_but_first
    BOUNDS          (1 unguarded) testgen.common.indent_but_first_with
    BOUNDS          (1 unguarded) testgen.ast.IrContext.replace
    NULL_PTR        (1 unguarded) testgen.ast.type_ann
    NULL_PTR        (1 unguarded) testgen.ast.within_parens
    BOUNDS          (1 unguarded) testgen.ast.Instance.ir

  TRUE POSITIVES (DSE-confirmed reachable):
     ⚠️ BOUNDS in testgen.ast.Instance.ir
     ⚠️ BOUNDS in testgen.ast.IrContext.replace
     ⚠️ NULL_PTR in testgen.ast.type_ann
     ⚠️ NULL_PTR in testgen.ast.within_parens
     ⚠️ BOUNDS in testgen.common.indent_but_first_with
     ⚠️ BOUNDS in testgen.common.indent_multiline_but_first
     ⚠️ BOUNDS in testgen.feature.Cross2F.plug
     ⚠️ BOUNDS in testgen.feature.Cross3F.plug
     ⚠️ BOUNDS in testgen.feature.Except0F.case_rec
     ⚠️ BOUNDS in testgen.feature.Except2FunTupleF.arg_n
     ⚠️ NULL_PTR in testgen.feature.LambdaF.lam
     ⚠️ NULL_PTR in testgen.feature.TlcSingletonFunF.fun_replace
     ⚠️ NULL_PTR in testgen.feature.TupleF.case_expr
     ⚠️ NULL_PTR in testgen.feature.combine_apalache
     ⚠️ NULL_PTR in testgen.feature.combine_tlc
     ⚠️ NULL_PTR in testgen.feature.combine_tlc_reduced
     ⚠️ BOUNDS in testgen.html_report.generate_failed_html
     ⚠️ BOUNDS in testgen.html_report.generate_feature_toc
     ⚠️ BOUNDS in testgen.html_report.generate_html_report
     ⚠️ BOUNDS in testgen.html_report.generate_index_workers_html
     ⚠️ NULL_PTR in testgen.testcase.TlcModel.render
     ⚠️ BOUNDS in testgen.type.RecordT.sample
     ⚠️ BOUNDS in testgen.type.UnionT.refine
     ⚠️ BOUNDS in testgen.type.UnionT.sample

======================================================================
SUMMARY
======================================================================
  Functions analysed:    1174
  Total bug instances:   804
  Proven false positive: 780 (97.0%)
  DSE unreachable:       0
  Remaining candidates:  24
    Production:          24
    Test-only:           0
  DSE-confirmed TPs:     24

  Results saved to results/ValidationTestSuite_results.json
  SARIF written to a3-results.sarif  (24 findings)

a3-results.sarif.json