Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make ArrayBoundsChecker a whole-program analysis to fix a concurrency bug #1453

Open
wants to merge 4 commits into
base: develop
Choose a base branch
from
Open

Make ArrayBoundsChecker a whole-program analysis to fix a concurrency bug #1453

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
b49f156
- Make ArrayBoundsChecker a whole-program analysis to fix a concurren…
invalid-email-address Sep 2, 2020
e35d8f0
Update ArrayBoundsChecker.java
tiziw Sep 2, 2020
44059c0
Update ArrayBoundsChecker.java
tiziw Sep 2, 2020
396402b
Update ArrayBoundsChecker.java
tiziw Sep 2, 2020
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
192 changes: 96 additions & 96 deletions eclipse/ca.mcgill.sable.soot/src/ca/mcgill/sable/soot/testing/TestOptionsDialogHandler.java
View file
Open in desktop

Large diffs are not rendered by default.

76 changes: 38 additions & 38 deletions eclipse/ca.mcgill.sable.soot/src/ca/mcgill/sable/soot/ui/PhaseOptionsDialog.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -627,6 +627,26 @@ private void initializeEnableGroups() {
getwjapwjap_purityannotate_widget().getButton().addSelectionListener(this);
getwjapwjap_purityverbose_widget().getButton().addSelectionListener(this);

makeNewEnableGroup("wjap", "wjap.abc");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcenabled_widget(), "enabled");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcwith_all_widget(), "with-all");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcwith_cse_widget(), "with-cse");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcwith_arrayref_widget(), "with-arrayref");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcwith_fieldref_widget(), "with-fieldref");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcwith_classfield_widget(), "with-classfield");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcwith_rectarray_widget(), "with-rectarray");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcprofiling_widget(), "profiling");
addToEnableGroup("wjap", "wjap.abc", getjapjap_abcadd_color_tags_widget(), "add-color-tags");
getjapjap_abcenabled_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_all_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_cse_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_arrayref_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_fieldref_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_classfield_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_rectarray_widget().getButton().addSelectionListener(this);
getjapjap_abcprofiling_widget().getButton().addSelectionListener(this);
getjapjap_abcadd_color_tags_widget().getButton().addSelectionListener(this);

