Instruments Java classes with iContract -DBC preprocessor. + +
+Instruments Java classes with iContract
+ DBC preprocessor.
+ The task can generate a properties file for iControl,
+ a graphical user interface that lets you turn on/off assertions. iControl generates a control file that you can refer to
+ from this task using the controlfile attribute.
+
| Attribute | Description | @@ -21,37 +28,54 @@ DBC preprocessor.|||
| srcdir | -Location of the java files | +Location of the java files. | Yes | |
| instrumentdir | -Indicates where the instrumented java and class files - should go | +Indicates where the instrumented source files should go. | Yes | |
| repositorydir | -Indicates where the repository java and class files should - go | +Indicates where the repository source files should go. | Yes | |
| builddir | +Indicates where the compiled instrumented classes should go. + Defaults to the value of instrumentdir. + + NOTE: Don't use the same directory for compiled instrumented classes + and uninstrumented classes. It will break the dependency checking. (Classes will + not be reinstrumented if you change them). | +No | +||
| repositorybuilddir | +Indicates where the compiled repository classes should go. + Defaults to the value of repositorydir. | +No | +||
| pre | Indicates whether or not to instrument for preconditions.
- Defaults to true |
+ Defaults to No | ||
| post | Indicates whether or not to instrument for postconditions.
- Defaults to true |
+ Defaults to No | ||
| invariant | Indicates whether or not to instrument for invariants.
- Defaults to true |
+ Defaults to No | ||
| No | ||||
| controlfile | -The name of the control file to pass to iContract. Default - is to not pass a file | +verbosity | +Indicates the verbosity level of iContract. Any combination
+ of error*,warning*,note*,info*,progress*,debug* (comma separated) can be
+ used. Defaults to error* |
No |
| verbosity | -Indicates the verbosity level of iContract. Any combination
- of error*,warning*,note*,info*,progress*,debug* (comma separated) can be
- used. Defaults to error*,warning* |
+ quiet | +Indicates if iContract should be quiet. Turn it off if many your classes extend uninstrumented classes
+ and you don't want warnings about this. Defaults to false |
+ No | +
| updateicontrol | +If set to true, it indicates that the properties file for
+ iControl in the current directory should be updated (or created if it doesn't exist).
+ Defaults to false. |
+ No | +||
| controlfile | +The name of the control file to pass to iContract. Consider using iControl to generate the file. + Default is not to pass a file. | +Only if updateicontrol=true |
+ ||
| classdir | +Indicates where compiled (unistrumented) classes are located. + This is required in order to properly update the icontrol.properties file, not + for instrumentation. | +Only if updateicontrol=true |
+ ||
| targets | +Name of the file that will be generated by this task, which lists all the + classes that iContract will instrument. If specified, the file will not be deleted after execution. + If not specified, a file will still be created, but it will be deleted after execution. | No |
+ Note: iContract will use the java compiler indicated by the project's
+ build.compiler property. See documentation of the Javac task for
+ more information. Nested includes and excludes are also supported.
Example:
+ Note: iContract will use the java compiler indicated by the project's -build.compiler property. See documentation for the Javac task for
+ build.compiler property. See documentation of the Javac task for
more information.
+
+ Nested includes and excludes can be done very much the same way as any subclass
+ of MatchingTask.
Example:
- <!-- =================================================================== -->
- <!-- Instruments source codes with iContract -->
- <!-- =================================================================== -->
- <target name="instrument" depends="compile">
- <icontract
- srcdir="${build.src}"
- instrumentdir="${instrumented.dir}"
- repositorydir="${repository.dir}"
- >
- <classpath>
- <fileset dir="./lib">
- <include name="*.jar"/>
- </fileset>
- </classpath>
- </icontract>
- </target>
+ <icontract
+ srcdir="${build.src}"
+ instrumentdir="${build.instrument}"
+ repositorydir="${build.repository}"
+ builddir="${build.instrclasses}"
+ updateicontrol="true"
+ classdir="${build.classes}"
+ controlfile="control"
+ targets="targets"
+ verbosity="error*,warning*"
+ quiet="true"
+ >
+ <classpath refid="compile-classpath"/>
+ </icontract>
truetrue unless controlfile is specified, in which case it
+ * defaults to false.
* truetrue unless controlfile is specified, in which case it
+ * defaults to false.
* truetrue unless controlfile is specified, in which case it
+ * defaults to false.
* error*,warning*,note*,info*,progress*,debug* (comma separated) can be
* used. Defaults to error*falsefalse.
+ * updateicontrol=trueupdateicontrol=truebuild.compiler property. See documentation for the Javac task for
+ * build.compiler property. See documentation of the Javac task for
* more information.
+ *
+ * Nested includes and excludes are also supported.
*
* Example:
- * *
- * <!-- =================================================================== -->
- * <!-- Instruments source codes with iContract -->
- * <!-- =================================================================== -->
- * <target name="instrument" depends="compile">
- * <icontract
- * srcdir="${build.src}"
- * instrumentdir="${instrumented.dir}"
- * repositorydir="${repository.dir}"
- * updateicontrol="true"
- * >
- * <classpath>
- * <fileset dir="./lib">
- * <include name="*.jar"/>
- * </fileset>
- * </classpath>
- * </icontract>
- * </target>
+ * <icontract
+ * srcdir="${build.src}"
+ * instrumentdir="${build.instrument}"
+ * repositorydir="${build.repository}"
+ * builddir="${build.instrclasses}"
+ * updateicontrol="true"
+ * classdir="${build.classes}"
+ * controlfile="control"
+ * targets="targets"
+ * verbosity="error*,warning*"
+ * quiet="true"
+ * >
+ * <classpath refid="compile-classpath"/>
+ * </icontract>
*
*
*/
-public class IContract extends Task {
+public class IContract extends MatchingTask {
+
+ private static final String ICONTROL_PROPERTIES_HEADER =
+ " You might want to set classRoot to point to your normal compilation class root directory.";
+
+ private static final String ICONTROL_PROPERTIES_MESSAGE =
+ "You should probably modify icontrol.properties' classRoot to where comiled (uninstrumented) classes go.";
/** \ on windows, / on linux/unix */
private static final String ps = System.getProperty( "path.separator" );
@@ -199,12 +250,18 @@ public class IContract extends Task {
/** source file root */
private File srcDir = null;
- /** instrumentation root */
+ /** instrumentation src root */
private File instrumentDir = null;
- /** repository root */
+ /** instrumentation build root */
+ private File buildDir = null;
+
+ /** repository src root */
private File repositoryDir = null;
+ /** repository build root */
+ private File repBuildDir = null;
+
/** classpath */
private Path classpath = null;
@@ -214,6 +271,9 @@ public class IContract extends Task {
/** The -v option */
private String verbosity = "error*";
+ /** The -q option */
+ private boolean quiet = false;
+
/** Indicates whether or not to use internal compilation */
private boolean internalcompilation = false;
@@ -222,16 +282,19 @@ public class IContract extends Task {
/** Indicates whether or not to instrument for preconditions */
private boolean pre = true;
+ private boolean preModified = false;
/** Indicates whether or not to instrument for postconditions */
private boolean post = true;
+ private boolean postModified = false;
/** Indicates whether or not to instrument for invariants */
private boolean invariant = true;
+ private boolean invariantModified = false;
/** Indicates whether or not to instrument all files regardless of timestamp */
// can't be explicitly set, is set if control file exists and is newer than any source file
- private boolean instrumentall = true;
+ private boolean instrumentall = false;
/**
* Indicates the name of a properties file (intentionally for iControl) where the classpath
@@ -239,6 +302,11 @@ public class IContract extends Task {
*/
private boolean updateIcontrol = false;
+ /**
+ * Regular compilation class root
+ */
+ private File classDir = null;
+
/**
* Sets the source directory
*
@@ -248,6 +316,15 @@ public class IContract extends Task {
this.srcDir = srcDir;
}
+ /**
+ * Sets the class directory (uninstrumented classes)
+ *
+ * @param srcDir the source directory
+ */
+ public void setClassdir( File classDir ) {
+ this.classDir = classDir;
+ }
+
/**
* Sets the instrumentation directory
*
@@ -255,15 +332,39 @@ public class IContract extends Task {
*/
public void setInstrumentdir( File instrumentDir ) {
this.instrumentDir = instrumentDir;
+ if ( this.buildDir == null ) {
+ setBuilddir( instrumentDir );
+ }
+ }
+
+ /**
+ * Sets the build directory for instrumented classes
+ *
+ * @param buildDir the build directory
+ */
+ public void setBuilddir( File buildDir ) {
+ this.buildDir = buildDir;
}
/**
- * Sets the repository directory
+ * Sets the build directory for repository classes
*
* @param repositoryDir the source directory
*/
public void setRepositorydir( File repositoryDir ) {
this.repositoryDir = repositoryDir;
+ if( this.repBuildDir == null ) {
+ setRepbuilddir( repositoryDir );
+ }
+ }
+
+ /**
+ * Sets the build directory for instrumented classes
+ *
+ * @param buildDir the build directory
+ */
+ public void setRepbuilddir( File repBuildDir ) {
+ this.repBuildDir = repBuildDir;
}
/**
@@ -273,6 +374,7 @@ public class IContract extends Task {
*/
public void setPre( boolean pre ) {
this.pre = pre;
+ preModified = true;
}
/**
@@ -282,6 +384,7 @@ public class IContract extends Task {
*/
public void setPost( boolean post ) {
this.post = post;
+ postModified = true;
}
/**
@@ -291,15 +394,16 @@ public class IContract extends Task {
*/
public void setInvariant( boolean invariant ) {
this.invariant = invariant;
+ invariantModified = true;
}
/**
* Sets the Throwable (Exception) to be thrown on assertion violation
*
- * @param clazz the Throwable class
+ * @param clazz the fully qualified Throwable class name
*/
- public void setFailthrowable( Class clazz ) {
- this.failThrowable = clazz.getName();
+ public void setFailthrowable( String clazz ) {
+ this.failThrowable = clazz;
}
/**
@@ -307,35 +411,40 @@ public class IContract extends Task {
* error*,warning*,note*,info*,progress*,debug* (comma separated)
* can be used. Defaults to error*,warning*
*
- * @param clazz the Throwable class
+ * @param verbosity verbosity level
*/
public void setVerbosity( String verbosity ) {
this.verbosity = verbosity;
}
/**
- * Turns on/off internal compilation.
- * build.compiler will be used, defaulting to javac,
- * and run in a separate VM.
+ * Tells iContract to be quiet.
*
- * @param internalcompilation set to true for internal compilation
+ * @param quiet true if iContract should be quiet.
*/
- /* FIXME: Doesn't work
- public void setInternalcompilation( boolean internalcompilation ) {
- this.internalcompilation = internalcompilation;
- }
- */
+ public void setQuiet( boolean quiet ) {
+ this.quiet = quiet;
+ }
+
+ /**
+ * Sets the name of the file where targets will be written.
+ * That is the file that tells iContract what files to process.
+ *
+ * @param targets the targets file name
+ */
+ public void setTargets( File targets ) {
+ this.targets = targets;
+ }
/**
* Sets the control file to pass to iContract.
*
- * @param clazz the Throwable class
+ * @param controlFile the control file
*/
public void setControlfile( File controlFile ) {
+ if( !controlFile.exists() ) {
+ log( "WARNING: Control file " + controlFile.getAbsolutePath() + " doesn't exist. iContract will be run without control file." );
+ }
this.controlFile = controlFile;
}
@@ -387,6 +496,25 @@ public class IContract extends Task {
preconditions();
scan();
if( dirty ) {
+
+ // turn off assertions if we're using controlfile, unless they are not explicitly set.
+ boolean useControlFile = (controlFile != null) && controlFile.exists();
+ if( useControlFile && !preModified ) {
+ pre = false;
+ }
+ if( useControlFile && !postModified ) {
+ post = false;
+ }
+ if( useControlFile && !invariantModified ) {
+ invariant = false;
+ }
+ // issue warning if pre,post or invariant is used together with controlfile
+ if( ( pre || post || invariant ) && controlFile != null ) {
+ log( "WARNING: specifying pre,post or invariant will override control file settings" );
+ }
+
+
+
// We want to be notified if iContract jar is missing. This makes life easier for the user
// who didn't understand that iContract is a separate library (duh!)
getProject().addBuildListener( new IContractPresenceDetector() );
@@ -397,15 +525,19 @@ public class IContract extends Task {
Mkdir mkdir = (Mkdir) project.createTask( "mkdir" );
mkdir.setDir( instrumentDir );
mkdir.execute();
+ mkdir.setDir( buildDir );
+ mkdir.execute();
mkdir.setDir( repositoryDir );
mkdir.execute();
- // Set the compiler
- setCompiler();
-
// Set the classpath that is needed for regular Javac compilation
Path baseClasspath = createClasspath();
+ // Might need to add the core classes if we're not using Sun's Javac (like Jikes)
+ String compiler = project.getProperty("build.compiler");
+ ClasspathHelper classpathHelper = new ClasspathHelper( compiler );
+ classpathHelper.modify( baseClasspath );
+
// Create the classpath required to compile the sourcefiles BEFORE instrumentation
Path beforeInstrumentationClasspath = ((Path) baseClasspath.clone());
beforeInstrumentationClasspath.append( new Path( getProject(), srcDir.getAbsolutePath() ) );
@@ -415,12 +547,14 @@ public class IContract extends Task {
afterInstrumentationClasspath.append( new Path( getProject(), instrumentDir.getAbsolutePath() ) );
afterInstrumentationClasspath.append( new Path( getProject(), repositoryDir.getAbsolutePath() ) );
afterInstrumentationClasspath.append( new Path( getProject(), srcDir.getAbsolutePath() ) );
+ afterInstrumentationClasspath.append( new Path( getProject(), buildDir.getAbsolutePath() ) );
// Create the classpath required to automatically compile the repository files
Path repositoryClasspath = ((Path) baseClasspath.clone());
repositoryClasspath.append( new Path( getProject(), instrumentDir.getAbsolutePath() ) );
repositoryClasspath.append( new Path( getProject(), srcDir.getAbsolutePath() ) );
repositoryClasspath.append( new Path( getProject(), repositoryDir.getAbsolutePath() ) );
+ repositoryClasspath.append( new Path( getProject(), buildDir.getAbsolutePath() ) );
// Create the classpath required for iContract itself
Path iContractClasspath = ((Path) baseClasspath.clone());
@@ -428,6 +562,7 @@ public class IContract extends Task {
iContractClasspath.append( new Path( getProject(), srcDir.getAbsolutePath() ) );
iContractClasspath.append( new Path( getProject(), repositoryDir.getAbsolutePath() ) );
iContractClasspath.append( new Path( getProject(), instrumentDir.getAbsolutePath() ) );
+ iContractClasspath.append( new Path( getProject(), buildDir.getAbsolutePath() ) );
// Create a forked java process
Java iContract = (Java) project.createTask( "java" );
@@ -440,17 +575,18 @@ public class IContract extends Task {
StringBuffer args = new StringBuffer();
args.append( directiveString() );
args.append( "-v" ).append( verbosity ).append( " " );
- args.append( "-b" ).append( icCompiler ).append( "\"" ).append( " -classpath " ).append( beforeInstrumentationClasspath ).append( "\" " );
- args.append( "-c" ).append( icCompiler ).append( "\"" ).append( " -classpath " ).append( afterInstrumentationClasspath ).append( "\" " );
- args.append( "-n" ).append( icCompiler ).append( "\"" ).append( " -classpath " ).append( repositoryClasspath ).append( "\" " );
+ args.append( "-b" ).append( "\"" ).append( icCompiler ).append( " -classpath " ).append( beforeInstrumentationClasspath ).append( "\" " );
+ args.append( "-c" ).append( "\"" ).append( icCompiler ).append( " -classpath " ).append( afterInstrumentationClasspath ).append( " -d " ).append( buildDir ).append( "\" " );
+ args.append( "-n" ).append( "\"" ).append( icCompiler ).append( " -classpath " ).append( repositoryClasspath ).append( "\" " );
args.append( "-d" ).append( failThrowable ).append( " " );
args.append( "-o" ).append( instrumentDir ).append( File.separator ).append( "@p" ).append( File.separator ).append( "@f.@e " );
args.append( "-k" ).append( repositoryDir ).append( File.separator ).append( "@p " );
- args.append( instrumentall ? "-a " : "" ); // reinstrument everything if controlFile exists and is newer than source
+ args.append( quiet ? "-q " : "" );
+ args.append( instrumentall ? "-a " : "" ); // reinstrument everything if controlFile exists and is newer than any class
args.append( "@" ).append( targets.getAbsolutePath() );
iContract.createArg().setLine( args.toString() );
-// System.out.println( "JAVA -classpath " + iContractClasspath + " com.reliablesystems.iContract.Tool " + args.toString() );
+//System.out.println( "JAVA -classpath " + iContractClasspath + " com.reliablesystems.iContract.Tool " + args.toString() );
// update iControlProperties if it's set.
if( updateIcontrol ) {
@@ -460,18 +596,21 @@ public class IContract extends Task {
} catch( IOException e ) {
log( "File icontrol.properties not found. That's ok. Writing a default one." );
}
- iControlProps.setProperty( "classRoot", srcDir.getAbsolutePath() );
- iControlProps.setProperty( "classpath", iContractClasspath.toString() );
- iControlProps.setProperty( "controlFile", "control" );
+ iControlProps.setProperty( "sourceRoot", srcDir.getAbsolutePath() );
+ iControlProps.setProperty( "classRoot", classDir.getAbsolutePath() );
+ iControlProps.setProperty( "classpath", afterInstrumentationClasspath.toString() );
+ iControlProps.setProperty( "controlFile", controlFile.getAbsolutePath() );
+ iControlProps.setProperty( "targetsFile", targets.getAbsolutePath() );
try { // to read existing propertiesfile
- iControlProps.store( new FileOutputStream( "icontrol.properties" ), "Edit the classRoot and controlfile properties if you like" );
- log( "Updated file icontrol.properties." );
+ iControlProps.store( new FileOutputStream( "icontrol.properties" ), ICONTROL_PROPERTIES_HEADER );
+ log( "Updated icontrol.properties" );
} catch( IOException e ) {
log( "Couldn't write icontrol.properties." );
}
}
+ // do it!
int result = iContract.executeJava();
if( result != 0 ) {
if( iContractMissing ) {
@@ -481,7 +620,8 @@ public class IContract extends Task {
}
throw new BuildException( "iContract instrumentation failed. Code=" + result );
}
- } else {
+
+ } else { // not dirty
//log( "Nothing to do. Everything up to date." );
}
}
@@ -502,36 +642,54 @@ public class IContract extends Task {
if (repositoryDir == null) {
throw new BuildException( "repositorydir attribute must be set!", location );
}
+ if (updateIcontrol == true && classDir == null) {
+ throw new BuildException( "classdir attribute must be specified when updateicontrol=true!", location );
+ }
+ if( updateIcontrol == true && controlFile == null ) {
+ throw new BuildException( "controlfile attribute must be specified when updateicontrol=true!", location );
+ }
}
/**
* Verifies whether any of the source files have changed. Done by comparing date of source/class files.
- * The whole lot is "dirty" if at least one source file is newer than the instrumented files. If not dirty,
- * iContract will not be executed.
+ * The whole lot is "dirty" if at least one source file or the control file is newer than the instrumented
+ * files. If not dirty, iContract will not be executed.
*