<commit_before>// Copyright (c) 2012, <NAME> (<EMAIL>)
// All rights reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are met:
//    * Redistributions of source code must retain the above copyright
//      notice, this list of conditions and the following disclaimer.
//    * Redistributions in binary form must reproduce the above copyright
//      notice, this list of conditions and the following disclaimer in the
//      documentation and/or other materials provided with the distribution.
//    * Neither the name of the <organization> nor the
//      names of its contributors may be used to endorse or promote products
//      derived from this software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
// ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
// WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
// DISCLAIMED. IN NO EVENT SHALL DAVID J. PEARCE BE LIABLE FOR ANY
// DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
// (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
// LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
// ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

package wyil.builders;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.BitSet;
import java.util.Collections;
import java.util.List;

import static wybs.lang.SyntaxError.internalFailure;
import wycs.core.Value;
import wycs.solver.Solver;
import wycs.syntax.Expr;
import static wycs.solver.Solver.*;

import wyautl.core.Automaton;
import wyautl.io.PrettyAutomataWriter;
import wybs.lang.Attribute;
import wybs.lang.SyntaxError;
import wybs.lang.SyntaxError.InternalFailure;
import wybs.util.Pair;
import wyil.lang.Block;
import wyil.lang.Code;
import wyil.lang.Constant;
import wyil.lang.Type;
import wyil.lang.WyilFile;

/**
 * <p>
 * Represents a path through the body of a Wyil method or function. A branch
 * accumulates the constraints known to hold through that particular execution
 * path. These constraints can then be checked for satisfiability at various
 * critical points in the function.
 * </p>
 * <p>
 * When verifying a given function or method, the verifier starts with a single
 * branch at the beginning of the method. When split points in the control-flow
 * graph are encountered, branches are accordingly forked off to represent the
 * alternate control-flow path. At control-flow meet points, branches may also
 * be joined back together (although this is not always strictly necessary). A
 * diagrammatic view might be:
 * </p>
 * 
 * <pre>
 *  entry
 *   ||
 *   ||
 *   ##\
 *   ||\\
 *   || \\
 *   || || 
 *   || ##\
 *   || ||\\
 *   ||//  \\
 *   ##/   ||
 *   ||    ||
 *   \/    \/
 *   B1    B3
 * </pre>
 * <p>
 * In the above example, we initially start with one branch <code>B1</code>.
 * This is then forked to give branch <code>B2</code> which, in turn, is forked
 * again to give <code>B3</code>. Subsequently, branch <code>B2</code> is joined
 * back with <code>B1</code>. However, <code>B3</code> is never joined and
 * terminates separately.
 * </p>
 * <p>
 * Every branch (except the first) has a <i>parent</i> branch which it was
 * forked from. Given any two branches there is always a <i>Least Common
 * Ancestor (LCA)</i> --- that is, the latest point which is common to both
 * branches. Finding the LCA can be useful, for example, to identify constraints
 * common to both branches.
 * </p>
 * 
 * @author <NAME>
 * 
 */
public class VcBranch {
	/**
	 * The parent branch which this branch was forked from, or <code>null</code>
	 * if it is the initial "master" branch for the function or method in
	 * question.
	 */
	private final VcBranch parent;

	/**
	 * Maintains the current assignment of variables to expressions.
	 */
	private final Expr[] environment;

	/**
	 * Maintains the current assignment of variables to their types.
	 */
	private final Type[] types;
	
	/**
	 * The stack of currently active scopes (e.g. for-loop). When the branch
	 * exits a scope, an exit scope event is generated in order that additional
	 * effects make be applied.
	 */
	private final ArrayList<Scope> scopes;
	
	/**
	 * The block of Wyil bytecode instructions which this branch is traversing
	 * (note: <code>parent == null || block == parent.block</code> must hold).
	 */
	private final Block block;

	/**
	 * The origin determines the bytecode offset in block where this branch was
	 * forked from. For the master branch, this will be <code>0</code>.
	 */
	private final int origin;

	/**
	 * The bytecode index into the above block that this branch is currently at.
	 */
	private int pc;

