symtrace webserver terminates before instrumenting code and providing output

[gparmer]

Problem

The symtrace webserver exits before the webpage client can retrieve information about instrumented execution. Thus, I can't get the symtrace output.

Details

When using raco symtrace prog.rkt, the built in webserver terminates before the code is instrumented, thus the webpage client shows no information (the spinner indicates it is awaiting information from the server, and no rows are shown). Below is the ouput for the automaton.rkt program. The same behavior happens when run on a program that [assert]s out as well.

$ cd ~/.local/share/racket/8.6/pkgs/rosette/sdsl/fsm/
$ raco symtrace automaton.rkt 
Your Web application is running at http://localhost:8000/?port=8048&title=automaton.rkt.
Stop this program at any time to terminate the Web Server.

Web Server stopped.
INSTRUMENTING #<path:/home/gparmer/.local/share/racket/8.6/pkgs/rosette/sdsl/fsm/automaton.rkt>

Note that I did not control-C out, or provide any keyboard input. The "Web Server stopped." without any input from me.

Using the javascript debugger, I've confirmed that no response is provided by the webserver to the GET request of the browser.

My guess: It looks to me like the builtin webserver is bombing out soon after being started.

Do I have to use the provided alpine container to use raco symtrace?

System Information

$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.5 LTS
Release:        20.04
Codename:       focal

$ racket --version
Welcome to Racket v8.6 [cs].

rep version ~/.local/share/racket/8.6/pkgs/rosette/info.rkt
               ("racket" #:version "8.1")
(define version "4.0")

I installed rosette with raco pkg install rosette.

Note that there shouldn't be any contention of the webserver's port.

$ lsof -i :8000
<returns nothing>

[gparmer]

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.

[sorawee]

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.

[gparmer]

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.

[sorawee]

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

[gparmer]

Very much appreciated. Closing.