From fe08c62ca4a126968d9b65a3590329b4fcdbc9a5 Mon Sep 17 00:00:00 2001 From: Chenglong Date: Fri, 20 Jan 2017 11:01:56 -0800 Subject: [PATCH] migrate from internal --- .gitignore | 1 + rosette/cosette.rkt | 30 ++++++++++ rosette/playground/eg-1.rkt | 22 +++++++ rosette/playground/eg-2.rkt | 57 +++++++++++++++++++ rosette/playground/eg-3.rkt | 54 ++++++++++++++++++ rosette/{main.rkt => playground/examples.rkt} | 0 .../query-examples.rkt} | 0 .../raw-queries.rkt} | 0 rosette/tests/aggr-join.rkt | 4 +- rosette/tests/aggr-pull-up.rkt | 17 +++--- rosette/{ => tests}/run-tests.sh | 11 ++-- rosette/util.rkt | 23 ++++++++ 12 files changed, 201 insertions(+), 18 deletions(-) create mode 100644 rosette/cosette.rkt create mode 100644 rosette/playground/eg-1.rkt create mode 100644 rosette/playground/eg-2.rkt create mode 100644 rosette/playground/eg-3.rkt rename rosette/{main.rkt => playground/examples.rkt} (100%) rename rosette/{queries.rkt => playground/query-examples.rkt} (100%) rename rosette/{Structs.rkt => playground/raw-queries.rkt} (100%) rename rosette/{ => tests}/run-tests.sh (74%) create mode 100644 rosette/util.rkt diff --git a/.gitignore b/.gitignore index 121a87b..b0ae9a9 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ *.vo #*# *.glob +*.DS_Store diff --git a/rosette/cosette.rkt b/rosette/cosette.rkt new file mode 100644 index 0000000..1e2f6d0 --- /dev/null +++ b/rosette/cosette.rkt @@ -0,0 +1,30 @@ +; The rosette interface for cosette + +#lang rosette + +(require "util.rkt" "table.rkt" "equal.rkt" "sql.rkt") +(require racket/pretty) +(require json) + +(provide cosette-sol->json + cosette-solve) + +(define (cosette-sol->json solution) + (let ([status (car solution)] + [tables (cdr solution)]) + (jsexpr->string + (hasheq 'status status + 'counter-example (map (lambda (t) (table->jsexpr t)) tables))))) + +(define (cosette-solve q1 q2 input-tables) + (let ([solution (verify (same q1 q2))]) + (cond + [(sat? solution) (cons "neq" (evaluate input-tables solution))] + [else (cons "eq" (list))]))) + +(define (table->jsexpr t) + (hasheq 'table-name (get-table-name t) + 'table-content (list (get-schema t) + (map (lambda (r) (list (car r) (cdr r))) + (get-content t))))) + diff --git a/rosette/playground/eg-1.rkt b/rosette/playground/eg-1.rkt new file mode 100644 index 0000000..04d0aef --- /dev/null +++ b/rosette/playground/eg-1.rkt @@ -0,0 +1,22 @@ +#lang rosette + +(require "../cosette.rkt" "../util.rkt" "../table.rkt" "../sql.rkt" "../evaluator.rkt" "../equal.rkt") + +(define t1 (Table "t1" (list "id") (gen-sym-schema 1 3))) +(define t2 (Table "t2" (list "id") (list))) + +;(define t2 (Table "t1" (list "id") (list (cons (list 0) 0)))) + +; SELECT * AS u FROM users WHERE id = 1 + +(define q1 + (SELECT (VALS "t1.id") + FROM (NAMED t1) + WHERE (BINOP "t1.id" = 1))) + +(define q2 (NAMED t2)) + +(cosette-sol->json (cosette-solve q1 q2 (list t1 t2))) +;(map (lambda (t) (table-to-json-obj t)) (cosette-verify q1 q2 (list t1 t2))) +;(time (verify (same q1 q2))) +;(time (verify (neq q1 q2))) diff --git a/rosette/playground/eg-2.rkt b/rosette/playground/eg-2.rkt new file mode 100644 index 0000000..06ab76e --- /dev/null +++ b/rosette/playground/eg-2.rkt @@ -0,0 +1,57 @@ +#lang rosette + +(require "../test-util.rkt" "../../table.rkt" "../../sql.rkt" "../../evaluator.rkt" "../../equal.rkt") + +(define (aggr-sum l) + (foldl + 0 (map (lambda (x) (* (car (car x)) (cdr x))) + (get-content l)))) + +(define t1 (Table "votes" (list "vote" "story_id") (gen-sym-schema 2 3))) +(define t2 (Table "stories" (list "id") (gen-sym-schema 1 2))) + +(define ct1 + (Table "votes" (list "vote" "story_id") + (list (cons (list 2 3) 2) + (cons (list 1 3) 1) + (cons (list 2 1) 3)))) + +(define ct2 + (Table "stories" (list "id") + (list (cons (list 2) 1) + (cons (list 3) 1)))) + + +(define t3 (Table "t" (list "sum") (list (cons (list -1) 1)))) +(define t4 (Table "t" (list "sum") (list))) + + +;(define t2 (Table "t1" (list "id") (list (cons (list 0) 0)))) + +; SELECT SUM(vote) AS sumv FROM votes AS v INNER JOIN stories AS s ON v.story_id = s.id; + +(define q1 + (SELECT (VALS (AGGR aggr-sum (SELECT (VALS "v.vote") + FROM (JOIN (AS (NAMED t1) ["v" (list "vote" "story_id")]) + (AS (NAMED t2) ["s" (list "id")])) + WHERE (BINOP "v.story_id" = "s.id")))) + FROM (NAMED t3) + WHERE (filter-empty))) + +(define q2 (NAMED t3)) + +(define q3 + (SELECT (VALS "j.s1") + FROM (AS (JOIN q1 q2) + ["j" (list "s1" "s2")]) + WHERE (BINOP "j.s1" > "j.s2"))) + +(define q4 (NAMED t4)) + +;(run q1) +;(get-content (run q2)) +;(get-content (run q3)) +;(get-content (run q4)) + +(time (verify (same q3 q4))) +(time (verify (neq q3 q4))) + diff --git a/rosette/playground/eg-3.rkt b/rosette/playground/eg-3.rkt new file mode 100644 index 0000000..a50a925 --- /dev/null +++ b/rosette/playground/eg-3.rkt @@ -0,0 +1,54 @@ +#lang rosette + +(require "../test-util.rkt" "../../table.rkt" "../../sql.rkt" "../../evaluator.rkt" "../../equal.rkt") + +;(current-bitwidth 32) + +(define (aggr-count l) + (foldl + 0 (map cdr (get-content l)))) + +(define t (Table "t" (list "v") (gen-sym-schema 1 8))) +(define ct (Table "t" (list "v") (list (cons (list 1) 10) (cons (list 2) 12)))) +(define t3 (Table "t" (list "v") (list (cons (list 50) 1)))) +(define t4 (Table "t" (list "v") (list))) + +;(define t2 (Table "t1" (list "id") (list (cons (list 0) 0)))) + +; SELECT SUM(vote) AS sumv FROM votes AS v INNER JOIN stories AS s ON v.story_id = s.id; + +(define q1 + (SELECT-DISTINCT + (VALS (AGGR aggr-count (SELECT-DISTINCT (VALS "t.v") FROM (NAMED t) WHERE (filter-empty)))) + FROM (NAMED t3) + WHERE (filter-empty))) + +(define cq1 + (SELECT-DISTINCT (VALS (AGGR aggr-count (SELECT-DISTINCT (VALS "t.v") FROM (NAMED ct) WHERE (filter-empty)))) + FROM (NAMED t3) + WHERE (filter-empty))) + +(define q2 + (SELECT (VALS "j.s1") + FROM (AS q1 ["j" (list "s1")]) + WHERE (BINOP "j.s1" < 8))) + +(define cq2 + (SELECT (VALS "j.s1") + FROM (AS cq1 ["j" (list "s1")]) + WHERE (BINOP "j.s1" < 50))) + +(define q4 (NAMED t4)) + +;(run cq1) +;(run cq2) +;(run q4) + +;(time (verify (same cq2 q4))) +;(time (verify (neq q2 q4))) +;(get-content (run q2)) +;(get-content (run q3)) +;(get-content (run q4)) + +(time (verify (same q2 q4))) +(time (verify (neq q2 q4))) + diff --git a/rosette/main.rkt b/rosette/playground/examples.rkt similarity index 100% rename from rosette/main.rkt rename to rosette/playground/examples.rkt diff --git a/rosette/queries.rkt b/rosette/playground/query-examples.rkt similarity index 100% rename from rosette/queries.rkt rename to rosette/playground/query-examples.rkt diff --git a/rosette/Structs.rkt b/rosette/playground/raw-queries.rkt similarity index 100% rename from rosette/Structs.rkt rename to rosette/playground/raw-queries.rkt diff --git a/rosette/tests/aggr-join.rkt b/rosette/tests/aggr-join.rkt index 018efbc..62719fd 100644 --- a/rosette/tests/aggr-join.rkt +++ b/rosette/tests/aggr-join.rkt @@ -9,8 +9,8 @@ ; (define ta (Table "R" (list "A" "B") concrete-table-2-col)) ; (define tb (Table "S" (list "C" "D") concrete-table-2-col)) -(define ta (Table "R" (list "A" "B") (gen-sym-schema 2 num-rows-in-sym-table))) -(define tb (Table "S" (list "C" "D") (gen-sym-schema 2 num-rows-in-sym-table))) +(define ta (Table "R" (list "A" "B") (gen-sym-schema 2 2))) +(define tb (Table "S" (list "C" "D") (gen-sym-schema 2 2))) (define (aggr-sum l) (foldl + 0 (map (lambda (x) (* (car (car x)) (cdr x))) diff --git a/rosette/tests/aggr-pull-up.rkt b/rosette/tests/aggr-pull-up.rkt index 09380d4..e55d744 100644 --- a/rosette/tests/aggr-pull-up.rkt +++ b/rosette/tests/aggr-pull-up.rkt @@ -5,9 +5,7 @@ (define (same q1 q2) (assert (bag-equal (get-content (run q1)) (get-content (run q2))))) - - -(define t1 (Table "t1" (list "c1" "c2" "c3") (gen-sym-schema 3 num-rows-in-sym-table))) +(define t1 (Table "t1" (list "c1" "c2" "c3") (gen-sym-schema 3 3))) ; (define t1 (Table "t1" (list "c1" "c2" "c3") concrete-table-3-col)) (define (aggr-sum l) @@ -71,16 +69,15 @@ (define model (time (verify (same subq-aggr-1 subq-aggr-2)))) (define model2 (verify (same subq-aggr-1 subq-aggr-wrong-2))) -model - +;model model2 -(evaluate t1 model2) -(evaluate (run subq-aggr-1) model2) +;(evaluate t1 model2) +;(evaluate (run subq-aggr-1) model2) ;(evaluate (run subq-aggr-wrong-2) model2) -(println "========") -(println "========") -(denote-sql subq-aggr-1 (make-hash)) +;(println "========") +;(println "========") +;(denote-sql subq-aggr-1 (make-hash)) ;(evaluate (Table-content t1) model) ;(evaluate (run subq-aggr-1) model) diff --git a/rosette/run-tests.sh b/rosette/tests/run-tests.sh similarity index 74% rename from rosette/run-tests.sh rename to rosette/tests/run-tests.sh index 60f43aa..431612a 100755 --- a/rosette/run-tests.sh +++ b/rosette/tests/run-tests.sh @@ -7,9 +7,9 @@ if [[ "$UNAME" == "Darwin" ]]; then fi function run_test { - for i in `seq 1 $3`; + for i in `seq 1 $2`; do - $SED "s/[0-9]/$i/" $2; + $SED "s/[0-9]/$i/"; for j in `seq 0 2`; do racket $1 | grep "cpu time" & @@ -19,8 +19,7 @@ function run_test { done; } -TEST_DIR=tests -ARGS_FILE=args.rkt +TEST_DIR=. EASY_TESTS="simpleRA.rkt push-projection.rkt subquery-exists.rkt magic-set.rkt" HARD_TESTS="aggr-pull-up.rkt subquery-test.rkt aggr-join.rkt" @@ -28,13 +27,13 @@ HARD_TESTS="aggr-pull-up.rkt subquery-test.rkt aggr-join.rkt" for test in $EASY_TESTS; do echo "============== $test =============="; - run_test $TEST_DIR/$test $TEST_DIR/$ARGS_FILE 4; + run_test $TEST_DIR/$test 4; done; wait for test in $HARD_TESTS; do echo "============== $test =============="; - run_test $TEST_DIR/$test $TEST_DIR/$ARGS_FILE 2; + run_test $TEST_DIR/$test 2; done; wait diff --git a/rosette/util.rkt b/rosette/util.rkt new file mode 100644 index 0000000..1f91678 --- /dev/null +++ b/rosette/util.rkt @@ -0,0 +1,23 @@ +#lang rosette + +(require "table.rkt" "equal.rkt" "sql.rkt") +(require json) + +(provide (all-defined-out)) + +;; assertions + +(define (same q1 q2) + (assert (bag-equal (get-content (run q1)) (get-content (run q2))))) + +(define (neq q1 q2) + (assert (not (bag-equal (get-content (run q1)) (get-content (run q2)))))) + +;; aggregation functions + +(define (aggr-count l) + (foldl + 0 (map cdr (get-content l)))) + +(define (aggr-sum l) + (foldl + 0 (map (lambda (x) (* (car (car x)) (cdr x))) + (get-content l))))