	/**
	 * Construct the master verification branch for a given code block. The
	 * master for a block has an origin <code>0</code> and an (initial) PC of
	 * <code>0</code> (i.e. the branch begins at the entry of the block).
	 * 
	 * @param automaton
	 *            --- the automaton to which constraints generated for this
	 *            block are stored.
	 * @param block
	 *            --- the block of code on which this branch is operating.
	 */
	public VcBranch(Block block) {
		this.parent = null;
		this.environment = new Expr[block.numSlots()];
		this.types = new Type[block.numSlots()];
		this.scopes = new ArrayList<Scope>();
		this.block = block;
		this.origin = 0;
		this.pc = 0;
		scopes.add(new Scope(block.size(), Collections.EMPTY_LIST));
	}
	
	/**
	 * Construct the master verification branch for a given code block. The
	 * master for a block has an origin <code>0</code> and an (initial) PC of
	 * <code>0</code> (i.e. the branch begins at the entry of the block).
	 * 
	 * @param automaton
	 *            --- the automaton to which constraints generated for this
	 *            block are stored.
	 * @param block
	 *            --- the block of code on which this branch is operating.
	 */
	public VcBranch(WyilFile.MethodDeclaration decl, Block block) {
		this.parent = null;				
		this.environment = new Expr[block.numSlots()];
		this.types = new Type[block.numSlots()];
		this.scopes = new ArrayList<Scope>();
		this.block = block;
		this.origin = 0;
		this.pc = 0;
		scopes.add(new EntryScope(decl, block.size(), Collections.EMPTY_LIST));
		ArrayList<Type> paramTypes = decl.type().params();
	}

	/**
	 * Private constructor used for forking a child-branch from a parent branch.
	 * 
	 * @param parent
	 *            --- parent branch being forked from.
	 */
	private VcBranch(VcBranch parent) {
		this.parent = parent;
		this.environment = parent.environment.clone();
		this.types = Arrays
				.copyOf(parent.types, environment.length);
		this.scopes = new ArrayList<Scope>();
		this.block = parent.block;
		this.origin = parent.pc;
		this.pc = parent.pc;
		for(Scope scope : parent.scopes) {
			this.scopes.add(scope.clone());
		}
	}

	/**
	 * Return the current Program Counter (PC) value for this branch. This must
	 * be a valid index into the code block this branch is operating over.
	 * 
	 * @return
	 */
	public int pc() {
		return pc;
	}

	/**
	 * Get the block entry at the current PC position.
	 * 
	 * @return
	 */
	public Block.Entry entry() {
		return block.get(pc);
	}

	/**
	 * Get the constraint variable which corresponds to the given Wyil bytecode
	 * register at this point on this branch.
	 * 
	 * @param register
	 * @return
	 */
	public Expr read(int register) {		
		return environment[register];
	}

	/**
	 * Get the type of a given register at this point in the block.
	 * 
	 * @return
	 */
	public Type typeOf(String var) {
		// FIXME: this is such an *horrific* hack, I can't believe I'm doing it.
		// But, it does work most of the time:(
		int register = Integer.parseInt(var.substring(1));		
		return types[register];
	}
	
	/**
	 * Get the type of a given register at this point in the block.
	 * 
	 * @return
	 */
	public Type typeOf(int register) {
		return types[register];
	}
	
	/**
	 * Assign a given expression stored in the automaton to a given Wyil
	 * bytecode register.
	 * 
	 * @param register
	 * @param expr
	 */
	public void write(int register, Expr expr, Type type) {
		environment[register] = expr;
		types[register] = type;
	}
	
	public int nScopes() {
		return scopes.size();
	}
	
	public Scope scope(int i) {
		return scopes.get(i);
	}
	
	/**
	 * Get the first scope matching a given scope kind.
	 * 
	 * @param clazz
	 * @return
	 */
	public <T extends Scope> T topScope(Class<T> clazz) {
		for(int i=scopes.size();i>0;) {
			i=i-1;
			Scope scope = scopes.get(i);
			if(clazz.isInstance(scope)) {
				return (T) scope;
			}
		}
		return null;
	}

	/**
	 * Terminate the current flow for a given register and begin a new one. In
	 * terms of static-single assignment, this means simply change the index of
	 * the register in question.
	 * 
	 * @param register
	 */
	public Expr.Variable invalidate(int register, Type type) {
		// to invalidate a variable, we assign it a "skolem" constant. That is,
		// a fresh variable which has been previously encountered in the
		// branch.
		Expr.Variable var = Expr.Variable("r" + Integer.toString(register));
		environment[register] = var;
		types[register] = type;
		return var;
	}
	
