Skip to content

README.md

Latest commit

 

History

History
101 lines (68 loc) · 3.61 KB

README.md

File metadata and controls

101 lines (68 loc) · 3.61 KB

Dataflow type system README

Requirements

In order to use the dataflow type system, you first need to set up the following four projects:

You'll need environment variables CHECKERFRAMEWORK, JAVA_HOME, and AFU set up appropriately. The insert-annotations-to-source script from AFU must be on your path.

The tool do-like-javac makes usage easier:

I created a shortcut for this tool:

alias dljc='/the/path/to/do-like-javac/dljc'

The tool graphviz could visualize the dot files that are generated by checker-framework.

Running Example

dataflowexample can be found under /the/path/to/checker-framework-inference/testing. This is a sample project that is annotated without any @Dataflow annotations, so you can play around with it: type check, type infer, insert the inferred annotations to source code, visualize the control flow graph, etc.

Here are some instructions that shows how to do these tasks with do-like-javac:

  1. Change into the dataflowexample directory:
cd /the/path/to/checker-framework-inference/testing/dataflowexample
  1. Compile sub-project libs that is referenced by sub-project project:
ant compile-libs
  1. Invoke the inference tool using do-like-javac. The ROUNDTRIP mode will generate and solve the constraints and then inserts the results back into the original source code. If the whole process runs successfully, the inserted output will be placed in annotated directory.
dljc -t inference --checker dataflow.DataflowChecker --solver dataflow.solvers.general.DataflowGeneralSolver --mode ROUNDTRIP --solverArgs="backEndType=MaxSAT" -afud annotated -- ant compile-project
  1. Invoke the checker tool with do-like-javac. This step will type check the newly created source code, and generate .dot files (in the dotfiles directory) that visualize the control flow graph.
dljc -t checker --checker "dataflow.DataflowChecker -Aflowdotdir=./dotfiles" -o logs -- ant check-annotated-src

Note the quotes around the --checker argument to ensure the whole string is used.

  1. Visualize the dot files by tool graphviz. This step will generate a pdf file that contains the control flow graph.
dot -Tpdf dotfiles/_init_Dataflow.dot -o CFG.pdf

If you compare the original source code with the source code generated by the third step, you can find the string field thisIsString and thisShouldbeString are annotated with @DataFlow(typeNames={"java.lang.String"}) in the new source code, although the declared type of thisShouldbeString is Object.

Alternatively, you can simply execute sh ./runDataflowSolver.sh under /the/path/to/checker-framework-inference/testing/dataflowexample to run the dataflow example.

Running On Open Source

If you want to infer Dataflow annotations for large open source projects, the steps are very similar to the above instructions.

In second step, instead of running:

dljc -t inference --checker dataflow.DataflowChecker
  --solver dataflow.solvers.classic.DataflowSolver -o logs 
  -m ROUNDTRIP -afud annotated -- ant compile-project

Changing ant compile-project to the build command for the open source project, and if the whole process runs successfully, the output with annotations inserted will be placed in annotated directory.