JSure User Guide

How to use and configure the JSure Eclipse client

The authors and publishers have taken care in the preparation of this documentation, but make no expressed or implied warranty of any kind and assume no responsibility for errors and omissions. No liability is assumed for incidental or consequential damages in connection with or arising out of the use of the information or programs herein.

Version 5.7.1—November 2015


Table of Contents

Preface
1. Audience
2. Contact information
1. Getting started
1.1. Introduction
1.2. Quick start
1.2.1. Installing Your License
1.2.2. Annotating and Assuring Your Code
1.3. Tutorials
1.3.1. Verifying BoundedFIFO
1.3.2. Verifying annotations from the book Java Concurrency In Practice
1.3.3. Verifying PlanetBaron
1.3.4. Scanning code using Ant
1.3.5. Uncovering a bug in java.util.logging
1.3.6. Verifying util.concurrent
1.3.7. Effective effects
1.3.8. Verifying non-null references
2. Reference
2.1. The JSure Menu
2.2. The Code Verification perspective
2.2.1. Switching to the Perspective
2.2.2. The JSure Scans view
2.2.3. The Modeling Problems view
2.2.4. The Verification Status view
2.2.5. The Verification Explorer view
2.2.6. The Analysis-Enabled Metrics view
2.2.7. The Proposed Annotation view
2.2.8. The Library Annotation Explorer view
2.2.9. The XML Library Annotation editor
2.2.10. The JSure Quick Search view
2.2.11. The JSure Historical Source view
2.3. JSure Preferences
2.3.1. JSure
2.3.2. Flashlight Generated Lock Models
2.3.3. Uninteresting Package Filtering
2.3.4. Verifying Analysis Selection
2.4. SureLogic tool properties file
2.5. Using Ant
2.5.1. jsure-scan task
2.6. Using Maven
2.7. License management
2.8. Bugs and tips
3. Release notes
3.1. JSure version 5.6.1
3.1.1. New and Noteworthy
3.2. JSure version 5.6.0
3.2.1. New and Noteworthy

List of Figures

1.1. The menu option to install a license for JSure
1.2. The SureLogic license management dialog
1.3. Opening the Code Verification Perspective
1.4. The Code Verification Perspective
1.5. Iconography used for reporting JSure results
1.6. Menu item to install tutorial projects into your workspace
1.7. Adding tutorial projects to your workspace
1.8. The PlanetBaron PlayerUI for Laurel
1.9. The ChatTestClient
1.10. Initial assurance results for PlanetBaron
1.11. Initial modeling problems for PlanetBaron
1.12. Expanded precondition results
1.13. Console output from scanning PlanetBaron with Ant inside Eclipse
1.14. Successful scan import
1.15. The concurrent exercise program to cause the library bug to throw a NullPointerException
1.16. Class Hierarchy rooted at SynchronizedVariable
2.1. The JSure menu
2.2. The Verify dialog box
2.3. The Add/Update Promises Library dialog box
2.4. The Open Library Annotations search dialog
2.5. The Import JSure Ant/Maven Scan dialog box
2.6. The Save Promises Library dialog box
2.7. The Save Documentation dialog box
2.8. The JSure Scans view
2.9. The JSure Scans view menu
2.10. The JSure Scans context menu
2.11. The Modeling Problems view
2.12. The Modeling Problems view context menu
2.13. The Modeling Problems view menu
2.14. The Verification Status view
2.15. The Verification Status view menu
2.16. The Verification Explorer view
2.17. The Verification Explorer view menu
2.18. The Analysis-Enabled Metrics view
2.19. The Analysis-Enabled Metrics view menu
2.20. The Proposed Annotation view
2.21. The Proposed Annotation view context menu adding two proposals to the code
2.22. The Proposed Annotation view menu
2.23. The Library Annotation Explorer view
2.24. The Library Annotation Explorer view showing only user-added/modified library annotations
2.25. The Library Annotation Explorer view menu
2.26. The XML Library Annotation editor showing the annotations on java.lang.Object
2.27. The JSure Quick Search view
2.28. The JSure Historical Source view
2.29. The JSure preferences pane
2.30. The Flashlight Generated Lock Models preferences pane
2.31. The Uninteresting Package Filtering preferences pane
2.32. The Verifying Analysis Selection preferences pane
2.33. Use of the surelogic-tools.properties to exclude the test source folder of the timingframework-core project
2.34. Use of the surelogic-tools.properties to exclude packages from the timingframework-swing project
2.35. The SureLogic license management dialog
2.36. Dialog warning that the installed JSure license is about to expire
2.37. Menu items to send bugs and tips to SureLogic
2.38. Dialog allowing the user to enter a tip to improve JSure
2.39. Dialog allowing the user to enter a problem report about JSure
2.40. Dialog allowing the user to send library annotations to SureLogic

Preface

1. Audience

This document is intended for Java developers who want to use the JSure tool within the Eclipse Java IDE. We assume that the reader understands both the Java programming language and the use of Eclipse for Java development.

2. Contact information

For technical support or other questions, please contact:

5808 Forbes Avenue, Pittsburgh, PA 15217-1602

Chapter 1. Getting started

1.1. Introduction

What is JSure? JSure is a model-based static analysis tool that helps developers answer the question “Are my threads accessing shared state in a safe way?” JSure provides positive assurance that correct locks are held when shared state is accessed. The tool uses a sound analysis, i.e., it is not based upon a rule-based analysis. This enables programmers to develop a high confidence that their code is “thread safe,” that is, that it satisfies state consistency requirements.

More specifically, JSure verifies that Java class implementations are consistent with programmer design intent as expressed using Java annotations. Annotations make JSure scalable: Unannotated classes have no design intent to assure. Annotations may be inserted incrementally in critical classes. Later, additional annotations may be added as required to assure additional classes. Verification results are, however, whole program: some annotations place requirements on class clients, and thus, the behavior of a client class is assured even if that class has no annotations of its own.

The JSure analysis engine is integrated into the Eclipse Java IDE. This enables JSure scans to be run in the background within Eclipse and verification results to be examined by the tool user within the widely-used Eclipse Java IDE.

1.2. Quick start

This section will quickly get you started with JSure. It describes how to install JSure into your Eclipse, how to install a license file that allows you to use JSure. It also describes how to enable JSure assurance of a Java project, and how to examine the assurance results.

1.2.1. Installing Your License

This section assumes that you have installed JSure. If you see a JSure menu item on your Eclipse main menu then you can assume JSure has been installed properly.

You need to install a license to use JSure. If you do not have a license file that was sent to you by SureLogic visit http://surelogic.com to obtain one. To install the license select Manage SureLogic Licenses from the JSure menu as shown in Figure 1.1

Figure 1.1. The menu option to install a license for JSure

The menu option to install a license for JSure

This will cause the Manage SureLogic Licenses window to appear as shown in Figure 1.2. Select the Install from File button to install your license if you saved it as a file on your disk. Select the Install from Clipboard button to install your license if you copied it from an email message.

Figure 1.2. The SureLogic license management dialog

The SureLogic license management dialog

JSure will not disrupt your Eclipse installation if a license for it is not installed, however, it will not allow you to use JSure functionality. We will assume from this point on that you have installed your license. For more information, see Section 2.7

1.2.2. Annotating and Assuring Your Code

For the impatient, this section provides a “bare-bones” description of how to prepare a Java project for verification by JSure.

JSure compares Java code with models of programmer design intent expressed using a set of Java annotation types. The tool verifies model-code consistency. To use JSure with your code, your project must be able to reference the SureLogic annotation types declared in package com.surelogic. The SureLogic annotation types are bundled together in promises-version.jar. This file must be on the build path of your project for the annotations be to used. As described below, the simplest way to add this JAR file to the project and its build path is to allow JSure to do it for you.

To manually add/update the JAR file select JSureAdd/Update Promises Library from the Eclipse main menu as shown below.

This action will prompt you through the process of adding or updating the JAR to your project's classpath. It does not scan that project (as described below).

You could also save the JSure JAR file to your disk and manually setup your project's classpath. To do this you would select JSureSave Promises Library As... from the Eclipse main menu. This command will prompt you where to save the JAR file to your disk. Then you can manually add it to any project's classpath you wish.

1.2.2.1. Scanning Your Projects with JSure

JSure can assure any number of projects at the same time time. Analysis by the tool is performed on a copy of your code in the background so that your work is not disrupted through the use of JSure.

To scan one or more of your projects with JSure select JSureVerify from the Eclipse main menu as shown below. Using the menu can become tedious in real tool use so this command is associated with the keyboard shortcut Ctrl+Alt+Shift+V. This keyboard shortcut is worth remembering to make JSure easier to use. In addition, the icon on the Eclipse toolbar can be used to start a JSure scan.

This action will open the dialog shown below.

This dialog allows you to select which projects are to be analyzed by JSure

When a project is scanned, JSure does not check to see if promises Jar file is on the project’s build path. Therefore make sure you add it to the project's you want to verify.

1.2.2.2. Excluding Your Test Code From a Scan

It is possible to exclude test code from a JSure scan by creating a surelogic-tools.properties file at the root of each project that contains test code.

For example, the screenshot above shows the use of the surelogic-tools.properties to exclude the test source folder of timingframework-core Java project. For more information on how to setup a surelogic-tools.properties file see Section 2.4.

1.2.2.3. Viewing Assurance Results

JSure scans run in the background on a copy of your code. Therefore you may safely continue your work while a JSure scan is running. When a scan is completed the results are displayed in the Verification Status and JSure Quick Search views. The easiest way to open this view is to switch to the Code Verification perspective. The first time a scan is completed on any project in the workspace JSure prompts you about switching to the Code Verification perspective:

Choosing Yes will immediately switch Eclipse to the perspective. Choosing No will leave the current Eclipse window in whatever perspective it is currently in. If you check Remember my decision and press Yes then whenever you focus verification on a project, Eclipse will switch to the perspective without asking you first.

You can also switch to the Code Verification perspective by selecting JSureOpen Code Verification Perspective. See Figure 1.3.

Figure 1.3. Opening the Code Verification Perspective

Opening the Code Verification Perspective

The code verification perspective defaults to showing the views shown in Figure 1.4.

Figure 1.4. The Code Verification Perspective

The Code Verification Perspective

The JSure Scans view lists all the scans you have run on your code. This view lets you select which scan to examine. Checking a scan updates all the other views with that scan's data. You can check a different at any time. This view also lets you delete older scans by selecting them and choosing Delete from the view's context menu.

The Modeling Problems view which tells you if any of the annotations in your code do not make sense to JSure. This view lists each bad annotation so that the programmer can fix them. If the icon for a report in the view is (note the + to the upper-right) then JSure "thinks" it can resolve the modeling problem with an automatic edit. Select the problem and choose Annotate Code To Fix... from the view's context menu and the tool will automatically fix the modeling problem. Multiple problems can be selected at one time. The edit is previewed before it is made to the code.

The Verification Status view is divided into sections to show the results of assuring different classes of design intent, such as effects, and concurrency, as well as showing less specific suggestions and warnings. The Verification Explorer view shows similar information but displays results in the context of Java declarations, e.g., by project, class, field, etc.

The icons shown in the Verification Status and Verification Explorer views have meaning. The table shown in Figure 1.5. is a quick reference about what each icon and decorator means. This table can be brought up as a dialog in JSure by pressing the toolbar button in the Verification Status and Verification Explorer views.

Figure 1.5. Iconography used for reporting JSure results

ImageSemantics
Iconography used for reporting JSure resultsAn annotation or promise about the code
Iconography used for reporting JSure resultsConsistent analysis result
Iconography used for reporting JSure resultsInconsistent analysis result
Iconography used for reporting JSure resultsInconsistent analysis result due to a user-specified execution timeout
Iconography used for reporting JSure resultsInconsistent analysis result vouched for by the programmer using @Vouch
Iconography used for reporting JSure resultsConsistent verification judgment
Iconography used for reporting JSure resultsUnused choice with consistent verification judgment
Iconography used for reporting JSure resultsInconsistent verification judgment
Iconography used for reporting JSure resultsUnused choice with inconsistent verification judgment
Iconography used for reporting JSure resultsTrusted promise decorator – the annotation is not checked by analysis
Iconography used for reporting JSure resultsRed dot – an @Vouch or trusted promise is used in the verification proof
Iconography used for reporting JSure resultsVirtual promise – created by @Promise
Iconography used for reporting JSure resultsInformational message – a possible next modeling step
Iconography used for reporting JSure resultsWarning message – a possible next modeling step
Iconography used for reporting JSure resultsFolder of results
Iconography used for reporting JSure resultsDelta – something in the tree has changed since the last scan
Highlights something new or changed since the last scan
Highlights an obsolete result only in the last scan
 Standard Eclipse images are used to represent Java declarations

The Proposed Annotations view lists annotations, also called promises about your code, that the tool has inferred you may want to add to your code. The tool uses your existing annotations and the verification results to generate this list of proposals. The tool will automatically add these to the code if you select the proposal and select Annotate Code... from the view's context menu. The edit is previewed before it is made to the code. The view presents its proposals in either a tree, showing the proposal in the context of the Java declaration it will annotate. The proposals listed in this view can save time in modeling, however, you should double check that the proposed promise represents actual design intent about your code.

The Library Annotation Explorer view shows all the annotations made on library code, binary code in Jar files, via special JSure XML files that indirectly annotate this code. You can examine these annotations and use them to open the library annotation editor (an editor provided by JSure) to add/modify annotations on Jar files.

The JSure Quick Search view allows you to query the scan results in an ad hoc manner. You can setup a series of filters on the results to focus on the particular scan results that are of immediate interest. Selecting a result brings up the code location of that result in your code. The context menu for a result can be used to highlight the same result in the Verification Status view.

FilterSemantics
Analysis ResultAllows you to filter the results by the type of analysis result reported by the tool's verifying analyses. An analysis result is a finding reported by one of the JSure tool's verifying analyses. These results form the basis used to prove that an annotation is consistent, i.e., a verification judgment about a promise. This filter could be used to quickly find all inconsistent analysis results so that you can work to eliminate them.
AnnotationAllows you to filter the results by annotation. This filter could be used to quickly find all @RegionLock annotations in your code.
Java PackageAllows you to filter the results to a particular set of Java packages.
Java TypeAllows you to filter the results to a particular set of Java types, e.g., class, interface, enum.
ProjectAllows you to filter the results to a particular set of Eclipse projects.
Verification JudgmentAllows you to filter the results by the verification judgment on an annotation. This filter could be used to find all consistent promises or find promises with a "red-dot" (contingent verification judgments).

The JSure Quick Search view is very flexible and allows you to chain many filters together before you Show a list of results. You can also save queries that you find useful via the toolbar at the bottom of the view.

The JSure Historical Source view is shown to the right of the Java editor at the bottom of the perspective. This view shows you what your source code looked like when JSure scanned your code. Because the scan you are examining may have been run at any time in the past, your may have changed since that time. This view helps you understand the tool results by showing the code as it was when the scan was run.

1.3. Tutorials

This section contains tutorials demonstrating the use of JSure and its program annotations to assure the correct use of locks in concurrent Java programs. The first two tutorials use small closed-world examples to demonstrate annotating code and using JSure, starting with no annotations at all. The remaining tutorials begin with a partially annotated program, and demonstrate more sophisticated concepts such as support for java.util.concurrent reader–writer locks.

Figure 1.6. Menu item to install tutorial projects into your workspace

Menu item to install tutorial projects into your workspace

These tutorials assume that you have installed JSure. If you see a JSure menu item on your Eclipse main menu than you can assume it has been installed properly. To follow along with the tutorials you will also need to add the tutorial projects to your workspace. From the Eclipse main menu, choose JSureInstall Tutorial Projects and add the projects to your workspace as displayed in Figure 1.6 and Figure 1.7.

Figure 1.7. Adding tutorial projects to your workspace

Adding tutorial projects to your workspace

[Note]Several of the imported projects will not compile in Eclipse

The JSureTutorial_PlanetBaron, JSureTutorial_EffectiveEffects, and JSureTutorial_NonNull projects will not compile without errors until you add the Promises Library Jar into the build path of each project. A few of the tutorial projects, such as JSureTutorial_ThreadSafeAndImmutable, will compile without errors because no annotations have been placed into the projects yet.

Next, we need to add the SureLogic annotation types in the package com.surelogic to each tutorial project's class path. This is most easily done by allowing JSure to do it for us:

  1. Select JSureAdd/Update Promises Library from the Eclipse menu.

  2. Press Select All in the dialog which appears. If you did not start with an empty Eclipse workspace, you may want to uncheck any of your own projects that appear in this dialog.

    Then press OK to add the promises Jar to each project's classpath.

All the tutorial projects should now compile in your Eclipse workspace without errors.

1.3.1. Verifying BoundedFIFO

In this tutorial we walk through the complete assurance of the JSureTutorial_BoundedFIFO project using JSure. Specifically, we assure both the implementation and usage of a simple class. That is, we demonstrate that it's not always enough to assure the implementation of a class: sometimes the clients of a class must conform to a specific behavior as well. This example focuses on two classes (plus one auxiliary class):

  • BoundedFIFOThe “thread safe” class. This class is taken “as is” from the Apache Log4J project.

  • BlockingFIFOThe client code. We wrote this class based on actual client code in the Apache Log4J project.

  • LoggingEventThe class of objects stored in the queue. This class is not interesting, and is merely a placeholder for queue objects.

In addition to showing the basic usage of JSure with Eclipse, this example shows off the JSure annotations @RegionLock, @RequiresLock, @Borrowed, @Unique, and @Promise.

After completely assuring the project, we show how the annotated model for BoundedFIFO can be augmented by named regions of state using the annotations @Region, @InRegion, and @UniqueInRegion.

1.3.1.1. Declaring Protected State

The BoundedFIFO class is a buffer meant to be shared between two threads. It obviously must be made thread-safe. The usual assumption is that an object protects its own state, and we intend for that to be the case here. Declare this design intent by adding a @RegionLock annotation to the class BoundedFIFO (and not to BlockingFIFO):

@RegionLock("BufLock is this protects Instance")
public class BoundedFIFO {
  …
}

[Note]Don't forget to import the annotation type

The annotation type RegionLock (and any other JSure annotation used in these examples) must be imported before the class name can be resolved by the compiler. There are a number of ways you can do this:

  • You can manually add import com.surelogic.RegionLock, or more generally, import com.surelogic.* to the list of imports at the top of BoundedFIFO.java.

  • If you are typing the annotation into the editor you can use the Eclipse “content assist” feature as you are typing the name RegionLock. The Java editor will automatically add the correct import clauses or enter the fully qualified name of the class, depending on your Eclipse preferences.

  • If you used copy-and-paste to copy the annotation from this tutorial and paste it into the Eclipse editor you can use the Eclipse “quick fix” feature to insert the import clause.

Adding annotations is not enough to see assurance results—you need to scan the project. To scan the project

  • Choose JSureVerify Project from the Eclipse main menu. You can also use the keyboard shortcut Ctrl+Alt+Shift+V.

  • This will bring up the dialog shown below which allows you to select the set of projects you want to scan from the set of open Java projects in your Eclipse workspace.

    Check JSureTutorial_BoundedFIFO and press OK to start a scan. A balloon notification will appear telling you that the scan has been started in the background and that you will be notified when the scan has been completed.

  • The scan should not take long to complete. When it finishes you will be prompted to switch to the Code Verification perspective.

    Choose Yes because we want to examine the scan results.

Switching to the Code Verification perspective at this point should look something like this:

We begin our examination of the results using the Verification Status view. This view shows the results of assuring model–code consistency. It is similar to a file system explorer, but instead of showing directories and files, it shows the chain of evidence used to build a verification judgment—consistent or inconsistent—about each of your annotations.

By digging into the Concurrency results, we see two results. First, notice that the lock model java.lang.Object.MUTEX is initially unassured. This intrinsic lock model is declared on java.lang.Object and defines the need to hold a lock when invoking the wait() and notify() methods on any Java object. The lock model declares this, the object itself, as the lock that protects the wait-notify queue, and requires that the lock be held before the wait() and notify() methods may be invoked. The fact that this model is unassured indicates that somewhere in the code JSure is unable to prove that a lock is held on an object that either wait() or notify() is invoked on. We will discover this finding to be accurate later in this tutorial.

Second, we note the single annotation we added to the code. Verification of this annotation by JSure produces a concurrency result indicating that the annotation is not assured, and a few warnings. There are 27 unprotected field accesses for BufLock, and no protected field accesses:

Opening up the results tree further we see that JSure identifies each location in the code where state is accessed without holding the correct lock:

Selecting any of the results in the Verification Status view focuses an Eclipse Java editor and the JSure Historical Source view on the offending line of code. Let us view the line of code from the assurance failure at line 52 by clicking on Lock "<this>.BufLock" not held when accessing this.numElts. Eclipse opens an editor window for BoundedFIFO and highlights the field expression numElts on line 52. In addition the JSure Historical Source view shows the same code because the current Java code and the code when the scan was performed are the same.

[Tip]How to show line numbers in the Eclipse Java editor

You can enable line numbering in the Java editor by right-clicking in the editor gutter and selecting Show Line Numbers or by going to GeneralEditorsText Editors in the Eclipse Preferences dialog box, and selecting Show line numbers in the preference pane.

This state access is one of many in the get() method. A quick inspection of the method shows that it does not acquire any locks. In fact, if you scroll through the rest of the BoundedFIFO you will see that no locks are acquired anywhere. There are several explanations for this situation, including

  1. The class is broken and needs to have synchronization statements added to it.

  2. The class expects the locks to acquired by users of instances of the class.

  3. The class uses some other technique to prevent data races.

It is very possible that 1 is the case. Another quick inspection of the code suggests that 3 is probably not the case. We need to inspect the clients of BoundedFIFO to consider 2.

