symtrace webserver terminates before instrumenting code and providing output about rosette HOT 5 CLOSED

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:

1. 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.
2. However, demo.rkt also doesn't show anything, and that appears to be because there is really no exception occurred during symbolic evaluation.
3. "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.
4. 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

1. 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)))

2. 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.