Pthread2CIVLWorker.java

package edu.udel.cis.vsl.civl.transform.common;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;

import edu.udel.cis.vsl.abc.ast.IF.AST;
import edu.udel.cis.vsl.abc.ast.IF.ASTFactory;
import edu.udel.cis.vsl.abc.ast.entity.IF.Entity;
import edu.udel.cis.vsl.abc.ast.entity.IF.Variable;
import edu.udel.cis.vsl.abc.ast.node.IF.ASTNode;
import edu.udel.cis.vsl.abc.ast.node.IF.NodePredicate;
import edu.udel.cis.vsl.abc.ast.node.IF.SequenceNode;
import edu.udel.cis.vsl.abc.ast.node.IF.declaration.FunctionDefinitionNode;
import edu.udel.cis.vsl.abc.ast.node.IF.declaration.VariableDeclarationNode;
import edu.udel.cis.vsl.abc.ast.node.IF.expression.CastNode;
import edu.udel.cis.vsl.abc.ast.node.IF.expression.ExpressionNode;
import edu.udel.cis.vsl.abc.ast.node.IF.expression.FunctionCallNode;
import edu.udel.cis.vsl.abc.ast.node.IF.expression.IdentifierExpressionNode;
import edu.udel.cis.vsl.abc.ast.node.IF.expression.OperatorNode;
import edu.udel.cis.vsl.abc.ast.node.IF.expression.OperatorNode.Operator;
import edu.udel.cis.vsl.abc.ast.node.IF.statement.BlockItemNode;
import edu.udel.cis.vsl.abc.ast.node.IF.statement.CompoundStatementNode;
import edu.udel.cis.vsl.abc.ast.node.IF.statement.ExpressionStatementNode;
import edu.udel.cis.vsl.abc.ast.node.IF.statement.ReturnNode;
import edu.udel.cis.vsl.abc.ast.node.IF.statement.StatementNode;
import edu.udel.cis.vsl.abc.ast.node.IF.type.FunctionTypeNode;
import edu.udel.cis.vsl.abc.ast.node.IF.type.PointerTypeNode;
import edu.udel.cis.vsl.abc.ast.node.IF.type.TypeNode;
import edu.udel.cis.vsl.abc.ast.node.IF.type.TypeNode.TypeNodeKind;
import edu.udel.cis.vsl.abc.ast.type.IF.Type.TypeKind;
import edu.udel.cis.vsl.abc.parse.IF.CParser;
import edu.udel.cis.vsl.abc.token.IF.SyntaxException;
import edu.udel.cis.vsl.civl.model.IF.CIVLUnimplementedFeatureException;
import edu.udel.cis.vsl.civl.transform.IF.Pthread2CIVLTransformer;

//TODO: add arguments to pthread_exit();

/**
 * TODO list all the transformation (e.g., pthread_create, pthread_exit to
 * _pthread_exit) with explanation of how it works and why it is necessary
 * 
 * @author zmanchun
 *
 */
public class Pthread2CIVLWorker extends BaseWorker {

	// private final static String PTHREAD_MUTEX_LOCK="pthread_mutex_lock";

	private final static String PTHREAD_POOL_TYPE = "$pthread_pool_t";

	private final static String MAIN = "main";

	private final static String GENERATED_MAIN = "_gen_main";

	private boolean fixedMain = false;

	static final String PTHREAD_MUTEX_LOCK = "pthread_mutex_lock";

	static final String PTHREAD_MUTEX_LOCK_NEW = "$pthread_mutex_lock";

	static final String PTHREAD_COND_WAIT = "pthread_cond_wait";

	static final String PTHREAD_COND_WAIT_NEW = "$pthread_cond_wait";

	final static String PTHREAD_POOL_CREATE = "$pthread_pool_create";

	final static String PTHREAD_GPOOL = "$pthread_gpool";

	private final static String PTHREAD_POOL = "_pthread_pool";

	// needs to go to MPI process scope
	final static String PTHREAD_CREATE = "pthread_create";

	private final static String PTHREAD_EXIT = "pthread_exit";

	final static String PTHREAD_EXIT_NEW = "$pthread_exit";

	private final static String PTHREAD_SELF = "pthread_self";

	final static String PTHREAD_SELF_NEW = "$pthread_self";

	// needs to go to MPI process scope
	final static String PTHREAD_EXIT_MAIN_NEW = "$pthread_exit_main";

	// private final static String ERROR = "ERROR";

	// private final static String VERIFIER_NONDET_UINT =
	// "__VERIFIER_nondet_uint";
	//
	// private final static String VERIFIER_NONDET_INT =
	// "__VERIFIER_nondet_int";
	//
	// private final static String VERIFIER_ASSUME = "__VERIFIER_assume";
	//
	// private final static String VERIFIER_ASSERT = "__VERIFIER_assert";
	//
	// private final static String VERIFIER_ATOMIC = "__VERIFIER_atomic";

	// private int numberOfNondetCall = 0;

	private boolean exitMainDone = false;

	/* **************************** Instance Fields ************************* */

	private Set<String> threadFunctionNames = new LinkedHashSet<>();

	private Set<FunctionDefinitionNode> nonThreadFunctionsWtSyncCalls = new HashSet<>();

	private Set<String> nonThreadFunctionNamesWtSyncCalls = new HashSet<>();

	private Set<String> newNonThreadFunctionNamesWtSyncCalls = new HashSet<>();

	private Set<String> currentNewNonThreadFunctionNamesWtSyncCalls = new HashSet<>();

	private List<String> syncCallFunctionNames = new ArrayList<>();

	private Set<VariableDeclarationNode> thread_local_variable_declarations = new LinkedHashSet<>();

	private Set<String> newNonThreadFunctionNamesWtThreadLocal = new HashSet<>();

	private Set<String> currentNewNonThreadFunctionNamesWtThreadLocal = new HashSet<>();

	private Set<String> nonThreadFunctionNamesWtThreadLocal = new HashSet<>();

	private Set<FunctionDefinitionNode> nonThreadFunctionsWtThreadLocal = new HashSet<>();

	private Set<VariableDeclarationNode> shared_variables = new HashSet<>();

	/* ****************************** Constructor ************************** */
	/**
	 * Creates a new instance of MPITransformer.
	 * 
	 * @param astFactory
	 *            The ASTFactory that will be used to create new nodes.
	 */
	public Pthread2CIVLWorker(ASTFactory astFactory) {
		super(Pthread2CIVLTransformer.LONG_NAME, astFactory);
		this.identifierPrefix = "$pthreads_";
		newNonThreadFunctionNamesWtSyncCalls.add(PTHREAD_COND_WAIT);
		// newNonThreadFunctionNamesWtSyncCalls.add(PTHREAD_EXIT_NEW);
		newNonThreadFunctionNamesWtSyncCalls.add(PTHREAD_MUTEX_LOCK);
		newNonThreadFunctionNamesWtSyncCalls.add(PTHREAD_SELF);
		nonThreadFunctionNamesWtSyncCalls.add(PTHREAD_COND_WAIT);
		nonThreadFunctionNamesWtSyncCalls.add(PTHREAD_MUTEX_LOCK);
		nonThreadFunctionNamesWtSyncCalls.add(PTHREAD_SELF);

	}

	/* *************************** Private Methods ************************* */

	private VariableDeclarationNode pthread_pool_declaration(
			boolean wtInitializer) {
		TypeNode pthreadPoolType;
		List<ExpressionNode> pthreadPoolCreateArgs;
		ExpressionNode pthreadPoolCreate;

		pthreadPoolType = nodeFactory.newTypedefNameNode(nodeFactory
				.newIdentifierNode(this.newSource("$phtread_pool_t type",
						CParser.IDENTIFIER), PTHREAD_POOL_TYPE), null);
		if (wtInitializer) {
			pthreadPoolCreateArgs = new ArrayList<>(2);
			pthreadPoolCreateArgs.add(this.hereNode());
			pthreadPoolCreateArgs.add(this.identifierExpression(PTHREAD_GPOOL));
			pthreadPoolCreate = nodeFactory.newFunctionCallNode(this.newSource(
					"function call " + PTHREAD_POOL_CREATE, CParser.CALL), this
					.identifierExpression(PTHREAD_POOL_CREATE),
					pthreadPoolCreateArgs, null);
			return this.variableDeclaration(PTHREAD_POOL, pthreadPoolType,
					pthreadPoolCreate);
		} else
			return this.variableDeclaration(PTHREAD_POOL, pthreadPoolType);
	}

	/**
	 * TODO javadocs
	 * 
	 * @param root
	 * @throws SyntaxException
	 */
	private void transformWorker(SequenceNode<BlockItemNode> root)
			throws SyntaxException {
		// getThreadFunctions(root);
		for (String threadFunction : this.threadFunctionNames) {
			this.newNonThreadFunctionNamesWtThreadLocal.remove(threadFunction);
			this.nonThreadFunctionNamesWtThreadLocal.remove(threadFunction);
		}
		for (BlockItemNode node : root) {
			if (node == null)
				continue;
			if (node instanceof FunctionDefinitionNode) {
				// if (config.svcomp()) {
				process_shared_variable_access((FunctionDefinitionNode) node);
				process_thread_functions((FunctionDefinitionNode) node);
				// process_VERIFIER_function_calls((FunctionDefinitionNode)
				// node);
				// }
				process_pthread_exits((FunctionDefinitionNode) node);
				// process_pthread_sync_calls((FunctionDefinitionNode) node);
			}
			// else if (/*
			// * config.svcomp() &&
			// */node instanceof FunctionDeclarationNode) {
			// process_VERIFIER_functions((FunctionDeclarationNode) node);
			// }
		}
		while (!this.newNonThreadFunctionNamesWtSyncCalls.isEmpty()
				|| !this.newNonThreadFunctionNamesWtThreadLocal.isEmpty()) {
			// currentNewNonThreadFunctionsWtSyncCalls = new HashSet<>(
			// newNonThreadFunctionsWtSyncCalls);
			currentNewNonThreadFunctionNamesWtSyncCalls = new HashSet<>(
					newNonThreadFunctionNamesWtSyncCalls);
			// newNonThreadFunctionsWtSyncCalls.clear();
			newNonThreadFunctionNamesWtSyncCalls.clear();

			this.currentNewNonThreadFunctionNamesWtThreadLocal = new HashSet<>(
					this.newNonThreadFunctionNamesWtThreadLocal);
			this.newNonThreadFunctionNamesWtThreadLocal.clear();
			for (ASTNode node : root.children()) {
				if (node == null)
					continue;
				if (node instanceof FunctionDefinitionNode) {
					process_pthread_sync_calls_thread_locals((FunctionDefinitionNode) node);
				}
			}
		}
		process_nonThread_functions_wt_syncCalls();
		process_nonThread_functions_wt_thread_locals();
		if (this.syncCallFunctionNames.size() > 0)
			process_function_call_of_functionsWtSyncCalls(root);
		// if (config.svcomp())
		// translateNode(root);
	}

	private void process_shared_variable_access(ASTNode node) {
		if (node instanceof ExpressionStatementNode) {
			this.transformAccess2SharedVariables((ExpressionStatementNode) node);
		} else {
			for (ASTNode child : node.children()) {
				if (child != null)
					process_shared_variable_access(child);
			}
		}
	}

	private void process_function_call_of_functionsWtSyncCalls(ASTNode root) {
		for (ASTNode node : root.children()) {
			if (node == null)
				continue;
			if (node instanceof FunctionCallNode) {
				FunctionCallNode call = (FunctionCallNode) node;
				ExpressionNode function = call.getFunction();

				if (function instanceof IdentifierExpressionNode) {
					String funcName = ((IdentifierExpressionNode) function)
							.getIdentifier().name();

					if (this.syncCallFunctionNames.contains(funcName)) {
						call.getArguments().addSequenceChild(
								this.identifierExpression(PTHREAD_POOL));
					}
				}
			}
			process_function_call_of_functionsWtSyncCalls(node);
		}
	}

	private void process_nonThread_functions_wt_syncCalls() {
		Iterator<FunctionDefinitionNode> iterator = this.nonThreadFunctionsWtSyncCalls
				.iterator();

		while (iterator.hasNext()) {
			FunctionDefinitionNode function = iterator.next();

			// function.getTypeNode()
			// .getParameters()
			// .addSequenceChild(
			// this.variableDeclaration(PTHREAD_POOL, nodeFactory
			// .newTypedefNameNode(nodeFactory
			// .newIdentifierNode(this.newSource(
			// "$phtread_pool_t type",
			// CParser.IDENTIFIER),
			// PTHREAD_POOL_TYPE), null)));
			FunctionTypeNode funcType = function.getTypeNode();
			VariableDeclarationNode pthread_pool_param = this
					.pthread_pool_declaration(false);

			if (hasVoidParameter(funcType))
				funcType.getParameters()
						.setSequenceChild(0, pthread_pool_param);
			else
				funcType.getParameters().addSequenceChild(pthread_pool_param);
		}
	}

	private boolean hasVoidParameter(FunctionTypeNode type) {
		if (type.getParameters().numChildren() == 1) {
			TypeNode parameterType = type.getParameters().getSequenceChild(0)
					.getTypeNode();

			if (parameterType.kind() == TypeNodeKind.VOID) {
				return true;
			}
		}
		return false;
	}

	private void process_nonThread_functions_wt_thread_locals() {
		Iterator<FunctionDefinitionNode> iterator = this.nonThreadFunctionsWtThreadLocal
				.iterator();

		while (iterator.hasNext()) {
			FunctionDefinitionNode function = iterator.next();
			// function.getTypeNode()
			// .getParameters()
			// .addSequenceChild(
			// this.variableDeclaration(PTHREAD_POOL, nodeFactory
			// .newTypedefNameNode(nodeFactory
			// .newIdentifierNode(this.newSource(
			// "$phtread_pool_t type",
			// CParser.IDENTIFIER),
			// PTHREAD_POOL_TYPE), null)));
			FunctionTypeNode funcType = function.getTypeNode();

			if (this.threadFunctionNames.contains(function.getName()))
				continue;
			for (VariableDeclarationNode threadLocalVar : this.thread_local_variable_declarations) {
				VariableDeclarationNode newParameter = threadLocalVar.copy();

				newParameter.setThreadLocalStorage(false);
				if (newParameter.getInitializer() != null)
					newParameter.setInitializer(null);
				funcType.getParameters().addSequenceChild(newParameter);
			}
		}
	}

	/**
	 * modify the function definition to take an extra argument: $pthread_pool_t
	 * pthread_pool
	 * 
	 * @param funcDef
	 */
	@SuppressWarnings("unused")
	private void process_sync_call_thread_local_function(
			FunctionDefinitionNode funcDef) {
		FunctionTypeNode funcType = funcDef.getTypeNode();
		VariableDeclarationNode pthread_pool_param = this
				.pthread_pool_declaration(false);

		funcType.getParameters().addSequenceChild(pthread_pool_param);
		// if (!this.funcList.contains(funcDef.getName()))
		// syncCallFunctionNames.add(funcDef.getName());
	}

	private void process_pthread_sync_calls_thread_locals(
			FunctionDefinitionNode node) {
		process_pthread_sync_calls_thread_locals(node, node);
	}

	private void process_pthread_sync_calls_thread_locals(
			FunctionDefinitionNode funcDef, ASTNode node) {
		for (ASTNode child : node.children()) {
			if (child == null)
				continue;
			if (child instanceof FunctionCallNode) {
				process_pthread_sync_call_and_thread_local_work(funcDef,
						(FunctionCallNode) child);
			}
			process_pthread_sync_calls_thread_locals(funcDef, child);
		}
	}

	/**
	 * transforms pthread_mutex_lock(mutex) to pthread_mutex_lock(mutex,
	 * _pthread_pool) and similar for pthread_cond_wait();
	 * 
	 * @param node
	 */
	private void process_pthread_sync_call_and_thread_local_work(
			FunctionDefinitionNode funcDef, FunctionCallNode node) {
		ExpressionNode function = node.getFunction();
		boolean hasSyncCall = false, hasThreadLocalCall = false;

		if (function instanceof IdentifierExpressionNode) {
			String calleeName = ((IdentifierExpressionNode) function)
					.getIdentifier().name();

			if (this.currentNewNonThreadFunctionNamesWtSyncCalls
					.contains(calleeName)) {
				hasSyncCall = true;
			} else if (this.currentNewNonThreadFunctionNamesWtThreadLocal
					.contains(calleeName)) {
				hasThreadLocalCall = true;
			}
			if (calleeName.equals(PTHREAD_MUTEX_LOCK)
					|| calleeName.equals(PTHREAD_COND_WAIT)
					|| calleeName.equals(PTHREAD_SELF)) {
				((IdentifierExpressionNode) function).getIdentifier().setName(
						"$" + calleeName);
			}
			if (hasSyncCall) {
				String funcName = funcDef.getName();

				node.getArguments().addSequenceChild(
						this.identifierExpression(PTHREAD_POOL));
				if (!this.threadFunctionNames.contains(funcName)
						&& !this.nonThreadFunctionNamesWtSyncCalls
								.contains(funcName)) {
					nonThreadFunctionsWtSyncCalls.add(funcDef);
					nonThreadFunctionNamesWtSyncCalls.add(funcName);
					// this.newNonThreadFunctionsWtSyncCalls.add(funcDef);
					this.newNonThreadFunctionNamesWtSyncCalls.add(funcName);
				}
			}
			if (hasThreadLocalCall) {
				String funcName = funcDef.getName();

				for (VariableDeclarationNode threadLocalVar : this.thread_local_variable_declarations) {
					node.getArguments()
							.addSequenceChild(
									this.identifierExpression(threadLocalVar
											.getName()));
				}
				if (!this.threadFunctionNames.contains(funcName)
						&& !this.nonThreadFunctionNamesWtThreadLocal
								.contains(funcName)) {
					this.nonThreadFunctionNamesWtThreadLocal.add(funcName);
					this.newNonThreadFunctionNamesWtThreadLocal.add(funcName);
					this.nonThreadFunctionsWtThreadLocal.add(funcDef);
				}
			}
		}
	}

	/**
	 * Insert pthread pool creation at the beginning of pthread functions
	 * 
	 * @param node
	 */
	private void process_thread_functions(FunctionDefinitionNode node) {
		String name = node.getName();

		if (this.threadFunctionNames.contains(name)) {
			CompoundStatementNode body = node.getBody();
			List<BlockItemNode> newBodyNodes = new LinkedList<>();
			VariableDeclarationNode pthreadPoolVar = this
					.pthread_pool_declaration(true);

			body.remove();
			newBodyNodes.add(pthreadPoolVar);
			for (VariableDeclarationNode threadLocalVar : this.thread_local_variable_declarations) {
				newBodyNodes.add(threadLocalVar.copy());
			}
			newBodyNodes.add(body);
			node.setBody(this.nodeFactory.newCompoundStatementNode(
					body.getSource(), newBodyNodes));
		}
	}

	private void transformAccess2SharedVariables(
			ExpressionStatementNode expressionStatement) {
		int index = expressionStatement.childIndex();
		ASTNode parent = expressionStatement.parent();

		ExpressionNode expression = expressionStatement.getExpression();

		if (expression instanceof OperatorNode) {
			OperatorNode operatorNode = (OperatorNode) expression;

			if (operatorNode.getOperator() == Operator.ASSIGN) {
				ExpressionNode rhs = operatorNode.getArgument(1);
				ExpressionNode lhs = operatorNode.getArgument(0);
				List<BlockItemNode> newItems = null;// =
													// transform_access_to_shared_varaibles(rhs);

				if (!(lhs instanceof IdentifierExpressionNode)) {
					newItems = breakAtomicity(lhs, rhs);
				}
				// List<BlockItemNode> newItems =
				// transform_access_to_shared_varaibles(rhs);
				//
				// if (newItems.size() <= 0) {
				// ExpressionNode lhs = operatorNode.getArgument(0);
				//
				// if (!(lhs instanceof IdentifierExpressionNode)) {
				// newItems = breakAtomicity(lhs, rhs);
				// }
				// }
				if (newItems != null && newItems.size() > 0) {
					expressionStatement.remove();
					newItems.add(expressionStatement);
					parent.setChild(index, this.nodeFactory
							.newCompoundStatementNode(
									expressionStatement.getSource(), newItems));
				}
			}
		}
	}

	private List<BlockItemNode> breakAtomicity(ExpressionNode lhs,
			ExpressionNode rhs) {
		List<BlockItemNode> result = new LinkedList<>();

		if (rhs.equiv(lhs)) {
			String tmpName = this.newUniqueIdentifier("tmp");
			VariableDeclarationNode tmpVariable = this.variableDeclaration(
					tmpName, this.typeNode(rhs.getType()), rhs.copy());

			rhs.parent().setChild(rhs.childIndex(),
					this.identifierExpression(tmpName));
			result.add(tmpVariable);
		} else {
			for (ASTNode child : rhs.children()) {
				if (child != null && (child instanceof ExpressionNode)) {
					List<BlockItemNode> subResult = breakAtomicity(lhs,
							(ExpressionNode) child);

					result.addAll(subResult);
				}
			}
		}
		return result;
	}

	// private List<BlockItemNode> transform_access_to_shared_varaibles(
	// ASTNode node) {
	// List<BlockItemNode> result = new LinkedList<>();
	//
	// if (node instanceof IdentifierExpressionNode) {
	// IdentifierExpressionNode identiferExpression = (IdentifierExpressionNode)
	// node;
	// VariableDeclarationNode replace =
	// process_identifier_expression(identiferExpression);
	//
	// if (replace != null) {
	// result.add(replace);
	// }
	// } else {
	// for (ASTNode child : node.children()) {
	// if (child == null)
	// continue;
	//
	// List<BlockItemNode> subResult =
	// transform_access_to_shared_varaibles(child);
	//
	// result.addAll(subResult);
	// }
	// }
	// return result;
	// }