We can investigate the clients of BoundedFIFO by seeing where the methods of the class are invoked. Of course, we know already that the class is used by BlockingFIFO, but suppose we did not already know that. We can find this out by using Eclipse to display the call hierarchy for a method. Open the context menu within the get() method and select Open Call Hierarchy. The Call Hierarchy view appears, and shows

This tells us that BoundedFIFO.get() is called by BlockingFIFO.get. Clicking on get() - test.BlockingFIFO opens BlockingFIFO in a Java editor and selects the call expression:

Here we can see that the BlockingFIFO.get() calls fifo.get() on line 38. The method acquires the lock on the object referenced by fifo on line 29. This suggests that it is the case the clients of BoundedFIFO are expected to acquire the lock.

1.3.1.2. Declaring Lock Preconditions

We can test this hypothesis by annotating all the methods of BoundedFIFO with the lock precondition @RequiresLock("BufLock"). There are seven methods in the class, so we could quickly add the annotations without too much work. We can also take advantage of the Proposed Annotations view to have JSure add these promises for us. First, we make sure the view is only showing inferred annotations by pressing the icon in the view's tool bar (or unselecting Show Only Proposals Inferred From Other Promises in the view's menu). In the tree view of the proposed annotations, select the project JSureTutorial_BoundedFIFO and choosing Expand:

The view shows annotations in the context of the Java declaration that they are proposed to be automatically placed on. Selecting any node in the tree, including a Java declaration or Eclipse project, and choosing Annotate Code... from the view context menu begins an automatic code edit. Doing this would bring up an Eclipse source code refactoring dialog box. We choose not to go this route here; however, an example of adding annotations using this view is presented below.

There is a way, however, to accomplish the same thing with only single annotation: we can use a scoped annotation to add the annotation to all the methods in the class.

@RegionLock("BufLock is this protects Instance")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  …
}
      

Here we use the @Promise annotation to add @RequiresLock("BufLock") to the class members that match the pattern *(**). In the scoped promise the quotation marks are removed from inside the parenthesis. This is to avoid having to escape the inner quotation marks (i.e., \"). The pattern *(**) matches each method with any name, *, with any parameter list, (**). Using a scoped promise has the additional advantage of better capturing the design intent: all methods in the class are expected to have the same lock precondition. Were we to add a new method to the class, and if we did not use the scoped annotation, we would have to remember to add the @RequiresLock annotation to the new method. The scoped annotation would automatically apply the lock precondition to a new method.

Add the @Promise annotation to BoundedFIFO and save the source file. You could choose JSureVerify Project from the Eclipse main menu to scan the project again or use the keyboard shortcut Ctrl+Alt+Shift+V, however there is an easy shortcut to re-run the same scan again. Select the scan in the JSure Scans view and choose Re-Verify from the context menu as shown below.

After the analysis completes, there is a new Scoped promises heading in the Verification Status view, and we can see all the places where the @Promise annotation added @RequiresLock annotations. Only 4 out of the 7 are currently satisfied:

Note that the view highlights differences in light yellow. In this case indicating that the scoped promise results are new since the previous scan. A decorates the lower-right of all images providing a trail from the root of the view's tree to new and changed results.

Let us look at the chain of evidence for the unassured @RequiresLock on the method BoundedFIFO.isFull():

We see that the caller is confused and is synchronized on this (as evidenced by the caller holding the lock this.MUTEX), although the analysis tells use that the lock on this.fifo is the lock that is needed. Clicking on the supporting information result opens a Java editor and selects the expression that acquires the lock:

Here we see that the method BlockingFIFO.put() acquires the lock on this. But in the context of BlockingFIFO, this refers to the BlockingFIFO object, not the BoundedFIFO object that is correctly referred to by fifo. Therefore, this code is acquiring the wrong lock. The synchronized statement in method isFull() needs to be changed:

public void put(LoggingEvent e) {
  synchronized (fifo) {
    …
  }
}
      

Indeed, this problem is why the java.lang.Object.MUTEX lock model has remained unassured. Notice that fifo.notify() is called within the synchronized block. The java.lang.Object.MUTEX lock model declares the object itself (in this case fifo) as the lock that protects the wait–notify queue, and requires that the lock be held before the wait() and notify() methods may be invoked. The verification state of this model also hinted that the wrong lock was being acquired in the code. This code change will allow the java.lang.Object.MUTEX lock model to assure.

Make this change to BlockingFIFO.java and run another JSure scan using the keyboard shortcut Ctrl+Alt+Shift+V or by using Re-Verify in the JSure Scans view.

1.3.1.3. Declaring a Thread-Confined Constructor

After analysis of the JSureTutorial_BoundedFIFO code completes, all the lock preconditions are assured, but there are still five unprotected field accesses:

Getting to these results can take several click in the Verification Status view. It is possible to get a list of the inconsistent analysis results more directly using the JSure Quick Search.

Select Analysis Result from the menu. This lets you filter the results by the type of analysis result. The graphics show that there are 40 analysis results and that 35 of those results are consistent and 5 are inconsistent. Check Inconsistent. This selection allows the inconsistent analysis results through this filter. We don't need another filter, so select Show to show the 5 inconsistent analysis results.

This query is useful so we want to save it for future use. Click on the icon at the lower-left of the view and enter X Results into the dialog.

Press OK to save the query. It now appears in the space below the view and can be selected at any time via a click. Let's test the saved query. First, clear the current query by pressing the image in the upper-right-hand corner of the view. The view resets to its initial state. Now, to get our query back, click on the X Results link at the bottom of the view. The query is redisplayed in the view.

If you click on the five assurance failures, the results at the right above, you will see that they point to the field initializers for the fields first, next, and numElts, and to the use of the fields buf and size in the class’s constructor. Constructors are interesting because we cannot require the caller to hold a lock on this because the instance does not exist before the constructor is called. Furthermore, it is bad practice to use synchronized blocks in the constructor to protect the state of the object under construction because we cannot create a single atomic block that encloses all the constructors invoked while initializing an object. There would have to be multiple distinct synchronized blocks: one in the constructor for the class and one in each constructor of any subclasses, etc.

The solution is to take advantage of the fact the constructor is operating on a newly created object. Specifically, we would like to assure that the constructor does not do anything that gives any thread other than the one that invoked the constructor access to the newly created object. If we can assure this, we know that the object can only be accessed by a single thread—the one that invoked the constructor—during the execution of the constructor. We can do this by annotating the constructor BoundedFIFO(int) with @Unique("return") to declare the intent that no aliases to the newly constructed object will be created during the execution of the constructor. This annotation is listed in the Proposed Annotation view:

Select the @Unique("return") annotation in the view and choose Annotate Code… from the context menu. An Eclipse refactoring dialog appears:

Select OK to insert the annotation. Re-scan the project and the model now assures:

[Tip]Tip

For constructors the annotations @Unique("return") and @Borrowed("this") are defined to be equivalent. That said, most programmers have a mental model of the constructor "returning" a new object. The idea that the returned object is required to be a unique reference is intuitive to them and, therefore, the @Unique("return") annotation is as well.

1.3.1.4. Aggregating State

Although the results show no outright assurance failures, there are still two warnings about references to possibly shared objects:

These warnings refer to access to the contents of the array referenced by the field buf. This array is an object separate from the BoundedFIFO object and is not protected by the lock protecting the fields of the BoundedFIFO object. We can extend protection to the contents of the array by declaring the array reference to be @Unique—no object but the BoundedFIFO object can hold a reference to it—this also declares that the state of the array is part of the state of the BoundedFIFO object (its Instance region):

@RegionLock("BufLock is this protects Instance")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  @Unique
  LoggingEvent[] buf;
  …
}
      

This annotation is suggested by JSure in the Verification Status view (under the suggestion) and in Proposed Promises view. Add the promise using the context menu in the Verification Status view. Select Annotate Code… to add the proposed @Unique annotation to the code.

Now, as part of the state of the BoundedFIFO object, the array object referenced by buf is also protected by the lock that protects that state of the buffer.

After adding the annotation to the field buf and performing a scan of the JSureTutorial_BoundedFIFO project again we can see the effects of this annotation: there are now 29 protected field accesses, up from 27. This is because the two array dereferences are now counted as protected accesses (lines 59 and 76):

The models and code in the JSureTutorial_BoundedFIFO project are now consistent with no warnings.

1.3.1.5. Using a Named Region

The lock BufLock is declared to protect the region Instance. This is a region declared in the class java.lang.Object that is the ancestor of every instance field declared in a class. By associating the lock with this region we declare that every instance field of the class, and every instance field declared in all subclasses of the class, are protected by the lock. This is not something that we always want to do, and using the Instance region in this way, while convenient, does not usually describe the design intent as well as one might like. It is often better to use an explicitly declared region. In real-world use of the JSure tool explicitly declared regions are far more common than the use of the default Instance region. It is important for you to understand how to use explicitly declared regions. Here we demonstrate how to annotate BoundedFIFO to use an explicitly declared region BufState.

We declare the new region using the Region annotation on the class BoundedFIFO. We also update the RegionLock annotation to protect BufState instead of Instance:

@Region("BufState")
@RegionLock("BufLock is this protects BufState")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  …
}

After making this change and performing a scan of the project, the model still assures, but upon closer inspection the assurance is essentially vacuous because it contains no protected or unprotected field accesses, although the method preconditions are still shown to be satisfied:

The problem here is that the region BufState is initially empty. It needs to be populated with actual state, that is, with fields. This is done by annotating fields with the InRegion annotation and changing our Unique annotation to a UniqueInRegion annotation:

@Region("BufState")
@RegionLock("BufLock is this protects BufState")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  @UniqueInRegion("BufState")
  LoggingEvent[] buf;

  @InRegion("BufState")
  int numElts = 0;
  @InRegion("BufState")
  int first = 0;
  @InRegion("BufState")
  int next = 0;
  @InRegion("BufState")
  int size;
  …
}

In this case, we place each of the fields into the region BufState. We also update the aggregation of the array referenced by buf so that the array elements are aggregated into BufState by replacing the previous @Unique annotation with @UniqueInRegion("BufState"). After these changes we again have 29 protected field accesses:

Region declarations, like field declarations, accept visibility modifiers. The absence of a modifier in the declaration for BufState means the region has “default” or “package” visibility. This is the minimum visibility necessary for this region because the fields we have populated it with have that same visibility. If we tried to declare the region to be private, JSure would report a modeling error because all the fields are of “default” visibility. To see this, change the @Region annotation to @Region("private BufState") and scan the project again. The expected modeling problems about field visibility will appear to the upper-right as shown below.

It would make more sense, however, for the region and fields in BoundedFIFO to be declared private; in this case there is no reason for them to be visible to other classes. This prevents, for example, a subclass from adding additional fields to the region—because the region is not visible to subclasses—and interfering with the design intent.

@Region("private BufState")
@RegionLock("BufLock is this protects BufState")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  @UniqueInRegion("BufState")
  private LoggingEvent[] buf;

  @InRegion("BufState")
  private int numElts = 0;
  @InRegion("BufState")
  private int first = 0;
  @InRegion("BufState")
  private int next = 0;
  @InRegion("BufState")
  private int size;
  …
}

Go ahead and make these changes and scan the project again. The verification results should not change but the modeling problems will go away.

1.3.1.6. Using an Inferred Named Region

This need to get the @Region declaration "just right" can be somewhat annoying and JSure (since version 5.6) can simply infer the correct region declaration. Let's try this out. Go ahead and delete the @Region declaration in your code as shown below.

@RegionLock("BufLock is this protects BufState")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  @UniqueInRegion("BufState")
  private LoggingEvent[] buf;

  @InRegion("BufState")
  private int numElts = 0;
  @InRegion("BufState")
  private int first = 0;
  @InRegion("BufState")
  private int next = 0;
  @InRegion("BufState")
  private int size;
  …
}

It is important to keep the @InRegion and @UniqueInRegion declarations because those are what the tool uses to infer the @Region declaration.

If we make the above change and scan the project again we get the results reported below.

This inference of declarations can make using @RegionLock simpler in practice.

1.3.1.7. Stating that BoundedFIFO is @ThreadSafe

We can now apply the @ThreadSafe annotations from Java Concurrency In Practice by Goetz, et. al. (Addison-Wesley 2006) to the BoundedFIFO class.

@ThreadSafe
@RegionLock("BufLock is this protects BufState")
@Promise("@RequiresLock(BufLock) for *(**)")
public class BoundedFIFO {
  …
}

If we re-scan the project with JSure we find that this does not assure. What is the problem?

While the BufLock lock model checked its protected state, placing an @ThreadSafe annotation on the class requires that all its state be thread safe—by being immutable, protected by a lock, and so on. The results show that the array buf cannot be assured as thread safe because it is not considered containable. To be containable means that instances of the class can be safely encapsulated via region aggregation into other objects because methods of the class do not leak references to themselves or any of the other objects that they reference, transitively. JSure cannot prove this for Java arrays (it is a surprisingly difficult aliasing problem). You can, however, continue to move the @ThreadSafe model toward consistency by "vouching" for the buf field.

The use of the @Vouch annotation allows you to "override" or "quiet" a tool reported inconsistency. Using this feature produces a icon in its upper-left. This is an indication of something in the consistency proof that is not being checked, or verified, by analysis. The @Vouch annotation is the reason the is used—it indicates that a programmer is willing to prick a finger and vouch for the unverified contingency with a small drop of blood—at least virtually. Use them with care and vouch for as little as possible.

The first approach states the field is altogether thread-safe. The annotation is shown below.

@Vouch("ThreadSafe")
@UniqueInRegion("BufState")
private LoggingEvent[] buf;

Make this change to the code and re-scan. The results are shown below.

This works as seen above, but we can make a less general vouch in this particular case. In particular, we do want JSure to check that the lock model actually protects the state of buf. To make sure that this is the case we vouch that the buf field is containable. This makes the aliasing assumption we want but causes the tool to verify that a lock protects the state (in this example BufLock).

@Vouch("Containable")
@UniqueInRegion("BufState")
private LoggingEvent[] buf;

Make this change to the code and re-scan. The results are shown below.

This is an improvement because we vouch only for the aliasing—not both aliasing and safe concurrency.

There are situations like the one described above, where the @Vouch annotation (and the @Assume annotation) can help, with correct code that JSure is not precise enough to verify. Read the Javadoc for these annotations to learn more about how they works and see more examples.

An approach that would avoid the need for a @Vouch annotation would be to change the buf array into a collection, such as an ArrayList. In fact, best Java practice in this case would probably be to remove the BoundedFIFO class altogether and replace its uses with a java.util.concurrent.BlockingQueue implementation, such as ArrayBlockingQueue. This would avoid client locking and simplify the code.

1.3.1.8. Deleting Old Scans

JSure saves each scan that you run. The JSure Scans view lists these scans and you can view their data by changing which scan is checked. Check a few of your earlier scans and note how the other JSure views change. Each time a new scan completes the view automatically selects this scan so that it's results are visible to the tool user.

The JSure Scans view also lets you delete old scans which take up disk space on your machine. This is done by selecting them and choosing Delete from the view's context menu.

We are done with the scans we performed on JSureTutorial_BoundedFIFO so select all the scans in the view (with the mouse or using Ctrl+A) and delete them with the view's context menu as shown below.

You are now finished with this tutorial. The next tutorial shows how to use the @ThreadSafe and @Immutable annotations to express design intent and verify it using JSure.

1.3.2. Verifying annotations from the book Java Concurrency In Practice

In this tutorial we walk through the complete assurance of the JSureTutorial_ThreadSafeAndImmutable project using JSure. Specifically, we assure the implementation of several classes that make up a simple 2D drawing framework. This tutorial focuses on the effective use of the @ThreadSafe and @Immutable annotations from Java Concurrency In Practice by Goetz, et. al. (Addison-Wesley 2006), hereafter referred to as JCIP.

We want our drawing library to be thread safe. We begin by examining the Point class.

public class Point {

  int x, y;

  private Point(int x, int y) {
    this.x = x;
    this.y = y;
  }

  public int getX() {
    return x;
  }

  public int getY() {
    return y;
  }

  private static List<Point> INSTANCES = new ArrayList<Point>();

  public static Point getInstance(int x, int y) {
    synchronized (INSTANCES) {
      for (Point p : INSTANCES) {
        if (p.x == x && p.y == y)
          return p;
      }
      final Point result = new Point(x, y);
      INSTANCES.add(result);
      return result;
    }
  }

  public static Point getInstance(Point from, int xOffset, int yOffset) {
    return getInstance(from.x + xOffset, from.y + yOffset);
  }
}

1.3.2.1. Declaring State Is ThreadSafe or Immutable

This class appears thread safe: note that its instance state is immutable (there are no "setter" methods). We consider being immutable to be superior to being thread safe, because immutable objects are always thread safe. Also observe that this class is, in fact, a Java implementation of the Flyweight design pattern from Design Patterns Gamma, et al. (Addison-Wesley 1994). SureLogic has augmented the JCIP annotations to be able to describe this situation. Annotate the Point class as shown below

@Immutable(appliesTo=Part.Instance)
@ThreadSafe(appliesTo=Part.Static)
public class Point {
  …
}

Scan the project with JSure. The class fails to assure as shown in the snippet from the Verification Status view below.

We focus on the immutable instance state of the Point class first and note that JSure tells us that it cannot assure the implementation because the x and y fields are not declared to be final. This is consistent with the advice from JCIP which specifies that an object is immutable if all its fields are final (among other things). Change the code as shown below to make all the fields final.

@Immutable(appliesTo=Part.Instance)
@ThreadSafe(appliesTo=Part.Static)
public class Point {

  final int x, y;
  …
  private static final List<Point> INSTANCES = new ArrayList<Point>();
  …
}
[Note]Final fields and JSure

To obtain verification, JSure often wants fields and (to a lesser degree) variables to be declared final. This is because it removes any doubt that the field/variables value may change from one point in the code to another point in the code. Get in the habit of declaring unchanging fields to be final to help JSure reach model–code consistency.

Now rescan the project with JSure. As shown below the @Immutable(appliesTo=Part.Instance) annotation on the Point class now verifies. The static portion which implements the Flyweight pattern, does not.

1.3.2.2. Locking Models Support ThreadSafe

Examining the implementation of the getInstance method we can see that locking is used to protect the contents of the INSTANCES collection because ArrayList is not thread safe. We need to express a locking model in the code, much like we did in the BoundedFIFO tutorial, to support the verification of the @ThreadSafe(appliesTo=Part.Static) annotation. In this example, a lock on the collection protects the contents of the collection. Add the model to the code as shown in the listing below.

@Immutable(appliesTo=Part.Instance)
@ThreadSafe(appliesTo=Part.Static)
@Region("static private FlyweightState")
@RegionLock("FlyweightLock is INSTANCES protects FlyweightState")
public class Point {
  …
  @UniqueInRegion("FlyweightState")
  private static final List<Point> INSTANCES = new ArrayList<Point>();
  …
}

With these changes in the code scan the project again with JSure. The models in the Point class are now consistent with its implementation.

The annotations precisely express the design intent of the programmer, and are expressed in the code so that this intent is conveyed in to future maintainers. This is important, because in our experience, many concurrency defects are introduced into the code during maintenance.

1.3.2.3. Annotating Type Hierarchies

We now turn our attention to the Shape interface listed below.

public interface Shape {

  /**
   * Gets the bounds of this shape.
   * 
   * @return a list containing four points: top-left point, top-right point,
   *         bottom-right point, and bottom-left point.
   * 
   * @throws IllegalArgumentException
   *           if something goes wrong.
   */
  List<Point> getBounds();

  /**
   * Gets the outline of this shape.
   * 
   * @return the outline of this shape, which should include at least three
   *         points.
   * 
   * @throws IllegalArgumentException
   *           if something goes wrong.
   */
  List<Point> getOutline();
}

This is the base interface for shapes, subtypes are shown in the following hierarchy:

We want this class and its subtypes to be thread safe, so we express this by placing a @ThreadSafe annotation on the interface. In this case there should be no static portion to consider, but @ThreadSafe with no appliesTo means that both the instance state and the static state are thread safe.

@ThreadSafe
public interface Shape {
  …
}

Edit the code as shown above and rescan the project with JSure. Although the model is consistent, we do get two new modeling problems. The problems are because JSure enforces annotation consistency across a type hierarchy. Because Shape is annotated @ThreadSafe the tool wants the subtypes Polygon and Rectangle to be as well. Putting it another way, the @ThreadSafe annotation on Shape states that all shapes are thread safe. We can allow the tool to perform the code edit by selecting both modeling problems and choosing Annotate Code To Fix... as shown below.

The code edit is previewed as shown below. You may accept the edit.

Now rescan the project again with JSure. The results should appear as

As shown above, the Rectangle class assures, but the Polygon class does not assure.

[Note]Automatic edits in JSure are intended to be helpful—not perfect

Automatic edits to your code, such as fixing modeling problems or including proposed annotations, are heuristic—most are abductively inferred from other annotations you have made to the code. They are designed to avoid tedious annotation entry. But they may not reflect programmer design intent, or, as in this example, may be incomplete. You should always carefully consider if the edit reflects an assertion about your code that is reasonable based upon your understanding of its design.

Let's examine the implementation of the Polygon class in more detail to determine why its @ThreadSafe annotation fails to assure. Of immediate interest in the listing below is the lock field and its use to protect the polygon's collection of points.

@ThreadSafe
public class Polygon implements Shape {

  public Polygon() {
    // callers use add to add points
  }

  private final Object lock = new Object();

  private final List<Point> outline = new ArrayList<Point>();

  public void add(Point value) {
    if (value != null) {
      synchronized (lock) {
        outline.add(value);
      }
    }
  }

