/*******************************************************************************
 * Copyright (c) 2009 Elliott Baron
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 *    Elliott Baron - initial API and implementation
 *******************************************************************************/
package org.eclipse.cdt.codan.extension;

import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.Map.Entry;

import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression;
import org.eclipse.cdt.core.dom.ast.IASTExpression;
import org.eclipse.cdt.core.dom.ast.IASTFileLocation;
import org.eclipse.cdt.core.dom.ast.IASTIdExpression;
import org.eclipse.cdt.core.dom.ast.IASTLiteralExpression;
import org.eclipse.cdt.core.dom.ast.IASTName;
import org.eclipse.cdt.core.dom.ast.IASTNode;
import org.eclipse.cdt.core.dom.ast.IASTUnaryExpression;
import org.eclipse.cdt.core.dom.ast.IBinding;
import org.eclipse.cdt.core.dom.ast.IVariable;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowEdge;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;

public class PropertySimulator {
	// Property simulation state info for CFG's edges
	private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo;
	private Queue<IBlock> worklist;
	private IControlFlowGraph cfg;
	private IPropertyFSM fsm;
	
	//XXX
	private Map<IBlock, Integer> exploreCount; 
	public PropertySimulator(IControlFlowGraph cfg, IPropertyFSM fsm) {
		this.cfg = cfg;
		this.fsm = fsm;
		worklist = new LinkedList<IBlock>();
		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
		exploreCount = new HashMap<IBlock, Integer>();
		for (IBlock blk : cfg.getBlocks()) {
			exploreCount.put(blk, 0);
		}
		solve();
		for (Entry<IBlock, Integer> entry : exploreCount.entrySet()) {
			if (entry.getValue().equals(0)) {
				IBlock blk = entry.getKey();
				System.out.println("Unprocessed block " + blk.getID() + ": ");
				blk.print();
			}
		}
	}

	private void solve() {
		for (IControlFlowEdge edge : cfg.getEdges()) {
			// Initialize edgeInfo for each edge
			Set<SymbolicState> set = new HashSet<SymbolicState>();
			edgeInfo.put(edge, set);
		}

		// Create edgeInfo for entry edge
		IControlFlowEdge entryEdge = cfg.getEntry().getOutEdges()[0];
		Set<SymbolicState> symStates = edgeInfo.get(entryEdge);
		Set<PropertyState> propStates = new HashSet<PropertyState>();
		propStates.add(fsm.getUninitState());
		symStates.add(new SymbolicState(propStates, new ExecutionState()));

		worklist.add(entryEdge.getTo());
		// XXX Debug
		System.out.println(printStates(entryEdge, symStates));

		while (!worklist.isEmpty()) {
			IBlock blk = worklist.remove();
			if (!blk.equals(cfg.getEntry()) && !blk.equals(cfg.getExit())) {
				Integer count = exploreCount.get(blk);
				exploreCount.put(blk, ++count);
			}
			
			if (isMerge(blk)) {
				// Apply flow function for a merge block
				Set<SymbolicState> newStates = flowMerge(blk, edgeInfo.get(blk.getInEdges()[0]), edgeInfo.get(blk.getInEdges()[1]));
				
				// Don't process the null exit block
				if (!blk.equals(cfg.getExit())) {
					add(blk.getOutEdges()[0], newStates);

					// XXX Debug
					System.out.println("MRG: " + printStates(blk.getOutEdges()[0], newStates));
				}
			}
			else if (isBranch(blk)) {
				// Apply flow function for a branch block
				Set<SymbolicState> oldStates = edgeInfo.get(blk.getInEdges()[0]);
				Set<SymbolicState> newStatesTrue = flowBranch(blk, oldStates, true);
				Set<SymbolicState> newStatesFalse = flowBranch(blk, oldStates, false);

				// Assumes 0th out-edge is true branch, 1st out-edge is false branch 
				add(blk.getOutEdges()[0], newStatesTrue);
				add(blk.getOutEdges()[1], newStatesFalse);
				
				// XXX Debug
				System.out.println("BR (T): " + printStates(blk.getOutEdges()[0], newStatesTrue));
				System.out.println("BR (F): " + printStates(blk.getOutEdges()[1], newStatesFalse));
			}
			else {
				// Apply flow function for a normal block
				Set<SymbolicState> newStates = flowOther(blk, edgeInfo.get(blk.getInEdges()[0]));
				
				// Don't process the null exit block
				if (!blk.equals(cfg.getExit())) {
					add(blk.getOutEdges()[0], newStates);
					// XXX Debug
					System.out.println("OTH: " + printStates(blk.getOutEdges()[0], newStates));
				}
			}
		}
	}