	/**
	 * Invalidate all registers from <code>start</code> upto (but not including)
	 * <code>end</code>.
	 * 
	 * @param start
	 *            --- first register to invalidate.
	 * @param end
	 *            --- first register not to invalidate.
	 */
	public void invalidate(int start, int end, Type type) {
		for (int i = start; i != end; ++i) {
			invalidate(i,type);
		}
	}
	
	/**
	 * Return a reference into the automaton which represents all of the
	 * constraints that hold at this position in the branch.
	 * 
	 * @return
	 */
	public Expr constraints() {		
		ArrayList<Expr> constraints = new ArrayList<Expr>();
		for (int i = 0; i != scopes.size(); ++i) {
			Scope scope = scopes.get(i);
			constraints.addAll(scope.constraints);
		}
		return And(constraints);		
	}

	/**
	 * Add a given constraint to the list of constraints which are assumed to
	 * hold at this point.
	 * 
	 * @param constraint
	 */
	public void add(Expr constraint) {
		topScope().constraints.add(constraint);
	}
	
	/**
	 * Add a given list of constraints to the list of constraints which are assumed to
	 * hold at this point.
	 * 
	 * @param constraints
	 */
	public void addAll(List<Expr> constraints) {
		topScope().constraints.addAll(constraints);
	}

