9 Strings and regular expressions🔗

Boogie has two built-in types that the language description does not mention at all: string and regex. They exist so that a Boogie program can reach the SMT-LIB theory of strings and regular expressions that Z3 and cvc5 implement. Boogie itself supplies almost nothing on top of them — there is a type, a literal syntax for strings, and equality. Every actual operation is obtained by declaring an uninterpreted function and tagging it with a :builtin attribute naming an SMT-LIB symbol.

The :builtin name is a string Boogie passes to the solver without looking at it, so almost nothing about a string program is checked until the solver sees it. The three files in Test/strings/ are, as of this writing, the entirety of the shipped documentation, and they use spellings that SMT-LIB 2.6 retired.

9.1 The string and regex types🔗

9.1.1 Syntax and resolution🔗

Neither string nor regex is a keyword, and no type production in Source/Core/BoogiePL.atg mentions either name. (The name string does occur in the grammar, but only as the name of the token for a string literal — see String literals.) TypeAtom lists three primitive types and nothing else:

TypeAtom<out Bpl.Type ty>

= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; .)

( "int"              (. ty = new BasicType(t, SimpleType.Int); .)

| "real"             (. ty = new BasicType(t, SimpleType.Real); .)

| "bool"             (. ty = new BasicType(t, SimpleType.Bool); .)

/* note: bitvectors and floats are handled in UnresolvedTypeIdentifier */

|

"("

Type<out ty>

")"

)

.

Note that the bitvector types are not there either, although the paper’s TypeAtom (§2.1) lists them; the comment in the production says where they went. real is in the production and is not in the paper.

A type written string or regex parses through the Ident alternative of Type as an UnresolvedTypeIdentifier, exactly like a user-declared type constructor. It is UnresolvedTypeIdentifier.ResolveType in Source/Core/AST/AbsyType.cs that turns the name into a type, and it does so before it consults any type binder, synonym or constructor: the order is bitvector types, float types, rmode, string, regex, then type variables, then user declarations. Applying either name to type arguments is an error (string type must not be applied to arguments).

Two consequences follow, and both are surprising.

First, string and regex remain ordinary identifiers everywhere else: var string: int; and var regex: bool; are legal global declarations, and a program that uses them verifies.

Second, you may declare a type synonym or a type constructor with either name; because resolution consults the built-in names first, the declaration has no effect on what the name means, and there is no way to shadow the built-in meaning:

type string = int;

type regex;

procedure main()

{

var s: string;

s := 3;

}

boogie shadow.bpl

shadow.bpl(7,2): Error: mismatched types in assignment command (cannot assign int to string)

1 type checking errors detected in shadow.bpl

The synonym type string = int was accepted, and then var s: string resolved to the built-in string type anyway.

9.1.2 What the language gives you🔗

Values of type string and regex are first-class in every structural sense. They may be the type of a local, a global, an in- or out-parameter, a const (including unique), a function argument or result, a map domain or range, or a quantified variable; they may be instantiated for a type parameter; and they participate in axioms and triggers like any other type.

What they do not have is operators. The only Boogie operations on string and regex are equality and disequality, plus the constructs that work at any type: if-then-else, map select and update, old, assignment and havoc. There is no concatenation operator, no ordering, no indexing, and no literal syntax for regex at all.

procedure main(a: string, b: string)

{

assert a + b == a;

}

no-operators.bpl(3,11): Error: invalid argument types (string and string) to binary operator +

1 type checking errors detected in no-operators.bpl

Everything structural works as expected:

function {:builtin "str.len"} len(string): int;

function {:builtin "str.++"} concat(string, string): string;

const greeting: string;

axiom greeting == concat("hello, ", "world");

var table: [string]int;

function short(s: string): bool;

axiom (forall s: string :: { short(s) } short(s) <==> len(s) < 5);

procedure main(a: string, b: string) returns (r: regex)

requires len(a) == 2 && len(b) == 2;

modifies table;

