Primitive crucible_setup_val_to_typed_term is broken

[brianhuffman]

Function setupToTerm, which is used to implement the saw-script primitive crucible_setup_val_to_typed_term, appears to be defined incorrectly:

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

Lines 161 to 205 in f991bb4

	-- | Convert a setup value to a SAW-Core term. This is a partial
	-- function, as certain setup values ---SetupVar, SetupNull and
	-- SetupGlobal--- don't have semantics outside of the symbolic
	-- simulator.
	setupToTerm ::
	Options ->
	SharedContext ->
	SetupValue ext ->
	MaybeT IO Term
	setupToTerm opts sc =
	\case
	SetupTerm term -> return (ttTerm term)
	SetupStruct _ _ fields ->
	do ts <- mapM (setupToTerm opts sc) fields
	lift $ scTuple sc ts
	SetupArray _ elems@(_:_) ->
	do ts@(t:_) <- mapM (setupToTerm opts sc) elems
	typt <- lift $ scTypeOf sc t
	vec <- lift $ scVector sc typt ts
	typ <- lift $ scTypeOf sc vec
	lift $ printOutLn opts Info $ show vec
	lift $ printOutLn opts Info $ show typ
	return vec
	SetupElem _ base ind ->
	case base of
	SetupArray _ elems@(e:_) ->
	do let intToNat = fromInteger . toInteger
	art <- setupToTerm opts sc base
	ixt <- lift $ scNat sc $ intToNat ind
	lent <- lift $ scNat sc $ intToNat $ length elems
	et <- setupToTerm opts sc e
	typ <- lift $ scTypeOf sc et
	lift $ scAt sc lent typ art ixt
	SetupStruct _ _ fs ->
	do st <- setupToTerm opts sc base
	lift $ scTupleSelector sc st ind (length fs)
	_ -> MaybeT $ return Nothing
	-- SetupVar, SetupNull, SetupGlobal
	_ -> MaybeT $ return Nothing

Specifically, it assumes the wrong meaning for the CrucibleElem constructor for SetupValues. In reality, CrucibleElem is like LLVM's getelementptr; it takes an argument that is a pointer to a struct or an array, and returns a pointer to a field or element. However, the code here assumes that it takes an argument that is not a pointer, but an actual array or struct literal. So if in saw-script you applied crucible_elem to a crucible_array or crucible_struct value (which doesn't really make sense) then crucible_setup_val_to_typed_term would assign the wrong meaning to the result.

EDIT: I should add that I'm looking at this function because its implementation uses mkTypedTerm, which I'm trying to eradicate (#718). I don't want to rewrite the definition to avoid mkTypedTerm while it's still wrong. Actually I'm not sure if it's even worth fixing the underlying problem, or if we should just remove crucible_setup_val_to_typed_term completely; it doesn't seem to be used by anything, as far as I can tell.

[robdockins]

I guess we should deprecate and remove this operation?

[brianhuffman]

Yeah, I guess deprecating it would be a good first step.