	private void add(IControlFlowEdge edge,
			Set<SymbolicState> ss) {
		//XXX
//		IBlock from = edge.getFrom();
//		if (from.getContent() != null
//				&& from.getContent().getRawSignature().contains("nextarg (\">\")")
//				&& edgeInfo.get(edge).size() > 0) {
//			System.out.println(printStates(edge, ss));
//			SymbolicState oldInfo = edgeInfo.get(edge).iterator().next();
//			SymbolicState newInfo = ss.iterator().next();
//			System.out.println("equals: " + oldInfo.equals(newInfo));
//			System.out.println("hashCode: " + (oldInfo.hashCode() == newInfo.hashCode()));
//		}
		if (!edgeInfo.get(edge).equals(ss)) {
			edgeInfo.put(edge, ss);
			worklist.add(edge.getTo());
		}
	}

	public Set<SymbolicState> getEndStates() {
		IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
		return edgeInfo.get(exitEdge);
	}
	
	private String printStates(IControlFlowEdge edge, Set<SymbolicState> states) {
		StringBuffer buf = new StringBuffer();
		IASTNode from = edge.getFrom().getContent();
		IASTNode to = edge.getTo().getContent();
		if (from != null) {
			IASTFileLocation loc = from.getFileLocation();
			if (loc != null) {
				int start = loc.getStartingLineNumber();
				int end = loc.getEndingLineNumber();
				if (start != end) {
					buf.append("lines " + start + " - " + end);
				}
				else {
					buf.append("line " + start);
				}
				buf.append(" ");
			}
		}
		buf.append("{");
		buf.append(from == null ? from : from.getRawSignature());
		buf.append(" -> ");
		buf.append(to == null ? to : to.getRawSignature());
		buf.append("} = ");
		buf.append(states);
		return buf.toString();		
	}

