Detect when jvm_return is missing when it was expected

[brianhuffman]

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:

• repeated jvm_field_is on the same field (Multiple jvm_field_is declarations on same field are not detected #937)
• invalid index for jvm_elem_is
• type checking for jvm_array_is
• jvm_array_is and jvm_elem_is on the same array
• number and type of arguments for jvm_execute_func
• type checking for jvm_return
• missing/extra jvm_return

[brianhuffman]

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.

saw-script/src/SAWScript/Crucible/Common/MethodSpec.hs

Lines 268 to 286 in 404e227

	-- | Test whether the pointer represented by the given SetupValue has
	-- been initialized already.
	testResolved ::
	SetupValue ext ->
	[Either String Int] {-^ path within this object (if any) -} ->
	ResolvedState ->
	Bool
	testResolved val0 path0 rs = go path0 val0
	where
	go path val =
	case val of
	SetupVar n -> test path (Map.lookup n (_rsAllocs rs))
	SetupGlobal _ c -> test path (Map.lookup c (_rsGlobals rs))
	SetupElem _ v idx -> go (Right idx : path) v
	SetupField _ v fld -> go (Left fld : path) v
	_ -> False
	test _ Nothing = False
	test path (Just paths) = any (`isPrefixOf` path) paths

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]

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