	// private VariableDeclarationNode process_identifier_expression(
	// IdentifierExpressionNode identifier) {
	// Entity entity = identifier.getIdentifier().getEntity();
	//
	// if (entity instanceof Variable) {
	// VariableDeclarationNode variableDeclaration = ((Variable) entity)
	// .getDefinition();
	//
	// if (this.shared_variables.contains(variableDeclaration)) {
	// String tmpName = this.newUniqueIdentifier("tmp");
	// VariableDeclarationNode tmpVariable = this.variableDeclaration(
	// tmpName, variableDeclaration.getTypeNode().copy(),
	// identifier.copy());
	//
	// identifier.parent().setChild(identifier.childIndex(),
	// this.identifierExpression(tmpName));
	// return tmpVariable;
	// }
	// }
	// return null;
	// }

	// /**
	// * Processes function calls starting with __VERIFIER_, which are special
	// * functions of the SV-COMP.
	// *
	// * @param node
	// * The function definition node whose body is to be searched for
	// * __VERIFIER_ calls for transformation.
	// * @throws SyntaxException
	// */
	// private void process_VERIFIER_function_calls(FunctionDefinitionNode node)
	// throws SyntaxException {
	// process_VERIFIER_function_call_worker(node);
	// }

	// /**
	// * TODO documentation about VERIFIER_nondet_int and VERIFIER_atomic
	// * Transforms __VERIFIER_ function calls into their corresponding
	// * counterparts:
	// * <ul>
	// * <li>VERIFIER_nondet_int: abstract integer function</li>
	// * <li>VERIFIER_atomic: atomic function</li>
	// * </ul>
	// *
	// * @param node
	// * ASTNode to be be checked for a VERIFIER
	// *
	// */
	// private void process_VERIFIER_function_call_worker(ASTNode node)
	// throws SyntaxException {
	// if (node instanceof FunctionCallNode) {
	// FunctionCallNode funcCall = (FunctionCallNode) node;
	// ExpressionNode function = funcCall.getFunction();
	//
	// if (function.expressionKind() == ExpressionKind.IDENTIFIER_EXPRESSION) {
	// IdentifierExpressionNode funcName = (IdentifierExpressionNode) function;
	// String name = funcName.getIdentifier().name();
	//
	// if (name.equals(VERIFIER_NONDET_INT)
	// || name.equals(VERIFIER_NONDET_UINT)) {
	// ExpressionNode newArg = nodeFactory.newIntegerConstantNode(
	// funcName.getSource(),
	// String.valueOf(numberOfNondetCall));
	//
	// this.numberOfNondetCall++;
	// funcCall.setArguments(nodeFactory.newSequenceNode(
	// funcName.getSource(), "Actual Arguments",
	// Arrays.asList(newArg)));
	// }
	// }
	// } else if (node instanceof FunctionDefinitionNode) {
	// IdentifierNode functionName = ((FunctionDefinitionNode) node)
	// .getIdentifier();
	// if (functionName.name().startsWith(VERIFIER_ATOMIC)) {
	// CompoundStatementNode tmp = ((FunctionDefinitionNode) node)
	// .getBody().copy();
	// Source source = tmp.getSource();
	// AtomicNode newAtomicBlock = nodeFactory.newAtomicStatementNode(
	// source, false, tmp);
	// CompoundStatementNode block = nodeFactory
	// .newCompoundStatementNode(source,
	// Arrays.asList((BlockItemNode) newAtomicBlock));
	// ((FunctionDefinitionNode) node).setBody(block);
	// }
	// for (ASTNode child : node.children()) {
	// if (child != null)
	// process_VERIFIER_function_call_worker(child);
	// }
	// } else {
	// for (ASTNode child : node.children()) {
	// if (child != null)
	// process_VERIFIER_function_call_worker(child);
	// }
	// }
	// }

	// /**
	// * Inserts an abstract function node in place of VERIFIER_nondet_int
	// *
	// * @param function
	// * Node to be checked and converted for VERIFIER function
	// *
	// */
	// private void process_VERIFIER_functions(FunctionDeclarationNode function)
	// {
	// IdentifierNode functionName = function.getIdentifier();
	//
	// if (functionName.name().equals(VERIFIER_NONDET_UINT)
	// || functionName.name().equals(VERIFIER_NONDET_INT)) {
	// FunctionTypeNode funcTypeNode = function.getTypeNode();
	// FunctionDeclarationNode abstractNode;
	//
	// funcTypeNode = nodeFactory
	// .newFunctionTypeNode(
	// funcTypeNode.getSource(),
	// funcTypeNode.getReturnType().copy(),
	// nodeFactory.newSequenceNode(this.newSource(
	// "formal parameter declarations of "
	// + functionName.name(),
	// CParser.DECLARATION_LIST),
	// "Formal Parameters",
	// Arrays.asList(this.variableDeclaration(
	// "seed",
	// this.basicType(BasicTypeKind.INT)))),
	// false);
	// abstractNode = nodeFactory.newAbstractFunctionDefinitionNode(
	// function.getSource(), function.getIdentifier().copy(),
	// funcTypeNode, null, 0);
	// function.parent().setChild(function.childIndex(), abstractNode);
	// }
	// }