  public List<Point> getBounds() {
    synchronized (lock) {
      if (outline.size() < 3)
        throw new IllegalArgumentException();
      Point top = null, bottom = null, right = null, left = null;
      boolean first = true;
      for (Point p : outline) {
        if (first) {
          top = bottom = right = left = p;
        } else {
          if (p.x < left.x)
            left = p;
          if (p.x > right.x)
            right = p;
          if (p.y < bottom.y)
            bottom = p;
          if (p.y > top.y)
            top = p;
        }
      }
      final ArrayList<Point> result = new ArrayList<Point>();
      result.add(Point.getInstance(left.getX(), top.getY()));
      result.add(Point.getInstance(right.getX(), top.getY()));
      result.add(Point.getInstance(right.getX(), bottom.getY()));
      result.add(Point.getInstance(left.getX(), bottom.getY()));
      return result;
    }
  }

  public List<Point> getOutline() {
    synchronized (lock) {
      if (outline.size() < 3)
        throw new IllegalArgumentException();
      return new ArrayList<Point>(outline);
    }
  }
}

The class uses a locking model: a lock on lock protects the contents of the collection outline. We can express this intent with the following annotations to the class.

@ThreadSafe
@Region("private PolygonState")
@RegionLock("PolygonLock is lock protects PolygonState")
public class Polygon implements Shape {

  @Unique("return")
  public Polygon() {
    // callers use add to add points
  }

  private final Object lock = new Object();

  @UniqueInRegion("PolygonState")
  private final List<Point> outline = new ArrayList<Point>();

  …
}

Make the above changes to the code and rescan the project with JSure. The tool reports that the Polygon class is now consistent with its annotations.

We now turn our attention to the Rectangle class. It verifies, but we should examine it to be sure its @ThreadSafe annotation reflects the programmer's design—In fact, it isn't an exact match.

@ThreadSafe
public class Rectangle implements Shape {

  private final Point topLeft;
  private final int width, height;

  public Rectangle(Point topLeft, int width, int height) {
    if (topLeft == null || width < 1 || height < 1)
      throw new IllegalArgumentException();
    this.topLeft = topLeft;
    this.width = width;
    this.height = height;
  }

  public Point getTopLeft() {
    return topLeft;
  }

  public int getWidth() {
    return width;
  }

  public int getHeight() {
    return height;
  }

  public List<Point> getBounds() {
    final ArrayList<Point> result = new ArrayList<Point>();
    result.add(topLeft);
    result.add(Point.getInstance(topLeft, width, 0));
    result.add(Point.getInstance(topLeft, width, -height));
    result.add(Point.getInstance(topLeft, 0, -height));
    return null;
  }

  public List<Point> getOutline() {
    return getBounds();
  }
}

This class, it appears from an examination of its code, is not just thread safe, it is immutable. Why? Because Point is immutable and the other two fields are int—a primitive type. Because an immutable class is always thread safe, we can replace the @ThreadSafe annotation with an @Immutable annotation.

@Immutable
public class Rectangle implements Shape {
  …
}

Make the above changes to the code and rescan the project with JSure.

The tool reports that the Rectangle class is assured to be immutable.

[Note]Should Rectangle be @ThreadSafe or @Immutable

We changed the annotation on Rectangle to @Immutable based upon its current implementation. However, an argument could be made that leaving Rectangle as @ThreadSafe allows greater implementation flexibility in maintenance of the codebase. Both are valid approaches—you should make the right choice for your code based upon your software design. You should always consider maintenance when annotating code.

1.3.2.4. Annotating Singleton Classes

We now consider the Canvas class which is listed below.

public final class Canvas {

  private final Set<Point> points = new CopyOnWriteArraySet<Point>();

  public void addPoint(Point value) {
    if (value != null)
      points.add(value);
  }

  private final List<Shape> shapes = new CopyOnWriteArrayList<Shape>();

  public void addShape(Shape value) {
    if (value != null)
      shapes.add(value);
  }

  public static Canvas getInstance() {
    return INSTANCE;
  }

  private static final Canvas INSTANCE = new Canvas();

  private Canvas() {
    // singleton
  }
}

We can make two observations about the implementation of this class. First, it is a Java implementation of the Singleton design pattern from Design Patterns Gamma, et al. (Addison-Wesley 1994). We even note an informal comment in the private constructor about this intent. Note that sometimes informal comments can help indicate that a JSure annotation might be appropriate. Second, the implementation appears to be thread safe. Both of these assertions can be expressed in JSure.

@ThreadSafe
@Singleton
public final class Canvas {
  …
}

Edit the code to appear as shown above and rescan the project with JSure. It will verify.

1.3.2.5. Annotating Utility Classes

We now consider the DrawingHelper class which is listed below.

public class DrawingHelper {

  public static void drawSquare(Point at, int width) {
    Shape square = new Rectangle(at, width, width);
    Canvas.getInstance().addShape(square);
  }

  public static void drawRectangle(Point at, int width, int height) {
    Shape square = new Rectangle(at, width, height);
    Canvas.getInstance().addShape(square);
  }

  public static void drawPoint(int x, int y) {
    Canvas.getInstance().addPoint(Point.getInstance(x, y));
  }
}

We observe that this class is a utility class as described by Bloch in Effective Java Item 4 (Addison-Wesley 2008). A utility class is a grouping of static methods and static fields. Such classes, as Bloch notes, have acquired a bad reputation because they have been abused in the past, but they do have valid uses. JSure allows annotating a utility class with the annotation @Utility.

@Utility
public class DrawingHelper {
  …
}

Edit the code to appear as shown above and rescan the project with JSure.

The @Utility annotation on the DrawingHelper class does not verify. What is wrong? The problem is that it violates Bloch's Item 4: Enforce noninstantiability with a private constructor. JSure wants to be sure that an instance of this class can never be created at runtime. To enforce this in our implementation of DrawingHelper we need to add a private constructor to the code.

@Utility
public class DrawingHelper {
  …
  private DrawingHelper() {
    // singleton
  }
}

Edit the code to appear as shown above and rescan the project with JSure. The @Utility annotation on the DrawingHelper class now verifies.

You are now finished with this tutorial. The next tutorial works on a larger codebase and presents the use of JSure to verify lock policies that use util.concurrent locks.

1.3.3. Verifying PlanetBaron

This example demonstrates more sophisticated annotations and analysis results using a simple network capture the planet game: PlanetBaron. It will use the tutorial project JSureTutorial_PlanetBaron.

Scan the JSureTutorial_PlanetBaron project with JSure. To do this choose JSureVerify Project from the Eclipse main menu. You can also use the keyboard shortcut Ctrl+Alt+Shift+V. This project already contains lock model annotations about its locking policies, not all of which assure (as you can see if you examine the scan results). In the rest of this tutorial we fix these verification failures.

1.3.3.1. Running PlanetBaron

Although we do not need to run PlanetBaron to analyze it with JSure, it is helpful in the discussion below to know what the game does. In particular, it makes it easier to understand the roles of the classes encountered in the assurance results. PlanetBaron is a network-based real-time strategy game. It contains three programs:

  • A server program that manages game state.

  • A client user interface program that allows players to interact with the game.

  • A program, called the chat-test client, that allows direct interaction with the server. The chat-test client is used to shutdown a running server.

Let us run a PlanetBaron game. In the Package Explorer, select Server.java in the com.surelogic.jsure.planetbaron.server package. Select Run AsJava Application in the context menu. You should see following output in the Console view which indicates that the server has started successfully:

[INFO "server-main"] PlanetBaron game server listening for clients on port 8693 and playing on a 15x15 map [com.surelogic.jsure.planetbaron.server.Server.startListening()]
      

Now we need to add some players. Select PlayerUI.java in the com.surelogic.jsure.planetbaron.client package. Select Run AsJava Application in the context menu. You will see a Swing application start that has a blank grid. In the lower right-hand-corner enter a player name, Laurel, and press Connect.

The screen will change to contain several planets and one ship with Laurel as its label. By moving your mouse around the grid you can direct your ship. Place your mouse over a planet and left-click. This action will cause your ship to move slowly to that planet. When your ship arrives you will become the owner of that planet. This is called “taking ownership” of a planet. Go ahead an take ownership of a planet. Note that while your ship is moving you are not allowed to change its destination. Once it arrives at the destination you selected you can then select a subsequent destination.

Now, go back to Eclipse and start a second instance of PlayerUI.java. In the lower right-hand-corner enter a player name, Hardy, and press Connect.

The game supports as many players as you choose to connect to the server. Notice that the planets that Laurel owns are red in the Hardy PlayerUI while they are white in the Laurel PlayerUI. Moving back and forth between the two PlayerUIs move the ships to play the game. Note that the idea of the game is to own as many planets as you can. A game screenshot is shown in Figure 1.8.

Figure 1.8. The PlanetBaron PlayerUI for Laurel

The PlanetBaron PlayerUI for Laurel

To finish the game press Disconnect in both PlayerUI instances and then terminate the programs by normally. This action ends both player user interfaces but the server is still running. To terminate the server we need to use the chat-test client program.

Select ChatTestClient.java in the com.surelogic.jsure.planetbaron.client package. Run AsJava Application in the context menu. You will see a Swing application start. This program allows you to directly control the game server. We want to use it to shutdown the game server. To do this, press Connect to connect to the game server and enter shutdown as the command. Your screen should now look like the one shown in Figure 1.9.

Figure 1.9. The ChatTestClient

The ChatTestClient

Press Send to shutdown the server. A dialog will appear stating that the server has disconnected from the ChatTestClient that you may dismiss. You can now terminate the ChatTestClient. Back in the Eclipse console for the server you should see the following message:

…      
[INFO "server-main"] PlanetBaron game server shutdown complete [com.surelogic.jsure.planetbaron.server.Server.startListening()]
      

We are now ready to examine the results from scanning the PlanetBaron codebase with JSure.

1.3.3.2. Initial Scan Results

The initial scan results for the JSureTutorial_PlanetBaron project are shown in Figure 1.10.

Figure 1.10. Initial assurance results for PlanetBaron

Initial assurance results for PlanetBaron

[Note]Do not worry about the Null value verification results for PlanetBaron

There are several problems with the Null value results for this project, which while interesting, are not the focus of this tutorial. In a nutshell, too much is being done in constructors and the analysis is pointing out that partially initialized objects may be being aliased or dispatched into before they should.

Lots of annotations have been placed in this code. Our focus is on the Concurrency models. You may poke around in the Verification Status and Verification Explorer views to determine what is causing assurance failures. In fact, it turns out that the lock model for lock ThingLock in class com.surelogic.jsure.planetbaron.game.Thing fails to assure—causing the related @ThreadSafe annotations, such as on Planet and Ship, to also fail to assure.

We also note, primarily because a view is painted in bright yellow, that the project has a modeling problem. This view is shown in Figure 1.11.

Figure 1.11. Initial modeling problems for PlanetBaron

Initial modeling problems for PlanetBaron

[Note]Do not worry about other library modeling problems

There may be other modeling problems in the standard library. This is especially true if you are using Java 8. It is safe to ignore these during this tutorial.

A modeling problem indicates a syntactic or semantic problem with an annotation that has been added to the code. Clicking on the one modeling problem will open the Thing class in the Java editor. This modeling problem is related to the visibility of f_lock, the lock specified in the ThingLock locking model. That is, the visibility of the field that references the lock object is less visible than the region protected by that lock. This is potentially problematic because it means there are contexts in which the region Instance is visible, but the reference to the lock, the field f_lock, is not visible.

We could fix this modeling problem by simply making the field f_lock public instead of protected. Generally speaking, however, this violates the principles of data hiding and abstraction. A reasonable approach would be to make a named region with protected visibility (as was demonstrated at the end of the BoundedFIFO tutorial). For this tutorial, however, we will use another alternative supported by JSure. We will add a “lock getter” method to Thing to return the lock object. We annotate this method with a @ReturnsLock annotation so JSure knows we intend to use it to return a lock object and assures that we do in fact return the correct lock object:

  @ReturnsLock("ThingLock")
  public final ReadWriteLock getThingLock() {
    return f_lock;
  }
      

Add this code to the the Thing class. Scan the project again to verify that the modeling problem is gone.

Now that we have fixed the modeling problem, we examine the lock model for ThingLock in more detail with the aim of fixing the model or the code to allow verification.

1.3.3.3. Introducing ThingLock

As can be seen in Figure 1.10, the code is inconsistent with the ThingLock annotation. This lock is declared in the class com.surelogic.jsure.planetbaron.game.Thing:

 20: @ThreadSafe
 21: @RegionLock("ThingLock is f_lock protects Instance")
 22: public abstract class Thing {
 23: 
 24:   /**
 25:    * A logger for subclasses.
 26:    */
 27:   @Vouch("ThreadSafe")
 28:   protected static final Logger LOG = ConciseFormatter.getLogger("things");
 29: 
 30:   private final GameMap f_map; // immutable
 31: 
 32:   @Unique("return")
 33:   Thing(GameMap map) {
 34:     assert map != null;
 35:     f_map = map;
 36:   }
 37: 
 38:   @Borrowed("this")
 39:   public GameMap getMap() {
 40:     return f_map;
 41:   }
 42: 
 43:   /**
 44:    * Protects the state of this object including state added by subclasses.
 45:    */
 46:   protected final ReadWriteLock f_lock = new ReentrantReadWriteLock();
 47: 
 48:   @ReturnsLock("ThingLock")
 49:   public final ReadWriteLock getThingLock() {
 50:     return f_lock;
 51:   }
 52: }

The lock ThingLock associates the lock object referenced by f_lock with the class’s non-static state. In this case, the lock field f_lock refers to a java.util.concurrent.lock.ReadWriteLock object. JSure understands the semantics of these locks, in particular that

  • Each lock() call must be matched to a unlock() call, and vice versa.

  • The protected region must not be written to when only the read lock is held.

Class Thing is the superclass for all the “things” in the game: it has the subclasses Player, Planet, and Ship. The lock annotation thus binds the implementations of these subclasses as well, extending its protection to all the instance fields declared in them.

Digging into the results for ThingLock we see that model–code consistency is prevented by one unprotected field access and three inconsistent lock preconditions:

Before we examine this problem in depth we switch to the Verification Explorer view by clicking on its tab (to the right of the Verification Explorer view). To see lock() and unlock() information press the in the view toolbar. Expand the JSureTutorial_PlanetBaron project, the com.surelogic.jsure.planetbaron.game package, and the Planet class.

If you open the the two methods, getOwner and setOwner we see, by the results, that JSure matches up lock() and unlock() calls. Calls to lock() and unlock() are tracked separately because they do not need to be matched up one-to-one. JSure will also flag if lock() or unlock() cannot be matched or if it matches inconsistently along different control-flow paths.

1.3.3.4. Unprotected Field Access

Returning to the problem with the ThingLock locking model, we first look at the unprotected field access:

The field f_location is read without holding the read lock in the class Ship. Before even looking at the field access, we emphasize that this error occurs in a subclass of Thing, and that the field f_location is declared in Ship. The erroneous access occurs in the method Ship.moveTo():

159:   public void moveTo(Location destination) {
160:     if (isMoving())
161:       throw new IllegalStateException(
162:           "a moving ship can't change its destination");
163: 
164:     if (f_location.equals(destination)) {
165:       LOG.log(Level.WARNING,
166:           "ignored attempt to move ship to its current location");
167:     } else {
168:       f_lock.writeLock().lock();
169:       try {
170:         f_isMoving = true;
171:         f_turnsMoving = 0;
172:         f_destination = destination;
173:         f_moveDistance = f_location.distanceTo(f_destination);
174:         f_percentageMoved = 0.0;
175:         sendReport(); // OK to invoked holding a write lock
176:       } finally {
177:         f_lock.writeLock().unlock();
178:       }
179:     }
180:   }

We see that the field access on line 164 in the condition of the if-statement occurs outside of the critical section that only spans the else-block. We need to edit the method to expand the critical section to contain the entire conditional statement:

  public void moveTo(Location destination) {
    if (isMoving())
      throw new IllegalStateException(
          "a moving ship can't change its destination");

    f_lock.writeLock().lock();
    try {
      if (f_location.equals(destination)) {
        LOG.log(Level.WARNING,
            "ignored attempt to move ship to its current location");
      } else {
        f_isMoving = true;
        f_turnsMoving = 0;
        f_destination = destination;
        f_moveDistance = f_location.distanceTo(f_destination);
        f_percentageMoved = 0.0;
        sendReport(); // OK to invoked holding a write lock
      }
    } finally {
      f_lock.writeLock().unlock();
    }
  }

Make the above changes (you can cut and paste the method into the code) and scan the code again. The new results for ThingLock have 54 protected field accesses, up from the previous 53:

1.3.3.5. Read–Write Locks

You can demonstrate to yourself that JSure understands when the read component and when the write component of a read–write lock needs to be held by changing lines 164 and 178 of Ship.moveTo() to acquire the read lock instead of the write lock:

159:   public void moveTo(Location destination) {
160:     if (isMoving())
161:       throw new IllegalStateException(
162:           "a moving ship can't change its destination");
163: 
164:     f_lock.readLock().lock();
165:     try {
166:       if (f_location.equals(destination)) {
167:         LOG.log(Level.WARNING,
168:             "ignored attempt to move ship to its current location");
169:       } else {
170:         f_isMoving = true;
171:         f_turnsMoving = 0;
172:         f_destination = destination;
173:         f_moveDistance = f_location.distanceTo(f_destination);
174:         f_percentageMoved = 0.0;
175:         sendReport(); // OK to invoked holding a write lock
176:       }
177:     } finally {
178:       f_lock.readLock().unlock();
179:     }
180:   }

If you save these changes, and run a scan, the results show 49 protected field accesses and 5 unprotected field accesses:

In particular, all the write access from the else-branch are unprotected because they require the write lock to be held, but only the read lock component of ThingLock is held.

If we switch over the the Verification Explorer view we can better see that the inconsistent results are all in the Ship.moveTo() method. This is shown in the image below. To match the image unselect in the view toolbar to hide suggestions and warnings and then select to show analysis results. Expand your view to show the Ship.moveTo() method.

The Verification Explorer view can be helpful for looking at the results in the context of their reported Java code location.

Restore the method to its previously corrected form by changing lines 162 and 176 to invoke writeLock() instead of readLock(). When you are finished making these changing these lines back, run another scan.

1.3.3.6. Unsatisfied Preconditions

We now move on to the three unsatisfied lock preconditions. Back in the Verification Status view, expanding the results as shown in Figure 1.12 reveals

  • The method drawPlanet() of class com.surelogic.jsure.planetbaron.client.MapView requires the read lock to be held on its Planet parameter.

  • The method drawShip() of class MapView requires the read lock to be held on its Ship parameter.

  • The method drawShipMovementTrail() of class MapView requires the read lock to be held on its Ship parameter.

Clicking on the results shows that all three erroneous method calls originate in the method paintComponent(Graphics) of class MapView.

Figure 1.12. Expanded precondition results

Expanded precondition results

Looking at the method MapView.paintComponent(), we see that it draws the basic game map, and then iterates over all the ships and planets to draw them individually by calling the methods drawShipMovementTrail() (line 157), drawPlanet() (line 162), and drawShip() (line 168):

142:   @Override
143:   protected void paintComponent(Graphics g) {
144:     super.paintComponent(g);
145: 
146:     final int height = getHeight();
147:     final int width = getWidth();
148: 
149:     // fill the entire component with black
150:     g.setColor(Color.black);
151:     g.fillRect(0, 0, width, height);
152: 
153:     drawGridOutline(g);
154: 
155:     for (Ship s : GameMap.getInstance().getShips()) {
156:       synchronized (s) {
157:         drawShipMovementTrail(g, s);
158:       }
159:     }
160:     for (Planet p : GameMap.getInstance().getPlanets()) {
161:       synchronized (p) {
162:         drawPlanet(g, p);
163:       }
164:     }
165:     drawCursor(g);
166:     for (Ship s : GameMap.getInstance().getShips()) {
167:       synchronized (s) {
168:         drawShip(g, s);
169:       }
170:     }
171:   }

At first glance, it is not easy to spot the problem because all the method calls originate from within synchronized blocks that appear to lock on the correct Ship or Planet object.

1.3.3.7. Mixed Lock Paradigms

The problem in this case is that the synchronized block is not the correct mechanism to acquire the needed locks. As stated previously, the needed locks in this case are the read locks of the Ship/Planet objects, and these are acquired and released via explicit method calls.

What if we, like the author of this method, were too forgetful to identify this problem on our own? JSure has already pointed out this problem to us via three warnings that appear with the assurance results for ThingLock as shown below. Make sure that the is selected in the view toolbar so that suggestions and warnings are displayed in the view.

JSure generates three warnings, one for each bad synchronized statement, telling us that the object being synchronized on is not known to be a lock (because there is no relevant @RegionLock annotation), but that the f_lock field of each object is known to be a java.util.concurrent lock object named ThingLock. These warnings are meant to suggest that we are locking on the wrong object, and that perhaps we should be using the object referenced by the field f_lock as the lock instead. A quick inspection of the f_lock field declaration tells us the lock is a ReadWriteLock.

The call sites can be fixed by replacing the synchronized blocks with the appropriate tryfinally blocks. Here we need to make use of the lock getter method getThingLock() because f_lock is not visible. Change (or cut and paste) the code to look like the listing below:

  @Override
  protected void paintComponent(Graphics g) {
    super.paintComponent(g);

    final int height = getHeight();
    final int width = getWidth();

    // fill the entire component with black
    g.setColor(Color.black);
    g.fillRect(0, 0, width, height);

    drawGridOutline(g);

    for (Ship s : GameMap.getInstance().getShips()) {
      s.getThingLock().readLock().lock();
      try {
        drawShipMovementTrail(g, s);
      } finally {
        s.getThingLock().readLock().unlock();
      }
    }
    for (Planet p : GameMap.getInstance().getPlanets()) {
      p.getThingLock().readLock().lock();
      try {
        drawPlanet(g, p);
      } finally {
        p.getThingLock().readLock().unlock();
      }
    }
    drawCursor(g);
    for (Ship s : GameMap.getInstance().getShips()) {
      s.getThingLock().readLock().lock();
      try {
        drawShip(g, s);
      } finally {
        s.getThingLock().readLock().unlock();
      }
    }
  }

