jvm_field_is and jvm_elem_is declarations should check types
#904
Assignees
Labels
subsystem: crucible-jvm
Issues related to Java verification with crucible-jvm
Comments
brianhuffman
added
the
subsystem: crucible-jvm
brianhuffman
pushed a commit
that referenced
this issue
Nov 20, 2020
Fixes #904. The check is performed at the spec-construction phase, as opposed to during simulation; this means that type mismatches are caught with either `crucible_jvm_verify` or `crucible_jvm_unsafe_assume_spec`. The check uses the rather weak notion of register-compatibility as the criterion. This means that any two reference types are considered compatible, for example. It may be worth considering switching to a stronger type compatibility relation at a later time.
brianhuffman
pushed a commit
that referenced
this issue
Nov 25, 2020
Fixes #904. The check is performed at the spec-construction phase, as opposed to during simulation; this means that type mismatches are caught with either `crucible_jvm_verify` or `crucible_jvm_unsafe_assume_spec`. The check uses the rather weak notion of register-compatibility as the criterion. This means that any two reference types are considered compatible, for example. It may be worth considering switching to a stronger type compatibility relation at a later time.
brianhuffman
pushed a commit
that referenced
this issue
Nov 25, 2020
Fixes #904. The check is performed at the spec-construction phase, as opposed to during simulation; this means that type mismatches are caught with either `crucible_jvm_verify` or `crucible_jvm_unsafe_assume_spec`. The check uses the rather weak notion of register-compatibility as the criterion. This means that any two reference types are considered compatible, for example. It may be worth considering switching to a stronger type compatibility relation at a later time.
brianhuffman
pushed a commit
that referenced
this issue
Nov 25, 2020
The goal is to ensure that ill-formed JVMSetup blocks are caught at an early stage by `crucible_jvm_unsafe_assume_spec`. The tests also include a bunch of known false positives for other well-formedness checks on JVMSetup blocks that we do not perform yet.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Currently, when using
crucible_jvm_verify, you can write specs that containjvm_field_isorjvm_elem_isdeclarations with values of the wrong type. The type mismatch is not detected while these points-to declarations are being processed; however they may (or may not!) eventually lead to an "incorrect variant" error message later during symbolic simulation when that field or array element is read.We should be checking for type compatibility of points-to declarations at an earlier phase, just like we do for LLVM specs. We also need to make some effort to ensure that specs used with
crucible_jvm_unsafe_assume_specare type-correct.The text was updated successfully, but these errors were encountered: