Synthesising with Grammar containing multiple instances of structs with different parameters returns unsat

[RafaeNoor]

I did not know how to title this issue but I will explain the issue I am running into here.

I have implemented a DSL in Rosette using struct embeddings with an interpreter. I will show a minimal failing example here.

For example:

;; Definitions
;; Reg indexes into a vector
(struct reg (id) #:transparent #:mutable)    
(struct BROADCAST (v0  size_o lane_size num_3 prec_i_o num_5 num_6 num_7) #:transparent)

(define (interpret prog env)
   (destruct prog
          [(reg id) (vector-ref-bv env id)]
            [ (BROADCAST v0 size_o lane_size num_3 prec_i_o num_5 num_6 num_7)                                                                                                                                                                                                                                                                                                                         
              (broadcast-impl (interpret v0 env) size_o lane_size                                                                                                                                                  
                                        num_3 prec_i_o num_5                                                                                                                                                                 
                                      num_6 num_7)                                                                                                                                                                         
             ]                  
   )
)
...

Note that the arguments to BROADCAST except v0 are integer parameters which affect how broadcast-impl functions. broadcast-impl takes an input bit vector and concatenates to itself (essentially broadcasting itself) depending on the specific values of the numeric parameters. Additionally, the bit vector length of the bit vector input v0 can be different, and hence the output length of this result may also be different. However for a given parameterisation of the parameters the input length and output length will be the same.

I want to use these structs and specific parameterisations to synthesise an equivalent function in this DSL. So I define the following grammar:

(define-grammar (base_2988_grammar_operations_tree)
                [expr 
                  (choose
                    (reg (bv 0 4)) 

                    (
                     BROADCAST
                     (expr) ;; 128-bit Bitvector operand
                     256                ;; Integer Operand 
                     256                ;; Lane Size 
                     256                ;; Integer Operand 
                     16             ;; Precision Operand 
                     0              ;; Integer Operand 
                     0              ;; Integer Operand 
                     0              ;; Integer Operand 
                     )

                    (BROADCAST (expr) ; <1 x i32>
                     512  512  512  32  0  0  0  )

                    )]
                )

(define bounded-grammar
  (base_2988_grammar_operations_tree  #:depth 2 )
  )

The synthesis query is issued as follows:

(define broadcast-expr 
  (BROADCAST (reg (bv 0 4)) ; <1 x i32>
                          512  512  512  32  0  0  0  )
  )

(define-symbolic sym-bv (bitvector 32))
(define env (vector sym-bv))

;; Result takes sym-bv  and concatenates
;; to itself 16 times
(define result (interpret broadcast-expr env))

(define sol?
  (synthesize
    #:forall (list  env)
    #:guarantee 
    (begin 
      (assert
        (equal?   result (interpret bounded-grammar env))
        )
      )
    ) 
  )

(displayln "Synthesizing Complete!")
(define satisfiable? (sat? sol?))

(define materialize 
  (if satisfiable? 
    (evaluate bounded-grammar sol?)
    '()
    )
  )

(displayln "Synthesized solution")
(println materialize)

The synthesis outputs:

Synthesizing Complete!
Synthesized solution
'() ;; Didn't find a solution so returned empty list

Given the construction of broadcast-expr, the grammar contains the clauses neccesary to synthesise the solution (BROADCAST (reg (bv #x0 4)) 512 512 512 32 0 0 0) but it appears to be failing as there are two clauses for BROADCAST but with different parameterisations (which are concrete).

However when I do the following the synthesis works as expected:

;; Definitions
;; Reg indexes into a vector
(struct reg (id) #:transparent #:mutable)    
(struct BROADCAST (v0  size_o lane_size num_3 prec_i_o num_5 num_6 num_7) #:transparent)

;; Identical definition to BROADCAST
(struct BROADCAST-OTHER (v0  size_o lane_size num_3 prec_i_o num_5 num_6 num_7) #:transparent)

(define (interpret prog env)
   (destruct prog
          [(reg id) (vector-ref-bv env id)]
            [ (BROADCAST v0 size_o lane_size num_3 prec_i_o num_5 num_6 num_7)                                                                                                                                                                                                                                                                                                                         
              (broadcast-impl (interpret v0 env) size_o lane_size                                                                                                                                                  
                                        num_3 prec_i_o num_5                                                                                                                                                                 
                                      num_6 num_7)                                                                                                                                                                         
             ]
            [ (BROADCAST-OTHER v0 size_o lane_size num_3 prec_i_o num_5 num_6 num_7)                                                                                                                                                                                                                                                                                                                         
              (broadcast-impl (interpret v0 env) size_o lane_size                                                                                                                                                  
                                        num_3 prec_i_o num_5                                                                                                                                                                 
                                      num_6 num_7)                                                                                                                                                                         
             ]                    
   )
)
...

;; Grammar now differentiates between the two clauses by the name of the struct, even though function being called inside is ;; the same. 
(define-grammar (base_2988_grammar_operations_tree)
                [expr 
                  (choose
                    (reg (bv 0 4)) 

                    (
                     BROADCAST-OTHER
                     (expr) ;; 128-bit Bitvector operand
                     256                ;; Integer Operand 
                     256                ;; Lane Size 
                     256                ;; Integer Operand 
                     16             ;; Precision Operand 
                     0              ;; Integer Operand 
                     0              ;; Integer Operand 
                     0              ;; Integer Operand 
                     )

                    (BROADCAST (expr) ; <1 x i32>
                     512  512  512  32  0  0  0  )

                    )]
                )

Upon doing this, the synthesis works as expected and as such returns the desired solutions: (BROADCAST (reg (bv #x0 4)) 512 512 512 32 0 0 0) . Is there something wrong in the previous approach which prevented the synthesis from succeeding ? Ideally would there be a way to keep the different parameterisations in the same struct and provide their concrete values in the grammar clauses.

Any help would be greatly appreciated!

[emina]

It seems that the behavior you're seeing may be due to some issue with broadcast-impl. I'm guessing this based on the following code that tries to replicate your example but gives the expected behavior with a stand-in implementation for broadcast-impl:

#lang rosette

(require rosette/lib/synthax rosette/lib/destruct)

(struct reg (id) #:transparent #:mutable)    
(struct BROADCAST (v0  size_o lane_size num_3 prec_i_o num_5 num_6 num_7) #:transparent)

(define broadcast-impl list)

(define (interpret prog env)
   (destruct prog
          [(reg id) (vector-ref-bv env id)]
            [ (BROADCAST v0 size_o lane_size num_3 prec_i_o num_5 num_6 num_7)                                                                                                                                                                                                                                                                                                                         
              (broadcast-impl (interpret v0 env) size_o lane_size                                                                                                                                                  
                                        num_3 prec_i_o num_5                                                                                                                                                                 
                                      num_6 num_7)                                                                                                                                                                         
             ]                  
   )
)

(define-grammar (base_2988_grammar_operations_tree)
                [expr 
                  (choose
                    (reg (bv 0 4)) 

                    (
                     BROADCAST
                     (expr) ;; 128-bit Bitvector operand
                     256                ;; Integer Operand 
                     256                ;; Lane Size 
                     256                ;; Integer Operand 
                     16             ;; Precision Operand 
                     0              ;; Integer Operand 
                     0              ;; Integer Operand 
                     0              ;; Integer Operand 
                     )

                    (BROADCAST (expr) ; <1 x i32>
                     512  512  512  32  0  0  0  )

                    )]
                )

(define bounded-grammar
  (base_2988_grammar_operations_tree  #:depth 2 )
  )

(define-symbolic sym-bv (bitvector 32))
(define env (vector sym-bv))

(define broadcast-expr 
  (BROADCAST (reg (bv 0 4)) ; <1 x i32>
                          512  512  512  32  0  0  0  )
  )

;; Result takes sym-bv  and concatenates
;; to itself 16 times
(define result (interpret broadcast-expr env))

(define sol?
  (synthesize
    #:forall (list  env)
    #:guarantee 
    (begin 
      (assert
        (equal?   result (interpret bounded-grammar env))
        )
      )
    ) 
  )

(displayln "Synthesizing Complete!")
(define satisfiable? (sat? sol?))

(define materialize 
  (if satisfiable? 
    (evaluate bounded-grammar sol?)
    '()
    )
  )

(displayln "Synthesized solution")
(println materialize)

[RafaeNoor]

Hey Emina, I'll share the implementation of the method below:

 (define (broadcast-impl  a %vectsize %lanesize1 %lanesize2 %elemsize %laneoffset %arg0 %arg1 )
   (define dst
      (apply
        concat
       (for/list ([%outer.it (reverse (range 0 %vectsize %lanesize1))]) ; 0 256 256 => 1
                 (apply
                    concat
                    (for/list ([j0.new (reverse (range %laneoffset %lanesize2 %elemsize))]) ; 0 256 16 => 16
                             (define %lastidx1 (-  %elemsize  1)) ; 15
                           (define %highidx0 (+  %lastidx1  %arg0)) ; 15 + 0 = 15
                            (define %1 (extract  %highidx0 %arg0 a)) ; 15 0 => first 16 bits
                            %1
                            )
                  )
                )
      )
     )
  dot
   )

[emina]

Yes, the problem is in broadcast-impl: it uses unsafe (unlifted) constructs, in this case for/list and range.

Specifically, range will error if %vectsize and/or %lanesize1 are symbolic. You can add a printf expression to this procedure and see that they are symbolic in your original implementation, because the two invocations of BROADCAST get merged into a single value during the construction of bounded-grammar. This happens because the BROADCAST struct is transparent. And then, because range errors unconditionally, there is no way to synthesize a solution that avoids the error.

When you introduce a second struct, the invocations are merged into a symbolic union instead, which gets destructed by the interpreter, so the values remain concrete when they are passed to the range function in broadcast-impl. You can achieve this effect without a second struct, by adding the #:mutable annotation to BROADCAST.

The above solution is fragile though. It will work only if you can be sure that the arguments to range will never get symbolic (i.e., the corresponding fields of BROADCAST will always be concrete).

A good way to debug these issues is to use the error tracer.

[RafaeNoor]

I didn't realise that Rosette was treating the concrete parameters as symbolic values! In our use case, the parameters will always be constant values so I believe adding #:mutable will do. Thank you for the answer. I'll definitely look into the error tracer tool too.