Repository navigation
Conversation
Daikon treats arbitrarily named program points such as :::POINT (used by convertcsv.pl) as leaves of the dataflow hierarchy, but the splitter hierarchy code treated only numbered exit points as leaves. As a result, splitting at such a program point produced no samples and no implications. Add PptTopLevel.is_dataflow_leaf() and use it consistently.
FileIO.process_sample and MergeInvariants now use is_dataflow_leaf() rather than their own leaf tests. is_dataflow_leaf() follows the declared ppt type when there is one, treats :::GLOBAL as a non-leaf, and is the basis of the final assertion in init_hierarchy_new. The new SplitPoint test splits a :::POINT program point.
… SplitPoint test * FileIO reads a "ppt-type exit" declaration of a numbered exit (such as foo:::EXIT22) as SUBEXIT, so is_subexit, is_combined_exit, and is_dataflow_leaf agree about it. is_dataflow_leaf no longer special-cases it. * process_sample again rejects samples at any combined-exit name. * init_hierarchy (old decls) also creates equality views for childless non-leaves such as :::GLOBAL; the assertion there excludes combined exits. * MergeInvariants builds the hierarchy from a decls file the same way Daikon does. * SplitPoint test data now yields implications relating x and y.
…e hierarchy dispatch Normalize a numbered exit typed EXIT or POINT to SUBEXIT, and a non-combined-exit name typed EXIT to POINT, in the PptTopLevel constructor and readObject, so that deserialized ppts also get consistent predicates. Remove MergeInvariants's assertion that non-leaves have children, allow childless combined exits, and drop splitters of childless non-leaves. Add PptRelation.init_hierarchy_for_decl_format.
…e normalization, merge-link cleanup, AnnotateNullable, shared helpers - MergeInvariants: set up equality views on childless non-leaves when the merge template comes from .inv files; remove only MERGE_CHILD relations in the final cleanup. - PptTopLevel.normalize_type: require EXIT followed by digits for SUBEXIT; a POINT- or EXIT-typed foo:::EXIT is a combined exit. - Daikon.create_combined_exits: do not replace a declared combined exit. - AnnotateNullable: accept a numbered exit with no combined-exit parent as a method's exit. - Share conditional-connection and hierarchy-finishing code between init_hierarchy and init_hierarchy_new; share equality-view creation.
… combined exits * PptTopLevel.normalize_type also derives ENTER, OBJECT, and CLASS from the name, and applies to ppts with no declared type, so the is_* predicates no longer need name-based fallbacks. PptConditional takes its parent's type. * Move the numbered-exit name test to PptName.isExitWithLineNumber. * AnnotateNullable processes a method once even when an .inv file lacks its combined exit, combining the annotations of all its numbered exits. * Reword the FileIO comment about samples at combined exit points. * init_hierarchy_new again includes conditional relations in its debug output.
# Conflicts: # tests/daikon-tests/Makefile
PptTopLevel.normalize_type derives the type from the name when the declaration gives no type, or gives the type exit or point, so the is_enter, is_exit, is_combined_exit, is_subexit, is_object, and is_class predicates no longer need name-based fallbacks. A numbered exit declared with type exit is a subexit. * Daikon.create_combined_exits does not replace a declared combined exit. * AnnotateNullable handles an .inv file that lacks a combined exit. * PptConditional takes its parent's type. Split from codespecs#858.
PptRelation.init_hierarchy (old declaration format) and init_hierarchy_new now share connect_conditionals and finish_hierarchy, so the old format also creates equality views for childless non-leaves. A non-leaf with no children has its splitters removed. New methods PptRelation.init_hierarchy_for_decl_format and PptTopLevel.create_equality_view replace duplicated code. Split from codespecs#858.
…ow-leaf # Conflicts: # java/daikon/PptRelation.java # java/daikon/PptTopLevel.java
* AnnotateNullable no longer handles .inv files that lack combined exits; it processes only combined exits and skips all other children. * PptTopLevel.readObject does not re-derive the type, which was wrong for a PptConditional. * MergeInvariants cleans the merge template on the decls path too, so leaves that get merge children have no equality view. * PptRelation.setup_childless_nonleaves skips leaves instead of asserting that there are none. * Suppress a purity warning in PptName.isExitWithLineNumber.
PptRelation.init_hierarchy (old declaration format) and init_hierarchy_new now share connect_conditionals and finish_hierarchy, so the old format also creates equality views for childless non-leaves. A non-leaf with no children has its splitters removed. New methods PptRelation.init_hierarchy_for_decl_format and PptTopLevel.create_equality_view replace duplicated code. Split from codespecs#858.
This was referenced Oct 6, 2026
|
Warning Review limit reached
This review includes 18 billable files and costs up to $4.50. Or wait 42 minutes for your next included review. View limit detailsLimit details: You’ve used all 2 included reviews currently available. Review configuration: ⚙️ Run configuration
⛔ Files ignored due to path filters (1)
📒 Files selected for processing (18)
Comment |
… ppt types * Add THROWS and GLOBAL ppt types, assigned from the name, so that is_dataflow_leaf depends only on the type. * Reject a declared ppt-type whose name does not have the required form, and reject a leaf that is declared as a parent. * MergeInvariants: clean only the ppts that get merge children, and give an equality view to a leaf that no input map contains. * Document the throws and global ppt types.
* A missing ppt-type is derived from the name; an explicit "point" is kept. * A ppt declared exit or subexit is a combined or numbered exit according to its name; any other declared type must conform to the name, or reading the declaration fails with an error. * Remove backward-compatibility code for older .inv files. * Daikon.create_combined_exits again replaces a declared combined exit. * Remove PptName.isExitWithLineNumber; use isNumberedExitPoint.
New method PptTopLevel.is_dataflow_leaf, also used by Daikon.setupEquality, identifies the ppts that get their invariants from samples. setup_childless_nonleaves now ignores leaves, and finish_hierarchy removes the splitters of a childless ppt only if it is not a leaf. This avoids assertion failures and lost conditional invariants for old-format CLASS ppts, :::POINT leaves with splitters, leaves when the equality optimization is disabled, and the not-yet-connected leaves in MergeInvariants. MergeInvariants now uses init_hierarchy_for_decl_format.
Convert every version 1 .decls and .dtrace test input to the version 2 format, in preparation for dropping support for version 1 files. The converted inputs produce the same output, with two exceptions: * pine_mdiep loses one invariant over a two-dimensional variable, which version 2 cannot represent. * Nine more splitters compile, because the version 2 declarations let the splitter generator find array variables. Also delete test inputs that no test uses, and delete tests/diff-tests/StackAr, which has been excluded from testing (and broken) since 2010.
Daikon no longer reads version 1 .decls and .dtrace files, and reports an error when it encounters one. Remove FileIO.new_decl_format and all code that was used only for version 1 files, including the name-based program point hierarchy (MergeInvariants now uses the declaration-based one) and the remove_post_vars configuration option. Remove the Perl front end (dfepl), which produced version 1 files. Port convertcsv.pl and the cluster analysis scripts to version 2, and remove scripts that processed only version 1 files.
…t-support-old-format
…are-hierarchy # Conflicts: # java/daikon/Daikon.java # java/daikon/PptRelation.java
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
….pl unescaping, remove version 1 leftovers * developer.texinfo: release snippets no longer test for the deleted front-end/ directory; example .decls is now in version 2 format; clarify that a file with no decl-version record is read as version 2. * CHANGELOG.md: accurately describe what identifies a version 1 file. * convertcsv.pl: unescapeDecl now handles \n and \r like FileIO.unescape_decl. * Remove lwpp-init.pl (only used with the removed lwpp.pl) and unused version 1 Kvasir goal files for SimpleDisambigStructTest. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…trace, cluster scripts - ppt_perc: never exclude GLOBAL/OBJECT/CLASS ppts (they are parents of included ppts); read ppt names via FileIO.declared_ppt_name, which applies user_mod_ppt_name. - MergeInvariants with a .decls file: create combined exits before init_hierarchy, and clean the ppt map for merging on both paths. - SplitDtrace: handle traces without declarations; pass header records through. - decls-add-cluster.pl: link the cluster variable to its parents. - dtrace-count.pl, dtrace-indent.pl: match declaration records exactly. - Remove simplify_expression/simplify_variable_names and the unused return value of read_decl_version. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…tDtrace comments - FileIO.is_parent_only_ppt_name: use PptName rather than a substring match on "GLOBAL". - read_ppt_decl: reuse declared_ppt_name to parse the ppt name. - SplitDtrace: use new FileIO.is_header_record, which also recognizes comment records. - MergeInvariants: clean ppts for merge only when reading .inv files. - developer manual: there is no longer a Perl front end. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…arability, truncated records * dtrace-diff.pl reports a difference when two declarations of a program point have different variables, and reuses read_ppt_decls. * sort-dtrace.pl writes the input file's line endings. * decls2comp.py recognizes arrays by their rep-type. * dtrace-count.pl honors a "// EOF" line among a record's leading comments. * util_daikon.pm and dtrace-diff.pl use English without match variables.
…file in dtrace-diff-fast.pl, dead code
… for variables without comparability
Member
Author
|
@coderabbitai review |
|
…-front-end # Conflicts: # doc/CHANGELOG.md
…ion-1-scripts # Conflicts: # doc/CHANGELOG.md
…test-inputs # Conflicts: # tests/diff-tests/Makefile.common # tests/diff-tests/StackAr/Makefile # tests/diff-tests/StackAr/StackAr-u.txt.goal
# Conflicts: # doc/CHANGELOG.md
# Conflicts: # doc/CHANGELOG.md
# Conflicts: # doc/CHANGELOG.md
# Conflicts: # java/daikon/PptTopLevel.java
…-type-from-name
(cherry picked from commit b694105)
(cherry picked from commit b694105)
(cherry picked from commit b694105)
…rmat # Conflicts: # java/daikon/SplitDtrace.java
# Conflicts: # doc/CHANGELOG.md # java/daikon/SplitDtrace.java
# Conflicts: # doc/CHANGELOG.md # java/daikon/SplitDtrace.java
…are-hierarchy # Conflicts: # doc/CHANGELOG.md
# Conflicts: # doc/CHANGELOG.md # java/daikon/PptTopLevel.java
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is one of three PRs split from #858, which it replaces, as does #873. Merge #876 and #875 first, and therefore #880, on which #875 depends. This PR includes the changes of #876 and #875, and therefore of #880.
PptTopLevel.normalize_type(from #876) checks a declared type against the program point's name, and it also handles the:::THROWSand:::GLOBALtypes that this PR adds.PptRelationassumed that numbered exits are the only leaves of the dataflow hierarchy. At any other leaf with splitters (such as a:::POINTprogram point, as produced byconvertcsv.pl), the samples went only to the conditional program points, so the program point had no samples and no implications.The new
PptTopLevel.is_dataflow_leaf()is the single definition of a leaf: the numbered exits and the general program points, except:::THROWSand:::GLOBAL.PptRelation,FileIO.process_sample,Daikon.setupEquality, andMergeInvariantsall use it.Other changes:
:::GLOBALis no longer a leaf, so when it has no children it gets its equality view fromsetup_childless_nonleaves.MergeInvariantsbuilds the hierarchy from a decls file the same way Daikon does, and at the end removes only the merge relations it added.The new
SplitPointtest splits a:::POINTprogram point.runcluster.pl(#856) depends on this change; its tests are intests/script-tests/runcluster/.