Status of the string theory

[felipeochoa]

Hi! I'm working on program verification/bug-finding and would like to use z3 as part of that. It seems that arithmetic and bit vectors get a lot of attention, so was curious to hear how robust the string solver in z3 is. Are the soundness bugs in the tracker relatively obscure corner cases, or is the theory still a little immature?

Thanks!

[NikolajBjorner]

Some comments:

There are two string solvers are available. seq (default) and z3str3.

First of all I do not advertise the seq solver as rock solid and certainly not scrutinized to the level of the arithmetic and bit-vector solvers.
It is also fairly complex given the many string operations being supported and the plethora
of case analyses considered by the string solver.

A good deal of the fuzz-bugs are about obscure corner cases,
but once in a while they point to flaws that could hurt realistic use cases.
Overall the fuzz-bugs are helping exposing the weaknesses and prepare the grounds for a
more reliable user experience, and generally I try to fast track user bugs over fuzz bugs
to unblock users.

[felipeochoa]

Thanks for the quick reply! For new projects would you recommend sticking with seq, or is z3str3 more future-proof?

Also, does z3 support unicode in strings?

[NikolajBjorner]

Switching between z3str3 and seq is just setting a configuration parameter.
I don't control the development of z3st3.

There are preliminary stubs for Unicode, but I don't want to switch until the solver for character classes is as efficient as what we have for ASCII.
It has also not been clear that Unicode is a strong priority: while it offers a sound basis for modeling characters it is also the case that many queries around string matching can be solved assuming ASCII and lifted to Unicode (@veanes).

[felipeochoa]

Re: unicode -- fwiw, our use case is probably in the world you describe: Concatenation + equality comparisons, with no unicode normalization.

For anyone else reading this, this works fine today in utf-8:

(declare-const a String)
(declare-const b String)
(assert (= a "$¢ह€"))
(assert (= (str.++ a b) "$¢ह€한𐍈"))
(check-sat)
(get-model)
;; returns
(
  (define-fun b () String
    "\\u{ffffffed}\\u{ffffff95}\\u{ffffff9c}\\u{fffffff0}\\u{ffffff90}\\u{ffffff8d}\\u{ffffff88}")
  (define-fun a () String
    "$\\u{ffffffc2}\\u{ffffffa2}\\u{ffffffe0}\\u{ffffffa4}\\u{ffffffb9}\\u{ffffffe2}\\u{ffffff82}\\u{ffffffac}")
)

It looks like strings are just treated as arrays of bytes, which is easy enough to encode where needed. I imagine there could be issues with the solver trying out invalid UTF-8 characters, though. I tested with UTF-32 (both BE and LE), which would eliminate these problems, but got some 'unexpected character' errors.

[NikolajBjorner]

It doesn't look right to me:

1. The parser is based on ASCII input assumption. If you want to pass unicode characters use the \u{...} escape conventions. Do not feed Z3 files with unicode characters. This is not supported (and I am weary about replacing char by wchar even though this is all 90's technology).
2. The default solver uses an 8 bit assumption. Characters encoded outside of the range are not really supported at the moment.

[pschanely]

Thanks for all this information!
I am also quite interested in unicode for CrossHair. I'd love to know a little more about your suggestion about "assuming ASCII and lifted to Unicode."

One challenge with using unicode-as-bytes under an encoding: it's hard to describe valid unicode strings simply. I've been considering using a sequence over 21-bit words:

• Then length works (at least in terms of codepoints)
• Constraining to valid code points (or unicode scalars) could be done with regular expression ranges. (regex seems to work in this case, but maybe there are gotchas?)

Do you think sounds like a good approach? I'd be happy to write up a little tutorial for others if so!

[NikolajBjorner]

I will be moving to unicode support pretty soon.

It is currently being tested. Once it is turned on by default users can enter unicode characters in ASCII strings
using the \u{XYZU} escapes defined in the SMTLIB2 specification for strings.

@mtrberzi - this is a good point to make sure theory_str works with the global option "unicode=true" from the command-line.

[mtrberzi]

That is a great point. I will work on the Unicode support for an upcoming PR. This should not be too much work, but there are a few places where we assume ASCII in legacy code and I will need to go through and make sure this is done properly.

[NikolajBjorner]

Unicode support is basically ready now.
Users just have to set the top-level configuration parameter unicode=true.
I would very soon want to do the following:

1. change internal representation for ASCII to the string theory custom type instead of bit-vectors.
2. change the default of unicode from "false" to "true".

It is clear that 2 breaks theory_str (it uses a character table and automata transitions based on 256 characters)
so setting smt.solver=z3str3 would have to be set together with unicode=false unless z3str3 is fixed.
It is also clear that 1 breaks theory_str_mc because it hard-wires dependency to bit-vectors at least 3 places.
It should have used the abstraction layer provided by seq_util to tell it what the character types are.

There is also a module called "seq_char" that handles character reasoning. It is basically equality reasoning for character and uses lazy bit-blasting to ensure bounds and comparisons between characters. It would be wise to use this layer. It already provides a 40% or so speedup in QF_SLIA benchmark sets over the bit-vector encoding even as it switches from ASCII to unicode that in the limit require 18 bits instead of 8.

I would therefore like to move on from the ASCII world and be SMTLIB2 compliant by default. Given the performance advantages, as well, I would flip the default for "unicode" from false to true by end of next week.

[mtrberzi]

Sounds good. I'll make the Unicode port a priority. I'm under a deadline for paper submission but I should be able to make good progress in the next week or so.

[pschanely]

Feel free to ask me to test things like the Python bindings!

[NikolajBjorner]

@schanely - currently the python and other bindings rely on ASCII re-encodings of strings.
String literals are converted into internal form using:

def StringVal(s, ctx=None):
    """create a string expression"""
    ctx = _get_ctx(ctx)
    return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx)

This function does not understand unicode characters. Z3 even crashed for this unit test:

from z3 import *
x = "$¢ह€"
s = Solver()
v = String('v')
s.add(v == x)
print(s.check())
print(s.model())

A different implementation of StringVal could avoid this by converting the argument 's' into an encoding.
For characters outside of the printable ASCII range it should use the escape sequence starting with \u{...}
as described in SMTLIB specification.

For example, if I add the line:

x = "".join(str(ch) if ord(ch) < 128 else "\\u{%x}" % (ord(ch)) for ch in x)

then x is translated correctly.
Using < 256 instead of 128 appears to have a subtle issue with backspace characters and string lengths, so even something as innocent as this piece can be tricky.
So a set of tests that also establish some more convenient ways to support strings for the APIs is certainly useful and so would fixing the python StringVal with something along the lines of what is proposed. If the proposed fix or a variant works for you, feel invited to add a pull request.

[NikolajBjorner]

I am adding this fixup for now. There are almost for sure a bunch of other issues.

[pschanely]

Fantastic; I'll try a build tomorrow at HEAD and see what else I notice. I imagine at a minimum something new needs to be done when fetching strings out of a model.

[pschanely]

Built and tried this out. At present, it looks like z3 is ignoring(?) the SMTLIB-escaping. Note here that it seems to think the length of this one character in python is 7 (which is the length of the SMTLIB string "\u{393}")

>>> len('\u0394')
1
>>> simplify(Length(StringVal('\u0394')))
7

I looks to me like Z3_mk_lstring doesn't expect escaping; it directly initializes zstring's buffer. The advantage of mk_lstring is that it handles null characters; but we could just handle those with unicode escapes as well? This delta seems to get things working for me; I'll submit a PR if you think it's reasonable:

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index dba147779..8371acd22 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10138,9 +10138,9 @@ def is_string_value(a):
 
 def StringVal(s, ctx=None):
     """create a string expression"""
-    s = "".join(str(ch) if ord(ch) < 128 else "\\u{%x}" % (ord(ch)) for ch in s)
+    s = "".join(str(ch) if 0 < ord(ch) < 128 else "\\u{%x}" % (ord(ch)) for ch in s)
     ctx = _get_ctx(ctx)
