key: cord-0053368-f410ydie
authors: Pan, Rong; Hu, Qinheping; Singh, Rishabh; D’Antoni, Loris
title: Solving Program Sketches with Large Integer Values
date: 2020-04-18
journal: Programming Languages and Systems
DOI: 10.1007/978-3-030-44914-8_21
sha: ba4174b25e113a08cf7e4634956fb28640aca6f6
doc_id: 53368
cord_uid: f410ydie

Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool, Sketch, can efficiently solve complex program sketches, but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this paper, we propose a new solving technique that allows Sketch to handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existing Sketch encodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existing Sketch solvers and can solve benchmarks that existing Sketch solvers cannot handle.

Program synthesis, the art of automatically generating programs that meet a user's intent, promises to increase the productivity of programmers by automating tedious, error-prone, and time-consuming tasks. Syntax-guided Synthesis (SyGuS) [2] , where the search space of possible programs is defined using a grammar or a domain-specific language, has emerged as a common program synthesis paradigm for many synthesis domains. One of the earliest and successful syntaxguided program synthesis frameworks is program sketching [19] , where (i ) the search space of the synthesis problem is described using a partial program in which certain integer constants are left unspecified (represented as holes), and (ii ) the specification is provided as a set of assertions describing the intended behavior of the program. The goal of the synthesizer is to automatically replace the holes in the program with integer values so that the resulting complete program satisfies all the assertions. Thanks to its simplicity, program sketching has found wide adoption in applications such as data-structure design [20] , personalized education [18] , program repair [7] , and many others.

The most popular sketching tool, Sketch [21] , can efficiently solve complex program sketches with hundreds of lines of code. However, Sketch often performs poorly if the sketched program manipulates large integer values. Sketch's synthesis is based on an algorithm called counterexample-guided inductive synthesis (Cegis) [21] . The Cegis algorithm iteratively considers a finite set I of inputs for the program and performs SAT queries to identify values for the holes so that the resulting program satisfies all the assertions for the inputs in I. Further SAT queries are then used to verify whether the generated solution is correct on all the possible inputs of the program. Sketch represents integers using a unary encoding (a variable for each integer value) so that arithmetic computations such as addition, multiplication etc. can be represented efficiently in the SAT formulas as lookup operations. This unary encoding, however, results in huge formulas for solving sketches with larger integer values as we also observe in our evaluation. Recently, an SMT-like technique that extends the SAT solver with native integer variables and integer constraints was proposed to alleviate this issue in Sketch. It guesses values for the integer variables and propagates them through the integer constraints, and learns from conflict clauses. However, this technique does not scale well when the sketches contain complex arithmetic operations-e.g., non-linear integer arithmetic.

In this paper, we propose a program transformation technique that allows Sketch to solve program sketches involving large integer values while retaining the unary encoding used by the traditional Sketch solver. Our technique rewrites a Sketch program into an equivalent one that performs computations over smaller values. The technique is based on the well-known Chinese Remainder Theorem, which states that, given distinct prime numbers p 1 , . . . , p n such that N = p 1 · . . . · p n , for every two distinct numbers 0 ≤ k 1 , k 2 < N, there exists a p i such that k 1 mod p i = k 2 mod p i . Intuitively, this theorem states that tracking the modular values of a number smaller than N for each p i is enough to uniquely recover the actual value of the number itself. We use this idea to replace a variable x in the program with n variables x p1 , . . . , x pn , so that for every i, x pi = x mod p i . Using closure properties of modular arithmetic we show that, as long as the program uses the operators +, −, * , ==, tracking the modular values of variables and performing the corresponding operations on such values is enough to ensure correctness. For example, to reflect the variable assignment x = y + z, we perform the assignment x pi = (y pi + z pi ) mod p i , for every p i . Similarly, the Boolean operation x == y will only hold if x pi = y pi , for every p i . To identify what variables and values in the program can be rewritten, we develop a data-flow analysis that computes what variables may flow into operations that are not sound in modular arithmetic-e.g., <, >, ≤, and /.

We provide a comprehensive theoretical analysis of the complexity of the proposed transformation. First, we derive how many prime numbers are needed to track values in a certain integer range. Second, we analyze the number of bits required to encode values in the original and rewritten program and show that, for the unary encoding used by Sketch, our technique offers an exponential saving in the number of required bits.

We evaluate our technique on 181 benchmarks from various applications of program sketching. Our results show that our technique results in significant speedups over existing Sketch solvers and is able to solve 48 benchmarks on which Sketch times out.

Contributions. In summary, our contributions are:

-A language IMP-MOD together with a modular semantics that represents integer values using their remainders for a given set of primes and a proof that this semantics is equivalent to the standard integer semantics ( § 4). -A data-flow analysis for detecting variables that can be soundly executed in the modular semantics and an algorithm for translating IMP programs into IMP-MOD ones ( § 5). -A synthesis algorithm for IMP-MOD programs and incremental synthesis algorithm that lazily increases the number of primes used in the modular semantics ( § 6).

-A complexity analysis that shows that synthesis for IMP-MOD programs requires exponentially smaller SAT queries than synthesis in IMP ( § 7). -An evaluation of our technique on 181 benchmarks that manipulate large integer values. Our solver outperforms the default Sketch unary solver, it can solve 48 new benchmarks that no Sketch solver can solve, and is 15.9X faster than the Sketch SMT-like integer solver on the hard benchmarks that take more than 10 seconds to solve ( § 8).

