jif.types

## Class AbstractSolver

- java.lang.Object
- - jif.types.AbstractSolver

- All Implemented Interfaces:
    Solver
  Direct Known Subclasses:
    SolverGLB

      public abstract class AbstractSolver
      extends java.lang.Object
      implements Solver

  A solver of Jif constraints. Finds solution to constraints essentially by propagating upper bounds backwards.

- - ### Nested Class Summary

    Nested Classes
    Modifier and Type | Class and Description
    --- | ---
    `protected static class` | `AbstractSolver.EquationQueue` A queue for equations.
    `protected class` | `AbstractSolver.Frame`

  - ### Field Summary

    Fields
    Modifier and Type | Field and Description
    --- | ---
    `protected VarMap` | `bounds`
    `protected polyglot.frontend.Compiler` | `compiler`
    `protected static int` | `constraint_counter` Counter of the number of constraints added to the system.
    `protected java.util.Set<Equation>` | `currentSCC`
    `protected java.util.Collection<Equation>` | `equations`
    `protected java.util.List<FailedConstraintSnapshot>` | `failedEquations`
    `protected java.util.Set<Variable>` | `fixedValueVars` Set of Variables that had their initial value fixed when the constraint was added.
    `java.util.List<InformationFlowTrace>` | `fullTrace`
    `protected AbstractSolver.EquationQueue` | `Q`
    `protected java.util.LinkedList<java.util.Set<Equation>>` | `scc`
    `protected static int` | `solverCounter` Number of solvers instantiated, for debugging purposes
    `protected java.util.Set<Equation>` | `staticFailedConstraints` Constraints that were added to the solver, and failed statically.
    `protected int` | `status`
    `protected static int` | `STATUS_NO_SOLUTION`
    `protected static int` | `STATUS_NOT_SOLVED`
    `protected static int` | `STATUS_SOLVED`
    `protected static int` | `STATUS_SOLVING`
    `protected static boolean` | `THROW_STATIC_FAILED_CONSTRAINTS`
    `protected static java.util.Collection<java.lang.String>` | `topics`
    `protected java.util.Map<VarLabel,java.util.List<polyglot.util.Pair<Equation,Label>>>` | `traces`
    `protected JifTypeSystem` | `ts`
    `protected boolean` | `useSCC` This boolean is used to turn on or off whether the strongly connected components optimization is used.

  - ### Constructor Summary

    Constructors
    Modifier | Constructor and Description
    --- | ---
    `protected` | `AbstractSolver(AbstractSolver js)` Constructor
    `protected` | `AbstractSolver(JifTypeSystem ts, polyglot.frontend.Compiler compiler, java.lang.String solverName)` Constructor
    `protected` | `AbstractSolver(JifTypeSystem ts, polyglot.frontend.Compiler compiler, java.lang.String solverName, boolean useSCC)` Constructor

  - ### Method Summary

    All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
    Modifier and Type | Method and Description
    --- | ---
    `void` | `addConstraint(Constraint c)` Add the constraint c to the system
    `protected void` | `addConstraintEquations(Constraint c)` Go through each equation in the constraint, add the equation if needed, and register dependencies for the equation.
    `protected abstract void` | `addDependencies(Equation eqn)` This abstract method must add the correct dependencies from Equation eqn to variables occurring in eqn, and dependencies in the other direction (that is, from variables occurring in eqn to eqn).
    `protected void` | `addDependency(Equation eqn, Variable var)` This method records a dependency from Equation eqn to variable var.
    `protected void` | `addDependency(Variable var, Equation eqn)` This method records a dependency from variable var to Equation eqn.
    `protected void` | `addEquationToQueue(Equation eqn)`
    `protected void` | `addEquationToQueueHead(Equation eqn)`
    `protected void` | `addTrace(VarLabel v, Label sourcelabel, Equation eqn, Label lb, InformationFlowTrace.Direction dir)` Record the fact that label variable v, in the constraint eqn had its bound set to the label lb.
    `Label` | `applyBoundsTo(Label L)` Substitute variables in L with the solution for the variables.
    `VarMap` | `bounds()` Get the bounds for this Solver.
    `protected void` | `checkCandidateSolution()` Check the candidate solution
    `protected void` | `checkEquationSatisfied(LabelEquation eqn)`
    `protected void` | `considerEquation(Equation eqn)`
    `protected void` | `considerEquation(LabelEquation eqn)`
    `protected void` | `considerEquation(PrincipalEquation eqn)`
    `protected java.util.Set<Equation>` | `eqnEqnDependencies(Equation eqn)` Returns the equations that are dependent on the equation eqn by finding the variables that eqn may alter if it is solved (useing the map eqnVarDependencies), and then finds the equations that depend on those variables (using the map varEqnDependencies)
    `protected java.util.Set<Equation>` | `eqnEqnReverseDependencies(Equation eqn)` Returns the equations that are reverse dependent on the equation eqn by finding the variables that may invalidate eqn (using the map eqnVarReverseDependencies), and then finding the equations that may alter those variables (using the map varEqnReverseDependencies)
    `protected Equation` | `findContradictiveEqn(Constraint c)`
    `protected abstract Equation` | `findContradictiveEqn(LabelConstraint c)`
    `protected polyglot.util.Pair<Equation[],int[]>` | `findSCCs()` Returns the pair [by_scc, scc_head] where by_scc is an array in which SCCs occur in topologically order.
    `protected Equation` | `findTrace(VarLabel var, Label threshold, boolean lowerThreshold)`
    `void` | `genFlowMessage(UnsatisfiableConstraintException ex)`
    `protected abstract Label` | `getDefaultLabelBound()` This method must return a constant label, which is the default bound of label variables.
    `protected abstract Principal` | `getDefaultPrincipalBound()` This method must return a constant principal, which is the default bound of principal variables.
    `protected java.util.List<Equation>` | `getQueue()`
    `protected void` | `inc_counter()` Increase the count of the number of constraints added (not just to this system, but to all instances of the Solver).
    `protected boolean` | `isFixedValueVar(Variable v)`
    `protected void` | `processConstraint(Constraint c)` Perform any special processing for the label constraint
    `static void` | `report(int level, java.lang.String s)` Convenience method to report messages for the appropriate topics
    `protected UnsatisfiableConstraintException` | `reportError(Equation eqn)` Report an unsatisfiable constraint
    `protected void` | `reportTrace(Variable v)` Report a trace for a given variable.
    `void` | `setBound(VarLabel v, Label newBound, LabelConstraint responsible)`
    `void` | `setBound(VarPrincipal v, Principal newBound, PrincipalConstraint responsible)`
    `void` | `setBounds(VarMap bnds)` Set the bounds for this Solver.
    `protected void` | `setStatus(int status)`
    `static boolean` | `shouldReport(int obscurity)` Convenience method to determine if messages of the given obscurity should be reported.
    `protected VarMap` | `solve_bounds()` Solve the system of constraints, by finding upper bounds for the label variables.
    `protected abstract void` | `solve_eqn(LabelEquation eqn)` This method changes the bounds of variables in the Equation eqn, to make the equation satisfied.
    `protected abstract void` | `solve_eqn(PrincipalEquation eqn)` This method changes the bounds of variables in the Equation eqn, to make the equation satisfied.
    `VarMap` | `solve()` Solve the system of constraints.
    `java.lang.String` | `solverName()`
    `protected Label` | `triggerTransforms(Label label, LabelEnv env)`
    `protected void` | `wakeUp(Variable v)` Awakens all equations in the system that depend on the variable v, ensuring that they are in the queue of active equations.

    - ### Methods inherited from class java.lang.Object

      `clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

- - ### Field Detail

    - #### Q

          protected AbstractSolver.EquationQueue Q

    - #### scc

          protected java.util.LinkedList<java.util.Set<Equation>> scc

    - #### currentSCC

          protected java.util.Set<Equation> currentSCC

    - #### equations

          protected java.util.Collection<Equation> equations

    - #### failedEquations

          protected java.util.List<FailedConstraintSnapshot> failedEquations

    - #### fixedValueVars

          protected java.util.Set<Variable> fixedValueVars

      Set of Variables that had their initial value fixed when the constraint was added.

    - #### STATUS_NOT_SOLVED

          protected static final int STATUS_NOT_SOLVED

      See Also:
        Constant Field Values

    - #### STATUS_SOLVING

          protected static final int STATUS_SOLVING

      See Also:
        Constant Field Values

    - #### STATUS_SOLVED

          protected static final int STATUS_SOLVED

      See Also:
        Constant Field Values

    - #### STATUS_NO_SOLUTION

          protected static final int STATUS_NO_SOLUTION

      See Also:
        Constant Field Values

    - #### status

          protected int status

    - #### bounds

          protected VarMap bounds

    - #### ts

          protected JifTypeSystem ts

    - #### staticFailedConstraints

          protected java.util.Set<Equation> staticFailedConstraints

      Constraints that were added to the solver, and failed statically. If the flag THROW_STATIC_FAILED_CONSTRAINTS is true, then the constraint will be thrown immediately, otherwise the constraint will be added to this set, and thrown when solve() is called.

    - #### THROW_STATIC_FAILED_CONSTRAINTS

          protected static final boolean THROW_STATIC_FAILED_CONSTRAINTS

      See Also:
        Constant Field Values

    - #### compiler

          protected final polyglot.frontend.Compiler compiler

    - #### traces

          protected java.util.Map<VarLabel,java.util.List<polyglot.util.Pair<Equation,Label>>> traces

    - #### fullTrace

          public java.util.List<InformationFlowTrace> fullTrace

    - #### topics

          protected static java.util.Collection<java.lang.String> topics

    - #### useSCC

          protected final boolean useSCC

      This boolean is used to turn on or off whether the strongly connected components optimization is used. If true, the constraints are partitioned into strongly connected components, which are then sorted in topological order. If false, then constraints are solved in the order they are added to the solver

    - #### solverCounter

          protected static int solverCounter

      Number of solvers instantiated, for debugging purposes

    - #### constraint_counter

          protected static int constraint_counter

      Counter of the number of constraints added to the system. For debugging purposes.

  - ### Constructor Detail

    - #### AbstractSolver

          protected AbstractSolver(JifTypeSystem ts,
                                   polyglot.frontend.Compiler compiler,
                                   java.lang.String solverName)

      Constructor

    - #### AbstractSolver

          protected AbstractSolver(JifTypeSystem ts,
                                   polyglot.frontend.Compiler compiler,
                                   java.lang.String solverName,
                                   boolean useSCC)

      Constructor

    - #### AbstractSolver

          protected AbstractSolver(AbstractSolver js)

      Constructor

  - ### Method Detail

    - #### report

          public static final void report(int level,
                                          java.lang.String s)

      Convenience method to report messages for the appropriate topics

    - #### shouldReport

          public static final boolean shouldReport(int obscurity)

      Convenience method to determine if messages of the given obscurity should be reported.

    - #### applyBoundsTo

          public Label applyBoundsTo(Label L)

      Description copied from interface: `Solver`
      Substitute variables in L with the solution for the variables. Should only be called after solve() has been called successfully.
      Specified by:
        `applyBoundsTo` in interface `Solver`
      Returns:
        L with variables replaced appropriately according to the solution.

    - #### triggerTransforms

          protected Label triggerTransforms(Label label,
                                            LabelEnv env)

    - #### getQueue

          protected java.util.List<Equation> getQueue()

    - #### addEquationToQueue

          protected void addEquationToQueue(Equation eqn)

    - #### addEquationToQueueHead

          protected void addEquationToQueueHead(Equation eqn)

    - #### bounds

          public VarMap bounds()

      Get the bounds for this Solver.

    - #### setBounds

          public void setBounds(VarMap bnds)

      Set the bounds for this Solver.

    - #### setBound

          public void setBound(VarLabel v,
                               Label newBound,
                               LabelConstraint responsible)
                        throws polyglot.types.SemanticException

      Parameters:
        `v` - the VarLabel to set the bound for
        `newBound` - the new bound for v
        `responsible` - the constraint that was responsible for modifying the bound.
      Throws:
        `polyglot.types.SemanticException` - if the new bound violates an equality constraint.

    - #### setBound

          public void setBound(VarPrincipal v,
                               Principal newBound,
                               PrincipalConstraint responsible)

    - #### solve

          public VarMap solve()
                       throws polyglot.types.SemanticException

      Solve the system of constraints. If the system has already been solved, then returned the cached solution.
      Specified by:
        `solve` in interface `Solver`
      Throws:
        `polyglot.types.SemanticException` - if the Solver cannot find a solution to the system of contraints.

    - #### genFlowMessage

          public void genFlowMessage(UnsatisfiableConstraintException ex)

    - #### setStatus

          protected void setStatus(int status)

    - #### getDefaultLabelBound

          protected abstract Label getDefaultLabelBound()

      This method must return a constant label, which is the default bound of label variables.

    - #### getDefaultPrincipalBound

          protected abstract Principal getDefaultPrincipalBound()

      This method must return a constant principal, which is the default bound of principal variables.

    - #### solve_bounds

          protected VarMap solve_bounds()
                                 throws polyglot.types.SemanticException

      Solve the system of constraints, by finding upper bounds for the label variables.
      Returns:
        a solution to the system of constraints, in the form of a VarMap of the upper bounds of the label variables.
      Throws:
        `polyglot.types.SemanticException` - if the Solver cannot find a solution to the system of constraints.

    - #### considerEquation

          protected void considerEquation(Equation eqn)
                                   throws polyglot.types.SemanticException

      Throws:
        `polyglot.types.SemanticException`

    - #### considerEquation

          protected void considerEquation(LabelEquation eqn)
                                   throws polyglot.types.SemanticException

      Throws:
        `polyglot.types.SemanticException`

    - #### solve_eqn

          protected abstract void solve_eqn(LabelEquation eqn)
                                     throws polyglot.types.SemanticException

      This method changes the bounds of variables in the Equation eqn, to make the equation satisfied. The method may postpone solving the equation by putting the equation back on the queue, using addEquationToQueue().
      Throws:
        `polyglot.types.SemanticException`

    - #### considerEquation

          protected void considerEquation(PrincipalEquation eqn)
                                   throws polyglot.types.SemanticException

      Throws:
        `polyglot.types.SemanticException`

    - #### solve_eqn

          protected abstract void solve_eqn(PrincipalEquation eqn)
                                     throws polyglot.types.SemanticException

      This method changes the bounds of variables in the Equation eqn, to make the equation satisfied. The method may postpone solving the equation by putting the equation back on the queue, using addEquationToQueue().
      Throws:
        `polyglot.types.SemanticException`

    - #### checkCandidateSolution

          protected final void checkCandidateSolution()
                                               throws polyglot.types.SemanticException

      Check the candidate solution
      Throws:
        `polyglot.types.SemanticException`

    - #### checkEquationSatisfied

          protected void checkEquationSatisfied(LabelEquation eqn)
                                         throws polyglot.types.SemanticException

      Throws:
        `polyglot.types.SemanticException`

    - #### wakeUp

          protected final void wakeUp(Variable v)

      Awakens all equations in the system that depend on the variable v, ensuring that they are in the queue of active equations.

    - #### solverName

          public java.lang.String solverName()

    - #### inc_counter

          protected final void inc_counter()

      Increase the count of the number of constraints added (not just to this system, but to all instances of the Solver). For debugging purposes, if the constraint counter is equal to the stop_constraint, then a RuntimeException is thrown.

    - #### isFixedValueVar

          protected boolean isFixedValueVar(Variable v)

    - #### addConstraint

          public void addConstraint(Constraint c)
                             throws polyglot.types.SemanticException

      Add the constraint c to the system
      Specified by:
        `addConstraint` in interface `Solver`
      Throws:
        `polyglot.types.SemanticException`

    - #### processConstraint

          protected void processConstraint(Constraint c)
                                    throws polyglot.types.SemanticException

      Perform any special processing for the label constraint
      Throws:
        `polyglot.types.SemanticException`

    - #### addConstraintEquations

          protected void addConstraintEquations(Constraint c)
                                         throws polyglot.types.SemanticException

      Go through each equation in the constraint, add the equation if needed, and register dependencies for the equation.
      Parameters:
        `c` -
      Throws:
        `polyglot.types.SemanticException`

    - #### addDependencies

          protected abstract void addDependencies(Equation eqn)

      This abstract method must add the correct dependencies from Equation eqn to variables occurring in eqn, and dependencies in the other direction (that is, from variables occurring in eqn to eqn). There is a dependency from Equation eqn to variable var if the bound on var may be modified as a result of solving eqn. This dependency should be recorded by calling the method addDependency(eqn, var). There is a dependency from variable var to Equation eqn if modifying the bound on var may cause eqn to no longer be satisfied. This dependency should be recorded by calling the method addDependency(var, eqn).

    - #### addDependency

          protected void addDependency(Variable var,
                                       Equation eqn)

      This method records a dependency from variable var to Equation eqn. This method should only be called by subclasses during the execution of the method addDependencies(). There is a dependency from variable var to Equation eqn if modifying the bound on var may cause eqn to no longer be satisfied.

    - #### addDependency

          protected void addDependency(Equation eqn,
                                       Variable var)

      This method records a dependency from Equation eqn to variable var. This method should only be called by subclasses during the execution of the method addDependencies(). There is a dependency from Equation eqn to variable var if the bound on var may be modified as a result of solving eqn.

    - #### eqnEqnDependencies

          protected java.util.Set<Equation> eqnEqnDependencies(Equation eqn)

      Returns the equations that are dependent on the equation eqn by finding the variables that eqn may alter if it is solved (useing the map eqnVarDependencies), and then finds the equations that depend on those variables (using the map varEqnDependencies)

    - #### eqnEqnReverseDependencies

          protected java.util.Set<Equation> eqnEqnReverseDependencies(Equation eqn)

      Returns the equations that are reverse dependent on the equation eqn by finding the variables that may invalidate eqn (using the map eqnVarReverseDependencies), and then finding the equations that may alter those variables (using the map varEqnReverseDependencies)

    - #### addTrace

          protected final void addTrace(VarLabel v,
                                        Label sourcelabel,
                                        Equation eqn,
                                        Label lb,
                                        InformationFlowTrace.Direction dir)

      Record the fact that label variable v, in the constraint eqn had its bound set to the label lb.

    - #### findTrace

          protected final Equation findTrace(VarLabel var,
                                             Label threshold,
                                             boolean lowerThreshold)

      Returns:
        an equation that contained label variable var, and that changed the bound of var to less than/greater than threshold. Null if no such equation exists. If lowerThreshold is true, then the equation returned is one that changed var to less than threshold; otherwise the equation returned is one that changed var to greater than the threshold

    - #### findContradictiveEqn

          protected Equation findContradictiveEqn(Constraint c)

    - #### findContradictiveEqn

          protected abstract Equation findContradictiveEqn(LabelConstraint c)

    - #### findSCCs

          protected polyglot.util.Pair<Equation[],int[]> findSCCs()

      Returns the pair [by_scc, scc_head] where by_scc is an array in which SCCs occur in topologically order. scc_head[n] where n is the first peer in an SCC is set to -1. scc_head[n] where n is the last peer in a (non-singleton) SCC is set to the index of the first peer. Otherwise it is -2. by_scc contains the peers grouped by SCC. scc_head marks where the SCCs are. The SCC begins with a -1 and ends with the index of the beginning of the SCC.

    - #### reportError

          protected UnsatisfiableConstraintException reportError(Equation eqn)

      Report an unsatisfiable constraint
      Parameters:
        `eqn` - The equation that is unsatisfiable
      Returns:
        a suitable exception to indicate the failure

    - #### reportTrace

          protected void reportTrace(Variable v)

      Report a trace for a given variable.