Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .travis-build.sh
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ if [[ "${GROUP}" == "cfi-tests" || "${GROUP}" == "all" ]]; then

./gradlew test

./gradlew testDataflowExternalSolvers
./gradlew testRefValExternalSolvers
fi

# Downstream tests
Expand Down
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ To test the build:
````
./gradlew testCheckerInferenceScript
./gradlew testCheckerInferenceDevScript
./gradlew testDataflowExternalSolvers
./gradlew testRefValExternalSolvers
````


Expand Down Expand Up @@ -133,9 +133,9 @@ Specifies which checker to run.
The three most supported checkers at the moment are
`ostrusted.OsTrustedChecker`,
`checkers.tainting.TaintingChecker` and
`dataflow.DataflowChecker`.
`refval.RefValChecker`.

You can find details of `dataflow.DataflowChecker` in [README.dataflow](src/dataflow/README.md)
You can find details of `refval.RefValChecker` in [README.refval](src/refval/README.md)

* `--solver`
Which solver to use on the constraints.
Expand Down
6 changes: 3 additions & 3 deletions build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -270,9 +270,9 @@ task testCheckerInferenceDevScript(type: Exec, dependsOn: [dist, dependenciesJar
'testdata/interning/MapAssignment.java']
}

task testDataflowExternalSolvers(type: Exec, dependsOn: [dist, dependenciesJar]) {
description 'Test Dataflow type system on its external solvers Lingeling and LogicBlox'
executable './testing/dataflowexample/travis-test.sh'
task testRefValExternalSolvers(type: Exec, dependsOn: [dist, dependenciesJar]) {
description 'Test Reference Value type system on its external solvers Lingeling and LogicBlox'
executable './testing/refval-example/travis-test.sh'
}

afterEvaluate {
Expand Down
2 changes: 1 addition & 1 deletion src/checkers/inference/DefaultInferenceResult.java
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ public class DefaultInferenceResult implements InferenceResult {
* 1) Try to create empty solution
* 2) Subclass calls this super constructor to begin with an empty map. Then subclass
* has its logic to adding solutions to the mapping {@link #varIdToAnnotation}. The existing two
* subclasses are: {@link dataflow.solvers.classic.DataflowResult} and {@link sparta.checkers.sat.IFlowResult}.
* subclasses are: {@link refval.solvers.classic.RefValResult} and {@link sparta.checkers.sat.IFlowResult}.
*/
public DefaultInferenceResult() {
this(new HashMap<>());
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@
import checkers.inference.model.ExistentialConstraint;
import checkers.inference.model.Slot;
import checkers.inference.model.SubtypeConstraint;
import dataflow.DataflowVisitor;
import dataflow.util.DataflowUtils;
import refval.RefValVisitor;
import refval.util.RefValUtils;

/**
* GraphBuilder builds the constraint graph and runs graph traversal algorithms
Expand Down Expand Up @@ -133,8 +133,8 @@ private Set<Constraint> BFSSearch(Vertex vertex) {
if (AnnotationUtils.areSame(top, next.getValue())) {
continue;
} else {
if (InferenceMain.getInstance().getVisitor() instanceof DataflowVisitor) {
String[] typeNames = DataflowUtils.getTypeNames(next.getValue());
if (InferenceMain.getInstance().getVisitor() instanceof RefValVisitor) {
String[] typeNames = RefValUtils.getTypeNames(next.getValue());
if (typeNames.length == 1 && typeNames[0].length() == 0) {
continue;
}
Expand Down
37 changes: 0 additions & 37 deletions src/dataflow/solvers/classic/DatatypeSolution.java

This file was deleted.

202 changes: 0 additions & 202 deletions src/dataflow/util/DataflowUtils.java

This file was deleted.

26 changes: 13 additions & 13 deletions src/dataflow/README.md → src/refval/README.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
Dataflow type system README
Reference Value type system README
===========================

Requirements
------------

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

- https://github.com/typetools/annotation-tools
Expand Down Expand Up @@ -32,15 +32,15 @@ The tool `graphviz` could visualize the dot files that are generated by checker-
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.
`refvalexample` can be found under `/the/path/to/checker-framework-inference/testing`. This is a sample project that is annotated without any @Refval 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:
1. Change into the refvalexample directory:

```
cd /the/path/to/checker-framework-inference/testing/dataflowexample
cd /the/path/to/checker-framework-inference/testing/refvalexample
```

2. Compile sub-project `libs` that is referenced by sub-project `project`:
Expand All @@ -55,7 +55,7 @@ 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
dljc -t inference --checker refval.RefValChecker --solver refval.solvers.general.RefvalSolverEngine --mode ROUNDTRIP --solverArgs="backEndType=MaxSAT" -afud annotated -- ant compile-project
```

4. Invoke the checker tool with `do-like-javac`.
Expand All @@ -64,7 +64,7 @@ This step will type check the newly created source code, and generate
control flow graph.

```
dljc -t checker --checker "dataflow.DataflowChecker -Aflowdotdir=./dotfiles" -o logs -- ant check-annotated-src
dljc -t checker --checker "refval.RefValChecker -Aflowdotdir=./dotfiles" -o logs -- ant check-annotated-src
```
Note the quotes around the `--checker` argument to ensure the
whole string is used.
Expand All @@ -73,26 +73,26 @@ whole string is used.
5. 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
dot -Tpdf dotfiles/_init_Refval.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`.
`@RefVal(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.
Alternatively, you can simply execute `sh ./runRefValSolver.sh` under `/the/path/to/checker-framework-inference/testing/refvalexample` to run the refval 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.
If you want to infer Refval 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
dljc -t inference --checker refval.RefValChecker
--solver refval.solvers.classic.RefValSolver -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.
Expand Down
Loading