search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

Detect when `jvm_return` is missing when it was expected #938

Open brianhuffman opened 4 years ago

brianhuffman commented 4 years ago

PR #929 adds a collection of regression tests that ensure that crucible_jvm_unsafe_assume_spec and crucible_jvm_verify will catch ill-formed JVMSetup blocks. The tests for the type-correctness checks added in #929 work as expected. However there are a lot of other bogus JVMSetup blocks that are not caught; these are marked in the test script as "KNOWN FALSE POSITIVE".

We should enhance the well-formedness checks in SAW/JVM to eliminate all the known false positives in the test suite. These include:

brianhuffman commented 3 years ago

PR #948 fixes almost all of the remaining known false positive test cases.

One that remains is "jvm_return missing when one was expected", which will need to be fixed in a different way from most of the others: While all the other error checks are associated with running a specific setup command, this error condition can only be detected at a slightly later phase, by the surrounding function that actually runs the entire setup block and processes the resulting methodspec.

The other remaining test is "jvm_array_is with previous jvm_elem_is", where we have already specified the contents of one or more individual array elements, and then later we try to specify the contents of the whole thing. The problem here is in the definition of function testResolved, which is used to determine whether the location being specified has been specified already. https://github.com/GaloisInc/saw-script/blob/404e22726fd9198dbd10efbb931304c1674ec832/src/SAWScript/Crucible/Common/MethodSpec.hs#L268-L286 That function is designed to only return True if the indicated location has been completely specified already; i.e. either the same location or else one that totally covers the current one is already in the map. But what we really want is a different check: We want to return False only if the indicated location is completely disjoint from all previously used locations; in the case of a partial overlap (like jvm_array_is after jvm_elem_is) we also want to get True. However, this change will need to be done with care, because this code is also used for LLVM specs and such a change could possibly break proof scripts. Probably the best approach is to make a PR that makes only this one small change.

brianhuffman commented 2 years ago

The issue with jvm_array_is and jvm_elem_is has been resolved; only the missing jvm_return case still remains.