search

uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
666 stars 54 forks source link

Cosette freezes (different from #63) #70

Closed primeapple closed 5 years ago

primeapple commented 5 years ago

Hey guys, I found another issue, you may not know about: When trying Cosette with a big chunk of queries, I had it freeze on one test:

schema schema_film_actor (last_update:Date, actor_id:Integer, film_id:Integer);
table film_actor(schema_film_actor);

schema schema_film (special_features:String, rental_duration:Integer, rental_rate:Double, release_year:Integer, length:Integer, replacement_cost:Double, rating:String, description:String, language_id:Integer, title:String, original_language_id:Integer, last_update:Date, film_id:Integer);
table film(schema_film);

query student
`SELECT DISTINCT t_0.film_id, t_0.title FROM film t_0, film t_1, film_actor t_2, film_actor t_3, film_actor t_4, film_actor t_5 WHERE NOT t_4.actor_id = t_2.actor_id AND t_4.actor_id = t_5.actor_id AND t_2.actor_id = t_3.actor_id AND t_2.film_id = t_0.film_id AND t_4.film_id = t_0.film_id AND t_3.film_id = t_1.film_id AND t_5.film_id = t_1.film_id AND t_0.rental_rate > (t_1.rental_rate * 2)`;

query master
`SELECT DISTINCT t_0.film_id, t_0.title FROM film t_0, film t_1, film_actor t_2, film_actor t_3, film_actor t_4, film_actor t_5`;

verify student master

I had the process: /HoTT/coq-HoTT/bin/coqtop -coqlib /usr/local/share/hott/coq -R /usr/local/share/hott/theories HoTT -Q /usr/local/share/hott/contrib -indices-matter -q -R . Cosette -compile WCiEiXyyQYrrQ.v running a couple hours on 100% for one core of my CPU. After I killed it, Cosette gave me the result:

CLICK ME

` {"rosette_log": "Rosette find an counterexample.", "coq_result": "ERROR", "coq_log": "Invalid generated Coq code. Please file an issue.", "rosette_source": "#lang rosette \n \n(require \"../cosette.rkt\" \"../sql.rkt\" \"../evaluator.rkt\" \"../syntax.rkt\") \n \n(provide ros-instance)\n \n(current-bitwidth #f)\n \n(define-symbolic div_ (~> integer? integer? integer?))\n \n(define film-info (table-info \"film\" (list \"special_features\" \"rental_duration\" \"rental_rate\" \"release_year\" \"length\" \"replacement_cost\" \"rating\" \"description\" \"language_id\" \"title\" \"original_language_id\" \"last_update\" \"film_id\")))\n \n(define film_actor-info (table-info \"film_actor\" (list \"last_update\" \"actor_id\" \"film_id\")))\n \n\n(define (student tables) \n (SELECT-DISTINCT (VALS \"t_0.film_id\" \"t_0.title\") \n FROM (JOIN (AS (NAMED (list-ref tables 0)) [\"t_0\"]) (JOIN (AS (NAMED (list-ref tables 0)) [\"t_1\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_2\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_3\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_4\"]) (AS (NAMED (list-ref tables 1)) [\"t_5\"])))))) \n WHERE (AND (AND (AND (AND (AND (AND (AND (NOT (BINOP \"t_4.actor_id\" = \"t_2.actor_id\")) (BINOP \"t_4.actor_id\" = \"t_5.actor_id\")) (BINOP \"t_2.actor_id\" = \"t_3.actor_id\")) (BINOP \"t_2.film_id\" = \"t_0.film_id\")) (BINOP \"t_4.film_id\" = \"t_0.film_id\")) (BINOP \"t_3.film_id\" = \"t_1.film_id\")) (BINOP \"t_5.film_id\" = \"t_1.film_id\")) (BINOP \"t_0.rental_rate\" > (VAL-BINOP \"t_1.rental_rate\" * 2)))))\n\n(define (master tables) \n (SELECT-DISTINCT (VALS \"t_0.film_id\" \"t_0.title\") \n FROM (JOIN (AS (NAMED (list-ref tables 0)) [\"t_0\"]) (JOIN (AS (NAMED (list-ref tables 0)) [\"t_1\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_2\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_3\"]) (JOIN (AS (NAMED (list-ref tables 1)) [\"t_4\"]) (AS (NAMED (list-ref tables 1)) [\"t_5\"])))))) \n WHERE (TRUE)))\n\n\n(define ros-instance (list student master (list film-info film_actor-info))) \n", "result": "ERROR", "counterexamples": [{"table-content": [["special_features", "rental_duration", "rental_rate", "release_year", "length", "replacement_cost", "rating", "description", "language_id", "title", "original_language_id", "last_update", "film_id"], [[[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], 15]]], "table-name": "film"}, {"table-content": [["last_update", "actor_id", "film_id"], [[[0, 0, 0], 2]]], "table-name": "film_actor"}], "rosette_result": "NEQ", "error_msg": "Invalid generated Coq code. Please file an issue. \n \n Rosette find an counterexample.", "coq_source": "Require Import HoTT. \nRequire Import UnivalenceAxiom. \nRequire Import HoTTEx. \nRequire Import Denotation. \nRequire Import UnivalentSemantics. \nRequire Import AutoTactics. \nRequire Import CQTactics. \n \nOpen Scope type. \n \nModule Optimization (T : Types) (S : Schemas T) (R : Relations T S) (A : Aggregators T S). \n Import T S R A. \n Module SQL_TSRA := SQL T S R A. \n Import SQL_TSRA. \n Module AutoTac := AutoTactics T S R A. \n Import AutoTac. \n Module CQTac := CQTactics T S R A. \n Import CQTac. \n \n Notation combine' := combineGroupByProj.\n \n Parameter count : forall {T}, aggregator T int. \n Notation \"'COUNT' ( e )\" := (aggregatorGroupByProj count e). \n Parameter sum : forall {T}, aggregator T int. \n Notation \"'SUM' ( e )\" := (aggregatorGroupByProj sum e). \n Parameter max : forall {T}, aggregator T int. \n Notation \"'MAX' ( e )\" := (aggregatorGroupByProj max e). \n Parameter min : forall {T}, aggregator T int. \n Notation \"'MIN' ( e )\" := (aggregatorGroupByProj min e). \n Parameter avg : forall {T}, aggregator T int. \n Notation \"'AVG' ( e )\" := (aggregatorGroupByProj avg e).\n \n Parameter gt: Pred (node (leaf int) (leaf int)). \n \n Variable integer_2: constant int. \n\n\n Definition Rule: Type. \n refine (forall ( \u0393 scm_schema_film scm_schema_film_actor: Schema) (rel_film: relation scm_schema_film) (rel_film_actor: relation scm_schema_film_actor) (schema_film_special_features : Column int scm_schema_film) (schema_film_rental_duration : Column int scm_schema_film) (schema_film_rental_rate : Column int scm_schema_film) (schema_film_release_year : Column int scm_schema_film) (schema_film_length : Column int scm_schema_film) (schema_film_replacement_cost : Column int scm_schema_film) (schema_film_rating : Column int scm_schema_film) (schema_film_description : Column int scm_schema_film) (schema_film_language_id : Column int scm_schema_film) (schema_film_title : Column int scm_schema_film) (schema_film_original_language_id : Column int scm_schema_film) (schema_film_last_update : Column int scm_schema_film) (schema_film_film_id : Column int scm_schema_film) (schema_film_actor_last_update : Column int scm_schema_film_actor) (schema_film_actor_actor_id : Column int scm_schema_film_actor) (schema_film_actor_film_id : Column int scm_schema_film_actor), _). \n refine (\u27e6 \u0393 \u22a2 DISTINCT (SELECT1 (combine (right\u22c5left\u22c5schema_film_film_id) (right\u22c5left\u22c5schema_film_title)) FROM1 (product (table rel_film) (product (table rel_film) (product (table rel_film_actor) (product (table rel_film_actor) (product (table rel_film_actor) (table rel_film_actor)))))) WHERE (and (and (and (and (and (and (and (negate (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)) (variable (right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)) (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5schema_film_actor_actor_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)) (variable (right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_actor_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_film_id)) (variable (right\u22c5left\u22c5schema_film_film_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_film_id)) (variable (right\u22c5left\u22c5schema_film_film_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5left\u22c5schema_film_actor_film_id)) (variable (right\u22c5right\u22c5left\u22c5schema_film_film_id)))) (equal (variable (right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5right\u22c5schema_film_actor_film_id)) (variable (right\u22c5right\u22c5left\u22c5schema_film_film_id)))) (castPred (combine (right\u22c5left\u22c5schema_film_rental_rate) (e2p (binaryExpr times_ (variable (right\u22c5right\u22c5left\u22c5schema_film_rental_rate)) (constantExpr integer_2))) ) gt))) : _ \u27e7 = \u27e6 \u0393 \u22a2 DISTINCT (SELECT1 (combine (right\u22c5left\u22c5schema_film_film_id) (right\u22c5left\u22c5schema_film_title)) FROM1 (product (table rel_film) (product (table rel_film) (product (table rel_film_actor) (product (table rel_film_actor) (product (table rel_film_actor) (table rel_film_actor)))))) ) : _ \u27e7). \n Defined. \n Arguments Rule /. \n \n Lemma ruleStand: Rule. \n start;\n first [sum_heuristic1| prod_heuristic1| deductive_proof'| conjunctiveQueryProof'| hott_ring']. \n Qed. \n \nEnd Optimization. \n"} `

Also, because it was pretty late already, I yesterday submitted the query to your Cosette Online Demo: https://demo.cosette.cs.washington.edu/ It is not available for me anymore (502 Proxy Error), I think I just broke your website, I'm sorry... :(

You should think about implementing some kind of timeout in your python script to kill threads like this, that do not get catched by the implemented timeout method.

EDIT: The website seems to be back up, which is nice. However, I would suggest you test it out for yourselfs with the query. I'm a little afraid to touch your webinterface again ;-)

Mestway commented 5 years ago

Hi! Sorry about the late reply. I have just tested it and the query is working in the current version now.

We do have a time-out mechanism but not sure what happened exactly at that time.

We'll incorporate the change on the demo host soon. Thanks a lot!