makeNewEnableGroup("shimple");
addToEnableGroup("shimple", getshimpleenabled_widget(), "enabled");
addToEnableGroup("shimple", getshimplenode_elim_opt_widget(), "node-elim-opt");
Expand Down Expand Up @@ -750,26 +770,6 @@ private void initializeEnableGroups() {
addToEnableGroup("jap", "jap.npcolorer", getjapjap_npcolorerenabled_widget(), "enabled");
getjapjap_npcolorerenabled_widget().getButton().addSelectionListener(this);

makeNewEnableGroup("jap", "jap.abc");
addToEnableGroup("jap", "jap.abc", getjapjap_abcenabled_widget(), "enabled");
addToEnableGroup("jap", "jap.abc", getjapjap_abcwith_all_widget(), "with-all");
addToEnableGroup("jap", "jap.abc", getjapjap_abcwith_cse_widget(), "with-cse");
addToEnableGroup("jap", "jap.abc", getjapjap_abcwith_arrayref_widget(), "with-arrayref");
addToEnableGroup("jap", "jap.abc", getjapjap_abcwith_fieldref_widget(), "with-fieldref");
addToEnableGroup("jap", "jap.abc", getjapjap_abcwith_classfield_widget(), "with-classfield");
addToEnableGroup("jap", "jap.abc", getjapjap_abcwith_rectarray_widget(), "with-rectarray");
addToEnableGroup("jap", "jap.abc", getjapjap_abcprofiling_widget(), "profiling");
addToEnableGroup("jap", "jap.abc", getjapjap_abcadd_color_tags_widget(), "add-color-tags");
getjapjap_abcenabled_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_all_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_cse_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_arrayref_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_fieldref_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_classfield_widget().getButton().addSelectionListener(this);
getjapjap_abcwith_rectarray_widget().getButton().addSelectionListener(this);
getjapjap_abcprofiling_widget().getButton().addSelectionListener(this);
getjapjap_abcadd_color_tags_widget().getButton().addSelectionListener(this);

makeNewEnableGroup("jap", "jap.profiling");
addToEnableGroup("jap", "jap.profiling", getjapjap_profilingenabled_widget(), "enabled");
addToEnableGroup("jap", "jap.profiling", getjapjap_profilingnotmainentry_widget(), "notmainentry");
Expand Down Expand Up @@ -15163,7 +15163,7 @@ private Composite japjap_abcCreate(Composite parent) {



defKey = "p phase-option"+" "+"jap.abc"+" "+"enabled";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"enabled";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15172,9 +15172,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcenabled_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("Enabled", "p phase-option", "jap.abc","enabled", "\n", defaultBool)));
setjapjap_abcenabled_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("Enabled", "p phase-option", "wjap.abc","enabled", "\n", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"with-all";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"with-all";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15183,9 +15183,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcwith_all_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With All", "p phase-option", "jap.abc","with-all", "\nSetting the With All option to true is equivalent to setting \neach of With CSE, With Array Ref, With Field Ref, With Class \nField, and With Rectangular Array to true.", defaultBool)));
setjapjap_abcwith_all_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With All", "p phase-option", "wjap.abc","with-all", "\nSetting the With All option to true is equivalent to setting \neach of With CSE, With Array Ref, With Field Ref, With Class \nField, and With Rectangular Array to true.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"with-cse";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"with-cse";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15194,9 +15194,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcwith_cse_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Common Sub-expressions", "p phase-option", "jap.abc","with-cse", "\nThe analysis will consider common subexpressions. For example, \nconsider the situation where r1 is assigned a*b; later, r2 is \nassigned a*b, where neither a nor b have changed between the two \nstatements. The analysis can conclude that r2 has the same value \nas r1. Experiments show that this option can improve the result \nslightly.", defaultBool)));
setjapjap_abcwith_cse_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Common Sub-expressions", "p phase-option", "wjap.abc","with-cse", "\nThe analysis will consider common subexpressions. For example, \nconsider the situation where r1 is assigned a*b; later, r2 is \nassigned a*b, where neither a nor b have changed between the two \nstatements. The analysis can conclude that r2 has the same value \nas r1. Experiments show that this option can improve the result \nslightly.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"with-arrayref";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"with-arrayref";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15205,9 +15205,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcwith_arrayref_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Array References", "p phase-option", "jap.abc","with-arrayref", "\nWith this option enabled, array references can be considered as \ncommon subexpressions; however, we are more conservative when \nwriting into an array, because array objects may be aliased. We \nalso assume that the application is single-threaded or that the \narray references occur in a synchronized block. That is, we \nassume that an array element may not be changed by other threads \nbetween two array references.", defaultBool)));
setjapjap_abcwith_arrayref_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Array References", "p phase-option", "wjap.abc","with-arrayref", "\nWith this option enabled, array references can be considered as \ncommon subexpressions; however, we are more conservative when \nwriting into an array, because array objects may be aliased. We \nalso assume that the application is single-threaded or that the \narray references occur in a synchronized block. That is, we \nassume that an array element may not be changed by other threads \nbetween two array references.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"with-fieldref";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"with-fieldref";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15216,9 +15216,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcwith_fieldref_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Field References", "p phase-option", "jap.abc","with-fieldref", "\nThe analysis treats field references (static and instance) as \ncommon subexpressions; however, we are more conservative when \nwriting to a field, because the base of the field reference may \nbe aliased. We also assume that the application is \nsingle-threaded or that the field references occur in a \nsynchronized block. That is, we assume that a field may not be \nchanged by other threads between two field references.", defaultBool)));
setjapjap_abcwith_fieldref_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Field References", "p phase-option", "wjap.abc","with-fieldref", "\nThe analysis treats field references (static and instance) as \ncommon subexpressions; however, we are more conservative when \nwriting to a field, because the base of the field reference may \nbe aliased. We also assume that the application is \nsingle-threaded or that the field references occur in a \nsynchronized block. That is, we assume that a field may not be \nchanged by other threads between two field references.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"with-classfield";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"with-classfield";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15227,9 +15227,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcwith_classfield_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Class Field", "p phase-option", "jap.abc","with-classfield", "\nThis option makes the analysis work on the class level. The \nalgorithm analyzes final or private class fields first. It can \nrecognize the fields that hold array objects of constant length. \nIn an application using lots of array fields, this option can \nimprove the analysis results dramatically.", defaultBool)));
setjapjap_abcwith_classfield_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Class Field", "p phase-option", "wjap.abc","with-classfield", "\nThis option makes the analysis work on the class level. The \nalgorithm analyzes final or private class fields first. It can \nrecognize the fields that hold array objects of constant length. \nIn an application using lots of array fields, this option can \nimprove the analysis results dramatically.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"with-rectarray";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"with-rectarray";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15238,9 +15238,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcwith_rectarray_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Rectangular Array", "p phase-option", "jap.abc","with-rectarray", "\nThis option is used together with wjap.ra to make Soot run the \nwhole-program analysis for rectangular array objects. This \nanalysis is based on the call graph, and it usually takes a long \ntime. If the application uses rectangular arrays, these options \ncan improve the analysis result.", defaultBool)));
setjapjap_abcwith_rectarray_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("With Rectangular Array", "p phase-option", "wjap.abc","with-rectarray", "\nThis option is used together with wjap.ra to make Soot run the \nwhole-program analysis for rectangular array objects. This \nanalysis is based on the call graph, and it usually takes a long \ntime. If the application uses rectangular arrays, these options \ncan improve the analysis result.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"profiling";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"profiling";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15249,9 +15249,9 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcprofiling_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("Profiling", "p phase-option", "jap.abc","profiling", "\nProfile the results of array bounds check analysis. The inserted \nprofiling code assumes the existence of a MultiCounter class \nimplementing the methods invoked. For details, see the \nArrayBoundsChecker source code.", defaultBool)));
setjapjap_abcprofiling_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("Profiling", "p phase-option", "wjap.abc","profiling", "\nProfile the results of array bounds check analysis. The inserted \nprofiling code assumes the existence of a MultiCounter class \nimplementing the methods invoked. For details, see the \nArrayBoundsChecker source code.", defaultBool)));

