diff options
Diffstat (limited to 'rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java')
-rw-r--r-- | rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java | 360 |
1 files changed, 360 insertions, 0 deletions
diff --git a/rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java b/rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java new file mode 100644 index 0000000..7f9da9c --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java @@ -0,0 +1,360 @@ +package rba.tool.core.z3; + +import java.io.IOException; +import java.lang.reflect.Field; +import java.net.URL; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import org.eclipse.core.resources.IContainer; +import org.eclipse.core.resources.IFile; +import org.eclipse.core.resources.IProject; +import org.eclipse.core.resources.IResource; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.core.runtime.FileLocator; +import org.eclipse.core.runtime.Platform; + +import com.microsoft.z3.ApplyResult; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import com.microsoft.z3.Goal; +import com.microsoft.z3.Solver; +import com.microsoft.z3.Status; +import com.microsoft.z3.Tactic; + +import groovy.util.GroovyScriptEngine; +import rba.tool.core.Activator; +import rba.tool.core.constraint.IConstraintCalculation; +import rba.tool.core.sort.ISortValueCalculation; + +public class Z3CodeManager { + + public static Z3CodeManager INSTNACE = new Z3CodeManager(); + + private static final String ERROR_ENV_PATH = "The Z3 storage path cannot be found. Area and content parameters are not derived correctly. \r\nSet the environment variable of the storage path of Z3."; + + private static final String ERROR_SCRIPT = "Z3 execution failed. There is an error in the script."; + + private static final String SORT_SCRIPT_NAME = "SortValueCalculation.java"; + + private static final String CONST_SCRIPT_NAME = "ConstraintCalculation.java"; + + private static final String ERROR_NOT_FOUND_SCRIPT = "Z3 execution failed. Failed to generate %s in the %s project."; + + private Z3CodeManager() { + } + + public boolean loadZ3Lib() { + String z3Path = ""; + try { + z3Path = getPath(); + } catch (Exception e1) { + e1.printStackTrace(); + return false; + } + if (null == z3Path || z3Path.isEmpty()) { + return false; + } + try { + // load necessary z3 DLLs + loadDLLs(z3Path); + // add z3 path to java.library.path + addLibraryPath(z3Path); + return true; + } catch (Exception e) { + e.printStackTrace(); + return false; + } + } + + private String getPath() throws IOException { + String path = ""; + String jvmBitMode = System.getProperty("sun.arch.data.model"); + // Check JVM 32 Bit. + if (jvmBitMode != null && jvmBitMode.contains("32")) { + URL bundleEntryUrl = Platform.getBundle(Activator.PLUGIN_ID).getEntry("lib32/z3"); + URL fileUrl = FileLocator.toFileURL(bundleEntryUrl); + path = fileUrl.getPath(); + } + // Check JVM 64 Bit. + if (jvmBitMode != null && jvmBitMode.contains("64")) { + URL bundleEntryUrl = Platform.getBundle(Activator.PLUGIN_ID).getEntry("lib/z3"); + URL fileUrl = FileLocator.toFileURL(bundleEntryUrl); + path = fileUrl.getPath(); + } + return path; + } + + public ISortValueCalculation getSortCaluculator(IProject project) throws RuntimeException { + + if (!loadZ3Lib()) { + String errMsg = ERROR_ENV_PATH; + throw new RuntimeException(errMsg); + } + + ISortValueCalculation calc = null; + IFile file = findFile(SORT_SCRIPT_NAME, project); + if (file != null) { + try { + String fileName = file.getName(); + String className = fileName.substring(0, fileName.lastIndexOf(".")); + + String string = file.getLocation().toString(); + String genPath = string.substring(0, string.length() - fileName.length()); + + GroovyScriptEngine e = new GroovyScriptEngine(new String[] { genPath }, getClass().getClassLoader()); + e.loadScriptByName(fileName); + Class<?> s = e.getGroovyClassLoader().loadClass(className); + + calc = (ISortValueCalculation) s.newInstance(); + } catch (Exception e) { + String errMsg = ERROR_SCRIPT; + throw new RuntimeException(errMsg); + } + + } else { + String errMsg = String.format(ERROR_NOT_FOUND_SCRIPT, project.getName(), SORT_SCRIPT_NAME); + throw new RuntimeException(errMsg); + } + + return calc; + } + + public IFile findFile(String name, IContainer container) { + try { + IResource[] resources; + resources = container.members(); + if (resources == null || resources.length == 0) { + return null; + } + for (IResource resource : resources) { + if (resource instanceof IFile && resource.getName().equals(name)) { + return (IFile) resource; + } + if (resource instanceof IContainer) { + IFile recursive = findFile(name, (IContainer) resource); + if (recursive != null) { + return recursive; + } + } + } + } catch (CoreException e) { + } + + return null; + } + + /** + * load z3 DLLs from the path + * @param z3Path + */ + private void loadDLLs(String z3Path) throws Exception { + System.load(z3Path + "\\Microsoft.Z3.dll"); + System.load(z3Path + "\\msvcr110.dll"); + System.load(z3Path + "\\msvcp110.dll"); + System.load(z3Path + "\\vcomp110.dll"); + System.load(z3Path + "\\libz3.dll"); + System.load(z3Path + "\\libz3java.dll"); + } + + /** + * add z3 path to java.library.path + * @param pathToAdd + */ + private void addLibraryPath(String pathToAdd) throws Exception { + final Field usrPathsField = ClassLoader.class.getDeclaredField("usr_paths"); + usrPathsField.setAccessible(true); + // get array of paths + final String[] paths = (String[]) usrPathsField.get(null); + // check if the path to add is already present + for (String path : paths) { + if (path.equals(pathToAdd)) { + return; + } + } + // add the new path + final String[] newPaths = Arrays.copyOf(paths, paths.length + 1); + newPaths[newPaths.length - 1] = pathToAdd; + usrPathsField.set(null, newPaths); + } + + public Map<String, Integer> setModel(Solver s, List<Expr> contentsList, Status st) { + switch (st) { + case UNKNOWN: + System.out.println("Unknown"); + break; + + case SATISFIABLE: + return setSat(s, contentsList); + case UNSATISFIABLE: + return setUnsat(s); + } + + return null; + } + + public Map<String, Integer> setSat(Solver s, List<Expr> evaluatedExpr) { + + Map<String, Integer> map = new HashMap<String, Integer>(); + + map.put(Z3Constants.TOTAL_RESULT, Z3Constants.SAT_VAL); + + for (Expr i : evaluatedExpr) { + String areaName = getName(i.getSExpr()); + String expVal = s.getModel().evaluate(i, false).toString(); + + map.put(areaName, Integer.valueOf(expVal)); + } + + return map; + } + + public Map<String, Integer> setUnsat(Solver s) { + + Map<String, Integer> map = new HashMap<String, Integer>(); + + map.put(Z3Constants.TOTAL_RESULT, Z3Constants.UNSAT_VAL); + + for (Expr i : s.getUnsatCore()) { + String areaName = getName(i.toString()); + map.put(areaName, Z3Constants.UNSAT_VAL); + } + return map; + } + + private String getName(String baseName) { + String name = baseName; + if (name.length() > 2 && name.startsWith("|") && name.endsWith("|")) { + name = name.substring(1, name.length() - 1); + } + + return name; + } + + public List<String> getErrors(Solver s, Status st) { + List<String> list = new ArrayList<String>(); + + switch (st) { + case UNKNOWN: + + list.add(Z3Constants.UNKNOWN); + list.add(s.getReasonUnknown()); + break; + case SATISFIABLE: + list.add(Z3Constants.SAT); + break; + case UNSATISFIABLE: + list.add(Z3Constants.UNSAT); + + for (Expr i : s.getUnsatCore()) { + list.add(getName(i.toString())); + } + } + + return list; + } + + public List<String> getErrors(Context ctx, Solver s, Status st, String constrName, List<BoolExpr> constrList, List<BoolExpr> constrLabelList) { + List<String> list = new ArrayList<String>(); + + switch (st) { + case UNKNOWN: + String reason = s.getReasonUnknown(); + System.out.println("*Unknown:" + constrName + " - " + reason); + + Goal g = ctx.mkGoal(false, false, false); + for (int i = 0; i < constrList.size(); i++) { + g.add(constrList.get(i), constrLabelList.get(i)); + } + + Tactic t = ctx.mkTactic("qfbv"); + try { + ApplyResult ar = t.apply(g); + if (ar.getNumSubgoals() == 1) { + if (ar.getSubgoals()[0].isDecidedSat()) { + System.out.println("=> SAT"); + list.add(Z3Constants.SAT); + break; + } + } + } catch (Exception e) { + System.out.println("2ND Check"); + + t = ctx.mkTactic("smt"); + try { + ApplyResult ar = t.apply(g); + if (ar.getNumSubgoals() == 1) { + if (ar.getSubgoals()[0].isDecidedSat()) { + System.out.println("==> SAT"); + list.add(Z3Constants.SAT); + break; + } + } + } catch (Exception e2) { + e2.printStackTrace(); + } + } + + list.add(Z3Constants.UNKNOWN); + list.add(reason); + break; + case SATISFIABLE: + list.add(Z3Constants.SAT); + break; + case UNSATISFIABLE: + list.add(Z3Constants.UNSAT); + + for (Expr i : s.getUnsatCore()) { + list.add(getName(i.toString())); + } + } + + return list; + } + + public IConstraintCalculation getConstraintCaluculator(IProject project) throws RuntimeException { + + if (!loadZ3Lib()) { + String errMsg = ERROR_ENV_PATH; + throw new RuntimeException(errMsg); + } + + IConstraintCalculation calc = null; + IFile file = findFile(CONST_SCRIPT_NAME, project); + if (file != null) { + String fileName = file.getName(); + String className = fileName.substring(0, fileName.lastIndexOf(".")); + + String string = file.getLocation().toString(); + String genPath = string.substring(0, string.length() - fileName.length()); + + calc = getConstraintCaluculator(fileName, className, genPath); + + } else { + String errMsg = String.format(ERROR_NOT_FOUND_SCRIPT, project.getName(), CONST_SCRIPT_NAME); + throw new RuntimeException(errMsg); + } + + return calc; + } + + public IConstraintCalculation getConstraintCaluculator(String fileName, String className, String genPath) throws RuntimeException { + IConstraintCalculation calc = null; + try { + GroovyScriptEngine e = new GroovyScriptEngine(new String[] { genPath }, getClass().getClassLoader()); + e.loadScriptByName(fileName); + Class<?> s = e.getGroovyClassLoader().loadClass(className); + + calc = (IConstraintCalculation) s.newInstance(); + } catch (Exception e) { + String errMsg = ERROR_SCRIPT; + System.out.println(e.getMessage()); + throw new RuntimeException(errMsg); + } + return calc; + } +} |