{

var s: string;

s := concat(a, b);

assert s != "";

assert short(s) == (len(s) < 5);

assert len(greeting) == 12;

table[greeting] := 1;

assert table["hello, world"] == 1;

}

Boogie program verifier finished with 1 verified, 0 errors

9.1.3 How the types reach the solver🔗

SMTLibExprLineariser.TypeToString maps string to the SMT-LIB sort String and regex to (RegEx String). Both are built-in sorts, so no declare-sort is emitted. For

function {:builtin "str.++"}    concat(string, string): string;

function {:builtin "str.to_re"} toRe(string): regex;

function {:builtin "re.none"}   none(): regex;

function {:builtin "str.in_re"} inRe(string, regex): bool;

procedure main(s: string, r: regex)

{

assert !inRe(concat(s, "cd"), none()) || r == toRe("x");

}

boogie /proverLog:encoding.smt2 encoding.bpl

the generated query contains

(declare-fun s () String)

(declare-fun r () (RegEx String))

...

(or (not (str.in_re (str.++ s "cd") re.none)) (= r (str.to_re "x")))

Note (RegEx String): that is Z3’s spelling of the regular-expression sort, which SMT-LIB 2.6 names RegLan. It is the spelling any solver driven by Boogie has to accept — see Portability to other solvers.

9.2 String literals🔗

9.2.1 The token🔗

The literal token is defined in Source/Core/BoogiePL.atg:

quote = '"'.

newLine = cr + lf.

regularStringChar = ANY - quote - newLine.

...

string = quote { regularStringChar | "\\\"" } quote.

"\\\"" is Coco/R’s notation for the two-character sequence \". So a string literal is a double quote, then any number of characters other than a double quote or a line break (a backslash included), possibly interspersed with the two-character sequence \", then a closing double quote.

A literal may not span lines, and there is no line continuation:

procedure main()

{

var s: string;

s := "a

b";

}

newline.bpl(4,8): error: invalid UnaryExpression

1 parse errors detected in newline.bpl

9.2.2 There are no escape sequences🔗

\" is the only sequence the token grammar recognises, and even it is not decoded. The parser builds the literal’s value with

| string                  (. e = new LiteralExpr(t, t.val.Trim('"')); .)

— it takes the raw token text and strips quote characters off both ends. Nothing is unescaped. A backslash in the source is a backslash in the value.

function {:builtin "str.len"} len(string): int;

procedure main()

{

assert len("") == 0;

assert len("hello, world") == 12;

assert len("a b\tc") == 6;      // no \t escape: backslash and t are two characters

assert len("a\\b") == 4;        // no \\ escape: two backslashes

assert len("\"") == 1;          // NOT a quote: the value is a single backslash

}

Boogie program verifier finished with 1 verified, 0 errors