	private Set<SymbolicState> flowMerge(IBlock blk, Set<SymbolicState> ss1,
			Set<SymbolicState> ss2) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>();
		ret.addAll(filterTruthAssignments(blk, ss1));
		ret.addAll(filterTruthAssignments(blk, ss2));
		return group(ret);
	}

	private Set<SymbolicState> filterTruthAssignments(IBlock blk, Set<SymbolicState> ss) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>(ss.size());
		for (SymbolicState s : ss) {
			SymbolicState copy = s.copy();
			Set<IVariable> toRemove = new HashSet<IVariable>();
			Map<IVariable, TruthAssignment> truthAssignments = copy.getExecutionState().getTruthAssignments();
			for (Entry<IVariable, TruthAssignment> ta : truthAssignments.entrySet()) {
				// FIXME could be better
				// Remove truth assignments that were added by a block that doesn't dominate this one
				List<IBlock> dominators = blk.getDOM();
				IBlock origin = ta.getValue().getOrigin();
				if (!dominators.contains(origin)) {
					// Schedule removal
					toRemove.add(ta.getKey());
				}
			}
			// Actually remove
			for (IVariable var : toRemove) {
				truthAssignments.remove(var);
			}
			ret.add(copy);
		}
		return ret;
	}

	private Set<SymbolicState> flowBranch(IBlock blk, Set<SymbolicState> ss, boolean value) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>();
		for (SymbolicState s : ss) {
			SymbolicState s0 = transferBranch(blk, s, value);
			if (!s0.getExecutionState().isBottom()) {
				ret.add(s0);
			}
		}
		return group(ret);
	}

	private Set<SymbolicState> flowOther(IBlock blk, Set<SymbolicState> ss) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>();
		for (SymbolicState s : ss) {
			SymbolicState s0 = transferOther(blk, s);
			ret.add(s0);
		}
		return group(ret);
	}

	private Set<SymbolicState> group(Set<SymbolicState> ss) {
		return groupPropSim(ss);
	}
	
	private Set<SymbolicState> groupPSA(Set<SymbolicState> ss) {
		return ss;
	}
	
	private Set<SymbolicState> groupPropSim(Set<SymbolicState> ss) {
		Set<SymbolicState> ret = new HashSet<SymbolicState>();
		
		// Group SymbolicStates by PropertyState
		Map<PropertyState, Set<SymbolicState>> statesPerProperty = new HashMap<PropertyState, Set<SymbolicState>>();
		for (SymbolicState s : ss) {
			for (PropertyState ps : s.getPropertyStates()) {
				if (!statesPerProperty.containsKey(ps)) {
					statesPerProperty.put(ps, new HashSet<SymbolicState>());
				}
				Set<SymbolicState> states = statesPerProperty.get(ps);
				states.add(s);
			}
		}
		
		// Iterate through result and create SymbolicStates per PropertyState with ExecutionStates joined
		for (PropertyState p : statesPerProperty.keySet()) {
			Set<PropertyState> ps = new HashSet<PropertyState>();
			ps.add(p);
			Set<SymbolicState> ssForProperty = statesPerProperty.get(p);
			Set<ExecutionState> esForProperty = new HashSet<ExecutionState>();
			for (SymbolicState s : ssForProperty) {
				esForProperty.add(s.getExecutionState());
			}
			if (ssForProperty.size() > 1) {
				// Join execution states in this set
				ESTruthTable tt = new ESTruthTable(esForProperty);
				ESSimplifier simp = new ESSimplifier(tt);
				esForProperty = simp.getExecutionStateCover();
				
				for (ExecutionState e : esForProperty) {
					SymbolicState newState = new SymbolicState(ps, e);
					// Join corresponding error conditions
					if (p.equals(fsm.getErrorState())) {
						// Get original ExecutionStates implied by this prime implicant
						Set<ExecutionState> implied = simp.getImplications(e);
						// Find the appropriate SymbolicState
						for (ExecutionState orig : implied) {
							SymbolicState s = findSymbolicState(ssForProperty, orig);
							// Add its error cause to the joined state
							newState.getErrorCauses().addAll(s.getErrorCauses());
						}
					}
					ret.add(newState);
				}
			}
			else {
				// Nothing to do
				SymbolicState s = ssForProperty.iterator().next();
				ret.add(s);
			}
			
		}		
		
		return ret;
	}

	private SymbolicState findSymbolicState(Set<SymbolicState> ss, ExecutionState es) {
		for (SymbolicState s : ss) {
			if (s.getExecutionState().equals(es)) {
				return s;
			}
		}
		return null;
	}

	private SymbolicState transferBranch(IBlock blk, SymbolicState s, boolean value) {
		IASTNode node = blk.getContent();
		
		SymbolicState ret = s.copy();
		if (node != null) {			
			ConditionalVisitor visitor = new ConditionalVisitor(ret.getExecutionState(), value);
			node.accept(visitor);
		}
		
		return ret;
	}

	private SymbolicState transferOther(IBlock blk, SymbolicState s) {
		IASTNode node = blk.getContent();		
		
		if (node != null) {
			// Process property state transition
			Set<PropertyState> oldStates = s.getPropertyStates();
			Set<PropertyState> newStates = new HashSet<PropertyState>();
			for (PropertyState state : oldStates) {
				PropertyState dest = state.transition(node);
				// If we transition to from non-error to error, store the node that caused it
				if (!state.equals(fsm.getErrorState()) && dest.equals(fsm.getErrorState())) {
					s.getErrorCauses().add(node);
				}
				newStates.add(dest);
			}
			s.setPropertyStates(newStates);
			
			// Modify execution state according to variable assignments
			node.accept(new VariableAssignmentVisitor(blk, s.getExecutionState()));
		}
		return s;
	}

	private boolean isBranch(IBlock blk) {
		return blk.getOutEdges().length > 1;
	}

	private boolean isMerge(IBlock blk) {
		return blk.getInEdges().length > 1;
	}
	
}