diff --git a/bin/counterexample.ml b/bin/counterexample.ml new file mode 100644 index 0000000..b2189fc --- /dev/null +++ b/bin/counterexample.ml @@ -0,0 +1,56 @@ +open Birds +open Expr + +let parse_args = + let log = ref false in + let cex_max = ref 5 in + let timeout = ref 180 in + let inputs = ref [] in + let anon_fun input = inputs := input :: !inputs in + let usage = "usage: dune exec counterexample [getput|putget|disdelta] [filename]" in + let speclist = [ + ("--log", Arg.Unit (fun () -> log := true), " Print running information"); + ("-x", Arg.Int (fun d -> cex_max := d), " Get a counterexample with the maximum size if the program is not well-behaved"); + ("--counterexample", Arg.Int (fun d -> cex_max := d), " The same as -x"); + ("-t", Arg.Int (fun d -> timeout := d), " Timeout (second) (default: 180s)"); + ("--timeout", Arg.Int (fun d -> timeout := d), " The same as -t"); + ] in + let _ = Arg.parse (Arg.align speclist) anon_fun usage in + (!log, !cex_max, !timeout, !inputs |> List.rev |> Array.of_list) + +let parse_property (property: string) = + match property with + | "getput" -> Result.Ok Counterexample.Getput + | "putget" -> Result.Ok Counterexample.Putget + | "disdelta" -> Result.Ok Counterexample.Disdelta + | p -> Result.Error ("function gen_counterexample called with an unkown property: " ^ p) + +let _ = + let (log, cex_max, timeout, inputs) = parse_args in + if Array.length inputs < 2 then + print_endline "Invalid arguments. File name must be passed." + else begin + let _ = Array.iter print_endline inputs in + let filename = inputs.(1) in + match parse_property inputs.(0) with + | Result.Error err -> + print_endline @@ err + | Result.Ok property -> + let chan = open_in filename in + let lexbuf = Lexing.from_channel chan in + let ast = Parser.main Lexer.token lexbuf in + let constr_ast = Utils.constraint2rule ast in + let error, counterexample = Counterexample.gen_counterexample log property cex_max timeout constr_ast in + let m = match property with + | Counterexample.Getput -> + if (error = "") then ("% Invalidity: The following counterexample shows that getput is not satisfied:\n" ^ string_of_prog {get_empty_expr with facts = counterexample} ) + else "% Fail to generate a counterexample of getput: " ^error + | Counterexample.Putget -> + if (error = "") then ("% Invalidity: The following counterexample shows that putget is not satisfied:\n" ^ string_of_prog {get_empty_expr with facts = counterexample}) + else "% Fail to generate a counterexample of putget: " ^error + | Counterexample.Disdelta -> + if (error = "") then ("% Invalidity: The following counterexample shows that deltas in the datalog program are not disjoint:\n" ^ (string_of_prog {get_empty_expr with facts = counterexample}) ) + else "% Fail to generate a couterexample of delta disjointness: " ^ error + in + print_endline m + end diff --git a/bin/dune b/bin/dune index 7998f69..7b7b049 100644 --- a/bin/dune +++ b/bin/dune @@ -46,3 +46,8 @@ (modules removebottom) (libraries birds)) +(executable + (public_name counterexample) + (name counterexample) + (modules counterexample) + (libraries birds)) diff --git a/examples/verify_invalid_getput1.dl b/examples/verify_invalid_getput1.dl new file mode 100644 index 0000000..6ccc0c4 --- /dev/null +++ b/examples/verify_invalid_getput1.dl @@ -0,0 +1,9 @@ +source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int). +view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int). +% view definition: +tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2. +% putdelta ++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q). +-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q). +% constraints +_|_ :- tracks3(T,R,A,Q), Q <= 2. diff --git a/examples/verify_invalid_getput2.dl b/examples/verify_invalid_getput2.dl new file mode 100644 index 0000000..9124ff8 --- /dev/null +++ b/examples/verify_invalid_getput2.dl @@ -0,0 +1,13 @@ +source a('A':int, 'B':int). +source b('B':int, 'C':int). +view s('A':int, 'B':int, 'C':int). +% view definition +s(A,B,C) :- a(A,B), b(B,C). +% putdelta +-a(A,B) :- a(A,B), not s(A,B,_). ++a(A,B) :- s(A,B,_), not a(A,B). +-b(B,C) :- b(B,C), s(_,B,_), not s(_,B,C). ++b(B,C) :- s(_,B,C), not b(B,C). +% constraints +%_|_ :- a(_,B), not b(B,_). +_|_ :- s(_,B,C1), s(_,B,C2), C1<>C2. diff --git a/examples/verify_invalid_putget1.dl b/examples/verify_invalid_putget1.dl new file mode 100644 index 0000000..2459d73 --- /dev/null +++ b/examples/verify_invalid_putget1.dl @@ -0,0 +1,9 @@ +source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int). +view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int). +% view definition: +tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2. +% putdelta ++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q). +-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q). +% constraints +%_|_ :- tracks3(T,R,A,Q), Q <= 2. diff --git a/examples/verify_invalid_putget2.dl b/examples/verify_invalid_putget2.dl new file mode 100644 index 0000000..c1bc6e2 --- /dev/null +++ b/examples/verify_invalid_putget2.dl @@ -0,0 +1,13 @@ +source a('A':int, 'B':int). +source b('B':int, 'C':int). +view s('A':int, 'B':int, 'C':int). +% view definition +s(A,B,C) :- a(A,B), b(B,C). +% putdelta +%-a(A,B) :- a(A,B), not s(A,B,_). ++a(A,B) :- s(A,B,_), not a(A,B). +-b(B,C) :- b(B,C), s(_,B,_), not s(_,B,C). ++b(B,C) :- s(_,B,C), not b(B,C). +% constraints +_|_ :- a(_,B), not b(B,_). +_|_ :- s(_,B,C1), s(_,B,C2), C1<>C2. diff --git a/examples/verify_valid1.dl b/examples/verify_valid1.dl new file mode 100644 index 0000000..ca2c7b7 --- /dev/null +++ b/examples/verify_valid1.dl @@ -0,0 +1,9 @@ +source tracks2('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int). +view tracks3('TRACK':string,'RATING':int,'ALBUM':string,'QUANTITY':int). +% view definition: +tracks3(T,R,A,Q) :- tracks2(T,R,A,Q),Q > 2. +% putdelta ++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q). +-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q), Q > 2. +% constraints +_|_ :- tracks3(T,R,A,Q), Q <= 2. diff --git a/examples/verify_valid2.dl b/examples/verify_valid2.dl new file mode 100644 index 0000000..2dbd8dc --- /dev/null +++ b/examples/verify_valid2.dl @@ -0,0 +1,13 @@ +source a('A':int, 'B':int). +source b('B':int, 'C':int). +view s('A':int, 'B':int, 'C':int). +% view definition +s(A,B,C) :- a(A,B), b(B,C). +% putdelta +-a(A,B) :- a(A,B), not s(A,B,_). ++a(A,B) :- s(A,B,_), not a(A,B). +-b(B,C) :- b(B,C), s(_,B,_), not s(_,B,C). ++b(B,C) :- s(_,B,C), not b(B,C). +% constraints +_|_ :- a(_,B), not b(B,_). +_|_ :- s(_,B,C1), s(_,B,C2), C1<>C2. diff --git a/src/ast2ros.ml b/src/ast2ros.ml new file mode 100644 index 0000000..d9a1aa7 --- /dev/null +++ b/src/ast2ros.ml @@ -0,0 +1,802 @@ +(*******************************************************) +(** +AST-to-Racket functions + *) +(********************************************************) +(* +@author: Vandang Tran +*) + +open Logic +open Expr +open Utils +open Rule_preprocess +open Derivation + +(** Given an aggregate function name, check if it is supported and returns it. *) +let check_agg_function fn = + let allowed = ["MAX";"MIN";"SUM";"AVG";"COUNT"] in + if List.mem fn allowed then fn + else raise (SemErr ( + "Aggregate function '"^fn^"' is not supported, "^ + "allowed functions are: "^(String.concat ", " allowed) + )) + +(** Given an arithmetic expression, return it in racket, this function is similar to string_of_vterm. *) +let racket_of_vterm (vt:vartab) (eqt:eqtab) (expr:vterm) = + let open_paren prec op_prec = + if prec > op_prec then "(" else "" in + let close_paren prec op_prec = + if prec > op_prec then ")" else "" in + let rec racket_of prec a_expr = match a_expr with + | Const c -> string_of_const c + | Var variable -> + (*If the variable appears in a positive rterm, the value + * is the name of the respective rterm's table column*) + if Hashtbl.mem vt (string_of_var variable) + then List.hd (Hashtbl.find vt (string_of_var variable)) + (*If the variable does not appear in a positive rterm, but + * it does in an equality value, then the value is the eq's evaluation*) + else if Hashtbl.mem eqt (Var variable) + then + let ve = (Hashtbl.find eqt (Var variable)) in racket_of prec ve + (*Else, the query is unsafe or inclomplete*) + else raise (SemErr ( + "Can not evaluate variable "^(string_of_var variable)^" because it is not in a positive "^ + "goal or strict equality relation." + ) + ) + | BinaryOp("+",f,g) -> (open_paren prec 0)^ (racket_of 0 f) ^ "+" ^ (racket_of 0 g) ^ (close_paren prec 0) + | BinaryOp("-",f,g) -> (open_paren prec 0) ^ (racket_of 0 f) ^ "-" ^ (racket_of 1 g) ^ (close_paren prec 0) + | BinaryOp("*",f,g) -> (open_paren prec 2) ^ (racket_of 2 f) ^ "*" ^ (racket_of 2 g) ^ (close_paren prec 2) + | BinaryOp("/",f,g) -> (open_paren prec 2)^ (racket_of 2 f) ^ "/" ^ (racket_of 3 g) ^ (close_paren prec 2) + | UnaryOp ("-", e) -> (open_paren prec 4)^ "-" ^ (racket_of 5 e)^(close_paren prec 4) + | BinaryOp("^",f,g) -> (open_paren prec 0)^ (racket_of 0 f) ^ "||" ^ (racket_of 0 g) ^ (close_paren prec 0) + | BinaryOp(op,_,_) | UnaryOp (op, _) -> failwith "Function sql_of_vterm is called with an unknown operator" ^ op + (* | BoolAnd (f,g) -> (open_paren prec 2) ^ (racket_of 2 f) ^ "*" ^ (racket_of 2 g) ^ (close_paren prec 2) + | BoolOr (f,g) -> (open_paren prec 0)^ (racket_of 0 f) ^ "+" ^ (racket_of 0 g) ^ (close_paren prec 0) + | BoolNot e -> (open_paren prec 4)^ "-" ^ (racket_of 5 e)^(close_paren prec 4) *) + in racket_of 0 expr + +(** Given a variable, returns the name of an EDB/IDB column that defines it, or if it is equal to a constant, the value of the constant. *) +let var_to_col (vt:vartab) (eqt:eqtab) key (variable:var) = + (*If the variable appears in a positive rterm, the value + * is the name of the respective rterm's table column*) + if Hashtbl.mem vt (string_of_var variable) + then List.hd (Hashtbl.find vt (string_of_var variable)) + (*If the variable does not appear in a positive rterm, but + * it does in an equality value, then the value is the eq's + * constant, the var has to be removed from the eqtab*) + else if Hashtbl.mem eqt (Var variable) + then racket_of_vterm vt eqt (eqt_extract eqt (Var variable)) + (*Else, the query is unsafe or inclomplete*) + else raise (SemErr ( + "Predicate "^(string_of_symtkey key)^ + " is unsafe, variable "^(string_of_var variable)^" is not in a positive "^ + "goal or strict equality relation." + ) + ) + +(** Given the head of the rule, the vartab, and te eqtab, returns the code that must be in the select clause. All columns are aliased as col0, col1, ... *) +let get_select_clause (vt:vartab) (eqt:eqtab) rterm = + let vlst = get_rterm_varlist rterm in + let key = symtkey_of_rterm rterm in + if vlst = [] then + (* select no colum, two choices: raise error or continue with select no column clause*) + (* raise (SemErr + ("Predicate "^(get_rterm_predname rterm)^ + " has arity 0, which is not allowed")) *) + "map (lambda (tuplelst) '())" + else + (*Transform variables to column names. Treat namedVars and + * aggregates differently*) + let var_value v = match v with + NamedVar _ | NumberedVar _ -> + var_to_col vt eqt key v + | AggVar (fn,vn) -> + (check_agg_function fn)^"("^(var_to_col vt eqt key (NamedVar vn))^")" + | _ -> invalid_arg ("not-expected vartype in head of predicate"^ + (string_of_symtkey key)) + in + let cols = List.map var_value vlst in + (*Create aliases*) + let rec alias = function + | [] -> "" + | [col] -> col + | col::col2::tl -> + col^" "^(alias (col2::tl)) + in + "map (lambda (tuplelst) (list "^(alias cols)^"))" + +let get_aggregation_racket (vt:vartab) (cnt:colnamtab) head agg_eqs agg_ineqs = + let vars = get_rterm_varlist head in + let key = symtkey_of_rterm head in + (*Merge the equalities and inequalities in a simple list*) + let eq_t = List.map extract_eq_tuple agg_eqs in + let aug_eq_t = List.map (fun (x,y) -> ("=",x,y)) eq_t in + let ieq_t = List.map extract_ineq_tuple agg_ineqs in + let comparisons = aug_eq_t@ieq_t in + (*Check if the rule has aggregation*) + let is_agg = List.exists is_aggvar vars in + if not is_agg then + if comparisons = [] then "" + else raise (SemErr ( + "Predicate "^(string_of_symtkey key)^ + " contains comparisons of aggregates but defines no "^ + "aggregations in its head")) + else + let cols = Hashtbl.find cnt key in + (*Calculate the GROUP BY clause*) + let group_var acc col = function + | NamedVar _ -> col::acc + | _ -> acc in + let grp_cols = List.fold_left2 group_var [] cols vars in + let group_by_racket = + if grp_cols = [] then "" + else ("GROUP BY "^(String.concat ", " grp_cols)) in + (*Calculate the HAVING clause*) + (*Extract the available aggregations in the head, and place them + * in a list, which values will be the function applied to a column-name*) + let av_aggs = Hashtbl.create 100 in + let fake_eqt:eqtab = Hashtbl.create 100 in + let insert_agg = function + | AggVar (fn,vn) -> + let col = var_to_col vt fake_eqt key (NamedVar vn) in + Hashtbl.add av_aggs (fn,vn) (fn^"("^col^")") + | _ -> () in + List.iter insert_agg vars; + (*Build the contraints and check for unavailable aggregates*) + let agg_var_col agv = + let tuple = extract_aggvar_tuple agv in + if Hashtbl.mem av_aggs tuple then Hashtbl.find av_aggs tuple + else raise (SemErr ( + "Predicate "^(string_of_symtkey key)^" contains comparisons of "^ + "aggregates that are not defined in its head" + )) in + let comp_const (op,e1,e2) = match (op,e1,e2) with + (* currently only support constraint for aggreation in the form agg_fun(X) comparason_op const*) + | (_, Var (AggVar (fn,vlst)), Const c) -> + (agg_var_col (AggVar (fn,vlst)))^" "^op^" "^(string_of_const c) + | _ -> raise (SemErr ( + "Predicate "^(string_of_symtkey key)^" contains comparisons of "^ + "aggregates that are not in the form of agg_fun(X) op const" + )) in + let comp_racket = List.map comp_const comparisons in + let having_racket = if comp_racket = [] then "" else + "HAVING "^(String.concat " AND " comp_racket) in + group_by_racket^" "^having_racket + +let rec non_rec_unfold_racket_of_symtkey (idb:symtable) (cnt:colnamtab) (goal:symtkey) = + (* get all the rule having this query in head *) + (* print_endline ("Reach " ^ (string_of_symtkey goal)); *) + if not (Hashtbl.mem idb goal) then raise (SemErr ("No rule for the idb predicate "^string_of_symtkey goal)) + else + let rule_lst = Hashtbl.find idb goal in + (* union all rules by appending the corresponding lists *) + let unfold_racket_of_rule_lst (idb:symtable) (cnt:colnamtab) rules = + let unfold_racket_of_rule (idb:symtable) (cnt:colnamtab) rule = + let head = rule_head rule in + let body = rule_body rule in + (*Split terms in the rule's body. Separate equalities + * and inequalities in variable and aggregates relations.*) + let (p_rt,n_rt,all_eqs,all_ineqs) = split_terms body in + let (agg_eqs,eqs) = List.partition is_agg_equality all_eqs in + let (agg_ineqs,ineqs) = List.partition is_agg_inequality all_ineqs in + (*Build vartab, and eqtab for select and where clauses, build vartabl by p_rt which is list of positive predicates*) + let vt = build_num_vartab cnt p_rt in + let eqtb = build_eqtab eqs in + let select_racket = get_select_clause vt eqtb head in + let unfold_get_from_clause (idb:symtable) rterms = + if rterms == [] then "'(1)" else + let idb_alias pname arity n = + (* generate racket query for idb predicate *) + let idb_racket = non_rec_unfold_racket_of_symtkey idb cnt (pname,arity) in + "("^idb_racket^")" + in + let edb_alias pname arity n = pname + in + let set_alias rterm (a_lst,n) = + let pname = get_rterm_predname rterm in + let arity = get_arity rterm in + let key = symtkey_of_rterm rterm in + let alias_f = if Hashtbl.mem idb key then idb_alias else edb_alias in + let alias = alias_f pname arity n in + (alias::a_lst,n-1) + in + let len = List.length rterms in + let (aliases,_) = List.fold_right set_alias rterms ([],len-1) in + "(cartesian-map list "^(String.concat " " aliases)^")" in + let from_racket = unfold_get_from_clause idb p_rt in + + let unfold_get_where_clause (idb:symtable) (vt:vartab) (cnt:colnamtab) (eqt:eqtab) ineq neg_rt = + (*Transform a list of column names in eq relations [a,b,c] -> ['a=b';'a=c']*) + let var_const _ cols acc = match cols with + | [] -> acc + | hd::tl -> + let eq_rels el = "(equal? "^ hd^" "^el^")" in + (List.map eq_rels tl)::acc + in + let fvt = List.flatten (Hashtbl.fold var_const vt []) in + (*Transform the equalities in the eqtab to strings of the form + * "CName = value" *) + let eq_comp e1 e2 acc = if (is_free_var vt e1) then acc else ( "(equal? "^ (racket_of_vterm vt eqt e1)^" "^(racket_of_vterm vt eqt e2) ^")")::acc in + let feqt = Hashtbl.fold eq_comp eqt [] in + (*Transform the inequalities in the list for strings of the form + * "CName op value" *) + let ineq_tuples = List.map extract_ineq_tuple ineq in + let ineq_comp (op,e1,e2) acc = + if (op="<>") then + ("(not (equal? "^ (racket_of_vterm vt eqt e1)^" "^(racket_of_vterm vt eqt e2)^"))")::acc + else + ("("^op^" "^ (racket_of_vterm vt eqt e1)^" "^(racket_of_vterm vt eqt e2)^")")::acc in + let fineq = List.fold_right ineq_comp ineq_tuples [] in + (*Transform the negated rterms into racket*) + let unfold_racket_of_negated_rterms (idb:symtable) (vt:vartab) (cnt:colnamtab) (eqt:eqtab) neg_rt = + let gen_neg_racket rt = + (*get basic info of the rterm*) + let key = symtkey_of_rterm rt in + let pname = get_rterm_predname rt in + let arity = get_arity rt in + let alias = pname^"_a"^(string_of_int arity) in + let vlst = get_rterm_varlist rt in + if not (Hashtbl.mem cnt key) then raise (SemErr ("not found edb or idb predicate "^string_of_symtkey key)) else + (*Get the from racket of the rterm*) + let from_racket = + if Hashtbl.mem idb key then + "("^ non_rec_unfold_racket_of_symtkey idb cnt (pname,arity) ^")" + else + pname + in + (* print_endline "___neg racket___"; print_string from_racket; print_endline "___neg racket___"; *) + (*Get the where racket of the rterm*) + let build_const acc col var = + let eq_to = "(equal? (list-ref negtuple "^col^") " in + match var with + | NamedVar vn -> + if Hashtbl.mem vt vn then + (eq_to^(List.hd (Hashtbl.find vt vn))^")")::acc + else if Hashtbl.mem eqt (Var var) then + (eq_to^(racket_of_vterm vt eqt (Hashtbl.find eqt (Var var)))^")")::acc + else raise (SemErr ( + "Program is unsafe, variable "^vn^ + " in negated call to predicate "^ + (string_of_symtkey key)^" does not appear in a positive "^ + "goal or strict equation. Try anonimous variables." + )) + | NumberedVar _ -> let vn = string_of_var var in + if Hashtbl.mem vt vn then + (eq_to^(List.hd (Hashtbl.find vt vn))^")")::acc + else if Hashtbl.mem eqt (Var var) then + (eq_to^(racket_of_vterm vt eqt (Hashtbl.find eqt (Var var)))^")")::acc + else raise (SemErr ( + "Program is unsafe, variable "^vn^ + " in negated call to predicate "^ + (string_of_symtkey key)^" does not appear in a positive "^ + "goal or strict equation. Try anonimous variables." + )) + | ConstVar c -> (eq_to^(string_of_const c)^")")::acc + | AnonVar -> acc + | _ -> invalid_arg "There is a non-expected type of var in a negated rterm" + in + let rec gen_nums ind n = + if ind "" + | _ -> "filter (lambda (negtuple) "^( + if (List.length const_lst = 1) then String.concat "" const_lst + else + List.fold_right (fun a b -> "(and " ^ a ^" "^b^")") const_lst "true" + )^")" in + (**Return the final string*) + "(= 0 (length "^ + (if (where_racket = "") then from_racket + else "("^where_racket^" "^from_racket^")") + ^"))" + in + List.map gen_neg_racket neg_rt in + let fnrt = unfold_racket_of_negated_rterms idb vt cnt eqt neg_rt in + (*merge all constraints*) + let constraints = fvt@feqt@fineq@fnrt in + match constraints with + | [] -> "" + | _ -> "filter (lambda (tuplelst) "^( + if (List.length constraints = 1) then String.concat "" constraints + else + List.fold_right (fun a b -> "(and " ^ a ^" "^b^")") constraints "true" + )^")" in + let where_racket = unfold_get_where_clause idb vt cnt eqtb ineqs n_rt in + let agg_racket = get_aggregation_racket vt cnt head agg_eqs agg_ineqs in + if (where_racket = "") then select_racket ^ " "^from_racket + else select_racket ^ " ("^where_racket^" "^from_racket^")" in + (* String.concat " " [select_racket;from_racket;where_racket;agg_racket] in *) + let racket_list = List.map (unfold_racket_of_rule idb cnt) rules in + if (List.length racket_list > 1) then + "append " ^ (String.concat " " (List.map (fun x -> "("^x^")") racket_list)) + else (String.concat "" racket_list) in + let racket = unfold_racket_of_rule_lst idb cnt rule_lst in + racket + +(** Take a query term and generate unfolded racket source code for it. *) +let non_rec_unfold_racket_of_query (idb:symtable) (cnt:colnamtab) (query:rterm) = + let qrule = rule_of_query query idb in + (* qrule is in the form of _dummy_(x,y) :- query_predicate(x,y), x=1 *) + let local_idb = Hashtbl.copy idb in + (* because insert a temporary dummy qrule, we should work with a local variable of idb *) + symt_insert local_idb qrule; + (* get column names (cols_by_var) for the view by using the dummy predicate which is head of qrule *) + let rec gen_nums ind n = + if ind "(list-ref tuplelst "^x^")") cols in + "map (lambda (tuplelst) (list "^(String.concat " " sel_lst)^")) " ^ + (* by inserting the dummy rule to idb, we now find racket for this dummy predicate *) + "("^non_rec_unfold_racket_of_symtkey local_idb cnt (symtkey_of_rterm (rule_head qrule))^")" + +(** Generate racket functions from the ast, the goal is the query predicate, the query is a query over source relations. *) +let unfold_query_racket_stt (debug:bool) (edb:symtable) prog = + let query_rt = get_query prog in + (*Extract and pre-process the IDB from the program*) + let idb = extract_idb prog in + preprocess_rules idb; + (* print_symtable idb; *) + (*Build the colnamtab for referencing the table's columns*) + let cnt = build_colnamtab edb idb in + (*Return the desired racket*) + let racket = non_rec_unfold_racket_of_query idb cnt query_rt in + racket + + +let unfold_program_query (debug:bool) prog = + if (debug) then print_endline ("==> generating racket function for a query of a datalog program"^ string_of_query (get_query prog)) else (); + let edb = extract_edb prog in + unfold_query_racket_stt debug edb prog + + +(** Take a view update datalog program (containing both get and put directions) and generate racket query of constraints involving view. *) +let view_constraint_racket_of_stt (dbschema:string) (debug:bool) (inc:bool) (optimize:bool) prog = + let clean_prog = keep_only_constraint_of_view debug prog in + if inc then + let inc_prog = incrementalize_by_view debug clean_prog in + let view_sch = get_view inc_prog in + let view_rt = get_schema_rterm view_sch in + let new_view_rt = rename_rterm "new_" view_rt in + let subst_prog = subst_pred (get_rterm_predname view_rt) (get_rterm_predname new_view_rt) inc_prog in + let prog2 = {subst_prog with sources = [ + get_rterm_predname (view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_deletion_rterm view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_insertion_rterm view_rt), get_schema_col_typs view_sch + ]@subst_prog.sources; rules = [ + (get_inc_original view_rt,[Rel (view_rt)]); + (get_inc_ins view_rt,[Rel (get_temp_delta_insertion_rterm view_rt)]); + (get_inc_del view_rt,[Rel (get_temp_delta_deletion_rterm view_rt)]) + ]@subst_prog.rules} in + (* let edb = extract_edb prog2 in *) + let idb = extract_idb prog2 in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + ( + (* keep_only_constraint_of_view debug view_rt edb idb ; *) + preprocess_rules idb; + (* let cnt = build_colnamtab edb idb in *) + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + let remain_rules = rules_of_symt idb in + let prog3 = {get_empty_expr with view = prog2.view; sources = prog2.sources; rules = remain_rules} in + (* non_rec_unfold_racket_of_query dbschema idb cnt get_empty_pred *) + let prog4 = if (optimize) then (Ast2fol.optimize_query_datalog debug {prog3 with query = Some get_empty_pred} ) else {prog3 with query = Some get_empty_pred} in + (* the optimization may drop the empty_predicate of prog4 when the empty_predicate is trival (always empty) *) + if (has_query prog4) then + (unfold_program_query debug prog4) + else "SELECT WHERE false" + else "SELECT WHERE false") + else "SELECT WHERE false" + else + let view_sch = get_view clean_prog in + let view_rt = get_schema_rterm view_sch in + let new_view_rt = rename_rterm "new_" view_rt in + let subst_prog = subst_pred (get_rterm_predname view_rt) (get_rterm_predname new_view_rt) (delete_rule_of_predname (get_rterm_predname view_rt) clean_prog) in + let prog2 = {subst_prog with sources = [ + get_rterm_predname (view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_deletion_rterm view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_insertion_rterm view_rt), get_schema_col_typs view_sch + ]@subst_prog.sources; rules = [ + (new_view_rt,[Rel (view_rt); Not (get_temp_delta_deletion_rterm view_rt)]); + (new_view_rt,[Rel (get_temp_delta_insertion_rterm view_rt)]) + ]@subst_prog.rules} in + (* let edb = extract_edb prog2 in *) + let idb = extract_idb prog2 in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + ( + (* keep_only_constraint_of_view debug view_rt edb idb ; *) + preprocess_rules idb; + (* let cnt = build_colnamtab edb idb in *) + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + let remain_rules = Hashtbl.fold (fun k rules lst -> rules@lst) idb [] in + let prog3 = {get_empty_expr with view = prog2.view; sources = prog2.sources; rules = remain_rules} in + (* non_rec_unfold_racket_of_query dbschema idb cnt get_empty_pred *) + let prog4 = if (optimize) then (Ast2fol.optimize_query_datalog debug {prog3 with query = Some get_empty_pred} ) else {prog3 with query = Some get_empty_pred} in + (* the optimization may drop the empty_predicate of prog4 when the empty_predicate is trival (always empty) *) + if (has_query prog4) then + (unfold_program_query debug prog4) + else "SELECT WHERE false" + else "SELECT WHERE false") + else "SELECT WHERE false" + + +(** Take a view update datalog program (containing both get and put directions) and generate a racket query of constraints not involving view. *) +let non_view_constraint_racket_of_stt (dbschema:string) (debug:bool) (inc:bool) (optimize:bool) prog = + let clean_prog = remove_constraint_of_view debug prog in + if inc then + let inc_prog = incrementalize_by_view debug clean_prog in + let view_sch = get_view inc_prog in + let view_rt = get_schema_rterm view_sch in + let new_view_rt = rename_rterm "new_" view_rt in + let subst_prog = subst_pred (get_rterm_predname view_rt) (get_rterm_predname new_view_rt) inc_prog in + let prog2 = {subst_prog with sources = [ + get_rterm_predname (view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_deletion_rterm view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_insertion_rterm view_rt), get_schema_col_typs view_sch + ]@subst_prog.sources; rules = [ + (get_inc_original view_rt,[Rel (view_rt)]); + (get_inc_ins view_rt,[Rel (get_temp_delta_insertion_rterm view_rt)]); + (get_inc_del view_rt,[Rel (get_temp_delta_deletion_rterm view_rt)]) + ]@subst_prog.rules} in + (* let edb = extract_edb prog2 in *) + let idb = extract_idb prog2 in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + ( + (* keep_only_constraint_of_view debug view_rt edb idb ; *) + preprocess_rules idb; + (* let cnt = build_colnamtab edb idb in *) + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + let remain_rules = rules_of_symt idb in + let prog3 = {get_empty_expr with view = prog2.view; sources = prog2.sources; rules = remain_rules} in + (* non_rec_unfold_racket_of_query dbschema idb cnt get_empty_pred *) + let prog4 = if (optimize) then (Ast2fol.optimize_query_datalog debug {prog3 with query = Some get_empty_pred} ) else {prog3 with query = Some get_empty_pred} in + (* the optimization may drop the empty_predicate of prog4 when the empty_predicate is trival (always empty) *) + if (has_query prog4) then + (unfold_program_query debug prog4) + else "SELECT WHERE false" + else "SELECT WHERE false") + else "SELECT WHERE false" + else + let view_sch = get_view clean_prog in + let view_rt = get_schema_rterm view_sch in + let new_view_rt = rename_rterm "new_" view_rt in + let subst_prog = subst_pred (get_rterm_predname view_rt) (get_rterm_predname new_view_rt) (delete_rule_of_predname (get_rterm_predname view_rt) clean_prog) in + let prog2 = {subst_prog with sources = [ + get_rterm_predname (view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_deletion_rterm view_rt), get_schema_col_typs view_sch; + get_rterm_predname (get_temp_delta_insertion_rterm view_rt), get_schema_col_typs view_sch + ]@subst_prog.sources; rules = [ + (new_view_rt,[Rel (view_rt); Not (get_temp_delta_deletion_rterm view_rt)]); + (new_view_rt,[Rel (get_temp_delta_insertion_rterm view_rt)]) + ]@subst_prog.rules} in + (* let edb = extract_edb prog2 in *) + let idb = extract_idb prog2 in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + ( + (* keep_only_constraint_of_view debug view_rt edb idb ; *) + preprocess_rules idb; + (* let cnt = build_colnamtab edb idb in *) + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + let remain_rules = Hashtbl.fold (fun k rules lst -> rules@lst) idb [] in + let prog3 = {get_empty_expr with view = prog2.view; sources = prog2.sources; rules = remain_rules} in + (* non_rec_unfold_racket_of_query dbschema idb cnt get_empty_pred *) + let prog4 = if (optimize) then (Ast2fol.optimize_query_datalog debug {prog3 with query = Some get_empty_pred} ) else {prog3 with query = Some get_empty_pred} in + (* the optimization may drop the empty_predicate of prog4 when the empty_predicate is trival (always empty) *) + if (has_query prog4) then + (unfold_program_query debug prog4) + else "SELECT WHERE false" + else "SELECT WHERE false") + else "SELECT WHERE false" + + +let stype_to_racket_type st = match st with + | Sint -> "integer?" + | Sreal -> "real?" + | Sbool -> "boolean?" + | Sstring -> "integer?" + +(* transform source relations in program into symbolic tables in rosette *) +let gen_symbolic_source size vocsize prog = + (* currently just set all the types are int (ℤ) *) + let p_el sym_table_lst (name, lst) = + let tup num = + (( String.concat "\n" ( List.map (fun (col,typ) -> "(define-symbolic "^name^"$"^col^"$"^ string_of_int num ^" " ^ stype_to_racket_type typ^")" ^(if (typ = Sstring) then "\n (assert (and (< -1 "^name^"$"^col^"$"^ string_of_int num ^") (< " ^name^"$"^col^"$"^ string_of_int num ^ " "^ string_of_int vocsize^")))" else "") ) lst) ) + ^ "\n\n(define "^name^"_tuple_"^ string_of_int num ^ " (list "^ String.concat " " ( List.map (fun (col,typ) -> name^"$"^col^"$"^ string_of_int num) lst)^")" ^")") in + let rec sym_tuples sz = if sz <= 0 then "" else sym_tuples (sz-1) ^ "\n\n" ^ (tup sz) in + let rec sym_table sz = if sz <= 0 then "" else sym_table (sz-1) ^ " " ^name^"_tuple_" ^string_of_int sz in + ((sym_tuples size) ^ "\n\n(define "^name^ " (list " ^ sym_table size ^ "))") ::sym_table_lst in + List.fold_left p_el [] prog.sources + +(* transform source relations in program into symbolic tables in rosette *) +let gen_symbolic_source_view size vocsize prog = + (* currently just set all the types are int (ℤ) *) + let p_el sym_table_lst (name, lst) = + let tup num = + (( String.concat "\n" ( List.map (fun (col,typ) -> "(define-symbolic "^name^"$"^col^"$"^ string_of_int num ^" " ^ stype_to_racket_type typ^")" ^(if (typ = Sstring) then "\n (assert (and (< -1 "^name^"$"^col^"$"^ string_of_int num ^") (< " ^name^"$"^col^"$"^ string_of_int num ^ " "^ string_of_int vocsize^")))" else "") ) lst) ) + ^ "\n\n(define "^name^"_tuple_"^ string_of_int num ^ " (list "^ String.concat " " ( List.map (fun (col,typ) -> name^"$"^col^"$"^ string_of_int num) lst)^")" ^")") in + let rec sym_tuples sz = if sz <= 0 then "" else sym_tuples (sz-1) ^ "\n\n" ^ (tup sz) in + let rec sym_table sz = if sz <= 0 then "" else sym_table (sz-1) ^ " " ^name^"_tuple_" ^string_of_int sz in + ((sym_tuples size) ^ "\n\n(define "^name^ " (list " ^ sym_table size ^ "))") ::sym_table_lst in + List.fold_left p_el [] (get_schema_stts prog) + +(* take a view update datalog program (containing both get and put directions) and generate a rosette constraint of getput property for its view update strategy *) +let ros_getput_of_stt (debug:bool) prog = + + let delta_rt_lst = get_delta_rterms prog in + (* remove overlap of delta and the source *) + let dummy_delta_rules = List.map (fun delta -> let dummy = rename_rterm "__dummy__" delta in + match delta with + Deltadelete (p,vars) -> (dummy, [Rel (Deltadelete (p,vars)); Rel(Pred(p,vars))]) + | Deltainsert (p,vars) -> (dummy, [Rel (Deltainsert (p,vars)); Not(Pred(p,vars))]) + | _ -> invalid_arg "Function ros_getput_of_stt called with not a delta predicate") delta_rt_lst in + let dummy_delta_rt_lst = List.map (rename_rterm "__dummy__") delta_rt_lst in + (* get the emptiness FO sentence of a relation *) + let getput_prog = Expr.add_rules dummy_delta_rules prog in + let edb = extract_edb getput_prog in + let idb = extract_idb getput_prog in + preprocess_rules idb; + if debug then ( + print_endline "_____preprocessed datalog rules_______"; + print_symtable idb; + print_endline "______________\n"; + ) else (); + let cnt = build_colnamtab edb idb in + let delta_definition rel = + let delta_ros_code = non_rec_unfold_racket_of_query idb cnt rel in + "(define "^ get_rterm_predname rel ^ " (" ^delta_ros_code^ "))" in + let delta_definition_lst = List.map delta_definition dummy_delta_rt_lst in + let emptiness = "(define emptiness (append "^String.concat " " (List.map get_rterm_predname dummy_delta_rt_lst) ^"))" in + let ros_constraint = "(solve (assert (< 0 (length emptiness))))" in + (String.concat "\n\n" delta_definition_lst) ^ "\n\n"^ emptiness ^ "\n\n" ^ ros_constraint + + +(* take a view update datalog program (containing both get and put directions) and generate a rosette constraint of delta disjointness property for its view update strategy *) +let ros_disdelta_of_stt (debug:bool) prog = + let edb = extract_edb prog in + (* need to change the view (in query predicate) to a edb relation *) + let view_rt = get_schema_rterm (get_view prog) in + (* need to convert the view to be an edb relation *) + symt_insert edb (view_rt,[]); + let idb = extract_idb prog in + symt_remove idb (symtkey_of_rterm view_rt); + let emptiness = Pred ("__emptiness",[]) in + let delta_rt_lst = get_delta_rterms prog in + (* get each pair of delta relations from the delta relation lst delta_rt_lst *) + let delta_pair_lst = + let pair_of_delta_insert lst ins_rel = + let del_rels = List.filter (is_delta_pair ins_rel) delta_rt_lst in + if (List.length del_rels = 0) then lst else (ins_rel, (List.hd del_rels))::lst in + List.fold_left pair_of_delta_insert [] delta_rt_lst in + List.iter (fun (r1,r2) -> symt_insert idb (emptiness,[ Rel r1; Rel r2])) delta_pair_lst; + preprocess_rules idb; + if debug then ( + print_endline "_____preprocessed datalog rules_______"; + print_symtable idb; + print_endline "______________\n"; + ) else (); + let cnt = build_colnamtab edb idb in + let disdelta_ros = non_rec_unfold_racket_of_query idb cnt emptiness in + let disdelta_emptiness = "(define disdelta_emptiness ("^disdelta_ros^"))" in + let ros_constraint = "(solve (assert (< 0 (length disdelta_emptiness))))" in + disdelta_emptiness ^ "\n\n" ^ ros_constraint + + +(* take a view update datalog program (containing both get and put directions) and generate a rosette constraint of putget property for its view update strategy *) +let ros_putget_of_stt (debug:bool) prog = + let putget_prog = datalog_of_putget debug false prog in + let edb = extract_edb putget_prog in + (* need to change the view (in query predicate) to a edb relation *) + let view_rt = get_schema_rterm (get_view putget_prog) in + (* need to convert the view to be an edb relation *) + symt_insert edb (view_rt,[]); + let idb = extract_idb putget_prog in + (* symt_remove idb (symtkey_of_rterm view_rt); *) + let new_view_rt = rename_rterm "__dummy_new_" view_rt in + let emptiness = rename_rterm "__emptiness" view_rt in + symt_insert idb (emptiness,[ Rel new_view_rt; Not view_rt]); + symt_insert idb (emptiness,[ Rel view_rt; Not new_view_rt]); + preprocess_rules idb; + if debug then ( + print_endline "_____preprocessed datalog rules_______"; + print_symtable idb; + print_endline "______________\n"; + ) else (); + let cnt = build_colnamtab edb idb in + let putget_ros = non_rec_unfold_racket_of_query idb cnt emptiness in + let putget_emptiness = "(define putget_emptiness ("^putget_ros^"))" in + let ros_constraint = "(solve (assert (< 0 (length putget_emptiness))))" in + putget_emptiness ^ "\n\n" ^ ros_constraint + + +(* take a view update datalog program (may contain both get and put directions) and generate FO sentence of all contraints *) +let ros_constraint_sentence_of_stt (debug:bool) prog = + if debug then (print_endline "==> generating racket code for all constraints";) else (); + let edb = extract_edb prog in + let idb = extract_idb prog in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + (* need to change the view (in query predicate) to a edb relation *) + let view_rt = get_schema_rterm (get_view prog) in + (* need to convert the view to be an edb relation *) + symt_insert edb (view_rt,[]); + (* if having get (view rules) then remove it *) + if Hashtbl.mem idb (symtkey_of_rterm view_rt) then + symt_remove idb (symtkey_of_rterm view_rt); + preprocess_rules idb; + if debug then ( + print_endline "_____preprocessed datalog rules_______"; + print_symtable idb; + print_endline "______________\n"; + ) else (); + let cnt = build_colnamtab edb idb in + let constr_ros = non_rec_unfold_racket_of_query idb cnt get_empty_pred in + let constr_emptiness = "(define constr_emptiness ("^constr_ros^"))" in + let ros_constraint = "(assert (= 0 (length constr_emptiness)))" in + constr_emptiness ^ "\n\n" ^ ros_constraint + else "" + + +(* take a view update datalog program (may contain both get and put directions) and generate FO sentence of contraints not involving view *) +let ros_non_view_constraint_sentence_of_stt (debug:bool) prog = + if debug then (print_endline "==> generating constraint not involving view";) else (); + let clean_prog = remove_constraint_of_view debug prog in + let edb = extract_edb clean_prog in + let idb = extract_idb clean_prog in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + (* need to change the view (in query predicate) to a edb relation *) + let view_rt = get_schema_rterm (get_view clean_prog) in + (* need to convert the view to be an edb relation *) + (* remove_constraint_of_view debug view_rt edb idb ; *) + symt_insert edb (view_rt,[]); + symt_remove idb (symtkey_of_rterm view_rt); + preprocess_rules idb; + if debug then ( + print_endline "_____preprocessed datalog rules_______"; + print_symtable idb; + print_endline "______________\n"; + ) else (); + let cnt = build_colnamtab edb idb in + let constr_ros = non_rec_unfold_racket_of_query idb cnt get_empty_pred in + let constr_emptiness = "(define constr_emptiness ("^constr_ros^"))" in + let ros_constraint = "(assert (= 0 (length constr_emptiness)))" in + constr_emptiness ^ "\n\n" ^ ros_constraint + else "" + + +(* take a view update datalog program (may contain both get and put directions) and generate FO sentence of only contraints involving view *) +let ros_view_constraint_sentence_of_stt (debug:bool) prog = + if debug then (print_endline "==> generating a sentence of only constraints involving view";) else (); + let clean_prog = keep_only_constraint_of_view debug prog in + let edb = extract_edb clean_prog in + let idb = extract_idb clean_prog in + if Hashtbl.mem idb (symtkey_of_rterm get_empty_pred) then + (* need to change the view (in query predicate) to a edb relation *) + let view_rt = get_schema_rterm (get_view clean_prog) in + (* need to convert the view to be an edb relation *) + (* remove_constraint_of_view debug view_rt edb idb ; *) + symt_insert edb (view_rt,[]); + symt_remove idb (symtkey_of_rterm view_rt); + preprocess_rules idb; + if debug then ( + print_endline "_____preprocessed datalog rules_______"; + print_symtable idb; + print_endline "______________\n"; + ) else (); + let cnt = build_colnamtab edb idb in + let constr_ros = non_rec_unfold_racket_of_query idb cnt get_empty_pred in + let constr_emptiness = "(define constr_emptiness ("^constr_ros^"))" in + let ros_constraint = "(assert (= 0 (length constr_emptiness)))" in + constr_emptiness ^ "\n\n" ^ ros_constraint + else "" + + +let predefined_ros = +"#lang rosette/safe + +(define curry + (lambda (f . c) (lambda x (apply f (append c x))))) + +(define stitch + (lambda (tuples element) + (map (curry cons element) tuples))) + +(define flatten + (curry apply append)) + +(define cartesian + (lambda (l1 l2) + (flatten (map (curry stitch l2) l1)))) + +(define cartesian-lists + (lambda (lists) + (foldr cartesian '(()) lists))) + +(define cartesian-map + (lambda (f . lists) + (map (curry apply f) (cartesian-lists lists)))) + +" + +let ros_check_disdelta_of_stt (debug:bool) srcsize vocsize prog = + predefined_ros^ (String.concat "\n" (gen_symbolic_source_view srcsize vocsize prog)) ^ "\n\n"^ ros_constraint_sentence_of_stt debug prog ^ "\n\n"^ ros_disdelta_of_stt debug prog + + +let ros_check_getput_of_stt (debug:bool) srcsize vocsize prog = + predefined_ros^ (String.concat "\n" (gen_symbolic_source srcsize vocsize prog)) ^ "\n\n"^ ros_non_view_constraint_sentence_of_stt debug prog ^ "\n\n"^ ros_getput_of_stt debug prog + + +let ros_check_putget_of_stt (debug:bool) srcsize vocsize prog = + predefined_ros^ (String.concat "\n" (gen_symbolic_source_view srcsize vocsize prog)) ^ "\n\n"^ ros_constraint_sentence_of_stt debug prog ^ "\n\n"^ ros_putget_of_stt debug prog + + +type cellkey = (string*string*int) (* table name, column name, rowid *) +type celltable = (cellkey, string) Hashtbl.t (* value of cells*) + +let parse_ros_models log str = + if log then print_endline ">>> parsing model from rosette"; + let stream = (Scanf.Scanning.from_string (String.sub str 6 ((String.length str) - 6))) in + let rec do_parse acc = + match (Scanf.bscanf stream " [%s@$%s@$%d %s@] " (fun rel col id value -> (rel,col,id,value) :: acc)) + with + | xs -> do_parse xs + | exception Scanf.Scan_failure _ -> acc + | exception End_of_file -> acc in + let raw_data = List.rev (do_parse []) in + let data:celltable = Hashtbl.create (List.length raw_data) in + List.iter (fun (rel,col,id,value) -> if log then print_endline ("("^rel^", "^col^", "^string_of_int id^") = "^ value); Hashtbl.add data (rel,col,id) value) raw_data; + data + +let get_default_val_of_type t = match t with + (* | Sint -> "ℤ" *) + | Sint -> "0" + (* | Sreal -> "ℝ" *) + (* | Sreal -> "real" *) + | Sreal -> "0.0" + | Sbool -> "true" + | Sstring -> "'none'" + + +let const_of_string str = + try (Int (int_of_string str)) with + (* try test () with *) + | Failure e -> + try (Real (float_of_string str)) with + (* try test () with *) + | Failure e -> + try (Bool (bool_of_string str)) with + (* try test () with *) + | Failure e | Invalid_argument e -> match str with + "null" -> Null + | "#t" -> (Bool true) + | "#f" -> (Bool false) + | _ -> String str + + +let instantiate_relation size string_adom (data:celltable) rel_chema = + let col_types = get_schema_col_typs rel_chema in + let rel_name = get_schema_name rel_chema in + let rec tuple_lst id = if (id<=0) then [] + else try + ( (Pred (rel_name, List.map (fun (col,typ) -> ConstVar (const_of_string ( + if Hashtbl.mem data (rel_name, col, id) then + let value = Hashtbl.find data (rel_name, col, id) in + if typ = Sstring then ( + let int_to_string i = List.nth string_adom i in + try (int_to_string (int_of_string value)) with + (* try test () with *) + | Failure e -> invalid_arg "Function instantiate_relation called with invalid data, tuple "^string_of_int id ^" of relation " ^ rel_name^" not valid" + ) + else value + else (get_default_val_of_type typ) (* given a default value for it *) + ))) col_types)) )::(tuple_lst (id-1)) + with Not_found -> + invalid_arg ("Function instantiate_relation called with invalid data, tuple "^string_of_int id ^" of relation " ^ rel_name^" not found") in + (* from bag to set *) + Lib.setify (List.rev (tuple_lst size)) diff --git a/src/counterexample.ml b/src/counterexample.ml new file mode 100644 index 0000000..a7c8039 --- /dev/null +++ b/src/counterexample.ml @@ -0,0 +1,102 @@ +(*******************************************************) +(** Functions for debugging a bidirectional Datalog program +*) +(********************************************************) +(* +@author: Vandang Tran +*) + +open Logic +open Expr +open Utils + +type property = Getput | Putget | Disdelta + +let string_of_property (property: property) = match property with + | Getput -> "getput" + | Putget -> "putget" + | Disdelta -> "disdelta" + +let init_vocabulary = [ + "'..aa..'"; + "'..bb..'"; + "'..cc..'"; + "'..dd..'"; + "'..ee..'"; + "'..ff..'"; + "'..gg..'"; + "'..hh..'"; + "'..ii..'"; + "'..jj..'"; + "'..kk..'"; + "'..ll..'"; + "'..mm..'"; + "'..nn..'"; + "'..oo..'"; + "'..pp..'"; + "'..qq..'"; + "'..rr..'"; + "'..ss..'"; + "'..tt..'"; + "'..uu..'"; + "'..vv..'"; + "'..ww..'"; + "'..xx..'"; + "'..yy..'"; + "'..zz..'" +] + +(** interatively generate a counterexample for a given property *) +let gen_counterexample (log:bool) (property:property) (maxsize:int) (timeout:int) (iprog: expr) = + let error_mess = ref "" in + (* let all_rules, non_rules = Rule_preprocess.seperate_rules iprog in *) + let string_adom = init_vocabulary@(Rule_preprocess.extract_rules_string_adom iprog.rules) in + let string_adom = Lib.sort (fun a b -> a < b) string_adom in + let adom_tbl = Hashtbl.create (List.length string_adom) in + List.iteri (fun i x -> Hashtbl.add adom_tbl x i) string_adom; + let string_to_int str = + if Hashtbl.mem adom_tbl str then + Hashtbl.find adom_tbl str + else invalid_arg "function string_to_int called with an unkown string" in + let prog = {iprog with rules = Rule_preprocess.string2int_rules string_to_int iprog.rules} in + if log then ( + print_endline "______string-mapped program______"; + print_endline @@"String active domain in the program is: " ^ (String.concat ", " string_adom); + print_endline (string_of_prog prog); + print_endline "__________________________________" + ); + let vocsize = List.length string_adom in + let rec gen_ctex i maxsize = + let exitcode, mes = check_ros_prog log timeout ( + match property with + | Getput -> if log then print_endline "==> generating a counterexample for getput"; Ast2ros.ros_check_getput_of_stt log i vocsize prog + | Putget -> if log then print_endline "==> generating a counterexample for putget"; Ast2ros.ros_check_putget_of_stt log i vocsize prog + | Disdelta -> if log then print_endline "==> generating a counterexample for delta disjointness"; Ast2ros.ros_check_disdelta_of_stt log i vocsize prog + ) in + if not (exitcode=0) then + if (exitcode = 124) then (error_mess := "Stop generating a counterexample of "^ string_of_property property ^": Timeout"; i,"") + else + (error_mess := "Stop generating a counterexample of "^ string_of_property property ^": \nExit code: " ^ string_of_int exitcode + ^ (if (log) then "\nError messange: "^ mes else ""); i,"") + else + if (!error_mess = "" && mes = "(unsat)" && i < maxsize) then + gen_ctex (i+1) maxsize + else + i,mes in + let size, message = gen_ctex 1 maxsize in + if (!error_mess = "") then + (if log then (print_endline "________Model from rosette______"; print_endline message; print_endline "_____________________"); + if (message = "(unsat)") then error_mess := "there is no counter example of the specified size for "^ string_of_property property; + let model_data = Ast2ros.parse_ros_models log message in + let relation_lst = (match property with + | Getput -> get_source_stts prog + | Putget -> get_schema_stts prog + | Disdelta -> get_schema_stts prog + ) in + let table_lst = List.map (Ast2ros.instantiate_relation size string_adom model_data) relation_lst in + let facts = List.concat table_lst in + if log then (print_endline ("\n________"^ string_of_property property^" counterexample________ ") ; + print_endline (string_of_prog {get_empty_expr with facts = facts} ); + print_endline "________________"); + !error_mess, facts) + else !error_mess, [] diff --git a/src/counterexample.mli b/src/counterexample.mli new file mode 100644 index 0000000..2b338b9 --- /dev/null +++ b/src/counterexample.mli @@ -0,0 +1,7 @@ + +open Expr + +type property = Getput | Putget | Disdelta + +(** interatively generate a counterexample for a given property *) +val gen_counterexample: bool -> property -> int -> int -> expr -> string * rterm list