	// /**
	// * Translates nodes if they meet one of various specific cases
	// *
	// * @param node
	// * Node to be translated
	// *
	// */
	// private void translateNode(ASTNode node) {
	// if (node instanceof LabeledStatementNode) {
	// LabeledStatementNode labelStatement = (LabeledStatementNode) node;
	// LabelNode labelNode = labelStatement.getLabel();
	//
	// if (labelNode instanceof OrdinaryLabelNode) {
	// OrdinaryLabelNode label = (OrdinaryLabelNode) labelNode;
	// String name = label.getName();
	// if (name.equals(ERROR))
	// labelStatement.setChild(1,
	// this.assertFalse(labelStatement.getSource()));
	// }
	// // } else if (node instanceof ExpressionStatementNode) {
	// // ExpressionNode expression = ((ExpressionStatementNode) node)
	// // .getExpression();
	// // StatementNode newStatementNode = null;
	// //
	// // if (expression.expressionKind() == ExpressionKind.FUNCTION_CALL)
	// // {
	// // FunctionCallNode functionCall = (FunctionCallNode) expression;
	// // ExpressionNode functionName = functionCall.getFunction();
	// //
	// // if (functionName.expressionKind() ==
	// // ExpressionKind.IDENTIFIER_EXPRESSION) {
	// // String name = ((IdentifierExpressionNode) functionName)
	// // .getIdentifier().name();
	// //
	// // switch (name) {
	// // case VERIFIER_ASSERT:
	// // newStatementNode = this.assertNode(functionCall
	// // .getSource(), functionCall.getArgument(0)
	// // .copy());
	// // break;
	// // case VERIFIER_ASSUME:
	// // newStatementNode = this.assumeNode(functionCall
	// // .getArgument(0).copy());
	// // break;
	// // default:
	// // }
	// // }
	// // if (newStatementNode != null)
	// // node.parent().setChild(node.childIndex(), newStatementNode);
	// // }
	// } else
	// for (ASTNode child : node.children())
	// if (child != null)
	// this.translateNode(child);
	// }

	// private StatementNode assertNode(Source mySource, ExpressionNode
	// expression) {
	// return nodeFactory.newExpressionStatementNode(this.functionCall(
	// mySource, ASSERT, Arrays.asList(expression)));
	// }

	// /**
	// * Creates a StatementNode for error report: $assert $false.
	// *
	// * @param mySource
	// *
	// * @return
	// */
	// private StatementNode assertFalse(Source mySource) {
	// ExpressionNode falseExpression = this.booleanConstant(false);
	//
	// return assertNode(mySource, falseExpression);
	// }

	/**
	 * TODO javadocs
	 * 
	 * @param function
	 * @param threadList
	 * @throws SyntaxException
	 */
	private void process_pthread_exits(FunctionDefinitionNode function)
			throws SyntaxException {
		String name = function.getName();
		TypeNode returnType = function.getTypeNode().getReturnType();
		boolean isMain = false;

		if (name.equals(GENERATED_MAIN)
				|| (!this.fixedMain && name.equals(MAIN))) {
			isMain = true;
			this.fixedMain = true;
		}
		if (isMain) {
			ExpressionNode ZERO = this.integerConstant(0);
			if (!hasReturn(function)) {
				if (returnType.getType().kind() == TypeKind.VOID)
					function.getBody().addSequenceChild(
							nodeFactory.newReturnNode(this.newSource(
									"return statement", CParser.RETURN), null));
				else
					function.getBody().addSequenceChild(
							nodeFactory.newReturnNode(this.newSource(
									"return statement", CParser.RETURN), ZERO));
			}
			process_pthread_exit(function, true);
			// return;
		}
		if ((this.isVoidPointerType(returnType) && this.threadFunctionNames
				.contains(name))) {
			String pthread_exit_name = isMain ? PTHREAD_EXIT_MAIN_NEW
					: PTHREAD_EXIT_NEW;

			if (!isMain
					&& function.getTypeNode().getParameters().numChildren() == 0) {
				function.getTypeNode().setParameters(
						nodeFactory.newSequenceNode(this.newSource(
								"parameter declaration of "
										+ function.getName(),
								CParser.DECLARATION_LIST), "parameters", Arrays
								.asList(this.variableDeclaration("arg",
										nodeFactory.newPointerTypeNode(this
												.newSource("type void *",
														CParser.TYPE), this
												.voidType())))));
			}
			ExpressionNode nullNode = nodeFactory.newCastNode(
					this.newSource("cast expression", CParser.CAST),
					nodeFactory.newPointerTypeNode(
							this.newSource("type void *", CParser.TYPE),
							this.voidType()), this.integerConstant(0));
			// ExpressionNode isMainArg = this.booleanConstant(false);
			FunctionCallNode newPthreadExit = nodeFactory.newFunctionCallNode(
					this.newSource("function call " + pthread_exit_name,
							CParser.CALL),
					this.identifierExpression(pthread_exit_name),
					isMain ? Arrays.asList(nullNode) : Arrays.asList(nullNode,
							this.identifierExpression(this.newSource(
									PTHREAD_POOL, CParser.IDENTIFIER),
									PTHREAD_POOL)), null);
			StatementNode pthreadExit = nodeFactory
					.newExpressionStatementNode(newPthreadExit);
			function.getBody().addSequenceChild(pthreadExit);
			process_pthread_exit(function, isMain);
			fix_duplicated_pthread_exits(function, isMain);
		}
	}

	private void fix_duplicated_pthread_exits(FunctionDefinitionNode function,
			boolean isMain) {
		// function.prettyPrint(System.out);
		this.reduceDuplicateNode(function, new NodePredicate() {
			@Override
			public boolean holds(ASTNode node) {
				return isFunctionCallStatementNodeOf(node, PTHREAD_EXIT_NEW);
			}

		});

		// CompoundStatementNode bodyNode = function.getBody();
		// BlockItemNode newBody = fix_duplicated_pthread_exits_worker(bodyNode,
		// isMain);
		//
		// if (newBody instanceof CompoundStatementNode)
		// function.setBody((CompoundStatementNode) newBody);
		// else
		// function.setBody(nodeFactory.newCompoundStatementNode(
		// bodyNode.getSource(), Arrays.asList(newBody)));
	}