Once the changes to the MapView class are completed, run another JSure scan.

At this point the complete model for ThingLock assures along with the associated @ThreadSafe models:

Why is there a red dot on the verification result? In this case it is because of the use of Vouch annotations. It could also mean that the code contains a Assume annotation. The use of the Vouch turns what would have been an result into a .

There is a simple way to find all the vouches in your code using the JSure Quick Search view. In this view select the Annotation filter and scroll down and check the Vouch. The graph shows you how many of each type of annotation. In this case there are several Vouch annotations in the code. To see the annotation, select Show in the menu to the right of the filter.

You are now finished with this tutorial. The next tutorial step through finding what was a real bug in a concurrency library.

1.3.4. Scanning code using Ant

This tutorial will demonstrate how to use the JSure Ant task to scan the PlanetBaron project in a script and load the resulting scan document into your Eclipse. The JSure Ant task is used to automate scans as part of a QA or nightly build process. This tutorial assumes you have run the previous tutorial. You may skip the previous tutorial but you will need to load the JSureTutorial_PlanetBaron project into your workspace.

First you will need to download and unzip the JSure Ant task from this location on the SureLogic web site. This will create a jsure-ant directory on your machine at the location you unzip the file.

In the PlanetBaron project create a file at the root of the project called jsure-ant-scan.xml with the below contents.

<?xml version="1.0" encoding="UTF-8"?>
<project name="JSureTutorial_PlanetBaron" default="scan" basedir=".">

	<!-- (CHANGE) path to the unzipped the JSure Ant task -->
	<property name="jsure.ant.home" location="C:\\Users\\Tim\\jsure-ant" />

	<!-- (COPY) JSure Ant task setup stuff -->
	<path id="jsure-ant.classpath">
		<dirset dir="${jsure.ant.home}" includes="lib/com.surelogic.*" />
		<fileset dir="${jsure.ant.home}" includes="lib/**/*.jar" />
	</path>
	<taskdef name="jsure-scan" classname="com.surelogic.jsure.ant.JSureScan">
		<classpath refid="jsure-ant.classpath" />
	</taskdef>


	<path id="prj.classpath">
		<fileset dir="${basedir}" includes="**/*.jar" />
	</path>

	<target name="scan">
		<javac srcdir="${basedir}/src" destdir="${basedir}/bin" source="1.7"
			includeantruntime="false">
			<classpath refid="prj.classpath" />
		</javac>

		<jsure-scan srcdir="${basedir}/src" source="1.7"
			includeantruntime="false" jsureanthome="${jsure.ant.home}"
			projectname="JSureTutorial_PlanetBaron">
			<classpath refid="prj.classpath" />
		</jsure-scan>
	</target>
</project>

You will have to modify the setting for jsure.ant.home to reference where you located the jsure-ant directory on your machine.

Within Eclipse run this as an Ant task by selecting the XML file and selecting Run As | Ant Build. Output from the running task will appear in the console as seen in Figure 1.13.

Figure 1.13. Console output from scanning PlanetBaron with Ant inside Eclipse

Console output from scanning PlanetBaron with Ant inside Eclipse

You should be able to see from the console output that the project was scanned, and a file containing the results was written to disk. In our example, the output file is located in the JSureTutorial_PlanetBaron directory and is called JSureTutorial_PlanetBaron.2015.06.30-at-14.29.01.442.jsure-scan.zip. You can change the output directory by adding a jsurescandir attribute to the task.

We can import this scan into Eclipse when we are ready to look at the results. To do this we choose JSureImport Ant/Maven Scan.... The tool will then notify you once the scan has finished importing.

Figure 1.14. Successful scan import

Successful scan import

This tutorial has introduced the use of the JSure Ant task. You now know how to use the Ant tasks to add JSure to your QA process or nightly build. Reference documentation for the JSure Ant tasks is found in Section 2.5.

1.3.5. Uncovering a bug in java.util.logging

In this tutorial we examine a real-world bug in the java.util.logging portion of the Java standard library. This is a check-then-act bug that was reported to Sun when it appeared in Java 5 but was not fixed until Java 7. Our version of the code for this tutorial is changed to be in a different package so that it doesn't conflict with the standard library.

The project we will be using is named JSureTutorial_java.util.logging.

1.3.5.1. A check-then-act problem

In the tutorial project go into the com.surelogic.util.logging package and open the Logger class in the Java editor. Examine the lines listed below.