An extended version containing all proofs and further details has been uploaded to arXiv as supplementary material.

In this section, we use a simple example to illustrate our technique and its effectiveness. Consider the Sketch program polyArray presented in Figure 1b . The goal of this synthesis problem is to synthesize a two-variable quadratic polynomial (lines 7-8) whose evaluation p on given inputs x and y is equal to a given expected-output array z (line 9). Solving the problem amounts to finding non-negative integer values for the holes (??) and sign values, i.e., -1 or 1, for the holes (?? s ) such that the assertion becomes true. 1 In this case, a possible solution is the polynomial:

When attempting to solve this problem, the Sketch synthesizer times out at 300 seconds. To solve this problem, Sketch creates SAT queries where the variables are the holes. Due to the large numbers involved in the computation of this program, the unary encoding of Sketch ends up with SAT formulas with approximately 45 million clauses. 

The technique we propose in this paper has the goal of reducing the complexity of the synthesis problem by transforming the program into an equivalent one that manipulates smaller integer values and that yields easier SAT queries. Given the Sketch program in Figure 1b , our technique produces the modified Sketch program pAPrime in Figure 1a . The new Sketch program has the same control flow graph as the original one, but instead of computing the actual values of the expressions x[·] and y[·], it tracks their remainders for the set of prime numbers {2, 3, 5, 7, 11, 13, 17} using new variables-e.g., x2[i] tracks the remainder of x[i] modulo 2.

