001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.decproc;
019:
020: import java.io.*;
021: import java.util.Map;
022: import java.util.WeakHashMap;
023: import java.util.zip.ZipEntry;
024: import java.util.zip.ZipOutputStream;
025:
026: import org.apache.log4j.*;
027:
028: import de.uka.ilkd.key.gui.DecisionProcedureSettings;
029: import de.uka.ilkd.key.gui.configuration.PathConfig;
030: import de.uka.ilkd.key.java.Services;
031: import de.uka.ilkd.key.logic.Constraint;
032: import de.uka.ilkd.key.proof.Goal;
033: import de.uka.ilkd.key.proof.Proof;
034: import de.uka.ilkd.key.proof.decproc.smtlib.Benchmark;
035:
036: /** Represents a basic class for the invocation of decisison procedures accepting the SMT-LIB
037: * format as input language on the translation of a KeY <tt>Goal</tt>.
038: * <p>
039: * An instance of this class takes a <tt>Goal</tt>, translates it in into a <tt>Benchmark</tt>
040: * for the SMT logic (QF_)AUFLIA and stores this translation result in a temporary file.
041: * <p>
042: * This class is intended to be subclassed by classes which invoke a concrete decision procedure
043: * supporting the SMT-LIB logic (QF_)AUFLIA. These subclasses must implement the provided hook method
044: * <tt>execDecProc()</tt>
045: *
046: * @author akuwertz
047: * @version 1.3, 10/02/2006 (Extended to support quantifiers (AUFLIA) )
048: */
049:
050: public abstract class DecisionProcedureSmtAuflia extends
051: AbstractDecisionProcedure {
052:
053: /* Additional fields */
054:
055: /* String constants for creation of the temporary file which stores the translation result */
056: private static final String tempPrefix = "key_smt_auflia_";
057: private static final String tempSuffix = ".smt";
058:
059: /* String constants for errors during file creation */
060: private static final String tempFileCreateError = "Temporary file could not be created!\n";
061: private static final String problemFileCopyError = "*******************************************\n"
062: + "An IOException occured during benchmark archiving!\n"
063: + "A problem file could not be copied!\n"
064: + "*******************************************";
065: private static final String archFileCreationError = "*******************************************\n"
066: + "An IOException occured during benchmark archiving!\n"
067: + "Archive file could not be created!\n"
068: + "*******************************************";
069: private static final String zipArchiveCreationError = "*******************************************\n"
070: + "An IOException occured during benchmark archiving!\n"
071: + "Problem could not be copied into a zipped archive!\n"
072: + "*******************************************";
073: private static final String problemPathFileCreationError = "*******************************************\n"
074: + "An IOException occured during benchmark archiving!\n"
075: + "Problem path could not be written into file!\n"
076: + "*******************************************";
077:
078: /** The <tt>Benchmark</tt> representing the translation result */
079: private Benchmark resultBenchmark;
080:
081: /** The temporary file in which the translation result is stored */
082: private final File tempFile;
083:
084: /** The <tt>File</tt> from with the current problem was loaded into KeY */
085: private static File loadedProblem;
086:
087: /** The <tt>Proof</tt> that is currently selected in the proofer */
088: private static Proof currentProof = null;
089:
090: /** A flag indicating that a new file was loaded */
091: private static boolean newProblemLoaded;
092:
093: /** A <tt>String</tt> denoting the path of the directory in which the <tt>Benchmark</tt>s
094: * created on the currently loaded problem will be archived */
095: private static String currentArchiveDir;
096:
097: /** */
098: private static Map fromProofToArchive = new WeakHashMap();
099:
100: private static final String logPrefix = "smt_";
101: private static final String logSuffix = "log";
102: private static final String logDir = PathConfig.KEY_CONFIG_DIR
103: + File.separator + "SmtTrans_Logs";
104: private static final String logFileCreateError = "SMT log file could not be created!\n";
105:
106: private static final String archiveDir = PathConfig.KEY_CONFIG_DIR
107: + File.separator + "SmtBench_Archive";
108: private static final String archiveFileExt = ".smt";
109: private static final String zipFileExt = ".zip";
110: private static final String notesAttrIntro = "\n This benchmark was translated from the following KeY sequent:\n"
111: + " -----------------Begin sequent-----------------\n";
112: private static final String notesAttrOutro = " ------------------End sequent------------------\n"
113: + " End of :notes";
114:
115: /** A <tt>Logger</tt> used to log the progress of the translation process.<br>
116: * Serves as root for the logger hierarchy used during the translation process. It therefore
117: * allows managing the configuration of all loggers in this hierarchy at a single point
118: *
119: * @see #configureLogger(Level)
120: */
121: private static final Logger logger = Logger
122: .getLogger(DecisionProcedureSmtAuflia.class.getPackage()
123: .getName());
124:
125: /** The pattern to format the output of log statements */
126: private static final String layoutPattern = "%-5p [%-22c{1}]: %m%n";
127:
128: /* Constructors */
129:
130: /** Mere constructor, just creates a new <tt>DecisionProcedureSmtAuflia</tt> instance
131: *
132: * @param goal the <tt>Goal</tt> which should be translated
133: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> used for translation
134: * @param services the <tt>Services</tt> used during translation
135: */
136: public DecisionProcedureSmtAuflia(Goal goal,
137: DecisionProcedureTranslationFactory dptf, Services services) {
138: super (goal, null, dptf, services);
139: try {
140: tempFile = File.createTempFile(tempPrefix, tempSuffix);
141: } catch (IOException e) {
142: throw new RuntimeException(tempFileCreateError
143: + e.getMessage());
144: }
145: }
146:
147: /* Static methods */
148:
149: /** Informs this class that a new problem has been loaded in KeY.
150: * <p>
151: * This method should be called every time when a new problem has been loaded to the KeY prover.<br>
152: * It delayedly sets up a new directory to store all benchmarks resulting from the loaded problem
153: *
154: * @param problemFile the problem <tt>File</tt> the has been loaded
155: * @param proof the <tt>Proof</tt> that has been created for the given problem
156: */
157: public static void fireNewProblemLoaded(File problemFile,
158: Proof proof) {
159: // If there is a previously loaded problem, save its context
160: if (currentProof != null) {
161: fireSelectedProofChanged(proof);
162: } else {
163: currentProof = proof;
164: }
165: loadedProblem = problemFile;
166: newProblemLoaded = true;
167:
168: }
169:
170: /** Informs this class the another <tt>Proof</tt> has been selected in the prover.
171: * <p>
172: * This method should be called every time when the selected <tt>Proof</tt> has changed.<br>
173: * It changes the directory in which the created SMT-Lib benchmarks will be archived so that
174: * all benchmarks resulting from one loaded problem will be stored in the same directory
175: *
176: * @param proof the <tt>Proof</tt> that is currently selected in the prover
177: */
178: public static void fireSelectedProofChanged(Proof proof) {
179: if (currentProof != proof && proof != null) {
180: // Save current settings:
181: // If archive dir hasn't been created yet, put problem file into map
182: if (newProblemLoaded)
183: fromProofToArchive.put(currentProof, loadedProblem);
184: // Else put the currently valid archive dir into map
185: else
186: fromProofToArchive.put(currentProof, currentArchiveDir);
187:
188: // Load new settings
189: currentProof = proof;
190: Object widget = fromProofToArchive.get(proof);
191: // If the widget is a File, then the archive dir hasn't been created yet
192: if (widget instanceof File) {
193: loadedProblem = (File) widget;
194: newProblemLoaded = true;
195: return;
196: }
197: // If the widget is a String, retrieve the current archive dir
198: if (widget instanceof String) {
199: currentArchiveDir = (String) widget;
200: newProblemLoaded = false;
201: }
202: // if the widget is null, none of the above holds (in case of a newly loaded problem)
203: }
204: }
205:
206: /* Public and protected method implementations */
207:
208: /* (non-Javadoc)
209: * @see de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure#run(boolean)
210: */
211: public DecisionProcedureResult run(boolean lightweight) {
212: return runInternal(null, lightweight);
213: }
214:
215: /* (non-Javadoc)
216: * @see de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure#runInternal(de.uka.ilkd.key.proof.decproc.ConstraintSet)
217: */
218: protected final DecisionProcedureResult runInternal(
219: ConstraintSet constraintSet, boolean lightWeight) {
220:
221: DecisionProcedureSettings currentDecprocSettings = currentProof
222: .getSettings().getDecisionProcedureSettings();
223:
224: // Translate given sequent
225: logger.info("Issuing new translation request at time: "
226: + getCurrentDateString().substring(11, 20));
227: SmtAufliaTranslation sequentTranslation = dptf
228: .createSmtAufliaTranslation(goal.sequent(),
229: this .services, currentDecprocSettings
230: .useQuantifiers());
231: logger.info("Retrieving translation result");
232: resultBenchmark = sequentTranslation.getBenchmark();
233: DecisionProcedureResult result;
234:
235: // Check if a backend decision procedure should be called or only archiving is to be done
236: if (!currentDecprocSettings.useSMT_Translation()) {
237:
238: // Backend decision procedure part
239: try {
240: // Write result to file
241: PrintWriter out = new PrintWriter(new FileWriter(
242: tempFile));
243: String input = resultBenchmark.toString();
244: logger.info("Storing result in tmp file: "
245: + tempFile.getName());
246: logger.debug(">--------Created Benchmark--------<");
247: logger.debug(input);
248: logger.debug(">----End of Created Benchmark-----<");
249: out.println(input);
250: out.close();
251: } catch (IOException e) {
252: throw new RuntimeException(tempFileCreateError
253: + e.getMessage());
254: }
255:
256: // Here follows the invocation of the used decision procedure,
257: // defined in an according subclass
258: logger.info("Invocating decision procedure...");
259: result = execDecProc();
260: logger.info("Decision procedure completed with result: "
261: + (result.getResult() ? "goal was closed!"
262: : "goal could not be closed!"));
263: logger.debug("Decision procedure said in detail: "
264: + result.getText());
265: logger.info("Returning results to KeY prover!");
266:
267: tempFile.delete();
268:
269: } else {
270: result = new DecisionProcedureResult(false,
271: "dummy result from mere translation",
272: Constraint.BOTTOM);
273: logger
274: .info("Dummy Translation: created dummy result without calling a "
275: + "decision procedure");
276: }
277:
278: // At last, archive the created benchmark
279:
280: if (currentDecprocSettings.doBenchmarkArchiving()
281: || currentDecprocSettings.useSMT_Translation()) {
282:
283: // If archiving of benchmarks is enabled, extend benchmarks with notes and archive them
284: logger.info("Setting extended benchmark attributes");
285: resultBenchmark.setSource();
286: resultBenchmark.setNotes(notesAttrIntro
287: + goal.sequent().prettyprint(services)
288: + notesAttrOutro);
289: if (newProblemLoaded) {
290: // Create new archive dir and store problem in an appropriate way
291: logger
292: .info("Newly loaded problem dectected: creating new current archive "
293: + "directory");
294: newProblemLoaded = false;
295: currentArchiveDir = archiveDir + File.separator
296: + getCurrentDateString().substring(0, 20);
297: File archDir = new File(currentArchiveDir);
298: archDir.mkdirs();
299: if (loadedProblem.isDirectory()) {
300: if (!currentProof.getSettings()
301: .getDecisionProcedureSettings()
302: .doZipProblemDir()) {
303: // Just save path to problem...
304: logger
305: .info("Directory zipping disabled. Saving problem file path");
306: File pathFile = new File(archDir, loadedProblem
307: .getName());
308: try {
309: PrintWriter writer = new PrintWriter(
310: new FileWriter(pathFile));
311: writer.println(loadedProblem
312: .getAbsolutePath());
313: writer.close();
314: } catch (IOException ioe) {
315: System.out
316: .println(problemPathFileCreationError);
317: ioe.printStackTrace();
318: }
319: } else {
320: // ... or stored the zipped dir
321: logger
322: .info("Zipping and storing problem directory to archive file");
323: File zipArchive = new File(archDir,
324: loadedProblem.getName() + zipFileExt);
325: ArchiveZipper zipper = new ArchiveZipper(
326: zipArchive, loadedProblem);
327: try {
328: zipper.zipDir();
329: } catch (IOException ioe) {
330: System.out.println(zipArchiveCreationError);
331: ioe.printStackTrace();
332: }
333: }
334:
335: } else {
336: // In all other cases store a copy of the loaded problem file
337: logger
338: .info("Copying problem file into current archive directory");
339: copyFile(loadedProblem, archDir);
340: }
341: }
342:
343: try {
344: logger.info("Creating benchmark archive file...");
345: String archiveFileName = currentArchiveDir
346: + File.separator
347: + "bm"
348: + new File(currentArchiveDir).listFiles().length
349: + archiveFileExt;
350: File archiveFile = new File(archiveFileName);
351: archiveFile.createNewFile();
352: PrintWriter archiveWriter = new PrintWriter(
353: new FileWriter(archiveFile));
354: logger.info("Storing benchmark in archive: "
355: + archiveFileName);
356: archiveWriter.println(resultBenchmark.toString());
357: archiveWriter.close();
358: } catch (IOException e) {
359: System.out.println(archFileCreationError);
360: e.printStackTrace();
361: }
362: }
363:
364: logger
365: .info(">>-------------------END-----------------------<<");
366: return result;
367: }
368:
369: /** This method provides a hook for subclasses.<br>
370: * It must be implemented by subclasses which execute a concrete decision procedure.
371: *
372: * @return a <tt>DecisionProcedureResult</tt> representing the result of the execution of
373: * the decision procedure on the created and temporal stored <tt>Benchmark</tt>
374: */
375: protected abstract DecisionProcedureResult execDecProc();
376:
377: /** Returns the temporary <tt>File</tt> the translation result is stored in
378: * @return the temporary <tt>File</tt> the translation result is stored in
379: */
380: protected File getTempFile() {
381: return tempFile;
382: }
383:
384: /** Returns the <tt>Benchmark</tt> that represents the translation result
385: * @return the <tt>Benchmark</tt> representing the translation result
386: */
387: protected Benchmark getResultBenchmark() {
388: return resultBenchmark;
389: }
390:
391: /** Configures the <tt>Logger</tt> hierarchy used to log the process of translating
392: * a <tt>Goal</tt> into SMT AUFLIA syntax.
393: * <p>
394: * If the specified <tt>Level</tt> is less or equal to <tt>INFO</tt>, a log file will be
395: * created in a log directory for SMT under the ".key" directory. All logged information
396: * will be stored in this file, and not go to any inherited <tt>Appender</tt>s.<br>
397: * Otherwise, no extra file will be created and all logged information output will go to
398: * any inherited <tt>Appender</tt>.
399: * <p>
400: * If this method is not called before calling any of the other methods of this class, the
401: * configuration of the <tt>Logger</tt> will be inherited from the rootlogger
402: *
403: * @param level the <tt>Level</tt> the <tt>Logger</tt> should be configured with
404: *
405: * @throws RuntimeException if the specified <tt>Level</tt> is less or equal to <tt>INFO</tt>
406: * and the log file could not be created
407: */
408: public static void configureLogger(Level level) {
409: logger.setLevel(level);
410: if (level == Level.DEBUG || level == Level.INFO) {
411: try {
412: // Assemble file name
413: String filename = logDir + File.separator + logPrefix
414: + getCurrentDateString().substring(0, 20) + "."
415: + logSuffix;
416: // Create directory and log file, if necessary
417: new File(logDir).mkdirs();
418: new File(filename).createNewFile();
419: // add appender to logger
420: Layout layout = new PatternLayout(layoutPattern);
421: logger.addAppender(new FileAppender(layout, filename));
422: } catch (IOException e) {
423: throw new RuntimeException(logFileCreateError
424: + e.getMessage());
425: }
426: logger.setAdditivity(false);
427: }
428: }
429:
430: /* Private helper methods */
431:
432: /** Creates a copy of a given file in the given target directory
433: * @param original the <tt>File</tt> to be copied
434: * @param targetDir the <tt>File</tt> denoting the target directory
435: */
436: private final void copyFile(File original, File targetDir) {
437: File copy = new File(targetDir, original.getName());
438: PrintWriter outCopy;
439: FileReader inCopy;
440: int chunkSize = 16 * 1024;
441: char[] chunks = new char[chunkSize];
442: boolean eof = false;
443: try {
444: copy.createNewFile();
445: outCopy = new PrintWriter(new FileWriter(copy));
446: inCopy = new FileReader(loadedProblem);
447: try {
448: while (!eof) {
449: int readChars = inCopy.read(chunks);
450: if (readChars != -1)
451: outCopy
452: .println(new String(chunks, 0,
453: readChars));
454: else
455: eof = true;
456: }
457: } catch (IOException e) {
458: throw e;
459: } finally {
460: inCopy.close();
461: }
462: outCopy.close();
463: } catch (IOException ioe) {
464: System.out.println(problemFileCopyError);
465: ioe.printStackTrace();
466: }
467: }
468:
469: /** This class extends the operations on <tt>File</tt>s by providing a zip operator for
470: * directories.
471: * <p>
472: * This operator takes a <tt>File</tt> denoting a directory and zips its content into a
473: * prior specified archive <tt>File</tt>
474: *
475: * @author akuwertz
476: */
477: private class ArchiveZipper {
478:
479: /* Additional fields */
480:
481: /** The <tt>File</tt> denoting the zip archive to be created */
482: private final File archiveFile;
483:
484: /** The <tt>File</tt> denoting the directory that should be zipped */
485: private final File processedDir;
486:
487: private ZipOutputStream zipOut;
488:
489: /** The number of bytes being read from a (disc-) file into a buffer in one (java) step */
490: private int readChunkSize = 16 * 1024;
491:
492: /* Constructors */
493:
494: /** Mere constructor. Constructs and configures a new <tt>ArchiveZipper</tt> instance
495: * @param archive a <tt>File</tt> denoting the zip archive to be created
496: * @param targetDir a <tt>File</tt> denoting the directory to be zipped
497: */
498: public ArchiveZipper(File archive, File targetDir) {
499: archiveFile = archive;
500: processedDir = targetDir;
501: }
502:
503: /* Public setter and main methods */
504:
505: /** Sets the default compression method used for the target directory. It is initially set
506: * to <tt>ZipOutputStream.DEFLATED</tt>.
507: *
508: * @param method the default compression method
509: * @throws IllegalArgumentException if the specified compression method is invalid
510: *
511: * @see ZipOutputStream#setMethod(int)
512: */
513: public void setMethod(int method) {
514: zipOut.setMethod(method);
515: }
516:
517: /** Sets the compression level used for the target directory if the compression
518: * method is set to <tt>ZipOutputStream.DEFLATED</tt>. The default setting is
519: * <tt>DEFAULT_COMPRESSION</tt>
520: *
521: * @param level the compression level (0-9)
522: * @throws IllegalArgumentException if the compression level is invalid
523: *
524: * @see ZipOutputStream#setLevel(int)
525: */
526: public void setLevel(int level) {
527: zipOut.setLevel(level);
528: }
529:
530: /** Sets the number of bytes read from a file in a single processing step.<br>
531: * This parameter is set to 16k per default, and can be adjusted for disc performance reasons
532: *
533: * @param chunkSize the number of bytes read from a file in one step
534: *
535: * @throws IllegalArgumentException if <tt>chunkSize</tt> is less or equal zero
536: */
537: public void setChunkSize(int chunkSize) {
538: readChunkSize = chunkSize;
539: }
540:
541: /** Zips the target directory into the archive file
542: *
543: * @throws IOException if the specified archive file could not be created or written to or
544: * is no regular file or if the specified target directory could not be read from
545: */
546: public void zipDir() throws IOException {
547: if (!archiveFile.exists())
548: archiveFile.createNewFile();
549: zipOut = new ZipOutputStream(new FileOutputStream(
550: archiveFile));
551: processDir(processedDir, processedDir);
552: zipOut.close();
553: }
554:
555: /* Private helper methods */
556:
557: /** Processes a given directory by zipping all contained files and recursively calling
558: * itself on all contained directories
559: *
560: * @param directory the <tt>File</tt> denoting the directory to be processed
561: * @param rootDir the <tt>File</tt> denoting the root directory that should be zipped (by
562: * calling the <tt>zipDir()</tt> method)
563: *
564: * @throws IOException if an IOError occurs during writing to the zipped archive or reading
565: * from the source files
566: */
567: private final void processDir(File directory, File rootDir)
568: throws IOException {
569: File[] dirContents = directory.listFiles();
570: String parentPath = rootDir.getParent() + File.separator;
571: FileInputStream zipIn;
572: byte[] chunks = new byte[readChunkSize];
573: boolean eof = false;
574: for (int i = 0; i < dirContents.length; i++) {
575: // Calculate hierarchical name the preserve tree structure in archive
576:
577: if (dirContents[i].isDirectory()) {
578: // Process this directory recursively
579: processDir(dirContents[i], rootDir);
580: } else {
581: // Write file content into ZipEntry
582: String zipEntryName = dirContents[i].getPath()
583: .replaceFirst(parentPath, "");
584: zipOut.putNextEntry(new ZipEntry(zipEntryName));
585: zipIn = new FileInputStream(dirContents[i]);
586: eof = false;
587: while (!eof) {
588: int readChars = zipIn.read(chunks);
589: if (readChars != -1)
590: zipOut.write(chunks, 0, readChars);
591: else
592: eof = true;
593: }
594: zipOut.closeEntry();
595: }
596: }
597: }
598:
599: }
600:
601: }
|