package exercises;

import java.util.*;
import gov.nasa.jpf.*;
import gov.nasa.jpf.util.*;
import gov.nasa.jpf.jvm.*;
import gov.nasa.jpf.jvm.bytecode.*;
import gov.nasa.jpf.search.*;

public class ChristmasListener extends PropertyListenerAdapter {

    /**
     * Just an immutable "constant array" tag.
     */
    private static class ConstTag {}
    /// We only need one tag.
    private static final ConstTag tag = new ConstTag();

    /// Descriptor for the initialization method
    MethodSpec initSpec;
    /// Error string
    String error;
    
    /**
     * Parse configuration and get what we are interested in.
     * @param conf JPF-Configuration.
     */
    public ChristmasListener(Config conf) {
	String init = conf.getString("cl.init");
	if (init == null)
	    throw conf.exception("Missing cl.init");
	initSpec = MethodSpec.createMethodSpec(init);
	if (initSpec == null)
	    throw conf.exception("Bad cl.init");
    }

    /**
     * The JVM just executed an instruction and notifies us about it.  If this
     * instruction was a write into a field we are interested in, do a null
     * check.
     * @param vm JPF-JVM
     */
    public void instructionExecuted(JVM vm) {
	Instruction insn = vm.getLastInstruction();
	ThreadInfo ti = vm.getLastThreadInfo();
	if (insn instanceof ARETURN) {
	    MethodInfo mi = insn.getMethodInfo();
	    if (initSpec.matches(mi))
		flagReturn(
		    (ElementInfo) ((ARETURN) insn).getReturnValue(ti), ti);
	} else if (insn instanceof ArrayStoreInstruction) {
	    checkMarked(vm, (ArrayStoreInstruction) insn, ti);
	}
    }

    private void flagReturn(ElementInfo arrayInfo, ThreadInfo ti) {
	if (arrayInfo.isArray()) {
	    /* This is a bug in JPF! arrayInfo.isReferenceArray() should
	       return true.
	    */
	    if (/*arrayInfo.isReferenceArray()*/
		arrayInfo.getFields() instanceof ReferenceArrayFields) {
		System.err.println("Flagging multidim array");
		// Handle multi-dimensional arrays
		for (int i = 0; i < arrayInfo.arrayLength(); ++i)
		    flagReturn(
			ti.getElementInfo(arrayInfo.getReferenceElement(i)),
			ti);
	    }
	    System.err.println("Flagging array");
	    arrayInfo.addObjectAttr(tag);
	}
    }
    
    private void checkMarked(JVM vm, ArrayStoreInstruction store,
			     ThreadInfo ti) {
	int arr = store.getArrayRef(ti);
	ElementInfo ei = ti.getElementInfo(arr);
	if (ei.hasObjectAttr(ConstTag.class)) {
	    storeError(vm, store);
	    vm.breakTransition();
	}
    }

    /**
     * Store an error message.
     * @param vm JPF-JVM
     * @param insn Array store instruction that wrote a value into a constant field
     */
    private void storeError(JVM vm, ArrayStoreInstruction insn) {
	ThreadInfo ti = vm.getLastThreadInfo();
	MethodInfo mi = insn.getMethodInfo();
	error = String.format("function %s assigned to a value to a constant array in thread %s at %s", mi.getLongName(), ti.getName(), insn.getSourceLocation());
    }

    public boolean check(Search search, JVM vm) {
	return error == null;
    }

    public String getErrorMessage() {
	return error;
    }

    public void reset() {
	error = null;
    }

}