CommonModelCombiner.java

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

import java.io.PrintStream;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.Map;
import java.util.Set;

import edu.udel.cis.vsl.civl.err.CIVLSyntaxException;
import edu.udel.cis.vsl.civl.model.IF.CIVLFunction;
import edu.udel.cis.vsl.civl.model.IF.CIVLSource;
import edu.udel.cis.vsl.civl.model.IF.Fragment;
import edu.udel.cis.vsl.civl.model.IF.Model;
import edu.udel.cis.vsl.civl.model.IF.ModelCombiner;
import edu.udel.cis.vsl.civl.model.IF.ModelFactory;
import edu.udel.cis.vsl.civl.model.IF.Scope;
import edu.udel.cis.vsl.civl.model.IF.expression.BinaryExpression.BINARY_OPERATOR;
import edu.udel.cis.vsl.civl.model.IF.expression.Expression;
import edu.udel.cis.vsl.civl.model.IF.location.Location;
import edu.udel.cis.vsl.civl.model.IF.statement.CallOrSpawnStatement;
import edu.udel.cis.vsl.civl.model.IF.statement.Statement;
import edu.udel.cis.vsl.civl.model.IF.variable.Variable;

/**
 * A model combiner takes two models and creates a single composite model for
 * comparative symbolic execution.
 * 
 * @author zirkel
 */
public class CommonModelCombiner implements ModelCombiner {

	private ModelFactory factory;

	private boolean debugging = false;

	private PrintStream debugOut = System.out;

	public CommonModelCombiner(ModelFactory factory) {
		this.factory = factory;
	}

	@Override
	public Model combine(Model model0, Model model1) {
		CIVLFunction system;
		CIVLSource source = factory.systemSource();
		Model compositeModel;
		CallOrSpawnStatement spawn0, spawn1;
		Fragment wait0, wait1, systemBody;
		Variable model0proc, model1proc;
		Map<String, Variable> model0outputs, model1outputs;

		system = factory.function(source,
				factory.identifier(factory.systemSource(), "_CIVL_system"),
				new ArrayList<Variable>(), null, null, null);
		// TODO: Combine sources from each model for the composite model
		compositeModel = factory.model(source, system);
		model0.system().setName(
				factory.identifier(model0.getSource(), "_CIVL_system_0"));
		model1.system().setName(
				factory.identifier(model0.getSource(), "_CIVL_system_1"));
		// spawn processes to run both models.
		spawn0 = factory.callOrSpawnStatement(source,
				factory.location(source, system.outerScope()), false,
				factory.functionPointerExpression(source, model0.system()),
				new LinkedList<Expression>(),
				factory.booleanLiteralExpression(source, true));
		model0proc = factory.variable(source, factory.processType(), factory
				.identifier(source, "model0proc"), system.outerScope()
				.numVariables());
		system.outerScope().addVariable(model0proc);
		spawn0.setLhs(factory.variableExpression(source, model0proc));
		systemBody = new CommonFragment(spawn0);
		spawn1 = factory.callOrSpawnStatement(source,
				factory.location(source, system.outerScope()), false,
				factory.functionPointerExpression(source, model1.system()),
				new LinkedList<Expression>(),
				factory.booleanLiteralExpression(source, true));
		model1proc = factory.variable(source, factory.processType(), factory
				.identifier(source, "model1proc"), system.outerScope()
				.numVariables());
		system.outerScope().addVariable(model1proc);
		spawn1.setLhs(factory.variableExpression(source, model1proc));
		systemBody = systemBody.combineWith(new CommonFragment(spawn1));
		// wait on the processes from both models
		wait0 = factory.joinFragment(source,
				factory.location(source, system.outerScope()),
				factory.variableExpression(source, model0proc));
		systemBody = systemBody.combineWith(wait0);
		wait1 = factory.joinFragment(source,
				factory.location(source, system.outerScope()),
				factory.variableExpression(source, model1proc));
		systemBody = systemBody.combineWith(wait1);
		model0outputs = modifyVariables(system.outerScope(), model0, true);
		model1outputs = modifyVariables(system.outerScope(), model1, false);
		model0.system().outerScope().setParent(system.outerScope());
		model1.system().outerScope().setParent(system.outerScope());
		model0.system().setContainingScope(system.outerScope());
		model1.system().setContainingScope(system.outerScope());
		systemBody = systemBody.combineWith(outputAssertions(model0outputs,
				model1outputs));
		systemBody = systemBody.combineWith(factory.returnFragment(source,
				factory.location(source, system.outerScope()), null, system));
		completeFunction(system, systemBody);
		for (CIVLFunction f : model0.functions()) {
			compositeModel.addFunction(f);
		}
		for (CIVLFunction f : model1.functions()) {
			compositeModel.addFunction(f);
		}
		system.setModel(compositeModel);
		staticAnalysis(compositeModel);
		return compositeModel;
	}

