9.1.1Integer and Real Theories🔗 i

Rosette supports assertions and assumptions containing symbolic values of integer or real type. But solving queries with these types is expensive (or, in the worst case, undecidable), and even simple queries can be unacceptably slow.

One solution is to change Rosette’s current-bitwidth parameter, which controls the reasoning precision used for queries. When current-bitwidth is set to a value k other than #f, Rosette approximates integer? and real? values using signed k-bit bitvector s, which can make queries involving integers and reals faster to solve.

But this approximation is unsound and may produce results that are incorrect under the infinite-precision semantics of integers and reals (while being correct under the finite-precision semantics). For example, this program incorrectly says that no integer greater than 15 exists, because the setting of current-bitwidth causes it to consider only values of x that can be represented as a 5-bit bitvector.

> (current-bitwidth 5)

> (define-symbolic xinteger? )

> (solve (assert (> x15)))

(unsat)

So, choosing the right reasoning precision for an application involves navigating this tradeoff between performance and soundness.

9.1.2Algorithmic Mismatch🔗 i

Small algorithmic changes can have a large impact on the efficiency of symbolic evaluation. Often, the most efficient algorithm for symbolic inputs is different to the most efficient one for concrete inputs—an algorithmic mismatch.

For example, consider this function to set the idxth element of a list lst to val:

> (define (list-setlstidxval)

(let-values ([(frontback)(split-at lstidx)])

(append front(cons val(cdr back)))))

> (list-set'(abc)1'd)

'(a d c)

While appropriate for concrete inputs, this function exhibits poor performance when the inputs are symbolic:

> (define-symbolic idxleninteger? )