-    return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx)
+    return SeqRef(Z3_mk_string(ctx.ref(), s), ctx)
 
 def String(name, ctx=None):
     """Return a string constant named `name`. If `ctx=None`, then the global context is used.

[NikolajBjorner]

it is an internal issue: it adds an extra escape character into buffers when converting between string representations.

This now works:

from z3 import *
set_param(unicode=True)
print(len('\u0394'))
print(Length(StringVal('\u0394')))
print(simplify(Length(StringVal('\u0394'))))

[mtrberzi]

@NikolajBjorner is there any plan to make seq_char into something like a first-class theory solver for character equalities? The way it is used right now is a bit awkward to integrate directly into theory_str_mc because of the way the character equalities are handled in a subsolver (I would prefer not to pollute the top-level solver context with character terms that are temporary). It would be very handy if I could assert character (in)equalities directly to a subsolver and call solve() on that as I do now with the bit-vector terms.

I should be able to change the sort that is used for characters to the seq_util abstraction without much trouble. The hard-coded ASCII character set is actually dead code, I found (nothing uses it since I introduced theory_str_mc)

[NikolajBjorner]

A first class theory solver requires some more infrastructure and therefore cycles to implement.
It is a tradeoff between adding a few cases in the main solver.
I have for now converterd seq_char into theory_char so that it can act as a stand-alone solver once the surrounding infrastructure is ready.
However, this still requires work so I would propose a gradual porting guide. The changes to the main str theory solvers are relatively minor compared to the other functionality that goes into these.
You are obviously invited to also create the infrastructure for the character plugins and model value factories that are the remaining pieces, and post a pull request for this.

[NikolajBjorner]

the first-class theory_char is now in and ready to be combined with theory_str if you add it to smt_setup.cpp.
I plan to toggle the default by end of week to Unicode and probably disable the bit-vector representation
all-together to avoid maintaining multiple approaches. I presume this is fair given that you say theory_str does not have ASCII dependencies.

[mtrberzi]

That's great, thanks a lot. I have a unicode branch with the fixes for this that I will refactor to use theory_char. It should be simple, if I have done everything right.

[mtrberzi]

What does it mean when the model returned by the character theory contains terms like the following:

  ;; universe for Unicode:
  ;;   Unicode!val!1 Unicode!val!0 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Unicode!val!1 () Unicode)
  (declare-fun Unicode!val!0 () Unicode)
  ;; cardinality constraint:
  (forall ((x Unicode)) (or (= x Unicode!val!1) (= x Unicode!val!0)))
  ;; -----------
<snip>
  (define-fun char!tmp6 () Unicode
    Unicode!val!0)

For other character terms I see a "concrete" model, like:

  (define-fun char!tmp12 () Unicode
    (_ Char 98))

I am further seeing some strange "multiple definitions" like:

  (define-fun Char () Unicode
    (_ Char 98))
  (define-fun Char () Unicode
    (_ Char 97))

[NikolajBjorner]

(_ Char NNN) is the function that creates a constant of type Unicode.
It should not be mixed up with the SMTLIB2 version (_ char NNN), which returns a String.

Regarding the first model issue: Maybe you want to add a line in smt_setup.cpp to register theory_char whenever theory_str is registered.

[mtrberzi]

That is strange, because I do initialize the character solver in smt_setup when theory_str is set up. However, I am also invoking a subsolver with a new smt::kernel. This is where the char assertions get solved. If the char type is BV but I don't set the logic to QF_BV in the new kernel I don't get a model at all. I tried QF_BVRE because it has both bitvectors and sequences (therefore chars) but don't get a model this way either.

…

On Thu, Jan 28, 2021, 1:10 AM Nikolaj Bjorner, ***@***.***> wrote: (_ Char NNN) is the function that creates a constant of type Unicode. It should not be mixed up with the SMTLIB2 version (_ char NNN), which returns a String. Regarding the first model issue: Maybe you want to add a line in smt_setup.cpp to register theory_char whenever theory_str is registered. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#4939 (reply in thread)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAHZE6BUHB6E6AWCJC35Y2LS4EEXBANCNFSM4VZUOFJA> .

[mtrberzi]

If I can add something like setup_QF_CHAR() in smt_setup then I can PR right away. Since I can't know whether the characters are bitvectors or Unicode chars (for now) I need to make sure the subsolver loads them both. All this method will do is call setup_QF_BV() followed by setup_char(). When the bitvector representation (eventually) goes away completely then this can just change to calling setup_char().

[NikolajBjorner]

I added setup_char in f48fb8d
It does not prevent using bit-vectors so it is safe.

[mtrberzi]

Opened #4981