404: public void log(LogRecord record) {
405:   if (record.getLevel().intValue() < levelValue || levelValue == offValue) {
406:     return;
407:   }
408:   synchronized (this) {
409:     if (filter != null && !filter.isLoggable(record)) {
410:       return;
411:     }
412:   }

Of interest is line 409 that filter is first checked that it is not null, followed by its use: !filter.isLoggable(record). This occurs in order because the && is a shortcut logical and which will return false if the first expression is false. This code is reasonable because if, in fact, filter is null then the expression !filter.isLoggable(record) would throw a NullPointerException.

A lock on the instance is held as this operation occurs: this lock is acquired using synchronized (this) at line 408. Therefore, it appears that the programmer intent is to hold a lock on the class when the filter is accessed. In fact, the Logger class is intended to be threadsafe. You can see this way up at line 121 which is within the Javadoc on the class declaration.

121:  * All methods on Logger are multi-thread safe.

We now turn our attention to the getter and setter for the filter field in the implementation of Logger. This code, which beings at line 365, is listed below.

365:   /**
366:    * Set a filter to control output on this Logger.
367:    * <P>
368:    * After passing the initial "level" check, the Logger will call this Filter
369:    * to check if a log record should really be published.
370:    * 
371:    * @param newFilter
372:    *            a filter object (may be null)
373:    * @exception SecurityException
374:    *                if a security manager exists and if the caller does not
375:    *                have LoggingPermission("control").
376:    */
377:   public void setFilter(Filter newFilter) throws SecurityException {
378:     if (!anonymous) {
379:       manager.checkAccess();
380:     }
381:     filter = newFilter;
382:   }
383: 
384:   /**
385:    * Get the current filter for this Logger.
386:    * 
387:    * @return a filter object (may be null)
388:    */
389:   public Filter getFilter() {
390:     return filter;
391:   }

The problem is that neither the setter nor the getter follow the locking model. Worse, the Javadoc at line 372 and line 387 makes it clear that a value of null is an acceptable value for the filter field.

The access of the filter field without holding the proper lock is the concurrency problem. We refer to this as a check-then-act problem because the change to null could occur, via the setter, after the null check at line 409, but before the use of the field in the !filter.isLoggable(record). Causing the program the throw a NullPointerException.

1.3.5.2. Causing a Logger to throw a NullPointerException

The Logger class can be exercised to throw a NullPointerException. We have included a small test program that has several threads obtain the same Logger instance and repeatedly change the filter from a value to null while logging output. This code is shown in Figure 1.15.

Figure 1.15. The concurrent exercise program to cause the library bug to throw a NullPointerException

The concurrent exercise program to cause the library bug to throw a NullPointerException

If you launch this program in Eclipse it will sometimes complete normally. Sometimes one thread will throw a NullPointerException. Sometimes more than one thread will throw a NullPointerException. This is due to the unpredictable nature of this type of concurrency problem.

1.3.5.3. (Optional) Use of Flashlight dynamic analysis to show the problem

If you have the SureLogic Flashlight tool you can use it to reliably uncover the problem with the filter field within the Logger class. Launch the program with Flashlight using either the Flashlight menu or the in the Eclipse launch toolbar. Let it finish its execution, and let the tool automatically prepare the data collected for querying. When prompted switch to the Flashlight perspective. The result should appear as shown in the screenshot below.

The news item of interest is boxed in red in the image above: Shared fields with writes that do not happen-before subsequent reads. What the Flashlight tool has observed during the program run is that there are (instance) fields that are not safely shared between two or more threads per the Java memory model. In particular, the tool could not establish that a write in one thread happened-before a read in a second thread. Click on this finding to find out what fields were observed to have this problem.

The Flashlight findings indicate the concurrency problem we described in the section above. However, it did this by examining if state was safely shared per the memory model, whereas we were examining consistent locking. Dynamic analysis results using the Java memory model are usually more precise, but Flashlight also noted the lack of consistent lock usage for the filter field within the Logger class. You can see this if you select the Shared fields with no common lock held for each access result in the bad news report, or the What fields (non-static) have an empty lock set after object construction? query from the Query Menu view.

Flashlight contains rich information about these findings that you can feel free to dig into, however, we will now turn our attention back to JSure. We want to now model the programmer intended locking model and fix the code bug.

1.3.5.4. Use of JSure to show the problem

Now let's switch back to JSure. To see the problem scan the project with JSure and examine the results. Some simple modeling has been done to the code. In particular, @ThreadSafe has been annotated on Filter and @Immutable on its subtype MyFilter in the concurrent exercise program described above. These both are verified by the tool.

The @ThreadSafe on Logger is unable to be verified by the tool. The image above expands these results. As is typical of placing @ThreadSafe on a complex mutable class, further annotation is needed to bring this model into consistency. Our focus for this tutorial is the filter field within the Logger class.

The results for the filter field are expanded in the image above. Note that there are two parts of convincing JSure that the field respects the assertion that the class is actually thread safe: (1) the field itself, (2) the object referenced by the field. In this case the latter is okay because the declared type of the field is Filter, which has been proven thread safe. The field itself needs to be protected. Because the filter field is mutable, and due to the (albeit inconsistent) use of locking in the class implementation, we will annotate that this field is protected with a lock. Add the annotation @RegionLock("FilterLock is this protects filter") to the top of the class so that the code looks as shown below.

At this point re-scan the project with JSure. As expected, the inconsistent locking of the filter field is noted by the tool.

If you click on the two protected accesses you will see that they refer to the references to filter in the log method. The two unprotected accesses reference the unprotected accesses in the getter getFilter and setter setFilter methods.

1.3.5.5. Fixing the inconsistent locking problem

To fix the issue of inconsistent locking on the filter field in the Logger class we need to change the getter getFilter and setter setFilter methods to hold a lock on this. This can be done in one of two ways: (1) declaring the method to be synchronized, and (2) adding a synchronized block on this within each of the methods.

So change setFilter to look like

public synchronized void setFilter(Filter newFilter) throws SecurityException {
  if (!anonymous) {
    manager.checkAccess();
  }
  filter = newFilter;
}

or

public void setFilter(Filter newFilter) throws SecurityException {
  if (!anonymous) {
    manager.checkAccess();
  }
  synchronized (this) {
    filter = newFilter;
  }
}

depending upon your preference. Further, change getFilter to look like

public synchronized Filter getFilter() {
  return filter;
}

or

public Filter getFilter() {
  synchronized (this) {
    return filter;
  }
}

depending upon your preference. Now, re-scan the project with JSure and the lock model should now be found consistent.

Also note in the results above that the filter field is now able to support its portion of the overall @ThreadSafe assertion on the Logger class. To complete all the modeling of the Logger class would take further work, which we will not do as part of this tutorial.

1.3.5.6. Quickly uncovering trouble during code evolution

A benefit of JSure annotations is that they stay with the code as it evolves over time. This can help you to spot the introduction of concurrency defects quickly in your software system. To illustrate this add a new method called getAnonymousLoggerFilter to the Logger class:

public static Filter getAnonymousLoggerFilter() {
  return getAnonymousLogger().filter;
}

So your code should appear as shown below.

This method, at first glance, may appear to be a nice addition that allows client code to directly get a reference to the filter being used by the anonymous logger.

At this point scan the project again with JSure. It finds the locking model has become inconsistent due to this code change.

This is because the filter field is accessed by this method without holding the lock. Well, one idea would be to mirror the getAnonymousLogger method and declare the method to be synchronized. This change is shown below.

Make this code change and re-scan the project with JSure. Again the tool reports model–code inconsistency. What is wrong? The problem is that we are holding the wrong lock. Because the getAnonymousLoggerFilter method is declared to be static, adding synchronized to the method obtains a lock on the Logger class—not on the anonymous logger instance! To fix this problem change the method implementation to the code listed below.

public static Filter getAnonymousLoggerFilter() {
  Logger anon = getAnonymousLogger();
  synchronized (anon) {
    return anon.filter;
  }
}

Save your changes and re-scan the project with JSure. The locking model for the filter field should once again be consistent.

Note the value of the annotations for keeping the intended concurrency policies of your code consistent with its implementation as code evolves. We are now finished with this tutorial.

1.3.6. Verifying util.concurrent

In this example we examine util.concurrent from Doug Lea, a concurrency library that eventually grew into the current java.util.concurrent library. This code is located in the JSureTutorial_util.concurrent.SynchronizedVariable project which was previously loaded into your workspace.

The class SynchronizedVariable is the parent class of several thread-safe wrapper classes. We can view this hierarchy in Eclipse by

  1. Selecting NavigateOpen Type in Hierarchy….

  2. Entering SynchronizedVariable in the resulting dialog box.

You should see a hierarchy like in Figure 1.16.

Figure 1.16. Class Hierarchy rooted at SynchronizedVariable

Class Hierarchy rooted at SynchronizedVariable

1.3.6.1. Declaring Protected State For Type Hierarchy

In this example we model the locking policy of SynchronizedVariable and its subclasses. Open the SynchronizedVariable in the Java editor and annotate it as shown below. Don't forget to import the annotation types.

@Region("protected VarState")
@RegionLock("VarLock is lock_ protects VarState")
public class SynchronizedVariable implements Executor {
  …
}

This creates an empty protected (as in protected visibility) region called VarState that is protected by holding a lock on the object referenced by the field lock_.

The class SychronizedVariable does not have any fields besides the lock reference: it is in the subclasses that we need to map data into VarState. A subclass can add state to any region declared in a superclass that is visible to it according to standard Java visibility rules. Add the following to the value_ field in the SynchronizedLong class:

  @InRegion("VarState")
  protected long value_;

Note that this is an example where we need to explicitly declare the region. Region inference only works within a class, this is too complex of a model for the tool to infer. Now scan the project with JSure. To do this choose JSureVerify Project from the Eclipse main menu or use the keyboard shortcut Ctrl+Alt+Shift+V.

At this point, if you drill into the Verification Status view, you should see the following results:

You could also use the X Results query we created during the BoundedFIFOJSure tutorial. To do this click on X Results link at the bottom of the JSure Quick Search view.

The lock model does not verify because there are three unprotected field accesses. We focus now on investigating these inconsistent results.

Closer inspection of the negative lock results (by clicking on the results in either view) reveals that the first two of these are field initializations in the class’s constructors. In the case of the constructors SynchronizedLong(long) and SynchronizedVariable(), we cannot use the annotation @Unique("return") because the constructor SynchronizedVariable() aliases the new object into the field lock_:

  /**
   * Create a SynchronizedVariable using itself as the lock
   **/
  public SynchronizedVariable() {
    lock_ = this;
  }

Instead we need to use state and thread effects to establish that the constructors are thread-confined. In general, a constructor is also considered to be thread-confined if it does not start any threads and only writes to the object under construction. This prevents the thread executing the constructor from passing information to any new or existing threads, respectively. The constructor may declare any amount of read effects. In this case, it is sufficient to declare that the constructors have no effects.

Annotate the constructors to be thread-confined by adding

  @Unique("return")

to SynchronizedVariable(Object) and SynchronizedLong(long, Object), and by adding

  @RegionEffects("none")
  @Starts("nothing")

to SynchronizedVariable() and SynchronizedLong(long).

Scan the project with JSure. The results below also assume you have left the JSureUse Uniqueness Verifying Analysis menu item checked — and, as such, uniqueness annotations are being tool verified.

1.3.6.2. An Implementation Bug

Scan the project with JSure. It is curious that there is still one unprotected field access. Note that the JSure Quick Search immediately updates to show the remaining inconsistent analysis result.

It is simple to "sync" up the Verification Status view. Use the context menu on the one result in the JSure Quick Search and select Open In Proof Context. This will "sync" the two views. When you select the result the tool will also bring up the code in both the Java editor and the JSure Historical Source view.

What is wrong? We see that the unprotected access is in the return statement of the swap method:

  public long swap(SynchronizedLong other) {
    if (other != this) {
      SynchronizedLong fst = this;
      SynchronizedLong snd = other;
      if (System.identityHashCode(fst) > System.identityHashCode(snd)) {
        fst = other;
        snd = this;
      }
      synchronized (fst.lock_) {
        synchronized (snd.lock_) {
          fst.set(snd.set(fst.get()));
        }
      }
    }
    return value_;
  }

This is incorrect for two reasons:

  1. By occurring outside of the synchronized blocks the return is not atomic with the rest of the method and thus another thread could alter the value of the value_ field before swap returns.

  2. Java does not guarantee that a read of the two 32-bit halves of a long value is atomic.

This is a real bug that existed in the released library. It was, in fact, uncovered using an earlier version of the JSure tool. It was quickly fixed.

This method is tricky to fix because of its preamble which both short-circuits the swap if both objects are the same, and (2) sorts the objects according to their identity hash code to establish a global lock ordering to prevent deadlock. To correct the method and preserve the atomicity intent (which is not assured by JSure), we must change it to

  public long swap(SynchronizedLong other) {
    if (other == this) return get();
    SynchronizedLong fst = this;
    SynchronizedLong snd = other;
    if (System.identityHashCode(fst) > System.identityHashCode(snd)) {
      fst = other;
      snd = this;
    }
    synchronized (fst.lock_) {
      synchronized (snd.lock_) {
        fst.set(snd.set(fst.get()));
        return get();
      }
    }
  }

Using the synchronized get method helps alleviate the problem that it is not statically detectable to know whether the lock on fst or snd is the correct lock for this.value_ inside the synchronized blocks.

Change the code of the swap method in the SychronizedVariable class as shown above and run a JSure scan. The VarLock lock model is judged to be consistent with the code:

This completes this tutorial. It has given you insight into modeling complex library code and uncovering (what was) a real-world defect.

1.3.7. Effective effects

One of the kinds of design intent that a programmer can declare and assure with JSure is method effects that describe program state that may be accessed when the method executes. Specifically, the @RegionEffects method annotation is used to declare an upper bound on the runtime state that a method or constructor may read or write. Affected state is expressed in terms of portions of objects, called regions, that are used to abstract away fields. This tutorial elaborates

  • The @RegionEffects annotations.

  • The region hierarchy.

  • Describing effects using targets.

  • @Unique fields and region aggregation.

  • Effect assurance and effect masking.

  • Regions, effects and method overriding.

To make effective use of JSure, you should be familiar with how to declare effects on method and constructors. Any program that makes non-trivial use of a @Unique (or @Borrowed) field is likely to require the addition of some effects annotations to support the assurance of the unique field. The reason for this is described below, after a brief introduction to declaring simple effects.

All the code used for this tutorial is contained in the JSureTutorial_EffectiveEffects project.

[Note]This tutorial is incomplete

This tutorial is a work in progress. The following section is meant to describe the basics of using effects with JSure. Future sections will describe the rest of the topics listed above, as well as the relationship between effects and the uniqueness analysis.

1.3.7.1. A Simple Variable Class

In this example we examine the SimpleVar class in the JSureTutorial_EffectiveEffects project which was previously loaded into your workspace.

Class com.surelogic.simple.SimpleVar in declares a simple class that implements an integer variable:

The methods set() and get() are annotated with @RegionEffects annotations. The methods getAndSet() and swap() are not yet annotated. The annotation on set() declares that the method writes the Instance region of the object referenced by this. The Instance region always contains all the non-final fields in an object. The declaration says that the method may read or write any mutable field of the object referenced by the method's receiver. In this implementation, the method simply assigns a value to the one-and-only field value. Similarly, the annotation on get() declares that the method may read any mutable field of the object referenced by the method's receiver. In this example this:Instance and Instance are interchangeable—they refer to the same state. Which you use depends upon your personal preference.

Run the JSure analysis to verify the project and switch to the Code Verification perspective. The effects declared on the set() and get() methods should verify. The Verification Status should look like the following:

We see that the annotation on get() assures because the only effect in the method is a read of the field value of the receiver, reads this:value, at line 15, the return statement. The field value is a subregion of Instance, and thus the actual effect of the method's implementation is included in the declared effects. Similarly, the implementation effect writes this:value of the assignment statement at line 10 in set() is included in the method's declared effects.

Methods that are not annotated with a @RegionEffects annotation are assumed to be annotated with @RegionEffects("writes java.lang.Object:All"), a declaration that means the method may read or write any field of any object in the heap; that is, the method can affect anything. Unannotated methods are not verified against this assumed annotation, however, because the default effects declare an upper-bound and no Java method can effect more than any object in the heap (so no analysis is required to verify such a claim). The assumed annotations are used, rather, when a call to an unannotated method is analyzed. Instead of verifying unannotated methods, JSure infers a legal @RegionEffects annotation for each unannotated method. These can be seen in the Proposed Promises view but are not displayed by default. To display them uncheck Show Only Proposals Inferred From Other Promisesin the view menu as shown below.

In the case of our example, there are three proposals:

  • One at line 6 for the implicit constructor Var().

  • One at line 18 for the method getAndSet().

  • One at line 24 for the method swap().

The effect inferred for the constructor is none. That is, the constructor has no effects on objects visible to the caller of the constructor. This means that the caller does not receive a reference to the newly created object until after the constructor returns, it is incapable of observing any effects that may have occurred to that object. Thus a constructor does not have to declare any effects on the Instance region of the receiver. We can make the effect declaration for the constructor explicit by selecting the proposal RegionEffects("none") in the view and choosing Add promises to code… in the contextual menu:

Because the constructor was originally implicit, it needs to be made explicit to be annotated. The refactoring applied in insert the annotation inserts the constructor declaration as well in this case:

We skip ahead momentarily to the proposal on line 24 for swap(): writes java.lang.Object:All. This proposal derives principally from the method call other.getAndSet(this.value). Because the called method getAndSet() is unannotated, it is considered to have the effect writes java.lang.Object:All, and this becomes the proposed effect declaration for swap(); the effect writes this:Instance from the method call this.set(otherVal) is subsumed by this effect.

JSure proposes the effect writes this:Instance for the method getAndSet(). This inference is very straightforward: the method reads and writes the field value of the object referenced by the receiver. Because a write effect includes the possibility of reading, only a write effect needs to be declared. The region Instance is used instead of the field value to preserve abstraction because the field is private and the method is public. After we apply this promise, the class is as follows:

Reverify the project to get the results

Of particular interest are the results for the constructor at line 6:

  • First we see that "nothing" is checked by "nothing" at line 6. This refers to the fact that the effects, nothing, of the implicit super constructor call are consistent with the declared effects of nothing. The prerequisite assertion for this result is the declared effects of the constructor Object() of class java.lang.Object.

  • Second, the effect writes this:value that originates from the field initialization at line 8 is ignored (as described above) because the affected region is part of the object being constructed.

We also see that the newly declared effects for getAndSet() assure. Furthermore, JSure uses the annotation on getAndSet() when proposing a promise for the still unannotated swap(). The Proposed Promises view now shows

The effect writes other:Instance, this:Instance means that the method may write the Instance region of the object referenced by the other at the start of the method, as well as the Instance region of the object referenced by the receiver. Add the promise to the code, and reverify the project. The annotation on swap() assures:

  • The method call other.getAndSet(…) at line 29 has the effect writes other:Instance. This effect assures against the declared effect writes other:Instance. The results also show the origin of this effect:

    1. The method getAndSet() is annotated with writes this:Instance.

    2. In the method call, the formal parameter this is bound to the variable other.

    3. At the point of the method call, the variable other still refers to the object it refers to at the start of the method call.

  • The field read this.value at line 29 has the effect reads this:Instance that is assured by the declared effect writes this:Instance.

  • The method call this.set(…) at line 30 has the effect writes this:Instance that also assures against the declared effect writes this:Instance. Again, because this is a method call, the results show the origin of the actual effect:

    1. The method set() is annotated with writes this:Instance.

    2. In the method call, the formal parameter this is bound to the receiver this of the calling method.

The class Var is now fully annotated with effects declarations and verified against them. What remains to be demonstrated is what a @RegionEffects assurance failure looks like. Change the effects annotation on set() to be reads this:Instance:

After reverifying the project, the results will show assurance failures:

The method @RegionEffects annotation on set() does not assure because the effect writes this:Instance is not accounted for by any of the effects in the annotation. The annotation on method swap() is also marked as unverified, because its assurance depends on the assurance of set(). As in the case of unannotated methods, JSure infers a legal, assurable @RegionEffects annotation for methods with unverified annotations. Select the proposed promise under the unaccounted for effect and select Annotate code… in the contextual menu to replace the annotation with the correct one inferred by JSure. Finally, run the JSure analysis to verify the fixed annotation.

1.3.7.2. Effects and Uniqueness

While annotating effects on classes documents worthwhile design intent in its own right, the most immediate reason you may need to add @RegionEffects annotations to a class is because of @Unique fields. Consider the classes in the com.surelogic.unique package. The main class EffectsAndUniqueness contains a single uniquely referenced integer array. The need for effects arises when the reference in the array is passed as an actual parameter in a method call, as in the method doStuff1():

public class EffectsAndUniqueness {
  @Unique
  private int[] values;
  
  // ...
  
  public int doStuff1() {
    return Util.sum(values);
  }
}

where the method Util.sum() has a @Borrowed parameter:

public class Util {
  public static int sum(@Borrowed final int[] array) {
    int sum = 0;
    for (final int v : array) {
      sum += v;
    }
    return sum;
  }
  
  // ...
}

When these classes are assured, the method doStuff1() fails to assure:

We have the error message Unique field values, made undefined by evaluating the actual arguments, may be read as an effect of the call unique.Util.sum(this.values). (Note this message does not match in initial unique+from implementation.) Basically, analysis determines that it is possible that executing the method call will cause the field values to be read. But how does it determine this, and why does it matter?

The field values is declared to be unique. Unique assurance thus requires that the object referenced by the field is never accessible by another reference. When the field is passed as an actual parameter to a method, the field becomes aliased if the formal parameter is @Borrowed; otherwise it becomes undefined according to the normal rules of using a unique field. In either case, assurance needs to determine if the called method may read from the field whose reference was passed as a formal parameter. In the case of a @Borrowed parameter, the field would be aliased during the method call because the object it referenced would be used by the method under two names: that of the field and that of the formal parameter. In the non-@Borrowed case, the method would end of reading from an undefined field because there is no way to assign the field a new value after it is read as an actual parameter but before the method is invoked. Analysis uses the declared effects of the called method to determine if it may read the unique field. Because the method sum() is unannotated, it is treated as being able to read or write any object, and thus it is possible it could read the field values of the receiver.

It is obvious by looking at the body of the method sum() that the only state it reads is the contents of the array referenced by its argument array. We can eliminate the uniqueness assurance failure by annotating the method with @RegionEffects("reads array:Instance"). You can do this manually or by adding the proposed promise from the Proposed Promises view. The classes should look like the following

After reverifying the project, the method doStuff1() assures:

The method doStuff2() exists to demonstrate the same issue but with a non-@Borrowed formal parameter: it calls the method nonBorrowedSum(). The try–finally block is necessary to make sure that the field values is made defined in the case that calling the method nonBorrowedSum() causes an exception to be thrown. The field must be defined on exit of doStuff2(), or else uniqueness analysis will raise an error. In this case, we still see that we have the same error invoking nonBorrowedSum() as we did invoking sum():

This can be fixed the same way: by adding @RegionEffects("reads array:Instance") to the method nonBorrowedSum(). It can also be fixed by rewriting the doStuff2() to reassign a value to values before the method call is made. This also eliminates the need for the unsightly try–finally:

After making the above change, the verification results are

1.3.7.3. Advanced Effects Examples

The package com.surelogic.advanced contains examples of using @RegionEffect annotations in more advanced situations:

  • Methods with read and write effects.

  • Effects on static fields.

  • Effects on referenced objects, including arrays.

  • Effects on inner class objects.

  • Declaring abstract regions.

  • Effect declarations and method overriding.

The listing below contains the classes in the package.

package com.surelogic.advanced;

import com.surelogic.RegionEffects;
import com.surelogic.Unique;

@SuppressWarnings("unused")
public class Examples {
  public static int staticField = 0;

  public int i;

  private AdvancedVar var;

  @Unique
  private AdvancedVar uniqueVar;

  private int[] array;

  @Unique
  private final int[] uniqueArray = new int[10];

  @RegionEffects("none")
  public Examples() {
    super();
  }

  /*
   * Effects on primitive types are not reported. So we don't care that 'a' and
   * 'b' are used, but we do report that the field 'i' of the receiver is
   * affected. Furthermore, 'i' is a public field, so we can explicit mention it
   * in the annotation on a public method.
   */
  @RegionEffects("reads i")
  public int m1(int a, int b) {
    return a * (this.i + b);
  }

  /*
   * Effects on newly created objects are not interesting to the caller of the
   * method, and do not need to be reported.
   */
  @RegionEffects("reads inVar:Instance")
  public static AdvancedVar m2(final AdvancedVar inVar, final int delta) {
    final AdvancedVar outVar = new AdvancedVar(inVar.get());
    outVar.inc(delta);
    return outVar;
  }

  /*
   * Declaring both read and write clauses. The object referenced by 'this.var'
   * is unknown to the caller, so we have to declare that the method could write
   * the 'Instance' region of any Var object.
   */
  @RegionEffects("reads Instance; writes any(AdvancedVar):Instance")
  public void m3(final int delta) {
    this.var.inc(delta);
  }

  /*
   * Looks like the above, but the in this case the field 'uniqueVar' is
   * annotated with @Unique: the field is known declared to (and separately
   * assured to) be the only field that refers to the object that it references.
   * In this case, the state of the referenced Var object is considered to be
   * part of the 'uniqueVar' field itself. So writing to the Var object via the
   * inc() method creates the effect "writes this:uniqueVar".
   * 
   * Also, in this case we can use a private field in the annotation because the
   * method is declared to be private.
   */
  @RegionEffects("writes this:uniqueVar")
  private void m4(final int delta) {
    this.uniqueVar.inc(delta);
  }

  /*
   * Arrays are objects, and accessing their elements is like accessing the
   * fields of objects. Like m5(), we have to declare that we don't know which
   * object is being modified by the method.
   * 
   * Also, it doesn't matter whether the "writes" or "reads" clause comes first.
   */
  @RegionEffects("writes any(java.lang.Object):Instance; reads Instance")
  public void m5(final int v) {
    for (int i = 0; i < array.length; i++) {
      array[i] = v;
    }
  }

  /*
   * The array is uniquely referenced, and thus aggregated. In this case, the
   * field 'uniqueArray' is final, so the regions of the array object are
   * aggregated directly into the 'Instance' region of the receiver.
   */
  @RegionEffects("writes Instance")
  public void m6(final int v) {
    for (int i = 0; i < uniqueArray.length; i++) {
      uniqueArray[i] = v;
    }
  }

  /*
   * Effects on static fields must also be declared. This method affects two
   * static fields, the field 'staticField' of the class Examples, and the field
   * 'staticField' of the class StaticState. Both have the same name, but are
   * distinct regions in the effects system.
   */
  @RegionEffects("reads staticField, com.surelogic.advanced.StaticState:staticField")
  public static int m7() {
    return staticField + StaticState.staticField;
  }

  /*
   * Like the above, but with a different annotation. The field 'staticField' in
   * the class StaticState, is declared to be a subregion of the abstract region
   * 'S'. So we can make a more general effect declaration.
   */
  @RegionEffects("reads staticField, com.surelogic.advanced.StaticState:S")
  public static int m8() {
    return staticField + StaticState.staticField;
  }

  /*
   * Like the above, but with a different annotation. The field 'staticField' in
   * the class StaticState, is defined to be within the predefined 'Static'
   * region. So we can make a more general effect declaration.
   */
  @RegionEffects("reads staticField, com.surelogic.advanced.StaticState:Static")
  public static int m9() {
    return staticField + StaticState.staticField;
  }

  protected class Inner {
    private int vv;

    @RegionEffects("none")
    public Inner(int v) {
      this.vv = v;
    }

    /*
     * Effects on outer objects (referenced by qualified receivers) must be
     * declared.
     */
    @RegionEffects("reads com.surelogic.advanced.Examples.this:i, this:Instance")
    public int sum() {
      return Examples.this.i + this.vv;
    }
  }

  /*
   * Although methods can be specific in describing their effects on outer
   * objects, it is hard to make use of these effects at the call site. Here we
   * have to declare that this method may read from any Example object because
   * given a reference to an object that is an instance of a nested class, we
   * have no way to know what are the outer objects of the instance. We do not
   * have to report the effect on the instance of Inner because that object is
   * known to be created local to the annotated method.
   * 
   * This lack of precision hasn't been a problem yet. If it becomes one, it is
   * possible to use a local data flow analysis to sometimes recover some of the
   * outer object information. For example, in this case, it is not difficult to
   * use flow analysis to discover that 'i' refers to an object created by the
   * expression "e. new Inner(0)", then recursively discover that 'e' originates
   * from "new Examples()", and deduce that the "Examples.this" argument of the
   * sum() method is really the object returned by "new Examples()". In this
   * case, we would also ignore any effects on this locally created object.
   */
  @RegionEffects("reads any(com.surelogic.advanced.Examples):i")
  public static int useInnerClass() {
    Examples e = new Examples();
    Inner i = e.new Inner(0);
    return i.sum();
  }
}

package com.surelogic.advanced;

import com.surelogic.Borrowed;
import com.surelogic.RegionEffects;
import com.surelogic.Unique;

/* Basically like SimpleVariable, so nothing new to say here. */
public class AdvancedVar {
  protected int value;

  @RegionEffects("none")
  @Unique("return")
  public AdvancedVar(final int v) {
    value = v;
  }

  @RegionEffects("reads Instance")
  @Borrowed("this")
  public int get() {
    return value;
  }

  @RegionEffects("writes Instance")
  @Borrowed("this")
  public void set(final int v) {
    value = v;
  }

  @RegionEffects("writes Instance")
  @Borrowed("this")
  public void inc(final int v) {
    set(value + v);
  }
}

package com.surelogic.advanced;

import com.surelogic.Borrowed;
import com.surelogic.RegionEffects;
import com.surelogic.Unique;

public class UndoableAdvancedVar extends AdvancedVar {
  /* This field is implicitly a subregion of Instance */
  private int lastValue = 0;

  @RegionEffects("none")
  @Unique("return")
  public UndoableAdvancedVar(final int v) {
    super(v);
  }

  /*
   * The declared effects can be no greater than the declared effects of the
   * overridden method. But because we have added an additional field to the
   * Instance region, we can modify it too.
   */
  @RegionEffects("writes Instance")
  @Borrowed("this")
  public void set(final int v) {
    lastValue = value;
    value = v;
  }

  /*
   * This is a new method not present in the super class so it may be freely
   * annotated.
   */
  @RegionEffects("writes Instance")
  @Borrowed("this")
  public void undo() {
    final int temp = value;
    value = lastValue;
    lastValue = temp;
  }
}

package com.surelogic.advanced;

import com.surelogic.InRegion;
import com.surelogic.Region;
import com.surelogic.RegionEffects;

/* Declare a new public static abstract region S */
@Region("public static S")
public class StaticState {
  /* Declare that the field is a subregion of the abstract region S */
  @InRegion("S")
  public static int staticField = 1;

  @RegionEffects("reads S")
  public static int getStaticField() {
    return staticField;
  }

  @RegionEffects("reads Static")
  public static int getStaticFieldAnotherWay() {
    return staticField;
  }
}

1.3.8.  Verifying non-null references

This tutorial demonstrates the use of @NonNull, @Initialized, and @TrackPartiallyInitialized annotations for declaring intent regarding non-null references. We assure two classes that could be part of a graphics package, Point and Rectangle. These classes are contrived, based on code patterns that we have encountered in production code. We use the tutorial to illustrate some complex modeling issues that may come up in your code. That said, typical modeling of null reference design intent is usually simpler than the contrived code we present below.

The class Point implements an immutable two-dimensional point:

@Immutable
public class Point {
  private final int x;
  private final int y;
  
  public Point(int x, int y) {
    this.x = x;
    this.y = y;
  }
  
  public int getX() {
    return x;
  }

  public int getY() {
    return y;
  }
  
  public Point translate(int dx, int dy) {
    return new Point(x + dx, y + dy);
  }
  
  public boolean isAboveLeftOf(Point p) {
    return this.x <= p.x && this.y <= p.y;
  }
}

Besides the getter methods, the class has the method translate that returns a new point instance, and the predicate isAboveLeftOf that returns whether the point is above, and to the left of the given point.

The mutable class Rectangle has three fields, @NonNull point references, and a cached perimeter value:

public class Rectangle {
  private @NonNull Point topLeft;
  private @NonNull Point bottomRight;
  
  private int perimeter;
  
  // ...
}

Our assurance of this class is going to be based around the @NonNull annotations on the topleft and bottomRight fields.

Now scan the project with JSure by choosing JSureVerify Project from the Eclipse main menu and selecting the JSureTutorial_NonNull project. You can quickly do rescans by pressing the toolbar icon in the JSure Scans view.

1.3.8.1. Initial results

The initial assurance results from the Verification Status view are shown below:

First we see that the @Immuable annotation on Point assures because the only fields in the class are final integer values. Second we see two unsatisfied @NonNull annotations: two on the fields topLeft and bottomRight. The annotations on the fields are explicit in the code (see above).

The rest of the tutorial proceeds as follows:

  1. We add the @TrackPartiallyInitialized annotation to the Rectangle class. This annotation is supports verification of @NonNull fields.

  2. The annotations on the fields topLeft and bottomRight are assured by adding additional annotations to method parameters and method return values.

  3. The virtual annotations on the receivers of copyFrom and computePerimeter are assured.

  4. The code is refactored to avoid the problems raised by copyFrom and computePerimeter .

1.3.8.2. Assuring the fields

The first issue we need to fix is to add a @TrackPartiallyInitialized to the Rectangle class. We get a report of this missing annotation for each constructor in a class that has a @NonNull field. This annotation expresses the desire for tracking and explicit annotation of any partially initialized object during construction of a Rectangle instance. The @TrackPartiallyInitialized annotation is required on any class that has a @NonNull field to ensure the invariant holds during object construction. This is easy to add because the tool can make the edit to your code for you. Simply select the proposed promise and choose Annotate Code... from the context menu as shown below.

This will bring up a preview of the code edit as shown below.

Choose OK to have the tool add the annotation to the code. Next go ahead and rescan the project in JSure. Partial initialization is now tracked but not yet consistent due to the issues we will consider later in this tutorial.

We continue our work by expanding the results for the fields topLeft and bottomRight . They are used similarly by the class implementation and thus have similar results:

The diff highlights the addition of @TrackPartiallyInitialized to the code via a positive result for each constructor in the class. The @NonNull annotation for each field has a positive “Definitely assigned” result. This is good news. JSure requires the every non null field be explicitly initialized during construction, otherwise the field's value will be the Java language default null value. In this case, JSure is satisfied that the fields are definitely assigned by the constructor Rectangle(Point, Point) . However, the tool is not satisfied that the constructor Rectangle(Rectangle) initializes the fields. This is because the constructor invokes a method copyFrom to initialize the fields:

  /**
   * Copy constructor.
   */
  public Rectangle(Rectangle other) {
    copyFrom(other);
  }

The verifying analysis cannot be sure what the invoked method may do, and thus cannot be sure that the constructor will initialize the fields to non-null values. We revisit this problem later in the tutorial, but put it on the backburner for now.

The first unacceptable assignment result for each field refers to values being assigned to the fields in the constructor Rectangle(Point, Point) . The constructor is as follows:

  /**
   * Caller responsibility to insure that the points really are
   * top-left and bottom-right.  Origin (0, 0) is the top-left corner
   * of the canvas.
   */
  private Rectangle(Point topLeft, Point bottomRight) {
    this.topLeft = topLeft;
    this.bottomRight = bottomRight;
    computePerimeter();
  }

Because the formal parameters topLeft and bottomRight are unannotated they are allowed to be passed the value null , and thus the fields could be initialized to null in violation of their @NonNull annotation. The solution, as proposed in the results, is to annotate the two parameters with @NonNull . Go ahead and change your code as shown below. You can, of course, use the proposed promise feature of JSure to automatically add the two annotations.

  private Rectangle(@NonNull Point topLeft, @NonNull Point bottomRight)

Next we see that topLeft and bottomRight have unacceptable assignments due to the “return value of method call” translate() . This is a method from the class Point that returns a new point translated from the original:

  public Point translate(int dx, int dy) {
    return new Point(x + dx, y + dy);
  }

JSure rejects the assignments to the fields because without any programmer annotation it assumes that a method may return the value null. In this case the method always returns a new object, and thus always returns a non-null reference. We can annotate this by adding the @NonNull annotation to the method:

  @NonNull
  public Point translate(int dx, int dy) {
    return new Point(x + dx, y + dy);
  }

Add the annotation and reverify the project. The five unacceptable assignments we just looked at are now acceptable. If you have Highlight differences from last scan button selected on the view, the changes to the results are highlighted in yellow:

The initialization of the topLeft in the constructor Rectangle(Point, Point) is now satisfied by the annotation on the formal parameter. Furthermore, calls to the constructor itself are also now verified to pass only non- null values as actuals. In this case, there is one call site and it passes a new object:

Similarly, the assigned to topLeft in Rectangle.translate() is now satisfied by the annotation on the return value of Point.translate() . And the chain of evidence continues to the actual return value of the method (the creation of the new Point object):

The results are similar for the field bottomRight.

Both fields have an “Acceptable assignment” result that shows with a to the lower-left. This means that some annotation that the chain of evidence relies on does not assure. In this case, the annotation is a recursive reference to the @NonNull annotation on the field itself:

You can tell the reference is recursive because of the upward pointing arrow. The reference is caused by an assignment in method copyFrom() where the the value of the field in one object is copied to the field in another object:

  public void copyFrom(Rectangle other) {
    topLeft = other.topLeft;
    bottomRight = other.bottomRight;
    perimeter = other.perimeter;
  }

This chain of evidence will sort itself out once the other assurance failures under the @NonNull annotation are corrected.

There is one more “Unacceptable assignment” for the field bottomRight:

The assignment in question is in the method setBottomRight() as is shown in the image above. This is another case of the field being assigned the value from an unannotated formal parameter. The solution once again is to add @NonNull to the formal parameter newCorner. Go ahead and do this now as shown below (you can use the tool-proposed promise to automatically make this edit).

  public void setBottomRight(@NonNull Point newCorner)

You may notice that just before setBottomRight() in the source code is the method setTopLeft(). This begs the question, why there is not a similar assurance failure of the assignment to topLeft in that method. The answer lies in the condition of the if-statements used to check that the top-left–bottom-right invariant on the fields is maintained. In setBottomRight() the expression !topLeft.isAboveLeftOf(newCorner) is used, with the field reference used as the receiver to isAboveLeftOf(). But in the method setTopLeft(), the expression !newCorner.isAboveLeftOf(bottomRight) is used, with formal parameter newCorner used as the receiver. Why does this matter? When analyzing the body of the method setTopLeft(), the analysis knows that receivers must always be non-null, or else the Java runtime will throw a NullPointerException. So the analysis knows that in any code that executes after the dereference of newCorner in the conditional of the if-statement the value of newCorner must not be null. It would still be wise from a documentation point of view to annotate the formal parameter of setTopLeft as @NonNull. Do this now and reverify the project.

The assignment in setBottomRight now assures:

We now redirect our attention away from the @NonNull annotations on the fields topLeft and bottomRight. We want to work to verify the @TrackPartiallyInitialized added earlier.

1.3.8.3. References to partially initialized objects

We now visit the unassured @TrackPartiallyInitialized annotation. If you expand this result several issues show up. The first shows a good chain of @TrackPartiallyInitialized up the superclass hierarchy of the Rectangle class. In this case this only includes java.lang.Object (which is annotated in XML). We start fixing issues with the last one reported about the receiver of Rectangle.computePerimeter().

What does this chain of evidence mean exactly? The result is on the method call computePerimeter() in the constructor Rectangle(Point, Point):

  private Rectangle(@NonNull Point topLeft, @NonNull Point bottomRight) {
    this.topLeft = topLeft;
    this.bottomRight = bottomRight;
    computePerimeter();
  }

JSure does not like the reference from this that is being used as the receiver to the method computePerimeter(). Specifically, unless otherwise annotated, a method expects that its receiver is @NonNull, but JSure finds in this case that the receiver is @Initialized(through="Object"). What does this mean? It means that the object referenced by this in the constructor is partially initialized, in this case through class Object. An @Initialized(through="X") reference is (1) never null ; and (2) only guaranteed to have the fields from ancestor classes through X initialized. So in this case, the fields from class Rectangle are not guaranteed to have been initialized—because the referenced object is only initialized through its Object portion—and thus may be seen to hold the value null despite being annotated as @NonNull . For this reason, even though an @Initialized reference is never null, it cannot be passed to a @NonNull reference because we must manage the fact that some of the fields of the referenced object may violate their @NonNull invariants. In our particular case here, we can see that the @NonNull fields topLeft and bottomRight are correctly initialized before calling computePerimeter . We use this fact in just a minute.

Partially initialized references originate in constructors: an object of type C is not fully initialized until its final constructor, the one defined within C, executes. If a reference to the receiver is passed to another method during construction—as it is in Rectangle(Point, Point)—then that reference is partially initialized through the most recently constructed superclass component. That is, if we have class C extends B extends A, and during the execution of the constructor for B a reference to the object being constructed is leaked, then that reference is partially initialized through A.

How can we satisfy the assurance for constructor Rectangle(Point, Point)? The most straightforward way to do so is to declare to computePerimeter() that the receiver is possible partially initialized by annotating it with an @Initialized annotation as shown below. This annotation can be added using the proposed promise in the results.

  @Initialized(through="Object", value="this")
  private void computePerimeter() {
    int width = bottomRight.getX() - topLeft.getX();
    int height = bottomRight.getY() - topLeft.getY();
    perimeter = (width + height) << 1;
  }

Above we use the value attribute of the annotation to indicate that that receiver of the method (and not the return value) is being annotated. You may notice that the value attribute is not explicit in the proposed promise in the results. When the @Initialized annotation is used on a method, the value attribute is "this" by default. We make it explicit in our listing above only for clarity. Add the @Initalized annotation to the code and reverify the project. At first glance the results seem acceptable. There is a new result node corresponding to the@Initialized annotation and all the call sites of the method are assured. Note that the actual receiver is @Initialized when the method is called from the constructor, but @NonNull when the method is called from other methods:

Unfortunately, there are also changed results for the @NonNull annotations on the two fields. This is noted by the small delta decoration on the icons. Opening up these results reveals new negative results about the field: possible dereferences of a null value.

The fields topLeft and bottomRight are not supposed to be null so how can we possibly read a null value from them? The receiver of the method computePerimeter is @Initialized(through="Object"), which means inside the method analysis must assume that the fields have not yet been initialized to a non-null value. So attempting to dereference the fields to use them as receivers for getX() and getY() can yield a null value. As null is not acceptable for a receiver, assurance creates a result here.

To verify the method computePerimeter() we need to handle the fact that the fields topLeft and bottomRight may be null. Let's try doing this by testing the fields against null and only computing the perimeter if they are not null. Make this code change and reverify.

  @Initialized(through="Object", value="this")
  private void computePerimeter() {
    Point tL = topLeft;
    Point bR = bottomRight;
    if (tL != null && bR != null) {
      int width = bR.getX() - tL.getX();
      int height = bR.getY() - tL.getY();
      perimeter = (width + height) << 1;
    }
  }

Here we first copy the value of the fields into local variables before testing against null. This is necessary because the flow analysis only tracks the values of local variables because it cannot be sure that the value of a field is not going to be modified by a concurrently executing thread of control. Flow analysis also understands comparisons against null and thus can determine that both tL and bR are non-null in the body of the if-statement. After reverifying the project the “possible dereference of a null value” negative results are gone:

Despite this apparent success at verifying the method, this approach is undesirable because it leaves the field perimeter in an unknown state when one of the corners of the rectangle is null. More importantly, it swallows the error when one of the fields is null. We could add error handling here, but what would we do? Throwing an exception is extreme because there isn't anything the caller of the method can do about the situation. The fact is that computePerimeter() must rely on the @NonNull annotations on topLeft and bottomRight.

So let's go ahead and return computePerimeter() to its original form. Change it back to look like the code below. In particular, be sure to remove the @Initialized annotation from the method.

  private void computePerimeter() {
    int width = bottomRight.getX() - topLeft.getX();
    int height = bottomRight.getY() - topLeft.getY();
    perimeter = (width + height) << 1;
  }

The best approach in this case is recognizing that the constructor Rectangle(Point, Point) has completed initializing the @NonNull fields before calling computePerimeter():

  private Rectangle(@NonNull Point topLeft, @NonNull Point bottomRight) {
    this.topLeft = topLeft;
    this.bottomRight = bottomRight;
    computePerimeter();
  }

So what we want to do is force the analysis to consider the receiver to be @NonNull when invoking computePerimeter(). We can do this using the method Cast.toNonNull(). This is a method in the SureLogic promises library that always returns it's given reference as a @NonNull reference. As a safe-guard it triggers a Java assertion failure if the given reference is actually null (and you have assertions enabled). JSure recognizes this method and treats it like a @Vouch in the results.

  private Rectangle(@NonNull Point topLeft, @NonNull Point bottomRight) {
    this.topLeft = topLeft;
    this.bottomRight = bottomRight;
    Cast.toNonNull(this).computePerimeter(); // N.B. topLeft and bottomRight are initialized
  }

After reverifying the project, the negative assurance result is gone. We also see a new vouch result corresponding to the call to Cast.toNonNull():

Now we look at the virtual @NonNull on method copyFrom(). If we expand this result we see the results shown below.

Again, we have an instance method called from a constructor using the object under construction as the receiver:

  /**
   * Copy constructor.
   */
  public Rectangle(Rectangle other) {
    copyFrom(other);
  }

As before, the obvious starting point is to annotate the receiver of copyFrom() as being a partially initialized object. This is obviously a safe thing to do because the method only writes the fields of the receiver. While we are at it, we also declare that the parameter other is @NonNull. So change your code to match that below and rescan the project.

  @Initialized(through="Object", value="this")
  public void copyFrom(@NonNull Rectangle other) {
    topLeft = other.topLeft;
    bottomRight = other.bottomRight;
    perimeter = other.perimeter;
  }

After reassuring the project, the @Initialized annotation assures, but the @NonNull annotation does not. The problem being that the formal parameter in the constructor used as the actual in the method call needs to be @NonNull as well:

Add the @NonNull annotation to the parameter other of Rectangle(Rectangle) (you can use the tool-proposed promise to do this). After reassuring the project, the new @NonNull annotations assure:

If you review the rest of the inconsistent results, you'll see that we still have a “Not definitely assigned” failure for each of the fields topLeft and bottomRight and recursive failures originating from the assignments in the method copyFrom. Again, the recursive failures originate in the fact the correctness of copy assignments depends on the fields topLeft and bottomRight being @NonNull which is not assuring due to the definite assignment errors.

As described previously, JSure requires that every @NonNull field be explicitly assigned in each constructor or in its field declaration. This is so that the Java-default value of null for references is never visible. Analysis is unable to determine that the fields topLeft and bottomRight are properly initialized in Rectangle(Rectangle) because the constructor relies on the method copyFrom() to initialize the fields. We must use a @Vouch annotation on the constructor to explicitly indicate that the fields are correctly initialized:

  @Vouch("topLeft and bottomRight are initialized by copyFrom()")
  public Rectangle(@NonNull Rectangle other) {
    copyFrom(other);
  }

Scanning the project after adding this annotation finally yields model-code consistency. This result is shown in the image below.

The “Not definitely assigned” results now display with a gray plus, indicating the that result has been explicitly made acceptable by the addition of the @Vouch annotation. We also see that the recursive dependency of the @NonNull field annotations finally assures because the rest of the inconsistencies have been resolved.

As this section illustrates, calling instance methods on the receiver from a constructor complicates the assurance of @NonNull fields by introducing references to partially initialized objects. Generally speaking, you should avoid calling methods on the object being constructed. The next two sections show how we can simplify the assurance of the classes in this example by rewriting the constructors to avoid calling methods on the under-construction object.

1.3.8.4.  Avoiding the need to cast the receiver within Rectangle(Point, Point)

In this section we improve our result by removing the need to cast the receiver within the Rectangle(Point, Point) constructor. We start with the constructor Rectangle(Point, Point) which calls the method computePerimeter(). This method is called by each method that updates the corners of the rectangle: setBottomRight(), setTopLeft(), and stretch(). The method is used to maintain the invariant that the value of the field perimeter is the geometric perimeter of the rectangle described by the two points. Because the perimeter needs to be computed in multiple places, it the authors of the class sensibly abstracted out the computePerimeter() method. Unfortunately, as we have seen calling an instance method from the constructor is bad practice. We need to refactor the class and the method to avoid this problem. Specifically, we are going to

  1. Rename the original method.

  2. Extract a new static method that computes and returns the value of the perimeter.

  3. In-line the method call in the constructor so that perimeter is explicitly set within the constructor.

Renaming the original method.  To rename the computePerimeter(), select computePerimeter in the Outline view. Then select RefactorRename…. Enter the name “updatePerimeter” in the dialog box:

This name better reflects the effects of the method. Click on OK and Eclipse renames the method and updates the method call sites.

Extracting a new method.  Next we want to extract a new method that computes and returns the perimeter value. We could do this using the Eclipse refactorings, but it would be tedious because we would first have to extract bogus local variables so that the Extract method refactoring could use them as formal parameters and as the return value. Then after extracting the method, we would have to in-line the bogus locals to get rid of them. In this case it is simpler to just edit the code by hand and update updatePerimeter() and add a new computePerimeter():

  private void updatePerimeter() {
    perimeter = computePerimeter(topLeft, bottomRight);
  }
  
  private static int computePerimeter(final Point topLeft, final Point bottomRight) {
    int width = bottomRight.getX() - topLeft.getX();
    int height = bottomRight.getY() - topLeft.getY();
    return (width + height) << 1;
  }

Note that computePerimeter() is static . This allows it to be called from a constructor without creating any problems with regard to verifying our null reference design intent.

In-lining the method call.  Finally we need to update the call to updatePerimeter() in the constructor Rectangle(Point, Point) itself. This is technically an in-lining operation because we want to unwrap updatePerimeter() to expose the assignment of the field perimeter. Using the Eclipse refactoring operation will not do exactly what we want, however, because it will perpetuate the use of Cast.toNull() and will use the fields topLeft and bottomRight as the actual arguments to computePerimeter when we want to use the formal parameters of the constructor. Better to edit the method by hand and update it to

  private Rectangle(@NonNull Point topLeft, @NonNull Point bottomRight) {
    this.topLeft = topLeft;
    this.bottomRight = bottomRight;
    this.perimeter = computePerimeter(topLeft, bottomRight);
  }

Now rescan the project. The “Cast.toNonNull()” drop no longer appears under the Vouches heading. This is as we expect because we removed the use of that method. More importantly, the model-code consistency result still holds for the project.

1.3.8.5.  Avoiding the need for a vouch on Rectangle(Rectangle)

In this section we improve our result by removing the need to vouch the Rectangle(Rectangle) constructor. Once again we do this through code and model changes in our project. Recall that the problem with the constructor Rectangle(Rectangle) is that it does not directly initialize the @NonNull fields topLeft and bottomRight. Instead it uses the method copyFrom() to do it. If we want to more cleanly assure this constructor—not use a @Vouch annotation—then we must explicitly initialize the fields in the body of the constructor. The best approach in this case is to inline the call to copyFrom() . Select the call

and choose RefactorInline…. Choose to inline only the selected location:

After refactoring, the method is

The @Vouch annotation is no longer necessary as the problematic method call has been removed. You should remove it now and then rescan the project. The project now assures completely without the explict programmer vouch.

The @Initialized annotation remains on the method copyFrom(). This is currently harmless because the method does not read from any fields of the receiver. But leaving it in place will constrain the evolution of the method. In this example, it is not clear that the method is necessary any more. In a more complex implementation the method may continue to be used. For this tutorial delete the method and rescan. Your results should appear as shown below.

We finish up by noting that we contrived this code to make several problems come up that you might encounter in your real-world Java code. The tutorial showed how to refactor code to simply the modeling required to verify null reference design intent. It is not always possible, but trying to avoid casts and vouches is desirable. In addition, partially initialized object can lead to bugs in Java code so they are undesirable. We have demonstrated the use of @TrackpartiallyInitialized to support @NonNull fields, but the annotation can be used on any class to uncover partial initiation problems in Java code.

Chapter 2. Reference

2.1. The JSure Menu

The JSure menu, see Figure 2.1, appears as an item on the Eclipse workspace main menu. This menu provides direct access to common JSure commands.

Figure 2.1. The JSure menu

The JSure menu

The commands on the JSure main menu are

  • VerifyThis command allows the user to choose which project should be assured by JSure. It is also available by pressing the icon on the Eclipse toolbar. A dialog is opened to allow the user to select which projects to analyze, as seen in Figure 2.2. This dialog remembers your prior selection and includes projects selected in the Package Explorer.

    Figure 2.2. The Verify dialog box

    The Verify dialog box

  • Add/Update Promises LibraryThis command lets the user add or update the promises library for a project. The dialog shown in Figure 2.3 is opened to allow the user to select the set of projects to update. For each selected project, this command copies the promises-version.jar into the root of the project and adds the JAR to the project's classpath.

    Figure 2.3. The Add/Update Promises Library dialog box

    The Add/Update Promises Library dialog box

  • Open Library Annotations…This command, similar to the Eclipse Java Open Type search, allows the tool user to open any type in the JSure library annotation editor. A dialog, shown in Figure 2.6, is opened to let the user to search for the type that they want to open in the library annotation editor. This command is most useful for opening types that have no annotations and, therefore, are not listed in the Library Annotation Explorer view.

    Figure 2.4. The Open Library Annotations search dialog

    The Open Library Annotations search dialog

  • Open Code Verification PerspectiveThis menu choice opens the Code Verification perspective. This perspective is useful for examining the JSure assurance results; see Section 2.2. This perspective may also be opened via the normal Eclipse menus and toolbars for perspectives.

  • Import Ant/Maven Scan…This command lets the user load a JSure scan made with the Ant task (in the future Maven). For more information on using Ant please see Section 2.5. The dialog shown in Figure 2.5 is opened to allow the user to select the scan Zip file to load into the Eclipse workspace.

    Figure 2.5. The Import JSure Ant/Maven Scan dialog box

    The Import JSure Ant/Maven Scan dialog box

  • Save Promises Library As…This command copies the promises-version.jar to the disk. A dialog, shown in Figure 2.6, is opened to let the user to specify the directory the JAR file should be placed within. This command is useful if you need, for any reason, to manually add the JSure annotation JAR file to a codebase.

    Figure 2.6. The Save Promises Library dialog box

    The Save Promises Library dialog box

  • Save Documentation As…This command copies the jsure-html-docs.zip to the disk. A dialog, shown in Figure 2.7, is opened to let the user to specify the directory the Zip file should be placed within. This command is useful if you want to open the JSure documentation in your web browser. This file contains HTML versions of all the JSure documentation also in your Eclipse help system. Many tool users prefer using a browser for JSure documentation rather than the build-in Eclipse help system (each of search, and so on).

    Figure 2.7. The Save Documentation dialog box

    The Save Documentation dialog box

  • Install Tutorial ProjectsThis command opens a dialog to allow the user to import one or more tutorial projects into their workspace and open the JSure help to the step by step tutorials. For more information please see Section 1.3.

  • Send Tip for ImprovementThis command opens a dialog to allow entry of a suggestion by the user to improve the JSure tool. For more information please see Section 2.8.

  • Send Problem ReportThis command opens a dialog to allow entry of a problem report by the user about the JSure tool. For more information please see Section 2.8.

  • Send Library Annotation ChangesThis command opens a dialog to allow you to send any changes to library annotations you have made to SureLogic. The dialog allows you to preview and edit what is being sent to SureLogic. This menu item is the best way to propose changes to the shipped set of Java standard library annotations. If you do not have an Internet connection you can print the message and fax it to SureLogic or save the message as a file and email it.

  • Manage SureLogic LicensesThis command opens the SureLogic license management dialog. This dialog allows the user to install, view, and uninstall licenses for JSure and other SureLogic tools. For more information see Section 2.7.

2.2. The Code Verification perspective

The Code Verification perspective organizes the Eclipse workbench to show views which will help you to interact with tool findings.

Each of the views shown in the screenshot above is discussed in the following sections. These views include

2.2.1. Switching to the Perspective

The Code Verification perspective can be enabled in several ways:

  • By selecting JSureOpen Code Verification Perspective.

  • By choosing to switch to the perspective when focusing verification on a project:

  • By selecting WindowOpen PerspectiveOther…, and then choosing Code Verification from the Open Perspective dialog box. Or by using any other standard Eclipse mechanism to switch perspectives, such as clicking the the perspective’s icon () in the shortcut bar.

2.2.2. The JSure Scans view

The JSure Scans view, as shown in Figure 2.8, lists the scans performed by the tool. One and only scan in this view can be checked. The checked scan is called the scan of focus. Results from the scan of focus are displayed in all the other JSure views.

Figure 2.8. The JSure Scans view

The JSure Scans view

Each row in the table represents a scan. The table displays has the following columns:

  • Time. The time the scan occurred.

  • Size. The size of the scan data on your disk.

  • Projects Examined. A comma separated list of the projects that were scanned.

  • Exclusion Specification (surelogic-tools.properties). The exclusions for source folders and packages from the surelogic-tools.properties file located at the project's root. This file is optional and its format is described in Section 2.4. Several of these files will be combined if multiple projects are scanned.

The view’s toolbar has three command icons:

  •  This button scans the disk and refreshes the list of JSure scans. This can be useful if an Ant scan was added to the JSure scan directory.

  •  This button "re-verifies" selected (not the checked) scan. This allows you to easily start a new scan on a set of projects that you have previously scanned.

  •  This button deletes the selected scans from the disk.

Figure 2.9. The JSure Scans view menu

The JSure Scans view menu

The view’s menu has three commands; see Figure 2.9. These commands match the toolbar commands described above.

Figure 2.10. The JSure Scans context menu

The JSure Scans context menu

The view’s context menu has three commands; see Figure 2.10:

  • Select to View ResultsSelecting this menu item causes the selected scan to be checked and become the scan of focus. This menu choice is only enabled when a single scan is selected and it is not the scan of focus.

  • Re-VerifyThis button "re-verifies" selected (not the checked) scan. This allows you to easily start a new scan on a set of projects that you have previously scanned. This menu choice is only enabled when a single scan is selected.

  • DeleteSelecting this menu item deletes the selected scans from the disk.

2.2.3. The Modeling Problems view

The Modeling Problems view, as shown in Figure 2.11, shows any annotations that are not well-formed. This means that they have syntax errors or other problems such as referencing models that are not defined or encapsulation/visibility issues.

Figure 2.11. The Modeling Problems view

The Modeling Problems view

The background of the Modeling Problems view changes to yellow if the selected scan has any modeling problems. This highlights the view to the tool user. The background is changed back to normal when no modeling problems exist in the selected scan.

Double-clicking on a modeling problem will open the Java editor and the JSure Historical Source view to the problem annotation. This same action can be accomplished by selecting Open from the view context menu. If the problem is in a binary the XML Library Annotation Editor can be opened by selecting Open Library Annotation Editor from the view context menu. This choice is only available for modeling problems about binaries.

If the icon for a reported modeling problem is (note the + to the upper-right) then JSure "thinks" it can resolve the modeling problem with an automatic edit. Select one or more modeling problems and choose Annotate Code To Fix... from the view's context menu (or press on the view's toolbar) and the tool will automatically fix the modeling problem as shown in Figure 2.12. The edit is previewed before it is made to the code. Carefully examine the proposed edit to your code to ensure it reflects your design.

