Compare commits
No commits in common. "xenia/patches" and "4.0" have entirely different histories.
xenia/patc
...
4.0
|
|
@ -1,6 +0,0 @@
|
|||
version: 2
|
||||
updates:
|
||||
- package-ecosystem: "github-actions"
|
||||
directory: "/"
|
||||
schedule:
|
||||
interval: "daily"
|
||||
|
|
@ -1,50 +0,0 @@
|
|||
name: Docker
|
||||
|
||||
on:
|
||||
push:
|
||||
tags:
|
||||
- '*'
|
||||
branches:
|
||||
- master
|
||||
pull_request:
|
||||
|
||||
jobs:
|
||||
docker:
|
||||
runs-on: ubuntu-latest
|
||||
|
||||
steps:
|
||||
- name: Clone Repository
|
||||
uses: actions/checkout@v4
|
||||
|
||||
- name: Configure Docker Metadata
|
||||
id: meta
|
||||
uses: docker/metadata-action@v5
|
||||
with:
|
||||
images: ghcr.io/${{ github.repository }}
|
||||
tags: |
|
||||
type=ref,event=branch
|
||||
type=ref,event=pr
|
||||
type=ref,event=tag
|
||||
type=semver,pattern={{version}}
|
||||
type=semver,pattern={{major}}.{{minor}}
|
||||
|
||||
- name: Authenticate to Package Registry
|
||||
uses: docker/login-action@v3
|
||||
if: ${{ github.event_name != 'pull_request' }}
|
||||
with:
|
||||
registry: ghcr.io
|
||||
username: ${{ github.actor }}
|
||||
password: ${{ secrets.GITHUB_TOKEN }}
|
||||
|
||||
- name: Set up Docker Buildx
|
||||
uses: docker/setup-buildx-action@v3
|
||||
|
||||
- name: Build and Publish Rosette Image
|
||||
uses: docker/build-push-action@v6
|
||||
with:
|
||||
context: .
|
||||
push: ${{ github.event_name != 'pull_request' }}
|
||||
tags: ${{ steps.meta.outputs.tags }}
|
||||
labels: ${{ steps.meta.outputs.labels }}
|
||||
cache-from: type=gha
|
||||
cache-to: type=gha,mode=max
|
||||
|
|
@ -5,16 +5,12 @@ on: [push, pull_request]
|
|||
env:
|
||||
CVC4_URL: "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt"
|
||||
BOOLECTOR_URL: "https://github.com/Boolector/boolector/archive/3.2.1.tar.gz"
|
||||
CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.7/cvc5-Linux"
|
||||
BITWUZLA_URL: "https://github.com/bitwuzla/bitwuzla/archive/93a3d930f622b4cef0063215e63b7c3bd10bd663.tar.gz"
|
||||
STP_URL: "https://github.com/stp/stp/archive/d70085462f07c8a5a2f1225f727cda3ef505b141.tar.gz"
|
||||
YICES2_URL: "https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz"
|
||||
|
||||
jobs:
|
||||
test:
|
||||
strategy:
|
||||
matrix:
|
||||
racket-version: ['8.1', 'current']
|
||||
racket-version: ['8.0', 'current']
|
||||
racket-variant: ['CS']
|
||||
allow-failure: [false]
|
||||
name: Racket ${{ matrix.racket-version }} (${{ matrix.racket-variant }})
|
||||
|
|
@ -23,14 +19,12 @@ jobs:
|
|||
steps:
|
||||
- uses: actions/checkout@master
|
||||
- name: Setup Racket
|
||||
uses: Bogdanp/setup-racket@v1.14
|
||||
uses: Bogdanp/setup-racket@v1.1
|
||||
with:
|
||||
architecture: x64
|
||||
version: ${{ matrix.racket-version }}
|
||||
variant: ${{ matrix.racket-variant }}
|
||||
- name: Install solvers
|
||||
# Note that setting LD_LIBRARY_PATH can be removed once this bug is
|
||||
# fixed: https://github.com/stp/stp/issues/485
|
||||
run: |
|
||||
mkdir bin &&
|
||||
wget $CVC4_URL -nv -O bin/cvc4 &&
|
||||
|
|
@ -46,50 +40,7 @@ jobs:
|
|||
make &&
|
||||
popd &&
|
||||
cp boolector/build/bin/boolector bin/ &&
|
||||
rm -rf boolector* &&
|
||||
wget $CVC5_URL -nv -O bin/cvc5 &&
|
||||
chmod +x bin/cvc5 &&
|
||||
sudo apt-get update &&
|
||||
sudo apt-get install -y ninja-build &&
|
||||
pip3 install meson &&
|
||||
wget $BITWUZLA_URL -nv -O bitwuzla.tar.gz &&
|
||||
mkdir bitwuzla &&
|
||||
tar xzf bitwuzla.tar.gz -C bitwuzla --strip-components=1 &&
|
||||
pushd bitwuzla &&
|
||||
./configure.py &&
|
||||
pushd build &&
|
||||
ninja &&
|
||||
popd &&
|
||||
popd &&
|
||||
cp bitwuzla/build/src/main/bitwuzla bin/ &&
|
||||
sudo apt-get install -y build-essential git cmake bison flex libboost-all-dev libtinfo-dev python3 perl &&
|
||||
wget $STP_URL -nv -O stp.tar.gz &&
|
||||
mkdir stp &&
|
||||
tar xzf stp.tar.gz -C stp --strip-components=1 &&
|
||||
pushd stp &&
|
||||
echo "LD_LIBRARY_PATH=$PWD/deps/cadical/build:$PWD/deps/cadiback/:$LD_LIBRARY_PATH" >> $GITHUB_ENV &&
|
||||
./scripts/deps/setup-gtest.sh &&
|
||||
./scripts/deps/setup-outputcheck.sh &&
|
||||
./scripts/deps/setup-cms.sh &&
|
||||
./scripts/deps/setup-minisat.sh &&
|
||||
mkdir build &&
|
||||
pushd build &&
|
||||
cmake .. &&
|
||||
cmake --build . &&
|
||||
popd &&
|
||||
popd &&
|
||||
ln -s stp/build/stp bin/stp &&
|
||||
sudo apt-get install -y gperf &&
|
||||
wget $YICES2_URL -nv -O yices2.tar.gz &&
|
||||
mkdir yices2 &&
|
||||
tar xvf yices2.tar.gz -C yices2 --strip-components=1 &&
|
||||
pushd yices2 &&
|
||||
autoconf &&
|
||||
./configure --prefix=$PWD/out/ &&
|
||||
make &&
|
||||
make install &&
|
||||
popd &&
|
||||
cp yices2/out/bin/yices-smt2 bin/yices-smt2
|
||||
rm -rf boolector*
|
||||
- name: Install Rosette
|
||||
run: raco pkg install --auto --name rosette
|
||||
- name: Compile Rosette tests
|
||||
|
|
|
|||
97
Dockerfile
97
Dockerfile
|
|
@ -1,97 +0,0 @@
|
|||
FROM alpine:3.15
|
||||
|
||||
## ========================== [ Install Racket ] =========================== ##
|
||||
|
||||
## Define default Racket version and variant. The Racket version is of the form
|
||||
## <major>.<minor>. The variant can be "cs" (Chez Scheme), "bc" (Before Chez) or
|
||||
## "natipkg" (where external libraries are included in the Racket packages).
|
||||
##
|
||||
ARG RACKET_VERSION=8.4
|
||||
ARG RACKET_VARIANT=cs
|
||||
|
||||
## Install Racket. We first install system dependencies: [gcompat] is needed for
|
||||
## Racket and [ncurses] is needed for the [xrepl] and [expeditor] packages,
|
||||
## providing the REPL. We then download the installer, run it with the right
|
||||
## parameters, then remove it. After that, all that remains is to set-up the
|
||||
## Racket packages and install [expeditor]. See later for a description of the
|
||||
## arguments to [raco pkg install].
|
||||
##
|
||||
RUN apk add --no-cache gcompat ncurses
|
||||
RUN wget "https://download.racket-lang.org/installers/${RACKET_VERSION}/racket-minimal-${RACKET_VERSION}-x86_64-linux-${RACKET_VARIANT}.sh"
|
||||
RUN echo 'yes\n1\n' | sh racket-minimal-${RACKET_VERSION}-x86_64-linux-${RACKET_VARIANT}.sh --create-dir --unix-style --dest /usr/
|
||||
RUN rm racket-minimal-${RACKET_VERSION}-x86_64-linux-${RACKET_VARIANT}.sh
|
||||
RUN raco setup --no-docs
|
||||
RUN raco pkg install -i --batch --auto --no-docs expeditor-lib
|
||||
|
||||
## =================== [ Install Rosette's Dependencies ] =================== ##
|
||||
|
||||
## Work on Rosette's installation within /usr/local. This directory will be
|
||||
## cleaned up later on so it could be anything.
|
||||
##
|
||||
WORKDIR /usr/local/rosette
|
||||
|
||||
## Get all the info.rkt files. Trying to install Rosette based only on these
|
||||
## files would fail, but we can use them to only install dependencies.
|
||||
##
|
||||
COPY info.rkt .
|
||||
COPY rosette/info.rkt rosette/
|
||||
|
||||
## Install only Rosette's dependencies. We have to install the external
|
||||
## dependencies [libstdc++] and [libgcc] because Z3 needs them at runtime. As
|
||||
## for the Racket dependencies only, we achieve that in three steps:
|
||||
##
|
||||
## 1. We use [raco pkg install --no-setup] to download and register Rosette
|
||||
## and all its dependencies without setting them up, that is without
|
||||
## compiling them. At this point, the system is in an inconsistent state,
|
||||
## where packages are registered but not actually present. The other flags
|
||||
## are the following:
|
||||
##
|
||||
## -i install packages for all users
|
||||
## --batch disable interactive mode and suppress prompts
|
||||
## --auto download missing packages automatically
|
||||
##
|
||||
## 2. We use [raco pkg remove --no-setup] to unregister Rosette. This keeps
|
||||
## the dependencies as registered. The system is still in an inconsistent
|
||||
## state. See above for the flags.
|
||||
##
|
||||
## 3. We use [raco setup] to set up all the registered package. This brings
|
||||
## the system back in a consistent state. Since Rosette's dependencies were
|
||||
## registered but not Rosette itself, this achieves our goal. The flags are
|
||||
## the following:
|
||||
##
|
||||
## --fail-fast fail on the first error encountered
|
||||
## --no-docs do not compile the documentations
|
||||
##
|
||||
RUN apk add --no-cache libstdc++ libgcc
|
||||
RUN raco pkg install -i --batch --auto --no-setup ../rosette
|
||||
RUN raco pkg remove -i --no-setup rosette
|
||||
RUN raco setup --fail-fast --no-docs
|
||||
|
||||
## ========================== [ Install Rosette ] =========================== ##
|
||||
|
||||
## Get all of Rosette; build and install it. The dependencies should all be
|
||||
## installed, so we can remove the --auto flag which will lead us to failure if
|
||||
## a dependency cannot be found. The additional flags are the following:
|
||||
##
|
||||
## --copy copy content to install path (instead of linking)
|
||||
##
|
||||
COPY . .
|
||||
RUN raco pkg install -i --batch --copy --no-docs ./rosette
|
||||
RUN rm -R /usr/local/rosette
|
||||
|
||||
## ===================== [ Prepare Clean Entry Point ] ====================== ##
|
||||
|
||||
## For further use of the image, we can start with user `rosette`, group
|
||||
## `rosette` in `/rosette` by default.
|
||||
##
|
||||
RUN addgroup rosette
|
||||
RUN adduser --system --shell /bin/false --disabled-password \
|
||||
--home /rosette --ingroup rosette rosette
|
||||
RUN chown -R rosette:rosette /rosette
|
||||
USER rosette
|
||||
WORKDIR /rosette
|
||||
|
||||
## Rosette files are simply Racket files using the Rosette library: the default
|
||||
## entry point of this image is therefore the Racket executable.
|
||||
##
|
||||
ENTRYPOINT ["/usr/bin/racket", "-I", "rosette"]
|
||||
16
NOTES.md
16
NOTES.md
|
|
@ -1,17 +1,13 @@
|
|||
# Release Notes
|
||||
|
||||
## Version 4.1
|
||||
|
||||
This is a minor bug-fixing release.
|
||||
|
||||
## Version 4.0
|
||||
|
||||
This is a major release with significant changes to the language and the runtime. Rosette 4.0 is *not backward compatible* with Rosette 3.x. But porting Rosette 3.x code to Rosette 4.0 should be straightforward for most applications.
|
||||
|
||||
This release includes the following features:
|
||||
|
||||
- Support for assumptions (see `assume`).
|
||||
- New symbolic evaluation core that tracks verification conditions (VCs) rather than path conditions and assertions.
|
||||
- Support for assumptions (see `assume`).
|
||||
- New symbolic evaluation core that tracks verification conditions (VCs) rather than path conditions and assertions.
|
||||
- New symbolic reflection constructs for working with VCs, including `vc`, `with-vc`, and `clear-vc!`.
|
||||
- New symbolic reflection facilities for managing symbolic `terms`, including the option of using a garbage-collected data structure.
|
||||
- Updated `verify`, `synthesize`, `solve`, and `optimize` queries.
|
||||
|
|
@ -22,7 +18,7 @@ This release includes the following features:
|
|||
The following features have been removed:
|
||||
|
||||
- The `debug` query.
|
||||
- Reflection facilities for working with path conditions and assertions: `pc`, `with-asserts`, `with-asserts-only`, `clear-asserts!`, and `asserts`.
|
||||
- Reflection facilities for working with path conditions and assertions: `pc`, `with-asserts`, `with-asserts-only`, `clear-asserts!`, and `asserts`.
|
||||
- Support for CPLEX.
|
||||
|
||||
## Version 3.2
|
||||
|
|
@ -33,11 +29,11 @@ This release includes minor updates and a new [value destructuring library].
|
|||
|
||||
## Version 3.1
|
||||
|
||||
This release includes bug fixes and updates Rosette to use the latest version of Z3 as its default SMT solver.
|
||||
This release includes bug fixes and updates Rosette to use the latest version of Z3 as its default SMT solver.
|
||||
|
||||
This release also includes the following new functionality contributed by [Sorawee Porncharoenwase][]:
|
||||
|
||||
- An interactive [value browser][] to help programmers navigate and read complex symbolic values.
|
||||
- An interactive [value browser][] to help programmers navigate and read complex symbolic values.
|
||||
- An *error tracer* for finding bugs in Rosette programs that manifest as exceptions intercepted during symbolic evaluation. To use the error tracer, run the command `raco symtrace <prog>`. The [debugging][] chapter in the Rosette guide describes some common issues due to intercepted exceptions, how to test for them, and how to find them with the error tracer.
|
||||
|
||||
|
||||
|
|
@ -71,7 +67,7 @@ This release also includes the following new functionality and features contribu
|
|||
|
||||
This release includes bug fixes and the following updates:
|
||||
|
||||
- Added support for quantified formulas. Quantifiers can appear in assertions passed to `solve` and `verify` queries. They should not be used with `synthesize` queries. When using quantified formulas, `current-bitwidth` must be set to `#f`.
|
||||
- Added support for quantified formulas. Quantifiers can appear in assertions passed to `solve` and `verify` queries. They should not be used with `synthesize` queries. When using quantified formulas, `current-bitwidth` must be set to `#f`.
|
||||
- Added the `unknown` solution type. An `unknown` solution is returned if the underlying solver cannot decide if a given set of constraints is (un)satisfiable.
|
||||
- Added the `distinct?` predicate that returns true iff all of its arguments are pairwaise un-equal. This has a direct (efficient) translation to Z3 if the arguments are primitive solvable values (booleans, integers, reals, or bitvectors).
|
||||
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ The Rosette Language
|
|||
|
||||
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
|
||||
* Download and install Racket 8.0 or later from http://racket-lang.org
|
||||
|
||||
* Use Racket's `raco` tool to install Rosette:
|
||||
|
||||
|
|
@ -19,7 +19,7 @@ The easiest way to install Rosette is from Racket's package manager:
|
|||
|
||||
Alternatively, you can install Rosette from source:
|
||||
|
||||
* Download and install Racket 8.1 or later from http://racket-lang.org
|
||||
* Download and install Racket 8.0 or later from http://racket-lang.org
|
||||
|
||||
* Clone the rosette repository:
|
||||
|
||||
|
|
|
|||
2
info.rkt
2
info.rkt
|
|
@ -5,7 +5,7 @@
|
|||
(define deps '("custom-load"
|
||||
"sandbox-lib"
|
||||
"scribble-lib"
|
||||
("racket" #:version "8.1")
|
||||
("racket" #:version "8.0")
|
||||
"r6rs-lib"
|
||||
"rfc6455"
|
||||
"net-lib"
|
||||
|
|
|
|||
|
|
@ -33,7 +33,6 @@
|
|||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||
@bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||
@concat @extract @sign-extend @zero-extend
|
||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
||||
@integer->bitvector @bitvector->integer @bitvector->natural
|
||||
; core/bvlib.rkt
|
||||
bit lsb msb bvzero? bvadd1 bvsub1
|
||||
|
|
|
|||
|
|
@ -14,19 +14,20 @@
|
|||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||
@bvneg @bvadd @bvsub @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||
@concat @extract @sign-extend @zero-extend
|
||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
||||
@integer->bitvector @bitvector->integer @bitvector->natural)
|
||||
|
||||
;; ----------------- Bitvector Types ----------------- ;;
|
||||
|
||||
; Cache of all bitvector types constructed so far, mapping sizes to types.
|
||||
(define bitvector-types (make-hasheq))
|
||||
(define bitvector-types (make-hash))
|
||||
|
||||
; Returns the bitvector type of the given size.
|
||||
(define (bitvector-type size)
|
||||
(assert (and (exact-positive-integer? size) (fixnum? size))
|
||||
(argument-error 'bitvector "(and/c exact-positive-integer? fixnum?)" size))
|
||||
(hash-ref! bitvector-types size (λ () (bitvector size))))
|
||||
(assert (exact-positive-integer? size) (argument-error 'bitvector "exact-positive-integer?" size))
|
||||
(or (hash-ref bitvector-types size #f)
|
||||
(let ([t (bitvector size)])
|
||||
(hash-set! bitvector-types size t)
|
||||
t)))
|
||||
|
||||
; Represents a bitvector type.
|
||||
(struct bitvector (size)
|
||||
|
|
@ -339,13 +340,6 @@
|
|||
(ite (bveq (bv 0 t) (bvand x (bv (bvsmin t) t))) (bv 0 t) (bv -1 t))]
|
||||
[(_ _) (expression @bvashr x y)]))
|
||||
|
||||
|
||||
(define (z3_ext_rotate_left x y)
|
||||
(expression @z3_ext_rotate_left x y))
|
||||
|
||||
(define (z3_ext_rotate_right x y)
|
||||
(expression @z3_ext_rotate_right x y))
|
||||
|
||||
(define-lifted-operator @bvnot bvnot T*->T)
|
||||
(define-lifted-operator @bvand bvand T*->T)
|
||||
(define-lifted-operator @bvor bvor T*->T)
|
||||
|
|
@ -353,8 +347,6 @@
|
|||
(define-lifted-operator @bvshl bvshl T*->T)
|
||||
(define-lifted-operator @bvlshr bvlshr T*->T)
|
||||
(define-lifted-operator @bvashr bvashr T*->T)
|
||||
(define-lifted-operator @z3_ext_rotate_left z3_ext_rotate_left T*->T)
|
||||
(define-lifted-operator @z3_ext_rotate_right z3_ext_rotate_right T*->T)
|
||||
|
||||
;; ----------------- Simplification ruules for bitwise operators ----------------- ;;
|
||||
|
||||
|
|
@ -603,7 +595,7 @@
|
|||
_))
|
||||
(if (< i size)
|
||||
(extract i j a)
|
||||
(expression @bvop a (bitvector-type (add1 i))))]
|
||||
(expression @bvop a (bitvector (add1 i))))]
|
||||
[(_ _ _) (expression @extract i j x)]))
|
||||
|
||||
(define-operator @extract
|
||||
|
|
|
|||
|
|
@ -152,7 +152,7 @@
|
|||
(match* ((car p) (cdr p))
|
||||
[(a (expression (== ite) a x _)) (cons a x)]
|
||||
[(a (expression (== ite) (expression (== @!) a) _ x)) (cons a x)]
|
||||
[((and (expression (== @!) a) !a) (expression (== ite) a _ x)) (cons !a x)]
|
||||
[((expression (== @!) a) (expression (== ite) a _ x)) (cons a x)]
|
||||
[(_ _) p]))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -19,12 +19,7 @@
|
|||
; These IDs are never reused, and they are used to impose an ordering on the children
|
||||
; of expressions with commutative operators.
|
||||
#|-----------------------------------------------------------------------------------|#
|
||||
|
||||
;; Initialize with #f so that the hash table cooperates with garbage collector.
|
||||
;; See #247
|
||||
(define current-terms (make-parameter #f))
|
||||
(current-terms (make-hash))
|
||||
|
||||
(define current-terms (make-parameter (make-hash)))
|
||||
(define current-index (make-parameter 0))
|
||||
|
||||
; Clears the entire term cache if invoked with #f (default), or
|
||||
|
|
@ -82,23 +77,17 @@
|
|||
; restores (terms) to its old value. If terms-expr is not given, it defaults to
|
||||
; (terms), so (with-terms expr) is equivalent to (with-terms (terms) expr).
|
||||
(define-syntax (with-terms stx)
|
||||
;; Parameterize with #f so that the hash table cooperates with garbage collector.
|
||||
;; See #247
|
||||
(syntax-parse stx
|
||||
[(_ expr)
|
||||
#'(let ([orig-terms (current-terms)])
|
||||
(parameterize ([current-terms #f])
|
||||
(current-terms (hash-copy orig-terms))
|
||||
expr))]
|
||||
#'(parameterize ([current-terms (hash-copy (current-terms))])
|
||||
expr)]
|
||||
[(_ terms-expr expr)
|
||||
#'(let ([orig-terms (current-terms)])
|
||||
(parameterize ([current-terms #f])
|
||||
(current-terms (hash-copy-clear orig-terms))
|
||||
(let ([ts terms-expr]
|
||||
[cache (current-terms)])
|
||||
(for ([t ts])
|
||||
(hash-set! cache (term-val t) t))
|
||||
expr)))]))
|
||||
#'(parameterize ([current-terms (hash-copy-clear (current-terms))])
|
||||
(let ([ts terms-expr]
|
||||
[cache (current-terms)])
|
||||
(for ([t ts])
|
||||
(hash-set! cache (term-val t) t))
|
||||
expr))]))
|
||||
|
||||
|
||||
|
||||
|
|
@ -132,21 +121,14 @@
|
|||
(define (term<? s1 s2) (< (term-ord s1) (term-ord s2)))
|
||||
|
||||
(define-syntax-rule (make-term term-constructor args type rest ...)
|
||||
(let ([val args]
|
||||
[ty type])
|
||||
(define cached (hash-ref (current-terms) val #f))
|
||||
(cond
|
||||
[cached
|
||||
(unless (equal? (term-type cached) ty)
|
||||
(error 'define-symbolic "type should remain unchanged"))
|
||||
cached]
|
||||
[else
|
||||
(define ord (current-index))
|
||||
(define out (term-constructor val ty ord rest ...))
|
||||
(current-index (add1 ord))
|
||||
((current-reporter) 'new-term out)
|
||||
(hash-set! (current-terms) val out)
|
||||
out])))
|
||||
(let ([val args])
|
||||
(or (hash-ref (current-terms) val #f)
|
||||
(let* ([ord (current-index)]
|
||||
[out (term-constructor val type ord rest ...)])
|
||||
(current-index (add1 ord))
|
||||
((current-reporter) 'new-term out)
|
||||
(hash-set! (current-terms) val out)
|
||||
out))))
|
||||
|
||||
(define (make-const id t)
|
||||
(unless (and (type? t) (solvable? t))
|
||||
|
|
|
|||
|
|
@ -43,8 +43,8 @@
|
|||
[type-cast type val [caller]] ; (-> type? any/c symbol? any/c)
|
||||
[type-name type] ; (-> type? symbol?)
|
||||
[type-applicable? type] ; (-> type? boolean?)
|
||||
[type-eq? type u v] ; (-> type? any/c any/c @boolean?)
|
||||
[type-equal? type u v] ; (-> type? any/c any/c @boolean?)
|
||||
[type-eq? type u v] ; (-> type? (-> any/c any/c @boolean?)))
|
||||
[type-equal? type u v] ; (-> type? (-> any/c any/c @boolean?)))
|
||||
[type-compress type force? ps] ; (-> type? (listof (cons @boolean? any/c)) (listof (cons @boolean? any/c)))
|
||||
[type-construct type vals] ; (-> type? (listof any/c) any/c)
|
||||
[type-deconstruct type val]) ; (-> type? any/c (listof any/c))
|
||||
|
|
|
|||
|
|
@ -140,7 +140,7 @@ equality (@racket[bveq]) and signed / unsigned versions of
|
|||
[(bvor [x (bitvector n)] ...+) (bitvector n)]
|
||||
[(bvxor [x (bitvector n)] ...+) (bitvector n)])]{
|
||||
|
||||
Returns the bitwise ``and'', ``or'', ``xor'' of one or more bitvector values of the same type.
|
||||
Returns the bitwise "and", "or", "xor" of one or more bitvector values of the same type.
|
||||
|
||||
@examples[#:eval rosette-eval
|
||||
(bvand (bv -1 4) (bv 2 4))
|
||||
|
|
@ -434,7 +434,7 @@ leads to faster solving times.
|
|||
|
||||
@(rosette-eval '(clear-vc!))
|
||||
|
||||
@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector 1))]{
|
||||
@defproc[(bitvector->bits [x (bitvector n)]) (listof (bitvector n))]{
|
||||
|
||||
Returns the bits of @racket[x] as a list, i.e., @racket[(list (bit 0 x) ... (bit (- n 1) x))].
|
||||
|
||||
|
|
|
|||
|
|
@ -3,11 +3,7 @@
|
|||
@(require (for-label
|
||||
rosette/solver/solver rosette/solver/solution
|
||||
rosette/solver/smt/z3 rosette/solver/smt/cvc4
|
||||
rosette/solver/smt/boolector
|
||||
rosette/solver/smt/bitwuzla
|
||||
rosette/solver/smt/cvc5
|
||||
rosette/solver/smt/stp
|
||||
rosette/solver/smt/yices
|
||||
rosette/solver/smt/boolector rosette/solver/smt/yices
|
||||
rosette/base/form/define rosette/query/query
|
||||
rosette/base/core/term (only-in rosette/base/base bv?)
|
||||
(only-in rosette/base/base assert)
|
||||
|
|
@ -25,11 +21,8 @@
|
|||
rosette/solver/solution
|
||||
rosette/solver/smt/z3
|
||||
rosette/solver/smt/cvc4
|
||||
rosette/solver/smt/boolector
|
||||
rosette/solver/smt/bitwuzla
|
||||
rosette/solver/smt/cvc5
|
||||
rosette/solver/smt/stp
|
||||
rosette/solver/smt/yices
|
||||
rosette/solver/smt/boolector
|
||||
#:use-sources
|
||||
(rosette/query/finitize
|
||||
rosette/query/query
|
||||
|
|
@ -37,11 +30,8 @@
|
|||
rosette/solver/solution
|
||||
rosette/solver/smt/z3
|
||||
rosette/solver/smt/cvc4
|
||||
rosette/solver/smt/boolector
|
||||
rosette/solver/smt/bitwuzla
|
||||
rosette/solver/smt/cvc5
|
||||
rosette/solver/smt/stp
|
||||
rosette/solver/smt/yices)]
|
||||
rosette/solver/smt/yices
|
||||
rosette/solver/smt/boolector)]
|
||||
|
||||
A @deftech{solver} is an automatic reasoning engine, used to answer
|
||||
@seclink["sec:queries"]{queries} about Rosette programs. The result of
|
||||
|
|
@ -291,146 +281,37 @@ Returns true if the Boolector solver is available for use (i.e., Rosette can loc
|
|||
If this returns @racket[#f], @racket[(boolector)] will not succeed
|
||||
without its optional @racket[path] argument.}
|
||||
|
||||
@subsection{Bitwuzla}
|
||||
|
||||
@defmodule[rosette/solver/smt/bitwuzla #:no-declare]
|
||||
|
||||
@defproc*[([(bitwuzla [#:path path (or/c path-string? #f) #f]
|
||||
[#:logic logic (or/c symbol? #f) #f]
|
||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
||||
[(bitwuzla? [v any/c]) boolean?])]{
|
||||
|
||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://bitwuzla.github.io/"]{Bitwuzla} solver.
|
||||
|
||||
To use this solver, download prebuilt Bitwuzla or build it yourself,
|
||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
||||
executable as the optional @racket[path] argument.
|
||||
Rosette currently tests Bitwuzla at commit
|
||||
@tt{93a3d930f622b4cef0063215e63b7c3bd10bd663}.
|
||||
|
||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
||||
emitted constraints fall within the chosen logic. The default is @racket[#f],
|
||||
which uses Bitwuzla's default logic.
|
||||
|
||||
The @racket[options] argument provides additional options that are sent to Bitwuzla
|
||||
via the @tt{set-option} SMT command.
|
||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
||||
will send the command @tt{(set-option :seed 5)} to Bitwuzla prior to solving.
|
||||
}
|
||||
|
||||
@defproc[(bitwuzla-available?) boolean?]{
|
||||
Returns true if the Bitwuzla solver is available for use (i.e., Rosette can locate a @tt{bitwuzla} binary).
|
||||
If this returns @racket[#f], @racket[(bitwuzla)] will not succeed
|
||||
without its optional @racket[path] argument.}
|
||||
|
||||
@subsection{CVC5}
|
||||
|
||||
@defmodule[rosette/solver/smt/cvc5 #:no-declare]
|
||||
|
||||
@defproc*[([(cvc5 [#:path path (or/c path-string? #f) #f]
|
||||
[#:logic logic (or/c symbol? #f) #f]
|
||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
||||
[(cvc5? [v any/c]) boolean?])]{
|
||||
|
||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://cvc5.github.io/"]{CVC5} solver.
|
||||
|
||||
To use this solver, download prebuilt CVC5 or build it yourself,
|
||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
||||
executable as the optional @racket[path] argument.
|
||||
Rosette currently tests CVC5 at version 1.0.7.
|
||||
|
||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
||||
emitted constraints fall within the chosen logic. The default is @racket[#f],
|
||||
which uses CVC5's default logic.
|
||||
|
||||
The @racket[options] argument provides additional options that are sent to CVC5
|
||||
via the @tt{set-option} SMT command.
|
||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
||||
will send the command @tt{(set-option :seed 5)} to CVC5 prior to solving.
|
||||
}
|
||||
|
||||
@defproc[(cvc5-available?) boolean?]{
|
||||
Returns true if the CVC5 solver is available for use (i.e., Rosette can locate a @tt{cvc5} binary).
|
||||
If this returns @racket[#f], @racket[(cvc5)] will not succeed
|
||||
without its optional @racket[path] argument.}
|
||||
|
||||
@subsection{STP}
|
||||
|
||||
@defmodule[rosette/solver/smt/stp #:no-declare]
|
||||
|
||||
@defproc*[([(stp [#:path path (or/c path-string? #f) #f]
|
||||
[#:logic logic (or/c symbol? #f) #f]
|
||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
||||
[(stp? [v any/c]) boolean?])]{
|
||||
|
||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://stp.github.io/"]{STP} solver.
|
||||
|
||||
To use this solver, download prebuilt STP or build it yourself,
|
||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
||||
executable as the optional @racket[path] argument.
|
||||
Rosette currently tests STP at commit
|
||||
@tt{0510509a85b6823278211891cbb274022340fa5c}.
|
||||
Note that as of December 2023, the STP version on Mac Homebrew is too old to be
|
||||
supported by Rosette.
|
||||
|
||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
||||
emitted constraints fall within the chosen logic. The default is @racket[#f],
|
||||
which uses STP's default logic.
|
||||
|
||||
The @racket[options] argument provides additional options that are sent to STP
|
||||
via the @tt{set-option} SMT command.
|
||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
||||
will send the command @tt{(set-option :seed 5)} to STP prior to solving.
|
||||
}
|
||||
|
||||
@defproc[(stp-available?) boolean?]{
|
||||
Returns true if the STP solver is available for use (i.e., Rosette can locate a @tt{stp} binary).
|
||||
If this returns @racket[#f], @racket[(stp)] will not succeed
|
||||
without its optional @racket[path] argument.}
|
||||
|
||||
@subsection{Yices2}
|
||||
@subsection{Yices}
|
||||
|
||||
@defmodule[rosette/solver/smt/yices #:no-declare]
|
||||
|
||||
@defproc*[([(yices [#:path path (or/c path-string? #f) #f]
|
||||
[#:logic logic (or/c symbol? #f) 'QF_BV]
|
||||
[#:logic logic symbol? 'ALL]
|
||||
[#:options options (hash/c symbol? any/c) (hash)]) solver?]
|
||||
[(yices? [v any/c]) boolean?])]{
|
||||
|
||||
Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver.
|
||||
|
||||
Returns a @racket[solver?] wrapper for the @hyperlink["http://yices.csl.sri.com/"]{Yices} solver from SRI.
|
||||
|
||||
To use this solver, download prebuilt Yices2 or build it yourself,
|
||||
and ensure the executable is on your @tt{PATH} or pass the path to the
|
||||
executable as the optional @racket[path] argument.
|
||||
Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2
|
||||
solver with its SMTLIB2 frontend enabled.
|
||||
Note that just building (without installing) Yices2 will produce an executable
|
||||
named @tt{yices_smt2}. Running the installation step produces an executable
|
||||
with the correct name. However, it is safe to skip the installation step and
|
||||
simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}.
|
||||
Rosette currently tests Yices2 at commit
|
||||
@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}.
|
||||
To use this solver, download and install Yices (version 2.6.0 or later),
|
||||
and either add the @tt{yices-smt2} executable to your @tt{PATH}
|
||||
or pass the path to the executable as the optional @racket[path] argument.
|
||||
|
||||
The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
|
||||
Specifying a logic can improve solving performance, but Rosette makes no effort to check that
|
||||
emitted constraints fall within the chosen logic. Yices2 expects a logic to be
|
||||
set; Rosette defaults to @racket['QF_BV].
|
||||
emitted constraints fall within the chosen logic. The default is @racket['ALL].
|
||||
|
||||
The @racket[options] argument provides additional options that are sent to Yices2
|
||||
The @racket[options] argument provides additional options that are sent to Yices
|
||||
via the @tt{set-option} SMT command.
|
||||
For example, setting @racket[options] to @racket[(hash ':seed 5)]
|
||||
will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
|
||||
For example, setting @racket[options] to @racket[(hash ':random-seed 5)]
|
||||
will send the command @tt{(set-option :random-seed 5)} to Yices prior to solving.
|
||||
}
|
||||
|
||||
@defproc[(yices-available?) boolean?]{
|
||||
Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
|
||||
Returns true if the Yices solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
|
||||
If this returns @racket[#f], @racket[(yices)] will not succeed
|
||||
without its optional @racket[path] argument.}
|
||||
|
||||
|
||||
@section{Solutions}
|
||||
|
||||
A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable (@racket[unsat?]),
|
||||
|
|
|
|||
|
|
@ -2,8 +2,7 @@
|
|||
|
||||
@(require (for-label
|
||||
rosette/base/form/define rosette/query/query
|
||||
rosette/base/core/term
|
||||
rosette/solver/solution
|
||||
rosette/base/core/term
|
||||
(only-in rosette/base/base assert define-symbolic union?
|
||||
vc clear-vc! bitvector bitvector? bv?
|
||||
bitvector->natural integer->bitvector
|
||||
|
|
|
|||
|
|
@ -1,21 +1,19 @@
|
|||
#lang scribble/manual
|
||||
|
||||
@(require (for-label
|
||||
racket
|
||||
(only-in racket/sandbox with-deep-time-limit)
|
||||
@(require (for-label racket (only-in racket/sandbox with-deep-time-limit))
|
||||
(for-label
|
||||
rosette/base/form/define
|
||||
rosette/query/query
|
||||
rosette/solver/solution
|
||||
(only-in rosette/base/base
|
||||
assert assume vc vc-asserts vc-assumes clear-vc!
|
||||
bv? bitvector
|
||||
(only-in rosette/base/base assert assume vc vc-asserts vc-assumes clear-vc!)
|
||||
rosette/query/query
|
||||
(only-in rosette/base/base bv? bitvector
|
||||
bvsdiv bvadd bvsle bvsub bvand
|
||||
bvor bvxor bvshl bvlshr bvashr
|
||||
bvnot bvneg)
|
||||
rosette/lib/synthax))
|
||||
|
||||
@(require racket/sandbox racket/runtime-path scribble/core scribble/racket
|
||||
scribble/example scribble/html-properties scriblib/footnote)
|
||||
@(require racket/sandbox racket/runtime-path scribble/core scribble/racket
|
||||
scribble/example scribble/html-properties scriblib/footnote
|
||||
(only-in racket [unsyntax racket/unsyntax]))
|
||||
|
||||
@(require (only-in "../refs.scrbl" ~cite rosette:onward13 rosette:pldi14)
|
||||
"../util/lifted.rkt")
|
||||
|
|
@ -142,7 +140,7 @@ Assumptions behave analogously to assertions on both concrete and symbolic value
|
|||
|
||||
@section[#:tag "sec:queries"]{Solver-Aided Queries}
|
||||
|
||||
The solver reasons about assumed and asserted properties only when we ask a question about them---for example, ``Does my program have an execution that violates an assertion while satisfying all the assumptions?'' We pose such @emph{solver-aided queries} with the help of constructs explained in the remainder of this chapter.
|
||||
The solver reasons about assumed and asserted properties only when we ask a question about them---for example, "Does my program have an execution that violates an assertion while satisfying all the assumptions?" We pose such @emph{solver-aided queries} with the help of constructs explained in the remainder of this chapter.
|
||||
|
||||
We will illustrate the queries on the following toy example. Suppose that we want to implement a
|
||||
procedure @racket[bvmid] that takes as input two non-negative 32-bit integers, @racket[lo] ≤ @racket[hi],
|
||||
|
|
@ -323,7 +321,7 @@ The synthesis query takes the form @racket[(synthesize #:forall #, @var[input] #
|
|||
|
||||
Rosette supports one more solver-aided query, which we call angelic execution. This query is the dual of verification. Given a program with symbolic values, it instructs the solver to find a binding for them that will cause the program to execute normally---that is, without any assumption or assertion failures.
|
||||
|
||||
Angelic execution can be used to solve puzzles, to run incomplete code, or to ``invert'' a program, by searching for inputs that produce a desired output. For example, we can ask the solver to search for two distinct legal inputs, @racket[l] and @racket[h], whose midpoint is the bitwise-and of their bits:
|
||||
Angelic execution can be used to solve puzzles, to run incomplete code, or to "invert" a program, by searching for inputs that produce a desired output. For example, we can ask the solver to search for two distinct legal inputs, @racket[l] and @racket[h], whose midpoint is the bitwise-and of their bits:
|
||||
@examples[#:eval rosette-eval #:label #f
|
||||
(define (bvmid-fast lo hi)
|
||||
(bvlshr (bvadd hi lo) (bv #x00000001 32)))
|
||||
|
|
@ -482,7 +480,7 @@ n2
|
|||
n3]
|
||||
In general, recursion terminates under symbolic evaluation only when the stopping condition is reached with concrete values.
|
||||
|
||||
We can force termination by placing a concrete bound @var{k} on the number of times @racket[bvsqrt] can call itself recursively. This approach is called @deftech{finitization}, and it is the standard way to handle unbounded loops and recursion under symbolic evaluation. The following code shows how to implement a @emph{sound} finitization policy. If a @racket[verify] query returns @racket[(unsat)] under a sound policy, we know that (1) the unrolling bound @var{k} is sufficient to execute all possible inputs to @racket[bvsqrt], and (2) all of these executions satisfy the query. If we pick a bound that is too small, the query will generate a counterexample input that needs a larger bound to compute the result. In our example, the bound of 16 is sufficient to verify the correctness of @racket[bvsqrt] on all inputs:
|
||||
We can force termination by placing a concrete bound @var{k} on the number of times @racket[bvsqrt] can call itself recursively. This approach is called @deftech{finitization}, and it is the standard way to handle unbounded loops and recursion under symbolic evaluation. The following code shows how to implement a @emph{sound} finitization policy. If a @racket[verify] query returns @racket[(unsat)] under a sound policy, we know that (1) the unrolling bound @var{k} is sufficient to execute all possible inputs to @racket[bvsqrt], and (2) all of these executions satisfy the query. If we pick a bound that is too small, the query will generate a counterexample input that needs a larger bound to compute the result. In our example, the bound of 16 is sufficient to verify the correctness of @racket[sqrt] on all inputs:
|
||||
@(rosette-eval '(clear-vc!))
|
||||
@(rosette-eval '(require (only-in racket make-parameter parameterize)))
|
||||
@examples[#:eval rosette-eval #:label #f #:no-prompt
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@
|
|||
|
||||
@title[#:tag "ch:syntactic-forms" #:style 'toc]{Syntactic Forms}
|
||||
|
||||
The core of the Rosette language (@racketmodname[rosette/safe]) consists of two kinds of syntax forms: a set of basic forms @deftech[#:key "lifted constructs"]{lifted} from Racket, and a set of forms for @seclink["ch:essentials"]{solver-aided programming}. We use the term ``lifted'' to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.
|
||||
The core of the Rosette language (@racket[rosette/safe]) consists of two kinds of syntax forms: a set of basic forms @deftech[#:key "lifted constructs"]{lifted} from Racket, and a set of forms for @seclink["ch:essentials"]{solver-aided programming}. We use the term "lifted" to refer to parts of the Racket language that can be used with symbolic values and other solver-aided constructs.
|
||||
|
||||
@[table-of-contents]
|
||||
@include-section["racket-forms.scrbl"]
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@
|
|||
|
||||
@title[#:tag "ch:libraries" #:style 'toc]{Libraries}
|
||||
|
||||
Chapters @seclink["ch:getting-started"]{1}-@seclink["ch:programmer-defined-datatypes"]{5} introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by @racketmodname[rosette/safe], as well as Rosette libraries that provide additional facilities for solver-aided development.
|
||||
Chapters @seclink["ch:getting-started"]{1}-@seclink["ch:programmer-defined-datatypes"]{5} introduce the basic constructs and datatypes for programming in Rosette. This chapter describes the parts of the core Racket libraries (e.g., I/O procedures) that are exported by @racket[rosette/safe], as well as Rosette libraries that provide additional facilities for solver-aided development.
|
||||
|
||||
@[table-of-contents]
|
||||
|
||||
|
|
|
|||
|
|
@ -17,4 +17,5 @@ Rosette exports the following facilities from the core Racket libraries:
|
|||
|
||||
These facilities are safe to use in Rosette programs, even in the presence of symbolic values, assertions, and solver-aided queries. They are not, however, @tech[#:key "lifted constructs"]{lifted}: if their Racket implementation expects a concrete value of a given type, they will fail when given a symbolic value. These constructs are safe to use in the sense that they will fail in a predictable fashion, according to their concrete Racket specification, instead of causing the enclosing Rosette program to exhibit unexpected behavior.
|
||||
|
||||
The @racketmodname[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism. This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}. Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files). In other words, arbitrary Racket code is, by default, unsafe to use.
|
||||
The @racket[rosette/safe] language allows programs to import arbitrary Racket code using the standard @racket[require] mechanism. This is strongly discouraged, however, unless the use of such code obeys the restrictions outlined in the @seclink["ch:unsafe"]{Chapter 8}. Violating these restrictions may lead to incorrect program behavior, crashes, and loss of data (for programs that perform external side-effects, such as writing to files). In other words, arbitrary Racket code is, by default, unsafe to use.
|
||||
|
||||
|
|
|
|||
|
|
@ -367,7 +367,7 @@ sol
|
|||
generated for programs that have been saved to disk.
|
||||
|
||||
This procedure cooperates with the constructs in the
|
||||
@racketmodname[rosette/lib/synthax] library to turn solutions into
|
||||
@racket[rosette/lib/synthax] library to turn solutions into
|
||||
code. It works by scanning program files for
|
||||
@racketlink[??]{constant}, @racketlink[choose]{choice}, and
|
||||
@racketlink[define-grammar]{grammar} holes, and replacing
|
||||
|
|
@ -471,4 +471,4 @@ sol
|
|||
}
|
||||
|
||||
|
||||
@(kill-evaluator rosette-eval)
|
||||
@(kill-evaluator rosette-eval)
|
||||
|
|
@ -55,7 +55,7 @@ integers and reals (while being correct under the
|
|||
finite-precision semantics). For example, this program
|
||||
incorrectly says that no integer greater than 15 exists,
|
||||
because the setting of @racket[current-bitwidth] causes it
|
||||
to consider only values of @racket[x] that can be
|
||||
to consider only values of @racket{x} that can be
|
||||
represented as a 5-bit bitvector.
|
||||
|
||||
@examples[#:eval rosette-eval #:label #f
|
||||
|
|
@ -387,15 +387,15 @@ the performance of @tt{verify-xform} to degrade, from a
|
|||
couple of seconds when @tt{N} = 5 to over a minute when @tt{N}
|
||||
= 20. To identify the source of this performance issue, we
|
||||
can invoke the @tech{symbolic profiler} on the verifier,
|
||||
producing the output below (after selecting the ``Collapse
|
||||
solver time'' checkbox):
|
||||
producing the output below (after selecting the "Collapse
|
||||
solver time" checkbox):
|
||||
|
||||
@(image profile-xform.png #:scale 0.425)
|
||||
|
||||
The symbolic profiler identifies @tt{list-set} as the
|
||||
bottleneck in this program. The output shows that @tt{list-set}
|
||||
creates many symbolic terms, and performs many symbolic
|
||||
operations (the ``Union Size'' and ``Merge Cases'' columns).
|
||||
operations (the "Union Size" and "Merge Cases" columns).
|
||||
|
||||
The core issue here is an @tech{algorithmic mismatch}: @tt{list-set}
|
||||
makes a recursive call guarded by a short-circuiting
|
||||
|
|
@ -431,4 +431,4 @@ and so the verification conditions no longer grow quadratically.
|
|||
(list-set* '(1 2 3) idx 4)]
|
||||
|
||||
The performance of @tt{verify-xform} after this change
|
||||
improves by 3× for @tt{N} = 20.
|
||||
improves by 3× for @tt{N} = 20.
|
||||
|
|
@ -241,8 +241,8 @@ as well as for tuning the performance of symbolic
|
|||
evaluation.
|
||||
|
||||
|
||||
@declare-exporting[rosette/base/core/forall
|
||||
#:use-sources (rosette/base/core/forall)]
|
||||
@declare-exporting[rosette/base/core/forall rosette/lib/lift
|
||||
#:use-sources (rosette/base/core/forall rosette/lib/lift)]
|
||||
|
||||
@defform[(for/all ([id val-expr maybe-exhaustive]) body ...+)
|
||||
#:grammar [(maybe-exhaustive (code:line) #:exhaustive)]]{
|
||||
|
|
@ -406,4 +406,4 @@ evaluation.
|
|||
}
|
||||
|
||||
|
||||
@(kill-evaluator rosette-eval)
|
||||
@(kill-evaluator rosette-eval)
|
||||
|
|
@ -9,28 +9,21 @@
|
|||
|
||||
@(define rosette:onward13
|
||||
(make-bib
|
||||
#:title @hyperlink["http://dl.acm.org/citation.cfm?id=2509586"]{Growing Solver-Aided Languages with Rosette}
|
||||
#:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.onward13.pdf"]{Growing Solver-Aided Languages with Rosette}
|
||||
#:author (authors "Emina Torlak" "Rastislav Bodik")
|
||||
#:date 2013
|
||||
#:location "New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)"))
|
||||
|
||||
@(define rosette:pldi14
|
||||
(make-bib
|
||||
#:title @hyperlink["http://dl.acm.org/citation.cfm?id=2594340"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
|
||||
#:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.pldi14.pdf"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
|
||||
#:author (authors "Emina Torlak" "Rastislav Bodik")
|
||||
#:date 2014
|
||||
#:location "Programming Language Design and Implementation (PLDI)"))
|
||||
|
||||
@(define sympro:oopsla18
|
||||
(make-bib
|
||||
#:title @hyperlink["https://dl.acm.org/citation.cfm?id=3276519"]{Finding Code That Explodes Under Symbolic Evaluation}
|
||||
#:title @hyperlink["https://unsat.cs.washington.edu/papers/bornholt-sympro.pdf"]{Finding Code That Explodes Under Symbolic Evaluation}
|
||||
#:author (authors "James Bornholt" "Emina Torlak")
|
||||
#:date 2018
|
||||
#:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
|
||||
|
||||
@(define rosette:popl22
|
||||
(make-bib
|
||||
#:title @hyperlink["https://doi.org/10.1145/3498709"]{A Formal Foundation for Symbolic Evaluation with Merging}
|
||||
#:author (authors "Sorawee Porncharoenwase" "Luke Nelson" "Xi Wang" "Emina Torlak")
|
||||
#:date 2022
|
||||
#:location "Principles of Programming Languages (POPL)"))
|
||||
#:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
|
||||
|
|
@ -4,7 +4,7 @@
|
|||
@(require (for-label rosette/base/form/define rosette/query/query rosette/solver/solution
|
||||
(only-in rosette/base/base assert vc-true? vc) )
|
||||
racket/runtime-path racket/sandbox)
|
||||
@(require (only-in "../refs.scrbl" ~cite rosette:pldi14 rosette:popl22))
|
||||
@(require (only-in "../refs.scrbl" ~cite rosette:pldi14))
|
||||
@(require "../util/lifted.rkt")
|
||||
|
||||
@(define-runtime-path root ".")
|
||||
|
|
@ -13,20 +13,20 @@
|
|||
@title[#:tag "ch:unsafe"]{Unsafe Operations}
|
||||
|
||||
Throughout this guide, we have assumed that Rosette programs are
|
||||
written in the @racketmodname[rosette/safe] dialect of the full language.
|
||||
written in the @racket[rosette/safe] dialect of the full language.
|
||||
This dialect extends a core subset of Racket with @seclink["ch:essentials"]{solver-aided
|
||||
functionality}. In this chapter, we briefly discuss the @racketmodname[rosette]
|
||||
functionality}. In this chapter, we briefly discuss the @racket[rosette]
|
||||
dialect of the language, which exports all of Racket.
|
||||
|
||||
Safe use of the full @racketmodname[rosette] language requires a basic understanding
|
||||
of how Rosette's Symbolic Virtual Machine (SVM) works @~cite[rosette:pldi14 rosette:popl22].
|
||||
Safe use of the full @racket[rosette] language requires a basic understanding
|
||||
of how Rosette's Symbolic Virtual Machine (SVM) works @~cite[rosette:pldi14].
|
||||
Briefly, the SVM hijacks the normal Racket execution for all procedures and
|
||||
constructs that are exported by @racketmodname[rosette/safe]. Any programs that are
|
||||
implemented exclusively in the @racketmodname[rosette/safe] language are therefore
|
||||
constructs that are exported by @racket[rosette/safe]. Any programs that are
|
||||
implemented exclusively in the @racket[rosette/safe] language are therefore
|
||||
fully under the SVM's control. This means that the SVM can correctly interpret
|
||||
the application of a procedure or a macro to a symbolic value, and it
|
||||
can correctly handle any side-effects (in particular, writes to memory) performed
|
||||
by @racketmodname[rosette/safe] code.
|
||||
by @racket[rosette/safe] code.
|
||||
|
||||
The following snippet demonstrates the non-standard execution that the SVM needs to
|
||||
perform in order to assign the expected meaning to Rosette code:
|
||||
|
|
@ -53,17 +53,17 @@ y
|
|||
(define sol2 (solve (assert (not b))))
|
||||
(evaluate y sol2)]
|
||||
|
||||
Because the SVM controls only the execution of @racketmodname[rosette/safe] code,
|
||||
it cannot, in general, guarantee the safety or correctness of arbitrary @racketmodname[rosette] programs.
|
||||
As soon as a @racketmodname[rosette] program calls an @tech[#:key "lifted construct"]{unlifted} Racket construct
|
||||
(that is, a procedure or a macro not implemented in or provided by the @racketmodname[rosette/safe] language),
|
||||
Because the SVM controls only the execution of @racket[rosette/safe] code,
|
||||
it cannot, in general, guarantee the safety or correctness of arbitrary @racket[rosette] programs.
|
||||
As soon as a @racket[rosette] program calls an @tech[#:key "lifted construct"]{unlifted} Racket construct
|
||||
(that is, a procedure or a macro not implemented in or provided by the @racket[rosette/safe] language),
|
||||
the execution escapes back to the Racket interpreter. The SVM has no control over the side-effects
|
||||
performed by the Racket interpreter, or the meaning that it (perhaps incorrectly) assigns to programs
|
||||
in the presence of symbolic values. As a result, the programmer is responsible for ensuring that
|
||||
a @racketmodname[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
|
||||
a @racket[rosette] program continues to behave correctly after the execution returns from the Racket interpreter.
|
||||
|
||||
As an example of incorrect behavior, consider the following @racketmodname[rosette] snippet.
|
||||
The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racketmodname[rosette/safe].
|
||||
As an example of incorrect behavior, consider the following @racket[rosette] snippet.
|
||||
The procedures @racket[make-hash], @racket[hash-ref], and @racket[hash-clear!] are not in @racket[rosette/safe].
|
||||
Whenever they are invoked, the execution escapes to the Racket interpreter.
|
||||
|
||||
@(rosette-eval '(require (only-in racket make-hash hash-clear! hash-ref)))
|
||||
|
|
@ -105,4 +105,4 @@ as long as they iterate over concrete sequences, and all guard expressions produ
|
|||
each iteration. In practice, Rosette programs can safely use many common Racket constructs, and with a
|
||||
bit of experience, it becomes easy to see when it is okay to break the effectively-concrete rule.
|
||||
|
||||
@(kill-evaluator rosette-eval)
|
||||
@(kill-evaluator rosette-eval)
|
||||
|
|
@ -16,13 +16,13 @@ Rosette is a @emph{solver-aided} programming system with two components:
|
|||
compiles them to logical constraints. The SVM enables Rosette
|
||||
to use the solver to automatically reason about program behaviors.}]
|
||||
|
||||
The name ``Rosette'' refers both to the language and the whole system.
|
||||
The name "Rosette" refers both to the language and the whole system.
|
||||
|
||||
@section[#:tag "sec:get"]{Installing Rosette}
|
||||
|
||||
To install Rosette, you will need to
|
||||
|
||||
@itemlist[@item{Download and install @hyperlink["http://racket-lang.org"]{Racket} (version 8.1 or later).}
|
||||
@itemlist[@item{Download and install @hyperlink["http://racket-lang.org"]{Racket} (version 8.0 or later).}
|
||||
@item{Use Racket's @tt{raco} tool to install Rosette:
|
||||
@nested{
|
||||
@verbatim|{> raco pkg install rosette}|}}]
|
||||
|
|
|
|||
|
|
@ -14,7 +14,10 @@
|
|||
(experimental))))
|
||||
;; Documentation category. On Racket 6.3+ this can be any string.
|
||||
|
||||
(define compile-omit-files '("lib/trace/report/node_modules"))
|
||||
;; Runs the code in `private/install.rkt` before installing this collection.
|
||||
(define pre-install-collection "private/install.rkt")
|
||||
(define compile-omit-files '("private/install.rkt"
|
||||
"lib/trace/report/node_modules"))
|
||||
|
||||
(define raco-commands
|
||||
'(("symprofile"
|
||||
|
|
|
|||
|
|
@ -48,11 +48,10 @@
|
|||
|
||||
(define-simple-macro (destruct val [pat:clause-pattern e:expr ...+] ...)
|
||||
#:do [(for-each check-duplicate-identifier! (attribute pat.id-set))]
|
||||
#:with match-expr (syntax/loc this-syntax (match var [pat (begin e ...)] ...))
|
||||
#:with result
|
||||
(syntax/loc this-syntax
|
||||
(for/all ([var val]);(guarded-values val)])
|
||||
match-expr))
|
||||
(match var [pat (begin e ...)] ...)))
|
||||
result)
|
||||
|
||||
(define-simple-macro (destruct* (val ...) [(pat:clause-pattern ...) e:expr ...+] ...)
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@
|
|||
"Only install the compile handler; do not run the profiler"
|
||||
(run-profiler? #f)]
|
||||
[("-m" "--module") name
|
||||
"Run submodule <name> (defaults to 'main')"
|
||||
"Run submodule <name> (defaults to 'main)"
|
||||
(module-name (string->symbol name))]
|
||||
[("-r" "--racket")
|
||||
"Instrument code in any language, not just `#lang rosette`"
|
||||
|
|
|
|||
|
|
@ -78,13 +78,8 @@
|
|||
; all events from the box. if that happened then the ENTER we're trying
|
||||
; to delete has already been published, and so we need to retain the
|
||||
; corresponding EXIT.
|
||||
(let loop ()
|
||||
(unless (box-cas! the-box evts (cdr evts))
|
||||
(if (eq? evts (unbox the-box))
|
||||
; spurious CAS failure; retry
|
||||
(loop)
|
||||
; box has changed, so we need to retain the EXIT
|
||||
(do-record-exit! out))))]))))))
|
||||
(unless (box-cas! the-box evts (cdr evts))
|
||||
(do-record-exit! out))]))))))
|
||||
|
||||
; Default version just uses the current-profile/current-reporter params
|
||||
(define default-record-exit
|
||||
|
|
|
|||
|
|
@ -296,4 +296,4 @@
|
|||
(define (print-forms sol)
|
||||
(for ([f (generate-forms sol)])
|
||||
(printf "~a:~a:~a\n" (syntax-source f) (syntax-line f) (syntax-column f))
|
||||
(pretty-write (syntax->datum f))))
|
||||
(pretty-print (syntax->datum f))))
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@
|
|||
|
||||
;; SymPro options
|
||||
[("-m" "--module") name
|
||||
"Run submodule <name> (defaults to 'main')"
|
||||
"Run submodule <name> (defaults to 'main)"
|
||||
(module-name (string->symbol name))]
|
||||
[("-r" "--racket")
|
||||
"Instrument code in any language, not just `#lang rosette`"
|
||||
|
|
|
|||
|
|
@ -21,8 +21,6 @@
|
|||
(string-prefix? (path->string (resolve-path a))
|
||||
(path->string (resolve-path b))))
|
||||
|
||||
(define pkg-cache (make-hash))
|
||||
|
||||
(define (make-rosette-load/use-compiled pkgs-to-instrument)
|
||||
(make-custom-load/use-compiled
|
||||
#:blacklist
|
||||
|
|
@ -30,6 +28,6 @@
|
|||
(cond
|
||||
[(path-prefix? path (find-collects-dir)) #f]
|
||||
[else
|
||||
(match (path->pkg path #:cache pkg-cache)
|
||||
(match (path->pkg path)
|
||||
[#f #t]
|
||||
[pkg-name (member pkg-name pkgs-to-instrument)])]))))
|
||||
|
|
|
|||
|
|
@ -14,40 +14,37 @@
|
|||
; the procedure for handling connections
|
||||
(define (ws-connection conn _state)
|
||||
; only one client may connect
|
||||
(let loop ()
|
||||
(cond
|
||||
[(box-cas! connected? #f #t) ; we won the race to connect
|
||||
; tell the main thread we're connected
|
||||
(channel-put channel 'connected)
|
||||
; loop until we're done
|
||||
(let loop ()
|
||||
(define sync-result (sync/timeout/enable-break interval channel))
|
||||
(define messages (get-message))
|
||||
(cond
|
||||
[(box-cas! connected? #f #t) ; we won the race to connect
|
||||
; tell the main thread we're connected
|
||||
(channel-put channel 'connected)
|
||||
; loop until we're done
|
||||
(let loop ()
|
||||
(define sync-result (sync/timeout/enable-break interval channel))
|
||||
(define messages (get-message))
|
||||
|
||||
; send the messages; bail out if it fails
|
||||
(define continue? (not (eq? sync-result 'finish)))
|
||||
(with-handlers ([exn:fail? (lambda (e)
|
||||
(eprintf "~e\n" e)
|
||||
(set! continue? #f))])
|
||||
(ws-send! conn (jsexpr->bytes messages)))
|
||||
(if continue?
|
||||
(loop)
|
||||
(begin
|
||||
(with-handlers ([exn:fail? void]) ; the connection might be dead, but we don't care
|
||||
(ws-send! conn (jsexpr->bytes (list (get-finish-message))))
|
||||
(ws-close! conn))
|
||||
; if we weren't told to shut down, we need to wait until we are.
|
||||
(cond
|
||||
[on-shutdown (on-shutdown)]
|
||||
[else
|
||||
(unless (eq? sync-result 'finish)
|
||||
(channel-get channel))
|
||||
(channel-put channel 'finish)]))))]
|
||||
[(unbox connected?)
|
||||
;; it's already connected
|
||||
(channel-put channel "another client is already connected")
|
||||
(ws-close! conn)]
|
||||
[else (loop)])))
|
||||
; send the messages; bail out if it fails
|
||||
(define continue? (not (eq? sync-result 'finish)))
|
||||
(with-handlers ([exn:fail? (lambda (e)
|
||||
(eprintf "~e\n" e)
|
||||
(set! continue? #f))])
|
||||
(ws-send! conn (jsexpr->bytes messages)))
|
||||
(if continue?
|
||||
(loop)
|
||||
(begin
|
||||
(with-handlers ([exn:fail? void]) ; the connection might be dead, but we don't care
|
||||
(ws-send! conn (jsexpr->bytes (list (get-finish-message))))
|
||||
(ws-close! conn))
|
||||
; if we weren't told to shut down, we need to wait until we are.
|
||||
(cond
|
||||
[on-shutdown (on-shutdown)]
|
||||
[else
|
||||
(unless (eq? sync-result 'finish)
|
||||
(channel-get channel))
|
||||
(channel-put channel 'finish)]))))]
|
||||
[else
|
||||
(channel-put channel "another client is already connected")
|
||||
(ws-close! conn)]))
|
||||
|
||||
; start the server
|
||||
(define conf-channel (make-async-channel))
|
||||
|
|
|
|||
|
|
@ -0,0 +1,107 @@
|
|||
#lang racket/base
|
||||
|
||||
;; Check whether z3 is installed during package setup.
|
||||
;; If missing, builds & links a z3 binary.
|
||||
|
||||
|
||||
(provide pre-installer)
|
||||
|
||||
(require racket/match
|
||||
racket/file
|
||||
racket/port
|
||||
net/url
|
||||
file/unzip)
|
||||
|
||||
(define (print-failure path msg)
|
||||
(printf "\n\n********** Failed to install Z3 **********\n\n")
|
||||
(printf "You'll need to manually install a Z3 binary\n")
|
||||
(printf "to this location: ~a\n\n" path)
|
||||
(printf "The problem was:\n~a\n\n" msg)
|
||||
(printf "*********\n\n\n"))
|
||||
|
||||
(define (pre-installer collections-top-path racl-path)
|
||||
(define bin-path (simplify-path (build-path racl-path ".." "bin")))
|
||||
(define z3-path (build-path bin-path "z3"))
|
||||
(with-handlers ([exn:fail? (lambda (e) (print-failure z3-path (exn-message e)))])
|
||||
(unless (custom-z3-symlink? z3-path)
|
||||
(define-values (z3-url z3-path-in-zip) (get-z3-url))
|
||||
(define z3-port (get-pure-port (string->url z3-url) #:redirections 10))
|
||||
(make-directory* bin-path) ;; Ensure that `bin-path` exists
|
||||
(delete-directory/files z3-path #:must-exist? #f) ;; Delete old version of Z3, if any
|
||||
(parameterize ([current-directory bin-path])
|
||||
(call-with-unzip z3-port
|
||||
(λ (dir)
|
||||
(copy-directory/files (build-path dir z3-path-in-zip) z3-path)))
|
||||
;; Unzipping loses file permissions, so we reset the z3 binary here
|
||||
(file-or-directory-permissions
|
||||
z3-path
|
||||
(if (equal? (system-type) 'windows) #o777 #o755))))))
|
||||
|
||||
(define (custom-z3-symlink? z3-path)
|
||||
(and (file-exists? z3-path)
|
||||
(let ([p (simplify-path z3-path)])
|
||||
(not (equal? (resolve-path p) p)))))
|
||||
|
||||
(define (get-z3-url)
|
||||
(define site "https://github.com/Z3Prover/z3/releases/download")
|
||||
(define version "z3-4.8.8")
|
||||
(define-values (os exe)
|
||||
(match (list (system-type) (system-type 'word))
|
||||
['(unix 64) (values "x64-ubuntu-16.04" "z3")]
|
||||
[`(macosx ,_) (values "x64-osx-10.14.6" "z3")]
|
||||
['(windows 64) (values "x64-win" "z3.exe")]
|
||||
[any (raise-user-error 'get-z3-url "Unknown system type '~a'" any)]))
|
||||
(define name (format "~a-~a" version os))
|
||||
(values
|
||||
(format "~a/~a/~a.zip" site version name)
|
||||
(format "~a/bin/~a" name exe)))
|
||||
|
||||
|
||||
;; A copy of net/url's get-pure-port/headers, except with the Location header
|
||||
;; for redirects made case-insensitive, fixing https://github.com/racket/racket/pull/3057
|
||||
(require net/http-client net/url-connect)
|
||||
(define (get-pure-port url #:redirections [redirections 0])
|
||||
(let redirection-loop ([redirections redirections] [url url])
|
||||
(define hc (http-conn-open (url-host url)
|
||||
#:ssl? (if (equal? "https" (url-scheme url))
|
||||
(current-https-protocol)
|
||||
#f)))
|
||||
(define access-string
|
||||
(url->string
|
||||
;; RFCs 1945 and 2616 say:
|
||||
;; Note that the absolute path cannot be empty; if none is present in
|
||||
;; the original URI, it must be given as "/" (the server root).
|
||||
(let-values ([(abs? path)
|
||||
(if (null? (url-path url))
|
||||
(values #t (list (make-path/param "" '())))
|
||||
(values (url-path-absolute? url) (url-path url)))])
|
||||
(make-url #f #f #f #f abs? path (url-query url) (url-fragment url)))))
|
||||
(http-conn-send! hc access-string #:method #"GET" #:content-decode '())
|
||||
(define-values (status headers response-port)
|
||||
(http-conn-recv! hc #:method #"GET" #:close? #t #:content-decode '()))
|
||||
|
||||
(define new-url
|
||||
(ormap (λ (h)
|
||||
(match (regexp-match #rx#"^[Ll]ocation: (.*)$" h)
|
||||
[#f #f]
|
||||
[(list _ m1b)
|
||||
(define m1 (bytes->string/utf-8 m1b))
|
||||
(with-handlers ((exn:fail? (λ (x) #f)))
|
||||
(define next-url (string->url m1))
|
||||
(make-url
|
||||
(or (url-scheme next-url) (url-scheme url))
|
||||
(or (url-user next-url) (url-user url))
|
||||
(or (url-host next-url) (url-host url))
|
||||
(or (url-port next-url) (url-port url))
|
||||
(url-path-absolute? next-url)
|
||||
(url-path next-url)
|
||||
(url-query next-url)
|
||||
(url-fragment next-url)))]))
|
||||
headers))
|
||||
(define redirection-status-line?
|
||||
(regexp-match #rx#"^HTTP/[0-9]+[.][0-9]+ 3[0-9][0-9]" status))
|
||||
(cond
|
||||
[(and redirection-status-line? new-url (not (zero? redirections)))
|
||||
(redirection-loop (- redirections 1) new-url)]
|
||||
[else
|
||||
response-port])))
|
||||
|
|
@ -150,12 +150,12 @@
|
|||
; ∃H. (∀I. assumes => asserts) ∧ (∃I. assumes).
|
||||
(define (cegis inputs assumes asserts guesser checker)
|
||||
|
||||
(define φ `(,(=> (apply && assumes) (apply && asserts))))
|
||||
(define φ (append assumes asserts))
|
||||
|
||||
(define ¬φ `(,@assumes ,(apply || (map ! asserts))))
|
||||
|
||||
(define (guess ψ)
|
||||
(solver-assert guesser ψ)
|
||||
|
||||
(define (guess sol)
|
||||
(solver-assert guesser (evaluate φ sol))
|
||||
(match (solver-check guesser)
|
||||
[(model m) (sat (for/hash ([(c v) m] #:unless (member c inputs)) (values c v)))]
|
||||
[other other]))
|
||||
|
|
@ -171,14 +171,14 @@
|
|||
v)))))]
|
||||
[other other]))
|
||||
|
||||
(let loop ([candidate (guess (append assumes asserts))])
|
||||
(let loop ([candidate (begin0 (guess (sat)) (solver-clear guesser))])
|
||||
(cond
|
||||
[(unsat? candidate) candidate]
|
||||
[else
|
||||
(let ([cex (check candidate)])
|
||||
(cond
|
||||
[(unsat? cex) candidate]
|
||||
[else (loop (guess (evaluate φ cex)))]))])))
|
||||
[else (loop (guess cex))]))])))
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -47,10 +47,7 @@
|
|||
[(cons x y)
|
||||
(cons (eval-rec x sol cache) (eval-rec y sol cache))]
|
||||
[(? vector?)
|
||||
(let ([v (for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))])
|
||||
(if (immutable? expr)
|
||||
(vector->immutable-vector v)
|
||||
v))]
|
||||
(for/vector #:length (vector-length expr) ([e expr]) (eval-rec e sol cache))]
|
||||
[(? box?)
|
||||
((if (immutable? expr) box-immutable box) (eval-rec (unbox expr) sol cache))]
|
||||
[(? typed?)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
#lang racket
|
||||
|
||||
(require syntax/parse/define
|
||||
"core.rkt"
|
||||
(require "core.rkt"
|
||||
(only-in "../base/core/reflect.rkt" symbolics)
|
||||
(only-in "../base/core/result.rkt" result-state)
|
||||
(only-in "../base/core/bool.rkt" ! vc with-vc vc-assumes vc-asserts vc-true))
|
||||
|
|
@ -71,15 +70,14 @@
|
|||
; generate any assumptions or assertions, these are reflected in the (vc) after
|
||||
; the optimize query returns. The assumptions and assertions generated by expr
|
||||
; are not added to (vc) after optimize returns.
|
||||
(define-syntax-parser optimize
|
||||
[(_ {~and kw {~or* #:minimize #:maximize}} opt #:guarantee expr)
|
||||
#'(let ([obj opt] ; evaluate objective first to add its spec to (vc)
|
||||
(define-syntax optimize
|
||||
(syntax-rules ()
|
||||
[(_ kw opt #:guarantee expr)
|
||||
(let ([obj opt] ; evaluate objective first to add its spec to (vc)
|
||||
[post (query-vc expr)])
|
||||
(∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw obj))]
|
||||
[(_ {~and kw1 {~or* #:minimize #:maximize}} opt1
|
||||
{~and kw2 {~or* #:minimize #:maximize}} opt2
|
||||
#:guarantee expr)
|
||||
#'(let ([obj1 opt1] ; evaluate objectives first to add their spec to (vc)
|
||||
[(_ kw1 opt1 kw2 opt2 #:guarantee expr)
|
||||
(let ([obj1 opt1] ; evaluate objectives first to add their spec to (vc)
|
||||
[obj2 opt2]
|
||||
[post (query-vc expr)])
|
||||
(∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))])
|
||||
[post (query-vc expr)])
|
||||
(∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))]))
|
||||
|
|
@ -12,8 +12,6 @@
|
|||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define (unique/reverse xs)
|
||||
(reverse (unique xs)))
|
||||
|
||||
(define (find-solver binary base-path [user-path #f])
|
||||
(cond
|
||||
|
|
@ -44,15 +42,14 @@
|
|||
(unless (list? bools)
|
||||
(raise-argument-error 'solver-assert "(listof boolean?)" bools))
|
||||
(define wfcheck-cache (mutable-set))
|
||||
(set-solver-asserts!
|
||||
self
|
||||
(append (for/list ([b bools] #:unless (equal? b #t))
|
||||
(unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
|
||||
(error 'assert "expected a boolean value, given ~s" b))
|
||||
(when wfcheck
|
||||
(wfcheck b wfcheck-cache))
|
||||
b)
|
||||
(solver-asserts self))))
|
||||
(set-solver-asserts! self
|
||||
(append (solver-asserts self)
|
||||
(for/list ([b bools] #:unless (equal? b #t))
|
||||
(unless (or (boolean? b) (and (term? b) (equal? @boolean? (term-type b))))
|
||||
(error 'assert "expected a boolean value, given ~s" b))
|
||||
(when wfcheck
|
||||
(wfcheck b wfcheck-cache))
|
||||
b))))
|
||||
|
||||
(define (solver-minimize self nums)
|
||||
(unless (null? nums)
|
||||
|
|
@ -71,7 +68,7 @@
|
|||
(server-shutdown (solver-server self)))
|
||||
|
||||
(define (solver-push self)
|
||||
(match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env level) self)
|
||||
(match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env level) self)
|
||||
(server-write
|
||||
server
|
||||
(begin
|
||||
|
|
@ -93,7 +90,7 @@
|
|||
(set-solver-level! self (drop level k)))
|
||||
|
||||
(define (solver-check self [read-solution read-solution])
|
||||
(match-define (solver server _ (app unique asserts) (app unique/reverse mins) (app unique/reverse maxs) env _) self)
|
||||
(match-define (solver server _ (app unique asserts) (app unique mins) (app unique maxs) env _) self)
|
||||
(cond [(ormap false? asserts) (unsat)]
|
||||
[else (server-write
|
||||
server
|
||||
|
|
@ -125,40 +122,35 @@
|
|||
|
||||
|
||||
; Reads the SMT solution from the server.
|
||||
; The solution consists of 'sat or 'unsat, followed by
|
||||
; followed by a suitably formatted s-expression. The
|
||||
; output of this procedure is a hashtable from constant
|
||||
; The solution consists of 'sat or 'unsat, followed by
|
||||
; followed by a suitably formatted s-expression. The
|
||||
; output of this procedure is a hashtable from constant
|
||||
; identifiers to their SMTLib values (if the solution is 'sat);
|
||||
; a non-empty list of assertion identifiers that form an
|
||||
; unsatisfiable core (if the solution is 'unsat and a
|
||||
; core was extracted); #f (if the solution is
|
||||
; unsatisfiable core (if the solution is 'unsat and a
|
||||
; core was extracted); #f (if the solution is
|
||||
; 'unsat and no core was extracted); or 'unknown otherwise.
|
||||
(define (read-solution server env #:unsat-core? [unsat-core? #f])
|
||||
(decode (parse-solution server #:unsat-core? unsat-core?) env))
|
||||
|
||||
(define (parse-solution server #:unsat-core? [unsat-core? #f])
|
||||
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
||||
(match (server-read server (read))
|
||||
[(== 'sat)
|
||||
(server-write server (get-model))
|
||||
(let loop ()
|
||||
(match (server-read server (read))
|
||||
[(list (== 'objectives) _ ...) (loop)]
|
||||
; The SMT-LIB spec says that a model should be just a list of
|
||||
; `define-fun`s, but many SMT solvers used to prefix that list
|
||||
; with `model`, so let's support both versions.
|
||||
; https://groups.google.com/g/smt-lib/c/5xpcIxdQ8-A/m/X4uQ7dIgAwAJ
|
||||
[(or (list (== 'model) def ...) (list def ...))
|
||||
(for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
|
||||
(values (cadr d) d))]
|
||||
[other (error 'read-solution "expected model, given ~a" other)]))]
|
||||
[(== 'unsat)
|
||||
(if unsat-core?
|
||||
(begin
|
||||
(server-write server (get-unsat-core))
|
||||
(match (server-read server (read))
|
||||
[(list (? symbol? name) ...) name]
|
||||
[other (error 'read-solution "expected unsat core, given ~a" other)]))
|
||||
'unsat)]
|
||||
[(== 'unknown) 'unknown]
|
||||
[other (error 'read-solution "unrecognized solver output: ~a" other)])))
|
||||
(decode
|
||||
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
||||
(match (server-read server (read))
|
||||
[(== 'sat)
|
||||
(server-write server (get-model))
|
||||
(let loop ()
|
||||
(match (server-read server (read))
|
||||
[(list (== 'objectives) _ ...) (loop)]
|
||||
[(list (== 'model) def ...)
|
||||
(for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
|
||||
(values (cadr d) d))]
|
||||
[other (error 'read-solution "expected model, given ~a" other)]))]
|
||||
[(== 'unsat)
|
||||
(if unsat-core?
|
||||
(begin
|
||||
(server-write server (get-unsat-core))
|
||||
(match (server-read server (read))
|
||||
[(list (? symbol? name) ...) name]
|
||||
[other (error 'read-solution "expected unsat core, given ~a" other)]))
|
||||
'unsat)]
|
||||
[(== 'unknown) 'unknown]
|
||||
[other (error 'read-solution "unrecognized solver output: ~a" other)]))
|
||||
env))
|
||||
|
|
|
|||
|
|
@ -1,106 +0,0 @@
|
|||
;;; Requires Bitwuzla 0.1.0 or later.
|
||||
#lang racket
|
||||
|
||||
(require racket/runtime-path
|
||||
"server.rkt" "cmd.rkt" "env.rkt"
|
||||
"../solver.rkt" "../solution.rkt"
|
||||
(prefix-in base/ "base-solver.rkt")
|
||||
(only-in "../../base/core/term.rkt" term term? term-type constant? expression constant with-terms)
|
||||
(only-in "../../base/core/bool.rkt" @boolean? @forall @exists)
|
||||
(only-in "../../base/core/bitvector.rkt" bitvector bitvector? bv? bv bv-value @extract @sign-extend @zero-extend @bveq)
|
||||
(only-in "../../base/core/function.rkt" function-domain function-range function? function fv)
|
||||
(only-in "../../base/core/type.rkt" type-of)
|
||||
(only-in "../../base/form/control.rkt" @if))
|
||||
|
||||
(provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)
|
||||
|
||||
(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
|
||||
(define bitwuzla-opts '("-m"))
|
||||
|
||||
(define (bitwuzla-available?)
|
||||
(not (false? (base/find-solver "bitwuzla" bitwuzla-path #f))))
|
||||
|
||||
(define (make-bitwuzla [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
|
||||
(define config
|
||||
(cond
|
||||
[(bitwuzla? solver)
|
||||
(base/solver-config solver)]
|
||||
[else
|
||||
(define real-bitwuzla-path (base/find-solver "bitwuzla" bitwuzla-path path))
|
||||
(when (and (false? real-bitwuzla-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
||||
(error 'bitwuzla "bitwuzla binary is not available (expected to be at ~a); try passing the #:path argument to (bitwuzla)" (path->string (simplify-path bitwuzla-path))))
|
||||
(base/config options real-bitwuzla-path logic)]))
|
||||
(bitwuzla (server (base/config-path config) bitwuzla-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
||||
|
||||
(struct bitwuzla base/solver ()
|
||||
#:property prop:solver-constructor make-bitwuzla
|
||||
#:methods gen:custom-write
|
||||
[(define (write-proc self port mode) (fprintf port "#<bitwuzla>"))]
|
||||
#:methods gen:solver
|
||||
[
|
||||
(define (solver-features self)
|
||||
'(qf_bv))
|
||||
|
||||
(define (solver-options self)
|
||||
(base/solver-options self))
|
||||
|
||||
(define (solver-assert self bools)
|
||||
(base/solver-assert self bools bitwuzla-wfcheck))
|
||||
|
||||
(define (solver-minimize self nums)
|
||||
(base/solver-minimize self nums))
|
||||
|
||||
(define (solver-maximize self nums)
|
||||
(base/solver-maximize self nums))
|
||||
|
||||
(define (solver-clear self)
|
||||
(base/solver-clear self))
|
||||
|
||||
(define (solver-shutdown self)
|
||||
(base/solver-shutdown self))
|
||||
|
||||
(define (solver-push self)
|
||||
(base/solver-push self))
|
||||
|
||||
(define (solver-pop self [k 1])
|
||||
(base/solver-pop self k))
|
||||
|
||||
(define (solver-check self [read-solution base/read-solution])
|
||||
(base/solver-check self read-solution))
|
||||
|
||||
(define (solver-debug self)
|
||||
(base/solver-debug self))])
|
||||
|
||||
(define (set-default-options server)
|
||||
void)
|
||||
|
||||
|
||||
(define (valid-type? t)
|
||||
(or (equal? t @boolean?)
|
||||
(bitvector? t)
|
||||
(and (function? t)
|
||||
(for/and ([d (in-list (function-domain t))]) (valid-type? d))
|
||||
(valid-type? (function-range t)))))
|
||||
; Check whether a term v is well-formed for bitwuzla -- it must not mention
|
||||
; types other than bitvectors, booleans, and uninterpreted functions over those
|
||||
; types. If not, raise an exception.
|
||||
(define (bitwuzla-wfcheck v [cache (mutable-set)])
|
||||
(unless (set-member? cache v)
|
||||
(set-add! cache v)
|
||||
(cond
|
||||
[(term? v)
|
||||
(unless (valid-type? (type-of v))
|
||||
(error 'bitwuzla "bitwuzla does not support values of type ~v (value: ~v)" (type-of v) v))
|
||||
(match v
|
||||
[(expression (or (== @forall) (== @exists)) vars body)
|
||||
(error 'bitwuzla "bitwuzla does not support quantified formulas (value: ~v)" v)]
|
||||
[(expression (== @extract) i j e)
|
||||
(bitwuzla-wfcheck e cache)]
|
||||
[(expression (or (== @sign-extend) (== @zero-extend)) v t)
|
||||
(bitwuzla-wfcheck v cache)]
|
||||
[(expression op es ...)
|
||||
(for ([e es]) (bitwuzla-wfcheck e cache))]
|
||||
[_ #t])]
|
||||
[else
|
||||
(unless (or (boolean? v) (bv? v))
|
||||
(error 'bitwuzla "bitwuzla does not support value (expected boolean? or bv?): ~v" v))])))
|
||||
|
|
@ -107,10 +107,28 @@
|
|||
|
||||
|
||||
; Reads the SMT solution from the server.
|
||||
; This is the same as `base/read-solution` except that it applies some fixups
|
||||
; for quirks in how various versions of Boolector have emitted models.
|
||||
; The solution consists of 'sat or 'unsat, followed by
|
||||
; followed by a suitably formatted s-expression. The
|
||||
; output of this procedure is a hashtable from constant
|
||||
; identifiers to their SMTLib values (if the solution is 'sat);
|
||||
; a non-empty list of assertion identifiers that form an
|
||||
; unsatisfiable core (if the solution is 'unsat and a
|
||||
; core was extracted); #f (if the solution is
|
||||
; 'unsat and no core was extracted); or 'unknown otherwise.
|
||||
(define (boolector-read-solution server env)
|
||||
(define raw-model (base/parse-solution server))
|
||||
(define raw-model
|
||||
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
||||
(match (server-read server (read))
|
||||
[(== 'sat)
|
||||
(server-write server (get-model))
|
||||
(match (server-read server (read))
|
||||
[(list (== 'model) def ...)
|
||||
(for/hash ([d def] #:when (and (pair? d) (equal? (car d) 'define-fun)))
|
||||
(values (cadr d) d))]
|
||||
[other (error 'read-solution "expected model, given ~a" other)])]
|
||||
[(== 'unsat) 'unsat]
|
||||
[(== 'unknown) 'unknown]
|
||||
[other (error 'read-solution "unrecognized solver output: ~a" other)])))
|
||||
; First, we need to fix up the model's shadowing of incremental variables
|
||||
(define stripped-raw-model (if (hash? raw-model) (fixup-incremental-names raw-model) raw-model))
|
||||
; Now decode in an environment with fake types for UFs
|
||||
|
|
|
|||
|
|
@ -1,68 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/runtime-path
|
||||
"server.rkt" "env.rkt"
|
||||
"../solver.rkt"
|
||||
(prefix-in base/ "base-solver.rkt"))
|
||||
|
||||
(provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
|
||||
|
||||
(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
|
||||
(define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))
|
||||
|
||||
(define (cvc5-available?)
|
||||
(not (false? (base/find-solver "cvc5" cvc5-path #f))))
|
||||
|
||||
(define (make-cvc5 [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
|
||||
(define config
|
||||
(cond
|
||||
[(cvc5? solver)
|
||||
(base/solver-config solver)]
|
||||
[else
|
||||
(define real-cvc5-path (base/find-solver "cvc5" cvc5-path path))
|
||||
(when (and (false? real-cvc5-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
||||
(error 'cvc5 "cvc5 binary is not available (expected to be at ~a); try passing the #:path argument to (cvc5)" (path->string (simplify-path cvc5-path))))
|
||||
(base/config options real-cvc5-path logic)]))
|
||||
(cvc5 (server (base/config-path config) cvc5-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
||||
|
||||
(struct cvc5 base/solver ()
|
||||
#:property prop:solver-constructor make-cvc5
|
||||
#:methods gen:custom-write
|
||||
[(define (write-proc self port mode) (fprintf port "#<cvc5>"))]
|
||||
#:methods gen:solver
|
||||
[
|
||||
(define (solver-features self)
|
||||
'(qf_bv))
|
||||
|
||||
(define (solver-options self)
|
||||
(base/solver-options self))
|
||||
|
||||
(define (solver-assert self bools)
|
||||
(base/solver-assert self bools))
|
||||
|
||||
(define (solver-minimize self nums)
|
||||
(base/solver-minimize self nums))
|
||||
|
||||
(define (solver-maximize self nums)
|
||||
(base/solver-maximize self nums))
|
||||
|
||||
(define (solver-clear self)
|
||||
(base/solver-clear self))
|
||||
|
||||
(define (solver-shutdown self)
|
||||
(base/solver-shutdown self))
|
||||
|
||||
(define (solver-push self)
|
||||
(base/solver-push self))
|
||||
|
||||
(define (solver-pop self [k 1])
|
||||
(base/solver-pop self k))
|
||||
|
||||
(define (solver-check self)
|
||||
(base/solver-check self))
|
||||
|
||||
(define (solver-debug self)
|
||||
(base/solver-debug self))])
|
||||
|
||||
(define (set-default-options server)
|
||||
void)
|
||||
|
|
@ -14,8 +14,7 @@
|
|||
@bvslt @bvsle @bvult @bvule
|
||||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
||||
@concat @extract @sign-extend @zero-extend))
|
||||
@concat @extract))
|
||||
|
||||
|
||||
(provide decode-model)
|
||||
|
|
@ -117,6 +116,7 @@
|
|||
(hash-ref ~env id)]
|
||||
[(== true) #t]
|
||||
[(== false) #f]
|
||||
[(? integer?) (inexact->exact expr)]
|
||||
[(? real?) expr]
|
||||
[(? symbol?)
|
||||
(cond
|
||||
|
|
@ -132,10 +132,6 @@
|
|||
(bv n (bitvector len))]
|
||||
[(list (list (== '_) (== 'extract) i j) s)
|
||||
`(, @extract ,(inline i sol ~env) ,(inline j sol ~env) ,(inline s sol ~env))]
|
||||
[(list (list (== '_) (== 'sign_extend) i) s)
|
||||
`(, @sign-extend ,(inline i sol ~env) ,(inline s sol ~env))]
|
||||
[(list (list (== '_) (== 'zero_extend) i) s)
|
||||
`(, @zero-extend ,(inline i sol ~env) ,(inline s sol ~env))]
|
||||
[(list (== 'let) binds body)
|
||||
(substitute (inline body sol ~env)
|
||||
(for/hash ([id:expr binds])
|
||||
|
|
@ -166,7 +162,6 @@
|
|||
'bvslt @bvslt 'bvsle @bvsle 'bvult @bvult 'bvule @bvule
|
||||
'bvnot @bvnot 'bvor @bvor 'bvand @bvand 'bvxor @bvxor
|
||||
'bvshl @bvshl 'bvlshr @bvlshr 'bvashr @bvashr
|
||||
'ext_rotate_left @z3_ext_rotate_left 'ext_rotate_right @z3_ext_rotate_right
|
||||
'bvneg @bvneg 'bvadd @bvadd 'bvmul @bvmul
|
||||
'bvudiv @bvudiv 'bvsdiv @bvsdiv
|
||||
'bvurem @bvurem 'bvsrem @bvsrem
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@
|
|||
@bvnot @bvor @bvand @bvxor @bvshl @bvlshr @bvashr
|
||||
@bvneg @bvadd @bvmul @bvudiv @bvsdiv @bvurem @bvsrem @bvsmod
|
||||
@concat @extract @zero-extend @sign-extend
|
||||
@z3_ext_rotate_left @z3_ext_rotate_right
|
||||
@integer->bitvector @bitvector->integer @bitvector->natural))
|
||||
|
||||
(provide enc)
|
||||
|
|
@ -109,7 +108,6 @@
|
|||
[@bveq $=] [@bvslt $bvslt] [@bvsle $bvsle] [@bvult $bvult] [@bvule $bvule]
|
||||
[@bvnot $bvnot] [@bvor $bvor] [@bvand $bvand] [@bvxor $bvxor]
|
||||
[@bvshl $bvshl] [@bvlshr $bvlshr] [@bvashr $bvashr]
|
||||
[@z3_ext_rotate_left $ext_rotate_left] [@z3_ext_rotate_right $ext_rotate_right]
|
||||
[@bvneg $bvneg] [@bvadd $bvadd] [@bvmul $bvmul] [@bvudiv $bvudiv] [@bvsdiv $bvsdiv]
|
||||
[@bvurem $bvurem] [@bvsrem $bvsrem] [@bvsmod $bvsmod] [@concat $concat])
|
||||
|
||||
|
|
|
|||
|
|
@ -68,8 +68,7 @@
|
|||
bvnot bvand bvor bvxor
|
||||
bvule bvult bvuge bvugt bvsle bvslt bvsge bvsgt
|
||||
bvneg bvadd bvsub bvmul bvsdiv bvudiv bvurem bvsrem bvsmod
|
||||
bvshl bvlshr bvashr concat
|
||||
ext_rotate_left ext_rotate_right)
|
||||
bvshl bvlshr bvashr concat)
|
||||
|
||||
(define (extract i j s)
|
||||
`((_ extract ,i ,j) ,s))
|
||||
|
|
|
|||
|
|
@ -1,69 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/runtime-path
|
||||
"server.rkt" "env.rkt"
|
||||
"../solver.rkt"
|
||||
(prefix-in base/ "base-solver.rkt"))
|
||||
|
||||
(provide (rename-out [make-stp stp]) stp? stp-available?)
|
||||
|
||||
(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
|
||||
(define stp-opts '("--SMTLIB2"))
|
||||
|
||||
(define (stp-available?)
|
||||
(not (false? (base/find-solver "stp" stp-path #f))))
|
||||
|
||||
(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
|
||||
(define config
|
||||
(cond
|
||||
[(stp? solver)
|
||||
(base/solver-config solver)]
|
||||
[else
|
||||
(define real-stp-path (base/find-solver "stp" stp-path path))
|
||||
(when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
||||
(error 'stp "stp binary is not available (expected to be at ~a); try passing the #:path argument to (stp)" (path->string (simplify-path stp-path))))
|
||||
(base/config options real-stp-path logic)]))
|
||||
(stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
||||
|
||||
(struct stp base/solver ()
|
||||
#:property prop:solver-constructor make-stp
|
||||
#:methods gen:custom-write
|
||||
[(define (write-proc self port mode) (fprintf port "#<stp>"))]
|
||||
#:methods gen:solver
|
||||
[
|
||||
(define (solver-features self)
|
||||
'(qf_bv))
|
||||
|
||||
(define (solver-options self)
|
||||
(base/solver-options self))
|
||||
|
||||
(define (solver-assert self bools)
|
||||
(base/solver-assert self bools))
|
||||
|
||||
(define (solver-minimize self nums)
|
||||
(base/solver-minimize self nums))
|
||||
|
||||
(define (solver-maximize self nums)
|
||||
(base/solver-maximize self nums))
|
||||
|
||||
(define (solver-clear self)
|
||||
(base/solver-clear self))
|
||||
|
||||
(define (solver-shutdown self)
|
||||
(base/solver-shutdown self))
|
||||
|
||||
(define (solver-push self)
|
||||
(base/solver-push self))
|
||||
|
||||
(define (solver-pop self [k 1])
|
||||
(base/solver-pop self k))
|
||||
|
||||
(define (solver-check self)
|
||||
(base/solver-check self))
|
||||
|
||||
(define (solver-debug self)
|
||||
(base/solver-debug self))])
|
||||
|
||||
(define (set-default-options server)
|
||||
void)
|
||||
|
||||
|
|
@ -1,9 +1,13 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/runtime-path
|
||||
"server.rkt" "env.rkt"
|
||||
"server.rkt" "env.rkt" "cmd.rkt"
|
||||
"../solver.rkt"
|
||||
(prefix-in base/ "base-solver.rkt"))
|
||||
(only-in "smtlib2.rkt" get-model echo)
|
||||
(prefix-in base/ "base-solver.rkt")
|
||||
(only-in "../../base/core/term.rkt" term? expression)
|
||||
(only-in "../../base/core/bool.rkt" @forall @exists)
|
||||
(only-in "../../base/core/bitvector.rkt" @integer->bitvector))
|
||||
|
||||
(provide (rename-out [make-yices yices]) yices? yices-available?)
|
||||
|
||||
|
|
@ -11,17 +15,17 @@
|
|||
(define yices-opts '("--incremental"))
|
||||
|
||||
(define (yices-available?)
|
||||
(not (false? (base/find-solver "yices-smt2" yices-path #f))))
|
||||
(define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error
|
||||
(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f])
|
||||
(not (false? (base/find-solver "yices" yices-path #f))))
|
||||
|
||||
(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic 'ALL] #:path [path #f])
|
||||
(define config
|
||||
(cond
|
||||
[(yices? solver)
|
||||
(base/solver-config solver)]
|
||||
[else
|
||||
(define real-yices-path (base/find-solver "yices-smt2" yices-path path))
|
||||
(define real-yices-path (base/find-solver "yices" yices-path path))
|
||||
(when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
||||
(error 'yices "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path))))
|
||||
(error 'yices "yices binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path))))
|
||||
(base/config options real-yices-path logic)]))
|
||||
(yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
||||
|
||||
|
|
@ -32,38 +36,112 @@
|
|||
#:methods gen:solver
|
||||
[
|
||||
(define (solver-features self)
|
||||
'(qf_bv))
|
||||
|
||||
'(qf_bv qf_uf qf_lia qf_lra))
|
||||
|
||||
(define (solver-options self)
|
||||
(base/solver-options self))
|
||||
|
||||
(define (solver-assert self bools)
|
||||
(base/solver-assert self bools))
|
||||
(base/solver-assert self bools yices-wfcheck))
|
||||
|
||||
(define (solver-minimize self nums)
|
||||
(base/solver-minimize self nums))
|
||||
|
||||
|
||||
(define (solver-maximize self nums)
|
||||
(base/solver-maximize self nums))
|
||||
|
||||
|
||||
(define (solver-clear self)
|
||||
(base/solver-clear self))
|
||||
|
||||
|
||||
(define (solver-shutdown self)
|
||||
(base/solver-shutdown self))
|
||||
|
||||
(define (solver-push self)
|
||||
(base/solver-push self))
|
||||
|
||||
|
||||
(define (solver-pop self [k 1])
|
||||
(base/solver-pop self k))
|
||||
|
||||
|
||||
(define (solver-check self)
|
||||
(base/solver-check self))
|
||||
|
||||
(base/solver-check self yices-read-solution))
|
||||
|
||||
(define (solver-debug self)
|
||||
(base/solver-debug self))])
|
||||
|
||||
(define (set-default-options server)
|
||||
void)
|
||||
|
||||
|
||||
; Check whether a term v is well-formed for Yices -- it must not
|
||||
; use integer->bitvector, which Yices doesn't support natively,
|
||||
; nor a quantifier.
|
||||
(define (yices-wfcheck v [cache (mutable-set)])
|
||||
(unless (set-member? cache v)
|
||||
(set-add! cache v)
|
||||
(when (term? v)
|
||||
(match v
|
||||
[(expression (or (== @forall) (== @exists)) vars body)
|
||||
(error 'yices "yices does not support quantified formulas (value: ~v)" v)]
|
||||
[(expression (== @integer->bitvector) rest ...)
|
||||
(error 'yices "yices does not support integer->bitvector (value: ~v)" v)]
|
||||
[(expression op es ...)
|
||||
(for ([e es]) (yices-wfcheck e cache))]
|
||||
[_ #t]))))
|
||||
|
||||
|
||||
; Reads the SMT solution from the server.
|
||||
; The solution consists of 'sat or 'unsat, followed by
|
||||
; followed by a suitably formatted s-expression. The
|
||||
; output of this procedure is a hashtable from constant
|
||||
; identifiers to their SMTLib values (if the solution is 'sat);
|
||||
; a non-empty list of assertion identifiers that form an
|
||||
; unsatisfiable core (if the solution is 'unsat and a
|
||||
; core was extracted); #f (if the solution is
|
||||
; 'unsat and no core was extracted); or 'unknown otherwise.
|
||||
;
|
||||
; For Yices, we need to adapt to its strange way of printing models,
|
||||
; which are just a list of terms of the form (= x y), with no delimiters
|
||||
; for the start and end of a model. We print a "done" symbol to detect when
|
||||
; to stop reading terms. We also need to handle Yices' format for printing
|
||||
; uninterpreted functions:
|
||||
; (= x @fun_6)
|
||||
; (function @fun_6
|
||||
; (type (-> int int))
|
||||
; (= (@fun_6 0) 0)
|
||||
; (= (@fun_6 1) 1)
|
||||
; (default 2))
|
||||
; We convert these models into define-fun forms, with each case becoming
|
||||
; a nested ITE. The define-fun forms have fake type information, since
|
||||
; decode doesn't use it (preferring to use the type info from env).
|
||||
(define (yices-read-solution server env)
|
||||
(define raw-model
|
||||
(parameterize ([current-readtable (make-readtable #f #\# #\a #f)]) ; read BV literals as symbols
|
||||
(match (server-read server (read))
|
||||
[(== 'sat)
|
||||
(server-write server
|
||||
(get-model)
|
||||
(echo "done"))
|
||||
(let loop ([model (hash)][functions (hash)])
|
||||
(match (server-read server (read))
|
||||
[(list (== '=) var val)
|
||||
(loop (hash-set model var `(define-fun ,var () X ,val)) functions)]
|
||||
[(list (== 'function) var type cases ...)
|
||||
(define args (for/list ([x (in-range (- (length (cadr type)) 2))]) (gensym)))
|
||||
(define (call->guard call)
|
||||
(if (equal? (length args) 1)
|
||||
`(= ,(car args) ,(cadr call))
|
||||
`(and ,@(for/list ([a args][c (cdr call)]) `(= ,a ,c)))))
|
||||
(define fun
|
||||
(let inner ([cases cases])
|
||||
(match (car cases)
|
||||
[(list (== 'default) val) val]
|
||||
[(list (== '=) call val)
|
||||
`(ite ,(call->guard call) ,val ,(inner (cdr cases)))])))
|
||||
(loop model
|
||||
(hash-set functions var `(define-fun ,var ,(for/list ([a args]) `(,a X)) X ,fun)))]
|
||||
['done
|
||||
(for/hash ([(var defn) (in-dict model)])
|
||||
(define val (fifth defn))
|
||||
(values var (hash-ref functions val defn)))]
|
||||
[other (error 'read-solution "expected model, given ~a" other)]))]
|
||||
[(== 'unsat) 'unsat]
|
||||
[(== 'unknown) 'unknown]
|
||||
[other (error 'read-solution "unrecognized solver output: ~a" other)])))
|
||||
(decode raw-model env))
|
||||
|
|
|
|||
|
|
@ -30,9 +30,7 @@
|
|||
[else
|
||||
(define real-z3-path (base/find-solver "z3" z3-path path))
|
||||
(when (and (false? real-z3-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
|
||||
(fprintf (current-error-port)
|
||||
"warning: could not find z3 executable at ~a\n"
|
||||
(path->string (simplify-path z3-path))))
|
||||
(printf "warning: could not find z3 executable at ~a\n" (path->string (simplify-path z3-path))))
|
||||
(define opts (hash-union default-options options #:combine (lambda (a b) b)))
|
||||
(base/config opts real-z3-path logic)]))
|
||||
(z3 (server (base/config-path config) z3-opts (base/make-send-options config)) config '() '() '() (env) '()))
|
||||
|
|
@ -54,10 +52,10 @@
|
|||
(base/solver-assert self bools))
|
||||
|
||||
(define (solver-minimize self nums)
|
||||
(base/set-solver-mins! self (append (reverse (numeric-terms nums 'solver-minimize)) (base/solver-mins self))))
|
||||
(base/set-solver-mins! self (append (base/solver-mins self) (numeric-terms nums 'solver-minimize))))
|
||||
|
||||
(define (solver-maximize self nums)
|
||||
(base/set-solver-maxs! self (append (reverse (numeric-terms nums 'solver-maximize)) (base/solver-maxs self))))
|
||||
(base/set-solver-maxs! self (append (base/solver-maxs self) (numeric-terms nums 'solver-maximize))))
|
||||
|
||||
(define (solver-clear self)
|
||||
(base/solver-clear-stacks! self)
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
#lang rosette
|
||||
|
||||
(require
|
||||
rosette/lib/lift
|
||||
(prefix-in racket/ (only-in racket string-append symbol->string regexp-match?)))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
|
|
|||
|
|
@ -3,11 +3,7 @@
|
|||
(require (only-in rosette solver-features current-solver) "base/solver.rkt"
|
||||
rosette/lib/roseunit
|
||||
rosette/solver/smt/z3 rosette/solver/smt/cvc4
|
||||
rosette/solver/smt/boolector
|
||||
rosette/solver/smt/cvc5
|
||||
rosette/solver/smt/bitwuzla
|
||||
rosette/solver/smt/stp
|
||||
rosette/solver/smt/yices
|
||||
rosette/solver/smt/boolector rosette/solver/smt/yices
|
||||
"config.rkt")
|
||||
|
||||
(error-print-width default-error-print-width)
|
||||
|
|
@ -42,7 +38,6 @@
|
|||
"base/distinct.rkt"
|
||||
"base/generics.rkt"
|
||||
"base/push-pop.rkt"
|
||||
"base/optimize-order.rkt"
|
||||
"base/reflect.rkt"
|
||||
"base/decode.rkt"
|
||||
"query/solve.rkt"
|
||||
|
|
@ -86,20 +81,8 @@
|
|||
(printf "===== Running Boolector tests =====\n")
|
||||
(run-tests-with-solver boolector))
|
||||
|
||||
(when (cvc5-available?)
|
||||
(printf "===== Running cvc5 tests =====\n")
|
||||
(run-tests-with-solver cvc5))
|
||||
|
||||
(when (bitwuzla-available?)
|
||||
(printf "===== Running bitwuzla tests =====\n")
|
||||
(run-tests-with-solver bitwuzla))
|
||||
|
||||
(when (stp-available?)
|
||||
(printf "===== Running stp tests =====\n")
|
||||
(run-tests-with-solver stp))
|
||||
|
||||
(when (yices-available?)
|
||||
(printf "===== Running Yices2 tests =====\n")
|
||||
(printf "===== Running Yices tests =====\n")
|
||||
(run-tests-with-solver yices))
|
||||
)
|
||||
|
||||
|
|
|
|||
|
|
@ -272,13 +272,13 @@
|
|||
(define tests:rotate-left
|
||||
(test-suite+
|
||||
"Tests for rotate-left in rosette/base/bvlib.rkt"
|
||||
#:features '(qf_lia int2bv qf_bv)
|
||||
#:features '(qf_lia qf_bv)
|
||||
(check-rotate rotate-left rotate-right bvrol)))
|
||||
|
||||
(define tests:rotate-right
|
||||
(test-suite+
|
||||
"Tests for rotate-right in rosette/base/bvlib.rkt"
|
||||
#:features '(qf_lia int2bv qf_bv)
|
||||
#:features '(qf_lia qf_bv)
|
||||
(check-rotate rotate-right rotate-left bvror)))
|
||||
|
||||
(module+ test
|
||||
|
|
|
|||
|
|
@ -1,27 +0,0 @@
|
|||
#lang rosette
|
||||
|
||||
;; This test is taken from https://www.philipzucker.com/z3-rise4fun/optimization.html
|
||||
|
||||
(require rackunit rackunit/text-ui racket/generator
|
||||
rosette/lib/roseunit)
|
||||
|
||||
(current-bitwidth #f)
|
||||
(define-symbolic x y z integer?)
|
||||
|
||||
(define (check-model sol m)
|
||||
(check-pred sat? sol)
|
||||
(check-equal? (model sol) m))
|
||||
|
||||
(define optimization-order-tests
|
||||
(test-suite+ "Tests for the optimization order"
|
||||
#:features '(optimize)
|
||||
|
||||
(define solver (current-solver))
|
||||
(solver-clear solver)
|
||||
(solver-assert solver (list (< x z) (< y z) (< z 5) (not (= x y))))
|
||||
(solver-maximize solver (list x))
|
||||
(solver-maximize solver (list y))
|
||||
(check-model (solver-check solver) (hash x 3 y 2 z 4))))
|
||||
|
||||
(module+ test
|
||||
(time (run-tests optimization-order-tests)))
|
||||
|
|
@ -14,10 +14,6 @@
|
|||
(define-symbolic b @boolean?)
|
||||
(define-symbolic c @boolean?)
|
||||
|
||||
(define (f type)
|
||||
(define-symbolic x type)
|
||||
x)
|
||||
|
||||
(define (check-ordered v1 v2)
|
||||
(check-true (and (or (term<? v1 v2) (term<? v2 v1))
|
||||
(not (and (term<? v1 v2) (term<? v2 v1))))))
|
||||
|
|
@ -53,47 +49,7 @@
|
|||
(check-cached @/ x y)
|
||||
(check-cached @remainder x y)
|
||||
(check-cached @= x y)
|
||||
(check-cached @< x y)
|
||||
|
||||
(f @integer?)
|
||||
(check-exn #px"type should remain unchanged" (lambda () (f @boolean?)))))
|
||||
|
||||
(define clear-terms!+gc-terms!-tests
|
||||
(test-suite+
|
||||
"Tests for clear-terms! and gc-terms!"
|
||||
|
||||
(with-terms '()
|
||||
(let ()
|
||||
(define-symbolic x y z @integer?)
|
||||
(define a (@+ x 1))
|
||||
(define b (@+ y 2))
|
||||
(define c (@+ z 3))
|
||||
(check-equal? (length (terms)) 6)
|
||||
|
||||
;; this should evict z and c
|
||||
(clear-terms! (list z))
|
||||
|
||||
(check-equal? (length (terms)) 4)
|
||||
|
||||
;; this doesn't affect strongly-held values
|
||||
(set! b #f)
|
||||
|
||||
(check-equal? (length (terms)) 4)
|
||||
|
||||
(gc-terms!) ; change the representation
|
||||
(collect-garbage)
|
||||
|
||||
(check-equal? (length (terms)) 3)
|
||||
|
||||
(clear-terms! (list x))
|
||||
(collect-garbage)
|
||||
|
||||
(check-equal? (length (terms)) 1)
|
||||
|
||||
;; this is a dummy check to reference a, b, and c so that
|
||||
;; they are not garbage-collected earlier
|
||||
(check-equal? (length (list a b c)) 3)))))
|
||||
(check-cached @< x y)))
|
||||
|
||||
(module+ test
|
||||
(time (run-tests value-tests))
|
||||
(time (run-tests clear-terms!+gc-terms!-tests)))
|
||||
(time (run-tests value-tests)))
|
||||
|
|
|
|||
Loading…
Reference in New Issue