search

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

user_func_spec sometimes picks the wrong input/output vars for the summary #346

Open codyroux opened 3 years ago

codyroux commented 3 years ago

In WP, user_func_spec (https://github.com/draperlaboratory/cbat_tools/blob/8891fdeaa7dd79ae2ba37a3476a5a74c603db3e9/wp/lib/bap_wp/src/precondition.ml#L1298) uses the vars_from_sub heuristic to pick both the inputs and outputs of its arguments.

This is already a bit fishy: why should the inputs and outputs be the same?

Second of all: it's often the case that the user knows what the "actual" affected registers are.

Probably the right solution is to extract the variables init_R?? and R?? from the sub_pre and sub_post strings, and use them as the inputs and outputs, respectively.