The program pAPrime initializes the modular variables with the corresponding modular values (lines [5] [6] [7] [8] . When rewriting a computation over modular variables, the same computation is performed modularly (lines [12] [13] [14] [15] [16] [17] . For example, the term ?? s 1 * ?? 1 *y[i] 2 when tracked modulo 2 is rewritten as

In the rewritten program, the variables i and n are not tracked modularly, since such a transformation would incorrectly access array indices. Finally, the assertions for different moduli share the same holes as the solution to the Sketch has to be correct for all modular values. In the rest of the paper, we develop a data flow analysis that detects when variables can be tracked modularly.

Sketch can solve the rewritten program in less than 2 seconds and produce hole values that are correct solutions for the original program. This speedup is due to the small integer values manipulated by the modular computations. In fact, the intermediate SAT formulas generated by Sketch for the program pAPrime have approximately 120 thousand clauses instead of the 45 million clauses for polyArray. Due to the complex arithmetic in the formulas, even if Sketch uses the SMT-like native integer encoding, it still requires more than 300 seconds to solve this problem.

While this technique is quite powerful, it does have some limitations. In particular, the solution to the rewritten Sketch is guaranteed to be a correct solution only for inputs that cause intermediate values of the program to be in a range [d 1 , d 2 ] such that d 2 − d 1 ≤ 2 × 3 × 5 × 7 × 11 × 13 × 17 = 510, 510. We will prove this result in Section 4.

In this section, we describe the IMP language that we will consider throughout the paper and briefly recall the counter-example guided inductive synthesis algorithm employed by the Sketch solver.

For simplicity, we consider a simple imperative language IMP with integer holes for defining the hypothesis space of programs. The syntax and semantics of IMP are shown in Appendix ??. Without loss of generality, we assume the programs consists of a single program f (v 1 , · · · , v n , ?? 1 , . . .?? m ) with n integer variables and m integer holes. The body of the program f consists of a sequence of statements, where a statement s can either be a variable assignment, a while loop statement, an if conditional statement, or an assert statement. The holes ?? denote integer constant values that are unknown and the goal of the synthesis process is to compute these values such that a set of desired program assertions are satisfied for every possible input values to f . 2 Example 1. An example IMP sketch denoting a partial program is shown below. The goal of the synthesizer is to compute the value of the hole ?? such that the assertion is true for all possible input values of n and h. For this example, ?? = 3 is a valid solution.

The Sketch solver uses the counter-example guided inductive synthesis algorithm (Cegis) to find hole values such that the desired assertions hold for all input values. Formally, the Sketch synthesizer solves the following constraint: 

The bounded domains make the synthesis problem decidable, but the secondorder quantified formula results in a search space of hole values that is still huge for any reasonable bounds. To solve such bounded equations efficiently, Sketch uses the Cegis algorithm to incrementally add inputs from the domain until obtaining hole values ?? that satisfy the assertion predicates for all the input values in the bounded domain. The algorithm solves the second-order formula by iteratively solving a series of first-order queries. It first encodes the existential query (synthesis query) over a randomly selected input value in 0 to find the hole values H that satisfy the predicate for in 0 using a SAT solver in the backend.

It then encodes another existential query (verification) to now find a counterexample in 1 for which the predicate is not satisfied for the previously found hole values.

If no counter-example input can be found, the hole values are returned as the desired solution. Otherwise, the algorithm computes a new hole value that satisfies the assertion for all the counter-example inputs found so far. This process continues iteratively until either a desired hole value is found (i.e. no counter-example input exists), no satisfiable hole value is found (i.e. the synthesis problem is infeasible), or the SAT solver times out.

The Sketch solver can efficiently solve the synthesis constraint in many domains, but it does not scale well for sketches manipulating large numbers. Sketch uses a unary encoding to represent integers, where the encoded formula consists of a variable for each integer value. The unary encoding allows for simplifying the representation of complex non-linear arithmetic operations. For example, a multiplication operation can be represented as simply a lookup table using this encoding. In practice, the unary encoding results in magnitudes of faster solving times compared to the logarithmic encoding for many synthesis problems. However, this also results in huge SAT formulas in presence of large integers. Recently, a new SMT-like technique based on extending the SAT solver with native integer variables and constraints was proposed to alleviate this issue in Sketch. Similar to the Boolean variables, this extended solver guesses for integer values and propagates them in the constraints while also learning from conflict clauses. Note that Sketch uses these SAT extensions and encodings instead of an SMT solver as SMT doesn't scale well for the nonlinear constraints typically found in the synthesis problems. Our new technique for handling computations over large numbers still maintains the efficient unary encoding of integers and computations over them.

In this section, we present the language IMP-MOD in which variables can be tracked using modular arithmetic. We start by recalling the Chinese Remainder Theorem, then define both a modular and integer semantics for the IMP-MOD language, and show that the two semantics are equivalent.

The Chinese Remainder Theorem is a powerful number theory result that shows the following: given a set of distinct primes P = {p 1 , . . . , p k }, any number n in an interval of size p 1 · . . . · p k can be uniquely identified from the remainders [n mod p 1 , · · · , n mod p k ]. In Section 4.2, we will use this idea to define the semantics of the IMP-MOD language. The main benefit of this idea is that the remainders could be much smaller than actual program values.

Example 2. For P = [3, 5, 7] and an integer 101, its remainders [2, 1, 3] are much smaller than 101. However, any number of the form 101 + 105 × n also has remainders [2, 1, 3] with respect to the same prime set.

In general, one cannot uniquely determine an arbitrary integer value from its remainders for some set P-i.e., the mapping from a number to its remainders is an abstraction in the sense of abstract interpretation [6] . However, if we are interested in a limited range of integer values [L, U ), one can choose a set of Theorem 1 (Chinese Remainder Theorem [4] ). Let p 1 , ..., p k be positive integers that are pairwise co-prime-i.e., no two numbers share a divisor larger than 1.

We define the translation function m P (x) := [x mod p i , · · · , x mod p k ] that maps an integer to its set of remainders with respect to P. When m P (x) is bijective on some set R, we denote with m −1,R

Example 3. Let x be a integer in the range [0, 105) (note that 105 = 3 × 5 × 7). If we know that the value of x is congruent to [2, 1, 3] modulo {3, 5, 7}, we can uniquely identify the value of x to be 101 by observing that 101 ≡ 2 mod 3, 101 ≡ 1 mod 5, and 101 ≡ 3 mod 7.

The following lemma shows that the function m P is closed under addition, subtraction and multiplication of integers. 

In this section, we define the IMP-MOD language (syntax in Figure 2 ), a variant of the IMP language for which the semantics can be defined using modular arithmetic. 3 An IMP-MOD program is parametric on a set P = {p 1 , . . . , prime numbers. The structure of an IMP-MOD program is similar to an IMP program, but IMP-MOD supports two types of variables and arithmetic expressions: the regular IMP ones (i.e., v, a, and b), which operate over an integer semantics, and the modular ones (i.e., v P , a P , and b P ), which take as an additional parameter the set of primes P and operate over a modular semantics. The semantics of some of the key constructs of IMP-MOD is shown in Figure 3 .

The key idea of the modular semantics is that the value of each program variable in v P and arithmetic expressions in a P is denoted by a tuple of values, one for each prime number p i ∈ P. For example, the value of the constant c P is represented by the tuple [c mod p 1 , · · · , c mod p k ], where each individual value denotes the remainder of c when divided by the prime number p i ∈ P. Formally, the program f has two sets of variables V Z = {v 1 , · · · , v n } and V P = {v P 1 , · · · , v P m }, which contain all the integer and prime variables respectively, and a set of holes H = {?? 1 , . . . , ?? k }. The denotation function, uses two valuation functions: (i ) σ : V Z ∪ H → Z, which maps variables and holes to integer values, (ii ) σ P : V P → [0, p 1 ) × · · · × [0, p k ), which maps primed variables to modular values. The expression toPrime(a) converts the integer value of an integer expression a to a modular tuple. Arithmetic expressions in a P are computed using modular values with the result being obtained using modular arithmetic with respect to the corresponding primes in P. Note that the only comparison operator allowed over modular expressions is == and that the division operator cannot be applied to modular expressions. While the syntax does not directly allow for holes to be represented modularly-i.e., we do not have expressions of the form ?? P -an expression of the form toPrime(??) effectively achieves the objective of representing a hole ?? modularly.

Next, we provide an alternative integer semantics, which applies the IMP integer semantics to modular expressions and show that, under some assumptions on the values manipulated by the program, the modular and integer semantics are equivalent. We will use this result to build our modified synthesis algorithm. Integer Semantics The integer semantics of IMP-MOD is shown in Figure 4 (denoted · σ1,σ2 ). In this semantics, modular expressions are evaluated as integer expressions using the same semantics as for IMP-i.e., the values of modular variables and modular arithmetic expressions are denoted by integer values. Therefore, in the integer semantics, we use two valuation functions σ 1 : V Z ∪ H → Z mapping variables and holes to integers and σ 2 : V P → Z mapping modular variables to integers. Relation between the Two Semantics We now show that the modular semantics is, in some sense, equivalent to the integer semantics. For the rest of this section, we fix a set of distinct primes P = {p 1 , · · · , p k }.

To prove the equivalence of the two program semantics, we will require the values of modular expressions to lie in some range that is covered by the prime numbers in P. The following definition captures this restriction. Definition 1. Given a modular arithmetic expression a P (resp. Boolean expression b) and some integers L < U, we say a P with context (σ 1 , σ 2 ) is uniformly in the range R := [L, U ) -a P ∈ σ1,σ2 R for short-if under the integer semantics, all evaluation of modular subexpressions of a P (resp. b) are in the range R: Given a valuation function σ : V P → Z, we write m P • σ to denote the modular valuation obtained by applying the m P function to σ-i.e., for every v P ∈ V P , (m P • σ)(v P ) = m P (σ(v P )). Similarly, for a modular valuation function

). The following lemma shows that, when the values of modular arithmetic expressions lay in an interval of size N = p 1 · . . . · p k the modular and integer semantics of modular arithmetic expressions are equivalent. Lemma 2. Given a set of primes P = {p 1 , · · · , p k }, an arithmetic expression a P , and two valuation functions

Similarly, we show that the two semantics are also equivalent for Boolean expressions.

We are now ready to show the equivalence between the modular semantics and the integer semantics for programs P ∈ IMP-MOD. The semantics of a program P = f (V Z , V P , H) {s} is a map from valuations to valuations, i.e., given a valuation σ 1 : V Z → Z for integer variables, a valuation σ 2 : V P → Z for modular variables and a valuation σ H : H → Z for holes, we have P (σ 1 , σ 2 , σ H ) = s σ1∪σ H ,σ2 and P P (σ 1 , σ 2 , σ H ) = s P σ1∪σ H ,m P •σ2 . Therefore, it is sufficient to show that the two semantics are equivalent for any statement s.

The two semantics are equivalent for a statement s if, under the same input valuations, the resulting valuations of the semantics can be translated to each other. Formally, given valuations σ 1 , σ 2 and an interval R of size N , we say s σ1,σ2 ≡ P s P σ1,m P •σ2 iff σ 1 = σ 1 , m P • σ 2 = σ P 2 and σ 2 = m −1,R P • σ P 2 where s σ1,σ2 = (σ 1 , σ 2 ) and s P σ1,m P •σ2 = (σ 1 , σ P 2 ). We define uniform inclusion for statements. Definition 2. Given a set of primes P, two integers L < U and a statement s, we say s with context (σ 1 , σ 2 ) is uniformly in the range R := [L, U )-s ∈ σ1,σ2 R for short-if under the integer semantics, all evaluation of modular subexpressions of s are in the range R:

At last, the two semantics are equivalent for statements.

Theorem 2. Given a set of primes P = [p 1 , · · · , p k ], a statement s and two valuation functions σ 1 : V Z ∪ H → Z and σ 2 : V P → Z, if there exists an interval R of size N such that s ∈ σ1,σ2 R, then s σ1,σ2 ≡ P s P σ1,m P •σ2 . 

In this section, we develop a data flow analysis for detecting variables in IMP programs for which it is sound to track values modularly. We then use this data flow analysis to rewrite an IMP program to an equivalent IMP-MOD program.

The formalization of IMP-MOD in Section 4.2 made it clear that the modular semantics is only appropriate when integer values are manipulated using addition, multiplication, subtraction, and equality. Other operations like division and less-than comparison cannot be computed soundly in modular arithmetic.

Consider an integer variable x with modular value x 2 under modulus 2 and x 3 under modulus 3, and an integer variable y with modular value y 2 , y 3 under corresponding moduli. Then the assignment of x = y + y; implies x 2 = (y 2 + y 2 ) mod 2; and x 3 = (y 3 + y 3 ) mod 3. However, x = x/y; does not imply x 2 = (x 2 /y 2 ) mod 2; and x 3 = (x 3 /y 3 ) mod 3.

We now define a data flow analysis (shown in Algorithm 1) for computing which variables in a program must be tracked with the integer semantics (i.e., the set V Z ) and which variables can be soundly tracked using the modular semantics (i.e., the set V P ). For each operator op in {/, <, >, ≤, ≥}, the analysis computes the set of variables that may flow into the operands of an expression of the form e 1 op e 2 . In practice, this is done via backward may analysis, noted as Dataflow procedure in Algorithm 1. The obtained set of variables must be tracked using the integer semantics. The remaining variables will never flow into a problematic operator and can therefore be tracked using the modular semantics. Implementation Remark Since our implementation also supports arrays and recursion, the data flow analysis in Algorithm 1 is inter-procedural and the set S also contains the array indexing operator [ ]-i.e., given an expression arr [a] , if a variable v may flow into a, then a must be tracked using the integer semantics. Furthermore, while in our formalization we allow variables to be tracked using only one of the two semantics, in our implementation, we allow variables to be tracked differently (using actual values or modular values) at different program points by tracking, for each variable v, the program points for which the actual value of v is needed, which is done by using the same data-flow analysis. In this case, a variable might initially need to be tracked using actual values but can later be tracked using modular values.

Example 5. Consider the sketch program polyArray in Figure 1b . For this program, Algorithm 1 will return that the variables x and y can be tracked modularly. However, the variables i and n must be tracked using the integer semantics since they are used in a < operation and as array indices.

Now that we have computed what sets of variables can be tracked modularly, we can transform the IMP program into an IMP-MOD program. The transformation R f that rewrites f into an IMP-MOD program is shown in Figure 5 . The key idea of the program transformation is to use the sets V Z and V P to only rewrite variables and sub-expressions of f for which the modular arithmetic can be performed soundly. Once we get a solution for the IMP-MOD program as hole values, we can get a solution for the IMP program by mapping the hole to integer values given by the integer semantics. Example 6. Consider a program where the dataflow analysis computes V Z = {i, n} and V P = {x}. The statement x = x + i + 1 is rewritten to x P = x P + toPrime(i) + 1 P .

The transformation R f is sound.

Given an IMP program f , and sets V Z and V P resulting from the data flow analysis on f , the program R f (f ) is in the IMP-MOD language. Moreover, f IMP = R f (f ) .

In this section, we discuss how synthesis in the modular semantics relates to synthesis in the integer semantics and provide an incremental algorithm for solving IMP-MOD sketches.

Similarly to what we saw in Section 3, we assume that the sketch has to be solved for finite ranges of possible values for the hole (R H ) and input values (R in ). Solving an IMP-MOD problem P = f (V, V P , H){s} for the integer semantics amounts to solving the following constraint:

According to Theorem. 2, given a set of distinct primes P = {p 1 , · · · , p k } and variable valuations σ H , σ 1 , and σ 2 , if there exists a range R of size N = p 1 · . . . · · · p k such that s ∈ σ1∪σ H ,σ2 R, the modular semantics and the integer semantics are equivalent to each other. Using this observation, we can define the set of variable valuations for which the two semantics are guaranteed to be equivalent:

Since for every σ H ∈ R H and σ 1 , σ 2 ∈ I P R we have that s P σ1∪σ H ,m P •σ2 = s σ1∪σ H ,σ2 , any solution to an IMP-MOD program in the modular semantics is also a solution to the following formula in the integer semantics:

When all valuations in σ 1 , σ 2 ∈ R in are also elements of I P R , any solution to an IMP-MOD program in the modular semantics is guaranteed to be a correct solution under the integer semantics.

To summarize, if the synthesizer returns UNSAT for the IMP-MOD program, the problem is unrealizable and does not admit a solution. When it returns a solution, the solution is correct if it only produces valuations in the range allowed by 

In this section, we propose an incremental synthesis algorithm that builds on the following observation. The set of variable valuations for which modular and integer semantics are equivalent increases monotonically in the size of P:

Algorithm 2 uses Equation 1 to add prime numbers lazily during the synthesis process. The algorithm first constructs a set P = {p 1 } with the first prime number p 1 ∈ P and synthesizes a solution that is correct for computations modulo the set P . It then checks if the synthesized solution f syn satisfies the assertions with respect to all prime numbers in P. If yes, f syn is returned as the solution. Otherwise, the algorithm finds a prime p cex ∈ P where Verify(f syn , p cex ) does not hold and it adds it to the set P continuing the iterative algorithm. Due to Equation 1, Algorithm 2 is sound and complete with respect to the synthesis algorithm that considers the full prime set P all at once.

In practice, the user could use domain knowledge to estimate a suitable set of primes or alternatively use our incremental algorithm to discover appropriate prime sets. The set of prime numbers {2, 3, 5, 7, 11, 13, 17} could usually instantiate a range R that is large enough for most synthesis tasks based on Sketch.

In this section, we analyze how many bits are necessary to encode numbers for both semantics using unary and binary bit-vector encodings of integers (Sec. 7.1 and 7.2), and show how many prime numbers are necessary in the modular semantics to cover values up to a certain bound (Sec. 7.3). The following results build upon several number theory results that the reader can consult at [9, 15] .

In this section, we analyze how many bits are necessary when representing an interval of size N in binary in our modular semantics. In the rest of the section, we consider the set of primes P n = {p | p < n} = {p 1 , . . . , p k } containing the prime numbers that have value smaller than n. We will show in Section 8 that this choice of prime number also yields good performance in practice. Concretely, we are interested in knowing what is the magnitude of the number N = p 1 ·. . .·p k and how many bits are used to represent the numbers in P n .

We start by introducing the notion of primorial.

. Given a number n, the primorial n# is defined as the product of all primes smaller than n-i.e., n# = p∈Pn p.

The primorial captures the size N of the interval covered by the Chinese Remainder Theorem when using prime numbers up to n. The following number theory result gives us a close form for the primorial and shows that the number N has approximately n bits.

n# = e (1+o(1))n = 2 (1+o(1))n

We use another number theory notion to quantify the number of bits in P n .

n-i.e., ϑ(n) = p∈Pn log p.

The following number theory result relates the primorial to the Chebyshev function. ϑ(n) = log(n#) = log 2 (1+o(1))n = (1 + o(1))n

Aside from rounding errors, the Chebyshev function captures the number of bits required to represent the numbers in P n . To obtain a more precise bound on this number, we need a bound for the formula p∈Pn log p .

We start by recalling the following fundamental number theory result.

Theorem 4 (Prime number theorem). The set P n has size approximately n/ log n.

Using Theorem 4, we get the following result.

Representing a number e n in a classic binary encoding requires log 2 (e n ) = (1 + o(1))n bits and, combining Equations 2 and 4, we get the following result.

Theorem 5. Representing a number 2 n in binary requires (1+o(1))n bits under both modular and integer semantics.

Hence, representing a number in binary requires the same number of bits in the both semantics.

Example 7. Consider the set P 18 = {2, 3, 5, 7, 11, 13, 17}, which can model an interval of N = 510, 510 integers (i.e., n = 18 in Theorem 5). Representing N in binary requires 19 bits while the binary representations of all the primes in P 18 use 22 bits. Both numbers are close to 18 as predicted by the theorem.

As discussed in Sec. 3, the default Sketch solver encodes numbers using a unary encoding-i.e., Sketch requires 2 n bits to encode the number 2 n . Representing the same number in unary under the modular semantics requires only prime numbers smaller than n and therefore p∈Pn p bits. We can then use the following closed form to approximate this quantity. Theorem 6. Representing a number 2 n in unary requires 2 n bits in the integer semantics and approximately n 2 2 log n bits in the modular semantics. These results show that, under a unary encoding, the modular semantics is exponentially more succinct than the integer semantics. 

We analyze how many primes are needed to represent a certain number in the modular semantics. We start by introducing the following alternative version of the primorial. The following known number theory result gives us an approximation for the prime primorial. p n # = e (1+o(1))n log n (6) Notice how the approximation of the primorial differs from that of the prime primorial. This is due to the fact that prime numbers are sparse-i.e., the n-th prime number is approximately n log n. Using Equation 6 we obtain the following result.

Theorem 7. Representing numbers in an interval of size N = e n log n in the modular semantics requires the first n prime numbers.

Since the relation k = n log n does not admit a closed form for n, we cannot derive exactly how many primes are needed to represent a number 2 k with k bits. It is however clear from the theorem that the number of required primes grows slower than k.

We implemented a prototype of our technique as a simple compiler in Java. Our implementation provides a simplified Sketch frontend, which only allows the limited syntax we support. Given a Sketch file, our tool rewrites it into a different Sketch file that operates according to the modular semantics. We will use Unary to denote the result obtained by running the default version of Sketch with unary integer encoding on the original Sketch file, Binary to denote the result obtained by running the version of Sketch using an SMT-like native integer solver based on binary integer encoding, Unary-p to denote the result of running the default Sketch version on our modified Sketch file, and Unaryp-inc to denote the result of running the default version of Sketch on the file generated by the incremental version of our algorithm described in Section 6. As expected from our theory, the prime technique is not beneficial for the SMT-like native integer solver and always results in worse runtime. Therefore, we do not present data for this solver. All experiments were performed on a machine with 4.0GHz Intel Core i7 CPU with 16GB RAM with Sketch-1.7.5 and we use a timeout value of 300 seconds (we also report out-of-memory errors as timeouts). Our evaluation answers the following research questions:

Q1 How does the performance of Unary-p compare to Unary and Binary? Q2 How does the incremental algorithm compare to the non-incremental one? Q3 Is Unary-p's performance sensitive to the set of selected prime numbers? Q4 How many primes are needed by Unary-p to produce correct solutions? Q5 Does Unary generate larger SAT queries than Unary-p?

We perform our evaluation on three families of programs. Polynomials The first set of benchmarks contains 81 variants of the polynomial synthesis problem presented in Figure 1 . Invariants The second set of benchmarks contain 46 variants of two invariant generation problems obtained from a public set of programs that require polynomial invariants to be verified [8] . We selected the two programs in which at least one variable could be tracked modularly by our tool (the other programs involved complex array operations or inequality operators) and turned the verification problems into synthesis problems by asking Sketch to find a polynomial equality (using the program variables) that is an invariant for the loop in the program. To control the size of the magnitudes of the inputs, we only require the invariants to hold for a fixed set of input examples. The first problem, mannadiv, iteratively computes the remainder and the quotient of two numbers given as input. The invariant required to verify mannadiv is a polynomial equality of degree 2 involving 5 variables. The Sketch template required to describe the space of all polynomial equalities has 32 holes and cannot be handled by any of the Sketch solvers we consider. We therefore simplify the invariant synthesis problems in two ways. In the first variant, we reduce the ranges of the hole values in the templates by considering cbits ∈ {2, 3}. In the second variant, we set cbits = {5, 6, 7}, but reduce the number of missing hole values to 4 (i.e., we provide part of the invariant). Each benchmark takes two random inputs and we consider the following input ranges { [1, 50] , [1, 100] }. In total, we have 10 benchmarks for mannadiv.

The second problem, petter, iteratively computes the sum 1≤i≤n i 5 for a given input n. The invariant required to verify petter is a polynomial equality of degree 6 involving 3 variables. The Sketch template required to describe all such polynomial equalities has 56 holes and cannot be handled by any of the Sketch solvers we consider. We consider the following simplified variants of the problem: (i ) petter_0 computes 1≤i≤n 1 and requires a polynomial invariant of degree one, (ii ) petter_x computes 1≤i≤n x for a given input variable x and requires a polynomial invariant of degree two, (iii ) petter_1 computes 1≤i≤n i and requires a polynomial invariant of degree two, and (iv ) petter_10 computes 1≤i≤n i + 1 and requires a polynomial invariant of degree two. Each benchmark takes two random inputs and we consider the following input ranges { [1, 10] , [1, 100] , [1, 1000] }. In total, we have 12 variants of petter, each run for values of cbits ∈ {5, 6, 7}-i.e., a total of 36 benchmarks.

The third set of benchmarks contains 54 variants of Sketch problems from the domain of automatic feedback generation for introductory programming assignments [7] . Each benchmark corresponds to an incorrect program submitted by a student and the goal of the synthesizer is to find a small variation of the program that behaves correctly on a set of test cases. We select the 6/11 benchmarks from the tool Qlose [7] for which (i ) our implementation can support all the features in the program, and (ii ) our data flow analysis identifies at least one variable that can be tracked modularly. Of the remaining benchmarks, 3/11 do not contain variables that can be tracked modularly, and 2/11 call auxiliary functions that cannot be translated into Sketch. For each program, we consider the original problem and two variants where the integer inputs are multiplied by 10 and 100, respectively. Further, for each program variants, we impose an assertion specifying that the distance between the original program and the repaired program is within a certain bound. We select three different bounds for each program: the minimum cost c, c + 100, and c + 200. Figure 7a shows a scatter plot (log scale) of the solving times for the two techniques: each point below the diagonal line denotes a benchmark on which Unary-p was faster than Unary. Points on the extreme right-hand side of the plot denote timeout for Unary. When both solvers terminate, Unary-p (avg. 1.7s) is 6.1X (geometric mean) faster than Unary (avg. 25.0s). Next, we compare the performance of Unary-p and Binary (Figure 7b ). On the 64 easier benchmarks that Binary can solve in less than 1 second, Binary (avg. 0.55s) outperforms Unary-p (avg. 2.32s), but Unary-p still has reasonable performance. On the 49 benchmarks that Binary can solve between 1 and the discussion throughout the paper, these are benchmarks typically involving complex operations but not involving overly large numbers.

We can now answer Q1. First, Unary-p consistently outperforms Unary across all benchmarks. Second, Unary-p outperforms Binary on hard-tosolve problems and can solve problems that Binary cannot solvee.g., Unary-p solved 28/46 invariant problems that Sketch could not solve. Unary-p and Binary have similar performance on easy problems. Comparison to full SMT encoding For completeness, we also compare our approach to a tool that uses SMT solvers to model the entire synthesis problem. We choose the state-of-the-art SMT-based synthesizer Rosette [23] for our comparison. Rosette is a programming language that encodes verification and synthesis constraints written in a domainspecific language into SMT formulas that can be solved using SMT solvers. We only run Rosette on the set of Polynomials because Rosette does support the theories of integers, but does not have native support for loops, so there is no direct way to encode Invariants and Program Repair benchmarks. To our knowledge, Rosette provides a way to specify the number k it uses to model integers and reals as k-bit words, but the user has no control over how many bits it uses for unknown holes specifically. So we evaluate 27 instead of 81 variants of the polynomial synthesis problem on Rosette, i.e., we consider different numbers of cbits. Figure 6 shows the running times (log scale) for Rosette and Binary with cbits=6. Rosette successfully solved 16/27 benchmarks and it terminates quickly (avg. 2.9s) when it can find a solution. However, Rosette times out on 11 benchmarks for which Binary terminates. The timeouts are due to the fact that Rosette employs full SMT encodings that combine multiple theories while Binary uses a SAT solver that is only modified to accommodate SMT-like integer constraints. Since we now know full SMT encodings are not as general and efficient as the encodings used in Sketch, we will only evaluate the effectiveness of our technique based on comparison with Binary.

Finally, we tried applying our prime-based technique to Rosette and, as expected, the technique is not beneficial due to the binary encoding of numbers in SMT, and causes all benchmarks to timeout. To summarize, (i ) SMT solvers cannot efficiently handle the synthesis problems considered in this paper, and (ii ) our technique is better suited for SAT solvers than SMT solvers.

Our implementation of the incremental solver Unary-p-inc first attempts to find a solution with the prime set P = {2, 3, 5, 7}. If the solver returns a correct solution, Unary-p-inc terminates. Otherwise, Unary-p-inc incrementally adds the next prime to P until it finds a correct solution, it proves there is no solution, or it times out. Unary-pinc is 25.2% (geometric mean) slower than Unary-p (Figure 8 (log scale) ). Unary-p-inc can solve three benchmarks for which both Unary-p and Binary timed out. To answer Q3, Unary-p-inc and Unary-p have similar performance.

In this experiment, we evaluate how different prime number sets affect Unary-p.

We consider the 5 increasing sets of primes: P 5 = {2, 3, 5}, P 7 = {2, 3, 5, 7}, P 11 = {2, 3, 5, 7, 11}, P 13 = {2, 3, 5, 7, 11, 13}, and P 17 = {2, 3, 5, 7, 11, 13, 17}. Figure 9a (log scale) shows the running times for all the polynomial benchmarks with cbits=7 (showing all benchmarks would clutter the plot). The points where the lines change from dashed to solid denote the number of primes for which the algorithm starts yielding correct solutions. As expected, a smaller set of primes leads to faster solving times as the resulting constraints are smaller and fewer bits are needed for encoding intermediate values. The runtime on average grows with the increasing size of the primes. For example, across all benchmarks, using P 17 takes 23% longer on average than using P 11 . To answer Q3, Unary-p is slower when using increasingly large sets of prime.

In terms of correctness, we find that smaller prime sets often yield incorrect solutions (P 5 (37% correct), P 7 (70%), P 11 (86%), P 13 (97 %), and P 17 (100%) because there is not enough discriminative power with fewer primes and the Figure 9b (log scale) shows the running time of Unary-p for the same benchmarks as Figure 9a . Larger prime sets of smaller prime values require less time to solve than smaller prime sets of larger prime values. This result is expected since, in the unary encoding of numbers, representing larger numbers requires more bits.

In this experiment, we compare the sizes of the intermediate SAT formulas generated by Unary-p and Unary. Figure 10a shows a scatter plot (log scale) of the number of clauses of the largest intermediate SAT query generated by the CEGIS algorithm for the two techniques. We only plot the instances in which Unary was able to produce at least a SAT formula. Unary produces SAT formulas that are on average 19.3X larger than those produced by Unary-p. To answer Q5, as predicted by our theory, Unary-p produces significantly smaller SAT queries than Unary. Performance vs Size of SAT Queries We also evaluate the correlation between synthesis time and size of SAT queries. Figure 10b plots the synthesis times of both solvers against the sizes of the SAT queries. It is clear that the synthesis 

Program Sketching Program sketching was designed to automatically synthesize efficient bit-vector manipulations from inefficient iterative implementations [21] . The Sketch tool has since been engineered to support complex language features and operations [19] . Thanks to its simplicity, sketching has found wide adoption in applications such as optimizing database queries [3] , automated feedback generation [18] , program repair [7] , and many others. Our work further extends the capabilities of Sketch in a new direction by leveraging number theory results. In particular, our technique allows Sketch to handle sketches manipulating large integer numbers. To the best of our knowledge, our technique is the first one that can solve many of the benchmarks presented in this paper.

Uses of Chinese Remainder Theorem The Chinese Remainder Theorem and its derivative corollaries have found wide application in several branches of Computer Science and, in particular, in Cryptography [11, 26] . The idea of using modular arithmetic to abstract integer values has been used in program analysis. Since modular fields are finite, they can be used as an abstract domain for verifying programs manipulating integers [5]-e.g., the abstract domain can track whether a number is even or odd. Our work extends this idea to the domain of program synthesis and requires us to solve several challenges. First, when used for verifying programs, the modular abstraction is used to overapproximate the set of possible values of the program and does not need to be precise. In particular, Clark et al. [5] allow program operations that are in the IMP language but not in the IMP-MOD language and lose precision when modeling such operations-e.g., when performing the assignment x = x/2 the value of x mod 2 can be either 0 or 1. Such imprecision is fine in program analysis since the abstraction is used to show that a program does not contain a bugi.e., even in the abstract domain, the problem behaves fine. In our setting, the problem is opposite as we use the abstraction to simplify the synthesis problem and provide a theory for when the modular and integer semantics are equivalent.

Pruning Spaces in Program Synthesis Many techniques have been proposed to prune large search space of possible programs [14] . Enumerative synthesis techniques [24, 12, 13, 17] enumerate programs in a search space and avoid enumerating syntactically and semantically equivalent terms. Some synthesizers such as Synquid [16] and Morpheus [10] use refinement types and first-order formulas over specifications of DSL constructs to refute inconsistent programs. Recently, Wang et al. [25] proposed a technique based on abstraction refinement for iteratively refining abstractions to construct synthesis problems of increasing complexity for incremental search over a large space of programs.

Instead of pruning programs in the syntactic space, our technique uses modular arithmetic to prune the semantic space-i.e., the complexity of verifying the correctness of the synthesized solution-while maintaining the syntactic space of programs. Our approach is related to that of Tiwari et al. [22] , who present a technique for component-based synthesis using dual semantics-where syntactic symbols in a language are provided two different semantics to capture different requirements. Our technique is similar in the sense that we also provide an additional semantics based on modular arithmetic. However, we formalize our analysis based on number theory results and develop it in the context of generalpurpose Sketch programs that manipulate integer values, unlike Tiwari et al.'s work that is developed for straight-line programs composed of components.

Cegis algorithm for solving syntax-guided synthesis (SyGuS) problems with large constants [1] . SyGuS differs from program sketching in how the synthesis problem is posed and in the type of programs that can be modeled. In particular, in SyGuS one can only describe programs representing SMT formulas and the logical specification for the problem can only relate the input and output of the program-i.e., there cannot be intermediate assertions within the program. The problem setup and the solving algorithms proposed in this paper are orthogonal to those of Abate et al. First, we focus on program sketching, which is orthogonal to SyGuS as sketching allows for richer and more generic program spaces as well as richer specifications. While it is true that certain synthesis problems can be expressed both as sketches and as SyGuS problems, this is not the case for our benchmarks programs, which use loops, arrays and non-linear integer arithmetic, all of which are not supported by SyGuS. Second, our technique is motivated by how Sketch encodes and solves program sketches through SAT solving. While the traditional Sketch encoding can explode for large constants, the same encoding allows Sketch to solve program sketches involving complex arithmetic and complex programming constructs. The algorithm proposed by Abate et al. iteratively builds SMT (not SAT) formulas that are required to be in a decidable logical theory. Such an encoding only works for the restricted programming models used in SyGuS problems.

Counterexample guided inductive synthesis modulo theories

Syntax-guided synthesis

Optimizing database-backed applications with query synthesis

The Chinese Remainder Theorem

Model checking and abstraction

Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

Qlose: Program repair with quantitative objectives

Polynomial invariants by linear algebra

Estimates of ψ,ϑ for large values of x without the riemann hypothesis

Componentbased synthesis of table consolidation and transformation tasks from examples

The chinese remainder theorem and its application in a high-speed rsa crypto chip

Automating string processing in spreadsheets using input-output examples

Spreadsheet data manipulation using examples

Program synthesis. Foundations and Trends in Programming Languages

The Prime Number Theorem

Program synthesis from polymorphic refinement types

Transforming spreadsheet data types using examples

Automated feedback generation for introductory programming assignments

Sketching concurrent data structures

Combinatorial sketching for finite programs

Program synthesis using dual interpretation

A lightweight symbolic virtual machine for solver-aided host languages

Transit: Specifying protocols with concolic snippets

Program synthesis using abstraction refinement

Rsa speedup with chinese remainder theorem immune against hardware fault cryptanalysis

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use