Inferring invariants with hierarchical dataflow

[michaelmior]

I'm working on a Daikon frontend and I'd like to be able to infer invariants spanning multiple program points with a parent/child relationship.

Version info (Daikon built from source)

$ java -version
openjdk version "11.0.20" 2023-07-18
OpenJDK Runtime Environment (build 11.0.20+8-post-Ubuntu-1ubuntu120.04)
OpenJDK 64-Bit Server VM (build 11.0.20+8-post-Ubuntu-1ubuntu120.04, mixed mode, sharing)
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.6 LTS
Release:        20.04
Codename:       focal

Here's an example without hierarchy that does what I expect. When I run this example, I get the invariant __ROOT__.baz == __ROOT__.foo.bar.

decl-version 2.0
ppt program.point:::POINT
ppt-type point
variable __ROOT__
  var-kind variable
  comparability 3
  dec-type Map
  rep-type hashcode
variable __ROOT__.baz
  var-kind field baz
  enclosing-var __ROOT__
  comparability 0
  dec-type java.lang.String
  rep-type java.lang.String
variable __ROOT__.foo
  var-kind field foo
  enclosing-var __ROOT__
  comparability 3
  dec-type Map
  rep-type hashcode
variable __ROOT__.foo.bar
  var-kind field bar
  enclosing-var __ROOT__.foo
  comparability 0
  dec-type java.lang.String
  rep-type java.lang.String

program.point:::POINT
__ROOT__
nonsensical
1
__ROOT__.baz
"baz"
1
__ROOT__.foo
nonsensical
1
__ROOT__.foo.bar
"baz"
1

However, I'd like to restructure this output so that instead of nesting the variables multiple levels, the associated program points are nested.

decl-version 2.0
ppt program.__ROOT__:::POINT
ppt-type point
variable __ROOT__
  var-kind variable
  comparability 3
  dec-type Map
  rep-type hashcode
variable __ROOT__.baz
  var-kind field baz
  enclosing-var __ROOT__
  comparability 0
  dec-type java.lang.String
  rep-type java.lang.String
variable __ROOT__.foo
  var-kind field foo
  enclosing-var __ROOT__
  comparability 3
  dec-type Map
  rep-type hashcode

program.__ROOT__:::POINT
__ROOT__
nonsensical
1
__ROOT__.baz
"baz"
1
__ROOT__.foo
nonsensical
1

ppt program.__ROOT__.foo:::POINT
ppt-type point
parent parent program.__ROOT__:::POINT 1
variable __ROOT__.foo.bar
  var-kind variable
  comparability 0
  dec-type java.lang.String
  rep-type java.lang.String

program.__ROOT__.foo:::POINT
__ROOT__.foo.bar
"baz"
1

Since the program point program.__ROOT__.foo:::POINT has a parent of parent program.__ROOT__:::POINT, I would expect a similar invariant to be reported across these program points, but it is not. I'm basing this on the following quote from the manual:

Suppose there are two program points X and its parent Y. Then every sample seen at X is also seen at Y, and every invariant that is true at Y is also true at X.

However, looking at the StackAr example, it seems that perhaps the trace entries need to be present at both program points for this to work? Some clarification here would be helpful. I'm trying to take advantage of incremental generation so I don't have to write out all the nested data structures at once. This is especially important when the nesting goes more than two deep since it would require repetition at all levels.