All five assertions hold. The last one repays a second reading: "\"" is a one-character string whose one character is a backslash. Trim(’"’) removes every leading and trailing quote character, so the quote written after the backslash goes with the closing delimiter.

9.3 Reaching the string theory: :builtin🔗

9.3.1 Mechanics🔗

Declare an uninterpreted function whose signature matches the SMT-LIB operation and attach :builtin with the SMT-LIB name. At translation time SMTLibExprLineariser.ExtractBuiltin reads the attribute; if it is present, the function is not declared to the solver and every application is emitted as an application of the named symbol. The Boogie-level name of the function is irrelevant to the solver, so you may call it whatever you like and may declare the same builtin under several names and several signatures.

Four details of the emission matter.

• SMTLibOpLineariser.WriteApplication writes the attribute string verbatim into the head position of the application, with an open parenthesis before it and the arguments after. The name therefore need not be a single symbol: an indexed identifier such as (_ re.loop 1 3) is accepted and comes out as ((_ re.loop 1 3) arg). That is the only way to reach SMT-LIB’s indexed string operators — see Indexed operators.

• A nullary builtin function is emitted without parentheses, as a bare symbol. This is what makes function {:builtin "re.none"} none(): regex; work: none() becomes re.none, not (re.none), which the solver would reject. You must still write the empty argument list at the Boogie call site — none without parentheses is an identifier, and resolution fails with undeclared identifier: none.

• Arity is taken from your declaration, so a variadic SMT-LIB operator can be declared at whatever arity you need. function {:builtin "str.++"} concat3(string, string, string): string; emits a three-argument str.++ and the solver accepts it.

• :bvbuiltin is checked before :builtin and is not restricted to bitvectors, so :bvbuiltin "str.len" behaves identically to :builtin "str.len". Use :builtin for string operations.

9.3.2 Nothing about the name is validated🔗

Boogie never inspects a :builtin string. It does not know which SMT-LIB symbols exist, what arities they take, or what sorts they have, so a name the solver does not recognise, or one applied at an arity or sort it does not accept, is diagnosed by the solver rather than by Boogie.

The line and column in such a message are positions in the SMT-LIB text Boogie pipes to the solver’s standard input (Z3 is run as z3 -smt2 -in), not positions in your Boogie source. /proverLog:file writes out that text; search it for the offending symbol.

9.3.3 Where :builtin applies🔗

ExtractBuiltin is consulted for Function declarations only, so that is where :builtin names an SMT-LIB operation. On a constant it has no effect: the constant is emitted as an ordinary uninterpreted symbol. Declare a nullary function instead.

On a type constructor, :builtin marks a sort that is built into SMT-LIB and therefore needs no declare-sort. The name Boogie renders this way is Seq, which is how the standard library reaches the SMT sequence theory (The standard library); the string sorts are reached through the type names string and regex.

9.4 String operations🔗

The table gives every string operation of the SMT-LIB 2.6 Unicode Strings theory, with the Boogie signature to declare for each. (str.to_re and str.in_re are string operations too, but they are listed with the regular-expression operators in the next section.) Indices are zero-based; every operation is total, and out-of-range behaviour is described in Corner cases of the SMT semantics.

All of them except the two str.replace_re operations verify with the bundled Z3 5.0.0:

function {:builtin "str.++"}         concat(string, string): string;

function {:builtin "str.len"}        len(string): int;

function {:builtin "str.at"}         at(string, int): string;

function {:builtin "str.substr"}     substr(string, int, int): string;

function {:builtin "str.prefixof"}   prefixOf(string, string): bool;

function {:builtin "str.suffixof"}   suffixOf(string, string): bool;

function {:builtin "str.contains"}   contains(string, string): bool;

function {:builtin "str.indexof"}    indexOf(string, string, int): int;

function {:builtin "str.replace"}    replace(string, string, string): string;

function {:builtin "str.replace_all"} replaceAll(string, string, string): string;

function {:builtin "str.is_digit"}   isDigit(string): bool;

function {:builtin "str.to_code"}    toCode(string): int;

function {:builtin "str.from_code"}  fromCode(int): string;

function {:builtin "str.to_int"}     toInt(string): int;

function {:builtin "str.from_int"}   fromInt(int): string;

function {:builtin "str.<"}          strLt(string, string): bool;

function {:builtin "str.<="}         strLe(string, string): bool;

procedure main()

{

assert concat("ab", "cd") == "abcd";

assert len("abcd") == 4;

assert at("abcd", 2) == "c";

assert substr("abcd", 1, 2) == "bc";

assert prefixOf("ab", "abcd");

assert suffixOf("cd", "abcd");

assert contains("abcd", "bc");

assert indexOf("abcdabcd", "cd", 3) == 6;

assert replace("aaa", "a", "b") == "baa";

assert replaceAll("aaa", "a", "b") == "bbb";

assert isDigit("4") && !isDigit("x");

assert toCode("a") == 97;

assert fromCode(97) == "a";

assert toInt("42") == 42;

assert fromInt(42) == "42";

assert strLt("a", "b") && strLe("a", "a");

}

Boogie program verifier finished with 1 verified, 0 errors

str.replace_re and str.replace_re_all are the exception, and a sharp one: Z3 5.0.0 gives up on them even when every argument is a literal.

function {:builtin "str.replace_re"}     replaceRe(string, regex, string): string;

function {:builtin "str.replace_re_all"} replaceReAll(string, regex, string): string;

function {:builtin "str.to_re"}          toRe(string): regex;

procedure main()

{

assert replaceRe("aaa", toRe("a"), "b") == "baa";

assert replaceReAll("aaa", toRe("a"), "b") == "bbb";

}

Prover error: Unexpected prover response (getting info about 'unknown' response): (:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory seq))")

