Add poc files
This commit is contained in:
Joey Yakimowich-Payne
parent
30da2412e3
commit
fa600b98f7
220 changed files with 45679 additions and 0 deletions
357
h_program-lang/datalog_code.ml
Normal file
357
h_program-lang/datalog_code.ml
Normal file
|
|
@ -0,0 +1,357 @@
|
|||
(* Yoann Padioleau
|
||||
*
|
||||
* Copyright (C) 2014 Facebook
|
||||
*
|
||||
* This library is free software; you can redistribute it and/or
|
||||
* modify it under the terms of the GNU Lesser General Public License
|
||||
* version 2.1 as published by the Free Software Foundation, with the
|
||||
* special exception on linking described in file license.txt.
|
||||
*
|
||||
* This library is distributed in the hope that it will be useful, but
|
||||
* WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the file
|
||||
* license.txt for more details.
|
||||
*)
|
||||
open Common
|
||||
|
||||
(*****************************************************************************)
|
||||
(* Prelude *)
|
||||
(*****************************************************************************)
|
||||
(*
|
||||
* See also prolog_code.ml!
|
||||
*
|
||||
* datalog engines:
|
||||
* - toy datalog using lua
|
||||
* - bddbddb, a scalabe engine!
|
||||
* - TODO: pydatalog, embedded DSL in python that can import data from
|
||||
* SQL
|
||||
* - ciao? xsb?
|
||||
* - http://www.learndatalogtoday.org/ and datomic.com
|
||||
*
|
||||
* TODO: https://yanniss.github.io/points-to-tutorial15.pdf
|
||||
*)
|
||||
|
||||
(*****************************************************************************)
|
||||
(* Types *)
|
||||
(*****************************************************************************)
|
||||
|
||||
(* for locals, but also right now for fields, globals, constants, enum, ... *)
|
||||
type var = string
|
||||
type func = string
|
||||
type fld = string
|
||||
|
||||
(* _cst_xxx, _str_line_xxx, _malloc_in_xxx_line, ... *)
|
||||
type heap = string
|
||||
(* _in_xxx_line_xxx_col_xxx *)
|
||||
type callsite = string
|
||||
|
||||
(* mimics datalog_code.dl top comment *)
|
||||
type fact =
|
||||
| PointTo of var * heap
|
||||
|
||||
| Assign of var * var
|
||||
| AssignContent of var * var
|
||||
| AssignAddress of var * var
|
||||
|
||||
| AssignDeref of var * var
|
||||
|
||||
| AssignLoadField of var * var * fld
|
||||
| AssignStoreField of var * fld * var
|
||||
| AssignFieldAddress of var * var * fld
|
||||
|
||||
| AssignArrayElt of var * var
|
||||
| AssignArrayDeref of var * var
|
||||
| AssignArrayElementAddress of var * var
|
||||
|
||||
| Parameter of func * int * var
|
||||
| Return of func * var (* ret_xxx convention *)
|
||||
| Argument of callsite * int * var
|
||||
| ReturnValue of callsite * var
|
||||
| CallDirect of callsite * func
|
||||
| CallIndirect of callsite * var
|
||||
|
||||
(*****************************************************************************)
|
||||
(* Meta *)
|
||||
(*****************************************************************************)
|
||||
|
||||
(* see datalog_code.dl domain *)
|
||||
type value =
|
||||
| V of var
|
||||
| F of fld
|
||||
| N of func
|
||||
| I of callsite
|
||||
| Z of int
|
||||
|
||||
let string_of_value = function
|
||||
| V x | F x | N x | I x -> x
|
||||
| Z _ -> raise Impossible
|
||||
|
||||
type _rule = string
|
||||
|
||||
type _meta_fact =
|
||||
string * value list
|
||||
|
||||
let meta_fact = function
|
||||
| PointTo (a, b) -> "point_to", [ V a; V b; ]
|
||||
| Assign (a, b) -> "assign", [ V a; V b; ]
|
||||
| AssignContent (a, b) -> "assign_content", [ V a; V b; ]
|
||||
| AssignAddress (a, b) -> "assign_address", [ V a; V b; ]
|
||||
| AssignDeref (a, b) -> "assign_deref", [ V a; V b; ]
|
||||
| AssignLoadField (a, b, c) -> "assign_load_field", [ V a; V b; F c ]
|
||||
| AssignStoreField (a, b, c) -> "assign_store_field", [ V a; F b; V c ]
|
||||
| AssignFieldAddress (a, b, c) -> "assign_field_address", [ V a; V b; F c ]
|
||||
| AssignArrayElt (a, b) -> "assign_array_elt", [ V a; V b; ]
|
||||
| AssignArrayDeref (a, b) -> "assign_array_deref", [ V a; V b; ]
|
||||
| AssignArrayElementAddress (a, b) -> "assign_array_element_address", [ V a; V b; ]
|
||||
| Parameter (a, b, c) -> "parameter", [ N a; Z b; V c ]
|
||||
| Return (a, b) -> "return", [ N a; V b; ]
|
||||
| Argument (a, b, c) -> "argument", [ I a; Z b; V c ]
|
||||
| ReturnValue (a, b) -> "call_ret", [ I a; V b; ]
|
||||
| CallDirect (a, b) -> "call_direct", [ I a; N b; ]
|
||||
| CallIndirect (a, b) -> "call_indirect", [ I a; V b; ]
|
||||
|
||||
|
||||
(*****************************************************************************)
|
||||
(* Toy datalog *)
|
||||
(*****************************************************************************)
|
||||
|
||||
let string_of_fact fact =
|
||||
let str, xs = meta_fact fact in
|
||||
spf "%s(%s)" str
|
||||
(xs +> List.map (function
|
||||
| V x | F x | N x | I x -> spf "'%s'" x
|
||||
| Z i -> spf "%d" i
|
||||
) +> Common.join ", "
|
||||
)
|
||||
|
||||
(*****************************************************************************)
|
||||
(* Bddbddb *)
|
||||
(*****************************************************************************)
|
||||
|
||||
(* "V", "F", ... *)
|
||||
type _domain = string
|
||||
|
||||
let domain_of_value = function
|
||||
| V _ -> "V"
|
||||
| F _ -> "F"
|
||||
| N _ -> "N"
|
||||
| I _ -> "I"
|
||||
| Z _ -> "Z"
|
||||
|
||||
type _idx = (string (* metadomain*), value Common.hashset) Hashtbl.t
|
||||
|
||||
|
||||
|
||||
let bddbddb_of_facts facts dir =
|
||||
let metas = facts +> List.map meta_fact in
|
||||
|
||||
let hvalues = Hashtbl.create 6 in
|
||||
let hrules = Hashtbl.create 30 in
|
||||
|
||||
(* build sets *)
|
||||
metas +> List.iter (fun (arule, xs) ->
|
||||
let listref =
|
||||
try Hashtbl.find hrules arule
|
||||
with Not_found ->
|
||||
let aref = ref [] in
|
||||
Hashtbl.add hrules arule aref;
|
||||
aref
|
||||
in
|
||||
listref := xs :: !listref;
|
||||
|
||||
xs +> List.iter (fun v ->
|
||||
let add_v v =
|
||||
let domain = domain_of_value v in
|
||||
let hdomain =
|
||||
try Hashtbl.find hvalues domain
|
||||
with Not_found ->
|
||||
let h = Hashtbl.create 10001 in
|
||||
Hashtbl.add hvalues domain h;
|
||||
h
|
||||
in
|
||||
Hashtbl.replace hdomain v true;
|
||||
in
|
||||
add_v v;
|
||||
(* for field_to_var and var_to_func *)
|
||||
(match v with
|
||||
| F s -> add_v (V s)
|
||||
| N s -> add_v (V s)
|
||||
| _ -> ()
|
||||
)
|
||||
)
|
||||
);
|
||||
|
||||
(* now build integer indexes *)
|
||||
let domains_idx =
|
||||
hvalues +> Common.hash_to_list +> List.map (fun (domain, hdomain) ->
|
||||
let conv = hdomain +> Common.hashset_to_list +> Common.index_list_0 in
|
||||
domain, (
|
||||
conv, conv +> Common.hash_of_list
|
||||
)
|
||||
)
|
||||
in
|
||||
|
||||
Common.command2 (spf "rm -f %s/*" dir);
|
||||
(* generate .map *)
|
||||
domains_idx +> List.iter (fun (domain, (map, _idx)) ->
|
||||
if domain <> "Z"
|
||||
then begin
|
||||
let file = Filename.concat dir (domain ^ ".map") in
|
||||
Common.with_open_outfile file (fun (pr_no_nl, _chan) ->
|
||||
let pr s = pr_no_nl (s ^ "\n") in
|
||||
|
||||
map +> List.iter (fun (v, _int) ->
|
||||
pr (string_of_value v)
|
||||
)
|
||||
)
|
||||
end
|
||||
);
|
||||
|
||||
(* generate .tuples *)
|
||||
hrules +> Common.hash_to_list +> List.iter (fun (arule, xxs) ->
|
||||
let arule =
|
||||
match arule with
|
||||
| "point_to" -> "point_to0"
|
||||
| "assign" -> "assign0"
|
||||
| s -> s
|
||||
in
|
||||
|
||||
let file = Filename.concat dir (arule ^ ".tuples") in
|
||||
Common.with_open_outfile file (fun (pr_no_nl, _chan) ->
|
||||
let pr s = pr_no_nl (s ^ "\n") in
|
||||
|
||||
(* todo: header?? *)
|
||||
(match !xxs with
|
||||
| [] -> ()
|
||||
| xs::_xxs ->
|
||||
let hcnt = Hashtbl.create 6 in
|
||||
pr (spf "# %s"
|
||||
(xs +> List.map (fun v ->
|
||||
let domain = domain_of_value v in
|
||||
let cnt =
|
||||
try Hashtbl.find hcnt domain
|
||||
with Not_found ->
|
||||
let cnt = ref 0 in
|
||||
Hashtbl.add hcnt domain cnt;
|
||||
cnt
|
||||
in
|
||||
let i = !cnt in
|
||||
incr cnt;
|
||||
(* less: size? *)
|
||||
spf "%s%d:18" domain i
|
||||
) +> Common.join " "))
|
||||
);
|
||||
|
||||
!xxs +> List.iter (fun xs ->
|
||||
let ints =
|
||||
xs +> List.map (fun v ->
|
||||
let i =
|
||||
match v with
|
||||
| Z i -> i
|
||||
| _ ->
|
||||
let domain = domain_of_value v in
|
||||
let (_, hdomainconv) = List.assoc domain domains_idx in
|
||||
Hashtbl.find hdomainconv v
|
||||
in
|
||||
i
|
||||
)
|
||||
in
|
||||
pr (ints +> List.map i_to_s +> Common.join " ")
|
||||
);
|
||||
)
|
||||
);
|
||||
|
||||
(* generate extra .tuples *)
|
||||
let fvals = try List.assoc "F" domains_idx +> fst with Not_found -> [] in
|
||||
let nvals = try List.assoc "N" domains_idx +> fst with Not_found -> [] in
|
||||
let (_vvals, vconv) = List.assoc "V" domains_idx in
|
||||
let arule = "field_to_var" in
|
||||
|
||||
let file = Filename.concat dir (arule ^ ".tuples") in
|
||||
Common.with_open_outfile file (fun (pr_no_nl, _chan) ->
|
||||
let pr s = pr_no_nl (s ^ "\n") in
|
||||
|
||||
pr "# F0:18 V0:18";
|
||||
|
||||
fvals +> List.iter (fun (fld, idx) ->
|
||||
match fld with
|
||||
| F s ->
|
||||
let v = V s in
|
||||
let idx2 = Hashtbl.find vconv v in
|
||||
pr (spf "%d %d" idx idx2)
|
||||
| _ ->
|
||||
pr2_gen (fld, idx);
|
||||
raise Impossible
|
||||
)
|
||||
);
|
||||
|
||||
let arule = "var_to_func" in
|
||||
|
||||
let file = Filename.concat dir (arule ^ ".tuples") in
|
||||
Common.with_open_outfile file (fun (pr_no_nl, _chan) ->
|
||||
let pr s = pr_no_nl (s ^ "\n") in
|
||||
|
||||
pr "# V0:18 N0:18";
|
||||
|
||||
nvals +> List.iter (fun (n, idx) ->
|
||||
match n with
|
||||
| N s ->
|
||||
let v = V s in
|
||||
let idx2 = Hashtbl.find vconv v in
|
||||
(* subtle, different order than for field_to_var, idx2 before *)
|
||||
pr (spf "%d %d" idx2 idx)
|
||||
| _ ->
|
||||
pr2_gen (n, idx);
|
||||
raise Impossible
|
||||
)
|
||||
);
|
||||
|
||||
|
||||
()
|
||||
|
||||
|
||||
|
||||
let bddbddb_explain_tuples file =
|
||||
let (d,b,_e) = Common2.dbe_of_filename file in
|
||||
let dst = Common2.filename_of_dbe (d,b,"explain") in
|
||||
Common.with_open_outfile dst (fun (pr_no_nl, _chan) ->
|
||||
let pr s = pr_no_nl (s ^ "\n") in
|
||||
|
||||
let xs = Common.cat file in
|
||||
(match xs with
|
||||
| header::xs ->
|
||||
if header =~ "# \\(.*\\)"
|
||||
then
|
||||
let s = Common.matched1 header in
|
||||
let flds = Common.split "[ \t]" s in
|
||||
let fld_domains =
|
||||
flds +> List.map (fun s ->
|
||||
if s =~ "\\([A-Z]\\)[0-9]?:"
|
||||
then Common.matched1 s
|
||||
else failwith (spf "could not find header in %s" file)
|
||||
)
|
||||
in
|
||||
let fld_translates =
|
||||
fld_domains +> List.map (fun s ->
|
||||
let mapfile = Common2.filename_of_dbe (d,s,"map") in
|
||||
Common.cat mapfile +> Array.of_list
|
||||
)
|
||||
in
|
||||
|
||||
xs +> List.iter (fun s ->
|
||||
let vs = Common.split "[ \t]" s +> List.map s_to_i in
|
||||
|
||||
let args =
|
||||
Common2.zip vs fld_translates +> List.map (fun (i, arr) ->
|
||||
arr.(i)
|
||||
)
|
||||
in
|
||||
pr (spf "%s(%s)" b (Common.join ", " args))
|
||||
)
|
||||
|
||||
else failwith (spf "could not find header in %s" file)
|
||||
|
||||
| [] -> pr2 (spf "empty file %s" file)
|
||||
)
|
||||
);
|
||||
dst
|
||||
Loading…
Add table
Add a link
Reference in a new issue