diff --git a/bincaml.opam b/bincaml.opam index 532328ea..f86f83c6 100644 --- a/bincaml.opam +++ b/bincaml.opam @@ -13,6 +13,7 @@ bug-reports: "https://github.com/username/reponame/issues" depends: [ "dune" {>= "3.19"} "ocaml" + "unionFind" "capstone_arm64_disas" "aslp_lifter_ocaml" {>= "1.1"} "ocaml-protoc-plugin" {>= "6.1.0"} diff --git a/dune-project b/dune-project index 6911101f..3878a8d8 100644 --- a/dune-project +++ b/dune-project @@ -37,6 +37,7 @@ (description "A longer description") (depends ocaml + unionFind capstone_arm64_disas (aslp_lifter_ocaml (>= 1.1)) (ocaml-protoc-plugin (>= 6.1.0)) diff --git a/lib/lang/dune b/lib/lang/dune index e2cd189a..858d4b56 100644 --- a/lib/lang/dune +++ b/lib/lang/dune @@ -1,24 +1,10 @@ +(include_subdirs qualified) + (library (public_name bincaml.ast) (name lang) - (modules - abstract_expr - attrib - spec_modifies - check - expr - algsimp - common - ops - viscfg - expr_smt - expr_eval - stmt - block - procedure - interp - program) (libraries + unionFind zarith fix ocamlgraph diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml index 0bfc1223..ca673a08 100644 --- a/lib/lang/expr.ml +++ b/lib/lang/expr.ml @@ -393,6 +393,7 @@ module BasilExpr = struct | BinaryExpr { op; arg1 = l; arg2 = r } -> ret_type_bin op l r |> get_ty | ApplyIntrin { op; args } -> ret_type_intrin op args |> get_ty | ApplyFun { func; args } -> + (* FIXME: this is wrong *) let _, rt = Types.uncurry func in rt | Lambda { op; bound_vars; in_body = b } -> diff --git a/lib/lang/hm.ml b/lib/lang/hm.ml deleted file mode 100644 index 3f71d220..00000000 --- a/lib/lang/hm.ml +++ /dev/null @@ -1,10 +0,0 @@ -module Type = struct - type t = - | BVVar of string - | Int - | BV of int - | Bool - | Var of string - | Sort of string - | Fun of t * t -end diff --git a/lib/lang/hm/elaboration.ml b/lib/lang/hm/elaboration.ml new file mode 100644 index 00000000..0bfab1e3 --- /dev/null +++ b/lib/lang/hm/elaboration.ml @@ -0,0 +1,247 @@ +open Common +open Abstract_expr + +(** Hindley-Milner type inference based on a union-find. *) + +module TypeInference (T : TypeExpr.TypeContext) = struct + include Inference.Make (T) + + let retype_var univ ctx id = + lookup_var_typ ~no_constraint:true univ ctx id |> find |> to_basil + |> fun typ -> Var.copy ~typ id + + let elaborate_phi univ ctx (p : Var.t Block.phi list) = + let open Block in + List.map + (fun { lhs; rhs } -> + let lhs = retype_var univ ctx lhs in + let rhs = List.map (fun (a, r) -> (a, retype_var univ ctx r)) rhs in + { lhs; rhs }) + p + + let ctx_to_string ctx = + TCtx.to_iter ctx + |> Iter.to_string (fun (a, b) -> + Printf.sprintf "%s %s" (V.to_string a) (scheme_to_string b)) + + let fresh_tvar ?(n = "a") () = fix @@ Var (gen.fresh ~name:n ()) + let unfix i = match i with Expr.BasilExpr.E i -> i + let rec cata alg e = (unfix %> AbstractExpr.map (cata alg) %> alg) e + + (** Extract type after full inference has run. *) + let elaborate_expr ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = + let alg e = + let e = + match e with + | AbstractExpr.RVar { id; attrib; typ } -> + (* avoid looking up the id in context as we may be in a local + binding *) + let id = Var.copy id ~typ:(to_basil @@ find typ) in + AbstractExpr.RVar { id; attrib; typ } + | o -> o + in + let t = AbstractExpr.get_typ e |> find |> to_basil in + AbstractExpr.set_typ e t |> Expr.BasilExpr.fix + in + e |> TypingExpr.cata alg + + let elaborate_stmt univ ctx stmt = + let retype_var v = + let typ = + lookup_var_typ ~no_constraint:true univ ctx v |> find |> to_basil + in + Var.copy ~typ v + in + Stmt.map + ~f_expr:(fun e -> elaborate_expr ~univ [%here] e ctx) + ~f_lvar:retype_var ~f_rvar:retype_var stmt + + let elaborate_block p univ ctx (b : ('a, 'b) Block.t) = + Block.map ~phi:(elaborate_phi univ ctx) (elaborate_stmt univ ctx) b + + let assume_proc_decl ctx ?(no_constraint = false) (p : Program.proc) = + let globs = Var.Decls.values (Procedure.local_decls p) in + let formals_in = Procedure.formal_in_params p |> StringMap.values in + let formals_out = Procedure.formal_out_params p |> StringMap.values in + let univ = V.proc_univ @@ Procedure.id p in + let ctx = + Iter.fold + (decl_var_typ ~no_constraint univ) + ctx + (Iter.append globs @@ Iter.append formals_in formals_out) + in + ctx + + let infer_proc vc prog ctx ?(no_constraint = false) (p : Program.proc) = + let spec = Procedure.specification p in + let univ = V.proc_univ @@ Procedure.id p in + let ibool_list b = + List.map + (fun a -> + let a = infer_expr vc ~univ [%here] a ctx in + let _ = unify (fix bool_type) (getty a) in + a) + b + in + let spec : ('a, 'b) Procedure.proc_spec = + { + requires = ibool_list spec.requires; + ensures = ibool_list spec.ensures; + rely = ibool_list spec.rely; + guarantee = ibool_list spec.guarantee; + captures_globs = + List.map (infer_var global_universe ctx) spec.captures_globs; + modifies_globs = + List.map (infer_var global_universe ctx) spec.modifies_globs; + } + in + + let new_spec ctx : (Var.t, Expr.BasilExpr.t) Procedure.proc_spec = + { + requires = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.requires; + ensures = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.ensures; + rely = List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.rely; + guarantee = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.guarantee; + captures_globs = spec.captures_globs |> List.map fst; + modifies_globs = spec.modifies_globs |> List.map fst; + } + in + + let ctx = assume_proc_decl ctx ~no_constraint p in + let bvlocks = + Procedure.iter_blocks_topo_fwd p + |> Iter.map (fun (i, b) -> (i, infer_block vc prog univ ctx b)) + |> Iter.persistent + in + + let elaborate_proc ctx = + Procedure.set_specification p (new_spec ctx) + |> (fun p -> + bvlocks + |> Iter.map (fun (bid, b) -> (bid, elaborate_block [%here] univ ctx b)) + |> Iter.fold (fun p (bid, b) -> Procedure.update_block p bid b) p) + |> Procedure.map_formal_in_params (StringMap.map (retype_var univ ctx)) + |> Procedure.map_formal_out_params (StringMap.map (retype_var univ ctx)) + in + Logs.debug (fun m -> m "%s" (ctx_to_string ctx)); + (elaborate_proc, ctx) + + (** Run type inference on a declaration, returning an updated typing scheme, + and elaboration function*) + let infer_decl visit_constraint prog scheme = + let open Program in + let infer_expr = infer_expr visit_constraint in + let infer_proc = infer_proc visit_constraint in + (* We have to be careful that inference is run immediately, not delayed until elaboration. *) + fun (decl_id, d) -> + match d with + | Type { binding; typ } -> + let ty = ty_of_basil typ in + let scheme = decl_type scheme binding ty in + let nty scheme = Type { binding; typ = to_basil (find ty) } in + (scheme, `Decl (decl_id, nty)) + | Function { binding; definition; attrib } -> ( + (* elaboration of var binding *) + let scheme = decl_var_typ global_universe scheme binding in + let binding s = retype_var global_universe s binding in + match definition with + | Axiom b -> + let bt = fix bool_type in + let b = infer_expr ~univ:global_universe [%here] b scheme in + let _ = unify (getty b) bt in + let new_axiom scheme = + Function + { + attrib; + binding = binding scheme; + definition = + Axiom + (elaborate_expr ~univ:global_universe [%here] b scheme); + } + in + (scheme, `Decl (decl_id, new_axiom)) + | Uninterpreted -> + let new_uf s = + Function + { binding = binding s; attrib; definition = Uninterpreted } + in + (scheme, `Decl (decl_id, new_uf)) + | Function definition -> + let e = + infer_expr ~univ:global_universe [%here] definition scheme + in + let new_fundef scheme = + Function + { + binding = binding scheme; + attrib; + definition = + Function + (elaborate_expr ~univ:global_universe [%here] e scheme); + } + in + (scheme, `Decl (decl_id, new_fundef))) + | Variable { binding; attrib; classification } -> + let scheme = decl_var_typ global_universe scheme binding in + let binding s = retype_var global_universe s binding in + let classification = + let tyv = + classification + |> Option.map (fun classi -> + infer_expr ~univ:global_universe [%here] classi scheme) + in + fun final_scheme -> + tyv + |> Option.map (fun e -> + elaborate_expr ~univ:global_universe [%here] e final_scheme) + in + let new_vardef fscheme = + Variable + { + binding = binding fscheme; + attrib; + classification = classification fscheme; + } + in + (scheme, `Decl (decl_id, new_vardef)) + | Procedure { definition } -> + let elaborate_proc, scheme = infer_proc prog scheme definition in + (scheme, `Procedure (decl_id, elaborate_proc)) + + (** The function that does everything *) + let infer_program prog = + let decls = Program.declarations prog |> Iter.to_list in + let constraints = ref [] in + let visit_constraint c = constraints := c :: !constraints in + (* We fold the inference context through every declaration and + calling the inference functions, returning an expressions typed with the + type expressions herein. We also return the resulting list of elaboration + functions, which take the final inference context and convert the HM-typed + expressions back to bincaml typed expressions. *) + let scheme, new_decls = + decls |> List.fold_map (infer_decl visit_constraint prog) TCtx.empty + in + let _ = solve_constraints ~max_iters:50 !constraints in + (* TODO: implicit decls; constructors need to be added after the types they + construct, probably simples to do implicits immediately after the thing they + relate to. Maybe they should just appear this way in the declaration + list. *) + let prog = + List.fold_left + (fun prog -> function + | `Decl (id, ndecl) -> + let decl = ndecl scheme in + (* assuming the id is the same (it has to be) *) + Program.update_decl prog decl + | `Procedure (id, nproc) -> + let proc = nproc scheme in + (* assuming the id is the same (it has to be) *) + let prog = Program.update_proc id (fun _ -> Some proc) prog in + prog) + prog new_decls + in + (scheme, prog) +end diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml new file mode 100644 index 00000000..c8a9b1ea --- /dev/null +++ b/lib/lang/hm/hm.ml @@ -0,0 +1,209 @@ +(** Simple hindley-milner type inference *) + +(** Union-find-based implementation of Hindley-Milner type inference for + type-annotating the AST, without let-generalisation at the moment. + + This is based on Algorithm J described in Milner, 1978; + {:https://doi.org/10.1016%2F0022-0000%2878%2990014-4}. + + The following may be more accessible: + + - {:https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Algorithm_J} + - {:https://bernsteinbear.com/blog/type-inference/} *) + +module TypeExpr = TypeExpr +(** {1 Type Expressions} + + Bincaml's AST is generic in the type annotation expression. + + The type system that is embedded in the concrete expression type we use is + defined in {! Common.Types}. + + This is the type loaded by the frontend, and attached to variables, and + expressions, and which all prettyprinters assume. + + The underlying expression type though, {! Expr.AbstractExpr.t} is generic in + the type. + + To perform type inference we lift the bincaml type to a minimal + representation, and create expressions annotated with this type expression. + + Once inference has finished, we extract again expressions typed with the + bincaml type. + + The HM type is simple, it is either + + - a type variable + - a type constructor of the form [(type list, constr. name)] + + {[ + type 'a expr = Var of tvar | TypeConstr of 'a list * string + ]} + + This type is open recursive so we can traverse it using the + {! Bincaml_util.Recursionscheme} module. + + This type is hash-consed so we can retrieve a canonical reference for each + corresponding bincaml type. + + This type is placed in a union-find datastructre in order to perform type + unification. *) + +(** {1 Type Inference} + + Type inference is split into two phases, inference and elaboration. + Inference determines the type for each expression in the program, raising + type errors when conflicts arise. Elaboration anotates the program with + these expressions. + + {2 Inference} *) + +module Hm_types = Hm_types +(** Conversions to/form HM state and bincaml types *) + +module Unification = Unification +module Inference = Inference + +(** Traversal of expressions to infer types + + We traverse the bincaml AST and construct a {! TypeExpr.t} for the type of + each expression, and perform unification to determine what the type is. + + Bincaml has some specific concerns: for its type system: + + {3 Ad-hoc polymorpic operators} + + Our operators are ad-hoc polymorphic. Polymorphism in HM is represented with + type schemes. A type-scheme in HM is a non-recursive universal quantifier + over type variables. + + {[ + type scheme = Forall of tvar list * t + ]} + + We represent our ad-hoc polymorphic operators by immediately generalising + them, returning a type scheme for a generic function type. For instance for + [bvadd] we know all the widths have to be equal, so the type scheme is + + [bvadd :: Forall i : Bitvector i -> Bitvector i -> Bitvector i] *) + +module Solve_bv = Solve_bv + +(** {3 Parametric Bitvectors} + + For cases like [bvadd], it is enough that one of their arguments (or return) + be type annotated in order to infer concrete types for all type variables in + the type scheme. + + However some operations, such as concatenation, are typed depending on + arithmetic over the width values of the arguments passed to them. + + We define the type constructor ℕ to represent numeric types, we interpret it + as a number when its argument is a type constructor which is the string + representation of a number. E.g. the type "5 ℕ" represents the number 5. + + The [bv] bitvector type is parametric in its width, i.e [bv5] is defined as; + + {[ + TypeConstr ([5 ℕ, "bv") + ]} + + When we do not know the exact width we use a type variable, and rely on + unification, and a width-solving post-pass to determine the precise type. + + If there is not enough information to determine a concrete width, extraction + to a bincaml type will fail with a type error. + + In order to solve for widths, we represent width-dependent operations as a a + pair of a type scheme and type constraint. E.g. for [concat] this type + constraint is of the form + + {[ + (* scheme *) + concat :: Forall a b c : Bitvector a -> Bitvector b -> Bitvector c + + (* constraint *) + Add { a ; b; equ=c } (** a + b = c *) + ]} + + These constraints are collected, and solved iteratively after the inference + pass has run. This proces is naive and exponential in the number of + deductive steps it has to make. *) + +module Elaboration = Elaboration +(** {2 Elaboration} + + As the inference returns a version of the program typed with the HM + [TypeExpr]s, the elaboration amounts to a traversal of the program which + constructs bincaml-typed representations of these structures. + + This module implements both inference and elaboratino for the high-level + program structures as this simplifies book-keeping of types. *) + +(** {1 High-level type-inference operations}*) + +open Common +open Abstract_expr + +(* + TODO: + + In order to maintain well-typedness of rewrites we will probably want to + inject the global type definitions into the program, always. Otherwise we + probably risk inferring inconsistent types. Maybe this goes for for all the + global bindings. I.e. if we use a definition incorrectly it will end up + ill-typed and that error will be harder to track down. Injecting all the + bindings is somewhat giving up though. + + We could justifiably just require + transforms to "know what they are doing" and inject enough type information for + it to be well-typed coming out. Mistakes could be found by running a global + program typecheck after the transform. *) + +(** Algebra that infers types of expressions in a fresh local context, assuming + all free variables are defined and annotated. *) +let locally_elaborate_expr (e : Expr.BasilExpr.t) = + let open AbstractExpr in + let open Ops.AllOps in + let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in + let constraints = ref [] in + let univ = "" in + let ctx = + Expr.BasilExpr.free_vars_iter e + |> Iter.fold (T.decl_var_typ univ) TypeExpr.TCtx.empty + in + let visit_constraint c = constraints := c :: !constraints in + (* TODO: need mode where we absorb take the existing annotations and try to + extend , rather than expecting everythign declared in context. *) + let i = T.infer_expr visit_constraint ~univ [%here] e ctx in + let _ = T.solve_constraints ~max_iters:100 !constraints in + let e = T.elaborate_expr ~univ [%here] i ctx in + e + +(** Algebra for returning the annotated type (for use with functions like + fold_with_type)*) +let elaborated_type_alg (e : Types.t Expr.BasilExpr.abstract_expr) = + Expr.AbstractExpr.get_typ e + +(** Partially apply args list to function type funtype and return resulting type +*) +let type_applied (funtype : Types.t) (args : Types.t list) = + let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in + let rt = T.fresh_tvar ~n:"ret" () in + let args = List.map T.ty_of_basil args in + + let funt = T.curry_f args rt in + let ft = T.ty_of_basil funtype in + try + T.unify ~pos:[%here] ft funt |> ignore; + Ok (T.to_basil rt) + with Hm_types.TypeErr e -> Error e + +(** Apply type inference to a program and return a fully type-annotated copy of + the program. *) +let elaborate_prog prog = + (* We need to create a local typing module in order to get fresh state for the + union find and hash cons. *) + let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in + let scheme, prog = T.infer_program prog in + prog diff --git a/lib/lang/hm/hm_types.ml b/lib/lang/hm/hm_types.ml new file mode 100644 index 00000000..1563b94e --- /dev/null +++ b/lib/lang/hm/hm_types.ml @@ -0,0 +1,120 @@ +(** Conversion from bincaml types to and from HM type inference environment *) + +open Common +open Abstract_expr + +exception TypeErr of string + +module Make (T : TypeExpr.TypeContext) = struct + module Ctx = T + include Ctx + include TypeExpr + include Typ + + type typ = T.Typ.t [@@deriving eq, ord] + + (** Recursion algebra for printing types *) + let printer_alg = function + | Var e -> ID.to_string e + | TypeConstr ([ l ], e) -> l ^ " " ^ e + | TypeConstr ([ a; b ], "->") -> a ^ " -> " ^ b + | TypeConstr ([], e) -> e + | TypeConstr (ls, e) -> + List.to_string ~start:"(" ~stop:")" ~sep:"," Fun.id ls ^ " " ^ e + + let type_to_string t = Rec.cata printer_alg t + + let plpos (l : Lexing.position) = + Printf.sprintf "%s:%d" l.pos_fname l.pos_lnum + + (** Type schemes; how values of the typing context are typed. *) + type scheme = Forall of tvar list * t + + let scheme_to_string = function + | Forall (tl, t) -> + List.to_string ID.to_string tl ^ ". " ^ type_to_string (find t) + + (** Function type, takes two arguments: we always curry. *) + let fun_type a b = TypeConstr ([ a; b ], "->") + + (** A type representing a number *) + let nat_val_type i = + let num = fix (TypeConstr ([], Int.to_string i)) in + TypeConstr ([ num ], "ℕ") + + let is_nat_val_type (i : t) = + match unfix i with + | TypeConstr ([ num ], "ℕ") -> ( + match unfix num with + | TypeConstr ([], num) -> Int.of_string num + | _ -> None) + | _ -> None + + (** A bitvector type parametric in its width *) + let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") + + (** Bitvector of arbitrary size *) + let bvunk i = TypeConstr ([ i ], "bv") + + (** {2 Primitive types} *) + + let int_type = TypeConstr ([], "int") + let bool_type = TypeConstr ([], "bool") + let unit_t = TypeConstr ([], "unit") + let top_t = TypeConstr ([], "top") + let nothing_t = TypeConstr ([], "nothing") + let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") + let ptr_typ = bv_type 64 + + let rec to_basil (t : t) : Types.t = + let wrapped t f = + try f () + with TypeErr e -> + raise (TypeErr ("error in " ^ (type_to_string @@ t) ^ ": " ^ e)) + in + let open Types in + wrapped t @@ fun () -> + match unfix t with + | TypeConstr ([ a; b ], "->") -> + let a = wrapped a @@ fun () -> to_basil a in + let b = wrapped b @@ fun () -> to_basil b in + Map (a, b) + | TypeConstr ([ w ], "bv") -> ( + match is_nat_val_type w with + | Some i -> Bitvector i + | None -> raise (TypeErr ("bitvector unresolved: " ^ type_to_string t))) + | TypeConstr ([], "unit") -> Unit + | TypeConstr ([], "bool") -> Boolean + | TypeConstr ([], "int") -> Integer + | TypeConstr ([], "top") -> Top + | TypeConstr ([], "nothing") -> Nothing + | TypeConstr ([], o) -> Sort (o, []) + | _ -> failwith "not impl" + + let rec ty_of_basil (t : Types.t) : t = + let e = + match t with + | Types.Boolean -> bool_type + | Types.Integer -> int_type + | Types.Bitvector i -> bv_type i + | Types.Unit -> unit_t + | Types.Top -> top_t + | Types.Nothing -> nothing_t + | Types.Map (a, b) -> fun_type (ty_of_basil a) (ty_of_basil b) + | Types.Sort (n, _) -> TypeConstr ([], n) + | Types.Struct _ -> failwith "unsupp" + | Types.Pointer { lower; upper } -> + ptr_typ_sub (ty_of_basil lower) (ty_of_basil upper) + | Types.Variable n -> Var (gen.fresh ~name:n ()) + in + fix e + + let curry (args : t expr list) (v : t expr) = + List.fold_left (fun a p -> fix @@ fun_type (fix p) a) (fix v) args + + let curry_f (args : t list) (v : t) = + List.fold_left (fun a p -> fix @@ fun_type p a) v args + + let types_universe = "" + let global_universe = "" +end diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml new file mode 100644 index 00000000..123f49e3 --- /dev/null +++ b/lib/lang/hm/inference.ml @@ -0,0 +1,338 @@ +open Common +open Abstract_expr +open Hm_types + +(** Hindley-Milner type inference based on a union-find. *) + +module Make (T : TypeExpr.TypeContext) = struct + open TypeExpr + include Solve_bv.Make (T) + + (** An AbstractExpr.t with [t] used as the type. *) + module AbsTypingExpr = struct + open Ops + include AllOps + module Var = Var + + type var = Var.t + + type t = E of (const, Var.t, unary, binary, intrin, typ, t) AbstractExpr.t + [@@unboxed] [@@deriving eq, ord] + + type nonrec typ = typ + + let top_typ = fix @@ top_t + let fix i = E i + let unfix i = match i with E i -> i + end + + module TypingExpr = Expr.Make (AbsTypingExpr) + + let getty = AbsTypingExpr.unfix %> Expr.AbstractExpr.get_typ + + let infer_var univ ctx id = + let typ = lookup_var_typ univ ctx id in + (id, typ) + + (** Return the generic type scheme for an op. We generalise the type, and hope + dearly that a concrete type is found by inference. + + TODO: some approach like weak type variables that makes it a type error to + fail to instantiate. *) + let scheme_of_op ~visit_constraint (gen : ID.generator) + (o : [ Ops.AllOps.const | Ops.AllOps.unary | Ops.AllOps.binary ]) = + let fv () = fix @@ Var (gen.fresh ~name:"a" ()) in + match o with + | `Extract (hi, lo) -> curry [ bvunk (fv ()) ] (bv_type (hi - lo)) + | `SignExtend bits -> + let a = fv () in + let equ = fv () in + let r = curry [ bvunk a ] (bvunk equ) in + visit_constraint @@ AddConst { a; b = bits; equ }; + r + | `ZeroExtend bits -> + let a = fv () and equ = fv () in + visit_constraint @@ AddConst { a; b = bits; equ }; + curry [ bvunk a ] (bvunk equ) + | `BOOLTOBV1 -> curry [ bool_type ] (bv_type 1) + | `Bitvector b -> fix @@ bv_type (Bitvec.size b) + | #Ops.BVOps.binary_unif -> + let a = fv () in + curry [ bvunk a; bvunk a ] (bvunk a) + | #Ops.BVOps.binary_pred -> + let a = fv () in + curry [ bvunk a; bvunk a ] bool_type + | #Ops.BVOps.unary_unif -> + let a = fv () in + curry [ bvunk a ] (bvunk a) + | `INTNEG -> curry [ int_type ] int_type + | #Ops.IntOps.binary_pred -> curry [ int_type; int_type ] bool_type + | #Ops.IntOps.const -> fix @@ int_type + | #Ops.IntOps.binary_unif -> curry [ int_type; int_type ] int_type + | #Ops.LogicalOps.binary -> curry [ bool_type; bool_type ] bool_type + | #Ops.LogicalOps.unary -> curry [ bool_type ] bool_type + | #Ops.LogicalOps.const -> fix @@ bool_type + | `Old -> + let a = fv () in + curry_f [ a ] a + | #Ops.AllOps.binary as o -> + failwith @@ "unsupported op" ^ Ops.AllOps.to_string o + | #Ops.AllOps.unary as o -> + failwith @@ "unsupported op" ^ Ops.AllOps.to_string o + | #Ops.AllOps.const as o -> + failwith @@ "unsupported op" ^ Ops.AllOps.to_string o + + (** return the generic type scheme of an intrinsic operation *) + let scheme_of_intrin ?(visit_constraint = fun a -> ()) (gen : ID.generator) + (o : Ops.AllOps.intrin) args = + let fv () = fix @@ Var (gen.fresh ~name:"a" ()) in + match o with + | `BVADD | `BVMUL | `BVOR | `BVXOR | `BVAND -> + let a = fv () in + curry_f (List.init args (fun _ -> a)) a + | `BVConcat -> + let args = List.init args (fun _ -> fv ()) in + let rs = + List.reduce_exn + (fun a b -> + let equ = fv () in + visit_constraint (Add { a; b; equ }); + equ) + args + in + let rs = bvunk rs in + let args = List.map bvunk args in + curry args rs + | `OR | `AND -> curry (List.init args (fun _ -> bool_type)) bool_type + | `MapUpdate -> + let a = fv () in + let b = fv () in + let m = curry_f [ a ] b in + curry_f [ m; a; b ] m + | `Cases -> fv () + + let do_infer ~visit_constraint + (infer : + univ:string -> + Lexing.position -> + Program.e -> + scheme TCtx.t -> + AbsTypingExpr.t) univ hr e c : AbsTypingExpr.t = + let mkv v = V.of_var univ v in + let r = fix @@ Var (gen.fresh ()) in + let open Abstract_expr.AbstractExpr in + let e = Expr.BasilExpr.unfix e in + let e = set_typ e r in + match e with + | RVar { id; attrib } -> + let typ = lookup_var_typ univ c id in + AbsTypingExpr.fix (RVar { attrib; id; typ }) + | Lambda { op; bound_vars; in_body; attrib; triggers } -> begin + let tvars = List.map (fun v -> (v, inst_annot_v v)) bound_vars in + let ictx = + List.map (fun (v, t) -> (mkv v, Forall ([], t))) tvars + |> TCtx.add_list c + in + let bdty = infer ~univ [%here] in_body ictx in + let typ = + match op with + | `Lambda -> getty bdty + | `Forall | `Exists -> unify (getty bdty) (fix bool_type) + in + ignore @@ unify r (curry_f (List.map snd tvars) (getty bdty)); + let triggers = + List.map (List.map (fun e -> infer ~univ [%here] e ictx)) triggers + in + AbsTypingExpr.fix + (Lambda { op; bound_vars; in_body = bdty; attrib; typ; triggers }) + end + | Constant { const = #Ops.AllOps.const as op; attrib } -> begin + let f = scheme_of_op ~visit_constraint gen op in + let r = unify r f in + AbsTypingExpr.fix (Constant { typ = r; const = op; attrib }) + end + | UnaryExpr { op = #Ops.AllOps.unary as op; arg; attrib } -> begin + let f = scheme_of_op ~visit_constraint gen op in + let arg = infer ~univ [%here] arg c in + ignore @@ unify f (curry_f [ getty arg ] r); + AbsTypingExpr.fix (UnaryExpr { typ = r; op; attrib; arg }) + end + | BinaryExpr { op = #Ops.AllOps.binary as op; arg1; arg2; attrib } -> begin + let f = scheme_of_op ~visit_constraint gen op in + let arg1 = infer ~univ [%here] arg1 c in + let arg2 = infer ~univ [%here] arg2 c in + ignore @@ unify f (curry_f [ getty arg1; getty arg2 ] r); + AbsTypingExpr.fix (BinaryExpr { typ = r; op; attrib; arg1; arg2 }) + end + | ApplyIntrin { op = #Ops.AllOps.intrin as op; args; attrib } -> begin + let f = scheme_of_intrin ~visit_constraint gen op (List.length args) in + let args = List.map (fun a -> infer ~univ [%here] a c) args in + ignore @@ unify f (curry_f (List.map getty args) r); + AbsTypingExpr.fix (ApplyIntrin { typ = r; op; attrib; args }) + end + | ApplyFun { func; args; attrib } -> + let f = infer ~univ [%here] func c in + let args = List.map (fun a -> infer ~univ [%here] a c) args in + ignore @@ unify (getty f) (curry_f (List.map getty args) r); + AbsTypingExpr.fix (ApplyFun { typ = r; func = f; attrib; args }) + | Let _ -> failwith "" + + let rec infer_expr visit_constraint ~univ (hr : Lexing.position) e = + fun (c : scheme TCtx.t) -> + Logs.debug (fun m -> + m "%s" @@ "infer " ^ plpos hr ^ " " ^ Expr.BasilExpr.to_string e); + let t = + try do_infer ~visit_constraint (infer_expr visit_constraint) univ hr e c + with TypeErr m -> + raise (TypeErr (m ^ " : " ^ Expr.BasilExpr.to_string e)) + in + t + + let infer visit_constraint ~univ (hr : Lexing.position) e (c : scheme TCtx.t) + = + let nexpr = + infer_expr visit_constraint ~univ hr e c + |> AbsTypingExpr.unfix |> AbstractExpr.get_typ + in + nexpr + + let unfix i = match i with Expr.BasilExpr.E i -> i + let rec cata alg e = (unfix %> AbstractExpr.map (cata alg) %> alg) e + + let infer_phi visit_constraint univ ctx (p : Var.t Block.phi list) = + let infer = infer visit_constraint in + let open Block in + let r = fix @@ Var (gen.fresh ()) in + List.fold_left + (fun acc { lhs; rhs } -> + let lhs = infer [%here] ~univ (Expr.BasilExpr.rvar lhs) ctx in + let e = + List.fold_left + (fun a (_, r) -> + let r = infer [%here] ~univ (Expr.BasilExpr.rvar r) ctx in + unify a r) + lhs rhs + in + unify acc e) + r p + + let ctx_to_string ctx = + TCtx.to_iter ctx + |> Iter.to_string (fun (a, b) -> + Printf.sprintf "%s %s" (V.to_string a) (scheme_to_string b)) + + let fresh_tvar ?(n = "a") () = fix @@ Var (gen.fresh ~name:n ()) + + let do_infer_stmt visit_constraint p univ ctx stmt = + let open Stmt in + let infer_ty h e = infer_expr visit_constraint ~univ h e ctx in + let infer = infer visit_constraint in + + (*let r = fix @@ Var (gen.fresh ()) in*) + match stmt with + | Instr_IntrinCall _ -> failwith "intrin unsupported" + | Instr_Assume { body; branch; attrib } -> + let body = infer_ty [%here] body in + ignore @@ unify (fix bool_type) (getty body); + Instr_Assume { body; branch; attrib } + | Instr_Assert { body; attrib } -> + let body = infer_ty [%here] body in + ignore @@ unify (fix bool_type) (getty body); + Instr_Assert { body; attrib } + | Instr_Assign { al = ls; attrib } -> + let ls = List.map (fun (l, r) -> (l, infer_ty [%here] r)) ls in + List.iter + (fun (l, r) -> + ignore + @@ unify (infer ~univ [%here] (Expr.BasilExpr.rvar l) ctx) (getty r)) + ls; + Instr_Assign { al = ls; attrib } + | Instr_Call { lhs; procid; args; attrib } -> + let p = Program.proc p procid in + let infer_param p = + infer ~univ:(V.proc_univ procid) [%here] (Expr.BasilExpr.rvar p) ctx + in + let args = StringMap.mapi (fun param a -> infer_ty [%here] a) args in + StringMap.iter + (fun parm act -> + let form = + infer_param (StringMap.find parm (Procedure.formal_in_params p)) + in + ignore @@ unify form (getty act)) + args; + lhs + |> StringMap.map (fun a -> infer_ty [%here] (Expr.BasilExpr.rvar a)) + |> StringMap.iter (fun param act -> + let form = + infer_param (StringMap.find param @@ Procedure.formal_out_params p) + in + ignore @@ unify form (getty act)); + Instr_Call { lhs; procid; args; attrib } + | Instr_IndirectCall { target; attrib } -> + let target = infer_ty [%here] target in + ignore @@ unify (getty target) (fix ptr_typ); + Instr_IndirectCall { target; attrib } + | Instr_Load { lhs; rhs; addr = Scalar; attrib } -> + let lhs' = infer_ty [%here] (Expr.BasilExpr.rvar lhs) in + let rhs' = infer_ty [%here] (Expr.BasilExpr.rvar rhs) in + let _ = unify (getty lhs') (getty rhs') in + Instr_Load { lhs; rhs; addr = Scalar; attrib } + | Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } -> + let addr = infer_ty [%here] addr in + let _ = unify (fix @@ ptr_typ) (getty addr) in + let mapt = fix @@ fun_type (getty addr) (fresh_tvar ()) in + let _ = unify (lookup_var_typ univ ctx rhs) mapt in + let _ = + unify + (infer_ty [%here] (Expr.BasilExpr.rvar lhs) |> getty) + (fix @@ bv_type size) + in + Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } + | Instr_Store { lhs; rhs; value; addr = Scalar; attrib } -> + let value = infer_ty [%here] value in + let _ = + unify (getty value) + @@ unify + (infer ~univ [%here] (Expr.BasilExpr.rvar lhs) ctx) + (infer ~univ [%here] (Expr.BasilExpr.rvar rhs) ctx) + in + Instr_Store { lhs; rhs; value; addr = Scalar; attrib } + | Instr_Store + { lhs; rhs; value; addr = Addr { addr; size; endian }; attrib } -> + let addr = infer_ty [%here] addr in + let _ = unify (fix @@ ptr_typ) (getty addr) in + let mapt = fix @@ fun_type (getty addr) (fresh_tvar ()) in + let _ = + unify mapt (infer ~univ [%here] (Expr.BasilExpr.rvar lhs) ctx) + in + let _ = unify (lookup_var_typ univ ctx rhs) mapt in + let value = infer_ty [%here] value in + let _ = unify (getty value) (fix @@ bv_type size) in + Instr_Store + { lhs; rhs; value; addr = Addr { addr; size; endian }; attrib } + + let infer_stmt vc p univ ctx s = + try do_infer_stmt vc p univ ctx s + with TypeErr m -> + raise + (TypeErr + (m ^ " " + ^ Stmt.to_string Var.pretty Var.pretty Expr.BasilExpr.pretty s)) + + let infer_block vc p univ ctx (b : Program.bloc) = + let _ = infer_phi vc univ ctx b.phis in + Block.map ~phi:Fun.id (infer_stmt vc p univ ctx) b + + let assume_proc_decl ctx ?(no_constraint = false) (p : Program.proc) = + let globs = Var.Decls.values (Procedure.local_decls p) in + let formals_in = Procedure.formal_in_params p |> StringMap.values in + let formals_out = Procedure.formal_out_params p |> StringMap.values in + let univ = V.proc_univ @@ Procedure.id p in + let ctx = + Iter.fold + (decl_var_typ ~no_constraint univ) + ctx + (Iter.append globs @@ Iter.append formals_in formals_out) + in + ctx +end diff --git a/lib/lang/hm/solve_bv.ml b/lib/lang/hm/solve_bv.ml new file mode 100644 index 00000000..1d00c305 --- /dev/null +++ b/lib/lang/hm/solve_bv.ml @@ -0,0 +1,77 @@ +(** Solve constraint system of dependently width typed bitvectors *) + +open Common +open Abstract_expr +open Hm_types + +module Make (T : TypeExpr.TypeContext) = struct + include Unification.Make (T) + + (** Naive solver *) + + (** Constraints between nat val types. *) + type dependent_bv_constraints = + | Add of { a : Typ.t; b : Typ.t; equ : Typ.t } (** a + b = equ*) + | AddConst of { a : Typ.t; b : int; equ : Typ.t } (** a + b = equ*) + + let show_dependent_bv_constraints = function + | Add { a; b; equ } -> + Printf.sprintf "%s + %s = %s" (type_to_string a) (type_to_string b) + (type_to_string equ) + | AddConst { a; b; equ } -> + Printf.sprintf "%s + (const %d) = %s" (type_to_string a) b + (type_to_string equ) + + (** Deduce the width if two values of the constraint have inferred widths *) + let unify_bv_constraint constr : Typ.t option = + match constr with + | Add { a; b; equ } -> ( + match List.map is_nat_val_type [ find a; find b; find equ ] with + | [ Some a_n; Some b_n; Some e_n ] -> + (* check constraint *) + if a_n + b_n <> e_n then + type_error (fix @@ nat_val_type (a_n + b_n)) equ; + Some equ + | [ Some a_n; Some b_n; None ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (a_n + b_n)) equ) + | [ Some a_n; None; Some e_n ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e_n - a_n)) b) + | [ None; Some b_n; Some e_n ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e_n - b_n)) a) + | _ -> None) + | AddConst { a; b; equ } -> ( + match (is_nat_val_type (find a), is_nat_val_type (find equ)) with + | Some a_n, Some e_n -> + (* check constraint *) + let e = fix @@ nat_val_type (a_n + b) in + Some (unify ~pos:[%here] e equ) + | Some a_n, None -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (a_n + b)) equ) + | None, Some e_n -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e_n - b)) a) + | _ -> None) + + (** Naive solver; loop over constraints and unify until everything is solved. + *) + let solve_constraints ~max_iters cls = + let show = List.to_string ~sep:"\n" show_dependent_bv_constraints in + let rec solve tries cs = + match cs with + | [] -> () + | _ when tries > max_iters -> + raise + (TypeErr + ("Gave up solving bitvec constraints with remaining:\n" ^ show cs)) + | cs -> + let remaining = + List.filter_map + (fun c -> + match unify_bv_constraint c with + | Some e -> None + | None -> Some c) + cs + in + solve (tries + 1) remaining + in + solve 0 cls +end diff --git a/lib/lang/hm/typeExpr.ml b/lib/lang/hm/typeExpr.ml new file mode 100644 index 00000000..8c4f9068 --- /dev/null +++ b/lib/lang/hm/typeExpr.ml @@ -0,0 +1,109 @@ +(** Hash-consed (interned) type expresions with recusion schemes. *) + +open Common +open UnionFind + +type tvar = ID.t [@@deriving eq, ord, show] +(** Type variable identifier *) + +(** Type scoping is handled by "universe" name strings. Hash consing enables + types to be canonically identified by their representation, then looked up + in the union-find datastructure. The union-find datastructrure is used for + type equivalence/unification solving. *) + +module V = struct + (** The keys for the typing context map. We use a simple "universe" string to + distinguish types defined in different scopes (i.e. local variables from + globals.) *) + + type t = { univ : string; v : string } [@@deriving eq, ord, show] + + let hash { univ; v } = Hash.pair Hash.string Hash.string (univ, v) + let to_string { univ; v } = univ ^ "::" ^ v + let local_univ = "" + let global_univ = "" + let proc_univ p = ID.to_string p + let create univ v = { univ; v } + + let of_var univ v = + if Var.is_global v then { univ = global_univ; v = Var.name v } + else { univ; v = Var.name v } +end + +module TCtx = Map.Make (V) +(** The type scheme / typing context : to store a map from scoped type variables + to types. *) + +module ATyp = struct + (** Open recursive type expression, either a variable or type constructor. *) + + type 'a expr = Var of tvar | TypeConstr of 'a list * string + [@@deriving eq, ord, show, map, fold] + + let hash he = function + | Var v -> ID.hash v + | TypeConstr (l, t) -> Hash.pair (Hash.list he) Hash.string (l, t) +end + +(** Create the union find and hash-consing structure for recording type + relations. This must be done each time we want to perform inference in an + independent environment, in order to construct a fresh hash-consing and + union-find state. *) +module MakeFresh () = struct + module Typ = struct + include ATyp + + type t = nt UnionFind.elem Fix.HashCons.cell + and nt = T of t expr + + module Hashed = struct + type t = nt elem + (* we hash cons the data underlying the uf reference so we can construct the + type and get the UF reference *) + + let hash (e : t) : int = + e |> UnionFind.get |> function T e -> ATyp.hash Fix.HashCons.hash e + + let equal (i : t) (j : t) : bool = + match (UnionFind.get i, UnionFind.get j) with + | T i, T j -> ATyp.equal_expr Fix.HashCons.equal i j + end + + open struct + module M = Fix.Memoize.ForHashedType (Hashed) + (** we need to make *) + end + + module H = Fix.HashCons.Make (M) + + let unfix : t -> t expr = + Fix.HashCons.data %> UnionFind.find %> UnionFind.get %> function + | T e -> e + + let fix (e : t expr) : t = H.make (UnionFind.make (T e)) + + let union (a : t) (b : t) : t = + H.make @@ UnionFind.union (Fix.HashCons.data a) (Fix.HashCons.data b) + + (** dubious; has invariant that H.make returns same ref as find ; + - should be true if we don't reassign refs but *) + let find e = Fix.HashCons.data e |> UnionFind.find |> H.make + + let merge f (a : t) (b : t) : t = + H.make + @@ UnionFind.merge + (fun (T a) (T b) -> T (f a b)) + (Fix.HashCons.data a) (Fix.HashCons.data b) + + let compare a b = Fix.HashCons.compare a b + let equal a b = Fix.HashCons.equal a b + end + + (** type name generator *) + let gen = ID.make_gen () + + module Rec = Bincaml_util.Recursionscheme.Recursion (Typ) +end + +module type TypeContext = module type of MakeFresh () +(** Type of mutable type context union find *) diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml new file mode 100644 index 00000000..cce1e5c1 --- /dev/null +++ b/lib/lang/hm/unification.ml @@ -0,0 +1,109 @@ +(** Unification of type expressions *) + +open Common +open Abstract_expr + +module Make (T : TypeExpr.TypeContext) = struct + open TypeExpr + include T + include Typ + open Hm_types + include Hm_types.Make (T) + + let type_error a b = + let a = find a in + let b = find b in + raise + (TypeErr ("type_error: " ^ type_to_string a ^ " <> " ^ type_to_string b)) + + let recursion_error a b = + let b = find b in + raise + (TypeErr + ("recursive: tvar " ^ ID.to_string a ^ " occurs in " ^ type_to_string b)) + + (** Check for type recursion: recursion is failure. *) + let occurs_in a b = + let check = function + | Var t -> equal_tvar t a + | TypeConstr (ls, _) -> List.exists Fun.id ls + in + Rec.cata check b + + (** Type unification.*) + let rec unify ?(pos = Lexing.dummy_pos) t t' = + Logs.debug (fun m -> + m "%s" + ("unify: " ^ plpos pos ^ " " + ^ type_to_string (find t) + ^ " with " + ^ type_to_string (find t'))); + match (map_expr unfix @@ Typ.unfix t, map_expr unfix @@ Typ.unfix t') with + | TypeConstr ([], "nothing"), _ -> t + | _, TypeConstr ([], "nothing") -> t' + | Var x, Var y -> Typ.union t t' + | Var x, _ when occurs_in x t' -> recursion_error x t' + | Var _, TypeConstr _ -> merge (fun a b -> b) t t' + | _, Var x -> unify ~pos:[%here] t' t + | TypeConstr (ars, n), TypeConstr (ars', n') when not (String.equal n n') -> + type_error t t' + | TypeConstr (ars, n), TypeConstr (ars', n') + when List.length ars <> List.length ars' -> + type_error t t' + | ( TypeConstr ([ (Var v as vr) ], "bv"), + TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv") ) + | ( TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv"), + TypeConstr ([ (Var v as vr) ], "bv") ) -> + (* prioritise bitvec consts *) + let v = merge (fun _ c -> c) (fix vr) (fix cst) in + fix @@ TypeConstr ([ v ], "bv") + | TypeConstr (ars, n), TypeConstr (ars', n') -> + let args = + List.combine ars ars' + |> List.map (fun (a, b) -> unify ~pos:[%here] (fix a) (fix b)) + in + merge (fun a b -> TypeConstr (args, n)) t t' + + (** instantiate typescheme for a single type-annotated variable *) + let inst_annot_v ?(no_constraint = false) v = + let ty = + match Var.typ v with + | _ when no_constraint -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) + | Nothing -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) + | o -> ty_of_basil o + in + ty + + (** lookup var and add unify with its type annotation *) + let lookup_var_typ univ ?(no_constraint = false) c v = + let vt = inst_annot_v v in + let a = + let v = V.of_var univ v in + TCtx.find_opt v c |> function + | Some v -> v + | None -> failwith ("var not found: " ^ V.to_string v) + in + let tt = match a with Forall (_, ty) -> union ty vt in + tt + + (** declare type with name in type scheme *) + let decl_type ctx name vt = + let tvar = V.create types_universe name in + TCtx.update tvar + (function + | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) + | None -> Some (Forall ([], vt)) + | _ -> failwith "unk") + ctx + + (** declare var with type in type scheme *) + let decl_var_typ univ ?(no_constraint = false) c v = + let vvar = V.of_var univ v in + let vt = inst_annot_v v in + TCtx.update vvar + (function + | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) + | None -> Some (Forall ([], vt)) + | _ -> failwith "unk") + c +end diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 8b421db7..78c7a68c 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -74,10 +74,10 @@ module WTO = Graph.WeakTopological.Make (G) module RevWTO = Graph.WeakTopological.Make (RevG) type ('v, 'e) proc_spec = { - requires : BasilExpr.t list; - ensures : BasilExpr.t list; - rely : BasilExpr.t list; - guarantee : BasilExpr.t list; + requires : 'e list; + ensures : 'e list; + rely : 'e list; + guarantee : 'e list; captures_globs : 'v list; modifies_globs : 'v list; } @@ -118,10 +118,10 @@ module PG : sig ?formal_out_params:'a StringMap.t -> ?captures_globs:'a list -> ?modifies_globs:'a list -> - ?requires:BasilExpr.t list -> - ?ensures:BasilExpr.t list -> - ?rely:BasilExpr.t list -> - ?guarantee:BasilExpr.t list -> + ?requires:'b list -> + ?ensures:'b list -> + ?rely:'b list -> + ?guarantee:'b list -> ?attrib:Attrib.attrib_map -> unit -> ('a, 'b) t diff --git a/lib/lang/program.mli b/lib/lang/program.mli index ea49abae..c7b77560 100644 --- a/lib/lang/program.mli +++ b/lib/lang/program.mli @@ -51,7 +51,7 @@ type declaration = | Procedure of { definition : proc } val decl_binding : declaration -> string -val pretty_proc : (Var.t, 'a) Procedure.t -> Containers_pp.t +val pretty_proc : (Var.t, Expr.BasilExpr.t) Procedure.t -> Containers_pp.t val pretty_declaration : declaration -> Containers_pp.t type t @@ -90,7 +90,9 @@ val update_proc : t -> t -val output_proc_pretty : out_channel -> (Var.t, 'a) Procedure.t -> unit +val output_proc_pretty : + out_channel -> (Var.t, Expr.BasilExpr.t) Procedure.t -> unit + val prog_pretty : t -> Containers_pp.t val declarations : t -> (ID.t * declaration) CCMap.iter val filter_decls : (ID.t -> declaration -> bool) -> t -> t diff --git a/lib/passes.ml b/lib/passes.ml index 49168f62..e753dd81 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -28,6 +28,14 @@ module PassManager = struct type t = { avail : pass StringMap.t } + let hm_elaborate = + { + name = "hindley-milner-elaborate"; + apply = Prog Hm.elaborate_prog; + invariants = Invariants.make (); + doc = "Perform hindley milner type inference on program"; + } + let chop_unreachable = { name = "trim-unreachable-proc"; @@ -435,6 +443,7 @@ module PassManager = struct let passes = [ lift_intrinsics_aarch64; + hm_elaborate; chop_unreachable; cse_elim; flatten_phis; diff --git a/test/lang/dune b/test/lang/dune index ffb11755..3e4e0560 100644 --- a/test/lang/dune +++ b/test/lang/dune @@ -33,7 +33,12 @@ (library (name test_expr_eval_expect) - (modules test_expr_eval_expect test_stmt test_interp test_expr_hash) + (modules + test_expr_eval_expect + test_stmt + test_interp + test_expr_hash + test_hm_inline) (libraries loader) (inline_tests) (preprocess @@ -63,6 +68,14 @@ (modules test_pagetable_qcheck) (libraries test_pagetable_spec qcheck-core.runner qcheck-stm.sequential)) +(test + (name test_hm) + (package bincaml) + (modules test_hm) + (preprocess + (pps ppx_expect)) + (libraries expr_gen alcotest qcheck-alcotest qcheck-core bincaml.analysis)) + (test (name test_value_soundness) (package bincaml) diff --git a/test/lang/expr_gen.ml b/test/lang/expr_gen.ml index d8428d3d..e0709e3d 100644 --- a/test/lang/expr_gen.ml +++ b/test/lang/expr_gen.ml @@ -60,6 +60,21 @@ let gen_bvconst ?min w = let* c = gen_bv ?min w in return (BasilExpr.bvconst c) +let vname = + let v = int_range 1 3 in + let vl = "abcdefghijklmnopqrstuvwxyz" |> String.to_list in + let vl = vl @ List.map Char.uppercase_ascii vl in + let cs = QCheck.Gen.oneof_list vl in + QCheck.Gen.(string_size ~gen:cs v) + +let gen_bvvar ?min w = + let* n = vname in + return (BasilExpr.rvar (Common.Var.create n (Common.Types.Bitvector w))) + +let gen_boolvar = + let* n = vname in + return (BasilExpr.rvar @@ Var.create n Common.Types.Boolean) + let make_bvconst wd x = BasilExpr.bvconst @@ Bitvec.of_int ~size:wd x let ensure_nonzero wd e = BasilExpr.binexp ~op:`BVOR e (make_bvconst wd 1) @@ -95,14 +110,15 @@ let gen_unop_advanced gen_bvexpr wd = (* assert (BasilExpr.type_of e = Bitvector wd); *) (* e *) -let gen_bvexpr = +let gen_bvexpr ~with_var = fix (fun self (size, wd) -> + let gvs = if with_var then [ (1, gen_bvvar wd) ] else [] in let self wd = self (size / 2, wd) in match size with | 0 -> gen_bvconst wd | size -> - oneof_weighted - [ + oneof_weighted @@ gvs + @ [ (1, gen_bvconst wd); (2, self wd >>= gen_unop); (2, gen_unop_advanced self wd); @@ -126,10 +142,10 @@ let gen_not f = module LT = List.Traverse (QCheck.Gen) -let gen_bv_pred = +let gen_bv_pred ~with_var = let* w = int_range 2 32 in - let* a = gen_bvexpr (2, w) in - let* b = gen_bvexpr (2, w) in + let* a = gen_bvexpr ~with_var (2, w) in + let* b = gen_bvexpr ~with_var (2, w) in let* op = oneof_list bv_binops_pred in return @@ BasilExpr.binexp ~op a b @@ -139,16 +155,17 @@ let gen_pred f = let* op = oneof_list [ `AND; `OR ] in return @@ BasilExpr.applyintrin ~op args -let gen_pred_expr = +let gen_pred_expr ~with_var = fix (fun self size -> let self = self (size / 2) in + let v = if with_var then [ (1, gen_boolvar) ] else [] in match size with | 0 -> gen_bool | size -> - oneof_weighted - [ + oneof_weighted @@ v + @ [ (1, gen_bool); - (2, gen_bv_pred); + (2, gen_bv_pred ~with_var); (2, gen_not self); (2, gen_pred self); ]) @@ -157,10 +174,10 @@ let gen_expr = let gbv = let* wd = int_range 2 65 in let* c = int_bound 3 in - gen_bvexpr (wd, c) + gen_bvexpr ~with_var:false (wd, c) in let gpred = let* c = int_bound 3 in - gen_pred_expr c + gen_pred_expr ~with_var:false c in oneof_weighted [ (1, gpred); (1, gbv) ] diff --git a/test/lang/test_expr_eval_qcheck.ml b/test/lang/test_expr_eval_qcheck.ml index df87dcf6..111d9f55 100644 --- a/test/lang/test_expr_eval_qcheck.ml +++ b/test/lang/test_expr_eval_qcheck.ml @@ -17,9 +17,7 @@ module EvalExprGen = struct let eval_expr = let open QCheck.Gen in let* wd = Expr_gen.gen_width in - Expr_gen.gen_bvexpr (1, wd) - - let arb_bvexpr = QCheck.make ~print:Expr.BasilExpr.to_string_annot eval_expr + Expr_gen.gen_bvexpr ~with_var:false (1, wd) let arb_partial_eval_bvexpr = QCheck.make ~print:(fun (e, p) -> diff --git a/test/lang/test_hm.ml b/test/lang/test_hm.ml new file mode 100644 index 00000000..b99a6fe6 --- /dev/null +++ b/test/lang/test_hm.ml @@ -0,0 +1,61 @@ +open Lang +open Common +open Hm + +module HMDifferential = struct + let arb_expr = + let open QCheck.Gen in + let* wd = Expr_gen.gen_width in + Expr_gen.gen_bvexpr ~with_var:true (5, wd) + + let infer e = + try + Ok + (locally_elaborate_expr e |> Expr.BasilExpr.unfix + |> Expr.AbstractExpr.get_typ) + with e -> Result.of_exn e + + let gener = + QCheck.make ~print:(fun (e, inf_b, inf_hm) -> + Printf.sprintf "%s : %s = %s" + (Expr.BasilExpr.to_string e) + (Types.to_string inf_b) + (Format.sprintf "%a" (Result.pp Types.pp) inf_hm)) + @@ + let open QCheck.Gen in + let* exp = arb_expr in + let inf_b = Expr.BasilExpr.get_typ exp in + let inf_hm = infer exp in + return (exp, inf_b, inf_hm) + + let expect_type_error e = + (* multiple variables with different types *) + let has_type (acc, m) v = + let e = + StringMap.find_opt (Var.name v) m + |> Option.for_all (Types.equal (Var.typ v)) + in + (acc && e, StringMap.add (Var.name v) (Var.typ v) m) + in + let var_types_compat, _ = + Expr.BasilExpr.free_vars_iter e + |> Iter.fold has_type (true, StringMap.empty) + in + not var_types_compat + + let predicate (a, b, hm) = + (expect_type_error a && Result.is_error hm) + || (Result.is_ok hm && Types.equal b (Result.get_ok hm)) + + let test = + QCheck.Test.make ~name:"Hm inference matches" ~count:10000 ~max_fail:1 gener + predicate +end + +let _ = + let suite = + List.map + (QCheck_alcotest.to_alcotest ~long:false ~speed_level:`Quick ~verbose:true) + [ HMDifferential.test ] + in + Alcotest.run "hm" [ ("diff", suite) ] diff --git a/test/lang/test_hm_inline.ml b/test/lang/test_hm_inline.ml new file mode 100644 index 00000000..e7fea613 --- /dev/null +++ b/test/lang/test_hm_inline.ml @@ -0,0 +1,25 @@ +open Lang +open Common +open Hm + +let%expect_test "return type of function" = + let open Types in + let args = [ Bitvector 64 ] in + let ft = Map (Bitvector 64, Map (Bitvector 64, Bitvector 64)) in + Printf.printf "function type: %s\n" (Types.to_string ft); + let _, ort = Types.uncurry ft in + Printf.printf "uncurry ret type: %s\n" (Types.to_string ort); + Format.force_newline (); + Format.printf "%s%a%a" "partially apply bv64: " (Result.pp Types.pp) + (type_applied ft args) Format.newline (); + Format.printf "%s%a%a" "type error: " (Result.pp Types.pp) + (type_applied ft [ Bitvector 24 ]) + Format.newline (); + [%expect + {| + function type: ((bv64)->(bv64->bv64)) + uncurry ret type: bv64 + + partially apply bv64: ok((bv64->bv64)) + type error: error(type_error: 64 <> 24) + |}] diff --git a/test/lang/test_value_soundness.ml b/test/lang/test_value_soundness.ml index 67064ca3..12659161 100644 --- a/test/lang/test_value_soundness.ml +++ b/test/lang/test_value_soundness.ml @@ -11,7 +11,8 @@ struct let arb_expr = let open QCheck.Gen in let* wd = Expr_gen.gen_width in - Expr_gen.gen_bvexpr (5, wd) + (* FIXME: soundness issues when variables *) + Expr_gen.gen_bvexpr ~with_var:false (5, wd) let arb_val = let open QCheck.Gen in @@ -37,7 +38,7 @@ struct let eval_abs e = Eval.eval Ops.AllOps.show_const Ops.AllOps.show_unary Ops.AllOps.show_binary Ops.AllOps.show_intrin - (fun _ -> failwith "no vars") + (fun _ -> V.top) e let join_symm (l, r) =