replace-re.bpl(5,11): Verification inconclusive (main)

Boogie program verifier finished with 0 verified, 0 errors, 1 inconclusive

The same file verifies under cvc5 1.3.3 (Portability to other solvers), so this is a Z3 limitation rather than anything Boogie does. cvc5 also confirms the asymmetry between the two: the empty match counts for str.replace_re and does not for str.replace_re_all, so replaceRe("abc", toRe(""), "X") is "Xabc" while replaceReAll("abc", toRe(""), "X") is "abc".

9.5 Regular-expression operations🔗

A regex value denotes a set of strings. There is no literal syntax; every regular expression is built by applying builtin functions, starting from str.to_re (the language containing exactly one string) or one of the constants.

Every regular-expression operator of the SMT-LIB 2.6 Unicode Strings theory is there; the three-argument re.loop row is a Z3 extension on top of it. The two indexed rows are explained in Indexed operators.

function {:builtin "str.to_re"}  toRe(string): regex;

function {:builtin "str.in_re"}  inRe(string, regex): bool;

function {:builtin "re.none"}    none(): regex;

function {:builtin "re.all"}     all(): regex;

function {:builtin "re.allchar"} allchar(): regex;

function {:builtin "re.++"}      reConcat(regex, regex): regex;

function {:builtin "re.union"}   reUnion(regex, regex): regex;

function {:builtin "re.inter"}   reInter(regex, regex): regex;

function {:builtin "re.*"}       star(regex): regex;

function {:builtin "re.+"}       plus(regex): regex;

function {:builtin "re.opt"}     opt(regex): regex;

function {:builtin "re.comp"}    comp(regex): regex;

function {:builtin "re.diff"}    diff(regex, regex): regex;

function {:builtin "re.range"}   range(string, string): regex;

function {:builtin "re.loop"}    loop(regex, int, int): regex;

procedure main()

{

assert inRe("abcd", toRe("abcd"));

assert !inRe("abcd", toRe("ABCD"));

assert !inRe("abcd", none());

assert inRe("abcd", all());

assert inRe("a", allchar()) && !inRe("ab", allchar());

assert inRe("ab", reConcat(toRe("a"), toRe("b")));

assert inRe("a", reUnion(toRe("a"), toRe("b")));

assert !inRe("a", reInter(toRe("a"), toRe("b")));

assert inRe("", star(toRe("a"))) && inRe("aaa", star(toRe("a")));

assert !inRe("", plus(toRe("a"))) && inRe("aaa", plus(toRe("a")));

assert inRe("", opt(toRe("a"))) && inRe("a", opt(toRe("a")));

assert inRe("b", comp(toRe("a")));

assert !inRe("a", diff(all(), toRe("a")));

assert inRe("c", range("a", "z")) && !inRe("C", range("a", "z"));

assert range("ab", "z") == none();   // non-singleton bounds give the empty language

assert inRe("aaa", loop(toRe("a"), 1, 3)) && !inRe("aaaa", loop(toRe("a"), 1, 3));

}

Boogie program verifier finished with 1 verified, 0 errors

The re.loop row above is Z3’s three-argument extension, and it is not SMT-LIB. Read the next subsection before using it.

9.5.1 Indexed operators🔗

