package jif.extension;

import jif.ast.Jif_c;
import jif.translate.ToJavaExt;
import jif.types.*;
import jif.types.label.Label;
import jif.visit.LabelChecker;
import polyglot.ast.Local;
import polyglot.ast.Node;
import polyglot.types.LocalInstance;
import polyglot.types.SemanticException;

/** The Jif extension of the <code>Local</code> node. 
 * 
 *  @see polyglot.ast.Local
 */
public class JifLocalExt extends Jif_c
{
    public JifLocalExt(ToJavaExt toJava) {
        super(toJava);
    }


    public Node labelCheckIncrement(LabelChecker lc) throws SemanticException
    {
	JifTypeSystem ts = lc.jifTypeSystem();
	JifContext A = lc.jifContext();

	Local lve = (Local) node();

	final LocalInstance li = lve.localInstance();

	Label L = ts.labelOfLocal(li, A.pc());

	PathMap X = ts.pathMap();
	X = X.N(A.pc());
	X = X.NV(L.join(A.pc()));

        // original constraint was X.NV() <= L
        // simplified to the equivalent constraint A.pc() <= L
        // (equivalent because X.NV == A.pc() join L)
        lc.constrain(new LabelConstraint(new NamedLabel("pc", 
                                                        "information revealed by reaching this program point", 
                                                        A.pc()), 
                                         LabelConstraint.LEQ, 
                                         new NamedLabel("label of local variable " + li.name(), L),
                                         A.labelEnv(),
                                         lve.position()) {
                 public String msg() {
                     return "Program counter at increment " + 
                            "more restrictive than the label for " + 
                            "local variable " + li.name();
                 }
                 public String detailMsg() { 
                     return "More information may be revealed by the program " +
                            "reaching this program point " +
                            "than is allowed to flow to " +
                            "the local variable " + li.name() + ". Because " +
                            li.name() + " is updated at this program point, " +
                            "the value of " + li.name() + " can reveal " +
                            "information at level A.pc. But this is more " +
                            "information than is allowed to flow to " + 
                            li.name() + ".";
                 }
                 public String technicalMsg() {
                     return "Invalid increment: [Xe.nv <= label(" + li.name() + 
                            ")] is not satisfied.";
                 }                     
         }
         );

	return X(lve, X);
    }

    public Node labelCheck(LabelChecker lc) throws SemanticException
    {
	JifTypeSystem ts = lc.jifTypeSystem();
	JifContext A = lc.jifContext();

	Local lve = (Local) node();

	LocalInstance li = lve.localInstance();

	Label L = ts.labelOfLocal(li, A.pc());

	PathMap X = ts.pathMap();
	X = X.N(A.pc());
	X = X.NV(L.join(A.pc()));

	return X(lve, X);
    }
}
