/*
 * Copyright (C) 2014, United States Government, as represented by the
 * Administrator of the National Aeronautics and Space Administration.
 * All rights reserved.
 *
 * The Java Pathfinder core (jpf-core) platform is licensed under the
 * Apache License, Version 2.0 (the "License"); you may not use this file except
 * in compliance with the License. You may obtain a copy of the License at
 * 
 *        http://www.apache.org/licenses/LICENSE-2.0. 
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and 
 * limitations under the License.
 */
package gov.nasa.jpf.listener;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
import gov.nasa.jpf.report.Publisher;
import gov.nasa.jpf.report.PublisherExtension;
import gov.nasa.jpf.vm.ClassInfo;
import gov.nasa.jpf.vm.Instruction;
import gov.nasa.jpf.vm.MethodInfo;
import gov.nasa.jpf.vm.ThreadInfo;
import gov.nasa.jpf.vm.VM;
import gov.nasa.jpf.vm.VMListener;

import java.io.PrintWriter;

/**
 * This listener monitors method invocations.  When JPF finishes, it publishes for each method invocation, 
 * <ul>
 * <li>the ID of the thread that executed the method invocation,</li>
 * <li>the depth of the stack of that thread,</li> 
 * <li>the name of the class to which the method belongs,</li> 
 * <li>the name of the method, and</li>
 * <li>the arguments of the method.</li>
 * </ul>
 * For example, consider the following.
 * <pre>
 * 0:    Example.first(1,true)
 * 0:     Example.second(2)
 * </pre>
 * Both method invocations are executed by thread 0, which is the main thread.  The number of spaces
 * following 0: indicates the depth of the stack.  Hence, the method second is invoked within the method first.
 * 
 * @author Unknown
 * @author Franck van Breugel
 */
public class CallMonitor extends ListenerAdapter implements VMListener, PublisherExtension {
	private StringBuilder result;

	/**
	 * Initializes this listener.
	 *
	 * @param configuration JPF's configuration.
	 * @param jpf JPF.
	 */
	public CallMonitor(Config configuration, JPF jpf) {
		super();
		this.result = new StringBuilder();
		jpf.addPublisherExtension(Publisher.class, this);
	}

	/**
	 * Whenever a method is invoked, information about the call is recorded.
	 *
	 * @param vm JPF's virtual machine.
	 * @param thread the thread that executed the instruction.
	 * @param next the next instruction to be executed.
	 * @param executed the executed instruction.
	 */
	@Override
	public void instructionExecuted(VM vm, ThreadInfo thread, Instruction next, Instruction executed) {
		if (executed instanceof JVMInvokeInstruction) {
			if (executed.isCompleted(thread) && !thread.isInstructionSkipped()) {
				JVMInvokeInstruction call = (JVMInvokeInstruction) executed;
				this.publishCall(call, thread);
			}
		}
	}

	/**
	 * Records information of the given call, executed by the given thread.  In particular, it records the thread ID, 
	 * the depth of the stack, the name of the class, the name of the method, and its arguments. 
	 *
	 * @param call the method invocation.
	 * @param thread the thread that executed the method invocation.
	 */
	private void publishCall(JVMInvokeInstruction call, ThreadInfo thread) {
		MethodInfo method = call.getInvokedMethod();
		Object[] argument = call.getArgumentValues(thread);
		ClassInfo clazz = method.getClassInfo();

		// thread ID
		this.result.append(thread.getId());
		this.result.append(": ");

		// stack depth
		int depth = thread.getStackDepth();
		for (int d = 0; d < depth; d++) {
			this.result.append(" ");
		}

		// class name
		if (clazz != null){
			this.result.append(clazz.getName());
			this.result.append('.');
		}

		// method name
		this.result.append(method.getName());
		this.result.append('(');

		// arguments
		int length = argument.length;
		for (int i = 0; i < length; i++) {
			if (argument[i] != null) {
				this.result.append(argument[i].toString());
			} else {
				this.result.append("null");
			}
			if (i < length - 1) { // no comma after the last argument
				this.result.append(',');
			}
		}
		this.result.append(')');

		this.result.append('\n');
	}

	/**
	 * When JPF has finished, the information of all method calls is published.
	 *
	 * @param publisher JPF's publisher.
	 */
	@Override
	public void publishFinished(Publisher publisher) {
		PrintWriter output = publisher.getOut();
		publisher.publishTopicStart("method invocations");
		output.print(this.result);
		publisher.publishTopicEnd("method invocations");
	}
}