Figure 2.12. The Modeling Problems view context menu

The Modeling Problems view context menu

Selecting a problem and choosing Copy from the view's context menu will copy the text of the problem to the clipboard so that it can be pasted into an email or any other program.

The view’s toolbar has six command icons:

  •  This button collapses all the nodes in the Java declaration tree.

  •  This button automatically edits the code to try and resolve the selected modeling problems. The edit is previewed before it is made to the code. Not all modeling problems have automatic fixes. If the problem's icon is it has an automatic fix. If the problem's icon is it must be fixed manually.

  •  Toggling this button controls whether or not differences are highlighted in the view. If a problem has changed its background is painted in white. In addition, a trail of images appear from the root of the tree to any problem that has changed.

  •  Toggling this button controls whether or not unchanged problems are displayed in this view. When this button is selected only problems with differences are displayed in the view. By default this is not selected.

  •  Toggling this button controls whether or not problems not about Java source code are displayed in this view. When this button is selected only problems about source code are displayed. By default this is not selected.

  •  This button opens the Uninteresting Package Filtering preference page. The filters defined by this preference filter modeling problems from this view. This can be used to filter out problems that you do not care to have reported, for example, about a library that you include in your codebase. For more information about this preference page see Section 2.3.3.

Figure 2.13. The Modeling Problems view menu

