Comments (4)
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)
from rosette.
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
)
from rosette.
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 destruct
ed 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.
from rosette.
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.
from rosette.
Related Issues (20)
- Support cvc5 HOT 2
- Recent change breaks Rosette on the package server HOT 1
- defining a prop before verify results in different behavior than just verify HOT 2
- symtrace webserver terminates before instrumenting code and providing output HOT 5
- Unintentional value retain
- Minimization causes read-solution: unrecognized solver output: (error line 262 column 10: maximization suspended) HOT 1
- Does not work on M1 Mac because the bundled z3 is not compatible HOT 2
- Symbolical conditions produce incorrect results in classes HOT 1
- Symbolic error tracing issue in recursive function for rosette synthesis HOT 8
- Adding Custom Floating Point Support HOT 3
- `raco symtrace` could use idiomatic `--` flag to indicate the end of symtrace flags/beginning of script-under-test flags HOT 2
- Call/cc support? HOT 2
- Bitwuzla converts 1-bit bitvectors to bools (similar to what boolector does) HOT 1
- Unknown sort 'Int' when using `QF_NRA theory
- choose* ing from list of unknown length HOT 2
- EOF error when running multiple programs with `synthesize` queries HOT 5
- Incompatible with z3 (4.8.12-3.1) version shipped in Debian Bookworm HOT 3
- EOF error when using bitwuzla HOT 5
- Confusing synthesizer behavior (choosing integers vs. forms) HOT 6
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from rosette.