	/**
	 * Move the input variables of the model to the specified scope. Rename the
	 * output variables of the model and move them to the target scope
	 * 
	 * @param scope
	 *            The destination scope for input and (renamed) output
	 *            variables.
	 * @param model
	 *            The model whose system function is being modified.
	 * @param isSpec
	 *            True iff this is the spec model (not the impl).
	 * @return Mapping from original output variable names to the corresponding
	 *         variable.
	 */
	private Map<String, Variable> modifyVariables(Scope scope, Model model,
			boolean isSpec) {
		Set<Variable> reducedVariableSet = new HashSet<Variable>();
		Map<String, Variable> outputs = new LinkedHashMap<String, Variable>();
		String outputSuffix;

		if (isSpec) {
			outputSuffix = "_spec";
		} else {
			outputSuffix = "_impl";
		}
		for (Variable v : model.system().outerScope().variables()) {
			if (v.isInput()) {
				if (!isSpec) {
					// Don't add duplicates of the same input.
					if (scope.containsVariable(v.name().name())) {
						// Make this version of the input variable point to the
						// right scope
						v.setScope(scope);
						v.setVid(scope.variable(v.name().name()).vid());
						continue;
					}
				}
				v.setVid(scope.numVariables());
				v.setScope(scope);
				scope.addVariable(v);
			} else if (v.isOutput()) {
				outputs.put(v.name().name(), v);
				v.setVid(scope.numVariables());
				v.setName(factory.identifier(v.getSource(), v.name().name()
						+ outputSuffix));
				v.setScope(scope);
				scope.addVariable(v);
			} else {
				v.setVid(reducedVariableSet.size());
				reducedVariableSet.add(v);
			}
		}
		model.system().outerScope().setVariables(reducedVariableSet);
		return outputs;
	}

	/**
	 * 
	 * @param map0
	 *            The map from output variable names to the spec output
	 *            variables.
	 * @param map1
	 *            The map from output variable names to the impl output
	 *            variables.
	 * @return A fragment consisting of a series of assertions of equality
	 *         between corresponding spec and impl output variables.
	 */
	private Fragment outputAssertions(Map<String, Variable> map0,
			Map<String, Variable> map1) {
		Fragment result = new CommonFragment();
		CIVLSource source = factory.systemSource();

		for (String s : map0.keySet()) {
			Variable v0 = map0.get(s);
			Variable v1 = map1.get(s);
			Statement assertion;

			if (v1 == null) {
				throw new CIVLSyntaxException(
						"For comparing functional equivalence, every output "
								+ "variable in the specification program should "
								+ "have a corresponding output variable of the "
								+ "same name in the implementation.", v0);
			}
			assertion = factory.assertStatement(source, factory.location(
					source, v0.scope()), factory.binaryExpression(source,
					BINARY_OPERATOR.EQUAL,
					factory.variableExpression(source, v0),
					factory.variableExpression(source, v1)));
			result = result.combineWith(new CommonFragment(assertion));
		}
		return result;
	}

	/**
	 * Add all statements and locations to the function.
	 * 
	 * @param function
	 *            The function to be completed.
	 * @param functionBody
	 *            The body of the function.
	 */
	private void completeFunction(CIVLFunction function, Fragment functionBody) {
		ArrayDeque<Location> workingLocations = new ArrayDeque<Location>();
		Location location;

		// start from the start location of the fragment
		workingLocations.add(functionBody.startLocation());
		function.setStartLocation(functionBody.startLocation());
		while (workingLocations.size() > 0) {
			// use first-in-first-out order to traverse locations so that they
			// are in natural order of the location id's
			location = workingLocations.pollFirst();
			function.addLocation(location);
			if (location.getNumOutgoing() > 0) {
				// for each statement in the outgoing set of a location, add
				// itself to function, and add its target location into the
				// working stack if it hasn't been encountered before.
				for (Statement statement : location.outgoing()) {
					Location newLocation = statement.target();

					function.addStatement(statement);
					if (newLocation != null) {
						if (!function.locations().contains(newLocation)) {
							workingLocations.add(newLocation);
						}
					}
				}
			}
		}
	}

	/**
	 * Perform static analysis, including: dereferences, purely local
	 * statements, etc.
	 */
	private void staticAnalysis(Model model) {
		Set<Variable> addressedOfVariables = new HashSet<>();
		// TODO: Figure out the right heap type

		for (CIVLFunction f : model.functions()) {
			f.simplify();
			// identify all purely local variables
			f.purelyLocalAnalysis();
			f.setModel(model);
			for (Statement s : f.statements()) {
				Set<Variable> statementResult = s.variableAddressedOf();

				if (statementResult != null) {
					addressedOfVariables.addAll(statementResult);
				}
				s.setModel(model);
				s.calculateDerefs();
			}
		}
		if (debugging) {
			debugOut.println("Variable addressed of:");
			for (Variable variable : addressedOfVariables) {
				debugOut.print(variable.name() + "-" + variable.scope().id()
						+ ", ");
			}
			debugOut.println();
		}
		for (CIVLFunction f : model.functions()) {
			// purely local statements can only be
			// identified after ALL variables have been
			// checked for being purely local or not
			for (Location loc : f.locations()) {
				loc.computeWritableVariables(addressedOfVariables);
				for (Statement s : loc.outgoing()) {
					s.purelyLocalAnalysis();
				}
			}
		}
		for (CIVLFunction f : model.functions()) {
			// purely local locations that enters an atomic block needs future
			// statements to be checked, thus it can only be
			// identified after ALL statements have been
			// checked for being purely local or not
			for (Location loc : f.locations()) {
				loc.purelyLocalAnalysis();
				factory.setImpactScopeOfLocation(loc);
			}
		}
		model.complete();
	}
}