The Modeling Problems view menu

The view’s menu has six commands; see Figure 2.9:

  • Collapse AllSelecting this menu item collapses all the nodes in the Java declaration tree.

  • Annotate Code To Fix... Selecting this menu item automatically edits the code to try and resolve the selected modeling problem. The edit is previewed before it is made to the code. Not all modeling problems have automatic fixes. If the problem's icon is it has an automatic fix. If the problem's icon is it must be fixed manually.

  • Highlight DifferencesToggling this menu item controls whether or not differences are highlighted in the view. If a problem has changed its background is painted in white. In addition, a trail of images appear from the root of the tree to any problem that has changed.

  • Show Only DifferencesToggling this menu item controls whether or not unchanged problems are displayed in this view. When this menu item is checked only problems with differences are displayed in the view. By default this is not selected.

  • Show Only From SourceToggling this button controls whether or not problems not about Java source code are displayed in this view. When this button is selected only problems about source code are displayed. By default this is not selected.

  • Modeling Problem Filtering... Selecting this menu item opens the Uninteresting Package Filtering preference page. The filters defined by this preference filter modeling problems from this view. This can be used to filter out problems that you do not care to have reported, for example, about a library that you include in your codebase. For more information about this preference page see Section 2.3.3.

2.2.4. The Verification Status view

The Verification Status view displays the JSure assurance results in a tree form; see Figure 2.14. The results are grouped by category, for example Effects, Concurrency, Uniqueness, and Thread effects. There is also a special category for warnings and informational results Suggestions and warnings. The iconography used in this view is summarized in Figure 1.5.

Figure 2.14. The Verification Status view

The Verification Status view

Clicking on a result in the Verification Status view highlights the code associated with that result in the Java editor and the JSure Historical Source view. This view also notes the differences between the current scan and the previous scan (in its far right column).

The view’s toolbar has seven command icons:

  •  This button collapses all the nodes in the result trees.

  •  This button displays a quick reference card to the user about what the iconography used in the Verification Status view means.

  •  This button gives an indication in the Verification Status view that modeling problems exist in the project. It is intended to be helpful when the user is using non-JSure perspectives, such as the Java perspective, where it can be difficult to know if any modeling problems exist in scanned projects if only this view is opened. The icon is disabled if no modeling problems exist—as shown in the screenshot above. It is bright yellow when modeling problems do exist‐as shown at the start of this paragraph.

  •  Toggling this on sorts leaf nodes of the tree by project name, package name, type name, and line number.

  •  Toggling this button on sorts leaf nodes of the tree alphabetically by their message.

  •  Toggling this button controls whether or not differences are highlighted in the view. If a result has changed its background is painted in light yellow (as shown in the image above). In addition, a trail of images appear from the root of the tree to any result that has changed.

  •  Toggling this button controls whether or not unchanged results are displayed in this view. When this button is selected only results with differences are displayed in the view. By default this is not selected.

  •  Toggling this button controls whether or not information and warning hints are displayed in the view.

Figure 2.15. The Verification Status view menu

The Verification Status view menu

The view’s menu has six commands; see Figure 2.15:

  • Collapse AllSelecting this menu item collapses all the nodes in the result trees.

  • Show Iconography Quick Reference CardSelecting this menu item displays a quick reference card to the user about what the iconography used in the Verification Status view means.

  • Sort Contents By Java LocationSelecting this menu item sorts leaf nodes of the tree by project name, package name, type name, and line number.

  • Sort Contents AlphabeticallySelecting this menu item sorts leaf nodes of the tree alphabetically by their message.

  • Highlight DifferencesToggling this menu item controls whether or not differences are highlighted in the view. If a result has changed its background is painted in light yellow (as shown in the image above). In addition, a trail of images appear from the root of the tree to any result that has changed.

  • Show Only DifferencesToggling this menu item controls whether or not unchanged results are displayed in this view. When this menu item is checked only results with differences are displayed in the view. By default this is not selected.

  • Show Information/Warning HintsToggling this menu item controls whether or not information and warning hints are displayed in the view.

2.2.5. The Verification Explorer view

The Verification Explorer view, as shown in Figure 2.16, shows all annotations that the current scan found in the source code or in XML about libraries and frameworks. It can also show analysis results. The major difference between this view and the Verification Status view is that this view shows results in the context of the code, while the Verification Status displays results by their verification proof context. The view contents change when the selected scan changes. This view is useful to determine if an annotation existed and was recognized by the tool during a particular scan. The iconography used in this view is summarized in Figure 1.5.

Figure 2.16. The Verification Explorer view

The Verification Explorer view

The view’s toolbar has nine command icons:

  •  This button collapses all the nodes in the Java declaration tree.

  •  This button displays a quick reference card to the user about what the iconography used in the Verification Explorer view means.

  •  This button gives an indication in the Verification Explorer view that modeling problems exist in the project. It is intended to be helpful when the user is using non-JSure perspectives, such as the Java perspective, where it can be difficult to know if any modeling problems exist in scanned projects if only this view is opened. The icon is disabled if no modeling problems exist—as shown in the screenshot above. It is bright yellow when modeling problems do exist‐as shown at the start of this paragraph.

  •  Toggling this button controls whether or not differences are highlighted in the view. If a result has changed its background is painted in light yellow (as shown in the image above). If a result is obsolete its background is painted in light red. In addition, a trail of images appear from the root of the tree to any result that has changed.

  •  Toggling this button controls whether or not unchanged results are displayed in this view. When this button is selected only results with differences are displayed in the view. By default this is not selected.

  •  Toggling this button controls whether or not obsolete results only in the prior scan are displayed. When this button is selected obsolete results from the last scan are displayed in the view. By default this is not selected.

  •  Toggling this button controls whether or not results not directly or indirectly derived from Java source code are displayed in this view. When this button is selected only results directly or indirectly related to source code are displayed. By default this is selected.

  •  Toggling this button controls whether or not analysis results are displayed in this view. When this button is selected analysis results, as well as annotations, are displayed. By default this is not selected.

  •  Toggling this button controls whether or not information and warning hints are displayed in the view.

Figure 2.17. The Verification Explorer view menu

The Verification Explorer view menu

The view’s menu has eight commands; see Figure 2.17:

  • Collapse AllSelecting this menu item collapses all the nodes in the Java declaration tree.

  • Show Iconography Quick Reference CardSelecting this menu item displays a quick reference card to the user about what the iconography used in the Verification Explorer view means.

  • Highlight DifferencesToggling this menu item controls whether or not differences are highlighted in the view. If a result has changed its background is painted in light yellow (as shown in the image above). If a result is obsolete its background is painted in light red. In addition, a trail of images appear from the root of the tree to any result that has changed.

  • Show Only DifferencesToggling this menu item controls whether or not unchanged results are displayed in this view. When this menu item is checked only results with differences are displayed in the view. By default this is not selected.

  • Show Obsolete ResultsToggling this menu item controls whether or not obsolete results only in the prior scan are displayed. When this menu item is checked obsolete results from the last scan are displayed in the view. By default this is not selected.

  • Show Only Results Derived From SourceToggling this menu item controls whether or not results not directly or indirectly derived from Java source code are displayed in this view. When this menu item is checked only results directly or indirectly related to source code are displayed. By default this is selected.

  • Show Analysis ResultsToggling this menu item controls whether or not analysis results are displayed in this view. When this menu item is checked analysis results, as well as annotations, are displayed. By default this is not selected.

  • Show Information/Warning HintsToggling this menu item controls whether or not information and warning hints are displayed in the view.

2.2.6. The Analysis-Enabled Metrics view

The Analysis-Enabled Metrics view, as shown in Figure 2.18, shows metrics collected during each scan of a codebase. These metrics can help answer questions about how much has been done to the codebase, how large it is, the scan performance, and so on.

Most tabs are interactive and show aggregate, scan-level, information as well as detailed counts on individual files. In particular, a threshold slider allows metric values above or below a threshold to be highlighted in the view. Only rows with data are highlighted—summary rows are not, however, a trail of decorators to the lower left of the row's image leads to highlighted rows in any tree-table displayed by this view.

Figure 2.18. The Analysis-Enabled Metrics view

The Analysis-Enabled Metrics view

The view’s toolbar has three command icons:

  •  This button collapses all the nodes in the metric tab being displayed.

  •  Toggling this button controls whether or not the nodes in the metric tab being shown are sorted in alphabetical order. When it is not pressed in tabs are sorted by the magnitude of the metric being displayed in the tab.

  •  Toggling this button controls whether or not nodes in the metric tab being shown are filtered by a threshold. Typically, nodes are highlighted if they exceed the metric threshold, but this toggle allows only those that exceed the threshold to be shown.

Figure 2.19. The Analysis-Enabled Metrics view menu

The Analysis-Enabled Metrics view menu

The view’s menu has three commands; see Figure 2.19:

  • Collapse AllSelecting this menu item collapses all the nodes in the Java declaration tree.

  • Sort Contents AlphabeticallyToggling this menu item controls whether or not the nodes in the metric tab being shown are sorted in alphabetical order. When it is unchecked tabs are sorted by the magnitude of the metric being displayed in the tab.

  • Filter By Metric ThresholdToggling this menu item controls whether or not nodes in the metric tab being shown are filtered by a threshold. Typically, nodes are highlighted if they exceed the metric threshold, but this toggle allows only those that exceed the threshold to be shown.

2.2.7. The Proposed Annotation view

The Proposed Annotation view, as shown in Figure 2.20, shows any annotations that have been proposed by the analysis for inclusion in the program's source code. The proposed annotations are inferred from other annotations in the code.

Figure 2.20. The Proposed Annotation view

The Proposed Annotation view

To add a proposed annotation to the code select one or more proposals in the view and select Annotate Code… as shown in Figure 2.21. The edit is previewed before it is made to the code. You can also select one or more Java declaration elements, including projects, to include all proposals within that declaration element. Proposals on binary code (the standard library, JAR files, or class files) do not (yet) edit XML files, however, in some cases @Assume annotations about binaries will be included as part of an edit to your source code.

Figure 2.21. The Proposed Annotation view context menu adding two proposals to the code

The Proposed Annotation view context menu adding two proposals to the code

The view’s toolbar has six command icons:

  •  This button collapses all the nodes in the Java declaration tree.

  •  This button automatically annotates all the selected proposals into the code. The edit is previewed before it is made to the code.

  •  Toggling this button controls whether or not differences are highlighted in the view. If a proposal has changed its background is painted in light yellow. In addition, a trail of images appear from the root of the tree to any proposal that has changed.

  •  Toggling this button controls whether or not unchanged proposals are displayed in this view. When this button is selected only proposals with differences are displayed in the view. By default this is not selected.

  •  Toggling this button controls whether or not proposals not for Java source code are displayed in this view. When this button is selected only proposals to source code are displayed. By default this is not selected.

  •  Toggling this button filters the proposals shown in this view. When pressed the view only displays proposals inferred from other annotations or proposals that resolve a modeling problem. For example, proposals for @RegionEffects annotations from unannotated code are filtered out. When unpressed all proposals from the scan are shown in the view.

Figure 2.22. The Proposed Annotation view menu

The Proposed Annotation view menu

The view’s menu has six commands; see Figure 2.22:

  • Collapse AllSelecting this menu item collapses all the nodes in the Java declaration tree.

  • Annotate Code... Selecting this menu item automatically annotates all the selected proposals into the code. The edit is previewed before it is made to the code.

  • Highlight DifferencesToggling this menu item controls whether or not differences are highlighted in the view. If a proposal has changed its background is painted in light yellow. In addition, a trail of images appear from the root of the tree to any proposal that has changed.

  • Show Only DifferencesToggling this menu item controls whether or not unchanged proposals are displayed in this view. When this menu item is checked only proposals with differences are displayed in the view. By default this is not selected.

  • Show Only Proposals To SourceToggling this button controls whether or not proposals not for Java source code are displayed in this view. When this button is selected only proposals to source code are displayed. By default this is not selected.

  • Show Only Proposals Inferred From Other PromisesToggling this menu item filters the proposals shown in this view. When pressed the view only displays proposals inferred from other annotations or proposals that resolve a modeling problem. For example, proposals for @RegionEffects annotations from unannotated code are filtered out. When unpressed all proposals from the scan are shown in the view.

2.2.8. The Library Annotation Explorer view

The Library Annotation Explorer view, as shown in Figure 2.23, shows any annotations that have been made in an XML file about a binary library—typically represented as JAR files in Java.

Figure 2.23. The Library Annotation Explorer view

The Library Annotation Explorer view

The view uses the '>' symbol (similar to source code control systems in Eclipse) to track user changes/additions to the standard annotations that ship with JSure from SureLogic. It is possible to only show user modified annotations by pressing the Show only user-added/modified library annotations toolbar button: . The view with this filter pressed is shown in Figure 2.24.

Figure 2.24. The Library Annotation Explorer view showing only user-added/modified library annotations

The Library Annotation Explorer view showing only user-added/modified library annotations

Clicking on a type or an annotation in this view brings up the XML library annotation editor (described below). Any changes to library annotations are made in this editor—the Library Annotation Explorer view does not allow the user to perform edits.

JSure tracks user library annotation differences across a series of tool releases and manage updates to the standard annotations shipped with each tool release. Users are notified if any of their annotations conflict with the standard library annotations. Warning symbols will appear in the Library Annotation Explorer view after a tool update if conflicts exist. Each warning can then be examined and fixed by the tool user.

The view’s toolbar has three command icons:

  •  This button collapses all the nodes in the Java declaration tree.

  •  Toggling this button controls if the view is filtered to shown only types that the user has added annotations to or modified baseline annotations. Baseline or standard annotations are shipped with JSure from SureLogic. JSure explicitly tracks changes to the baseline annotations.

  •  Selecting this button opens a search dialog, shown in Figure 2.6, to let the user search for the type that they want to open in the library annotation editor. This command is most useful for opening types that have no annotations and, therefore, are not listed in the Library Annotation Explorer view. This menu item is also on the JSure main menu.

Figure 2.25. The Library Annotation Explorer view menu

The Library Annotation Explorer view menu

The view’s menu has three commands; see Figure 2.25:

  • Collapse AllSelecting this menu item collapses all the nodes in the Java declaration tree.

  • Show Only User-Added/Modified Library AnnotationsToggling this menu item controls if the view is filtered to shown only types that the user has added annotations to or modified baseline annotations. Baseline or standard annotations are shipped with JSure from SureLogic. JSure explicitly tracks changes to the baseline annotations.

  • Open Library Annotations... Selecting this menu item opens a search dialog, shown in Figure 2.6, to let the user search for the type that they want to open in the library annotation editor. This command is most useful for opening types that have no annotations and, therefore, are not listed in the Library Annotation Explorer view. This menu item is also on the JSure main menu.

2.2.9. The XML Library Annotation editor

The XML Library Annotation editor, as shown in Figure 2.26, allows the tool user to edit annotations about a binary library—typically represented as JAR files in Java.

Figure 2.26. The XML Library Annotation editor showing the annotations on java.lang.Object

The XML Library Annotation editor showing the annotations on java.lang.Object

The editor contains three tabs: Editor, Baseline, and Diffs. Each of these tab is described below.

  • Editor — The Editor tab shows a tree of the declarations in the Java type. The user can select an element and right-click to add an annotation. The two other tabs do not allow editing (in this release—this may change in a future release). When annotations are added to an element the proper XML is automatically created by the editor (this is complex due to the "diff" approach used by JSure for library annotations as discussed below). The Baseline tab shows the XML file about this type that shipped with JSure from Surelogic. The Diffs tab shows any user changes to the annotations about this type.

    The user must type in portions of many annotations. If the syntax is obviously wrong the editor with make the text that the user typed red to highlight the problem. Edits can be saved, however, it is likely that saving "red" annotations will result in modeling errors being reported when the next JSure scan is run.

    To add an annotation bring up the context menu on any Java declaration and select Add Annotation.... Note that if you want to add an annotation to a method or constructor parameter you must expand the tree and select the parameter (a sub-item of the method or constructor).

    This will bring up a dialog, shown below, to allow you to select the annotation you want add to the declaration.

    To edit the attributes on an annotation bring up the context menu and select Edit Annotation... or double-click on the annotation. This will bring up a dialog that allows you to edit all attributes of the annotation. This dialog for a @Unique annotation is shown below

    A useful context menu item in the editor is Revert All Changes. This allows you to quickly undo any changes you have made to the standard baseline annotations that shipped with JSure.

    It is possible to copy and paste annotations from one type to another. You can copy a single annotation, all annotations on a declaration, or all annotations on all declarations within a type. The paste operation will not change an existing annotation, therefore it is best to paste onto unannotated declarations. This feature is useful for copying a set of annotation from a parent type to one of its subtypes.

    By default, unannotated methods in the editor are marked with a small red-dot. This is helpful to find a method that might have been skipped by a copy/paste or is new in a library release. This marking can be turned off by unchecking Mark Unannotated Methods in the context menu.

    Two useful context menu items in the editor are Open and Open Type Hierarchy which open the type in the Eclipse Java editor or the Eclipse Java Type Hierarchy view, respectively. These can help examine the code you are annotating as well as its parent and child types.

  • Baseline — The Baseline tab displays the XML that represents the standard library annotations that shipped with JSure. This tab does not allow editing (in this release—this may change in a future release).

  • Diffs — The Diffs tab displays the XML that represents the user's edits to the standard library annotations that shipped with JSure. This tab does not allow editing (in this release—this may change in a future release).

2.2.10. The JSure Quick Search view

The JSure Quick Search view, as shown in Figure 2.27, shows tool results to the tool user in a flexible, query-oriented, manner.

Figure 2.27. The JSure Quick Search view

The JSure Quick Search view

The JSure Quick Search view allows you to query the scan results in an ad hoc manner. You can setup a series of filters on the results to focus on the particular scan results that are of immediate interest. Selecting a result highlights that result in the Verification Status view. Clicking on a result in the JSure Quick Search view highlights the code associated with that result in the Java editor and the JSure Historical Source.

FilterSemantics
Analysis ResultAllows you to filter the results by the type of analysis result reported by the tool's verifying analyses. An analysis result is a finding reported by one of the JSure tool's verifying analyses. These results form the basis used to prove that an annotation is consistent, i.e., a verification judgment about a promise. This filter could be used to quickly find all inconsistent analysis results so that you can work to eliminate them.
AnnotationAllows you to filter the results by annotation. This filter could be used to quickly find all @RegionLock annotations in your code.
Java PackageAllows you to filter the results to a particular set of Java packages.
Java TypeAllows you to filter the results to a particular set of Java types.
ProjectAllows you to filter the results to a particular set of Eclipse projects.
Used By ProofAllows you to filter the results to those used in a verification proof or those not used in a verification proof. Many proofs have conjunction or OR choices that are made. This filter allows you to easily exclude those results not choosen.
Verification JudgmentAllows you to filter the results by the verification judgment on an annotation. This filter could be used to find all consistent promises or find promises with a "red-dot" (contingent verification judgments).

The JSure Quick Search view is very flexible and allows you to chain many filters together before you Show a list of results. You can also save queries that you find useful via the toolbar at the bottom of the view. As you construct a chain of many filters you may dismiss some of them by pressing the in the upper-right-hand corner of the filter box. For example, in the screenshot above, the is next to where the tool lists the text 2,094 Results in the Project filter.

The view’s toolbar has three command icons at the bottom:

  • Open SearchThis button opens a dialog that lists all the saved searches. The user can select a search and it is loaded into the JSure Quick Search view. Note that the links to the right of the toolbar list as many searches as can fit. This toolbar ensures that a long list of searches can be saved.

  • Save Search AsThis button brings up a dialog that lets the user name the current search. The search currently being shown in the JSure Quick Search view is saved under the given name.

  • Delete SearchThis button brings up a dialog that lists all saved searches. The tool user is allowed to select one or more saved searches to delete.

2.2.11. The JSure Historical Source view

The JSure Historical Source view, as shown in Figure 2.28, shows what the code looked like at the time that the scan was performed.

Figure 2.28. The JSure Historical Source view

The JSure Historical Source view

When a JSure scan is run all the source code is saved to that it can be shown to the user in this view. This helps the user understand if their code has changed since the JSure scan was performed. This new view is shown, in the Code Verification perspective, to the right of the Java editor at the bottom of the perspective.

2.3. JSure Preferences

JSure adds four panes to the Eclipse Preferences window:

  • JSure

  • JSureFlashlight Generated Lock Models

  • JSureUninteresting Package Filtering

  • JSureVerifying Analysis Selection

To open the Eclipse preferences select Window | Preferences... from the Eclipse main menu. JSure should be visible in the outline on the left of the dialog that appears. If you type JSure in the text box to the upper-left of the dialog then the outline will be filtered to only shown the JSure preference pages.

2.3.1. JSure

Figure 2.29. The JSure preferences pane

The JSure preferences pane

The JSure pane, see Figure 2.29, allows you to control the tool's appearance and operation.

The Data directory shows where the tool stores scans. This location is relative to your workspace and cannot be changed.

