ModelExtractor.java

package edu.udel.cis.vsl.tass.front.minimp;

import java.io.IOException;

import edu.udel.cis.vsl.tass.config.CompareConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration.Frontend;
import edu.udel.cis.vsl.tass.config.VerifyConfiguration;
import edu.udel.cis.vsl.tass.front.minimp.ast.misc.AST;
import edu.udel.cis.vsl.tass.front.minimp.parser.TreeParser;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;

public class ModelExtractor {

	private ModelBuilder builder;

	private RunConfiguration configuration;

	public ModelExtractor(RunConfiguration configuration) {
		this.configuration = configuration;
		builder = new ModelBuilder(configuration);
	}

	public ModelBuilder builder() {
		return builder;
	}

	public ModelIF extract() throws IOException, SyntaxException {
		VerifyConfiguration configuration = (VerifyConfiguration) this.configuration;

		edu.udel.cis.vsl.tass.front.FrontendIF frontend = null;
		if (configuration.getFrontend() == null
				|| configuration.getFrontend() == Frontend.ANTLR) {
			frontend = new TreeParser(configuration);
		} else if (configuration.getFrontend() == Frontend.CLANG) {
			// frontend = new ClangParser(configuration.sourceFile());
		}
		AST program = frontend.processAST(configuration.sourceFile());
		ModelIF model = builder.buildModel(program);

		return model;
	}

	public ModelPair extractPair() throws IOException, SyntaxException {
		CompareConfiguration configuration = (CompareConfiguration) this.configuration;
		TreeParser parser1 = new TreeParser(configuration.specSourceFile()
				.toString(), configuration, null);
		AST program1 = parser1.processAST();
		TreeParser parser2 = new TreeParser(configuration.implSourceFile()
				.toString(), configuration, program1);
		AST program2 = parser2.processAST();
		ModelIF[] models = builder.buildModel(new AST[] { program1, program2 });
		ModelPair pair = new ModelPair(models[0], models[1]);

		return pair;
	}

	public static ModelIF extractModel(VerifyConfiguration configuration)
			throws IOException, SyntaxException {
		ModelExtractor extractor = new ModelExtractor(configuration);

		return extractor.extract();
	}

	public static ModelPair extractModelPair(CompareConfiguration configuration)
			throws IOException, SyntaxException {
		ModelExtractor extractor = new ModelExtractor(configuration);

		return extractor.extractPair();
	}
}