/*******************************************************************************
 * 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.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;
	
	public PropertySimulator(IControlFlowGraph cfg, IPropertyFSM fsm) {
		this.cfg = cfg;
		this.fsm = fsm;
		worklist = new LinkedList<IBlock>();
		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
		solve();
	}

	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
		printStates(entryEdge, symStates);

		while (!worklist.isEmpty()) {
			IBlock blk = worklist.remove();
			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]));
				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));
				}
			}
		}
	}
	
	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();
		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) {			
			// Modify execution state according to branch condition
			ExecutionStateClause clause = null;
			// *N.B.* content for condition IBlock is condition expression itself
			if (node instanceof IASTBinaryExpression) {
				// FIXME compound conditionals
				IASTBinaryExpression binExpr = (IASTBinaryExpression) node;
				int op = binExpr.getOperator();

				// FIXME other ops
				// Check operator is an equality operator
				if (op == IASTBinaryExpression.op_equals) { // if (x == 0)
					IASTExpression o1 = binExpr.getOperand1();
					if (o1 instanceof IASTIdExpression) {
						IASTName name = ((IASTIdExpression) o1).getName();
						clause = parseConditional(clause, name, binExpr.getOperand2(), value);
					}
				}
				else if (op == IASTBinaryExpression.op_notequals) { // if (x != 0)
					IASTExpression o1 = binExpr.getOperand1();
					if (o1 instanceof IASTIdExpression) {
						IASTName name = ((IASTIdExpression) o1).getName();
						clause = parseConditional(clause, name, binExpr.getOperand2(), !value); // Negation
					}
				}
			}
			else if (node instanceof IASTUnaryExpression) { // if (!x)
				IASTUnaryExpression uExpr = (IASTUnaryExpression) node;
				int op = uExpr.getOperator();
				
				// Check operator is a negation operator
				if (op == IASTUnaryExpression.op_not) {
					IASTExpression operand = uExpr.getOperand();
					if (operand instanceof IASTIdExpression) {
						IASTName name = ((IASTIdExpression) operand).getName();
						clause = parseConditional(clause, name, !value); // Negation
					}
				}
			}
			else if (node instanceof IASTIdExpression) { // if (x)
				IASTName name = ((IASTIdExpression) node).getName();
				clause = parseConditional(clause, name, value);
			}
			
			if (clause != null) {
				ret.getExecutionState().addClause(clause);
				// TODO Theorem Prover goes here! / Determine if branch is feasible
				ret.getExecutionState().bindTruthAssignments();
			}
			else {
				// FIXME Handle unresolvable case
			}
		}
		
		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 void add(IControlFlowEdge edge,
			Set<SymbolicState> ss) {
		if (!edgeInfo.get(edge).equals(ss)) {
			edgeInfo.put(edge, ss);
			worklist.add(edge.getTo());
		}
	}
	
	private boolean isBranch(IBlock blk) {
		return blk.getOutEdges().length > 1;
	}

	private boolean isMerge(IBlock blk) {
		return blk.getInEdges().length > 1;
	}
	
	// FIXME REFACTOR
	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, IASTExpression valueExpr, boolean branchTruth) {
		IBinding binding = name.resolveBinding();
		if (binding instanceof IVariable) {
			IVariable var = (IVariable) binding;
			Boolean truth = getTruthValue(valueExpr);
			if (truth != null) {
				clause = new ExecutionStateClause(var, truth == branchTruth);
			}
		}
		return clause;
	}
	
	private ExecutionStateClause parseConditional(ExecutionStateClause clause, IASTName name, boolean branchTruth) {
		IBinding binding = name.resolveBinding();
		if (binding instanceof IVariable) {
			IVariable var = (IVariable) binding;
			clause = new ExecutionStateClause(var, branchTruth);
		}
		return clause;
	}

	private Boolean getTruthValue(IASTExpression valueExpr) {
		Boolean result = null;
		// Handle assignment from literals
		if (valueExpr instanceof IASTLiteralExpression) {
			int kind = ((IASTLiteralExpression) valueExpr).getKind();
			String value = String.valueOf(((IASTLiteralExpression) valueExpr).getValue());
			switch (kind) {
			case IASTLiteralExpression.lk_integer_constant:
				// 0 = False, > 0 = True
				result = !value.equals("0");
			}
		}
		// TODO other variable assignments
		return result;
	}
}