	@SuppressWarnings("unused")
	private BlockItemNode fix_duplicated_pthread_exits_worker(
			CompoundStatementNode block, boolean isMain) {
		String pthread_exit_name = isMain ? PTHREAD_EXIT_MAIN_NEW
				: PTHREAD_EXIT_NEW;
		int lastIndex = -1;
		List<BlockItemNode> newItems = new LinkedList<>();

		for (int i = 0; i < block.numChildren(); i++) {
			BlockItemNode child = block.getSequenceChild(i);

			if (child == null)
				continue;
			if (child instanceof CompoundStatementNode) {
				BlockItemNode newChild = fix_duplicated_pthread_exits_worker(
						(CompoundStatementNode) child, isMain);

				block.setChild(i, newChild);
				child = newChild;
			}
			if (isFunctionCallStatementNodeOf(child, pthread_exit_name)) {
				if (lastIndex >= 0)
					block.removeChild(i);
				else
					lastIndex = i;
			}
		}
		for (BlockItemNode item : block) {
			if (item == null)
				continue;
			item.remove();
			newItems.add(item);
		}
		if (newItems.size() > 1)
			return nodeFactory.newCompoundStatementNode(block.getSource(),
					newItems);
		else if (newItems.size() == 1)
			return newItems.get(0);
		else
			return null;
	}

	private boolean isFunctionCallStatementNodeOf(ASTNode node, String function) {
		if (node instanceof ExpressionStatementNode) {
			ExpressionNode expression = ((ExpressionStatementNode) node)
					.getExpression();

			if (expression instanceof FunctionCallNode) {
				ExpressionNode functionNode = ((FunctionCallNode) expression)
						.getFunction();

				if (functionNode instanceof IdentifierExpressionNode) {
					return ((IdentifierExpressionNode) functionNode)
							.getIdentifier().name().equals(function);
				}
			}
		}
		return false;
	}

	/**
	 * In main(), translate pthread_exit(arg) to pthread_exit(arg, true); in
	 * other function, translate pthread_exit(arg) to pthread_exit(arg, false).
	 * 
	 * @param function
	 * @throws SyntaxException
	 */
	private void process_pthread_exit(FunctionDefinitionNode function,
			boolean isMain) throws SyntaxException {
		process_pthread_exit_worker(function, isMain);
	}

	/**
	 * TODO javadoc
	 * 
	 * @param node
	 * @param isMain
	 * @throws SyntaxException
	 */
	private void process_pthread_exit_worker(ASTNode node, boolean isMain)
			throws SyntaxException {
		for (ASTNode child : node.children()) {
			if (child == null)
				continue;
			if (child instanceof FunctionCallNode) {
				FunctionCallNode funcCall = (FunctionCallNode) child;
				ExpressionNode funcName = funcCall.getFunction();

				if (funcName instanceof IdentifierExpressionNode) {
					IdentifierExpressionNode name = (IdentifierExpressionNode) funcName;
					String nameString = name.getIdentifier().name();

					if (nameString.equals(PTHREAD_EXIT)) {
						// ExpressionNode isMainArg =
						// this.booleanConstant(isMain);
						ExpressionNode oldArg = funcCall.getArgument(0);
						SequenceNode<ExpressionNode> newArgs;

						if (!isMain) {
							name.getIdentifier().setName(PTHREAD_EXIT_NEW);
							oldArg.parent().removeChild(oldArg.childIndex());
							newArgs = nodeFactory
									.newSequenceNode(
											this.newSource(
													"actual parameter list of "
															+ nameString,
													CParser.ARGUMENT_LIST),
											"Actual parameters",
											Arrays.asList(
													oldArg,
													this.identifierExpression(
															this.newSource(
																	PTHREAD_POOL,
																	CParser.IDENTIFIER),
															PTHREAD_POOL)));
							funcCall.setArguments(newArgs);
						} else if (!exitMainDone) {
							this.exitMainDone = true;
							name.getIdentifier().setName(PTHREAD_EXIT_MAIN_NEW);
						}
					}
				}
			} else if (child instanceof ReturnNode
					&& (!isMain || !exitMainDone)) {
				// ExpressionNode isMainArg = this.booleanConstant(isMain);
				String pthread_exit_name = isMain ? PTHREAD_EXIT_MAIN_NEW
						: PTHREAD_EXIT_NEW;
				ExpressionNode returnExpr = ((ReturnNode) child)
						.getExpression();
				ExpressionNode newExpr = returnExpr == null ? this
						.nullPointerNode() : returnExpr.copy();

				if (isMain)
					exitMainDone = true;
				FunctionCallNode newPthreadExit = nodeFactory
						.newFunctionCallNode(
								this.newSource("function call of "
										+ pthread_exit_name, CParser.CALL),
								this.identifierExpression(pthread_exit_name),
								isMain ? Arrays.asList(nullPointerNode())
										: Arrays.asList(
												newExpr,
												this.identifierExpression(
														this.newSource(
																PTHREAD_POOL,
																CParser.IDENTIFIER),
														PTHREAD_POOL)), null);
				StatementNode pthreadExit = nodeFactory
						.newExpressionStatementNode(newPthreadExit);

				child.parent().setChild(child.childIndex(), pthreadExit);
			} else {
				process_pthread_exit_worker(child, isMain);
			}
		}
	}

	private ExpressionNode nullPointerNode() throws SyntaxException {
		return nodeFactory.newCastNode(
				this.newSource("cast expression", CParser.CAST),
				nodeFactory.newPointerTypeNode(
						this.newSource("type void *", CParser.TYPE),
						this.voidType()), this.integerConstant(0));
	}

