Tree filter missed pattern in 3.5.2-generated Java code

[brlarson]

Tree filters are powerful ANLTR magic, but maddening when they don't recognize the desired pattern. It's really hard to compose a bug report, because the (undesired) behavior is that nothing happens. I believe the problem is mis-calculation of follow sets encoded as BitSet. My application is a proof engine for transforming proof outlines (actions annotated with logical assertions) into complete, formal proofs that behavior meets specification.

Watching execution in the debugger for hours merely calculates "0" for a switch. Eventually, I made the tree filter just recognize the pattern I wanted, and then added in other patterns until the filter no longer fired. My work-around was to put definition_of_iff into its own grammar.

The specific situation is: (I'm having trouble getting literal text through Wiki, and I can't find means to upload source)

[serial 1374]: VI::Simple_App_Thread.imp
P [116] << PO_ALARM() or RM_ALARM() >>
S [117]->
Q [1] << true iff (PO_ALARM() or RM_ALARM()) >>
  What for: Distribute Carets:  (A^k op B^k or C^k) is (A op B op C)^k [serial 1368]

The tree filter is supposed to replace trees like LITERAL_iff | LITERAL_true --- X and with just tree X, as in

[serial 1375]: VI::Simple_App_Thread.imp
P [116] << PO_ALARM() or RM_ALARM() >>
S [117]->
Q [1] << (PO_ALARM() or RM_ALARM()) >>
  What for: Superfluisity of iff:  true iff a is a [serial 1374]

Each of my tree filters attempts to apply several proof rules. I put all of the "iff" rules into its own grammar for debugging. The following grammar fails when the line in "topdown" for definition_of_iff is uncommented:

topdown
  @before{substitutionMade = false;}
  : 
//  definition_of_iff | 
  true_iff
  | false_iff
  ;

definition_of_iff
    @after {reason=Reason.DEF_IFF;
      substitutionMade = true;
      }   //end  of @after
  :
  ^(LITERAL_iff a=. b=. {$a.equalsTree($b)}?)
    ->  LITERAL_true["true"]
  ;

true_iff
    @after {reason=Reason.TRUE_IFF_A;
      substitutionMade = true;
      }   //end  of @after
  :
  ^(i=LITERAL_iff LITERAL_true a=. 
  )
    ->  $a
  |
  ^(LITERAL_iff a=. LITERAL_true )
    ->  $a
  ;

false_iff
    @after {reason=Reason.TRUE_IFF_A;
      substitutionMade = true;
      }   //end  of @after
  :
  ^(LITERAL_iff LITERAL_false a=. )
    ->  ^(LITERAL_not["not"] {Algebra.addParenthesesIfNeeded($a)})
  |
  ^(LITERAL_iff a=. LITERAL_false )
    ->  ^(LITERAL_not["not"] {Algebra.addParenthesesIfNeeded($a)})
  ;

T: I will gladly upload the grammar that produces AST from text, and ANTLR source or generated Java code both with and without the commented line if it will help.

--Brian

[parrt]

Hi Brian. Sorry for the hassles. Adding to the list...

[brlarson]

T:I appreciate your apology, but it's not necessary.ANTLR magic is powerful, but when tree filters don't fire, it can be hard to figure out what to do.In this case, I worked around the issue, but narrowed-down the difference between working and not to commenting a single line.  Hopefully, this will let an experienced eye discern the difference.As a systems engineer at my previous employer, I was able to elicit unintended behavior in a Class III medical device.  The developers much appreciated my detailed, specific description how to elicit the anomaly.--Brian

-------- Original Message -------- Subject: Re: [antlr3] Tree filter missed pattern in 3.5.2-generated Java code (#159) From: Terence Parr notifications@github.com Date: Mon, July 21, 2014 11:10 am To: antlr/antlr3 antlr3@noreply.github.com Cc: brlarson brl@multitude.netHi Brian. Sorry for the hassles. Adding to the list... —Reply to this email directly or view it on GitHub.

[brlarson]

For those who may have similar problems, Workaround: split-off the tree filter productions that aren't firing but (you think) should. I had a problem with a tree filter for associativity: A and (B and C) => A and B and C Splitting it off from the other things done in that tree filter, works fine. Now that I know the workaround, it took only 15 minutes to do.