Libstdlib.java

/**
 * 
 */
package edu.udel.cis.vsl.civl.library.stdlib;

import java.util.HashSet;
import java.util.Set;

import edu.udel.cis.vsl.civl.err.CIVLUnimplementedFeatureException;
import edu.udel.cis.vsl.civl.model.IF.Identifier;
import edu.udel.cis.vsl.civl.model.IF.statement.Statement;
import edu.udel.cis.vsl.civl.semantics.Executor;
import edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor;
import edu.udel.cis.vsl.civl.state.State;
import edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression;

/**
 * Executor for stdlib function calls.
 * 
 * @author zirkel
 * 
 */
public class Libstdlib implements LibraryExecutor {

	// private StateFactoryIF factory;
	// private SymbolicUniverse universe;

	// private Vector<SymbolicType> elementTypes;
	// private SymbolicType heapUnionType;
	// private SymbolicExpression heap;

	/**
	 * Executor for stdlib function calls.
	 */
	public Libstdlib(Executor primaryExecutor) {
		// this.factory = primaryExecutor.stateFactory();
		// this.universe = primaryExecutor.universe();
		// elementTypes = new Vector<SymbolicType>();
		// // TODO: Get the set of malloc'd types from the model.
		// elementTypes.add(universe.booleanType());
		// elementTypes.add(universe.integerType());
		// elementTypes.add(universe.realType());
		// heapUnionType = universe.unionType(universe.stringObject("heap"),
		// elementTypes);
		// heap = universe.array(heapUnionType, new
		// Vector<SymbolicExpression>());
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor#name()
	 */
	@Override
	public String name() {
		return "stdlib";
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor#execute(edu.udel.cis
	 * .vsl.civl.state.State, int,
	 * edu.udel.cis.vsl.civl.model.IF.statement.Statement)
	 */
	@Override
	public State execute(State state, int pid, Statement statement) {
		Identifier name;
		State result = null;

		throw new CIVLUnimplementedFeatureException(
				"stdlib not yet implemented", statement);

		// if (!(statement instanceof CallOrSpawnStatement)) {
		// throw new RuntimeException("Unsupported statement for stdlib: "
		// + statement);
		// }
		// name = ((CallOrSpawnStatement) statement).function().name();
		// if (name.name().equals("malloc")) {
		// // Vector<SymbolicExpression> heapElements = new
		// // Vector<SymbolicExpression>();
		//
		// } else if (name.name().equals("free")) {
		//
		// } else {
		// throw new RuntimeException("Unsupported statement for stdlib: "
		// + statement);
		// }
		// return result;
		//	// TODO Auto-generated method stub

	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor#containsFunction(java
	 * .lang.String)
	 */
	@Override
	public boolean containsFunction(String name) {
		Set<String> functions = new HashSet<String>();

		functions.add("malloc");
		functions.add("free");
		return functions.contains(name);
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor#initialize(edu.udel
	 * .cis.vsl.civl.state.State)
	 */
	@Override
	public State initialize(State state) {
		// TODO Auto-generated method stub
		return state;
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor#wrapUp(edu.udel.cis
	 * .vsl.civl.state.State)
	 */
	@Override
	public State wrapUp(State state) {
		// TODO Auto-generated method stub
		return state;
	}

	@Override
	public BooleanExpression getGuard(State state, int pid, Statement statement) {
		// TODO Auto-generated method stub
		return null;
	}

}