diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/drl/executor.ml | 11 | ||||
| -rw-r--r-- | lib/drl/gate.ml | 82 | ||||
| -rw-r--r-- | lib/drl/parser.ml | 5 | ||||
| -rw-r--r-- | lib/drl/sublanguage.ml | 26 | ||||
| -rw-r--r-- | lib/drl_verified/drl_verified.ml | 76 | ||||
| -rw-r--r-- | lib/drl_verified/drl_verified.mli | 29 |
6 files changed, 228 insertions, 1 deletions
diff --git a/lib/drl/executor.ml b/lib/drl/executor.ml index 27f52c2..322fada 100644 --- a/lib/drl/executor.ml +++ b/lib/drl/executor.ml @@ -3,8 +3,17 @@ module Make(Storage : Management.Physical.S) = struct module Ops = Manipulation.Make(Storage) type error = + | ParseError of string | RelationNotFound of string - | AlgebraError of Algebra.error + | AlgebraError of Algebra.error + + let sexp_of_error e = + let open Sexplib.Sexp in + match e with + | ParseError s -> List [Atom "parse-error"; Atom s] + | RelationNotFound s -> List [Atom "relation-not-found"; Atom s] + | AlgebraError (Algebra.StorageError s) -> List [Atom "storage-error"; Atom s] + | AlgebraError (Algebra.GeneratorError s) -> List [Atom "generator-error"; Atom s] let wrap = Result.map_error (fun e -> AlgebraError e) diff --git a/lib/drl/gate.ml b/lib/drl/gate.ml new file mode 100644 index 0000000..222e935 --- /dev/null +++ b/lib/drl/gate.ml @@ -0,0 +1,82 @@ +(** Finiteness gate for DRL queries. + + Converts Sakura types to Coq-extracted types and calls the + verified [predicted_finite] function. Rejects queries whose + result cannot be statically proven finite. *) + +(* -- string -> char list impedance --------------------------------- *) + +let string_to_chars (s : string) : char list = + List.init (String.length s) (String.get s) + +(* -- Sakura AST -> extracted AST ----------------------------------- *) + +let rec query_of_ast : Ast.query -> Drl_verified.query = function + | Ast.Base name -> + Drl_verified.Base (string_to_chars name) + | Ast.Const pairs -> + Drl_verified.Const + (List.map + (fun (k, v) -> + (string_to_chars k, value_of_ast_value v)) + pairs) + | Ast.Select (filter, source) -> + Drl_verified.Select (query_of_ast filter, query_of_ast source) + | Ast.Join (attrs, q1, q2) -> + Drl_verified.Join + (List.map string_to_chars attrs, query_of_ast q1, query_of_ast q2) + | Ast.Cartesian (q1, q2) -> + Drl_verified.Cartesian (query_of_ast q1, query_of_ast q2) + | Ast.Project (attrs, q) -> + Drl_verified.Project (List.map string_to_chars attrs, query_of_ast q) + | Ast.Rename (renames, q) -> + Drl_verified.Rename + (List.map + (fun (o, n) -> (string_to_chars o, string_to_chars n)) + renames, + query_of_ast q) + | Ast.Union (q1, q2) -> + Drl_verified.Union (query_of_ast q1, query_of_ast q2) + | Ast.Diff (q1, q2) -> + Drl_verified.Diff (query_of_ast q1, query_of_ast q2) + | Ast.Take (n, q) -> + Drl_verified.Take (n, query_of_ast q) + +and value_of_ast_value : Ast.value -> Drl_verified.literal = function + | Ast.Int n -> Drl_verified.LitInt n + (* The Coq model has no float literal. This truncation is harmless: + the finiteness gate inspects only relation names and query structure, + never literal values. *) + | Ast.Float f -> Drl_verified.LitInt (int_of_float f) + | Ast.Str s -> Drl_verified.LitStr (string_to_chars s) + | Ast.Bool b -> Drl_verified.LitBool b + +(* -- database snapshot --------------------------------------------- *) + +let is_finite (c : Conventions.Cardinality.t) : bool = + match c with + | Conventions.Cardinality.Finite _ | Conventions.Cardinality.ConstrainedFinite -> true + | Conventions.Cardinality.AlephZero | Conventions.Cardinality.Continuum -> false + +let database_snapshot (db : Management.Database.t) : Drl_verified.database = + Management.Database.RelationMap.fold + (fun name (rel : Relation.t) acc -> + let entry : Drl_verified.relation = + { rel_name = string_to_chars name; + rel_finite = is_finite rel.cardinality } + in + (string_to_chars name, entry) :: acc) + db.relations + [] + +(* -- public interface ---------------------------------------------- *) + +let admit (db : Management.Database.t) (ast : Ast.query) : (unit, string) result = + let vdb = database_snapshot db in + let vq = query_of_ast ast in + match Drl_verified.predicted_finite vdb vq with + | Some true -> Ok () + | Some false -> + Error "query produces potentially infinite result; use Take to bound it" + | None -> + Error "referenced relation not found in finiteness check" diff --git a/lib/drl/parser.ml b/lib/drl/parser.ml index 71d694b..36ce15a 100644 --- a/lib/drl/parser.ml +++ b/lib/drl/parser.ml @@ -1,5 +1,10 @@ type error = ParseError of string +let of_sexp sexp = + match Ast.query_of_sexp sexp with + | q -> Ok q + | exception exn -> Error (ParseError (Printexc.to_string exn)) + let of_string s = match Sexplib.Sexp.of_string s |> Ast.query_of_sexp with | q -> Ok q diff --git a/lib/drl/sublanguage.ml b/lib/drl/sublanguage.ml new file mode 100644 index 0000000..f57af95 --- /dev/null +++ b/lib/drl/sublanguage.ml @@ -0,0 +1,26 @@ +module Make (Storage : Management.Physical.S) = struct + module Exec = Executor.Make(Storage) + + type storage = Storage.t + type ast = Ast.query + type error = Exec.error + + let name = "drl" + + let parse_sexp sexp = + match Parser.of_sexp sexp with + | Ok r -> Ok r + | Error (Parser.ParseError s) -> Error (Exec.ParseError s) + + let execute storage db ast = + match Gate.admit db ast with + | Error msg -> Error (Exec.ParseError msg) + | Ok () -> + match Exec.execute storage db ast with + | Ok rel -> Ok (Sublanguage.Query rel) + | Error e -> Error e + + let sexp_of_error = Exec.sexp_of_error +end + +module Memory = Make(Management.Physical.Memory) diff --git a/lib/drl_verified/drl_verified.ml b/lib/drl_verified/drl_verified.ml new file mode 100644 index 0000000..b5aeaa7 --- /dev/null +++ b/lib/drl_verified/drl_verified.ml @@ -0,0 +1,76 @@ + +(** val eqb : char list -> char list -> bool **) + +let rec eqb s1 s2 = + match s1 with + | [] -> (match s2 with + | [] -> true + | _::_ -> false) + | c1::s1' -> + (match s2 with + | [] -> false + | c2::s2' -> if (=) c1 c2 then eqb s1' s2' else false) + +type attr_name = char list + +type relation = { rel_name : char list; rel_finite : bool } + +type database = (char list * relation) list + +(** val db_lookup : char list -> database -> relation option **) + +let rec db_lookup name = function +| [] -> None +| p :: rest -> + let (n, r) = p in if eqb name n then Some r else db_lookup name rest + +type literal = +| LitInt of int +| LitStr of char list +| LitBool of bool + +type query = +| Base of char list +| Const of (attr_name * literal) list +| Select of query * query +| Join of attr_name list * query * query +| Cartesian of query * query +| Project of attr_name list * query +| Rename of (attr_name * attr_name) list * query +| Union of query * query +| Diff of query * query +| Take of int * query + +(** val predicted_finite : database -> query -> bool option **) + +let rec predicted_finite db = function +| Base name -> + (match db_lookup name db with + | Some r -> Some r.rel_finite + | None -> None) +| Select (_, source) -> predicted_finite db source +| Join (_, q1, q2) -> + (match predicted_finite db q1 with + | Some f1 -> + (match predicted_finite db q2 with + | Some f2 -> Some ((&&) f1 f2) + | None -> None) + | None -> None) +| Cartesian (q1, q2) -> + (match predicted_finite db q1 with + | Some f1 -> + (match predicted_finite db q2 with + | Some f2 -> Some ((&&) f1 f2) + | None -> None) + | None -> None) +| Project (_, q0) -> predicted_finite db q0 +| Rename (_, q0) -> predicted_finite db q0 +| Union (q1, q2) -> + (match predicted_finite db q1 with + | Some f1 -> + (match predicted_finite db q2 with + | Some f2 -> Some ((&&) f1 f2) + | None -> None) + | None -> None) +| Diff (q1, _) -> predicted_finite db q1 +| _ -> Some true diff --git a/lib/drl_verified/drl_verified.mli b/lib/drl_verified/drl_verified.mli new file mode 100644 index 0000000..31acc7a --- /dev/null +++ b/lib/drl_verified/drl_verified.mli @@ -0,0 +1,29 @@ + +val eqb : char list -> char list -> bool + +type attr_name = char list + +type relation = { rel_name : char list; rel_finite : bool } + +type database = (char list * relation) list + +val db_lookup : char list -> database -> relation option + +type literal = +| LitInt of int +| LitStr of char list +| LitBool of bool + +type query = +| Base of char list +| Const of (attr_name * literal) list +| Select of query * query +| Join of attr_name list * query * query +| Cartesian of query * query +| Project of attr_name list * query +| Rename of (attr_name * attr_name) list * query +| Union of query * query +| Diff of query * query +| Take of int * query + +val predicted_finite : database -> query -> bool option |