	/**
	 * Transform this branch into a list of constraints representing that which
	 * is known to hold at the end of the branch. The generated constraint will
	 * only be in terms of the given parameters and return value for the block.
	 * 
	 * @param transformer
	 *            --- responsible for transformining individual bytecodes into
	 *            constraints capturing their semantics.
	 * @return
	 */
	public Expr transform(VcTransformer transformer) {		
		ArrayList<VcBranch> children = new ArrayList<VcBranch>();
		int blockSize = block.size();
		while (pc < blockSize) {
									
			// first, check whether we're departing a scope or not.
			int top = scopes.size() - 1;
			while (top >= 0 && scopes.get(top).end < pc) {
				// yes, we're leaving a scope ... so notify transformer.
				Scope topScope = scopes.get(top);
				scopes.remove(top);
				dispatchExit(topScope, transformer);
				top = top - 1;
			}			
			
			// second, continue to transform the given bytecode
			Block.Entry entry = block.get(pc);
			Code code = entry.code;
			if(code instanceof Code.Goto) {				
				goTo(((Code.Goto) code).target);
			} else if(code instanceof Code.If) {
				Code.If ifc = (Code.If) code;
				VcBranch trueBranch = fork();	
				transformer.transform(ifc,this,trueBranch);
				trueBranch.goTo(ifc.target);
				children.add(trueBranch);
			} else if(code instanceof Code.Switch) {
				Code.Switch sw = (Code.Switch) code;
				VcBranch[] cases = new VcBranch[sw.branches.size()];
				for(int i=0;i!=cases.length;++i) {					
					cases[i] = fork();
					children.add(cases[i]);
				}				
				transformer.transform(sw,this,cases);
				for(int i=0;i!=cases.length;++i) {					
					cases[i].goTo(sw.branches.get(i).second());					
				}				
			} else if(code instanceof Code.IfIs) {
				Code.IfIs ifs = (Code.IfIs) code;
				Type type = typeOf(ifs.operand);				
				// First, determine the true test
				Type trueType = Type.intersect(type,ifs.rightOperand);		
				Type falseType = Type.intersect(type,Type.Negation(ifs.rightOperand));
				
				if(trueType.equals(Type.T_VOID)) {
					// This indicate that the true branch is unreachable and
					// should not be explored. Observe that this does not mean
					// the true branch is dead-code. Rather, since we're
					// preforming a path-sensitive traversal it means we've
					// uncovered an unreachable path. In this case, this branch
					// remains as the false branch.<commit_msg>WYIL: minor additional fix for #222.  Now it's passing all tests!!<commit_after>// Copyright (c) 2012, <NAME> (<EMAIL>)
// All rights reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are met:
//    * Redistributions of source code must retain the above copyright
//      notice, this list of conditions and the following disclaimer.
//    * Redistributions in binary form must reproduce the above copyright
//      notice, this list of conditions and the following disclaimer in the
//      documentation and/or other materials provided with the distribution.
//    * Neither the name of the <organization> nor the
//      names of its contributors may be used to endorse or promote products
//      derived from this software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
// ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
// WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
// DISCLAIMED. IN NO EVENT SHALL DAVID J. PEARCE BE LIABLE FOR ANY
// DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
// (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
// LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
// ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

package wyil.builders;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.BitSet;
import java.util.Collections;
import java.util.List;

import static wybs.lang.SyntaxError.internalFailure;
import wycs.core.Value;
import wycs.solver.Solver;
import wycs.syntax.Expr;
import static wycs.solver.Solver.*;

import wyautl.core.Automaton;
import wyautl.io.PrettyAutomataWriter;
import wybs.lang.Attribute;
import wybs.lang.SyntaxError;
import wybs.lang.SyntaxError.InternalFailure;
import wybs.util.Pair;
import wyil.lang.Block;
import wyil.lang.Code;
import wyil.lang.Constant;
import wyil.lang.Type;
import wyil.lang.WyilFile;

/**
 * <p>
 * Represents a path through the body of a Wyil method or function. A branch
 * accumulates the constraints known to hold through that particular execution
 * path. These constraints can then be checked for satisfiability at various
 * critical points in the function.
 * </p>
 * <p>
 * When verifying a given function or method, the verifier starts with a single
 * branch at the beginning of the method. When split points in the control-flow
 * graph are encountered, branches are accordingly forked off to represent the
 * alternate control-flow path. At control-flow meet points, branches may also
 * be joined back together (although this is not always strictly necessary). A
 * diagrammatic view might be:
 * </p>
 * 
 * <pre>
 *  entry
 *   ||
 *   ||
 *   ##\
 *   ||\\
 *   || \\
 *   || || 
 *   || ##\
 *   || ||\\
 *   ||//  \\
 *   ##/   ||
 *   ||    ||
 *   \/    \/
 *   B1    B3
 * </pre>
 * <p>
 * In the above example, we initially start with one branch <code>B1</code>.
 * This is then forked to give branch <code>B2</code> which, in turn, is forked
 * again to give <code>B3</code>. Subsequently, branch <code>B2</code> is joined
 * back with <code>B1</code>. However, <code>B3</code> is never joined and
 * terminates separately.
 * </p>
 * <p>
 * Every branch (except the first) has a <i>parent</i> branch which it was
 * forked from. Given any two branches there is always a <i>Least Common
 * Ancestor (LCA)</i> --- that is, the latest point which is common to both
 * branches. Finding the LCA can be useful, for example, to identify constraints
 * common to both branches.
 * </p>
 * 
 * @author <NAME>
 * 
 */
public class VcBranch {
	/**
	 * The parent branch which this branch was forked from, or <code>null</code>
	 * if it is the initial "master" branch for the function or method in
	 * question.
	 */
	private final VcBranch parent;

	/**
	 * Maintains the current assignment of variables to expressions.
	 */
	private final Expr[] environment;

	/**
	 * Maintains the current assignment of variables to their types.
	 */
	private final Type[] types;
	
	/**
	 * The stack of currently active scopes (e.g. for-loop). When the branch
	 * exits a scope, an exit scope event is generated in order that additional
	 * effects make be applied.
	 */
	private final ArrayList<Scope> scopes;
	
	/**
	 * The block of Wyil bytecode instructions which this branch is traversing
	 * (note: <code>parent == null || block == parent.block</code> must hold).
	 */
	private final Block block;

	/**
	 * The origin determines the bytecode offset in block where this branch was
	 * forked from. For the master branch, this will be <code>0</code>.
	 */
	private final int origin;

	/**
	 * The bytecode index into the above block that this branch is currently at.
	 */
	private int pc;

	/**
	 * Construct the master verification branch for a given code block. The
	 * master for a block has an origin <code>0</code> and an (initial) PC of
	 * <code>0</code> (i.e. the branch begins at the entry of the block).
	 * 
	 * @param automaton
	 *            --- the automaton to which constraints generated for this
	 *            block are stored.
	 * @param block
	 *            --- the block of code on which this branch is operating.
	 */
	public VcBranch(Block block) {
		this.parent = null;
		this.environment = new Expr[block.numSlots()];
		this.types = new Type[block.numSlots()];
		this.scopes = new ArrayList<Scope>();
		this.block = block;
		this.origin = 0;
		this.pc = 0;
		scopes.add(new Scope(block.size(), Collections.EMPTY_LIST));
	}
	
	/**
	 * Construct the master verification branch for a given code block. The
	 * master for a block has an origin <code>0</code> and an (initial) PC of
	 * <code>0</code> (i.e. the branch begins at the entry of the block).
	 * 
	 * @param automaton
	 *            --- the automaton to which constraints generated for this
	 *            block are stored.
	 * @param block
	 *            --- the block of code on which this branch is operating.
	 */
	public VcBranch(WyilFile.MethodDeclaration decl, Block block) {
		this.parent = null;				
		this.environment = new Expr[block.numSlots()];
		this.types = new Type[block.numSlots()];
		this.scopes = new ArrayList<Scope>();
		this.block = block;
		this.origin = 0;
		this.pc = 0;
		scopes.add(new EntryScope(decl, block.size(), Collections.EMPTY_LIST));
		ArrayList<Type> paramTypes = decl.type().params();
	}

	/**
	 * Private constructor used for forking a child-branch from a parent branch.
	 * 
	 * @param parent
	 *            --- parent branch being forked from.
	 */
	private VcBranch(VcBranch parent) {
		this.parent = parent;
		this.environment = parent.environment.clone();
		this.types = Arrays
				.copyOf(parent.types, environment.length);
		this.scopes = new ArrayList<Scope>();
		this.block = parent.block;
		this.origin = parent.pc;
		this.pc = parent.pc;
		for(Scope scope : parent.scopes) {
			this.scopes.add(scope.clone());
		}
	}

	/**
	 * Return the current Program Counter (PC) value for this branch. This must
	 * be a valid index into the code block this branch is operating over.
	 * 
	 * @return
	 */
	public int pc() {
		return pc;
	}

	/**
	 * Get the block entry at the current PC position.
	 * 
	 * @return
	 */
	public Block.Entry entry() {
		return block.get(pc);
	}

	/**
	 * Get the constraint variable which corresponds to the given Wyil bytecode
	 * register at this point on this branch.
	 * 
	 * @param register
	 * @return
	 */
	public Expr read(int register) {		
		return environment[register];
	}

	/**
	 * Get the type of a given register at this point in the block.
	 * 
	 * @return
	 */
	public Type typeOf(String var) {
		// FIXME: this is such an *horrific* hack, I can't believe I'm doing it.
		// But, it does work most of the time:(
		int register = Integer.parseInt(var.substring(1));		
		return types[register];
	}
	
	/**
	 * Get the type of a given register at this point in the block.
	 * 
	 * @return
	 */
	public Type typeOf(int register) {
		return types[register];
	}
	
	/**
	 * Assign a given expression stored in the automaton to a given Wyil
	 * bytecode register.
	 * 
	 * @param register
	 * @param expr
	 */
	public void write(int register, Expr expr, Type type) {
		environment[register] = expr;
		types[register] = type;
	}
	
	public int nScopes() {
		return scopes.size();
	}
	
	public Scope scope(int i) {
		return scopes.get(i);
	}
	
	/**
	 * Get the first scope matching a given scope kind.
	 * 
	 * @param clazz
	 * @return
	 */
	public <T extends Scope> T topScope(Class<T> clazz) {
		for(int i=scopes.size();i>0;) {
			i=i-1;
			Scope scope = scopes.get(i);
			if(clazz.isInstance(scope)) {
				return (T) scope;
			}
		}
		return null;
	}

	/**
	 * Terminate the current flow for a given register and begin a new one. In
	 * terms of static-single assignment, this means simply change the index of
	 * the register in question.
	 * 
	 * @param register
	 */
	public Expr.Variable invalidate(int register, Type type) {
		// to invalidate a variable, we assign it a "skolem" constant. That is,
		// a fresh variable which has been previously encountered in the
		// branch.
		Expr.Variable var = Expr.Variable("r" + Integer.toString(register));
		environment[register] = var;
		types[register] = type;
		return var;
	}
	
	/**
	 * Invalidate all registers from <code>start</code> upto (but not including)
	 * <code>end</code>.
	 * 
	 * @param start
	 *            --- first register to invalidate.
	 * @param end
	 *            --- first register not to invalidate.
	 */
	public void invalidate(int start, int end, Type type) {
		for (int i = start; i != end; ++i) {
			invalidate(i,type);
		}
	}
	
	/**
	 * Return a reference into the automaton which represents all of the
	 * constraints that hold at this position in the branch.
	 * 
	 * @return
	 */
	public Expr constraints() {		
		ArrayList<Expr> constraints = new ArrayList<Expr>();
		for (int i = 0; i != scopes.size(); ++i) {
			Scope scope = scopes.get(i);
			constraints.addAll(scope.constraints);
		}
		return And(constraints);		
	}

	/**
	 * Add a given constraint to the list of constraints which are assumed to
	 * hold at this point.
	 * 
	 * @param constraint
	 */
	public void add(Expr constraint) {
		topScope().constraints.add(constraint);
	}
	
	/**
	 * Add a given list of constraints to the list of constraints which are assumed to
	 * hold at this point.
	 * 
	 * @param constraints
	 */
	public void addAll(List<Expr> constraints) {
		topScope().constraints.addAll(constraints);
	}

	/**
	 * Transform this branch into a list of constraints representing that which
	 * is known to hold at the end of the branch. The generated constraint will
	 * only be in terms of the given parameters and return value for the block.
	 * 
	 * @param transformer
	 *            --- responsible for transformining individual bytecodes into
	 *            constraints capturing their semantics.
	 * @return
	 */
	public Expr transform(VcTransformer transformer) {		
		ArrayList<VcBranch> children = new ArrayList<VcBranch>();
		int blockSize = block.size();
		while (pc < blockSize) {
									
			// first, check whether we're departing a scope or not.
			int top = scopes.size() - 1;
			while (top >= 0 && scopes.get(top).end < pc) {
				// yes, we're leaving a scope ... so notify transformer.
				Scope topScope = scopes.get(top);
				scopes.remove(top);
				dispatchExit(topScope, transformer);
				top = top - 1;
			}			
			
			// second, continue to transform the given bytecode
			Block.Entry entry = block.get(pc);
			Code code = entry.code;
			if(code instanceof Code.Goto) {				
				goTo(((Code.Goto) code).target);
			} else if(code instanceof Code.If) {
				Code.If ifc = (Code.If) code;
				VcBranch trueBranch = fork();	
				transformer.transform(ifc,this,trueBranch);
				trueBranch.goTo(ifc.target);
				children.add(trueBranch);
			} else if(code instanceof Code.Switch) {
				Code.Switch sw = (Code.Switch) code;
				VcBranch[] cases = new VcBranch[sw.branches.size()];
				for(int i=0;i!=cases.length;++i) {					
					cases[i] = fork();
					children.add(cases[i]);
				}				
				transformer.transform(sw,this,cases);
				for(int i=0;i!=cases.length;++i) {					
					cases[i].goTo(sw.branches.get(i).second());					
				}				
				goTo(sw.defaultTarget);
			} else if(code instanceof Code.IfIs) {
				Code.IfIs ifs = (Code.IfIs) code;
				Type type = typeOf(ifs.operand);				
				// First, determine the true test
				Type trueType = Type.intersect(type,ifs.rightOperand);		
				Type falseType = Type.intersect(type,Type.Negation(ifs.rightOperand));
				
				if(trueType.equals(Type.T_VOID)) {
					// This indicate that the true branch is unreachable and
					// should not be explored. Observe that this does not mean
					// the true branch is dead-code. Rather, since we're
					// preforming a path-sensitive traversal it means we've
					// uncovered an unreachable path. In this case, this branch
					// remains as the false branch.
{'fraction_non_alphanumeric': 0.10987435384673433, 'fraction_numerical': 0.002377089386107233, 'mean_word_length': 3.0090757827862653, 'pattern_counts': {'":': 0, '<': 127, '<?xml version=': 0, '>': 127, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1779293', 'n_tokens_mistral': 8714, 'n_tokens_neox': 7709, 'n_words': 2970}