Skip to content

emina/rosette

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

* Fix unintentional value retain

To quote to the documentation of parameters
(https://docs.racket-lang.org/reference/parameters.html),

> as far as the memory manager is concerned,
> the value originally associated with a parameter through parameterize
> remains reachable as long the continuation is reachable,
> even if the parameter is mutated.

The parameter current-terms is initialized and/or parameterized to a
strong hash, making it not possible to GC the hash.
This PR fixes the issue by initializing and/or parameterizing to #f
first, and then mutates the parameter to a desired value later.

Fixes #247
d3c7abf

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

The Rosette Language

Tests

Rosette is a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more. This repository includes the source code for Rosette, as well as several example solver-aided DSLs.

Installing Rosette

The easiest way to install Rosette is from Racket's package manager:

  • Download and install Racket 8.1 or later from http://racket-lang.org

  • Use Racket's raco tool to install Rosette:

    $ raco pkg install rosette

Installing from source

Alternatively, you can install Rosette from source:

  • Download and install Racket 8.1 or later from http://racket-lang.org

  • Clone the rosette repository:

    $ git clone https://github.com/emina/rosette.git

  • Uninstall any previous versions of Rosette:

    $ raco pkg remove rosette

  • Use Racket's raco tool to install Rosette:

    $ cd rosette
    $ raco pkg install

Executing Rosette programs

  • Open the target program in DrRacket (e.g., rosette/sdsl/fsm/demo.rkt) and hit run!

  • DrRacket is the preferred way to execute Rosette programs. If you need to use the command line, make sure to first compile the program:

    $ raco make <your program>
    $ racket <your program>

Available languages

  • Rosette ships with two languages: #lang rosette/safe and #lang rosette.

  • The rosette/safe language includes only constructs that are safe to use with symbolic values. This (for now) excludes some nice Racket features, such as iteration constructs. The semantics of these constructs can be expressed in the core language, however, so no expressiveness is lost (just convenience). It is recommended for new users of Rosette to start with the rosette/safe language. To see the list of syntactic forms and procedures provided by rosette/safe, type the following into the Rosette REPL:

    > (rosette)
    '(define assert let let* ...)

  • The rosette language includes all of Racket. This places the burden on the programmer to decide whether a given Racket construct (which is not overridden by Rosette) is safe to use in a given context. Rosette provides no guarantees or checks for programs that use unsafe constructs. In the best case, such a program will fail with an exception if a symbolic value flows to a construct that does not support it. In the worst case, it will continue executing with incorrect semantics or cause more serious problems (e.g., data loss if it writes to a file).

  • For more on using Rosette, see The Rosette Guide. Rosette's internals are described in this PLDI'14 paper.