In SMT-LIB 2.6 bounded repetition is an indexed operator: the bounds sit inside the identifier, as ((_ re.loop i n) r), and re.^ exists only in that form. Z3 additionally accepts re.loop as an ordinary three-argument function, which is what Test/strings/ uses and what the table above records.

You do not have to settle for the extension. Because the :builtin string goes into the head position unchanged, the whole indexed identifier can be put inside it. The index is then fixed at declaration time, so you need one Boogie function per index — but the result is standard SMT-LIB, and it is the only route to re.^:

// The whole indexed identifier goes inside the :builtin string.

function {:builtin "(_ re.loop 1 3)"} loop13(regex): regex;

function {:builtin "(_ re.^ 2)"}      pow2(regex): regex;

function {:builtin "str.to_re"} toRe(string): regex;

function {:builtin "str.in_re"} inRe(string, regex): bool;

procedure main()

{

assert inRe("aaa", loop13(toRe("a"))) && !inRe("aaaa", loop13(toRe("a")));

assert inRe("aa", pow2(toRe("a"))) && !inRe("aaa", pow2(toRe("a")));

}

Boogie program verifier finished with 1 verified, 0 errors

The query contains ((_ re.loop 1 3) (str.to_re "a")), and cvc5 verifies the same file unchanged — which the three-argument form does not (Portability to other solvers).

9.6 Legacy and standard spellings🔗

The tests in Test/strings/ predate SMT-LIB 2.6 and use spellings the standard has since replaced. Z3 still accepts the old names as aliases, so the shipped tests pass, but new code should use the standard names.

Z3 5.0.0 treats each pair as the same operation, which the solver will prove for you:

// Pre-2.6 spellings.  Z3 still accepts them; other solvers may not.

function {:builtin "str.to.int"}  toIntOld(string): int;

function {:builtin "int.to.str"}  fromIntOld(int): string;

function {:builtin "str.to.re"}   toReOld(string): regex;

function {:builtin "str.in.re"}   inReOld(string, regex): bool;

function {:builtin "re.nostr"}    noneOld(): regex;

function {:builtin "str.indexof"} indexOf2(string, string): int;

// The 2.6 spellings of the same operations.

function {:builtin "str.to_int"}  toInt(string): int;

function {:builtin "str.from_int"} fromInt(int): string;

function {:builtin "str.to_re"}   toRe(string): regex;

function {:builtin "str.in_re"}   inRe(string, regex): bool;

function {:builtin "re.none"}     none(): regex;

function {:builtin "str.indexof"} indexOf3(string, string, int): int;

procedure main(s: string, t: string)

{

assert toIntOld(s) == toInt(s);

assert fromIntOld(3) == fromInt(3);

assert toReOld(s) == toRe(s);

assert inReOld(s, toRe(t)) == inRe(s, toReOld(t));

assert noneOld() == none();

assert indexOf2(s, t) == indexOf3(s, t, 0);

}

Boogie program verifier finished with 1 verified, 0 errors

Because Boogie passes the name straight through, the choice of spelling is purely a portability decision — and not a hypothetical one. cvc5 rejects all four dotted names as undeclared symbols, and rejects the two-argument str.indexof on arity (Terms with kind STRING_INDEXOF must have at least 3 children and at most 3 children (the one under construction has 2)). See Portability to other solvers.

9.7 Corner cases of the SMT semantics🔗

Boogie contributes nothing to the meaning of these operations, so the semantics are SMT-LIB’s. They are total: there are no partial functions and no well-formedness proof obligations, and out-of-range arguments produce designated values rather than errors. The following all verify.

function {:builtin "str.at"}       at(string, int): string;

function {:builtin "str.substr"}   substr(string, int, int): string;

function {:builtin "str.indexof"}  indexOf(string, string, int): int;

function {:builtin "str.to_int"}   toInt(string): int;

function {:builtin "str.from_int"} fromInt(int): string;

function {:builtin "str.to_code"}  toCode(string): int;

function {:builtin "re.range"}     range(string, string): regex;