	// TODO: what is this function trying to do for pthread_create? What kind of
	// transformation and why?
	/**
	 * find out all functions used for pthread_create, i.e., all functions that
	 * will be executed in a thread.
	 * 
	 * @param node
	 */
	private void getThreadFunctions(ASTNode node) {
		for (ASTNode child : node.children()) {
			if (child == null)
				continue;
			if (child instanceof FunctionCallNode) {
				FunctionCallNode funcCall = (FunctionCallNode) child;
				ExpressionNode funcName = funcCall.getFunction();
				if (funcName instanceof IdentifierExpressionNode) {
					IdentifierExpressionNode named = (IdentifierExpressionNode) funcName;
					String nameString = named.getIdentifier().name();
					if (nameString.equals(PTHREAD_CREATE)) {
						ExpressionNode arg = funcCall.getArgument(2);

						if (arg instanceof OperatorNode) {
							OperatorNode argOp = (OperatorNode) arg;
							IdentifierExpressionNode threadName = (IdentifierExpressionNode) argOp
									.getArgument(0);

							threadFunctionNames.add(threadName.getIdentifier()
									.name());
						} else if (arg instanceof IdentifierExpressionNode) {
							IdentifierExpressionNode threadName = (IdentifierExpressionNode) funcCall
									.getArgument(2);

							threadFunctionNames.add(threadName.getIdentifier()
									.name());
						} else if (arg instanceof CastNode) {
							IdentifierExpressionNode threadName = (IdentifierExpressionNode) ((CastNode) arg)
									.getArgument();

							threadFunctionNames.add(threadName.getIdentifier()
									.name());
						} else {
							throw new CIVLUnimplementedFeatureException(
									"unimplemented handling of Pthread transformer for expression of "
											+ arg.expressionKind()
											+ " kind as the function pointer argument of pthread_create()");
						}
					}
				}
			} else {
				getThreadFunctions(child);
			}
		}
	}

	@SuppressWarnings("unused")
	private ReturnNode returnNull() throws SyntaxException {
		ExpressionNode nullNode = nodeFactory.newCastNode(
				this.newSource("cast expression", CParser.CAST),
				nodeFactory.newPointerTypeNode(
						this.newSource("type void *", CParser.TYPE),
						this.voidType()), this.integerConstant(0));

		return nodeFactory.newReturnNode(
				this.newSource("return statement", CParser.RETURN), nullNode);
	}

	/**
	 * 
	 * @param type
	 * @return
	 */
	private boolean isVoidPointerType(TypeNode type) {
		if (type.kind() == TypeNodeKind.POINTER) {
			PointerTypeNode pointer = (PointerTypeNode) type;

			if (pointer.referencedType().kind() == TypeNodeKind.VOID)
				return true;
		}
		return false;
	}

	/*
	 * 
	 */

	private boolean hasReturn(ASTNode node) {
		if (node instanceof ReturnNode) {
			return true;
		} else {
			for (ASTNode child : node.children()) {
				if (child != null) {
					if (hasReturn(child)) {
						return true;
					}
				}
			}
		}
		return false;
	}

	// private void process_thread_local(SequenceNode<BlockItemNode> root,
	// Collection<SourceFile> sourceFiles) throws SyntaxException {
	// if (this.thread_local_variable_declarations.size() > 0) {
	// AST ast = astFactory.newAST(root, sourceFiles);
	//
	// Analysis.performStandardAnalysis(
	// Configurations.newMinimalConfiguration(), ast);
	// dd
	// }
	// }

	private void check_thread_local_accesses(SequenceNode<BlockItemNode> root) {
		for (BlockItemNode item : root) {
			if (item == null)
				continue;
			if (item instanceof VariableDeclarationNode) {
				VariableDeclarationNode varDecl = (VariableDeclarationNode) item;

				if (varDecl.hasThreadLocalStorage())
					this.thread_local_variable_declarations.add(varDecl);
				else {
					if (!varDecl.getTypeNode().isInputQualified())
						this.shared_variables.add(varDecl.getEntity()
								.getDefinition());
				}
			} else if (item instanceof FunctionDefinitionNode) {
				if (thread_local_variable_declarations.size() > 0) {
					FunctionDefinitionNode function = (FunctionDefinitionNode) item;

					if (!function.getName().equals("main")
							&& !function.getName().equals("_gen_main")
							&& has_reference_to_thread_local_variables(function
									.getBody())) {
						this.newNonThreadFunctionNamesWtThreadLocal
								.add(function.getName());
						this.nonThreadFunctionsWtThreadLocal.add(function);
						this.nonThreadFunctionNamesWtThreadLocal.add(function
								.getName());
					}
				}
			}
		}
	}

	private boolean has_reference_to_thread_local_variables(ASTNode node) {
		if (node instanceof IdentifierExpressionNode) {
			IdentifierExpressionNode identifier = (IdentifierExpressionNode) node;
			Entity entity = identifier.getIdentifier().getEntity();

			if (entity instanceof Variable) {
				Variable variable = (Variable) entity;

				if (this.thread_local_variable_declarations.contains(variable
						.getDefinition())) {
					return true;
				}
			}
		} else {
			for (ASTNode child : node.children()) {
				if (child == null)
					continue;
				if (this.has_reference_to_thread_local_variables(child))
					return true;
			}
		}
		return false;
	}

	/* ********************* Methods From BaseTransformer ****************** */

	@Override
	public AST transform(AST ast) throws SyntaxException {
		SequenceNode<BlockItemNode> root = ast.getRootNode();

		assert this.astFactory == ast.getASTFactory();
		assert this.nodeFactory == astFactory.getNodeFactory();

		check_thread_local_accesses(root);
		this.getThreadFunctions(root);
		ast.release();
		transformWorker(root);
		this.completeSources(root);
		AST result = astFactory.newAST(root, ast.getSourceFiles());
		// result.prettyPrint(System.out, false);
		return result;
	}
}