> (define lst(take '(abc)len))

> (list-setlstidx'd);Symbolic union with 6 parts.

(union #:size 6 #:hash -437123915298968900)

The root cause is the split-at operation, which separates the front and back of the list into different variables. Because the index idx to split at is symbolic, Rosette creates two symbolic unions to capture the possible front and back values as a function of idx. Even though the possible values of front and back are related, this separation loses the relationship.

A better implementation for symbolic inputs avoids splitting the list by iterating over it, updating each position depending on whether its index is equal to idx:

> (define (list-set*lstidxval)

(for/all ([lstlst])

(map (lambda (iv)(if (= idxi)valv))

(build-list (length lst)identity )

lst)))

> (list-set*'(abc)1'd)

'(a d c)

> (list-set*lstidx'd);Smaller symbolic union with 4 parts.

(union #:size 4 #:hash -976833215883912073)

9.1.3Irregular Representation🔗 i

Just as the best algorithm for symbolic inputs can differ from that for concrete inputs (an algorithmic mismatch), so can the best data structure. Programming with symbolic values is most efficient when data structures are regular. Even though an irregular representation may be more space efficient for concrete data, it can have negative performance impacts when the data is symbolic.

For example, consider representing a (mutable) 2D grid data structure using Rosette’s lifted support for vectors. The obvious representation is to use nested vectors to represent the two dimensions:

> (define-values (widthheight)(values 55))

> (define-symbolic xyinteger? )

> (define grid/2d

(for/vector ([_ height])

(make-vector width#f)))

> (vector-set! (vector-ref grid/2dy)x'a)

This representation is inefficient when indexed with symbolic values, because the dereferences are irregular: the dereference of the y-coordinate returns a vector, whereas the dereference of the x-coordinate returns a value. This irregularity requires Rosette to perform more symbolic evaluation work to faithfully track the usages of the nested vector.

An alternative representation stores the entire grid in one vector, indexed using simple arithmetic:

> (define grid/flat

(make-vector (* widthheight)#f))

> (vector-set! grid/flat(+ (* ywidth)x)'a)

This variant improves performance by about 2×.

9.1.4Missed Concretization🔗 i

In addition to employing careful algorithmic and representational choices, fast solver-aided code provides as much information as possible about the feasible choices of symbolic values. Failure to make this information explicit results in missed concretization opportunities, leading to performance degradation.

For example, consider the following toy procedure, that returns the idxth element of the list lst, but only if idx is 0 or 1:

> (define (maybe-reflstidx)

(if (<= 0idx1)

(list-ref lstidx)

-1))

> (define-symbolic idxinteger? )

> (maybe-ref'(567)idx)

(ite

(&& (<= 0 idx) (<= idx 1))

(ite* (⊢ (= 0 idx) 5) (⊢ (= 1 idx) 6) (⊢ (= 2 idx) 7))

-1)

This procedure has poor performance when given a symbolic index idx, because the call to (list-ref lstidx) passes a symbolic index, but the conditional establishes that the only possible values for that index are 0 or 1. When Rosette evaluates the first side of the conditional, it does not simplify the value of idx to be only 0 or 1, and so the resulting encoding creates infeasible branches for cases where idx is outside that range. An alternative version captures that concreteness:

> (define (maybe-ref*lstidx)

(cond [(= idx0)(list-ref lst0)]

[(= idx1)(list-ref lst1)]

[else -1]))

> (maybe-ref*'(567)idx)

(ite (= 0 idx) 5 (ite (= 1 idx) 6 -1))

This variant avoids generating infeasible return values for the cases where idx is greater than 1.

9.2.1Options and Caveats🔗 i

By default, the symbolic profiler instruments only code that is within a module whose initial module path is either rosette or rosette/safe. In other words, only files beginning with #lang rosette or #lang rosette/safe will be instrumented. To instrument all code, use the --racket flag described below.

Similarly, by default, the symbolic profiler instruments only code that does not belong to installed packages. To instrument given installed packages, use the --pkg flag described below.

The raco symprofile ‹prog› command accepts the following command-line flags:

• --stream — stream profile data to a browser while executing the program, rather than producing output only once the program completes. This option is useful for programs that do not terminate, or take a very long time to run.

• -d ‹delay› — delay between samples when using the --stream option, in seconds (defaults to 2 s).

• -m ‹module-name› — run the specified ‹module-name› submodule of ‹prog› (defaults to the main submodule).

• -t ‹threshold› — prune function calls whose execution time is less than ‹threshold› milliseconds (defaults to 1 ms).

• --racket — instrument code in any language, not just those derived from Rosette.

• --pkg ‹pkg-name› — instrument code in ‹pkg-name›.

9.3.1Performance Bottlenecks🔗 i

Verifying sub->add for larger values of N causes the performance of verify-xform to degrade, from a couple of seconds when N = 5 to over a minute when N = 20. To identify the source of this performance issue, we can invoke the symbolic profiler on the verifier, producing the output below (after selecting the “Collapse solver time” checkbox):

The symbolic profiler identifies list-set as the bottleneck in this program. The output shows that list-set creates many symbolic terms, and performs many symbolic operations (the “Union Size” and “Merge Cases” columns).

The core issue here is an algorithmic mismatch: list-set makes a recursive call guarded by a short-circuiting condition (= idx0) that is symbolic when idx is unknown. When a condition’s truth value is unknown, Rosette must execute both branches of the conditional, and then merge the resulting symbolic values. So, in our example, Rosette always executes the recursive call, and each call creates a larger symbolic value that encodes the results of all the previous recursive calls. This behavior leads to a quadratic growth in the symbolic representation of the list returned by list-set:

> (define-symbolic idxinteger? )

> (list-set'(123)idx4)

(list

(ite (= 0 idx) 4 1)

(ite (= 0 idx) 2 (ite (= 0 (+ -1 idx)) 4 2))

(ite (= 0 idx) 3 (ite (= 0 (+ -1 idx)) 3 (ite (= 0 (+ -2 idx)) 4 3))))

The solution is to alter list-set to recurse unconditionally:

(define (list-set*lstidxval)

(match lst

[(cons xxs)

(cons (if (= idx0)valx)

(list-set*xs(- idx1)val))]

[_ lst]))

In this revision, Rosette still evaluates both branches of the conditional, but neither side of the conditional recurses, and so the verification conditions no longer grow quadratically.

> (list-set*'(123)idx4)

(list

(ite (= 0 idx) 4 1)

(ite (= 0 (+ -1 idx)) 4 2)

(ite (= 0 (+ -2 idx)) 4 3))

The performance of verify-xform after this change improves by 3× for N = 20.