There are some slight differences between smtlib and sexplib and different notions of allowed identifiers in bap, smtlib, and sexplib that have continually made things awkward. In addition, there is in principle a possibility of name clashing of high level variables and low level variables.
namespace all variables with disjoint prefixes cbatvar_, highlevelvar_, realreg etc as need be. The names will still be | quoted in the presence of #, but sexplib will work. let name = "cbat_" ^ name in would basically do it
Replace # with a friendlier character here. Anything else. The smtlib allows for " a non-empty sequence of letters, digits and the characters + - / * = % ? ! . $ _ ˜ & ˆ < > @ that does not start with a digit"
Leave as is. The new feature will use sprintf injection of smtlib library functions and not use Sexp.t
Ask bap very nicely to use a different character for it's internally generated names. This is of course not really under our control and would probably break all sorts of stuff across the bap ecosystem. So not a very good solution.
As a possible increase of scope of this ticket, perhaps we also want a better way to namespace the init__orig, _mod versions of variables.
There are some slight differences between smtlib and sexplib and different notions of allowed identifiers in bap, smtlib, and sexplib that have continually made things awkward. In addition, there is in principle a possibility of name clashing of high level variables and low level variables.
The canonical example (perhaps only really) that causes this issue is the bap generated identifier like
#80. A#character in smtlib identifiers must be quoted using|#80|syntax. Z3 is not entirely consistent to my understanding of how it treats the|quotes, so we sometimes have to strip them https://github.com/draperlaboratory/cbat_tools/blob/176753aea3d49b6d8b9a3590b25399727a07abe0/wp/lib/bap_wp/src/z3_utils.ml#L35 This however clashes with sexplib, which uses|#and#|to denote block comments. To abandon or replicate sexplib merely for this feels insane. That led to this embarassing hack https://github.com/draperlaboratory/cbat_tools/blob/176753aea3d49b6d8b9a3590b25399727a07abe0/wp/lib/bap_wp/src/z3_utils.ml#L263Here are possible suggestions both of which can be done at https://github.com/draperlaboratory/cbat_tools/blob/176753aea3d49b6d8b9a3590b25399727a07abe0/wp/lib/bap_wp/src/environment.ml#L111 I believe:
cbatvar_,highlevelvar_,realregetc as need be. The names will still be|quoted in the presence of#, but sexplib will work.let name = "cbat_" ^ name inwould basically do it#with a friendlier character here. Anything else. The smtlib allows for " a non-empty sequence of letters, digits and the characters + - / * = % ? ! . $ _ ˜ & ˆ < > @ that does not start with a digit"sprintfinjection of smtlib library functions and not use Sexp.tAs a possible increase of scope of this ticket, perhaps we also want a better way to namespace the
init__orig,_modversions of variables.