function {:builtin "re.none"}      none(): regex;

procedure main()

{

// Out-of-range indices give the empty string, never an error.

assert at("abc", 9) == "" && at("abc", -1) == "";

assert substr("abc", 5, 2) == "";

assert substr("abc", 1, 99) == "bc";

assert substr("abc", 1, -1) == "";

// str.indexof yields -1 when the needle is absent or the offset is out of range,

// and the offset itself when the needle is empty.

assert indexOf("abc", "z", 0) == -1;

assert indexOf("abc", "a", 9) == -1;

assert indexOf("abc", "", 1) == 1;

// str.to_int is -1 for anything that is not a non-empty sequence of digits,

// including negative-looking strings.

assert toInt("007") == 7;

assert toInt("") == -1;

assert toInt("-1") == -1;

assert toInt("1a") == -1;

// str.from_int is the empty string for negative arguments.

assert fromInt(-5) == "";

// str.to_code is -1 unless the argument has length one.

assert toCode("ab") == -1 && toCode("") == -1;

// re.range with bounds that are not single characters is the empty language.

assert range("ab", "z") == none();

assert range("z", "a") == none();

}

Boogie program verifier finished with 1 verified, 0 errors

Note in particular that str.to_int does not distinguish failure from the value -1, and that str.from_int is not its inverse: fromInt(toInt(s)) == s is false for any s that is not a canonical digit string.

9.8 Reasoning about strings🔗

9.8.1 Incompleteness is normal🔗

The SMT theory of strings is undecidable in general, and Z3’s solver for it is incomplete. A string query the solver gives up on does not produce a counterexample; it produces Verification inconclusive, a distinct outcome from an error. The solver’s stated reason is printed with it, on a Prover error: line; that line is unconditional — /proverWarnings governs Prover warning: messages only.

function {:builtin "str.replace_all"} replaceAll(string, string, string): string;

function {:builtin "str.len"} len(string): int;

procedure main(s: string)

requires len(s) == 3;

{

assert len(replaceAll(s, "a", "bb")) >= 3;

}

boogie inconclusive.bpl

Prover error: Unexpected prover response (getting info about 'unknown' response): (:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory seq))")

inconclusive.bpl(4,11): Verification inconclusive (main)

Boogie program verifier finished with 0 verified, 0 errors, 1 inconclusive

The assertion is true. Symbolic arguments to the more intricate string operations — str.replace_all above — are one way to reach this state.

9.8.2 Counterexample models🔗

String values appear in printed models, in the solver’s own syntax:

function {:builtin "str.len"} len(string): int;

procedure main(s: string)

requires len(s) == 2;

{

assert s == "ab";

}

boogie /printModel:1 model.bpl

model.bpl(6,3): Error: this assertion could not be proved

Execution trace:

model.bpl(6,3): anon0

*** MODEL

s -> ("BA")

ControlFlow -> {

0 0 -> 3

0 2 -> (- 1)

0 3 -> 2

else -> (- 1)

}

tickleBool -> {

false -> true

true -> true

else -> true

}

*** STATE <initial>

s -> ("BA")

*** END_STATE

*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error

The value is printed with the solver’s parentheses and quoting; Boogie does not translate it back into Boogie literal syntax.

9.8.3 Quantifiers and triggers🔗

Quantification over string and regex works normally and needs the same care with triggers as any other type. A builtin application is a legal trigger term, with one wrinkle: a trigger on len(s) matches len(s) for a symbolic s and does not match len("abc"). The query Boogie generates does contain (marker (str.len "abc")) and the pattern (str.len s); the solver folds the ground application away before the pattern can match it.

function {:builtin "str.len"} len(string): int;

function marker(int): bool;

axiom (forall s: string :: { len(s) } marker(len(s)));

procedure symbolic(s: string) { assert marker(len(s)); }

procedure ground()            { assert marker(len("abc")); }

trigger-folding.bpl(7,33): Error: this assertion could not be proved

