path: root/org.eclipse.cdt.codan.extension/src/org/eclipse/cdt/codan/extension/checkers/CloseOpenedFilesChecker.java

/*******************************************************************************
 * 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.checkers;

import java.io.File;
import java.net.URI;
import java.text.MessageFormat;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

import org.eclipse.cdt.codan.core.model.AbstractIndexAstChecker;
import org.eclipse.cdt.codan.extension.Activator;
import org.eclipse.cdt.codan.extension.ExecutionState;
import org.eclipse.cdt.codan.extension.ExecutionStateClause;
import org.eclipse.cdt.codan.extension.PropertyState;
import org.eclipse.cdt.codan.extension.SymbolicState;
import org.eclipse.cdt.codan.extension.VariableAssignmentVisitor;
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.IASTStatement;
import org.eclipse.cdt.core.dom.ast.IASTTranslationUnit;
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.core.resources.IProject;
import org.eclipse.core.resources.IResource;
import org.eclipse.core.resources.IWorkspaceRoot;
import org.eclipse.core.resources.ResourcesPlugin;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.GraphCreator;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IBlock;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraph;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.ICallGraphNode;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowEdge;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.IControlFlowGraph;
import org.eclipse.ptp.pldt.mpi.analysis.cdt.graphs.impl.ControlFlowGraph;

public class CloseOpenedFilesChecker extends AbstractIndexAstChecker {
	private static final String ERR_ID = Activator.PLUGIN_ID + ".CloseOpenedFilesProblem";
	
	private static final String OPEN = "open";
	private static final String CLOSE = "close";
	private Queue<IBlock> worklist;
	
	// Property simulation state info for CFG's edges
	private Map<IControlFlowEdge, Set<SymbolicState>> edgeInfo;
	
	// Property FSM states
	private PropertyState uninit;
	private PropertyState error;
	private PropertyState opened;
	
	// Most recent node to cause transition to error state
	private IASTNode errorNode;

	public CloseOpenedFilesChecker() {
		worklist = new LinkedList<IBlock>();
		edgeInfo = new HashMap<IControlFlowEdge, Set<SymbolicState>>();
		initFSM();
	}

	public void processAst(IASTTranslationUnit ast) {
		GraphCreator creator = new GraphCreator();

		// Retrieve resource corresponding to this translation unit
		String path = ast.getFilePath();
		URI fileURI = new File(path).toURI();
		IWorkspaceRoot wsRoot = ResourcesPlugin.getWorkspace().getRoot();
		IResource[] resources = wsRoot.findFilesForLocationURI(fileURI);
		if (resources != null && resources.length > 0) {
			IProject proj = resources[0].getProject();

			// Create call graph for project
			ICallGraph cg = creator.createCallGraph(proj);
			creator.computeCallGraph(cg);

			// Create control flow graph for each function
			for (ICallGraphNode node : cg.getAllNodes()) {
				IASTStatement fnBody = node.getFuncDef().getBody();
				IControlFlowGraph cfg = new ControlFlowGraph(fnBody);
				cfg.buildCFG();

				// Search for error states using property simulation algorithm
				solve(cfg);

				// Check if the exit edge of the CFG contains an error state
				IControlFlowEdge exitEdge = cfg.getExit().getInEdges()[0];
				for (SymbolicState s : edgeInfo.get(exitEdge)) {
					if (s.getPropertyStates().contains(error)) {
						// Report problem
						reportProblem(errorNode, s.getExecutionState());
					}
				}
			}
		}		
	}


	private void solve(IControlFlowGraph cfg) {
		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(uninit);
		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));
				}
			}
		}
	}


	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(ss1);
		ret.addAll(ss2);
		return group(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<ExecutionState>> statesPerProperty = new HashMap<PropertyState, Set<ExecutionState>>();
		for (SymbolicState s : ss) {
			for (PropertyState ps : s.getPropertyStates()) {
				if (!statesPerProperty.containsKey(ps)) {
					statesPerProperty.put(ps, new HashSet<ExecutionState>());
				}
				Set<ExecutionState> states = statesPerProperty.get(ps);
				states.add(s.getExecutionState());
			}
		}
		
		// 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<ExecutionState> es = statesPerProperty.get(p);
			if (es.size() > 1) {
				// Join execution states in this set
				es = ExecutionState.join(es);
			}
			for (ExecutionState e : es) {
				SymbolicState s = new SymbolicState(ps, e);
				ret.add(s);
			}
		}		
		
		return ret;
	}

	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) {
				newStates.add(state.transition(node));
			}
			s.setPropertyStates(newStates);
			
			// Modify execution state according to variable assignments
			node.accept(new VariableAssignmentVisitor(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 void initFSM() {
		uninit = new PropertyState("$u") {			
			@Override
			public PropertyState transition(IASTNode node) {
				PropertyState dest = uninit;
				if (containsOpen(node)) {
					dest = opened;
				}
				else if (containsClose(node)) {
					dest = error;
					errorNode = node;
				}
				return dest;
			}
		};
		
		opened = new PropertyState("o") {			
			@Override
			public PropertyState transition(IASTNode node) {
				PropertyState dest = opened;
				if (containsOpen(node)) {
					dest = error;
					errorNode = node;
				}
				if (containsClose(node)) {
					dest = uninit;
				}
				return dest;
			}
		};
		
		error = new PropertyState("$e") {
			
			@Override
			public PropertyState transition(IASTNode node) {
				return error;
			}
		};
	}

	protected boolean containsOpen(IASTNode node) {
		FunctionNameParser parser = new FunctionNameParser(node, OPEN, new String[] { "const char *", "int" });
		return parser.matches();
	}

	protected boolean containsClose(IASTNode node) {
		FunctionNameParser parser = new FunctionNameParser(node, CLOSE, new String[] { "int" });
		return parser.matches();
	}

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

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

	private void reportProblem(IASTNode node, ExecutionState condition) {
		String message = MessageFormat.format("Improper use of open/close given {0}.", condition);
		reportProblem(ERR_ID, node, message);
	}
	
	// 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;
	}
}