Environment leak in innermost visit

[jurgenvinju]

Describe the bug

This example code by Thomas van Binsbergen shows how a variable binding leaks from one case into the next during an innermost visit:

module Rewriting

import IO;
import Set;
import List;
import String;
import util::Maybe;

import lang::java::m3::Core;
import lang::java::m3::AST; 

void eval(loc file) {
  if (\compilationUnit(_,[\class(_,_,_,[\method(_,_,_,_,\block(stmts))])]) 
       := createAstFromFile(file, true)) {
    for (\expressionStatement(\methodCall(_,_,_,[expr])) <- rewrite(stmts)) {
      println(expr);
     }
   }
}

/*
&T rewrite(&T term) = innermost visit(term) {
       case \bracket(X0) => X0
       case \infix(\booleanLiteral(true),"&&",X1) => X1
       case \infix(X2:\booleanLiteral(false),"&&",_) => X2
       case \infix(X3,"&&",\booleanLiteral(true)) => X3
       case \infix(_,"&&",X4:\booleanLiteral(false)) => X4
       
       case \infix(X5:\booleanLiteral(true),"||",_) => X5
       case \infix(_,"||",X6:booleanLiteral(true)) => X6
       case \infix(\booleanLiteral(false),"||",X7) => X7
       case \infix(X8,"||",\booleanLiteral(false)) => X8
       
       case \conditional(\booleanLiteral(true),X9,_) => X9
       case \conditional(\booleanLiteral(false),_,X10) => X10
      };
*/

&T rewrite(&T term) = innermost visit(term) {
       case \bracket(X)                              => X
       case \infix(\booleanLiteral(true),"&&",X)     => X
       case \infix(X:\booleanLiteral(false),"&&",_)  => X
       case \infix(Expression Z,"&&",\booleanLiteral(true))     => Z // THIS RULE LEAKS Z
       case \infix(_,"&&",X:\booleanLiteral(false))  => X
       case \infix(X:\booleanLiteral(true),"||",_)   => X
       case \infix(_,"||", X1:booleanLiteral(true))   => X1 when bprintln("WHAT?? <Z>") // this rule observes Z
       case \infix(\booleanLiteral(false),"||",X)    => X
       case \infix(Expression Y,"||",\booleanLiteral(false))    => Y 
       case \conditional(\booleanLiteral(true),X,_)  => X
       case \conditional(\booleanLiteral(false),_,Y) => Y
      };

Example Java code to run this one:

class Booleans {
  
    public static void main(String[] args) {
      System.out.println(true && (false && true) && true && false);
      System.out.println(true && (false && true) ? (false || true) : false);
      System.out.println(false||true);
      System.out.println((true && (true && true)) ? (false || true) : false);
      System.out.println(true && (false && true) ? null : true ? null : null);
    }
}

The current output:

Reloading module Rewriting
WHAT?? booleanLiteral(false,src=|project://code-as-data-demo/src/Booleans.java|(185,5,<5,52>,<5,57>),typ=boolean())
WHAT?? booleanLiteral(false,src=|project://code-as-data-demo/src/Booleans.java|(235,5,<6,25>,<6,30>),typ=boolean())
WHAT?? booleanLiteral(false,src=|project://code-as-data-demo/src/Booleans.java|(302,5,<7,53>,<7,58>),typ=boolean())
booleanLiteral(false,src=|project://code-as-data-demo/src/Booleans.java|(99,5,<4,34>,<4,39>),typ=boolean())
booleanLiteral(false,src=|project://code-as-data-demo/src/Booleans.java|(202,5,<5,69>,<5,74>),typ=boolean())
booleanLiteral(true,src=|project://code-as-data-demo/src/Booleans.java|(242,4,<6,32>,<6,36>),typ=boolean())
booleanLiteral(true,src=|project://code-as-data-demo/src/Booleans.java|(311,4,<7,62>,<7,66>),typ=boolean())
null(src=|project://code-as-data-demo/src/Booleans.java|(392,4,<8,65>,<8,69>),typ=null())

This is a serious issue since the previous bindings will prevent succeeding matching because fresh variables
are not used and equality is checked against the previous binding.

The code is now running on the example because we renamed the variables to be unique. The original code used X for all open positions that needed to be bound.

[jurgenvinju]

rewriting to a solve with repeated bottom-up instead of innermost makes no difference. so it's not innermost that causes this. And this happens both with top-down and bottom-up strategies.

[jurgenvinju]

it seems the bug requires:

• visit statement
• two outermost constructors that are the same
• one is tried and matches a variable and binds it, but then fails
• the other is tried next and observes a leaked variable bind

[jurgenvinju]

The code that iterated over a list of alternative matches with the same outermost function symbol did not apply the environment hygiene rules that are normally used for backtracking over alternatives bindings (try {pushEnv; ...} finally {popEnv).

[ltbinsbe]

Many thanks for the thorough investigation!

[jurgenvinju]

thanks for the report @ltbinsbe; it's fixed now, but lacking some tests.