-
Notifications
You must be signed in to change notification settings - Fork 63
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #1293 from GaloisInc/jvm-static-field-writable
Set and use writability permission bits on JVM static fields
- Loading branch information
Showing
10 changed files
with
245 additions
and
33 deletions.
There are no files selected for viewing
Submodule crucible
updated
3 files
| +10 −2 | crucible-jvm/src/Lang/Crucible/JVM/Context.hs | |
| +38 −15 | crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs | |
| +7 −4 | crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| %.class: %.java | ||
| javac -g $< |
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
| class Test | ||
| { | ||
| static int a; | ||
| int b; | ||
|
|
||
| public void set(int x) { | ||
| a = x; | ||
| b = x; | ||
| } | ||
| public int test_a(int x) { | ||
| set(x); | ||
| return a; | ||
| } | ||
| public int test_b(int x) { | ||
| set(x); | ||
| return b; | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,90 @@ | ||
| // This is a regression test for saw-script issue #900; it tests whether | ||
| // `jvm_verify` will successfully verify a spec that does not specify a | ||
| // new value for a field, when the method actually does modify that | ||
| // field. For soundness of compositional verification, it is required | ||
| // that such a verification will fail. | ||
| // https://github.com/GaloisInc/saw-script/issues/900 | ||
|
|
||
| enable_experimental; | ||
| c <- java_load_class "Test"; | ||
|
|
||
| let set_spec_1 = | ||
| do { | ||
| this <- jvm_alloc_object "Test"; | ||
| x <- jvm_fresh_var "x" java_int; | ||
| jvm_execute_func [this, jvm_term x]; | ||
| jvm_field_is this "b" (jvm_term x); | ||
| }; | ||
|
|
||
| let set_spec_2 = | ||
| do { | ||
| this <- jvm_alloc_object "Test"; | ||
| x <- jvm_fresh_var "x" java_int; | ||
| jvm_execute_func [this, jvm_term x]; | ||
| jvm_static_field_is "a" (jvm_term x); | ||
| }; | ||
|
|
||
| set_ov_1 <- jvm_unsafe_assume_spec c "set" set_spec_1; | ||
| set_ov_2 <- jvm_unsafe_assume_spec c "set" set_spec_2; | ||
|
|
||
| let one = jvm_term {{ 1:[32] }}; | ||
| let two = jvm_term {{ 2:[32] }}; | ||
|
|
||
| // A correct spec for test_a. | ||
| jvm_verify c "test_a" [] false | ||
| do { | ||
| this <- jvm_alloc_object "Test"; | ||
| jvm_static_field_is "a" one; | ||
| jvm_execute_func [this, two]; | ||
| jvm_static_field_is "a" two; | ||
| jvm_field_is this "b" two; | ||
| jvm_return two; | ||
| } | ||
| z3; | ||
|
|
||
| // An incorrect spec for test_a, which can be proven using the bogus | ||
| // spec set_ov_1. | ||
| jvm_verify c "test_a" [set_ov_1] false | ||
| do { | ||
| this <- jvm_alloc_object "Test"; | ||
| jvm_static_field_is "a" one; | ||
| jvm_execute_func [this, two]; | ||
| jvm_static_field_is "a" one; | ||
| jvm_field_is this "b" two; | ||
| jvm_return one; | ||
| } | ||
| z3; | ||
|
|
||
| // A correct spec for test_b. | ||
| jvm_verify c "test_b" [] false | ||
| do { | ||
| this <- jvm_alloc_object "Test"; | ||
| jvm_static_field_is "a" one; | ||
| jvm_field_is this "b" one; | ||
| jvm_execute_func [this, two]; | ||
| jvm_static_field_is "a" two; | ||
| jvm_field_is this "b" two; | ||
| jvm_return two; | ||
| } | ||
| z3; | ||
|
|
||
| // An incorrect spec for test_b, which can be proven using the bogus | ||
| // spec set_ov_2. | ||
| jvm_verify c "test_b" [set_ov_2] false | ||
| do { | ||
| this <- jvm_alloc_object "Test"; | ||
| jvm_static_field_is "a" one; | ||
| jvm_field_is this "b" one; | ||
| jvm_execute_func [this, two]; | ||
| jvm_static_field_is "a" two; | ||
| jvm_field_is this "b" one; | ||
| jvm_return one; | ||
| } | ||
| z3; | ||
|
|
||
| // It should be impossible to verify the bogus set_spec_1. | ||
| fails (jvm_verify c "set" [] false set_spec_1 z3); | ||
|
|
||
| // It should be impossible to verify the bogus set_spec_2. | ||
| // FIXME: this should fail | ||
| jvm_verify c "set" [] false set_spec_2 z3; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| $SAW test.saw |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.