Execution trace:

trigger-folding.bpl(7,33): anon0

Boogie program verifier finished with 1 verified, 1 error

9.9 Portability to other solvers🔗

Boogie can drive cvc5 with /proverOpt:SOLVER=cvc5. Doing so shows exactly which parts of Boogie’s string support are Z3-specific. The runs below use cvc5 1.3.3.

The standard string operations are portable: the str.* example above verifies unchanged.

boogie /proverOpt:SOLVER=cvc5 /proverOpt:PROVER_PATH=.../cvc5 string-ops.bpl

Boogie program verifier finished with 1 verified, 0 errors

So does the str.replace_re example, which Z3 5.0.0 could not decide:

boogie /proverOpt:SOLVER=cvc5 /proverOpt:PROVER_PATH=.../cvc5 replace-re.bpl

Boogie program verifier finished with 1 verified, 0 errors

The legacy spellings are not portable at all:

boogie /proverOpt:SOLVER=cvc5 /proverOpt:PROVER_PATH=.../cvc5 legacy-spellings.bpl

Prover error: Parse Error: <stdin>:17.107: Symbol 'str.to.int' not declared as a variable

Advisory: main SKIPPED due to I/O exception: Pipe is broken.

legacy-spellings.bpl(17,11): Verification encountered solver exception (main)

Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions

Neither is re.loop in its three-argument form:

boogie /proverOpt:SOLVER=cvc5 /proverOpt:PROVER_PATH=.../cvc5 regex-ops.bpl

Prover error: Parse Error: <stdin>:15.2531: Symbol 're.loop' not declared as a variable

Advisory: main SKIPPED due to I/O exception: Pipe is broken.

regex-ops.bpl(17,11): Verification encountered solver exception (main)

Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions

Replacing that declaration with the standard indexed spelling of Indexed operators — function {:builtin "(_ re.loop 1 3)"} loop13(regex): regex; — makes the whole file portable:

boogie /proverOpt:SOLVER=cvc5 /proverOpt:PROVER_PATH=.../cvc5 regex-ops-indexed.bpl

Boogie program verifier finished with 1 verified, 0 errors

With re.loop either removed or written in indexed form, every regular-expression operator in the table verifies under cvc5. What does not survive is any program that mentions the regex type where a sort must be written down — a regex variable, parameter, constant or map component — because Boogie writes that sort as Z3’s (RegEx String) rather than SMT-LIB 2.6’s RegLan:

boogie /proverOpt:SOLVER=cvc5 /proverOpt:PROVER_PATH=.../cvc5 encoding.bpl

Prover error: Parse Error: <stdin>:14.32: Symbol 'RegEx' not declared as a type

Advisory: main SKIPPED due to I/O exception: Pipe is broken.

encoding.bpl(6,11): Verification encountered solver exception (main)

Boogie program verifier finished with 0 verified, 0 errors, 1 solver exceptions

A regular-expression program that never stores a regex in a named symbol is portable, because every regex term is then an application that gets inlined and no sort declaration is needed.

The Lean back end does not support either type:

boogie /noVerify /printLean:- string-ops.bpl

Failed translation: (0,0): Unsupported type: String.

9.10 Divergences from This is Boogie 2🔗

This is Boogie 2 does not describe strings, and says so explicitly. Introducing StringLiteral as the terminal used for attribute arguments in §11 it remarks:

“Note that string literals are not used anywhere else in Boogie.”

That is no longer true: the same token is now an atomic expression of type string. The paper’s TypeAtom production (§2.1) lists bool, int and the bitvector types; the implementation’s lists bool, int and real. Neither the bitvector types nor string, regex, rmode and the float types are in the parser’s TypeAtom at all — all of them are recognised during name resolution instead. The rest of the paper applies unchanged: strings are an ordinary type in the sense of §2, values of different types are disjoint, and :builtin is an instance of the tool directives of §11, to which “the Boogie language does not assign any formal meaning”.