ConfigFactory.java
package edu.udel.cis.vsl.sarl.config.common;
import static java.io.StreamTokenizer.TT_EOF;
import static java.io.StreamTokenizer.TT_NUMBER;
import static java.io.StreamTokenizer.TT_WORD;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.PrintStream;
import java.io.StreamTokenizer;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import edu.udel.cis.vsl.sarl.IF.SARLException;
import edu.udel.cis.vsl.sarl.IF.SARLInternalException;
import edu.udel.cis.vsl.sarl.IF.config.ProverInfo;
import edu.udel.cis.vsl.sarl.IF.config.ProverInfo.ProverKind;
import edu.udel.cis.vsl.sarl.IF.config.SARLConfig;
/**
* Factory for producing and manipulating SARL configuration files and
* {@link SARLConfig} objects.
*
* @author siegel
*
*/
public class ConfigFactory {
// Fields...
/**
* Nickname for <code>System.err</code>.
*/
public final static PrintStream err = System.err;
/**
* Nickname for <code>System.out</code>.
*/
public final static PrintStream out = System.out;
/**
* Map from the names of the (JNI) dynamic libraries to the kind of the
* theorem prover. Add more entries as needed.
*/
private static Map<String, ProverKind> dylibMap = new HashMap<>();
static {
// dylibMap.put("cvc3jni", ProverKind.CVC3_API); // too fragile
// dylibMap.put("cvc4jni", ProverKind.CVC4_API); // crashes too much
// dylibMap.put("z3java", ProverKind.Z3_API); // not yet implemented
}
// Private methods...
/**
* <p>
* Function converting a string representation of the theorem prover kind to
* an actual {@link ProverKind} object.
* </p>
*
* <p>
* The {@link ProverKind} enumerated type provides some classification of
* theorem provers. There might be multiple entries for one actual prover,
* for example, because one entry is needed for the executable version using
* one input language, another entry is needed for the executable version
* using a different input language, and another version is needed for the
* API version. Add entries as needed.
* </p>
*
* @param kindString
* the exact string representation of the kind
* @return the kind which corresponds exactly to that string, or
* <code>null</code> is there is no such kind
*/
private static ProverKind kind(String kindString) {
switch (kindString) {
case "CVC4":
return ProverKind.CVC4;
case "CVC4_API":
return ProverKind.CVC4_API;
case "Z3":
return ProverKind.Z3;
case "Z3_API":
return ProverKind.Z3_API;
case "Why3":
return ProverKind.Why3;
default:
return null;
}
}
private static ProverKind proverKindFromExecutable(String execFileName) {
// Strip ".exe" from executable name if it is present.
int length = execFileName.length();
if (length > 4 && execFileName.substring(length - 4).equals(".exe"))
execFileName = execFileName.substring(0, length - 4);
switch (execFileName) {
case "cvc4":
return ProverKind.CVC4;
case "z3":
return ProverKind.Z3;
case "why3":
return ProverKind.Why3;
default:
return null;
}
}
/**
* Returns the command argument(s) for the given kind of theorem prover that
* causes that prover to print its version number. Add new entries as
* needed.
*
* @param kind
* the kind of theorem prover
* @return the command line arguments that cause the version number to be
* printed
* @throws SARLException
* if the kind is not of the executable variety
*/
private static String versionCommand(ProverKind kind) {
switch (kind) {
case CVC4:
case Why3:
return "--version";
case Z3:
return "-version";
default:
throw new SARLException("Unknown executable prover kind: " + kind);
}
}
/**
* Compares two version strings. Both are assumed to have form
* something.something....
*
* @param version1
* a version string
* @param version2
* a version string
* @return a negative int if version1 is lower than version2; 0 if they are
* equal; a positive int if version1 is higher that version2
*/
private static int compareVersions(String version1, String version2) {
if (version1 == null) { // null lower than everything
return version2 == null ? 0 : -1;
}
if (version2 == null) {
return 1;
}
String[] split1 = version1.split("\\."), split2 = version2.split("\\.");
int n1 = split1.length, n2 = split2.length;
for (int i = 0; i < n1; i++) {
if (i >= n2) { // anything higher than nothing
return 1;
}
String s1 = split1[i], s2 = split2[i];
Integer x1, x2;
int result;
try {
x1 = Integer.valueOf(s1);
} catch (NumberFormatException e) {
x1 = null;
}
try {
x2 = Integer.valueOf(s2);
} catch (NumberFormatException e) {
x2 = null;
}
if (x1 != null & x2 != null) { // two numbers: numerical order
result = x1 - x2;
} else if (x1 != null) { // number higher than non-number
result = 1;
} else if (x2 != null) {// number higher than non-number
result = -1;
} else { // two non-numbers: alphabetical order
result = s1.compareTo(s2);
}
if (result != 0)
return result;
}
return 0;
}
/**
* Returns an exception object in the case where a SARL configuration file
* has incorrect syntax.
*
* @param file
* the SARL configuration file being parsed
* @param st
* the stream tokenizer being used to parse the configuration
* file
* @param msg
* an error message
* @return a {@link SARLException} with a nice presentation of the error
* message, file name, and line number
*/
private static SARLException parseErr(File file, StreamTokenizer st,
String msg) {
return new SARLException(file + " " + st.toString() + " " + msg);
}
/**
* Determines whether a file with a specified name exists in a specified
* directory. The file must be a regular file, not a directory.
*
* @param dir
* directory in which to look
* @param filename
* name of file
* @return if the directory exists and the file exists and is a regular file
* in that directory: the {@link File} object corresponding to the
* file; otherwise <code>null</code>
*/
private static File getFile(File dir, String filename) {
if (dir.isDirectory()) {
File file = new File(dir, filename);
if (file.isFile())
return file;
}
return null;
}
/**
* Checks that an executable prover actually can be executed and creates a
* corresponding {@link ProverInfo} object for it.
*
* @param kind
* the kind of theorem prover
* @param alias
* the alias string to use in the configuration entry
* @param executableFile
* the executable theorem prover
* @return a new {@link ProverInfo} object corresponding to the specified
* prover, or <code>null</code> if the prover could not be executed
* correctly
*/
private static ProverInfo processExecutableProver(ProverKind kind,
String alias, File executableFile) {
String fullPath = executableFile.getAbsolutePath();
ProcessBuilder pb = new ProcessBuilder(fullPath, versionCommand(kind));
Process process = null;
String line;
try {
process = pb.start();
BufferedReader stdout = new BufferedReader(
new InputStreamReader(process.getInputStream()));
line = stdout.readLine().trim();
process.destroy();
} catch (Throwable e) {
if (process != null)
process.destroy();
out.println("Failed to execute " + fullPath);
return null;
}
int pos = line.lastIndexOf("version ");
if (pos < 0) {
out.println("Unexpected output from " + fullPath);
return null;
}
String version = line.substring(pos + "version ".length());
ProverInfo info = new CommonProverInfo();
info.addAlias(alias);
info.setKind(kind);
info.setPath(executableFile);
info.setVersion(version);
info.setTimeout(10.0);
info.setShowQueries(false);
info.setShowInconclusives(false);
info.setShowErrors(true);
if (kind == ProverKind.Why3) {
info.addOption("cvc4-15");
info.addOption("z3");
info.setTimeout(5.0);
// set environment for helping why3 finding prover executables:
info.setEnv(System.getenv("PATH"));
}
return info;
}
/**
* Checks that a candidate dynamic library prover can be loaded, and, if so,
* returns a new {@link ProverInfo} object corresponding to it.
*
* @param kind
* the kind of the candidate theorem prover (should end in
* "_API")
* @param alias
* the alias to assign to this prover in the configuration file
* @param jnidylib
* the name of the JNI dynamic library that should be loaded,
* e.g. "cvc3jni"
* @return a new {@link ProverInfo} object if that dynamic library was
* loaded successfully; otherwise, <code>null</code>
*/
private static ProverInfo processDynamicProver(ProverKind kind,
String alias, String jnidylib) {
String libraryName;
try {
libraryName = System.mapLibraryName(jnidylib);
System.loadLibrary(jnidylib);
} catch (Throwable e) {
return null;
}
ProverInfo info = new CommonProverInfo();
info.addAlias(alias);
info.setKind(kind);
info.setPath(new File(libraryName));
info.setVersion("UNKNOWN");
info.setTimeout(10.0);
info.setShowQueries(false);
info.setShowInconclusives(false);
info.setShowErrors(true);
return info;
}
// Public methods...
/**
* Parses a SARL configuration file.
*
* @param configFile
* the configuration file
* @return the {@link SARLConfig} object resulting from parsing that file
* @throws IOException
* if anything goes wrong reading the file
* @throws SARLException
* if the configuration file does not conform to the proper
* syntax
*/
public static SARLConfig fromFile(File configFile) throws IOException {
BufferedReader reader = new BufferedReader(new FileReader(configFile));
StreamTokenizer st = new StreamTokenizer(reader);
LinkedList<ProverInfo> proverInfos = new LinkedList<>();
Set<String> allAliases = new HashSet<>();
ProverInfo why3info = null;
st.commentChar('#');
st.quoteChar('"');
st.quoteChar('\'');
st.parseNumbers();
st.eolIsSignificant(false);
st.slashSlashComments(true);
st.slashStarComments(true);
st.lowerCaseMode(false);
st.wordChars('_', '_');
for (int token = st.nextToken(); token != TT_EOF; token = st
.nextToken()) {
if (token != TT_WORD || !"prover".equalsIgnoreCase(st.sval))
throw parseErr(configFile, st, "expected \"prover\"");
token = st.nextToken();
if (token != '{')
throw parseErr(configFile, st, "expected '{'");
ProverInfo info = new CommonProverInfo();
for (token = st.nextToken(); token != '}'; token = st.nextToken()) {
String keyword;
if (token != TT_WORD)
throw parseErr(configFile, st, "expected a key-word");
keyword = st.sval;
token = st.nextToken();
if (token != '=')
throw parseErr(configFile, st, "expected '='");
switch (keyword) {
case "aliases": {
int numAliases = 0;
for (token = st.nextToken(); token != ';'; token = st
.nextToken()) {
if (numAliases > 0) {
if (token != ',')
throw parseErr(configFile, st, "expected ','");
token = st.nextToken();
}
if (token != TT_WORD)
throw parseErr(configFile, st,
"expected a plain word to be used as alias");
if (!allAliases.add(st.sval))
throw parseErr(configFile, st,
"alias used more than once");
info.addAlias(st.sval);
numAliases++;
}
if (numAliases == 0)
throw parseErr(configFile, st,
"expected at least one alias");
break;
}
case "path": {
token = st.nextToken();
if (token != '"' && token != '\'')
throw parseErr(configFile, st,
"expected quoted string");
if (info.getPath() != null)
throw parseErr(configFile, st, "more than one path");
info.setPath(new File(st.sval));
token = st.nextToken();
if (token != ';')
throw parseErr(configFile, st, "expected ';'");
break;
}
case "options": {
boolean first = true;
for (token = st.nextToken(); token != ';'; token = st
.nextToken()) {
if (first)
first = false;
else {
if (token != ',')
throw parseErr(configFile, st, "expected ','");
token = st.nextToken();
}
if (token != '"' && token != '\'')
throw parseErr(configFile, st,
"expected a quoted string");
info.addOption(st.sval);
}
break;
}
case "version": {
token = st.nextToken();
if (token != '"' && token != '\'')
throw parseErr(configFile, st,
"expected quoted string");
if (info.getVersion() != null)
throw parseErr(configFile, st, "more than one version");
info.setVersion(st.sval);
token = st.nextToken();
if (token != ';')
throw parseErr(configFile, st, "expected ';'");
break;
}
case "kind": {
token = st.nextToken();
if (token != TT_WORD)
throw parseErr(configFile, st, "expected word");
if (info.getKind() != null)
throw parseErr(configFile, st, "more than one kind");
ProverKind kind = kind(st.sval);
if (kind == null)
throw parseErr(configFile, st, "unknown prover kind");
info.setKind(kind);
token = st.nextToken();
if (token != ';')
throw parseErr(configFile, st, "expected ';'");
break;
}
case "showQueries":
case "showInconclusives":
case "showErrors": {
token = st.nextToken();
if (token != TT_WORD)
throw parseErr(configFile, st, "expected word");
boolean value;
switch (st.sval) {
case "true":
value = true;
break;
case "false":
value = false;
break;
default:
throw parseErr(configFile, st,
"expected true or false");
}
switch (keyword) {
case "showQueries":
info.setShowQueries(value);
break;
case "showInconclusives":
info.setShowInconclusives(value);
break;
case "showErrors":
info.setShowErrors(value);
break;
default:
throw new SARLInternalException("Unreachable");
}
token = st.nextToken();
if (token != ';')
throw parseErr(configFile, st, "expected ';'");
break;
}
case "timeout": {
token = st.nextToken();
if (token != TT_NUMBER)
throw parseErr(configFile, st,
"expected number (time in seconds)");
info.setTimeout(st.nval);
token = st.nextToken();
if (token != ';')
throw parseErr(configFile, st, "expected ';'");
break;
}
case "environment": {
token = st.nextToken();
if (token != '"' && token != '\'')
throw parseErr(configFile, st,
"expected quoted string");
info.setEnv(st.sval);
token = st.nextToken();
if (token != ';')
throw parseErr(configFile, st, "expected ';'");
break;
}
default:
throw parseErr(configFile, st,
"unknown keyword: " + keyword);
} // end of switch
} // end of for
if (info.getKind() != ProverKind.Why3)
proverInfos.add(info);
else
why3info = info;
} // end of for
reader.close();
CommonSARLConfig config = new CommonSARLConfig(proverInfos);
config.setWhy3ProvePlatform(why3info);
return config;
}
/**
* Looks for a SARL configuration file by first looking in the current
* working directory for a file named <code>.sarl</code>. If no file by that
* name is found, it looks in the user's home directory for
* <code>.sarl</code>. If that is not found, it looks in the current working
* directory for a file named <code>.sarl_default</code>. If that is not
* found, it looks in the home directory for <code>.sarl_default</code>.
*
* @return the SARL configuration file, or <code>null</code> if not found
*/
public static File findSARLConfigFile() {
File workingDir = new File(System.getProperty("user.dir"));
File result = getFile(workingDir, ".sarl");
if (result != null)
return result;
File homeDir = getHomeDir();
result = getFile(homeDir, ".sarl");
if (result != null)
return result;
result = getFile(workingDir, ".sarl_default");
if (result != null)
return result;
result = getFile(homeDir, ".sarl_default");
return result;
}
/**
* gets the user home directory:
*
* if the vm argument -Duser.home=$HOME, the value of the environment
* variable needs to be figured out.
*
* @return
*/
private static File getHomeDir() {
// when -Duser.home=$HOME is used, System.getProperty("user.home")
// returns "$HOME" (HOME could be any identifier)
String userHome = System.getProperty("user.home");
if (userHome.startsWith("$")) {
// getting the value of "HOME" (HOME could be any identifier)
userHome = System.getenv(userHome.substring(1));
}
return new File(userHome);
}
/**
* Checks that a {@link SARLConfig} object corresponds to the actual system
* on which we are running.
*
* @param config
* a {@link SARLConfig} object
* @throws SARLException
* if a theorem prover specified in the config is not found, or
* cannot be executed/loaded, or does not have the version
* specified
*/
public static void checkConfig(SARLConfig config) throws SARLException {
for (ProverInfo info : config.getProvers()) {
if (info.isExecutable()) {
ProverInfo reread = processExecutableProver(info.getKind(),
info.getFirstAlias(), info.getPath());
if (reread == null)
throw new SARLException("no theorem prover "
+ info.getFirstAlias() + " at " + info.getPath());
if (!reread.getVersion().equals(info.getVersion()))
throw new SARLException("expected version "
+ info.getVersion() + " for " + info.getFirstAlias()
+ " but found " + reread.getVersion());
} else {
for (Entry<String, ProverKind> entry : dylibMap.entrySet()) {
if (entry.getValue() == info.getKind()) {
File path = new File(
System.mapLibraryName(entry.getKey()));
if (path.equals(info.getPath())) {
try {
System.loadLibrary(entry.getKey());
return;
} catch (Throwable e) {
throw new SARLException(
"unable to load dynamic library "
+ path);
}
}
}
}
throw new SARLException("dynamic library " + info.getPath()
+ " for " + info.getFirstAlias() + " not found");
}
}
}
/**
* Finds and parses the SARL configuration file.
*
* @return {@link SARLConfig} object resulting from parsing the
* configuration file, or <code>null</code> if a configuration file
* was not found
* @throws IOException
* if anything goes wrong reading the configuration file
* @throws SARLException
* if the configuration file does not conform to the proper
* syntax
*/
public static SARLConfig findConfig() throws IOException {
File configFile = findSARLConfigFile();
if (configFile == null)
return null;
return fromFile(configFile);
}
/**
* Searches for theorem provers on the user's system and creates a SARL
* configuration file <code>.sarl</code> in the user's home directory.
*
* @throws FileNotFoundException
* if the configuration file cannot be created in the home
* directory
*/
public static void makeConfigFile() throws FileNotFoundException {
File userHomeDir = getHomeDir();
File configFile = new File(userHomeDir, ".sarl");
if (configFile.exists()) {
if (configFile.isFile()) {
File newLocation = new File(userHomeDir, ".sarl.old");
out.println("Moving existing SARL configuration file to "
+ newLocation.getAbsolutePath());
out.flush();
configFile.renameTo(newLocation);
} else {
System.err.println("Remove the non-ordinary-file "
+ configFile.getAbsolutePath() + " and try again.");
System.err.flush();
System.exit(2);
}
}
String path = System.getenv("PATH");
String[] pathDirs = path.split(File.pathSeparator);
PrintStream stream = new PrintStream(new FileOutputStream(configFile));
Map<ProverKind, ProverInfo> executableFoundMap = new HashMap<>();
ArrayList<ProverInfo> provers = new ArrayList<>();
HashSet<String> seenPaths = new HashSet<>();
out.println("Creating SARL configuration file in " + configFile);
out.flush();
stream.println("/* This is a SARL configuration file.");
stream.println(
" * It contains one entry for each theorem prover SARL may use.");
stream.println(
" * To resolve a query, by default, SARL will use the first prover here.");
stream.println(
" * If that result in inconclusive, it will try the second prover.");
stream.println(
" * And so on, until a conclusive result has been reached, or all provers");
stream.println(" * have been exhausted.");
stream.println(" * ");
stream.println(
" * SARL looks for a configuration file by looking in the following");
stream.println(" * places in order:");
stream.println(" * 1. .sarl in current working directory");
stream.println(" * 2. .sarl in user's home directory");
stream.println(" * 3. .sarl_default in current working directory");
stream.println(" * 4. .sarl_default in user's home directory");
stream.println(" */");
stream.println();
stream.flush();
for (String dirName : pathDirs) {
File dir = new File(dirName);
String fullDirName = dir.getAbsolutePath();
if (dir.isDirectory()) {
if (!seenPaths.add(fullDirName))
continue;
File[] files = dir.listFiles();
for (File file : files) {
if (!file.canExecute())
continue;
String name = file.getName();
ProverKind kind = proverKindFromExecutable(name);
if (kind != null) {
String alias = kind.toString().toLowerCase();
ProverInfo prover = processExecutableProver(kind, alias,
file);
if (prover != null) {
String msg = kind + " version "
+ prover.getVersion() + " at "
+ prover.getPath();
ProverInfo oldProver = executableFoundMap.get(kind);
if (oldProver != null) {
int compare = compareVersions(
prover.getVersion(),
oldProver.getVersion());
if (compare == 0) {
out.println("Ignoring equivalent " + msg);
out.flush();
continue;
}
if (compare < 0) {
out.println("Ignoring older " + msg);
out.flush();
continue;
}
out.println("Replacing previous " + kind
+ " with " + msg);
out.flush();
} else {
out.println("Adding " + msg);
}
executableFoundMap.put(kind, prover);
}
}
}
}
}
provers.addAll(executableFoundMap.values());
// now the dynamic libraries...
for (Entry<String, ProverKind> entry : dylibMap.entrySet()) {
String libraryName = entry.getKey();
ProverKind kind = entry.getValue();
String alias = kind.toString().toLowerCase();
ProverInfo prover = processDynamicProver(kind, alias, libraryName);
if (prover != null) {
out.println("Found " + kind + " implemented as native library "
+ libraryName);
out.flush();
provers.add(prover);
}
}
Collections.sort(provers);
for (ProverInfo prover : provers) {
prover.print(stream);
stream.println();
}
stream.close();
if (provers.isEmpty()) {
err.println(
"No appropriate theorem provers were found in your PATH.");
err.println(
"SARL's theorem proving capability will be very limited.");
err.println(
"Consider installing at least one of CVC3, CVC4, or Z3.");
err.flush();
}
out.println("SARL configuration file created successfully in "
+ configFile.getAbsolutePath());
out.println(
"By default, SARL will use all provers listed in the configuration file,");
out.println("in order, until a conclusive result is obtained.");
out.println(
"Edit the file as necessary to remove or change the order of provers.");
out.flush();
}
}