The XML library annotation "diffs" directory shows where the changes and additions made to the standard library annotations are stored. This location can be changed, for example, to be placed under version control and shared by all members of a programming team. If this location is changed, Eclipse should be restarted. In addition, it is not recommended to have any library annotation editors opened because data could be lost. Files are not copied from the old location to the new location. Therefore, a manual copy of files is required if the old location had data that you want to continue to use.

It has five options under the Appearance heading:

  • Show 'balloon' notifications for scan start and completionIf selected, pop-up notifications (also called balloon notifications) will be displayed when a JSure scan is started and when it is competed.

  • Prompt to change to the Code Verification perspective on project focusIf selected, whenever a project is selected to receive the JSure focus, you will be prompted to change to the Code Verification perspective if it is not already the active perspective.

  • If no prompt, automatically change to the Code Verification perspectiveIf selected, and JSure is not set to prompt for a perspective change, JSure automatically changes to the Code Verification perspective when a project receives the JSure focus.

  • Allow the user to select the set of projects to scan even when projects are selected (in the Package Explorer)If this is checked then the project selection dialog is always shown when a scan is started. If it is not checked it is only displayed if no projects are selected in the Package Explorer view.

  • Allow the user to select the set of projects to update the promises library even when projects are selectedIf this is checked then the project selection dialog is always shown when Add/Update Promises Library in Project is selected in the JSure menu. If it is not checked it is only displayed if no projects are selected in the Package Explorer view.

  • Always save editors before verifyingIf this is checked then any edits are automatically saved. It it is not checked the user is prompted to decided if they want to save edits before the scan is started.

  • Tree views should save and restore expansion and selection (may be slow for larger scans)If this is checked then the expansion and selection state of tree viewers is saved and restored on Eclipse exit and startup and when the scan is changed. Unchecking this may speed scan load performance. Note that expansion and selection restoration of a view will aromatically timeout after roughly 3 seconds, so this preference is rarely needs to be unchecked.

It has five options under the Verifying Scan Settings heading:

  • Number of threads the analysis is allowed to usePortions of the JSure analysis are able to use multiple threads to increase performance of the analysis. This setting allows the user to control the number of threads used by the JSure analysis. The default for this setting is the number of cores detected on the user's computer.

  • Maximum VM memory allowed for scansSets the maximum machine memory the external VM started for a JSure scan is allowed to use. In some cases, for very large codebases, the default value may need to be raised.

  • Warn when analysis execution time exceedsReports a warning in the Verification Status view when the time to analyze a method or constructor exceeds the value set in this preference.

  • Enable timeout of analysis executionEnables timeouts (stopping) of an analysis that is taking too long. The time limit is defined by the value of Timeout when analysis execution time exceeds.

  • Timeout when analysis execution time exceedsSets a time limit for analysis of a method or constructor. For this time to stop the analysis Enable timeout of analysis execution must be checked.

  • Compression may be used to reduce output size (may slow scan execution)To save space on your disk, JSure compresses the snapshot of the verification proof results output at the end of each scan. This is enabled by default and should really not be changed unless suggested by SureLogic technical support. Not checking this preference can result in enormous scan directories that take long periods of time to load, the only benefit being only a small improvement in scan execution time.

  • Analysis may propose promises not based on existing models (may slow scan execution and use significant memory)The verifying analysis can propose promises about all code in the system—regardless if any annotations exist in your code. This feature may be useful to some users, but it can slow scan execution and cause the Eclipse instance that is loading up the results of a scan to consume significant memory for very large code bases. Today, turning on this feature will produce @RegionEffects proposals on every method and constructor in your codebase.

  • Load entire classpath into memory (used for testing library annotation consistency)To save memory and time, JSure only loads classes from JAR files into memory during a scan if they are referenced, directly or indirectly, by code in the project. This selection directs JSure to load the entire project classpath into memory. This is not recommended for normal tool use, however, it is very helpful when annotating binary libraries with the Library Annotation Explorer and editor. This is because it can help check that all subtypes of an annotated binary class are properly annotated.

What can be done about a method that takes a long time to analyze? If possible, reduce the number of local variables in the method. This will speed analysis. Typically methods that are very large can be broken up into smaller methods or refactored to call a series of new methods extracted from the larger method. Doing this will also speed analysis.

The pane also has a Manage SureLogic Licenses button that brings up the dialog box for installing and removing licenses; see Section 2.7.

2.3.2. Flashlight Generated Lock Models

Figure 2.30. The Flashlight Generated Lock Models preferences pane

The Flashlight Generated Lock Models preferences pane

The Model Naming pane, see Figure 2.30, controls inferred models from the Surelogic Flashlight tool.

2.3.3. Uninteresting Package Filtering

Figure 2.31. The Uninteresting Package Filtering preferences pane

The Uninteresting Package Filtering preferences pane

The Uninteresting Package Filtering pane, see Figure 2.31, controls what modeling problems and proposed promises are not shown to the tool user by defining a set of filters on the package and type names a result is within.

If any of the filters match the resource that the modeling problem or proposed promise is within, then the problem or proposal. is not shown. The filters are defined using Java regular expressions.

This preference pane has a set of reasonable defaults that cover the Java standard library. Filters can be added to avoid reports about code that you are not interested in, for example, modeling problems about a library included in your code that you do not maintain.

2.3.4. Verifying Analysis Selection

Figure 2.32. The Verifying Analysis Selection preferences pane

The Verifying Analysis Selection preferences pane

The Verifying Analysis Selection pane allows you to choose which assurance analyses are actually executed by JSure. Most of the time you do not need to change these settings unless directed by SureLogic technical support.

2.4. SureLogic tool properties file

It is possible to exclude particular Eclipse source folders or Java packages from a scan. This feature can be useful to exclude test or obsolete code from scans. It is also possible to treat particular Eclipse source folders or Java packages as if they were a library (a Jar).

To do this you create a surelogic-tools.properties file at the root of an Eclipse Java project. Four properties are recognized

  • scan.exclude.source.folderThis property excludes one or more source folders of a project from scans. The source folder is referenced by its name relative to the root of the project. More than one source folder can be specified using a comma separated list.

  • scan.exclude.source.packageThis property excludes the contents of one or more packages from scans. Packages may be listed explicitly using a comma separated list. A * can be used within a package name as a wildcard to match several packages.

  • scan.source.folder.as.bytecodeThis property treats one or more source folders of a project as if all its code was binary, or bytecode (such as if it were within Jar). The source folder is referenced by its name relative to the root of the project. More than one source folder can be specified using a comma separated list.

  • scan.source.package.as.bytecodeThis property treats the contents of one or more packages as if all its code was binary, or bytecode (such as if it were within Jar). Packages may be listed explicitly using a comma separated list. A * can be used within a package name as a wildcard to match several packages.

The example shown in Figure 2.33 excludes the test source folder of the timingframework-core project.

Figure 2.33.  Use of the surelogic-tools.properties to exclude the test source folder of the timingframework-core project

Use of the surelogic-tools.properties to exclude the test source folder of the timingframework-core project

The example shown in Figure 2.34 excludes any package in the timingframework-swing project that's name starts with org.jdesktop.swing.animation.demos. For this example that matches two packages: org.jdesktop.swing.animation.demos and org.jdesktop.swing.animation.demos.splineeditor.

Figure 2.34.  Use of the surelogic-tools.properties to exclude packages from the timingframework-swing project

Use of the surelogic-tools.properties to exclude packages from the timingframework-swing project

Some further examples of excluding code within an Eclipse Java project from a scan are shown in the table below.

ExampleDescription
scan.exclude.source.folder=test Excludes a source folder named test located at the root of the project folder from scans.
scan.exclude.source.folder=test1,test2,test3 Excludes three source folders from scans: test1, test2, andtest3.
scan.exclude.source.package=com.surelogic.tests,com.surelogic.demos Excludes two packages from scans: com.surelogic.tests and com.surelogic.demos.
scan.exclude.source.package=*test* Excludes any package from scans that contains test as part of its name.
scan.exclude.source.package=*.test.* Excludes any package from scans that is a sub-package of a test package, but not the elements of the test package itself.
scan.exclude.source.package=*test*,com.surelogic.demos Excludes any package from scans that contains test as part of its name as well as the com.surelogic.demos package.

2.5. Using Ant

The JSure Ant task can scan a project and produce JSure results. It is, by design intended to be similar to the javac Ant task. This task results in a Zip file that can be loaded into Eclipse using the Import Ant/Maven Scan... on the JSure menu. Once loaded into Eclipse the JSure scan results can be examined just like any other scan.

The Ant tasks are not included within the Eclipse plugin (to save space) but can be downloaded here on the SureLogic website.

The special attributes are given below, note that other javac task attributes work as well. The idea is for you to copy or "clone" your javac task and modify it just a bit (with the attributes below) to be a JSure scan task.

Note that you must run this task in a Java 7 VM (it can analyze any code).

2.5.1. jsure-scan task

This task scans code and produces a scan file on the disk. This task is, for convenience, very similar to the javac task. The new attributes are:

AttributeDescriptionRequired
projectname This attribute sets the name of your project when the scan is loaded into Eclipse. This value is also used to name the resulting Zip file. projectname="JSureTutorial_BoundedFIFO" Yes
jsureanthome This attribute sets set this to the location of the bits for the JSure Ant task (where you unzipped them). Typically you copy the pattern illustrated in the Ant script below and set this path as the property "jsure.ant.home" so that it can be used to specify the task classpath as well as the value of this attribute. e.g.,<property name="jsure.ant.home" location="C:\\Users\\Tim\\jsure-ant" /> ... jsureanthome="${jsure.ant.home}" Yes
jsurescandir This attribute sets a directory to create the scan Zip file within. If it is not set then output is written to the current directory. This may be useful if you want to gather results in a particular location on your disk. jsurescandir="C:\\Users\\Tim\\myscans" No, output defaults to the current directory.
surelogictoolspropertiesfile This attribute sets the location of a surelogic-tools.properties file to be read to control the scan. This file can control aspects of the JSure scan (please see Section 2.4). If this attribute is not set the tool looks for a surelogic-tools.properties file in the current directory and uses that if it is found. surelogictoolspropertiesfile="C:\\Users\\Tim\\surelogic-tools.properties" No, if not set the tool looks for a surelogic-tools.properties file in the current directory (a useful default if you place the Ant script and the properties file at the root of a Java project). If found then that file is used, if not then no properties are used.

For the JSureTutorial_BoundedFIFO project create a build.xml at the project root:

<?xml version="1.0" encoding="UTF-8"?>
<project name="JSureTutorial_BoundedFIFO" default="scan" basedir=".">

  <!-- (CHANGE) path to the unzipped the JSure Ant task -->
  <property name="jsure.ant.home" location="C:\\Users\\Tim\\jsure-ant" />

  <!-- (COPY) JSure Ant task setup stuff -->
  <path id="jsure-ant.classpath">
    <dirset  dir="${jsure.ant.home}" includes="lib/com.surelogic.*" />
    <fileset dir="${jsure.ant.home}" includes="lib/**/*.jar" />
  </path>
  <taskdef name="jsure-scan" classname="com.surelogic.jsure.ant.JSureScan">
    <classpath refid="jsure-ant.classpath" />
  </taskdef>

  <path id="tf.classpath">
    <fileset dir="${basedir}" includes="**/*.jar" />
  </path>

  <target name="scan">
    <javac srcdir="${basedir}/src"
           destdir="${basedir}/bin"
           source="1.7"
           includeantruntime="false">
       <classpath refid="tf.classpath" />
    </javac>

    <jsure-scan srcdir="${basedir}/src"
                source="1.7"
                includeantruntime="false"
                jsureanthome="${jsure.ant.home}"
                projectname="JSureTutorial_BoundedFIFO">
       <classpath refid="tf.classpath" />
    </jsure-scan>
  </target>
</project>

To run a scan open a prompt to this directory and run "ant" or run as Ant task in your Eclipse. The output of the above Ant script on the JSureTutorial_BoundedFIFO project will look like

Buildfile: C:\Users\Tim\Source\eclipse-work\meta-work\JSureTutorial_BoundedFIFO\build.xml
scan:
[jsure-scan] Project to scan w/JSure = JSureTutorial_BoundedFIFO
[jsure-scan] Scan output directory   = .
[jsure-scan] Scan JSureTutorial_Bounde-2015.05.18-at-12.37.55.231 examining 3 Java files
BUILD SUCCESSFUL
Total time: 8 seconds

Next you would load the JSureTutorial_Bounde-2015.05.18-at-12.37.55.231.jsure-scan.zip file into your Eclipse by choosing the JSureImport Ant/Maven Scan... from the Eclipse main menu. The file is located at the root of the JSureTutorial_BoundedFIFO project on your disk (where the script was located).

2.6. Using Maven

A Maven task for JSure is still under development. A workaround is to use Ant within Maven as discussed here and here.

2.7. License management

JSure is commercial software and a license is required to use it. Licenses are obtained from SureLogic and expire after some period of time. Lack of a license will prohibit you from scanning code with JSure. Selecting Manage SureLogic Licenses from the JSure menu brings up the license management form as seen in Figure 2.35. For JSure to operate properly either a JSure or All Tools license must be installed.

Figure 2.35. The SureLogic license management dialog

The SureLogic license management dialog

By default license installation requires internet access. SureLogic can, in special cases, provide licenses that do not require internet access. Further use of the product does not require internet access. If a manual uninstall is done, before license expiration, internet access is also required. SureLogic tracks the number of times a particular license is installed and uninstalled. We stress that JSure does not, unlike other plug-ins such as MyEclipse, “talk-back” to SureLogic each time Eclipse is started.

The installed license expires after a period of time (clearly visible to the user) and a new license has to be installed to continue to use JSure.

Licenses can be installed more than once. Thus, one license can be used for all of an organization or SureLogic can issue one per location or one per organizational entity.

If the JSure Eclipse plug-in does not have a valid license it will not affect the Eclipse installation that JSure is installed into. The IDE will load and function normally, but when JSure functions are executed they will fail noting the lack of a license. Serviceability functions of the tool (e.g., sending problem reports to SureLogic, installing and uninstalling licenses) function properly without a license. The unlicensed JSure plug-in can be uninstalled or disabled within Eclipse.

When you receive a license file from SureLogic it is installed via this dialog. To install the license select the row in the license table that matches the type of license. For example, if you have been sent a JSure license select the JSure row in the license table. Next press the Install from File or Install from Clipboard button depending upon if you saved your license to a file or copied it from an email. Once the license is loaded press Activate to activate it with SureLogic. The tool checks with SureLogic and reports that your license has been installed and returns showing information about the installed license. The license file is not examined by the tool after the installation is completed unless you install the file again (after an uninstall).

To uninstall a license, select the row in the license table and press the Uninstall License. You will be asked if you are sure you want to uninstall the license. If you confirm the uninstall then the license is removed. This may take a minute as SureLogic is informed that your license has been uninstalled.

When a license is nearing expiration the tool warns the user with the dialog shown in Figure 2.36

Figure 2.36. Dialog warning that the installed JSure license is about to expire

Dialog warning that the installed JSure license is about to expire

When a license does expire it disappears from the dialog. The tool is considered unlicensed at that point. To fix this situation install a new license (it is not required to install a new version of JSure).

2.8. Bugs and tips

JSure allows any user to send problem reports and suggestions to SureLogic from the main menu. Selecting JSureSend Tip for Improvement or JSureSend Problem Report allows a tip or problem report to be send to SureLogic directly within Eclipse as shown in Figure 2.37. These menu choices bring up dialogs that allow the user to control exactly what information is sent to SureLogic. In addition, the user can preview the exact text that will be sent over the Internet.

Figure 2.37. Menu items to send bugs and tips to SureLogic

Menu items to send bugs and tips to SureLogic

The Send Tip for Improvement command opens a dialog to allow entry of a suggestion by the user to improve the JSure tool as seen in Figure 2.38. The dialog allows the user to control exactly what information is sent to SureLogic. In addition, the user can preview and edit the exact text that will be sent. If you have no Internet connection you can print or save the text of your problem report (to fax or email).

Figure 2.38. Dialog allowing the user to enter a tip to improve JSure

Dialog allowing the user to enter a tip to improve JSure

The Send Problem Report command opens a dialog to allow entry of a problem report by the user about the JSure tool as seen in Figure 2.39 The dialog allows the user to control exactly what information is sent to SureLogic. In addition, the user can preview and edit the exact text that will be sent. If you have no Internet connection you can print or save the text of your problem report (to fax or email).

Figure 2.39. Dialog allowing the user to enter a problem report about JSure

Dialog allowing the user to enter a problem report about JSure

The Send Library Annotation Changes command opens a dialog to allow the user to send any library annotation changes that they have made to SureLogic to be added into the standard set of annotations shipped with the JSure tool. The dialog that opens is seen in Figure 2.40 The dialog allows the user to control exactly what information is sent to SureLogic. In addition, the user can preview and edit the exact text that will be sent. If you have no Internet connection you can print or save the text of your annotation changes (to fax or email).

Figure 2.40. Dialog allowing the user to send library annotations to SureLogic

Dialog allowing the user to send library annotations to SureLogic

Messages sent from these dialogs go over HTTP to SureLogic. If a proxy is used on your network then you may need to configure Eclipse to use it. To do this open the Eclipse Preferences and examine the Network Connections under the General preferences. This dialog allows you to configure Eclipse for your network.

Chapter 3. Release notes

For each release of JSure there are new and noteworthy features to try out, and known limitations to avoid or workaround. These are presented in the sections below for each released version of JSure.

3.1. JSure version 5.6.1

This section describes the 5.6.1 version of the JSure Eclipse client.

3.1.1. New and Noteworthy

This section describes new and noteworthy features in this version of JSure.

  1. Reorganization of JSure menu — To make the JSure menu simpler to use we have reorganized it. Items are better grouped by use. This was driven, in part, by several changes to the tool are discussed below. The top section contains commands to operate JSure in Eclipse. The second section contains commands that import or export files. The third section contains commands to send feedback to SureLogic and run the JSure tutorials. The last section contains a command to open a dialog to manage your tool license.

  2. Improved Ant task — Several changes to the JSure Ant task are included in this version. If you use the Ant task you'll have to make some changes to your scripts. If not, the improvements made in this tool release may make the task useful in your development environment. A summary of the changes is listed below.

    1. The task is no longer included in the Eclipse distribution. It must be downloaded here on the surelogic website. The reason for this change is to reduce the Eclipse tool distribution size. When adding the Ant task, JSure doubles in size, with Ant and Maven it is 3X the download size. Now folks can download only what they need.

    2. The task has been simplified. It is still similar to the Ant javac task but now has simpler setup.

    3. Output from the Ant task is a Zip file that can be loaded into Eclipse. The name of the file encodes the information needed to load it into Eclipse.

    This approach is also intended to be supported in Maven but the Maven plugin for JSure is not yet complete. Further we plan to use the Ant and Maven to support predicates on the tool results (e.g., all annotations are consistent with the code). This future work will enable automated use of JSure in a "back office" automated build.

  3. HTML version of this documentation packaged with the tool — You can choose the Save Documentation As... menu item shown in the image below to save a jsure-html-docs.zip file on your disk. Inside this Zip file is the HTML version of this documentation that you can open in your browser. Some users prefer this format because they can display it in the browser of their preference.

3.2. JSure version 5.6.0

This section describes the 5.6.0 version of the JSure Eclipse client.

3.2.1. New and Noteworthy

This section describes new and noteworthy features in this version of JSure.

  1. Region declarations can now be inferred by JSure — You can use @InRegion or @UniqueInRegion annotations to allow inference of @Region annotations. This allows you to have the tool infer the correct information to declare a region of state. The intent is to make @RegionLock as simple to use as @GuardedBy.

    The image below shows the Animator class prior to this change. The explicit region declaration is highlighted.

    With this enhancement the code no longer needs this declaration as shown below.

    The promise is inferred and shows up in the verification results as a virtual promise (marked with a V).

    Of course, this feature is optional and the explicit declaration is still supported.

  2. New @TrackPartiallyInitialized annotation limits partially initialized object annotations in large existing codebases — The use of @NonNull on fields in an object now requires that class to be annotated @TrackPartiallyInitialized. This new annotation turns on checking of the class implementation and its superclass implementations to verify that dispatching during construction is annotated with @Initialized(through) annotations. Originally we did this analysis across the entire codebase but this proved tedious to annotate in large existing codebases. While you may place this annotation on any class you want it is only required if (a) the class contains @NonNull field or (b) a subclass of the class is annotated @TrackPartiallyInitialized.

    In the example above the Animator class is required to be annotated @TrackPartiallyInitialized because its f_startDirection field is @NonNull. This also forces any superclasses to be annotated @TrackPartiallyInitialized. In this example, that is only java.lang.Object, which, as we can see below, is annotated @TrackPartiallyInitialized.

    The tool will propose this annotation. So for many users this annotation can be edited in by the tool when you add @NonNull on one of the fields in your code. Just keep adding the proposed @TrackPartiallyInitialized promise to classes (goes up the class hierarchy) until no more proposals are made by the tool.

  3. Uniqueness annotations simplified — The uniqueness verifying analysis is still turned off by default, however, if it is turned on in this release (via the JSure menu in Eclipse) you will note that is simpler to use and its results are more understandable. In addition the promises have been simplified as of this release. The changes include the following: The @Borrowed annotation no longer has an allowReturn attribute. The @Immutable annotation no longer applies to references. The @BorrowedInRegion and @ReadOnly promises has been removed. The @Unique annotation annotation no longer has an allowRead attribute. The @UniqueInRegion annotation annotation no longer has an allowRead attribute.

    We will continue to work to make this analysis more straightforward to use over the next several JSure releases. This analysis is very useful for verifying security and concurrency properties of a codebase.