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 UsageChecker extends PropertyListenerAdapter {

    /// Error string
    String error;
    
    /**
     * Parse configuration and get what we are interested in.
     * @param conf JPF-Configuration.
     */
    public UsageChecker(Config conf) {
	// TODO: Implement
    }

    /**
     * The JVM just executed an instruction and notifies us about it.  If this
     * instruction was a method call we are interested in, do some checks.
     * @param vm JPF-JVM
     */
    public void instructionExecuted(JVM vm) {
	Instruction insn = vm.getLastInstruction();
	if (insn instanceof InvokeInstruction) {
	    InvokeInstruction invoke = (InvokeInstruction) insn;
	    ElementInfo ei = getLastThis(vm, invoke);
	    if (ei != null) {
		// TODO: Implement	
	    }
	}
    }

    private ElementInfo getLastThis(JVM vm, InvokeInstruction invoke) {
	int objRef = invoke.getLastObjRef();
	if (objRef != -1)
	    return vm.getHeap().get(objRef);
	return null;
    }

    /**
     * Store an error message.
     * @param vm JPF-JVM
     * @param insn Invokation instruction.
     */
    private void storeError(JVM vm, InvokeInstruction insn) {
	// TODO: This gives ugly error messages...
	ThreadInfo ti = vm.getLastThreadInfo();
	error = String.format(
	    "call to method %s with signature %s in thread %s at %s violates " +
	    "calling convention", insn.getInvokedMethodName(),
	    insn.getInvokedMethodSignature(), ti.getName(),
	    insn.getSourceLocation());
    }

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

    public String getErrorMessage() {
	return error;
    }

    public void reset() {
	error = null;
    }

}