Ccasin/user func spec modified vars fix

[ccasin]

Changes how we calculate what system state is modified when using a user function spec.

The old story was that we analyzed the actual implementation of the function to see what state it touched, and treated everything it touched as both an input an an output to the function. This had a few issues. Most pressingly, it doesn't work at all for functions where the implementation is unavailable or can't be analyzed. It also meant we overestimated what state is changed by a function.

The new system is to look at the variables in the user-provided function spec. Uses of variables corresponding to the initial values of registers/memory mean those are inputs, and uses of variables corresponding to the final values of registers/memory mean those are updated by the function. This works well enough - the tests pass (I haven't added new tests since it is exercised by all our existing user function spec tests).

[ccasin]

For the implementation, there are two hurdles: 1) get the variables, as strings, from the user-provided spec, and 2) find the corresponding Var.ts (since that is what is needed by the function summary code).

For 1: The user specs are parsed by mk_smtlib2_single. This function already finds the variables we care about, so it seems easiest to just have it return them in addition to the constraint. So I made a new version of it, mk_smtlib2_single_with_vars that does. (I changed mk_smtlib2_single to be defined in terms of it, to avoid code duplication).

For 2: It wasn't immediately obvious to me the best way to go from the variable strings to the corresponding Var.ts. I ended up just getting the set of Var.ts for all registers and memory from the env, and then filtering out anything that's not mentioned in the user spec.

Let me know if there's a better way to do either of these.

[fortunac]

For the implementation, there are two hurdles: 1) get the variables, as strings, from the user-provided spec, and 2) find the corresponding Var.ts (since that is what is needed by the function summary code).

For 1: The user specs are parsed by mk_smtlib2_single. This function already finds the variables we care about, so it seems easiest to just have it return them in addition to the constraint. So I made a new version of it, mk_smtlib2_single_with_vars that does. (I changed mk_smtlib2_single to be defined in terms of it, to avoid code duplication).

For 2: It wasn't immediately obvious to me the best way to go from the variable strings to the corresponding Var.ts. I ended up just getting the set of Var.ts for all registers and memory from the env, and then filtering out anything that's not mentioned in the user spec.

Let me know if there's a better way to do either of these.

I can't think of a better solution for those issues. One pressing question I have would be if there is ever a case where the user has a virtual variable in their spec. If there is a case, are we able to handle this?

[ccasin]

Your last question is a good one, but I think we're fine. The way sub_inputs and sub_outputs are calculated is that we start from the set of register/memory names we got out of the environment, and we then keep only the ones that match a name in the user spec. We are never adding random things from the user spec to this set.