Comments (5)
raco symtrace
by default doesn't run the test
submodule ((module+ test ...)
). To run it, you need to invoke it with the -m
option. I.e. raco symtrace -m test <your-file.rkt>
.
from rosette.
I forgot to say: thank you so much for rosette and for maintaining it! Great, amazing tool. I'm having a wonerful time using it. My productivity at this point is hampered by not being able to introspect on assertions, but I'm really impressed with the system. As someone who oversees large code bases in academia, I'm really impressed with rosette.
from rosette.
A couple of things:
automaton.rkt
has nothing to run. The file simply declares many functions, but it doesn't really execute anything.demo.rkt
is the actual entrypoint.- However,
demo.rkt
also doesn't show anything, and that appears to be because there is really no exception occurred during symbolic evaluation. - "Web Server stopped." is totally expected. The web server is only needed to launch the initial page, so it shuts down right after that. Rosette does continue to communicate with the page via the WebSocket protocol.
- Try some examples in https://docs.racket-lang.org/rosette-guide/ch_error-tracing.html to see how
symtrace
works.
from rosette.
Thanks! Indeed, you're right that the following does result in useful symtrace output. (I include this below as the example on the webpage is almost, but not quite, self-contained).
The examples I'm using are much larger and are generated by Serval. Given your feedback, I'm hacked my examples apart and found that
- symtrace does not run properly with:
;; ... lots of code, and included symbex of C code including the check-retype-from-untyped function
(define cos-tests
(test-suite+ "Tests for cos.c"
(test-case+ "check-retype-from-untyped" (check-retype-from-untyped))))
(module+ test
(time (run-tests cos-tests)))
- symtrace gives feedback for assertions when I remove the test harness above and instead directly do:
(check-retype-from-untyped)
Given this, I'm guessing the test harness code for serval or rackunit doesn't play well with symtrace in some way (e.g. code pulled in from https://github.com/uw-unsat/serval/blob/master/serval/lib/unittest.rkt#L49). I'm assuming the issue is with the serval and/or unit test harness, not Rosette, so I believe we can close this issue.
I'm happy to provide any information you may like, but I believe we can close the issue. I can't thank you enough for your guidance.
Example that works with symtrace
derived from Rosette Guide
#lang rosette/safe
(define-symbolic xs integer? #:length 4)
(define (select xs n)
(cond
[(empty? xs) (assert #f "unexpected empty list")]
[else (define pivot (first xs))
(define non-pivot (rest xs))
(define <pivot (filter (λ (x) (< x pivot)) non-pivot))
(define >=pivot (filter (λ (x) (>= x pivot)) non-pivot))
(define len< (length <pivot))
(cond
[(= n len<) pivot]
[(< n len<) (select <pivot)] ; Bug: should be (select <pivot n).
[else (select >=pivot (- n len< 1))])]))
(define-symbolic n k integer?)
(assume
(and (<= 0 n (sub1 (length xs)))
(= k (select xs n))))
(verify
(assert (= k (list-ref (sort xs <) n))))
Included for completeness.
from rosette.
Very much appreciated. Closing.
from rosette.
Related Issues (20)
- Support cvc5 HOT 2
- Recent change breaks Rosette on the package server HOT 1
- Synthesising with Grammar containing multiple instances of structs with different parameters returns unsat HOT 4
- defining a prop before verify results in different behavior than just verify HOT 2
- 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.