Smtlib identifier difficulties

[philzook58]

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

cbat_tools/wp/lib/bap_wp/src/z3_utils.ml

Line 35 in 176753a

let var_name = String.strip ~drop:(fun c -> Char.(c = '|')) (Expr.to_string z3_var) in

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

cbat_tools/wp/lib/bap_wp/src/z3_utils.ml

Line 263 in 176753a

let pound_token = "MYSPECIALPOUND682" in

Here are possible suggestions both of which can be done at

cbat_tools/wp/lib/bap_wp/src/environment.ml

Line 111 in 176753a

let mk_z3_expr (ctx : Z3.context) ~name:(name : string) ~typ:(typ : Type.t) : Constr.z3_expr =

I believe:

• 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.