OSTRICH

An SMT Solver for String Constraints

OSTRICH is an automata-based SMT solver for string constraints.

The theory behind OSTRICH is explained in the slides of our POPL'24 tutorial.

Using Ostrich

After installing the Scala Build tool (SBT), you can assemble a JAR file using sbt assembly. To run it, use either the ostrich script in the root folder, or ostrich-client. The latter transparently spins up a server that continuously serves requests from the client script; useful to avoid cold-starting the JVM if you are running many instances.

In general, OSTRICH supports all options of the Princess SMT solver, which can be displayed with ./ostrich -h.

There are some additional string-specific options offered by OSTRICH:

Option	Explanation
`[+-]cea`	Use the cost-enriched automata back-end instead of the standard back-end. Default: `-cea`
`-portfolio=strings`	Use a portfolio of different string solving configurations. Disabled by default.
`[+-]forwardPropagation`	Forward propagation of regular expression constraints. Default: `-forwardPropagation`
`[+-]backwardPropagation`	Backward propagation of regular expression constraints. Default: `+backwardPropagation`
`[+-]nielsenSplitter`	Splitting of equations using Nielsen transformation. Default: `+nielsenSplitter`
`-length=[on,off,auto]`	Switch length reasoning on or off. Default: `-length=auto`
`[+-]parikh`	Introduce letter count equations for all letters that occur in a problem. Default: `-parikh`
`[+-]minimizeAutomata`	Eager minimization of automata. Default: `-minimizeAutomata`
`[+-]eager`	Eager intersection of regular expression constraints. Default: `-eager`

Web Interface

For experiments, OSTRICH can also be used through its web interface.

Input Format

OSTRICH accepts constraints written using the SMT-LIB theory of strings.

In addition to the standardized SMT-LIB operators, OSTRICH can handle a number of further functions.

Additional string functions

Name	Explanation
str.reverse	Reverse a string

Unary transducers

Finite-state transducers are a general way to introduce further string functions. Examples of functions that can be represented as transducers are encoders, decoders, extraction of sub-strings, removal of white-space characters, etc.

Finite-state transducers can be defined as (mutually) recursive functions, see this file for an example.

It is also possible to use prioritised finite-state transducers: multiple outgoing transitions from a state can be given priorities, and the transducer will take the transition with highest priority that will lead to a successful run. See this file for an example.

Additional regular expression constructors

Name	Explanation
re.from_ecma2020	Parse a regular expression in textual ECMAScript 2020 format (example)
re.from_ecma2020_flags	Parse a regular expression in textual ECMAScript 2020 format, with a second argument to specify flags (example)
re.case_insensitive	Make any regular expression case insensitive (example)
re.from_automaton	Parse a finite-state automaton (example)

Handling of capture groups

OSTRICH can also process regular expressions that include capture groups, lazy quantifiers, and anchors. For this functionality, OSTRICH understands a number of additional regular expression operators:

Name	Explanation
re.*?	Non-greedy star: similar to re.* but matching as few characters as possible
re.+?	Non-greedy plus
re.opt?	Non-greedy option
(_ re.loop? a b)	Non-greedy loop
(_ re.capture n)	Capture group with index n
(_ re.reference n)	Reference to the contents of capture group n
re.begin-anchor	The anchor ^
re.end-anchor	The anchor $

Such augmented regular expressions can be used in combination with several new string functions. Those functions support in particular capture groups and references in the replacement strings:

Name	Explanation
(_ str.extract n)	Extract the contents of the n'th capture group (example)
str.replace_cg	Replace the first match of a regular expression (example)
str.replace_cg_all	Replace all matches of a regular expression (example)

GraalVM Native Image

OSTRICH can optionally be built as a native executable using GraalVM Native Image.
This can significantly reduce JVM startup overhead.

Prerequisites

GraalVM (JDK 24 or newer) with native-image installed
sbt

If GraalVM was installed via SDKMAN!:

export GRAALVM_HOME="$HOME/.sdkman/candidates/java/current"
export PATH="$GRAALVM_HOME/bin:$PATH"
native-image --version

If native-image is missing:

gu install native-image

Building the native executable

Generate reachability metadata by running OSTRICH with the tracing agent:

sbt 'set Compile / run / javaOptions += "-agentlib:native-image-agent=config-merge-dir=src/main/resources/META-INF/native-image/uuverifiers/ostrich"' \
    'run tests/adt.smt2'

This generates or updates:

src/main/resources/META-INF/native-image/uuverifiers/ostrich/reachability-metadata.json

You may be required to run this tracing agent on multiple files and with different flags to ensure that the entire code base is covered (The current metadata should contain all relevant classes).

Build the native executable:

sbt nativeImage

Build a fully static Linux executable:

Supported platform: Linux x86_64
Required in addition to the prerequisites above: a 64-bit musl toolchain with zlib on PATH

The release workflow in this repository installs that toolchain automatically. For a local build, follow the GraalVM static linking guide and install a musl toolchain first, for example:

curl -SLO https://gds.oracle.com/download/bfs/archive/musl-toolchain-1.2.5-oracle-00001-linux-amd64.tar.gz
tar xzf musl-toolchain-1.2.5-oracle-00001-linux-amd64.tar.gz
export PATH="$(pwd)/musl-toolchain/bin:$PATH"

Then build the binary with:

OSTRICH_STATIC_NATIVE_IMAGE=true sbt nativeImage

This toggle only enables GraalVM's --static --libc=musl options. It does not install GraalVM, native-image, or the musl toolchain for you. The same flag can be enabled via sbt -Dostrich.staticNativeImage=true nativeImage.

To verify that the result is fully static, run:

ldd target/native-image/ostrich

For a fully static binary, ldd should report not a dynamic executable. Static linking is only supported for Linux builds; on macOS and Windows use the regular sbt nativeImage build instead.

uuverifiers / ostrich 2.0