defKey = "p phase-option"+" "+"jap.abc"+" "+"add-color-tags";
defKey = "p phase-option"+" "+"wjap.abc"+" "+"add-color-tags";
defKey = defKey.trim();

if (isInDefList(defKey)) {
Expand All @@ -15260,7 +15260,7 @@ private Composite japjap_abcCreate(Composite parent) {
defaultBool = false;
}

setjapjap_abcadd_color_tags_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("Add Color Tags", "p phase-option", "jap.abc","add-color-tags", "\nAdd color tags to the results of the array bounds check \nanalysis.", defaultBool)));
setjapjap_abcadd_color_tags_widget(new BooleanOptionWidget(editGroupjapjap_abc, SWT.NONE, new OptionData("Add Color Tags", "p phase-option", "wjap.abc","add-color-tags", "\nAdd color tags to the results of the array bounds check \nanalysis.", defaultBool)));


return editGroupjapjap_abc;
Expand Down
134 changes: 67 additions & 67 deletions src/main/generated/options/soot/AntTask.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -628,14 +628,14 @@ public void setannot_purity(boolean arg) {
if(arg) addArg("-annot-purity");
}

public void setannot_nullpointer(boolean arg) {
if(arg) addArg("-annot-nullpointer");
}

public void setannot_arraybounds(boolean arg) {
if(arg) addArg("-annot-arraybounds");
}

public void setannot_nullpointer(boolean arg) {
if(arg) addArg("-annot-nullpointer");
}

public void setannot_side_effect(boolean arg) {
if(arg) addArg("-annot-side-effect");
}
Expand Down Expand Up @@ -2306,6 +2306,69 @@ public void setverbose(boolean arg) {

}

public Object createp_wjap_abc() {
Object ret = new PhaseOptwjap_abc();
phaseopts.add(ret);
return ret;
}
public class PhaseOptwjap_abc {

public void setenabled(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("enabled:"+(arg?"true":"false"));
}

public void setwith_all(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("with-all:"+(arg?"true":"false"));
}

public void setwith_cse(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("with-cse:"+(arg?"true":"false"));
}

public void setwith_arrayref(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("with-arrayref:"+(arg?"true":"false"));
}

public void setwith_fieldref(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("with-fieldref:"+(arg?"true":"false"));
}

public void setwith_classfield(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("with-classfield:"+(arg?"true":"false"));
}

public void setwith_rectarray(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("with-rectarray:"+(arg?"true":"false"));
}

public void setprofiling(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("profiling:"+(arg?"true":"false"));
}

public void setadd_color_tags(boolean arg) {
addArg("-p");
addArg("wjap.abc");
addArg("add-color-tags:"+(arg?"true":"false"));
}

}

public Object createp_shimple() {
Object ret = new PhaseOptshimple();
phaseopts.add(ret);
Expand Down Expand Up @@ -2744,69 +2807,6 @@ public void setenabled(boolean arg) {

}

public Object createp_jap_abc() {
Object ret = new PhaseOptjap_abc();
phaseopts.add(ret);
return ret;
}
public class PhaseOptjap_abc {

public void setenabled(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("enabled:"+(arg?"true":"false"));
}

public void setwith_all(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("with-all:"+(arg?"true":"false"));
}

public void setwith_cse(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("with-cse:"+(arg?"true":"false"));
}

public void setwith_arrayref(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("with-arrayref:"+(arg?"true":"false"));
}

public void setwith_fieldref(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("with-fieldref:"+(arg?"true":"false"));
}

public void setwith_classfield(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("with-classfield:"+(arg?"true":"false"));
}

public void setwith_rectarray(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("with-rectarray:"+(arg?"true":"false"));
}

public void setprofiling(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("profiling:"+(arg?"true":"false"));
}

public void setadd_color_tags(boolean arg) {
addArg("-p");
addArg("jap.abc");
addArg("add-color-tags:"+(arg?"true":"false"));
}

}

public Object createp_jap_profiling() {
Object ret = new PhaseOptjap_profiling();
phaseopts.add(ret);
Expand Down
Loading